[milestone Milestone 12 — Symbolic Reasoning Core] `bench/smt-comparison/` — solver evaluation harness: compare Z3 against `cel_e...

[telleroutlook]

🤖 Auto-filed from milestone doc bullet.

Repo: WasmAgent/symkernel
Milestone: Milestone 12 — Symbolic Reasoning Core: Z3 Integration (Phase 1b)
Bullet:

bench/smt-comparison/ — solver evaluation harness: compare Z3 against cel_expr and existing keyword/n-gram baseline on the 12 formal-verification tasks from bscode/fixtures/bench-v1/tasks/; measure solve time, memory footprint, and counterexample quality

Relevant code context (from worktree)

new (does not exist yet): bench/smt-comparison/
new (does not exist yet): keyword/n-gram
new (does not exist yet): bscode/fixtures/bench-v1/tasks/
contains 'bench': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/examples/benchmarks/judge/judge.py
contains 'bench': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/docs/.vitepress/config.ts
contains 'bench': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/claude-agent-sdk/src/index.ts
contains 'comparison': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/docs/.vitepress/config.ts
contains 'comparison': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/compliance/src/runner/ComplianceRun.ts
contains 'comparison': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/compliance/benchmarks/ifeval/compare-seeds.ts
contains 'solver': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/compliance/src/ir/ConstraintIR.test.ts
contains 'solver': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/compliance/src/ir/ConstraintIR.ts
contains 'solver': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/compliance/src/verifier/ComplianceVerifier.ts

Implementation note: Files marked "new (does not exist yet)" must be created from scratch. verify-first should return PROCEED (not NOT_YET) — there is no prerequisite blocking this work.

Acceptance criteria

• Command go build ./... passes
• The specific work described in the bullet above is implemented in the smallest number of files required.
• No unrelated files touched (git status --short output limited to the intended change).

Notes for the implementer

This issue was auto-created by SweepMilestoneBulletToIssue. The bullet text is verbatim
from the milestone doc. If ambiguous or too large for a single implement cycle,
verify-first should return NEEDS_SPLIT with sub-issue proposals or NEEDS_HUMAN with the blocker.

---

Filed automatically.

[telleroutlook]

Closing: repeated failures (retry_count >= 3) without successful implementation. Beyond current bot capability with available providers.