bench/check-ce/oracles/falseCE_Z3,4.8.10_SP.oracle

   1 <check_ce:categorization>Categorizations of models:
   2 - Selected model 0: BAD_CE
   3   - Concrete RAC: STUCK (failure in precondition of `rsa` at "bench/check-ce/falseCE.mlw", line 12, characters 4-7)
   4   - Abstract RAC: STUCK (failure in precondition of `rsa` at "bench/check-ce/falseCE.mlw", line 12, characters 4-7)
   5 File "bench/check-ce/falseCE.mlw", line 15, characters 11-21:
   6 Sub-goal Assertion of goal rsa'vc.
   7 Prover result is: Step limit exceeded (3000020 steps).
   8 Sorry, we don't have a good counterexample for you :(
   9
  10