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

   1 File "bench/check-ce/log-post.mlw", line 20, characters 14-20:
   2 Sub-goal Assertion of goal f1'vc.
   3 Prover result is: Valid (991 steps).
   4
   5 <check_ce:categorization>Categorizations of models:
   6 - Selected model 0: NC
   7   - Concrete RAC: FAILURE (postcondition at "bench/check-ce/log-post.mlw", line 18, characters 14-33)
   8   - Abstract RAC: FAILURE (postcondition at "bench/check-ce/log-post.mlw", line 18, characters 14-33)
   9 - Checked model 1: INCOMPLETE
  10   - Concrete RAC: INCOMPLETE (fatal rac error: missing value for global `a`)
  11   - Abstract RAC: INCOMPLETE (fatal rac error: missing value for global `a`)
  12 File "bench/check-ce/log-post.mlw", line 18, characters 14-33:
  13 Sub-goal Postcondition of goal f1'vc.
  14 Prover result is: Step limit exceeded (3000065 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 log-post.mlw:
  25   Line 12:
  26     a = 43
  27   Line 14:
  28     b = {contents= 0}
  29   Line 16:
  30     x = 0
  31     y = {contents= 0}
  32     x = 0
  33     y = {contents= 0}
  34     Execution of main function `f1` with env:
  35       a = 43
  36       b = {contents= 0}
  37       x = 0
  38       y = {contents= 0}
  39       zero = 0
  40       one = 1
  41   Line 19:
  42     Normal execution of function `contents` with args:
  43       arg = {contents= 0}
  44     Normal execution of function `(+)` with args:
  45       _ = 0
  46       _ = 0
  47   Line 21:
  48     Normal execution of function `contents` with args:
  49       arg = {contents= 0}
  50     Normal execution of function `contents` with args:
  51       arg = {contents= 0}
  52     Normal execution of function `(+)` with args:
  53       _ = 0
  54       _ = 0
  55   Line 18:
  56     Property failure at postcondition of `f1` with:
  57       b = {contents= 0}
  58       x = 0
  59       y = {contents= 0}
  60