# 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 =