bench/check-ce/oracles/array_mono_Z3,4.8.10_WP.oracle

   1 File bench/check-ce/array_mono.mlw:
   2 Goal array'vc.
   3 Prover result is: Valid (259 steps).
   4
   5 <check_ce:categorization>Categorizations of models:
   6 - Selected model 0: NC
   7   - Concrete RAC: FAILURE (precondition at "bench/check-ce/array_mono.mlw", line 36, characters 4-8)
   8   - Abstract RAC: FAILURE (precondition at "bench/check-ce/array_mono.mlw", line 36, characters 4-8)
   9 - Checked model 1: INCOMPLETE
  10   - Concrete RAC: INCOMPLETE (terminated because Precondition of `([])` cannot be evaluated)
  11   - Abstract RAC: INCOMPLETE (terminated because Precondition of `([])` cannot be evaluated)
  12 File "bench/check-ce/array_mono.mlw", line 36, characters 4-8:
  13 Sub-goal Index in array bounds of goal f1'vc.
  14 Prover result is: Step limit exceeded (100017 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 array_mono.mlw:
  25   Line 35:
  26     a = {elts= fun (x:int) -> 0; length= 0}
  27     a = {elts= fun (x:int) -> 0; length= 0}
  28     Execution of main function `f1` with env:
  29       a = {elts= fun (x:int) -> 0; length= 0}
  30       zero = 0
  31       one = 1
  32   Line 36:
  33     (giant-step) execution of unimplemented function `([])`
  34       a = {elts= fun (x:int) -> 0; length= 0}
  35       i = 0
  36     Property failure at precondition of `([])` with:
  37       a = {elts= fun (x:int) -> 0; length= 0}
  38       i = 0
  39
  40 File "bench/check-ce/array_mono.mlw", line 41, characters 4-14:
  41 Sub-goal Index in array bounds of goal f2'vc.
  42 Prover result is: Valid (442 steps).
  43
  44 <check_ce:categorization>Categorizations of models:
  45 - Checked model 0: INCOMPLETE
  46   - Concrete RAC: INCOMPLETE (terminated because Postcondition of `([]<-)` cannot be evaluated)
  47   - Abstract RAC: INCOMPLETE (terminated because Postcondition of `([]<-)` cannot be evaluated)
  48 - Selected model 1: INCOMPLETE
  49   - Concrete RAC: INCOMPLETE (terminated because Precondition of `f2` cannot be evaluated)
  50   - Abstract RAC: INCOMPLETE (terminated because Precondition of `f2` cannot be evaluated)
  51 File "bench/check-ce/array_mono.mlw", line 40, characters 14-26:
  52 Sub-goal Postcondition of goal f2'vc.
  53 Prover result is: Step limit exceeded (100052 steps).
  54 The following counterexample model could not be verified
  55   (both RAC terminated because Precondition of `f2` cannot be evaluated):
  56 File array_mono.mlw:
  57   Line 38:
  58     a :  = "undefined"
  59     a :  = "undefined"
  60