From 5f40c06c51c7071946dcbf0984a3aae50895fa77 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Tue, 6 Oct 2026 11:53:17 +0200
Subject: [PATCH] fix(smt): do not wait for provers whose interrupt was lost

When a prover answers, the remaining ones are interrupted and waited
for. why3server kills the process group of a prover, but that group
is created by the forked child itself. An interrupt sent right after
the run request (typically when the first prover already answered
while the next task was being prepared) can be handled before the
group exists: the kill is silently lost and `smt` waits until the
loser reaches its own time limit.

Re-send the interrupt until the prover is reported as finished,
instead of blocking on the first one. Retries start after 10ms and
back off exponentially up to 1s.
---
 src/ecProvers.ml | 40 ++++++++++++++++++++++++++++++++--------
 1 file changed, 32 insertions(+), 8 deletions(-)

diff --git a/src/ecProvers.ml b/src/ecProvers.ml
index ccb56bbb2..9e2f74e60 100644
--- a/src/ecProvers.ml
+++ b/src/ecProvers.ml
@@ -658,12 +658,36 @@ let execute_task ?(notify : notify option) (pi : prover_infos) task =
       else if !status = 0 then None
       else if !status < pi.pr_quorum then None else Some true)
 
-    (* Clean-up: hard kill + wait for remaining provers *)
+    (* Clean-up: hard kill + wait for remaining provers.                *)
+    (*                                                                  *)
+    (* why3server kills the process group of the prover, which the      *)
+    (* forked child creates itself. An interrupt received right after   *)
+    (* the run request may be handled before that group exists: the     *)
+    (* kill is then lost and the prover runs until its own time limit.  *)
+    (* We therefore re-send the interrupt until the prover is reported  *)
+    (* as finished, instead of blocking on the first one. Retries start *)
+    (* at 10ms (the group exists by then) and back off up to 1s.        *)
     (fun () ->
-      for i = 0 to (Array.length pcs) - 1 do
-        match pcs.(i) with
-        | None -> ()
-        | Some (_prover, pc) ->
-            CP.interrupt_call ~config:(Config.main ()) pc;
-            (try ignore (CP.wait_on_call pc : CP.prover_result) with _ -> ());
-      done)
+      let config = Config.main () in
+
+      let finished pc =
+        match CP.query_call pc with
+        | CP.ProverFinished _
+        | CP.ProverInterrupted
+        | CP.InternalFailure _ -> true
+        | CP.NoUpdates
+        | CP.ProverStarted -> false in
+
+      let interrupt pc =
+        try CP.interrupt_call ~config pc with _ -> () in
+
+      let pcs = List.pmap (omap snd) (Array.to_list pcs) in
+
+      List.iter interrupt pcs;
+      List.iter (fun pc ->
+        let rec wait delay =
+          let finished = try finished pc with _ -> true in
+          if not finished then begin
+            Unix.sleepf delay; interrupt pc; wait (min 1.0 (2.0 *. delay))
+          end
+        in wait 0.01) pcs)