bench/check-ce/oracles/jlamp_array_poly_Z3,4.8.10_SP.oracle

   1 <check_ce:categorization>Categorizations of models:
   2 - Checked model 0: INCOMPLETE
   3   - Concrete RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
   4   - Abstract RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
   5 - Selected model 1: INCOMPLETE
   6   - Concrete RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
   7   - Abstract RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
   8 File "bench/check-ce/jlamp_array_poly.mlw", line 22, characters 4-16:
   9 Sub-goal Index in array bounds of goal f'vc.
  10 Prover result is: Unknown (unknown) (21161 steps).
  11 The following counterexample model could not be verified
  12   (both RAC terminated because Precondition of `f` cannot be evaluated):
  13 File jlamp_array_poly.mlw:
  14   Line 8:
  15     to_int : t -> int = [|{to_int => 2} => 2; {to_int => 3} => 3; _ => 2|]
  16   Line 11:
  17     two : t = {to_int => 2}
  18   Line 14:
  19     three : t = {to_int => 3}
  20   Line 18:
  21     a :  = [|_ => epsilon _. true|]
  22     a :  = [|_ => epsilon _. true|]
  23
  24 <check_ce:categorization>Categorizations of models:
  25 - Checked model 0: INCOMPLETE
  26   - Concrete RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
  27   - Abstract RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
  28 - Selected model 1: INCOMPLETE
  29   - Concrete RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
  30   - Abstract RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
  31 File "bench/check-ce/jlamp_array_poly.mlw", line 21, characters 14-27:
  32 Sub-goal Postcondition of goal f'vc.
  33 Prover result is: Step limit exceeded (3000048 steps).
  34 The following counterexample model could not be verified
  35   (both RAC terminated because Precondition of `f` cannot be evaluated):
  36 File jlamp_array_poly.mlw:
  37   Line 11:
  38     two :  = "undefined"
  39   Line 14:
  40     three :  = "undefined"
  41   Line 18:
  42     a :  = [|_ => epsilon _. true|]
  43     a :  = [|_ => epsilon _. true|]
  44
  45 File "bench/check-ce/jlamp_array_poly.mlw", line 28, characters 4-16:
  46 Sub-goal Index in array bounds of goal g'vc.
  47 Prover result is: Valid (4323 steps).
  48
  49 <check_ce:categorization>Categorizations of models:
  50 - Checked model 0: BAD_CE
  51   - Concrete RAC: STUCK (failure in precondition of `g` at "bench/check-ce/jlamp_array_poly.mlw", line 24, characters 6-7)
  52   - Abstract RAC: STUCK (failure in precondition of `g` at "bench/check-ce/jlamp_array_poly.mlw", line 24, characters 6-7)
  53 - Selected model 1: BAD_CE
  54   - Concrete RAC: STUCK (failure in precondition of `g` at "bench/check-ce/jlamp_array_poly.mlw", line 24, characters 6-7)
  55   - Abstract RAC: STUCK (failure in precondition of `g` at "bench/check-ce/jlamp_array_poly.mlw", line 24, characters 6-7)
  56 File "bench/check-ce/jlamp_array_poly.mlw", line 27, characters 14-27:
  57 Sub-goal Postcondition of goal g'vc.
  58 Prover result is: Step limit exceeded (3000053 steps).
  59 Sorry, we don't have a good counterexample for you :(
  60
  61
  62 File "bench/check-ce/jlamp_array_poly.mlw", line 34, characters 4-16:
  63 Sub-goal Index in array bounds of goal h'vc.
  64 Prover result is: Valid (4323 steps).
  65
  66 <check_ce:categorization>Categorizations of models:
  67 - Checked model 0: BAD_CE
  68   - Concrete RAC: STUCK (failure in precondition of `h` at "bench/check-ce/jlamp_array_poly.mlw", line 30, characters 6-7)
  69   - Abstract RAC: STUCK (failure in precondition of `h` at "bench/check-ce/jlamp_array_poly.mlw", line 30, characters 6-7)
  70 - Selected model 1: BAD_CE
  71   - Concrete RAC: STUCK (failure in precondition of `h` at "bench/check-ce/jlamp_array_poly.mlw", line 30, characters 6-7)
  72   - Abstract RAC: STUCK (failure in precondition of `h` at "bench/check-ce/jlamp_array_poly.mlw", line 30, characters 6-7)
  73 File "bench/check-ce/jlamp_array_poly.mlw", line 33, characters 14-27:
  74 Sub-goal Postcondition of goal h'vc.
  75 Prover result is: Step limit exceeded (3000053 steps).
  76 Sorry, we don't have a good counterexample for you :(
  77
  78