Pipe the solver's stderr instead of inheriting it

[coord-e]

cargo test sometimes stops making progress locally while CI stays green. The hang is not
in the solver but in the pipe the test harness reads from.

A solver timeout terminates the solver process itself, not anything that process spawned.
tests/thrust-pcsat-wrapper spawns docker run, and CommandConfig::run set only stdout,
leaving stderr inherited — which, under ui_test, is the pipe Command::output() reads the
whole thrust-rustc invocation from. So a timed-out pcsat test leaves the container client
running with a write end of that pipe. thrust-rustc exits, the survivor keeps the
descriptor open, the read never reaches EOF, and ui_test waits forever. Plain z3 tests are
unaffected: there the timeout kills the only holder of the pipe.

CI does not hit this because it pins COAR_IMAGE by digest and pulls it before cargo test,
so the pcsat tests finish inside their timeout and nothing is orphaned. A local run without
that falls back to the :main tag and pulls the image under the solver timeout, which makes
the timeouts — and the orphans — routine.

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.

The second commit records the image pull in CLAUDE.md, next to the Z3 and dockerd setup
already documented there.

Verification

Both directions were checked against the real binary, with a stand-in solver that reproduces
the wrapper's shape (a bash script whose grandchild outlives a SIGKILL to it) driven through
the same Command::output() semantics ui_test uses, at a 5s solver timeout:

• before: thrust-rustc exits after 5s, the caller is still blocked at 60s
• after: the caller returns in 5.3s

The full suite passes with Z3 5.0.0 and the pinned COAR image: 316 ui tests and 2 doc tests,
plus cargo fmt --check and cargo clippy -- -D warnings.

Not addressed

This stops the harness from hanging; the orphaned docker run and its container still
survive the timeout and keep consuming CPU, which can cascade into further timeouts. Killing
the whole process group, or cleaning up the container from the wrapper via --cidfile and a
trap, would be a separate change.

---

Generated by Claude Code

[Copilot]

Pull request overview

This PR fixes a local test-harness hang by ensuring the external CHC solver’s stderr is captured via a dedicated pipe rather than inherited from the thrust-rustc process, preventing orphaned descendants (e.g., a timed-out docker run) from keeping the harness’ output pipe open indefinitely.

Changes:

• Pipe the solver’s stderr (Stdio::piped()) so orphaned descendants can’t hold open the harness’ inherited stderr pipe and so stderr is available for CheckSatError::Error.
• Document the need to pull the pinned COAR_IMAGE digest before running cargo test locally.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File	Description
src/chc/solver.rs	Pipes solver stderr so solver output collection is self-contained and avoids ui_test hangs caused by inherited pipes held open by orphaned subprocesses.
CLAUDE.md	Adds local testing guidance to pre-pull the pinned COAR image to avoid routine timeouts/orphans during image pulls.

---

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