# HG changeset patch
# User blanchet
# Date 1292676504 -3600
# Node ID 56b7e277fd7dc5a5396d0b971124dbdbff699688
# Parent  958fee9ec2757ba907a17f4a028e8d820c2e9c8f
higher hard timeout

diff -r 958fee9ec275 -r 56b7e277fd7d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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