[Zhishulo]

Fixes #4270

问题

tests/verif-generic-append-stability.test.ts:50 与 tests/verif-responses-ingress.test.ts:52 的 guard 写的是裸 t.skip(...)。t.skip() 只置标记、不中断函数体,所以无求解器环境下「跳过」之后 body 继续执行,第一次碰文件或求解器就抛错:node:test 于是在日志尾部再列一个 ✖ failing tests: 段(CI TAP 上即 not ok … # SKIP no SMT solver available),把干净 skip 渲染成失败——就是 #4140 instance 3 里那条掉出所有计数桶的畸形行。

同目录另外 7 个 solver-gated verif 测试都写的是 return t.skip(...)(bug3676-wire-reorder / bug3691-oscillation / bug3769-orphan-window / induction-append-stability / symbolic-smoke)。本 PR 把这两处对齐。

改动

2 行,无其他改动:

-  if (!haveSolver) t.skip("no SMT solver available (set VERIF_PYTHON or VERIF_SOLVER_CMD)");
+  if (!haveSolver) return t.skip("no SMT solver available (set VERIF_PYTHON or VERIF_SOLVER_CMD)");

验证(本机,无求解器,编译产物)

before:

﹣ generic append-only stability: … # no SMT solver available (…)
﹣ responses-ingress: … # no SMT solver available (…)
ℹ tests 2 / pass 0 / fail 0 / skipped 2

✖ failing tests:
test at …verif-generic-append-stability.test.js:35:1
﹣ generic append-only stability: … # no SMT solver available (…)
  Error: ENOENT: no such file or directory, open '…\kernel\src\refs.ts'
      at readFileSync → loadModule (verif/symbolic.js:281) → loadImportGraph (:255) → translateFunction (:377) → runAssign

after:

﹣ generic append-only stability: … # no SMT solver available (…)
﹣ responses-ingress: … # no SMT solver available (…)
ℹ tests 2 / pass 0 / fail 0 / skipped 2

无 ✖ failing tests: 段。另:npx tsc --noEmit -p tsconfig.json 与 emit(--noEmit false --outDir … --rewriteRelativeImportExtensions)均绿。

与相邻票的关系(避免重复/冲突)

• Windows: verif symbolic driver path gets a doubled drive letter (D:\D:\a\...) — solver-less CI renders skip-with-error #4195:记录了同一现象(windows 上 not ok … # SKIP + 双盘符 ENOENT),但归因于 verif/symbolic.ts:292-316 的 win32 路径拼接。即使 join 修对,body 仍会继续跑、随后撞 z3/python 缺失,skip-with-error 依旧;两个缺陷应分开修,本 PR 只补 guard 返回,不动 loadModule/loadImportGraph。
• [PR] fix: stabilize Windows CI flakes — verif detect-once solver cache + deterministic #286 migration savedAt (#4140 instances 3&4) #4269(open):在 body 的 Q1/Q2/Q3 加了 t.skip(...); return;,管的是「guard 探测通过、之后再丢求解器」;本 PR 管「一开始就没有求解器」。hunk 不重叠(generic 第 50 行 vs [PR] fix: stabilize Windows CI flakes — verif detect-once solver cache + deterministic #286 migration savedAt (#4140 instances 3&4) #4269 的 139/152/161),可无冲突合入;tests/verif-responses-ingress.test.ts 由本 PR 覆盖,[PR] fix: stabilize Windows CI flakes — verif detect-once solver cache + deterministic #286 migration savedAt (#4140 instances 3&4) #4269 未触及。
• Windows CI test shards go red randomly: two flake signatures (cleanup rmdir race in #1952 lease test, egress-fuse e2e hang in #4079) #4140:instance 3 的畸形 TAP 行由本 PR + [PR] fix: stabilize Windows CI flakes — verif detect-once solver cache + deterministic #286 migration savedAt (#4140 instances 3&4) #4269 两半合起来关闭。

影响面

仅测试 harness;有求解器环境 haveSolver 为 true,执行路径逐字节不变。无产品代码、无新配置、无 cache/wire/折叠行为变更,因此不涉及 kernel-change:。

[Zhishulo]

重复提示:#4272(ework 对 #4270 的自动分诊 PR)与本 PR 是同一处 2 行改动、同一 base(0a9c639),内容逐字节相同;本 PR 先开(384bc12),#4272 在 #4270 分诊后由机器人补开。

两份都可合,建议只保留一个:

• 若合本 PR → [PR] fix: verif solver-less entry guard must return — clean skip instead of skip-with-error #4272 可关闭(内容已被覆盖);
• 若合 [PR] fix: verif solver-less entry guard must return — clean skip instead of skip-with-error #4272 → 本 PR 可按 superseded 关闭,我不再改动这里。

不阻塞任何一方;证据与 before/after 输出在 #4270。若之后要合,请注意与 #4269 的 hunk 不重叠(本 PR 在 generic :50 / ingress :52,#4269 在 generic :139+),两者可独立合入。

[Zhishulo]

已 rebase 到当前 master 94f75cc（该 base 已含 #4195 的 df5e82412 fileURLToPath 修复），新 head c63b725，diff 仍恰好 2 行 × 1 行替换，与 #4269 的 body 内 hunk 不重叠。

新 base 上的本地复验（无求解器环境）：kernel tsc / tsc --noEmit / emit 全部 exit 0；单跑这两个测试 = tests 2 / pass 0 / fail 0 / skipped 2，报告里没有 ✖ failing tests: 段。修前同环境是 skipped 2 加一段 Error: ENOENT … kernel/src/refs.ts（readFileSync → loadModule → loadImportGraph → translateFunction → runAssign）。

补一点完整性证据（语句级清点，不是按消息字符串匹配）：tests/*.test.ts 共 64 个 .skip( 调用点 / 22 个文件。其中 15 个是同行 return t.skip(...)，47 个是 t.skip(...) 后紧跟 return;（含 verif-bug3691-oscillation.test.ts:88 的 catch (e) { t.skip(...); return; } 同行收尾），裸调用只有本 PR 的这 2 处。所以这个缺陷形状在仓库里没有第三处；#4269 处理的是测试中途求解器丢失（body 内），位置不同，两者互补。

另：本 PR 与自动生成的 #4272 内容等价（同一 issue 的两条路径），合任意一个即可，剩下的我按 superseded 处理。

[Zhishulo]

CI 重跑说明（同一 diff，新 head 37810b5d5）

上一轮 run 39735594754（head c63b72541）的 1 条红与本 PR 无关：

• job test (windows-latest, 22, 2)（119681287575），唯一失败簇在 tests/issue1993-preflight-400.test.ts:248（#1993 non-size 4xx does not shrink: 401 fails fast after exactly one summary call）：failureType: cancelledByParent、error: Promise resolution is still pending but the event loop has already resolved、duration_ms: 4884；同文件紧随的 1423/1424 为 duration_ms: 0 连坐，1420/1421 正常。
• 这是「事件循环提前排空」形态，与已关闭的 Flaky Windows CI: issue1993-preflight-400 suite cancelled by early event-loop drain | Windows CI 偶发假红：preflight-400 测试进程提前退出致 5 例取消 #3665（issue1993-preflight-400 suite cancelled by early event-loop drain）同签名，属 Windows CI test shards go red randomly: two flake signatures (cleanup rmdir race in #1952 lease test, egress-fuse e2e hang in #4079) #4140 清单家族（open 相关：CI false red: persistent event-loop drain blocks the merge gate, and same-machine retries can't recover it — a drain-pas | CI 假红: 持续性 event-loop drain 卡死合并门, 同机重试救不回, 需要 drain-pass 政策 (#3665 round 3) #4212、[PR] fix: bounded harness close + CI drain-cancel retry shape (#3356) | win22 分片收尾挂起不再无声连坐:harness 有界 close + 重试门识别 drain-cancel 形态 #3563）。该 job 日志里只有一次 runner 启动，无相内重试痕迹。
• 本 PR 只改两个 verif 测试入口守卫的 skip/return（test-harness-only），不存在影响该文件时序的机制路径；失败文件在另一个分片上跑。

处置：我没有上游 repo 的 Actions 重跑权限（POST /repos/ranxianglei/billion-context/actions/jobs/119681287575/rerun → 403 Must have admin rights to Repository.），因此通过改提交时间重触发同一 diff（head c63b72541 → 37810b5d5，改动仍为 2 files × 1 line，字节内容不变）。新 run 39757808610：8 条 e2e 车道 + PR Build Artifact 已 success，test 矩阵仍在跑。

[ranxianglei]

按取代关闭:与 #4272 平行的同题修复(verif 守卫 skip 缺 return),#4272 已于 2026-10-23 04:35 合并,#4270 已随之关闭。无遗留工作。