--- a/src/HOL/Tools/SMT/smt_systems.ML Wed Nov 19 10:31:15 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML Wed Nov 19 10:31:15 2014 +0100
@@ -85,10 +85,10 @@
avail = make_avail "CVC4",
command = make_command "CVC4",
options = cvc4_options,
- smt_options = [],
+ smt_options = [(":produce-unsat-cores", "true")],
default_max_relevant = 400 (* FUDGE *),
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
- parse_proof = NONE,
+ parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
replay = NONE }
end