bench/check-ce/oracles/tuple1_CVC4,1.8_WP.oracle

   1 <check_ce:categorization>Categorizations of models:
   2 - Checked model 0: INCOMPLETE
   3   - Concrete RAC: INCOMPLETE (terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45)
   4   - Abstract RAC: INCOMPLETE (terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45)
   5 - Selected model 1: INCOMPLETE
   6   - Concrete RAC: INCOMPLETE (terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45)
   7   - Abstract RAC: INCOMPLETE (terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45)
   8 File "bench/check-ce/tuple1.mlw", line 7, characters 14-19:
   9 Sub-goal Integer overflow of goal swap'vc.
  10 Prover result is: Unknown (unknown + incomplete) (2681 steps).
  11 The following counterexample model could not be verified
  12   (both RAC terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45):
  13 File int.mlw:
  14   Line 459:
  15     int63'int :
  16       int63
  17       ->
  18       int = fun bOUND_VARIABLE_4561 ->
  19              if {mach.int.Int63.int63'int => -4611686018427387903} = bOUND_VARIABLE_4561
  20              then -4611686018427387903
  21              else if {mach.int.Int63.int63'int => -4611686018427387904} = bOUND_VARIABLE_4561
  22                   then -4611686018427387904
  23                   else if {mach.int.Int63.int63'int => 4611686018427387903} = bOUND_VARIABLE_4561
  24                        then 4611686018427387903 else -4611686018427387902
  25   Line 475:
  26     max_int : int63 = {mach.int.Int63.int63'int => 4611686018427387903}
  27   Line 477:
  28     min_int : int63 = {mach.int.Int63.int63'int => -4611686018427387904}
  29 File tuple1.mlw:
  30   Line 6:
  31     a : int63 = {mach.int.Int63.int63'int => -4611686018427387903}
  32     b : int63 = {mach.int.Int63.int63'int => -4611686018427387902}
  33   Line 7:
  34     a : int63 = {mach.int.Int63.int63'int => -4611686018427387903}
  35     b : int63 = {mach.int.Int63.int63'int => -4611686018427387902}
  36
  37 File "bench/check-ce/tuple1.mlw", line 7, characters 14-23:
  38 Sub-goal Integer overflow of goal swap'vc.
  39 Prover result is: Valid (1709 steps).
  40
  41 File "bench/check-ce/tuple1.mlw", line 7, characters 3-8:
  42 Sub-goal Integer overflow of goal swap'vc.
  43 Prover result is: Valid (1793 steps).
  44
  45 File "bench/check-ce/tuple1.mlw", line 7, characters 3-12:
  46 Sub-goal Integer overflow of goal swap'vc.
  47 Prover result is: Valid (1869 steps).
  48
  49 File "bench/check-ce/tuple1.mlw", line 5, characters 38-43:
  50 Sub-goal Postcondition of goal swap'vc.
  51 Prover result is: Valid (3287 steps).
  52