bench/check-ce/oracles/jlamp_array_mono_Alt-Ergo,2.5.4_SP.oracle

   1 File bench/check-ce/jlamp_array_mono.mlw:
   2 Goal array'vc.
   3 Prover result is: Valid (2 steps).
   4
   5 <check_ce:categorization>Categorizations of models:
   6 - Selected model 0: INCOMPLETE
   7   - Concrete RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
   8   - Abstract RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
   9 - Checked model 1: INCOMPLETE
  10   - Concrete RAC: INCOMPLETE (terminated with uncaught exception `Failure("set_constr")`)
  11   - Abstract RAC: INCOMPLETE (terminated with uncaught exception `Failure("set_constr")`)
  12 - Checked model 2: INCOMPLETE
  13   - Concrete RAC: INCOMPLETE (terminated with uncaught exception `Failure("set_constr")`)
  14   - Abstract RAC: INCOMPLETE (terminated with uncaught exception `Failure("set_constr")`)
  15 File "bench/check-ce/jlamp_array_mono.mlw", line 48, characters 4-16:
  16 Sub-goal Index in array bounds of goal f'vc.
  17 Prover result is: Unknown (unknown) (5 steps).
  18 The following counterexample model could not be verified
  19   (both RAC terminated because Precondition of `f` cannot be evaluated):
  20 File jlamp_array_mono.mlw:
  21   Line 11:
  22     two :  = "undefined"
  23   Line 14:
  24     three :  = "undefined"
  25   Line 44:
  26     a :  = "undefined"
  27     a :  = "undefined"
  28
  29 <check_ce:categorization>Categorizations of models:
  30 - Selected model 0: INCOMPLETE
  31   - Concrete RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
  32   - Abstract RAC: INCOMPLETE (terminated because Precondition of `f` cannot be evaluated)
  33 - Checked model 1: BAD_CE
  34   - Concrete RAC: NORMAL
  35   - Abstract RAC: NORMAL
  36 - Checked model 2: BAD_CE
  37   - Concrete RAC: NORMAL
  38   - Abstract RAC: NORMAL
  39 File "bench/check-ce/jlamp_array_mono.mlw", line 47, characters 14-27:
  40 Sub-goal Postcondition of goal f'vc.
  41 Prover result is: Unknown (unknown) (10 steps).
  42 The following counterexample model could not be verified
  43   (both RAC terminated because Precondition of `f` cannot be evaluated):
  44 File jlamp_array_mono.mlw:
  45   Line 11:
  46     two :  = "undefined"
  47   Line 14:
  48     three :  = "undefined"
  49   Line 44:
  50     a :  = "undefined"
  51     a :  = "undefined"
  52
  53 File "bench/check-ce/jlamp_array_mono.mlw", line 54, 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 - Selected model 0: INCOMPLETE
  59   - Concrete RAC: INCOMPLETE (terminated because Precondition of `g` cannot be evaluated)
  60   - Abstract RAC: INCOMPLETE (terminated because Precondition of `g` cannot be evaluated)
  61 - Checked model 1: BAD_CE
  62   - Concrete RAC: NORMAL
  63   - Abstract RAC: NORMAL
  64 - Checked model 2: BAD_CE
  65   - Concrete RAC: NORMAL
  66   - Abstract RAC: NORMAL
  67 File "bench/check-ce/jlamp_array_mono.mlw", line 53, 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 terminated because Precondition of `g` cannot be evaluated):
  72 File jlamp_array_mono.mlw:
  73   Line 11:
  74     two :  = "undefined"
  75   Line 14:
  76     three :  = "undefined"
  77   Line 50:
  78     a :  = "undefined"
  79     a :  = "undefined"
  80
  81 File "bench/check-ce/jlamp_array_mono.mlw", line 60, characters 4-16:
  82 Sub-goal Index in array bounds of goal h'vc.
  83 Prover result is: Valid (4 steps).
  84
  85 <check_ce:categorization>Categorizations of models:
  86 - Selected model 0: INCOMPLETE
  87   - Concrete RAC: INCOMPLETE (terminated because Precondition of `h` cannot be evaluated)
  88   - Abstract RAC: INCOMPLETE (terminated because Precondition of `h` cannot be evaluated)
  89 - Checked model 1: BAD_CE
  90   - Concrete RAC: NORMAL
  91   - Abstract RAC: NORMAL
  92 - Checked model 2: BAD_CE
  93   - Concrete RAC: NORMAL
  94   - Abstract RAC: NORMAL
  95 File "bench/check-ce/jlamp_array_mono.mlw", line 59, characters 14-27:
  96 Sub-goal Postcondition of goal h'vc.
  97 Prover result is: Unknown (unknown) (16 steps).
  98 The following counterexample model could not be verified
  99   (both RAC terminated because Precondition of `h` cannot be evaluated):
 100 File jlamp_array_mono.mlw:
 101   Line 11:
 102     two :  = "undefined"
 103   Line 14:
 104     three :  = "undefined"
 105   Line 56:
 106     a :  = "undefined"
 107     a :  = "undefined"
 108