src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 41268 56b7e277fd7d
parent 41266 b6b77c963f11
child 41274 6a9306c427b9
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 13:43:46 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 13:48:24 2010 +0100
@@ -419,7 +419,9 @@
     val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
     val dir = AList.lookup (op =) args keepK
     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
-    val hard_timeout = SOME timeout (* always use a hard timeout *)
+    (* always use a hard timeout, but give some slack so that the automatic
+       minimizer has a chance to do its magic *)
+    val hard_timeout = SOME (2 * timeout)
     val (msg, result) =
       run_sh prover_name prover type_sys hard_timeout timeout dir st
   in