# HG changeset patch
# User blanchet
# Date 1298040292 -3600
# Node ID 70d4585b11a61ba6032f5879a5049e7f4e5d270a
# Parent  a710e96583d5358bfec5c7f31bd3fedafcd44be9
better fudge factors for Sledgehammer

diff -r a710e96583d5 -r 70d4585b11a6 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Feb 18 15:44:52 2011 +0100
@@ -62,7 +62,7 @@
     avail = make_avail is_remote "CVC3",
     command = make_command is_remote "CVC3",
     options = cvc3_options,
-    default_max_relevant = 250,
+    default_max_relevant = 200,
     supports_filter = false,
     outcome =
       on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
@@ -86,7 +86,7 @@
   options = (fn ctxt => [
     "--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
     "--smtlib"]),
-  default_max_relevant = 275,
+  default_max_relevant = 200,
   supports_filter = false,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   cex_parser = NONE,
@@ -131,7 +131,7 @@
     avail = make_avail is_remote "Z3",
     command = z3_make_command is_remote "Z3",
     options = z3_options,
-    default_max_relevant = 225,
+    default_max_relevant = 250,
     supports_filter = true,
     outcome = z3_on_last_line,
     cex_parser = SOME Z3_Model.parse_counterex,