--- a/src/HOL/Tools/SMT/smt_solver.ML Wed May 18 12:24:33 2016 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri May 20 07:54:54 2016 +0200
@@ -81,8 +81,8 @@
with_trace ctxt ("Using cached certificate from " ^
Path.print (Cache_IO.cache_path_of certs) ^ " ...") I output))
-(* Z3 returns 1 if "get-model" or "get-model" fails *)
-val normal_return_codes = [0, 1]
+(* Z3 returns 1 if "get-proof" or "get-model" fails. veriT returns 255. *)
+val normal_return_codes = [0, 1, 255]
fun run_solver ctxt name mk_cmd input =
let
--- a/src/HOL/Tools/SMT/smt_systems.ML Wed May 18 12:24:33 2016 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML Fri May 20 07:54:54 2016 +0200
@@ -108,8 +108,7 @@
"--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]),
smt_options = [(":produce-proofs", "true")],
default_max_relevant = 200 (* FUDGE *),
- outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
- "(error \"status is not unsat.\")"),
+ outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown"),
parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
replay = NONE }