--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 25 14:58:20 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 25 14:58:50 2010 +0100
@@ -104,8 +104,9 @@
else is_atp_installed thy name
end
-val smt_default_max_relevant = 200 (* FUDGE *)
-val auto_max_relevant_divisor = 2 (* FUDGE *)
+(* FUDGE *)
+val smt_default_max_relevant = 200
+val auto_max_relevant_divisor = 2
fun default_max_relevant_for_prover thy name =
if is_smt_prover name then smt_default_max_relevant
@@ -432,6 +433,7 @@
| failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
| failure_from_smt_failure _ = UnknownError
+(* FUDGE *)
val smt_max_iter = 8
val smt_iter_fact_divisor = 2
val smt_iter_min_msecs = 5000