src/HOL/Tools/ATP/atp_systems.ML
changeset 56404 9cb137ec6ec8
parent 56397 6e08b45432f6
child 56848 67e6803e3765
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Apr 04 14:44:51 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Apr 04 15:56:40 2014 +0200
@@ -620,7 +620,7 @@
 val z3_tptp_config : atp_config =
   {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
-     "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
+     "-core -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
    proof_delims = [("SZS status Theorem", "")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,