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