# HG changeset patch
# User Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1636041003 -3600
# Node ID 634e2323b6cf7ea29c6fd44694521853ff56fa40
# Parent  55a4b319b2b9a7ec99facb8186bce357f6d748dc
proper support of verit's return code for timeout

diff -r 55a4b319b2b9 -r 634e2323b6cf src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Nov 04 15:57:21 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Nov 04 16:50:03 2021 +0100
@@ -81,8 +81,11 @@
           with_trace ctxt ("Using cached certificate from " ^
             Path.print (Cache_IO.cache_path_of certs) ^ " ...") I output))
 
-(* Z3 returns 1 if "get-proof" or "get-model" fails. veriT returns 255. *)
-val normal_return_codes = [0, 1, 255]
+(* Z3 and cvc returns 1 if "get-proof" or "get-model" fails.
+veriT returns 255 in that case and 14 for timeouts. *)
+fun normal_return_codes "z3" = [0, 1]
+  | normal_return_codes "verit" = [0, 14, 255]
+  | normal_return_codes _ = [0, 1]
 
 fun run_solver ctxt name mk_cmd input =
   let
@@ -99,7 +102,7 @@
     val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
     val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
 
-    val _ = member (op =) normal_return_codes return_code orelse
+    val _ = member (op =) (normal_return_codes name) return_code orelse
       raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
   in output end
 
diff -r 55a4b319b2b9 -r 634e2323b6cf src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Thu Nov 04 15:57:21 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Thu Nov 04 16:50:03 2021 +0100
@@ -126,7 +126,7 @@
   options = veriT_options,
   smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 200 (* FUDGE *),
-  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "timeout"),
+  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"),
   parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
   replay = SOME Verit_Replay.replay }