Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
increase defensive timeout that should typically not kick in thanks to solid time limits in Sledgehammer (otherwise, Mirabelle-based evaluations might be distorted)
authorboehmes
Tue, 07 Aug 2012 10:28:04 +0200
changeset 48702 e1752ccccc34
parent 48701 3b414244acb1
child 48703 d408ff0abf23
increase defensive timeout that should typically not kick in thanks to solid time limits in Sledgehammer (otherwise, Mirabelle-based evaluations might be distorted)
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 06 22:12:17 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 07 10:28:04 2012 +0200
@@ -533,7 +533,7 @@
     val max_new_mono_instancesLST =
       available_parameter args max_new_mono_instancesK max_new_mono_instancesK
     val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
-    val hard_timeout = SOME (2 * timeout)
+    val hard_timeout = SOME (4 * timeout)
     val (msg, result) =
       run_sh prover_name prover type_enc strict max_facts slice lam_trans
         uncurried_aliases e_selection_heuristic term_order force_sos
isabelle