changeset 61611 | a9c0572109af |
parent 61587 | c3974cd2d381 |
child 63102 | 71059cf60658 |
--- a/src/HOL/Tools/SMT/smt_systems.ML Tue Nov 10 14:43:29 2015 +0000 +++ b/src/HOL/Tools/SMT/smt_systems.ML Tue Nov 10 17:49:54 2015 +0100 @@ -109,7 +109,7 @@ smt_options = [(":produce-proofs", "true")], default_max_relevant = 200 (* FUDGE *), outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" - "warning : proof_done: status is still open"), + "(error \"status is not unsat.\")"), parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), replay = NONE }