bench/check-ce/oracles/703_reduce_term_Z3,4.8.10_SP.oracle

   1 Warning: term reduction aborted (term size blows up from 289 to 491721, after 278 steps).
   2
   3 Warning: term reduction aborted (takes more than 1024 steps).
   4
   5 Warning: term reduction aborted (term size blows up from 289 to 491721, after 278 steps).
   6
   7 Warning: term reduction aborted (takes more than 1024 steps).
   8
   9 Warning: term reduction aborted (term size blows up from 289 to 491721, after 278 steps).
  10
  11 Warning: term reduction aborted (takes more than 1024 steps).
  12
  13 Warning: term reduction aborted (term size blows up from 289 to 491721, after 278 steps).
  14
  15 Warning: term reduction aborted (takes more than 1024 steps).
  16
  17 <check_ce:categorization>Categorizations of models:
  18 - Selected model 0: INCOMPLETE
  19   - Concrete RAC: INCOMPLETE (terminated because Precondition of `local` cannot be evaluated)
  20   - Abstract RAC: INCOMPLETE (terminated because Precondition of `local` cannot be evaluated)
  21 - Checked model 1: INCOMPLETE
  22   - Concrete RAC: INCOMPLETE (terminated because Precondition of `local` cannot be evaluated)
  23   - Abstract RAC: INCOMPLETE (terminated because Precondition of `local` cannot be evaluated)
  24 File "bench/check-ce/703_reduce_term.mlw", line 391, characters 4-55:
  25 Sub-goal Precondition of goal def'vc.
  26 Prover result is: Step limit exceeded (500114 steps).
  27 The following counterexample model could not be verified
  28   (both RAC terminated because Precondition of `local` cannot be evaluated):
  29 File 703_reduce_term.mlw:
  30   Line 5:
  31     base : t = #x00000001
  32     base : t = #x00000001
  33   Line 13:
  34     oor :
  35       t
  36       ->
  37       t
  38       ->
  39       t = fun x!01 x!11 ->
  40            if x!01 = #x00000000 /\ x!11 = #x00000001 then #x00000000
  41            else if x!01 = #x00000000 /\ x!11 = #x00000002 then #x00000000
  42                 else if x!01 = #x00000000 /\ x!11 = #x00000004
  43                      then #x00000000
  44                      else if x!01 = #x00000000 /\ x!11 = #x00000008
  45                           then #x00000000
  46                           else if x!01 = #x00000000 /\ x!11 = #x00000010
  47                                then #x00000000
  48                                else if x!01 = #x00000000 /\ x!11 = #x00000020
  49                                     then #x00000000
  50                                     else if x!01 = #x00000000 /\
  51                                             x!11 = #x00000040
  52                                          then #x00000000
  53                                          else if x!01 = #x00000000 /\
  54                                                  x!11 = #x00000080
  55                                               then #x00000000
  56                                               else if x!01 = #x00000000 /\
  57                                                       x!11 = #x00000100
  58                                                    then #x00000000
  59                                                    else if x!01 = #x00000000 /\
  60                                                            x!11 = #x00000200
  61                                                         then #x00000000
  62                                                         else if x!01 = #x00000000 /\
  63                                                                 x!11 = #x00000400
  64                                                              then #x00000000
  65                                                              else if
  66                                                                   x!01 = #x00000000 /\
  67                                                                   x!11 = #x00000800
  68                                                                   then #x00000000
  69                                                                   else
  70                                                                   if
  71                                                                   x!01 = #x00000000 /\
  72                                                                   x!11 = #x00001000
  73                                                                   then #x00000000
  74                                                                   else
  75                                                                   if
  76                                                                   x!01 = #x00000000 /\
  77                                                                   x!11 = #x00002000
  78                                                                   then #x00000000
  79                                                                   else
  80                                                                   if
  81                                                                   x!01 = #x00000000 /\
  82                                                                   x!11 = #x00004000
  83                                                                   then #x00000000
  84                                                                   else
  85                                                                   if
  86                                                                   x!01 = #x00000000 /\
  87                                                                   x!11 = #x00008000
  88                                                                   then #x00000000
  89                                                                   else
  90                                                                   if
  91                                                                   x!01 = #x00000000 /\
  92                                                                   x!11 = #x00010000
  93                                                                   then #x00000000
  94                                                                   else
  95                                                                   if
  96                                                                   x!01 = #x00000000 /\
  97                                                                   x!11 = #x00020000
  98                                                                   then #x00000000
  99                                                                   else
 100                                                                   if
 101                                                                   x!01 = #x00000000 /\
 102                                                                   x!11 = #x00040000
 103                                                                   then #x00000000
 104                                                                   else
 105                                                                   if
 106                                                                   x!01 = #x00000000 /\
 107                                                                   x!11 = #x00080000
 108                                                                   then #x00000000
 109                                                                   else
 110                                                                   if
 111                                                                   x!01 = #x00000000 /\
 112                                                                   x!11 = #x00100000
 113                                                                   then #x00000000
 114                                                                   else
 115                                                                   if
 116                                                                   x!01 = #x00000000 /\
 117                                                                   x!11 = #x00200000
 118                                                                   then #x00000000
 119                                                                   else
 120                                                                   if
 121                                                                   x!01 = #x00000000 /\
 122                                                                   x!11 = #x00400000
 123                                                                   then #x00000000
 124                                                                   else
 125                                                                   if
 126                                                                   x!01 = #x00000000 /\
 127                                                                   x!11 = #x00800000
 128                                                                   then #x00000000
 129                                                                   else
 130                                                                   if
 131                                                                   x!01 = #x00000000 /\
 132                                                                   x!11 = #x01000000
 133                                                                   then #x00000000
 134                                                                   else #x00000000
 135     oor :
 136       t
 137       ->
 138       t
 139       ->
 140       t = fun x!01 x!11 ->
 141            if x!01 = #x00000000 /\ x!11 = #x00000001 then #x00000000
 142            else if x!01 = #x00000000 /\ x!11 = #x00000002 then #x00000000
 143                 else if x!01 = #x00000000 /\ x!11 = #x00000004
 144                      then #x00000000
 145                      else if x!01 = #x00000000 /\ x!11 = #x00000008
 146                           then #x00000000
 147                           else if x!01 = #x00000000 /\ x!11 = #x00000010
 148                                then #x00000000
 149                                else if x!01 = #x00000000 /\ x!11 = #x00000020
 150                                     then #x00000000
 151                                     else if x!01 = #x00000000 /\
 152                                             x!11 = #x00000040
 153                                          then #x00000000
 154                                          else if x!01 = #x00000000 /\
 155                                                  x!11 = #x00000080
 156                                               then #x00000000
 157                                               else if x!01 = #x00000000 /\
 158                                                       x!11 = #x00000100
 159                                                    then #x00000000
 160                                                    else if x!01 = #x00000000 /\
 161                                                            x!11 = #x00000200
 162                                                         then #x00000000
 163                                                         else if x!01 = #x00000000 /\
 164                                                                 x!11 = #x00000400
 165                                                              then #x00000000
 166                                                              else if
 167                                                                   x!01 = #x00000000 /\
 168                                                                   x!11 = #x00000800
 169                                                                   then #x00000000
 170                                                                   else
 171                                                                   if
 172                                                                   x!01 = #x00000000 /\
 173                                                                   x!11 = #x00001000
 174                                                                   then #x00000000
 175                                                                   else
 176                                                                   if
 177                                                                   x!01 = #x00000000 /\
 178                                                                   x!11 = #x00002000
 179                                                                   then #x00000000
 180                                                                   else
 181                                                                   if
 182                                                                   x!01 = #x00000000 /\
 183                                                                   x!11 = #x00004000
 184                                                                   then #x00000000
 185                                                                   else
 186                                                                   if
 187                                                                   x!01 = #x00000000 /\
 188                                                                   x!11 = #x00008000
 189                                                                   then #x00000000
 190                                                                   else
 191                                                                   if
 192                                                                   x!01 = #x00000000 /\
 193                                                                   x!11 = #x00010000
 194                                                                   then #x00000000
 195                                                                   else
 196                                                                   if
 197                                                                   x!01 = #x00000000 /\
 198                                                                   x!11 = #x00020000
 199                                                                   then #x00000000
 200                                                                   else
 201                                                                   if
 202                                                                   x!01 = #x00000000 /\
 203                                                                   x!11 = #x00040000
 204                                                                   then #x00000000
 205                                                                   else
 206                                                                   if
 207                                                                   x!01 = #x00000000 /\
 208                                                                   x!11 = #x00080000
 209                                                                   then #x00000000
 210                                                                   else
 211                                                                   if
 212                                                                   x!01 = #x00000000 /\
 213                                                                   x!11 = #x00100000
 214                                                                   then #x00000000
 215                                                                   else
 216                                                                   if
 217                                                                   x!01 = #x00000000 /\
 218                                                                   x!11 = #x00200000
 219                                                                   then #x00000000
 220                                                                   else
 221                                                                   if
 222                                                                   x!01 = #x00000000 /\
 223                                                                   x!11 = #x00400000
 224                                                                   then #x00000000
 225                                                                   else
 226                                                                   if
 227                                                                   x!01 = #x00000000 /\
 228                                                                   x!11 = #x00800000
 229                                                                   then #x00000000
 230                                                                   else
 231                                                                   if
 232                                                                   x!01 = #x00000000 /\
 233                                                                   x!11 = #x01000000
 234                                                                   then #x00000000
 235                                                                   else #x00000000
 236   Line 16:
 237     oor__function_guard :
 238       t
 239       ->
 240       t
 241       ->
 242       t
 243       ->
 244       t = fun x!0 x!1 x!2 ->
 245            if x!0 = #x00000000 /\ x!1 = #x00000000 /\ x!2 = #x00000001
 246            then #x00000000
 247            else if x!0 = #x00000000 /\ x!1 = #x00000000 /\ x!2 = #x00000002
 248                 then #x00000000
 249                 else if x!0 = #x00000000 /\ x!1 = #x00000000 /\
 250                         x!2 = #x00000004
 251                      then #x00000000
 252                      else if x!0 = #x00000000 /\ x!1 = #x00000000 /\
 253                              x!2 = #x00000008
 254                           then #x00000000
 255                           else if x!0 = #x00000000 /\ x!1 = #x00000000 /\
 256                                   x!2 = #x00000010
 257                                then #x00000000
 258                                else if x!0 = #x00000000 /\ x!1 = #x00000000 /\
 259                                        x!2 = #x00000020
 260                                     then #x00000000
 261                                     else if x!0 = #x00000000 /\
 262                                             x!1 = #x00000000 /\
 263                                             x!2 = #x00000040
 264                                          then #x00000000
 265                                          else if x!0 = #x00000000 /\
 266                                                  x!1 = #x00000000 /\
 267                                                  x!2 = #x00000080
 268                                               then #x00000000
 269                                               else if x!0 = #x00000000 /\
 270                                                       x!1 = #x00000000 /\
 271                                                       x!2 = #x00000100
 272                                                    then #x00000000
 273                                                    else if x!0 = #x00000000 /\
 274                                                            x!1 = #x00000000 /\
 275                                                            x!2 = #x00000200
 276                                                         then #x00000000
 277                                                         else if x!0 = #x00000000 /\
 278                                                                 x!1 = #x00000000 /\
 279                                                                 x!2 = #x00000400
 280                                                              then #x00000000
 281                                                              else if
 282                                                                   x!0 = #x00000000 /\
 283                                                                   x!1 = #x00000000 /\
 284                                                                   x!2 = #x00000800
 285                                                                   then #x00000000
 286                                                                   else
 287                                                                   if
 288                                                                   x!0 = #x00000000 /\
 289                                                                   x!1 = #x00000000 /\
 290                                                                   x!2 = #x00001000
 291                                                                   then #x00000000
 292                                                                   else
 293                                                                   if
 294                                                                   x!0 = #x00000000 /\
 295                                                                   x!1 = #x00000000 /\
 296                                                                   x!2 = #x00002000
 297                                                                   then #x00000000
 298                                                                   else
 299                                                                   if
 300                                                                   x!0 = #x00000000 /\
 301                                                                   x!1 = #x00000000 /\
 302                                                                   x!2 = #x00004000
 303                                                                   then #x00000000
 304                                                                   else
 305                                                                   if
 306                                                                   x!0 = #x00000000 /\
 307                                                                   x!1 = #x00000000 /\
 308                                                                   x!2 = #x00008000
 309                                                                   then #x00000000
 310                                                                   else
 311                                                                   if
 312                                                                   x!0 = #x00000000 /\
 313                                                                   x!1 = #x00000000 /\
 314                                                                   x!2 = #x00010000
 315                                                                   then #x00000000
 316                                                                   else
 317                                                                   if
 318                                                                   x!0 = #x00000000 /\
 319                                                                   x!1 = #x00000000 /\
 320                                                                   x!2 = #x00020000
 321                                                                   then #x00000000
 322                                                                   else
 323                                                                   if
 324                                                                   x!0 = #x00000000 /\
 325                                                                   x!1 = #x00000000 /\
 326                                                                   x!2 = #x00040000
 327                                                                   then #x00000000
 328                                                                   else
 329                                                                   if
 330                                                                   x!0 = #x00000000 /\
 331                                                                   x!1 = #x00000000 /\
 332                                                                   x!2 = #x00080000
 333                                                                   then #x00000000
 334                                                                   else
 335                                                                   if
 336                                                                   x!0 = #x00000000 /\
 337                                                                   x!1 = #x00000000 /\
 338                                                                   x!2 = #x00100000
 339                                                                   then #x00000000
 340                                                                   else
 341                                                                   if
 342                                                                   x!0 = #x00000000 /\
 343                                                                   x!1 = #x00000000 /\
 344                                                                   x!2 = #x00200000
 345                                                                   then #x00000000
 346                                                                   else
 347                                                                   if
 348                                                                   x!0 = #x00000000 /\
 349                                                                   x!1 = #x00000000 /\
 350                                                                   x!2 = #x00400000
 351                                                                   then #x00000000
 352                                                                   else
 353                                                                   if
 354                                                                   x!0 = #x00000000 /\
 355                                                                   x!1 = #x00000000 /\
 356                                                                   x!2 = #x00800000
 357                                                                   then #x00000000
 358                                                                   else
 359                                                                   if
 360                                                                   x!0 = #x00000000 /\
 361                                                                   x!1 = #x00000000 /\
 362                                                                   x!2 = #x01000000
 363                                                                   then #x00000000
 364                                                                   else #x00000000
 365     oor__function_guard :
 366       t
 367       ->
 368       t
 369       ->
 370       t
 371       ->
 372       t = fun x!0 x!1 x!2 ->
 373            if x!0 = #x00000000 /\ x!1 = #x00000000 /\ x!2 = #x00000001
 374            then #x00000000
 375            else if x!0 = #x00000000 /\ x!1 = #x00000000 /\ x!2 = #x00000002
 376                 then #x00000000
 377                 else if x!0 = #x00000000 /\ x!1 = #x00000000 /\
 378                         x!2 = #x00000004
 379                      then #x00000000
 380                      else if x!0 = #x00000000 /\ x!1 = #x00000000 /\
 381                              x!2 = #x00000008
 382                           then #x00000000
 383                           else if x!0 = #x00000000 /\ x!1 = #x00000000 /\
 384                                   x!2 = #x00000010
 385                                then #x00000000
 386                                else if x!0 = #x00000000 /\ x!1 = #x00000000 /\
 387                                        x!2 = #x00000020
 388                                     then #x00000000
 389                                     else if x!0 = #x00000000 /\
 390                                             x!1 = #x00000000 /\
 391                                             x!2 = #x00000040
 392                                          then #x00000000
 393                                          else if x!0 = #x00000000 /\
 394                                                  x!1 = #x00000000 /\
 395                                                  x!2 = #x00000080
 396                                               then #x00000000
 397                                               else if x!0 = #x00000000 /\
 398                                                       x!1 = #x00000000 /\
 399                                                       x!2 = #x00000100
 400                                                    then #x00000000
 401                                                    else if x!0 = #x00000000 /\
 402                                                            x!1 = #x00000000 /\
 403                                                            x!2 = #x00000200
 404                                                         then #x00000000
 405                                                         else if x!0 = #x00000000 /\
 406                                                                 x!1 = #x00000000 /\
 407                                                                 x!2 = #x00000400
 408                                                              then #x00000000
 409                                                              else if
 410                                                                   x!0 = #x00000000 /\
 411                                                                   x!1 = #x00000000 /\
 412                                                                   x!2 = #x00000800
 413                                                                   then #x00000000
 414                                                                   else
 415                                                                   if
 416                                                                   x!0 = #x00000000 /\
 417                                                                   x!1 = #x00000000 /\
 418                                                                   x!2 = #x00001000
 419                                                                   then #x00000000
 420                                                                   else
 421                                                                   if
 422                                                                   x!0 = #x00000000 /\
 423                                                                   x!1 = #x00000000 /\
 424                                                                   x!2 = #x00002000
 425                                                                   then #x00000000
 426                                                                   else
 427                                                                   if
 428                                                                   x!0 = #x00000000 /\
 429                                                                   x!1 = #x00000000 /\
 430                                                                   x!2 = #x00004000
 431                                                                   then #x00000000
 432                                                                   else
 433                                                                   if
 434                                                                   x!0 = #x00000000 /\
 435                                                                   x!1 = #x00000000 /\
 436                                                                   x!2 = #x00008000
 437                                                                   then #x00000000
 438                                                                   else
 439                                                                   if
 440                                                                   x!0 = #x00000000 /\
 441                                                                   x!1 = #x00000000 /\
 442                                                                   x!2 = #x00010000
 443                                                                   then #x00000000
 444                                                                   else
 445                                                                   if
 446                                                                   x!0 = #x00000000 /\
 447                                                                   x!1 = #x00000000 /\
 448                                                                   x!2 = #x00020000
 449                                                                   then #x00000000
 450                                                                   else
 451                                                                   if
 452                                                                   x!0 = #x00000000 /\
 453                                                                   x!1 = #x00000000 /\
 454                                                                   x!2 = #x00040000
 455                                                                   then #x00000000
 456                                                                   else
 457                                                                   if
 458                                                                   x!0 = #x00000000 /\
 459                                                                   x!1 = #x00000000 /\
 460                                                                   x!2 = #x00080000
 461                                                                   then #x00000000
 462                                                                   else
 463                                                                   if
 464                                                                   x!0 = #x00000000 /\
 465                                                                   x!1 = #x00000000 /\
 466                                                                   x!2 = #x00100000
 467                                                                   then #x00000000
 468                                                                   else
 469                                                                   if
 470                                                                   x!0 = #x00000000 /\
 471                                                                   x!1 = #x00000000 /\
 472                                                                   x!2 = #x00200000
 473                                                                   then #x00000000
 474                                                                   else
 475                                                                   if
 476                                                                   x!0 = #x00000000 /\
 477                                                                   x!1 = #x00000000 /\
 478                                                                   x!2 = #x00400000
 479                                                                   then #x00000000
 480                                                                   else
 481                                                                   if
 482                                                                   x!0 = #x00000000 /\
 483                                                                   x!1 = #x00000000 /\
 484                                                                   x!2 = #x00800000
 485                                                                   then #x00000000
 486                                                                   else
 487                                                                   if
 488                                                                   x!0 = #x00000000 /\
 489                                                                   x!1 = #x00000000 /\
 490                                                                   x!2 = #x01000000
 491                                                                   then #x00000000
 492                                                                   else #x00000000
 493   Line 24:
 494     oand :
 495       t
 496       ->
 497       t
 498       ->
 499       t = fun x!03 x!13 ->
 500            if x!03 = #x00000001 /\ x!13 = #x00000000 then #x00000000
 501            else #x00000000
 502     oand :
 503       t
 504       ->
 505       t
 506       ->
 507       t = fun x!03 x!13 ->
 508            if x!03 = #x00000001 /\ x!13 = #x00000000 then #x00000000
 509            else #x00000000
 510   Line 27:
 511     oand__function_guard :
 512       t
 513       ->
 514       t
 515       ->
 516       t
 517       ->
 518       t = fun x!02 x!12 x!21 ->
 519            if x!02 = #x00000000 /\ x!12 = #x00000001 /\ x!21 = #x00000000
 520            then #x00000000 else #x00000000
 521     oand__function_guard :
 522       t
 523       ->
 524       t
 525       ->
 526       t
 527       ->
 528       t = fun x!02 x!12 x!21 ->
 529            if x!02 = #x00000000 /\ x!12 = #x00000001 /\ x!21 = #x00000000
 530            then #x00000000 else #x00000000
 531   Line 391:
 532     base : t = #x00000001
 533     base : t = #x00000001
 534