[milestone Milestone 12 — Symbolic Reasoning Core] `internal/z3` — CGO bindings to Z3 4.13+: `Solve(constraints string, model map...

[telleroutlook]

🤖 Auto-filed from milestone doc bullet.

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

internal/z3 — CGO bindings to Z3 4.13+: Solve(constraints string, model map[string]any) (sat bool, model map[string]any, error) with SMT-LIB2 parsing; fallback to pure-Go solver when CGO unavailable via build tag !z3_cgo

Relevant code context (from worktree)

file: internal/z3/z3_test.go
file: internal/z3/z3.go
contains 'internal': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/claude-agent-sdk/src/memory.ts
contains 'internal': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/compliance/src/repair/RepairPlanner.ts
contains 'internal': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/cloudflare-worker/src/CloudflareWorkflowEngine.ts
contains 'bindings': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/cloudflare-worker/src/rateLimit.ts
contains 'bindings': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/cloudflare-worker/src/AgentDO.ts
contains 'bindings': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/evals-runner/src/suites/multi-turn-scaffold-arms.ts
contains 'solve': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/examples/benchmarks/judge/judge.py
contains 'solve': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/docs/examples/python-emitter/emit_record.py
contains 'solve': ""/tmp/tmp.ufhVOKX3Uq"/wasmagent-js"/packages/capability-compiler/src/index.ts

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.