bench/check-ce/oracles/jlamp_array_poly_Alt-Ergo,2.5.4_WP.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 - Checked model 1: INCOMPLETE
   6   - Concrete RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
   7   - Abstract RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
   8 - Selected model 2: INCOMPLETE
   9   - Concrete RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  10   - Abstract RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  11 File "bench/check-ce/jlamp_array_poly.mlw", line 22, characters 4-16:
  12 Sub-goal Index in array bounds of goal f'vc.
  13 Prover result is: Unknown (unknown) (5 steps).
  14 The following counterexample model could not be verified
  15   (both RAC fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds):
  16 File jlamp_array_poly.mlw:
  17   Line 8:
  18     to_int : t -> int = [|{to_int => 3} => 3; _ => 2|]
  19   Line 11:
  20     two : t = {to_int => 2}
  21   Line 14:
  22     three : t = {to_int => 2}
  23   Line 18:
  24     a :  = [|_ => epsilon _. true|]
  25     a :  = [|_ => epsilon _. true|]
  26
  27 <check_ce:categorization>Categorizations of models:
  28 - Checked model 0: 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 - Checked model 1: INCOMPLETE
  32   - Concrete RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  33   - Abstract RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  34 - Selected model 2: INCOMPLETE
  35   - Concrete RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  36   - Abstract RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  37 File "bench/check-ce/jlamp_array_poly.mlw", line 21, characters 14-27:
  38 Sub-goal Postcondition of goal f'vc.
  39 Prover result is: Unknown (unknown) (10 steps).
  40 The following counterexample model could not be verified
  41   (both RAC fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds):
  42 File jlamp_array_poly.mlw:
  43   Line 8:
  44     to_int : t -> int = [|{to_int => 3} => 3; _ => 2|]
  45   Line 11:
  46     two : t = {to_int => 2}
  47   Line 14:
  48     three : t = {to_int => 2}
  49   Line 18:
  50     a :  = [|_ => epsilon _. true|]
  51     a :  = [|_ => epsilon _. true|]
  52
  53 File "bench/check-ce/jlamp_array_poly.mlw", line 28, characters 4-16:
  54 Sub-goal Index in array bounds of goal g'vc.
  55 Prover result is: Valid (4 steps).
  56
  57 <check_ce:categorization>Categorizations of models:
  58 - Checked model 0: BAD_CE
  59   - Concrete RAC: STUCK (failure in precondition of `g` at "bench/check-ce/jlamp_array_poly.mlw", line 24, characters 6-7)
  60   - Abstract RAC: STUCK (failure in precondition of `g` at "bench/check-ce/jlamp_array_poly.mlw", line 24, characters 6-7)
  61 - Checked model 1: INCOMPLETE
  62   - Concrete RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  63   - Abstract RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  64 - Selected model 2: INCOMPLETE
  65   - Concrete RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  66   - Abstract RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  67 File "bench/check-ce/jlamp_array_poly.mlw", line 27, characters 14-27:
  68 Sub-goal Postcondition of goal g'vc.
  69 Prover result is: Unknown (unknown) (15 steps).
  70 The following counterexample model could not be verified
  71   (both RAC fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds):
  72 File jlamp_array_poly.mlw:
  73   Line 8:
  74     to_int : t -> int = [|{to_int => 3} => 3; _ => 2|]
  75   Line 11:
  76     two : t = {to_int => 2}
  77   Line 14:
  78     three : t = {to_int => 2}
  79   Line 24:
  80     a :  = [|_ => epsilon _. true|]
  81     a :  = [|_ => epsilon _. true|]
  82
  83 File "bench/check-ce/jlamp_array_poly.mlw", line 34, characters 4-16:
  84 Sub-goal Index in array bounds of goal h'vc.
  85 Prover result is: Valid (4 steps).
  86
  87 <check_ce:categorization>Categorizations of models:
  88 - Checked model 0: BAD_CE
  89   - Concrete RAC: STUCK (failure in precondition of `h` at "bench/check-ce/jlamp_array_poly.mlw", line 30, characters 6-7)
  90   - Abstract RAC: STUCK (failure in precondition of `h` at "bench/check-ce/jlamp_array_poly.mlw", line 30, characters 6-7)
  91 - Checked model 1: INCOMPLETE
  92   - Concrete RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  93   - Abstract RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  94 - Selected model 2: INCOMPLETE
  95   - Concrete RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  96   - Abstract RAC: INCOMPLETE (fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds)
  97 File "bench/check-ce/jlamp_array_poly.mlw", line 33, characters 14-27:
  98 Sub-goal Postcondition of goal h'vc.
  99 Prover result is: Unknown (unknown) (16 steps).
 100 The following counterexample model could not be verified
 101   (both RAC fatal rac error: cannot evaluate builtin ([]<-) because index is out of bounds):
 102 File jlamp_array_poly.mlw:
 103   Line 8:
 104     to_int : t -> int = [|{to_int => 3} => 3; _ => 2|]
 105   Line 11:
 106     two : t = {to_int => 2}
 107   Line 14:
 108     three : t = {to_int => 2}
 109   Line 30:
 110     a :  = [|_ => epsilon _. true|]
 111     a :  = [|_ => epsilon _. true|]
 112