# HG changeset patch
# User desharna
# Date 1633335402 -7200
# Node ID 9b6dcf689efe9c871f46ba6697bd2954425aced0
# Parent  3604db245a639605840a184d4962affd5e221286
considered slices overhead in sledgehammer

diff -r 3604db245a63 -r 9b6dcf689efe src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Sep 29 16:48:23 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Oct 04 10:16:42 2021 +0200
@@ -211,7 +211,9 @@
           end
 
         val real_ms = Real.fromInt o Time.toMilliseconds
-        val slices_timeout = real_ms timeout
+        (* TODO: replace this seems-to-work per-slice overhead with actually-measured value *)
+        val slices_overhead_ms = Int.max (0, num_actual_slices * 25)
+        val slices_timeout_ms = real (Time.toMilliseconds timeout - slices_overhead_ms)
 
         fun run_slice time_left (cache_key, cache_value) (slice, (time_frac,
             (key as ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans,
@@ -228,7 +230,7 @@
             val slice_timeout =
               (real_ms time_left
                |> (if slice < num_actual_slices - 1 then
-                     curry Real.min (time_frac * slices_timeout)
+                     curry Real.min (time_frac * slices_timeout_ms)
                    else
                      I))
               * 0.001