bench/check-ce/oracles/val_function_CVC4,1.8_SP.oracle

   1 <check_ce:categorization>Categorizations of models:
   2 - Checked model 0: INCOMPLETE
   3   - Concrete RAC: INCOMPLETE (terminated because Postcondition of `f` cannot be evaluated)
   4   - Abstract RAC: INCOMPLETE (terminated because Postcondition of `f` cannot be evaluated)
   5 - Selected model 1: INCOMPLETE
   6   - Concrete RAC: INCOMPLETE (terminated because Postcondition of `f` cannot be evaluated)
   7   - Abstract RAC: INCOMPLETE (terminated because Postcondition of `f` cannot be evaluated)
   8 File "bench/check-ce/val_function.mlw", line 7, characters 12-24:
   9 Sub-goal Postcondition of goal main_f'vc.
  10 Prover result is: Unknown (sat) (145 steps).
  11 The following counterexample model could not be verified
  12   (both RAC terminated because Postcondition of `f` cannot be evaluated):
  13 File val_function.mlw:
  14   Line 6:
  15     y :  = 0
  16     y : int = 0
  17   Line 9:
  18     result of call at line 9, characters 2-5 : int = 42
  19
  20 <check_ce:categorization>Categorizations of models:
  21 - Checked model 0: BAD_CE
  22   - Concrete RAC: STUCK (failure in postcondition of `g` at unknown location)
  23   - Abstract RAC: STUCK (failure in postcondition of `g` at unknown location)
  24 - Selected model 1: NC
  25   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/val_function.mlw", line 16, characters 12-24)
  26   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/val_function.mlw", line 16, characters 12-24)
  27 File "bench/check-ce/val_function.mlw", line 16, characters 12-24:
  28 Sub-goal Postcondition of goal main_g'vc.
  29 Prover result is: Unknown (unknown + incomplete) (342 steps).
  30 The program does not comply to the verification goal, for example during the
  31   following execution:
  32 File int.mlw:
  33   Line 13:
  34     Constant zero initialization
  35     zero = 0
  36   Line 14:
  37     Constant one initialization
  38     one = 1
  39 File val_function.mlw:
  40   Line 15:
  41     y = 42
  42     y = 42
  43     Execution of main function `main_g` with env:
  44       y = 42
  45       zero = 0
  46       one = 1
  47   Line 18:
  48     (giant-step) execution of unimplemented function `g`
  49       x = 42
  50     result of `g` = 43
  51   Line 19:
  52     Normal execution of function `(+)` with args:
  53       _ = 43
  54       _ = 1
  55   Line 16:
  56     Property failure at postcondition of `main_g` with:
  57       result = 44
  58