bench/check-ce/oracles/threshold_CVC5,1.0.5_WP.oracle

   1 <check_ce:categorization>Categorizations of models:
   2 - Checked model 0: BAD_CE
   3   - Concrete RAC: STUCK (for range projection int32 at "bench/check-ce/threshold.mlw", line 8, characters 13-16)
   4   - Abstract RAC: STUCK (for range projection int32 at "bench/check-ce/threshold.mlw", line 8, characters 13-16)
   5 - Selected model 1: NC
   6   - Concrete RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 11, characters 11-20)
   7   - Abstract RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 11, characters 11-20)
   8 File "bench/check-ce/threshold.mlw", line 11, characters 11-20:
   9 Sub-goal Integer overflow of goal f'vc.
  10 Prover result is: Unknown (unknown + incomplete) (574 steps).
  11 The program does not comply to the verification goal, for example during the
  12   following execution:
  13 File int.mlw:
  14   Line 13:
  15     Constant zero initialization
  16     zero = 0
  17   Line 14:
  18     Constant one initialization
  19     one = 1
  20 File int.mlw:
  21   Line 281:
  22     Constant min_int32 initialization
  23     min_int32 = (-2147483648)
  24   Line 282:
  25     Constant max_int32 initialization
  26     max_int32 = 2147483647
  27 File threshold.mlw:
  28   Line 8:
  29     n = epsilon x:int32. int32'int x = (- 1)
  30     min = epsilon x:int32. int32'int x = (- 1)
  31     max = epsilon x:int32. int32'int x = (- 2147483648)
  32     n = epsilon x:int32. int32'int x = (- 1)
  33     min = epsilon x:int32. int32'int x = (- 1)
  34     max = epsilon x:int32. int32'int x = (- 2147483648)
  35     Execution of main function `f` with env:
  36       n = epsilon x:int32. int32'int x = (- 1)
  37       min = epsilon x:int32. int32'int x = (- 1)
  38       max = epsilon x:int32. int32'int x = (- 2147483648)
  39       zero = 0
  40       one = 1
  41       min_int32 = (-2147483648)
  42       max_int32 = 2147483647
  43   Line 11:
  44     (giant-step) execution of unimplemented function `(+)`
  45       a = epsilon x:int32. int32'int x = (- 1)
  46       b = epsilon x:int32. int32'int x = (- 2147483648)
  47     Property failure at precondition of `(+)` with:
  48       a = epsilon x:int32. int32'int x = (- 1)
  49       b = epsilon x:int32. int32'int x = (- 2147483648)
  50
  51 <check_ce:categorization>Categorizations of models:
  52 - Selected model 0: NC
  53   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 9, characters 13-33)
  54   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 9, characters 13-33)
  55 - Checked model 1: NC
  56   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 9, characters 13-33)
  57   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 9, characters 13-33)
  58 File "bench/check-ce/threshold.mlw", line 9, characters 13-33:
  59 Sub-goal Postcondition of goal f'vc.
  60 Prover result is: Unknown (unknown + incomplete) (1589 steps).
  61 The program does not comply to the verification goal, for example during the
  62   following execution:
  63 File int.mlw:
  64   Line 13:
  65     Constant zero initialization
  66     zero = 0
  67   Line 14:
  68     Constant one initialization
  69     one = 1
  70 File int.mlw:
  71   Line 281:
  72     Constant min_int32 initialization
  73     min_int32 = (-2147483648)
  74   Line 282:
  75     Constant max_int32 initialization
  76     max_int32 = 2147483647
  77 File threshold.mlw:
  78   Line 8:
  79     n = epsilon x:int32. int32'int x = 0
  80     min = epsilon x:int32. int32'int x = 0
  81     max = epsilon x:int32. int32'int x = (- 1)
  82     n = epsilon x:int32. int32'int x = 0
  83     min = epsilon x:int32. int32'int x = 0
  84     max = epsilon x:int32. int32'int x = (- 1)
  85     Execution of main function `f` with env:
  86       n = epsilon x:int32. int32'int x = 0
  87       min = epsilon x:int32. int32'int x = 0
  88       max = epsilon x:int32. int32'int x = (- 1)
  89       zero = 0
  90       one = 1
  91       min_int32 = (-2147483648)
  92       max_int32 = 2147483647
  93   Line 11:
  94     (giant-step) execution of unimplemented function `(+)`
  95       a = epsilon x:int32. int32'int x = 0
  96       b = epsilon x:int32. int32'int x = (- 1)
  97     result of `(+)` = epsilon x:int32. int32'int x = (- 1)
  98   Line 12:
  99     (giant-step) execution of unimplemented function `(<)`
 100       a = epsilon x:int32. int32'int x = 0
 101       b = epsilon x:int32. int32'int x = 0
 102     result of `(<)` = false
 103     (giant-step) execution of unimplemented function `(>)`
 104       a = epsilon x:int32. int32'int x = 0
 105       b = epsilon x:int32. int32'int x = (- 1)
 106     result of `(>)` = true
 107   Line 9:
 108     Property failure at postcondition of `f` with:
 109       min = epsilon x:int32. int32'int x = 0
 110       max = epsilon x:int32. int32'int x = (- 1)
 111       result = epsilon x:int32. int32'int x = (- 1)
 112
 113 <check_ce:categorization>Categorizations of models:
 114 - Selected model 0: NC
 115   - Concrete RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 116   - Abstract RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 117 - Checked model 1: NC
 118   - Concrete RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 119   - Abstract RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 120 File "bench/check-ce/threshold.mlw", line 30, characters 11-24:
 121 Sub-goal Arithmetic overflow of goal f'vc.
 122 Prover result is: Unknown (unknown + incomplete) (146995 steps).
 123 The program does not comply to the verification goal, for example during the
 124   following execution:
 125 File int.mlw:
 126   Line 13:
 127     Constant zero initialization
 128     zero = 0
 129   Line 14:
 130     Constant one initialization
 131     one = 1
 132 File threshold.mlw:
 133   Line 26:
 134     n = (0:t)
 135     min = (4294967295:t)
 136     max = (4294967295:t)
 137     n = (0:t)
 138     min = (4294967295:t)
 139     max = (4294967295:t)
 140     Execution of main function `f` with env:
 141       n = (0:t)
 142       min = (4294967295:t)
 143       max = (4294967295:t)
 144       zero = 0
 145       one = 1
 146   Line 30:
 147     (giant-step) execution of unimplemented function `u_add`
 148       a = (4294967295:t)
 149       b = (4294967295:t)
 150     Property failure at precondition of `u_add` with:
 151       a = (4294967295:t)
 152       b = (4294967295:t)
 153
 154 <check_ce:categorization>Categorizations of models:
 155 - Selected model 0: NC
 156   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 27, characters 13-45)
 157   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 27, characters 13-45)
 158 - Checked model 1: NC
 159   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 27, characters 13-45)
 160   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 27, characters 13-45)
 161 File "bench/check-ce/threshold.mlw", line 27, characters 13-45:
 162 Sub-goal Postcondition of goal f'vc.
 163 Prover result is: Step limit exceeded (150192 steps).
 164 The program does not comply to the verification goal, for example during the
 165   following execution:
 166 File int.mlw:
 167   Line 13:
 168     Constant zero initialization
 169     zero = 0
 170   Line 14:
 171     Constant one initialization
 172     one = 1
 173 File threshold.mlw:
 174   Line 26:
 175     n = (4294967293:t)
 176     min = (4294967294:t)
 177     max = (1:t)
 178     n = (4294967293:t)
 179     min = (4294967294:t)
 180     max = (1:t)
 181     Execution of main function `f` with env:
 182       n = (4294967293:t)
 183       min = (4294967294:t)
 184       max = (1:t)
 185       zero = 0
 186       one = 1
 187   Line 30:
 188     (giant-step) execution of unimplemented function `u_add`
 189       a = (4294967294:t)
 190       b = (1:t)
 191     result of `u_add` = (4294967295:t)
 192   Line 31:
 193     (giant-step) execution of unimplemented function `u_lt`
 194       a = (4294967293:t)
 195       b = (4294967294:t)
 196     result of `u_lt` = true
 197   Line 27:
 198     Property failure at postcondition of `f1` with:
 199       min = (4294967294:t)
 200       max = (1:t)
 201       result = (4294967294:t)
 202