# HG changeset patch
# User blanchet
# Date 1693920228 -7200
# Node ID a7bcd2af71908705d3e221e22007471a4794d783
# Parent  d5a1d64a563d00a834d59f38540eb5d557572014
respect timeout better

diff -r d5a1d64a563d -r a7bcd2af7190 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Sep 03 19:28:59 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Sep 05 15:23:48 2023 +0200
@@ -464,7 +464,7 @@
   end
 
 fun run_sledgehammer (params as {verbose, spy, provers, falsify, induction_rules, max_facts,
-    max_proofs, slices, ...}) mode writeln_result i (fact_override as {only, ...}) state =
+    max_proofs, slices, timeout, ...}) mode writeln_result i (fact_override as {only, ...}) state =
   if null provers then
     error "No prover is set"
   else
@@ -577,6 +577,8 @@
             val launch = launch_prover_and_preplay params mode has_already_found_something
               found_something massage_message writeln_result learn
 
+            val timer = Timer.startRealTimer ()
+
             val schedule =
               if mode = Auto_Try then provers
               else schedule_of_provers provers slices
@@ -597,7 +599,8 @@
             else
               (learn chained_thms;
                Par_List.map (fn (prover, slice) =>
-                   if Synchronized.value found_proofs_and_falsifications < max_proofs then
+                   if Synchronized.value found_proofs_and_falsifications < max_proofs
+                      andalso Timer.checkRealTimer timer < timeout then
                      launch problem slice prover
                    else
                      (SH_None, ""))