bench/check-ce/oracles/log-cond_CVC5,1.0.5_WP.oracle

   1 <check_ce:categorization>Categorizations of models:
   2 - Selected model 0: NC
   3   - Concrete RAC: FAILURE (assertion at "bench/check-ce/log-cond.mlw", line 22, characters 19-38)
   4   - Abstract RAC: FAILURE (assertion at "bench/check-ce/log-cond.mlw", line 22, characters 19-38)
   5 - Checked model 1: NC
   6   - Concrete RAC: FAILURE (assertion at "bench/check-ce/log-cond.mlw", line 22, characters 19-38)
   7   - Abstract RAC: FAILURE (assertion at "bench/check-ce/log-cond.mlw", line 22, characters 19-38)
   8 File "bench/check-ce/log-cond.mlw", line 22, characters 19-38:
   9 Sub-goal Assertion of goal f1'vc.
  10 Prover result is: Unknown (unknown + incomplete) (585 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 log-cond.mlw:
  21   Line 12:
  22     a = 43
  23   Line 14:
  24     b = {contents= 0}
  25   Line 16:
  26     x = 0
  27     y = {contents= 0}
  28     x = 0
  29     y = {contents= 0}
  30     Execution of main function `f1` with env:
  31       a = 43
  32       b = {contents= 0}
  33       x = 0
  34       y = {contents= 0}
  35       zero = 0
  36       one = 1
  37   Line 18:
  38     Normal execution of function `contents` with args:
  39       arg = {contents= 0}
  40     Normal execution of function `(+)` with args:
  41       _ = 0
  42       _ = 0
  43   Line 19:
  44     Normal execution of function `contents` with args:
  45       arg = {contents= 0}
  46     Normal execution of function `(<=)` with args:
  47       x = 0
  48       y = 42
  49   Line 21:
  50     Normal execution of function `contents` with args:
  51       arg = {contents= 0}
  52     Normal execution of function `contents` with args:
  53       arg = {contents= 0}
  54     Normal execution of function `(+)` with args:
  55       _ = 0
  56       _ = 0
  57   Line 22:
  58     Property failure at assertion with:
  59       b = {contents= 0}
  60       x = 0
  61       y = {contents= 0}
  62
  63 File "bench/check-ce/log-cond.mlw", line 27, characters 17-23:
  64 Sub-goal Assertion of goal f1'vc.
  65 Prover result is: Valid (537 steps).
  66