--- a/src/HOL/Tools/SMT2/smt2_systems.ML Tue Jun 03 10:13:44 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML Tue Jun 03 10:35:51 2014 +0200
@@ -55,9 +55,7 @@
command = make_command "CVC3_NEW",
options = cvc3_options,
default_max_relevant = 400 (* FUDGE *),
- can_filter = false,
- outcome =
- on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
+ outcome = on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
parse_proof = NONE,
replay = NONE }
@@ -77,7 +75,6 @@
string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
"--smtlib"]),
default_max_relevant = 350 (* FUDGE *),
- can_filter = false,
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
parse_proof = NONE,
replay = NONE }
@@ -143,7 +140,6 @@
command = z3_make_command "Z3_NEW",
options = z3_options,
default_max_relevant = 350 (* FUDGE *),
- can_filter = true,
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
parse_proof = SOME Z3_New_Replay.parse_proof,
replay = SOME Z3_New_Replay.replay }