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 ended 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 leaves the solver to exit on it, so a solver command that holds resources of its own can release them. terminate_for_timeout is dropped, which is also what makes the signal safe to send: without it the timed-out child is neither killed nor reaped, so its identifier stays allocated and cannot be handed to an unrelated process in the meantime.

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 1.26s, so nothing is spent waiting on the solver after the timeout.
• Repeated over six runs at 1s and 3s timeouts, with no container and no wrapper or client process left behind. An instrumented copy of the wrapper puts the SIGTERM 935ms after docker create was asked for a container, and the removal at 150-200ms after the signal.
• 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.

Notes

A solver command that does not exit on SIGTERM is left running; nothing kills it afterwards. So is anything it started of its own, as the signal reaches only the command itself.

A container is also left behind if the timeout expires in the moment between docker create being asked for a container and the trap being set, measured at ~55ms against a warm daemon. It takes a timeout far shorter than the 30s default to land there.

[Copilot]

Pull request overview

Updates solver timeout handling so processes can clean up resources before exiting, addressing issue #49.

Changes:

• Sends SIGTERM instead of immediately killing timed-out solvers.
• Adds Docker container cleanup to the PCSAT wrapper.
• Adds the nix signal dependency.

Reviewed changes

Copilot reviewed 3 out of 4 changed files in this pull request and generated 1 comment.

File	Description
tests/thrust-pcsat-wrapper	Traps SIGTERM and removes the solver container.
src/chc/solver.rs	Sends SIGTERM when solver execution times out.
Cargo.toml	Adds nix for signal handling.
Cargo.lock	Records updated dependencies.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.