bench/check-ce/oracles/log-simple_Z3,4.8.10_SP.oracle

   1 <check_ce:categorization>Categorizations of models:
   2 - Selected model 0: NC
   3   - Concrete RAC: FAILURE (assertion at "bench/check-ce/log-simple.mlw", line 18, characters 14-33)
   4   - Abstract RAC: FAILURE (assertion at "bench/check-ce/log-simple.mlw", line 18, characters 14-33)
   5 - Checked model 1: INCOMPLETE
   6   - Concrete RAC: INCOMPLETE (fatal rac error: missing value for global `a`)
   7   - Abstract RAC: INCOMPLETE (fatal rac error: missing value for global `a`)
   8 File "bench/check-ce/log-simple.mlw", line 18, characters 14-33:
   9 Sub-goal Assertion of goal f1'vc.
  10 Prover result is: Step limit exceeded (3000062 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-simple.mlw:
  21   Line 10:
  22     a = 43
  23   Line 12:
  24     b = {contents= 0}
  25   Line 14:
  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 16:
  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 17:
  44     Normal execution of function `contents` with args:
  45       arg = {contents= 0}
  46     Normal execution of function `contents` with args:
  47       arg = {contents= 0}
  48     Normal execution of function `(+)` with args:
  49       _ = 0
  50       _ = 0
  51   Line 18:
  52     Property failure at assertion with:
  53       b = {contents= 0}
  54       x = 0
  55       y = {contents= 0}
  56