# HG changeset patch
# User desharna
# Date 1633335431 -7200
# Node ID d6f1ca21a3c1545a11dc0fe1c4fb698f4ff5b9ab
# Parent  9b6dcf689efe9c871f46ba6697bd2954425aced0
tuned zipperposition config in sledgehammer

diff -r 9b6dcf689efe -r d6f1ca21a3c1 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Oct 04 10:16:42 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Oct 04 10:17:11 2021 +0200
@@ -533,8 +533,8 @@
   in
     {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
      arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ =>
-       ["--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
-        |> extra_options <> "" ? prefix (extra_options ^ " ")],
+       ["--input tptp", "--output tptp", "--timeout " ^ Time.toString timeout, extra_options,
+        File.bash_path problem],
      proof_delims = tstp_proof_delims,
      known_failures =
        [(TimedOut, "SZS status ResourceOut")] @   (* odd way of timing out *)