# HG changeset patch
# User blanchet
# Date 1351679001 -3600
# Node ID 34b0464d7eef48620709c5090ce937829bee30fb
# Parent  4de92b4aa74a738ca89fad4f99894ce4390c31c2
soft SMT timeout

diff -r 4de92b4aa74a -r 34b0464d7eef src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Sun Oct 28 02:22:39 2012 +0000
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -60,7 +60,8 @@
 local
   fun cvc3_options ctxt = [
     "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
-    "-lang", "smtlib", "-output-lang", "presentation"]
+    "-lang", "smtlib", "-output-lang", "presentation",
+    "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]
 
   fun mk is_remote = {
     name = make_name is_remote "cvc3",
@@ -91,6 +92,8 @@
   command = make_local_command "YICES",
   options = (fn ctxt => [
     "--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
+    "--timeout=" ^
+      string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)),
     "--smtlib"]),
   default_max_relevant = 350 (* FUDGE *),
   supports_filter = false,
@@ -143,9 +146,12 @@
 
   fun z3_options ctxt =
     ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
-      "MODEL=true", "-smt"]
+      "MODEL=true",
+      "SOFT_TIMEOUT=" ^
+        string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)),
+      "-smt"]
     |> not (Config.get ctxt SMT_Config.oracle) ?
-         append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
+         append ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
 
   fun z3_on_first_or_last_line solver_name lines =
     let
diff -r 4de92b4aa74a -r 34b0464d7eef src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sun Oct 28 02:22:39 2012 +0000
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -157,8 +157,6 @@
   fun rewrite _ [] = I
     | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
 
-  fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
-
   fun lookup_assm assms_net ct =
     Z3_Proof_Tools.net_instances assms_net ct
     |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))