CI test lane: verif SMT tests go red instead of auto-skipping when the runner's python lacks cvc5 #4431

来源: PR #4233 (#4233) 分析 #4200 时发现
查重: 无（检索 open+closed issues/PRs：cvc5 / SMT / solver / verif 签名均无既有条目）

Symptom

On the CI test lane (ubuntu-latest, node 24, shard 1 — run 39689822199, PR #4233 head 6cce12f), two verif property tests went RED although NO solver is configured in CI (no VERIF_PYTHON / VERIF_SOLVER_CMD is set anywhere under .github/workflows/):

• tests/verif-generic-append-stability.test.ts:48 — "generic append-only stability: arbitrary inputs over assignRefs + renderVisibleRefs"
• tests/verif-responses-ingress.test.ts:50 — "responses-ingress: idempotence, canonicalization, locality over the real pipeline"

Exact TAP signature of both:

not ok N - <test name> # SKIP no SMT solver available (set VERIF_PYTHON or VERIF_SOLVER_CMD)
  ---
  failureType: 'testCodeFailure'
  exitCode: 1
  error: |- ... ModuleNotFoundError: No module named 'cvc5'
  code: 'ERR_TEST_FAILURE'

The tests DO reach t.skip(...) (the # SKIP annotation is present on the line), yet the worker process still exits 1 — the solver-probe subprocess failure (runner python has no cvc5 module) escapes as an uncontained error AFTER the skip decision, turning a would-be skip into a shard failure.

Contract violated

AGENTS.md Key Design Decision 14 (verif module): solver tests "无求解器环境自动 skip 不会红" (auto-skip in solver-less environments, never red). The probe path — haveSolver IIFE calling solveSmt2("(set-logic ALL)(check-sat)", []) (tests/verif-generic-append-stability.test.ts:49, same pattern tests/verif-responses-ingress.test.ts:52) — must contain ANY spawn/exec failure of the probe itself (missing binary, non-zero exit, missing python module) as "no solver".

Impact

Any PR whose shard happens to draw these two files can go red on the affected lane for a reason unrelated to its diff — blocks merges and forces manual triage each occurrence. Because the 3-way sharding assigns different files per lane, the red appears intermittently across PRs and looks like a random flake.

Suggested fix

Contain the probe: treat any solver-probe execution failure as "no solver" → clean t.skip(); ensure the probe subprocess cannot propagate errors out of the haveSolver IIFE (await/settle the child before the skip decision, or capture its exit). Add a regression test that points VERIF_PYTHON at a stub interpreter that exits 1 with a ModuleNotFoundError and asserts the suite reports SKIP, not FAIL.

Note: observed once on PR #4233 (ubuntu node-24 shard 1). The windows node-22 shard 1 failure in the same run could not be attributed (job-log download truncated mid-run, zero not ok in the visible portion) and may be an unrelated flake.