bench/check-ce/oracles/loop_inv_real_mono_CVC4,1.8_WP.oracle

   1 File "bench/check-ce/loop_inv_real_mono.mlw", line 19, characters 16-31:
   2 Sub-goal Loop invariant init of goal f'vc.
   3 Prover result is: Valid (145 steps).
   4
   5 <check_ce:categorization>Categorizations of models:
   6 - Checked model 0: INCOMPLETE
   7   - Concrete RAC: INCOMPLETE (terminated because Loop invariant init cannot be evaluated)
   8   - Abstract RAC: INCOMPLETE (terminated because Loop invariant init cannot be evaluated)
   9 - Selected model 1: INCOMPLETE
  10   - Concrete RAC: INCOMPLETE (terminated because Loop invariant init cannot be evaluated)
  11   - Abstract RAC: INCOMPLETE (terminated because Loop invariant init cannot be evaluated)
  12 File "bench/check-ce/loop_inv_real_mono.mlw", line 19, characters 16-31:
  13 Sub-goal Loop invariant preservation of goal f'vc.
  14 Prover result is: Unknown (sat) (566 steps).
  15 The following counterexample model could not be verified
  16   (both RAC terminated because Loop invariant init cannot be evaluated):
  17 File loop_inv_real_mono.mlw:
  18   Line 8:
  19     a :  = {c = [0.0000000000000000e+00, 0.0000000000000000e+00]}
  20   Line 10:
  21     b :  = {c = [0.0000000000000000e+00, 0.0000000000000000e+00]}
  22   Line 12:
  23     _ :  = Tuple0
  24
  25 File "bench/check-ce/loop_inv_real_mono.mlw", line 14, characters 12-24:
  26 Sub-goal Postcondition of goal f'vc.
  27 Prover result is: Valid (381 steps).
  28