Repository navigation
[PR] fix(verif): emit str.substr so cvc5 can parse slice queries — 3691 harness was silently solver-dead - #3980
Merged
Merged
Conversation
The Seq facade emitted (str.extract s i j); cvc5's SMT-LIB parser only knows str.substr, so every query touching the String#slice translation died in InputParser.nextCommand and the harness catch turned that into a silent skip. Since the #3935 clip-window rework made the truncation slice offsets symbolic, the bug3691 oscillation harness has been solver-dead on master - coverage lost with no red signal. Renamed to str.substr (also valid z3 syntax). Full verif suite: 15/15 pass, 0 skipped (was 14/15 with 1 silent skip).
Contributor
📦 Built Package ArtifactBranch: Option A — Install this exact build (recommended)npm install -g billion-context@0.0.4756-pr.3980.845a5bbThis exact version is immutable and reproducible. The rolling Option B — Download artifact
tar xzf billion-context-pr3980.tgz
npm install -g packageInstall instructions are refreshed on each push. |
ranxianglei
changed the title
Contributor
📦 Merged Build PublishedThis merge to master was published as npm install -g billion-context@0.0.682-master.8589423 # this exact build
npm install -g billion-context@master # always the newest merged build
|
This was referenced Oct 20, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
(ai: zhipuai-lb/glm-5.3)
What broke
verif/terms.ts序列 facade 的extract()发射(str.extract s i j),但 cvc5 的 SMT-LIB 解析器只认识str.substr。任何触到String#slice翻译的 query 在InputParser.nextCommand直接抛RuntimeError: Symbol 'str.extract' not declared as a variable,而 harness 的 catch 把求解器异常转成 静默 skip。自 #3935 截断窗口改造使截断 slice 偏移变成符号量后,
bug3691振荡 harness 在 master 上一直是 solver-dead —— 覆盖率丢了却没有红灯。Fix
一行:发射名
str.extract→str.substr(z3 同样接受)。Evidence
verif-bug3691-oscillation.test.ts1 pass / 1 skipped(master 805c0a5 与 74090ac 均复现,cvc5 直接解析报错)VERIF_PYTHON=/tmp/verifenv12/bin/python)Scope
仅
verif/一行,无 kernel 改动,与 #3961(wire 保真)无文件冲突。Part of #3938(判官/证明层可用性)。