# HG changeset patch
# User blanchet
# Date 1314107427 -7200
# Node ID 1b0a31b7cfe877dc0a41d9a43e0df8653c0e17ea
# Parent  a39d94de1aeb7392407b7a9dcf334256a9bb642a
updated known failures for Z3 3.0 TPTP

diff -r a39d94de1aeb -r 1b0a31b7cfe8 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 15:18:46 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 15:50:27 2011 +0200
@@ -356,11 +356,11 @@
      "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
    proof_delims = [],
    known_failures =
-     [(Unprovable, "\nsat"),
-      (GaveUp, "\nunknown"),
-      (GaveUp, "SZS status Satisfiable"),
-      (ProofMissing, "\nunsat"),
-      (ProofMissing, "SZS status Unsatisfiable")],
+     [(GaveUp, "SZS status Satisfiable"),
+      (GaveUp, "SZS status CounterSatisfiable"),
+      (GaveUp, "SZS status GaveUp"),
+      (ProofMissing, "SZS status Unsatisfiable"),
+      (ProofMissing, "SZS status Theorem")],
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices =