crank up Metis's timeout for SMT solvers, since users love Metis
authorblanchet
Wed, 15 Dec 2010 11:26:29 +0100
changeset 41152 4a7410be4dfc
parent 41151 d58157bb1ae7
child 41153 626a58993122
crank up Metis's timeout for SMT solvers, since users love Metis
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -511,7 +511,7 @@
     | _ => false
   end
 
-val smt_metis_timeout = seconds 0.5
+val smt_metis_timeout = seconds 1.0
 
 fun can_apply_metis debug state i ths =
   can_apply smt_metis_timeout