bench/check-ce/oracles/threshold_CVC5,1.0.5_SP.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 7-8)
   4   - Abstract RAC: STUCK (for range projection int32 at "bench/check-ce/threshold.mlw", line 8, characters 7-8)
   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) (493 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 = (- 2147483648)
  30     min = epsilon x:int32. int32'int x = (- 2147483648)
  31     max = epsilon x:int32. int32'int x = (- 1)
  32     n = epsilon x:int32. int32'int x = (- 2147483648)
  33     min = epsilon x:int32. int32'int x = (- 2147483648)
  34     max = epsilon x:int32. int32'int x = (- 1)
  35     Execution of main function `f` with env:
  36       n = epsilon x:int32. int32'int x = (- 2147483648)
  37       min = epsilon x:int32. int32'int x = (- 2147483648)
  38       max = epsilon x:int32. int32'int x = (- 1)
  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 = (- 2147483648)
  46       b = epsilon x:int32. int32'int x = (- 1)
  47     Property failure at precondition of `(+)` with:
  48       a = epsilon x:int32. int32'int x = (- 2147483648)
  49       b = epsilon x:int32. int32'int x = (- 1)
  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) (1289 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 = 1
  81     max = epsilon x:int32. int32'int x = 0
  82     n = epsilon x:int32. int32'int x = 0
  83     min = epsilon x:int32. int32'int x = 1
  84     max = epsilon x:int32. int32'int x = 0
  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 = 1
  88       max = epsilon x:int32. int32'int x = 0
  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 = 1
  96       b = epsilon x:int32. int32'int x = 0
  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 = 1
 102     result of `(<)` = true
 103   Line 9:
 104     Property failure at postcondition of `f` with:
 105       min = epsilon x:int32. int32'int x = 1
 106       max = epsilon x:int32. int32'int x = 0
 107       result = epsilon x:int32. int32'int x = 1
 108
 109 <check_ce:categorization>Categorizations of models:
 110 - Selected model 0: NC
 111   - Concrete RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 112   - Abstract RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 113 - Checked model 1: NC
 114   - Concrete RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 115   - Abstract RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 116 File "bench/check-ce/threshold.mlw", line 30, characters 11-24:
 117 Sub-goal Arithmetic overflow of goal f'vc.
 118 Prover result is: Unknown (unknown + incomplete) (8279 steps).
 119 The program does not comply to the verification goal, for example during the
 120   following execution:
 121 File int.mlw:
 122   Line 13:
 123     Constant zero initialization
 124     zero = 0
 125   Line 14:
 126     Constant one initialization
 127     one = 1
 128 File threshold.mlw:
 129   Line 26:
 130     n = (0:t)
 131     min = (4294967295:t)
 132     max = (4294967295:t)
 133     n = (0:t)
 134     min = (4294967295:t)
 135     max = (4294967295:t)
 136     Execution of main function `f` with env:
 137       n = (0:t)
 138       min = (4294967295:t)
 139       max = (4294967295:t)
 140       zero = 0
 141       one = 1
 142   Line 30:
 143     (giant-step) execution of unimplemented function `u_add`
 144       a = (4294967295:t)
 145       b = (4294967295:t)
 146     Property failure at precondition of `u_add` with:
 147       a = (4294967295:t)
 148       b = (4294967295:t)
 149
 150 <check_ce:categorization>Categorizations of models:
 151 - Selected model 0: NC
 152   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 27, characters 13-45)
 153   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 27, characters 13-45)
 154 - Checked model 1: NC
 155   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 27, characters 13-45)
 156   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/threshold.mlw", line 27, characters 13-45)
 157 File "bench/check-ce/threshold.mlw", line 27, characters 13-45:
 158 Sub-goal Postcondition of goal f'vc.
 159 Prover result is: Step limit exceeded (150162 steps).
 160 The program does not comply to the verification goal, for example during the
 161   following execution:
 162 File int.mlw:
 163   Line 13:
 164     Constant zero initialization
 165     zero = 0
 166   Line 14:
 167     Constant one initialization
 168     one = 1
 169 File threshold.mlw:
 170   Line 26:
 171     n = (4294967293:t)
 172     min = (4294967294:t)
 173     max = (1:t)
 174     n = (4294967293:t)
 175     min = (4294967294:t)
 176     max = (1:t)
 177     Execution of main function `f` with env:
 178       n = (4294967293:t)
 179       min = (4294967294:t)
 180       max = (1:t)
 181       zero = 0
 182       one = 1
 183   Line 30:
 184     (giant-step) execution of unimplemented function `u_add`
 185       a = (4294967294:t)
 186       b = (1:t)
 187     result of `u_add` = (4294967295:t)
 188   Line 31:
 189     (giant-step) execution of unimplemented function `u_lt`
 190       a = (4294967293:t)
 191       b = (4294967294:t)
 192     result of `u_lt` = true
 193   Line 27:
 194     Property failure at postcondition of `f1` with:
 195       min = (4294967294:t)
 196       max = (1:t)
 197       result = (4294967294:t)
 198