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

   1 File "bench/check-ce/func_call5.mlw", line 8, characters 12-24:
   2 Sub-goal Postcondition of goal g1'vc.
   3 Prover result is: Valid (221 steps).
   4
   5 File "bench/check-ce/func_call5.mlw", line 14, characters 10-14:
   6 Sub-goal Precondition of goal f1'vc.
   7 Prover result is: Valid (47 steps).
   8
   9 <check_ce:categorization>Categorizations of models:
  10 - Checked model 0: INCOMPLETE
  11   - Concrete RAC: NORMAL
  12   - Abstract RAC: INCOMPLETE (fatal rac error: missing value for return value of call to g1 at "bench/check-ce/func_call5.mlw", line 14, characters 10-14)
  13 - Selected model 1: INCOMPLETE
  14   - Concrete RAC: NORMAL
  15   - Abstract RAC: INCOMPLETE (fatal rac error: missing value for return value of call to g1 at "bench/check-ce/func_call5.mlw", line 14, characters 10-14)
  16 File "bench/check-ce/func_call5.mlw", line 15, characters 11-17:
  17 Sub-goal Assertion of goal f1'vc.
  18 Prover result is: Unknown (unknown + incomplete) (307 steps).
  19 The following counterexample model could not be verified
  20   (abstract RAC fatal rac error: missing value for return value of call to g1 at "bench/check-ce/func_call5.mlw", line 14, characters 10-14):
  21 File func_call5.mlw:
  22   Line 11:
  23     x :  = 1
  24     x : int = 1
  25
  26 <check_ce:categorization>Categorizations of models:
  27 - Selected model 0: NC
  28   - Concrete RAC: FAILURE (assertion at "bench/check-ce/func_call5.mlw", line 21, characters 11-17)
  29   - Abstract RAC: FAILURE (assertion at "bench/check-ce/func_call5.mlw", line 21, characters 11-17)
  30 - Checked model 1: NC
  31   - Concrete RAC: FAILURE (assertion at "bench/check-ce/func_call5.mlw", line 21, characters 11-17)
  32   - Abstract RAC: FAILURE (assertion at "bench/check-ce/func_call5.mlw", line 21, characters 11-17)
  33 File "bench/check-ce/func_call5.mlw", line 21, characters 11-17:
  34 Sub-goal Assertion of goal f2'vc.
  35 Prover result is: Unknown (unknown + incomplete) (272 steps).
  36 The program does not comply to the verification goal, for example during the
  37   following execution:
  38 File int.mlw:
  39   Line 13:
  40     Constant zero initialization
  41     zero = 0
  42   Line 14:
  43     Constant one initialization
  44     one = 1
  45 File func_call5.mlw:
  46   Line 19:
  47     x = 0
  48     x = 0
  49     Execution of main function `f2` with env:
  50       x = 0
  51       zero = 0
  52       one = 1
  53   Line 20:
  54     Normal execution of function `g2` with args:
  55       y = 0
  56   Line 17:
  57     Normal execution of function `(+)` with args:
  58       _ = 0
  59       _ = 1
  60     Normal execution of function `ref` with args:
  61       contents = 1
  62     Normal execution of function `ref'mk` with args:
  63       contents = 1
  64   Line 21:
  65     Property failure at assertion with:
  66       x = 0
  67       z = {contents= 1}
  68