bench/check-ce/oracles/703_reduce_term_CVC4,1.8_SP.oracle

   1 Warning: term reduction aborted (term size blows up from 289 to 491721, after 278 steps).
   2
   3 Warning: term reduction aborted (takes more than 1024 steps).
   4
   5 Warning: term reduction aborted (term size blows up from 289 to 491721, after 278 steps).
   6
   7 Warning: term reduction aborted (takes more than 1024 steps).
   8
   9 Warning: term reduction aborted (term size blows up from 289 to 491721, after 278 steps).
  10
  11 Warning: term reduction aborted (takes more than 1024 steps).
  12
  13 Warning: term reduction aborted (term size blows up from 289 to 491721, after 278 steps).
  14
  15 Warning: term reduction aborted (takes more than 1024 steps).
  16
  17 <check_ce:categorization>Categorizations of models:
  18 - Checked model 0: INCOMPLETE
  19   - Concrete RAC: INCOMPLETE (terminated because Precondition of `local` cannot be evaluated)
  20   - Abstract RAC: INCOMPLETE (terminated because Precondition of `local` cannot be evaluated)
  21 - Selected model 1: INCOMPLETE
  22   - Concrete RAC: INCOMPLETE (terminated because Precondition of `local` cannot be evaluated)
  23   - Abstract RAC: INCOMPLETE (terminated because Precondition of `local` cannot be evaluated)
  24 File "bench/check-ce/703_reduce_term.mlw", line 391, characters 4-55:
  25 Sub-goal Precondition of goal def'vc.
  26 Prover result is: Unknown (unknown + incomplete) (33345 steps).
  27 The following counterexample model could not be verified
  28   (both RAC terminated because Precondition of `local` cannot be evaluated):
  29 File 703_reduce_term.mlw:
  30   Line 5:
  31     base : t = 3
  32   Line 390:
  33     __void_param :  = Tuple0
  34     __void_param :  = Tuple0
  35