# HG changeset patch
# User blanchet
# Date 1277460472 -7200
# Node ID fc2f979b9a08347ef1834fb4ed9648f06ebc0798
# Parent  a62f742f1d580b11f6a75d55e988153c74bf5c77
split SPASS time slot between SOS and non-SOS, in case SOS times out

diff -r a62f742f1d58 -r fc2f979b9a08 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Thu Jun 24 21:01:13 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 25 12:07:52 2010 +0200
@@ -223,7 +223,7 @@
           val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss
           val result =
             do_run false
-            |> (fn (_, msecs0, _, SOME IncompleteUnprovable) =>
+            |> (fn (_, msecs0, _, SOME _) =>
                    do_run true
                    |> (fn (output, msecs, proof, outcome) =>
                           (output, msecs0 + msecs, proof, outcome))
@@ -298,9 +298,11 @@
 val spass_config : prover_config =
   {home_var = "SPASS_HOME",
    executable = "SPASS",
+   (* "div 2" accounts for the fact that SPASS is often run twice. *)
    arguments = fn complete => fn timeout =>
      ("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
-      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
+      \-VarWeight=3 -TimeLimit=" ^
+      string_of_int (to_generous_secs timeout div 2))
      |> not complete ? prefix "-SOS=1 ",
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =