Flaky: TestSolve_HardTimeout_FakeSolverIgnoringT reds `go test ./...` on clean dev (pidfile race, survived the CI-flake sprint)

[sunholo-voight-kampff]

go test ./... is red on unmodified dev for internal/smt, while the same test passes in isolation. Found during mission iteration 151 while verifying an unrelated sprint (#601) outside the codex sandbox; it is not caused by that change.

Measurement

Two controlled arms, run on both the main checkout at 263df3df8 (unmodified) and a sprint worktree:

Arm	Command	Result
Full suite	go test ./...	rc=1 — FAIL internal/smt
Isolated test	go test ./internal/smt -run TestSolve_HardTimeout_FakeSolverIgnoringT	rc=0
Whole package	go test -count=1 ./internal/smt	rc=0

The full-suite arm was also run with no other load and still failed, so this is not an artifact of my running two suites concurrently.

Failure:

--- FAIL: TestSolve_HardTimeout_FakeSolverIgnoringT (3.00s)
    solver_timeout_test.go:42: read child pid: open /tmp/.../TestSolve_HardTimeout_FakeSolverIgnoringT.../001/child.pid: no such file or directory

Cause

internal/smt/solver_timeout_test.go:19 calls Solve with Timeout: time.Second against a fake solver script that writes its PID to a file and then sleeps. readChildPID (line 42) then reads that pidfile.

The test assumes the child process gets scheduled and writes its pidfile before the 1s solver timeout kills it. Under the parallel load of a full go test ./..., that assumption can lose: the child is killed before the write lands, the pidfile never exists, and readChildPID fails. Nothing in the test waits for the pidfile to appear.

This is a defect in the test, not in the hard-timeout mechanism it covers — Solve behaved correctly in every observed run (the status/elapsed/error assertions above line 42 all passed).

Why CI is green

CI runs the identical go test -timeout 300s ./... (.github/workflows/ci.yml:98) and dev is green at 263df3df8, so the runners' load profile happens to stay on the winning side of the race. That makes this a latent CI flake rather than a purely local annoyance — the same class the just-closed M-CI-FLAKE-SYSTEMIC-FIX sprint (#591–#600) was about, and it is a survivor of it.

Suggested fix

Poll for the pidfile with a bounded deadline instead of assuming it exists by the time the solver timeout fires — or have the fake solver write its pidfile before doing anything else and have the test wait on that file with a bounded retry, failing loudly on expiry. internal/testutil's bounded helpers (added in #591) are the natural home for the wait.

Related: TestSolve_HardTimeout_FakeSolverIgnoringT is also one of the two tests already known to fail from a /tmp-rooted checkout, so it is sensitive to both tmp location and timing.

🤖 Generated with Claude Code

[sunholo-voight-kampff]

Measured (mission iteration 154): the race is REAL, but the budget is 3s — not 1s — and the rate is ~1 in 300

Reproduction was attempted first-party at e70fb7484 before any fix. The suite did not red in either
full-suite arm — so this is not "confirmed by re-running it". It is confirmed by measuring the
variable directly, which also corrects the Cause section above.

Correction: the fake solver's budget is ~3s, not 1s

The Cause section says the child is killed by "the 1s solver timeout". It isn't. solver.go:158:

hardTimeout := max(config.Timeout, effectiveTimeout) + solverKillGrace   // solverKillGrace = 2s

With Timeout: time.Second, timeoutSecs=1 → effectiveTimeout=1s → hardTimeout = 3s.
Corroborated rather than just read: the isolated arm takes 3.274s.

The two full-suite arms did NOT reproduce

Arm	Command	Result	Control
A	go test ./internal/smt -run TestSolve_HardTimeout_FakeSolverIgnoringT -count=1	rc=0 (3.274s)	—
B	go test -count=1 ./internal/smt	rc=0 (8.217s)	—
C	go test ./...	rc=0, 0 FAIL	108 ok; but 86 cached, only 22 ran
D	go test -count=1 ./...	rc=0, 0 FAIL	108 ran for real, 0 cached; smt ok 9.446s

Arm C is reported with its limitation attached: a warm cache meant it was a much lighter load than the
issue's conditions. Arm D is the honest full-load arm. internal/smt took 9.4s under load vs 8.2s
alone, so load does bite — just not enough to red on these two runs.

The direct measurement — this is the actual finding

A standalone probe replicating the spawn exactly (same script, same Setpgid, fresh TempDir +
freshly-written script per trial) measuring time from spawn to child.pid appearing:

Condition	n	mean	max	over 3s budget
Idle	200	209ms	232ms	0
During go test -count=1 ./... (load 13.6)	150	424ms	3.435s	1
During go test -count=1 ./... (load 24.4)	150	219ms	268ms	0

One spawn in 300 under load exceeded the budget, at 3.435s against 3s — margin −435ms. That
run is exactly the reported failure: the pidfile does not exist when readChildPID reads it.

So the defect is confirmed at a rate of ~0.3% per spawn. The package spawns twice
(TestSolve_... and TestZ3Version_...), so ~0.7% per suite run — which is why CI stays green,
why it survived the CI-flake sprint, and why a couple of local runs cannot refute it.

Worth noting against the "load" framing: the over-budget trial occurred at load 13.6, not at the
higher 24.4. This is an outlier/tail effect (first exec of a freshly written script — page-in and
signature validation), not a smooth function of load average. A fix tuned to "more load" would miss it.

What this implies for the fix

The suggested fix — poll for the pidfile with a bounded deadline — does not work on its own. When
the race is lost the shell was killed before echo $! > file ever ran, so the file will never
appear no matter how long the test waits. (Note the grandchild is forked before the write, so a
lost race can also orphan a sleep whose PID nothing ever recorded.)

Grounded in the 0.3% figure, the fix that is both fast and non-vacuous is retry-on-inconclusive:
if the pidfile is absent, the trial proved nothing about process-group kill — retry the whole
scenario, bounded, and fail loudly if every attempt loses. At p≈0.003, three attempts leave a
~3e-8 residue. Crucially it cannot mask a real regression: if killProcessGroup breaks, the
assertProcessGoneWithin assertion fails on every attempt, so the test still reds deterministically.

🤖 Generated with Claude Code