increased hard timeout -- minimization can take time
authorblanchet
Sat, 05 Jan 2013 22:31:31 +0100
changeset 50749 82dee320d340
parent 50748 c056718eb687
child 50750 518f0b5ef3d9
increased hard timeout -- minimization can take time
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Jan 05 22:31:30 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Jan 05 22:31:31 2013 +0100
@@ -68,7 +68,7 @@
                   {state, goal, subgoal, subgoal_count, facts} name =
   let
     val ctxt = Proof.context_of state
-    val hard_timeout = time_mult 2.0 (timeout |> the_default one_day)
+    val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, hard_timeout)
     val max_facts =