-
David Hauzar authored
When resource limit is hit, cvc4 outputs useless counterexample. Query cvc4 for the reason of answer unknown and use the answer to decide whether resource limit was hit. If it was hit, do not display the counterexample. * src/driver/call_provers.{ml|mli} (parse_prover_run): If the prover answers unknown, get the information about the reason of this answer. * src/printer/smtv2.ml (print_prop_decl): Query solver for the reason of answer unknown. * src/driver/driver.ml (load_driver): Initialize Unknown with no information about the reason of answer unknown. * src/session/session.ml (load_result): Initialize Unknown with no information about the reason of answer unknown. * src/session/session_scheduler.ml (schedule_proof_attempt) (edit_proof): Initialize Unknown with no information about the reason of answer unknown. * src/why3session/why3session_lib.ml (filter_spec): Initialize Unknown with no information about the reason of answer unknown.
5c3038bf