# HG changeset patch
# User blanchet
# Date 1289150344 -3600
# Node ID a29b2fee592beb80773af3db69f1e63ea761ee61
# Parent  6461fc0f9f47d82fe82869546e5d76bf3524dca5
always use a hard timeout in Mirabelle

diff -r 6461fc0f9f47 -r a29b2fee592b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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
diff -r 6461fc0f9f47 -r a29b2fee592b src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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 =