bench/check-ce/oracles/int32_mono_CVC5,1.0.5_SP.oracle

   1 File "bench/check-ce/int32_mono.mlw", line 11, characters 11-20:
   2 Sub-goal Integer overflow of goal dummy_update'vc.
   3 Prover result is: Valid (416 steps).
   4
   5 <check_ce:categorization>Categorizations of models:
   6 - Selected model 0: NC
   7   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/int32_mono.mlw", line 9, characters 14-32)
   8   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/int32_mono.mlw", line 9, characters 14-32)
   9 - Checked model 1: NC
  10   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/int32_mono.mlw", line 9, characters 14-32)
  11   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/int32_mono.mlw", line 9, characters 14-32)
  12 File "bench/check-ce/int32_mono.mlw", line 9, characters 14-32:
  13 Sub-goal Postcondition of goal dummy_update'vc.
  14 Prover result is: Unknown (unknown + incomplete) (736 steps).
  15 The program does not comply to the verification goal, for example during the
  16   following execution:
  17 File int.mlw:
  18   Line 13:
  19     Constant zero initialization
  20     zero = 0
  21   Line 14:
  22     Constant one initialization
  23     one = 1
  24 File int.mlw:
  25   Line 281:
  26     Constant min_int32 initialization
  27     min_int32 = (-2147483648)
  28   Line 282:
  29     Constant max_int32 initialization
  30     max_int32 = 2147483647
  31 File int32_mono.mlw:
  32   Line 7:
  33     r = {c= epsilon x:int32. int32'int x = 22}
  34     r = {c= epsilon x:int32. int32'int x = 22}
  35     Execution of main function `dummy_update` with env:
  36       r = {c= epsilon x:int32. int32'int x = 22}
  37       zero = 0
  38       one = 1
  39       min_int32 = (-2147483648)
  40       max_int32 = 2147483647
  41   Line 11:
  42     Normal execution of function `c` with args:
  43       arg = {c= 42}
  44     Normal execution of function `c` with args:
  45       arg = {c= 42}
  46     (giant-step) execution of unimplemented function `(+)`
  47       a = 42
  48       b = 42
  49     result of `(+)` = epsilon x:int32. int32'int x = 84
  50   Line 9:
  51     Property failure at postcondition of `dummy_update` with:
  52       r = {c= epsilon x:int32. int32'int x = 84}
  53