# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1463723694 -7200
# Node ID 71059cf60658458955a901d7b050411c35486502
# Parent  65f1d7829463d68e215d1b0cf4e4911fc7cbc48c
better handling of veriT's 'unknown' status

diff -r 65f1d7829463 -r 71059cf60658 src/HOL/Tools/SMT/smt_solver.ML
--- 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
diff -r 65f1d7829463 -r 71059cf60658 src/HOL/Tools/SMT/smt_systems.ML
--- 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 }