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