From 0ef1a17bf42f7ab1ed2d86a18d30b905109b812a Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 15 Aug 2026 00:52:22 +0000 Subject: [PATCH 1/2] Pipe the solver's stderr instead of inheriting it A solver timeout terminates the solver process itself, not anything that process spawned. `tests/thrust-pcsat-wrapper` spawns `docker run`, so a timed-out pcsat test leaves that container client running with the stderr it inherited, which is the pipe `ui_test` reads the whole `thrust-rustc` invocation from. `thrust-rustc` exits, but the survivor holds a write end open, so the read never reaches EOF and `cargo test` stops making progress. Give the solver its own stderr pipe. A survivor then holds a descriptor that dies with `thrust-rustc` rather than one the test harness waits on. It also fills in the `stderr` of `CheckSatError::Error`, which was always empty while the solver wrote straight to the inherited descriptor. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01FrCiKotN28PrBDKAheSAYc --- src/chc/solver.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/chc/solver.rs b/src/chc/solver.rs index 5792d756..3c3ffba2 100644 --- a/src/chc/solver.rs +++ b/src/chc/solver.rs @@ -75,6 +75,7 @@ impl CommandConfig { .args(&self.args) .arg(path_arg) .stdout(stdout) + .stderr(std::process::Stdio::piped()) .spawn()?; tracing::info!(program = self.name, args = ?self.args, path = %path_arg.to_string_lossy(), pid = child.id(), "spawned"); From f2345cb7d55318796ea8446266c52b468a99aca3 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 15 Aug 2026 00:52:22 +0000 Subject: [PATCH 2/2] Note the COAR image pull in CLAUDE.md Thirty-four ui tests solve inside the container `tests/thrust-pcsat-wrapper` runs. CI pins that image by digest and pulls it before `cargo test`; a session that does neither has each of those tests fall back to the `:main` tag and pull the image itself, under the solver timeout meant for solving. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01FrCiKotN28PrBDKAheSAYc --- CLAUDE.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CLAUDE.md b/CLAUDE.md index 7428b5a8..1926e77c 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -26,3 +26,6 @@ keep from reaching it. Neither prerequisite of `cargo test` is set up in the session container. Install Z3 at the version `.github/actions/setup-z3` pins for CI, and start a Docker daemon with `dockerd &`. The daemon dies from time to time, so restart it whenever the tests that need it fail. + +Export the `COAR_IMAGE` digest that `.github/workflows/ci.yml` pins, and `docker pull` it +before running `cargo test`.