1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jul 26 14:50:15 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jul 26 14:53:00 2011 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4      handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
     1.5  )
     1.6  
     1.7 -fun to_secs time = (Time.toMilliseconds time + 999) div 1000
     1.8 +fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
     1.9  
    1.10  val sosN = "sos"
    1.11  val no_sosN = "no_sos"
    1.12 @@ -200,7 +200,7 @@
    1.13     arguments =
    1.14       fn ctxt => fn _ => fn method => fn timeout => fn weights =>
    1.15          "--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
    1.16 -        " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout),
    1.17 +        " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
    1.18     proof_delims = tstp_proof_delims,
    1.19     known_failures =
    1.20       [(Unprovable, "SZS status: CounterSatisfiable"),
    1.21 @@ -240,7 +240,7 @@
    1.22     required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
    1.23     arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
    1.24       ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
    1.25 -      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
    1.26 +      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
    1.27       |> sos = sosN ? prefix "-SOS=1 ",
    1.28     proof_delims = [("Here is a proof", "Formulae used in the proof")],
    1.29     known_failures =
    1.30 @@ -275,7 +275,7 @@
    1.31    {exec = ("VAMPIRE_HOME", "vampire"),
    1.32     required_execs = [],
    1.33     arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
    1.34 -     "--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^
    1.35 +     "--proof tptp --mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
    1.36       " --thanks \"Andrei and Krystof\" --input_file"
    1.37       |> sos = sosN ? prefix "--sos on ",
    1.38     proof_delims =
    1.39 @@ -313,7 +313,7 @@
    1.40    {exec = ("Z3_HOME", "z3"),
    1.41     required_execs = [],
    1.42     arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
    1.43 -     "MBQI=true -p -t:" ^ string_of_int (to_secs timeout),
    1.44 +     "MBQI=true -p -t:" ^ string_of_int (to_secs 1 timeout),
    1.45     proof_delims = [],
    1.46     known_failures =
    1.47       [(Unprovable, "\nsat"),
    1.48 @@ -373,7 +373,7 @@
    1.49    {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    1.50     required_execs = [],
    1.51     arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
    1.52 -     "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs timeout))
    1.53 +     "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
    1.54       ^ " -s " ^ the_system system_name system_versions,
    1.55     proof_delims = union (op =) tstp_proof_delims proof_delims,
    1.56     known_failures = known_failures @ known_perl_failures @