--- 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, ""))