better fudge factors for CVC3 and Yices based on Judgment Day
authorblanchet
Mon, 21 Feb 2011 14:02:07 +0100
changeset 41800 7f333b59d5fb
parent 41799 98b3d5ce0935
child 41801 ed77524f3429
better fudge factors for CVC3 and Yices based on Judgment Day
src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Feb 21 13:59:44 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Feb 21 14:02:07 2011 +0100
@@ -62,7 +62,7 @@
     avail = make_avail is_remote "CVC3",
     command = make_command is_remote "CVC3",
     options = cvc3_options,
-    default_max_relevant = 200 (* FUDGE *),
+    default_max_relevant = 150 (* FUDGE *),
     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 = 200 (* FUDGE *),
+  default_max_relevant = 150 (* FUDGE *),
   supports_filter = false,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   cex_parser = NONE,