--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Sat Apr 21 11:15:49 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Sat Apr 21 11:15:49 2012 +0200
@@ -67,7 +67,7 @@
avail = make_avail is_remote "CVC3",
command = make_command is_remote "CVC3",
options = cvc3_options,
- default_max_relevant = 150 (* FUDGE *),
+ default_max_relevant = 400 (* FUDGE *),
supports_filter = false,
outcome =
on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
@@ -91,7 +91,7 @@
options = (fn ctxt => [
"--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
"--smtlib"]),
- default_max_relevant = 150 (* FUDGE *),
+ default_max_relevant = 350 (* FUDGE *),
supports_filter = false,
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
cex_parser = NONE,
@@ -163,7 +163,7 @@
avail = make_avail is_remote "Z3",
command = z3_make_command is_remote "Z3",
options = z3_options,
- default_max_relevant = 250 (* FUDGE *),
+ default_max_relevant = 350 (* FUDGE *),
supports_filter = true,
outcome = z3_on_last_line,
cex_parser = SOME Z3_Model.parse_counterex,