src/HOL/Tools/ATP/atp_systems.ML

   val extend = I
   fun merge data : T = Symtab.merge (eq_snd op =) data
     handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
 )
 
-fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
+fun to_secs time = (Time.toMilliseconds time + 999) div 1000
 
 
 (* E *)
-
-(* Give E an extra second to reconstruct the proof. Older versions even get two
-   seconds, because the "eproof" script wrongly subtracted an entire second to
-   account for the overhead of the script itself, which is in fact much
-   lower. *)
-fun e_bonus () =
-  if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000
 
 val tstp_proof_delims =
   [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
    ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
 

   {exec = ("E_HOME", "eproof"),
    required_execs = [],
    arguments = fn ctxt => fn slice => fn timeout => fn weights =>
      "--tstp-in --tstp-out -l5 " ^
      e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
-     " -tAutoDev --silent --cpu-limit=" ^
-     string_of_int (to_secs (e_bonus ()) timeout),
+     " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
      [(Unprovable, "SZS status: CounterSatisfiable"),
       (Unprovable, "SZS status CounterSatisfiable"),
       (ProofMissing, "SZS status Theorem"),

 val spass_config : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/spass"),
    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
    arguments = fn ctxt => fn slice => fn timeout => fn _ =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
-      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
+      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
      |> (slice < 2 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
      known_perl_failures @
      [(GaveUp, "SPASS beiseite: Completion found"),

 
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
    arguments = fn ctxt => fn slice => fn timeout => fn _ =>
-     "--proof tptp --mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
+     "--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^
      " --thanks \"Andrei and Krystof\" --input_file"
      |> (slice < 2 orelse Config.get ctxt vampire_force_sos)
         ? prefix "--sos on ",
    proof_delims =
      [("=========== Refutation ==========",

 
 val z3_atp_config : atp_config =
   {exec = ("Z3_HOME", "z3"),
    required_execs = [],
    arguments = fn _ => fn _ => fn timeout => fn _ =>
-     "MBQI=true -p -t:" ^ string_of_int (to_secs 0 timeout),
+     "MBQI=true -p -t:" ^ string_of_int (to_secs timeout),
    proof_delims = [],
    known_failures =
      [(Unprovable, "\nsat"),
       (GaveUp, "\nunknown"),
       (GaveUp, "SZS status Satisfiable"),

 fun remote_config system_name system_versions proof_delims known_failures
                   conj_sym_kind prem_kind formats best_slice : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn _ => fn timeout => fn _ =>
-     "-t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
+     "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs timeout))
      ^ " -s " ^ the_system system_name system_versions,
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @
      [(Unprovable, "says Satisfiable"),
       (Unprovable, "says CounterSatisfiable"),