one more LEO-II failure
authorblanchet
Wed, 19 Oct 2011 21:40:32 +0200
changeset 45207 1d13334628a9
parent 45206 fe8d0706a8aa
child 45208 9a00f9cc8707
one more LEO-II failure
src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Oct 19 19:45:19 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Oct 19 21:40:32 2011 +0200
@@ -258,7 +258,9 @@
         "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
         |> sos = sosN ? prefix "--sos ",
    proof_delims = tstp_proof_delims,
-   known_failures = known_szs_status_failures,
+   known_failures =
+     known_szs_status_failures @
+     [(TimedOut, "CPU time limit exceeded, terminating")],
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>