--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Nov 07 18:15:13 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Nov 07 18:19:04 2010 +0100
@@ -7,7 +7,6 @@
val proverK = "prover"
val prover_timeoutK = "prover_timeout"
-val prover_hard_timeoutK = "prover_hard_timeout"
val keepK = "keep"
val full_typesK = "full_types"
val minimizeK = "minimize"
@@ -407,8 +406,7 @@
val (prover_name, prover) = get_prover (Proof.context_of st) args
val dir = AList.lookup (op =) args keepK
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
- val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
- |> Option.map (fst o read_int o explode)
+ val hard_timeout = SOME timeout (* always use a hard timeout *)
val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st
in
case result of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Nov 07 18:15:13 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Nov 07 18:19:04 2010 +0100
@@ -420,14 +420,8 @@
fun smt_filter_loop iter outcome0 msecs_so_far remote timeout state facts i =
let
val timer = Timer.startRealTimer ()
- (* The "timeout" argument passed to "smt_filter" is a soft timeout. We make
- it hard using "timeLimit". *)
val {outcome, used_facts, run_time_in_msecs} =
- TimeLimit.timeLimit timeout
- (SMT_Solver.smt_filter remote timeout state facts) i
- handle TimeLimit.TimeOut =>
- {outcome = SOME SMT_Solver.Time_Out, used_facts = [],
- run_time_in_msecs = NONE}
+ SMT_Solver.smt_filter remote timeout state facts i
val outcome0 = if is_none outcome0 then SOME outcome else outcome0
val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
val too_many_facts_perhaps =