src/HOL/Tools/SMT/smt_systems.ML

--- 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 }