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

   1 <check_ce:categorization>Categorizations of models:
   2 - Selected model 0: NC
   3   - Concrete RAC: FAILURE (precondition at "bench/check-ce/bv32_toBig.mlw", line 8, characters 27-40)
   4   - Abstract RAC: FAILURE (precondition at "bench/check-ce/bv32_toBig.mlw", line 8, characters 27-40)
   5 - Checked model 1: NC
   6   - Concrete RAC: FAILURE (precondition at "bench/check-ce/bv32_toBig.mlw", line 8, characters 27-40)
   7   - Abstract RAC: FAILURE (precondition at "bench/check-ce/bv32_toBig.mlw", line 8, characters 27-40)
   8 File "bench/check-ce/bv32_toBig.mlw", line 8, characters 27-40:
   9 Sub-goal Precondition of goal ok'vc.
  10 Prover result is: Unknown (sat) (724 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 bv32_toBig.mlw:
  21   Line 8:
  22     i = (8:t)
  23     i = (8:t)
  24     Execution of main function `ok` with env:
  25       i = (8:t)
  26       zero = 0
  27       one = 1
  28     (giant-step) execution of unimplemented function `toBig`
  29       _ = (8:t)
  30     result of `toBig` = (8:t1)
  31     (giant-step) execution of unimplemented function `u`
  32       i = (8:t1)
  33     Property failure at precondition of `u` with:
  34       i = (8:t1)
  35
  36 <check_ce:categorization>Categorizations of models:
  37 - Selected model 0: NC
  38   - Concrete RAC: FAILURE (precondition at "bench/check-ce/bv32_toBig.mlw", line 10, characters 27-41)
  39   - Abstract RAC: FAILURE (precondition at "bench/check-ce/bv32_toBig.mlw", line 10, characters 27-41)
  40 - Checked model 1: NC
  41   - Concrete RAC: FAILURE (precondition at "bench/check-ce/bv32_toBig.mlw", line 10, characters 27-41)
  42   - Abstract RAC: FAILURE (precondition at "bench/check-ce/bv32_toBig.mlw", line 10, characters 27-41)
  43 File "bench/check-ce/bv32_toBig.mlw", line 10, characters 27-41:
  44 Sub-goal Precondition of goal ko'vc.
  45 Prover result is: Unknown (sat) (716 steps).
  46 The program does not comply to the verification goal, for example during the
  47   following execution:
  48 File int.mlw:
  49   Line 13:
  50     Constant zero initialization
  51     zero = 0
  52   Line 14:
  53     Constant one initialization
  54     one = 1
  55 File bv32_toBig.mlw:
  56   Line 10:
  57     i = (8:t)
  58     i = (8:t)
  59     Execution of main function `ko` with env:
  60       i = (8:t)
  61       zero = 0
  62       one = 1
  63     (giant-step) execution of unimplemented function `stoBig`
  64       _ = (8:t)
  65     result of `stoBig` = (8:t1)
  66     (giant-step) execution of unimplemented function `u`
  67       i = (8:t1)
  68     Property failure at precondition of `u` with:
  69       i = (8:t1)
  70
  71 <check_ce:categorization>Categorizations of models:
  72 - Selected model 0: NC
  73   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/bv32_toBig.mlw", line 13, characters 14-40)
  74   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/bv32_toBig.mlw", line 13, characters 14-40)
  75 - Checked model 1: NC
  76   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/bv32_toBig.mlw", line 13, characters 14-40)
  77   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/bv32_toBig.mlw", line 13, characters 14-40)
  78 File "bench/check-ce/bv32_toBig.mlw", line 13, characters 14-40:
  79 Sub-goal Postcondition of goal ko2'vc.
  80 Prover result is: Unknown (sat) (728 steps).
  81 The program does not comply to the verification goal, for example during the
  82   following execution:
  83 File int.mlw:
  84   Line 13:
  85     Constant zero initialization
  86     zero = 0
  87   Line 14:
  88     Constant one initialization
  89     one = 1
  90 File bv32_toBig.mlw:
  91   Line 12:
  92     i = (2147483648:t)
  93     i = (2147483648:t)
  94     Execution of main function `ko2` with env:
  95       i = (2147483648:t)
  96       zero = 0
  97       one = 1
  98   Line 13:
  99     (giant-step) execution of unimplemented function `stoBig`
 100       _ = (2147483648:t)
 101     result of `stoBig` = (18446744071562067968:t1)
 102     Property failure at postcondition of `ko2` with:
 103       result = (18446744071562067968:t1)
 104