Give a timed-out solver a chance to clean up after itself

[coord-e]

Closes #49.

The cause

Two things together, of which only the first is described in the issue.

Thrust ends a solver that exceeds its timeout with SIGKILL (terminate_for_timeout), which the process cannot act on. But even a wrapper that could run a trap would not have been enough: docker run is only a client of the daemon, so killing it does not touch the container, and --rm removes a container once it stops, which a running solver never does on its own. Observed after killing the wrapper:

9534     1 /bin/bash ./tests/thrust-pcsat-wrapper ...   # reparented to init, still alive
9536  9534 docker start --attach 7e35cdcd...            # the client is alive too

Nothing tells the container to stop, so the solver runs until it finishes — forever on an instance it cannot solve, which is how the issue was hit.

The change

Thrust sends SIGTERM and kills only what has not exited two seconds later, so a solver command that holds resources of its own can release them. terminate_for_timeout is dropped, which is also what keeps the escalation safe: without it the child is neither killed nor reaped on timeout, so its identifier stays allocated and the later SIGKILL cannot reach an unrelated process.

The wrapper removes its container from a SIGTERM trap. It starts the container in the background and waits on it, because bash runs a trap only once the command in the foreground has finished — which would be the very solver the signal is meant to stop. docker create + docker start --attach replaces docker run so the trap has the container's id before the solver starts; it reports the same output and exit status.

nix (signal feature only) is added for kill; libc directly would have been the first unsafe in src/.

Verification

Against the pinned COAR_IMAGE, with THRUST_SOLVER_TIMEOUT_SECS=1 on tests/ui/pass/iterators/annot_range_loop.rs:

• error: verification error: Timeout(1s), the running container is gone, and the run takes 3.3s — the 1s timeout plus the 2s grace.
• A stub solver that ignores SIGTERM (trap '' TERM; sleep 300) is killed by the escalation, and Thrust does not hang on it.
• cargo test: 308 UI tests and 2 doc tests pass, with no container and no stray .smt2 left behind. The stray temp files are incidentally fixed too — the wrapper's EXIT trap could not run under SIGKILL either.

Note

A solver command that ignores SIGTERM still leaves its own children orphaned, since the escalation reaches only the direct child. That is unchanged, and holds for any command that declines to clean up after itself.

---

Generated by Claude Code