bench/check-ce/oracles/log-call-nc_Z3,4.8.10_WP.oracle

   1 File "bench/check-ce/log-call-nc.mlw", line 14, characters 12-21:
   2 Sub-goal Postcondition of goal f'vc.
   3 Prover result is: Valid (1051 steps).
   4
   5 File "bench/check-ce/log-call-nc.mlw", line 19, characters 2-5:
   6 Sub-goal Precondition of goal f1'vc.
   7 Prover result is: Valid (33 steps).
   8
   9 <check_ce:categorization>Categorizations of models:
  10 - Selected model 0: NC
  11   - Concrete RAC: FAILURE (assertion at "bench/check-ce/log-call-nc.mlw", line 20, characters 11-16)
  12   - Abstract RAC: FAILURE (assertion at "bench/check-ce/log-call-nc.mlw", line 20, characters 11-16)
  13 - Checked model 1: NC
  14   - Concrete RAC: FAILURE (assertion at "bench/check-ce/log-call-nc.mlw", line 20, characters 11-16)
  15   - Abstract RAC: STUCK (failure in postcondition of `f` at "bench/check-ce/log-call-nc.mlw", line 14, characters 12-21)
  16 File "bench/check-ce/log-call-nc.mlw", line 20, characters 11-16:
  17 Sub-goal Assertion of goal f1'vc.
  18 Prover result is: Step limit exceeded (3000032 steps).
  19 The program does not comply to the verification goal, for example during the
  20   following execution:
  21 File int.mlw:
  22   Line 13:
  23     Constant zero initialization
  24     zero = 0
  25   Line 14:
  26     Constant one initialization
  27     one = 1
  28 File log-call-nc.mlw:
  29   Line 9:
  30     Constant x initialization
  31     (giant-step) execution of unimplemented function with args:
  32     result = 0
  33     Normal execution of function `ref` with args:
  34       contents = 0
  35     Normal execution of function `ref'mk` with args:
  36       contents = 0
  37     x = {contents= 0}
  38 Unknown location:
  39     _ = ()
  40 File log-call-nc.mlw:
  41   Line 17:
  42     _ = ()
  43     Execution of main function `f1` with env:
  44       x = {contents= 0}
  45       _ = ()
  46       zero = 0
  47       one = 1
  48   Line 19:
  49     Normal execution of function `f` with args:
  50       y = 1
  51   Line 15:
  52     Normal execution of function `contents` with args:
  53       arg = {contents= 0}
  54     Normal execution of function `(+)` with args:
  55       _ = 0
  56       _ = 1
  57   Line 20:
  58     Property failure at assertion with:
  59       x = {contents= 1}
  60