Fix #288: [milestone Milestone 12] internal/symbolic/cache — Decision cache for Z3 queries: LRU cache keyed by ...

[telleroutlook]

Fixes #288

Generated by claude-bot-go worker.

[telleroutlook]

Summary

Cache hits can return incorrect solver timing metadata, masking whether solving occurred.

Severity

medium

Blocking findings

1. internal/z3/z3.go:60 On a cache hit, solutionFromDecision returns a Solution with SolverMs set to zero, so callers receive misleading solver timing metadata instead of the elapsed solver time expected from SolveConstraintsCtx.

Verdict

❌ Rejected

Merge risk

medium

Audit

• model: opus
• effort: high
• tokens: input=0, output=0

{
  "approved": false,
  "severity": "medium",
  "summary": "Cache hits can return incorrect solver timing metadata, masking whether solving occurred.",
  "findings": [
    {
      "file": "internal/z3/z3.go",
      "line": 60,
      "issue": "On a cache hit, solutionFromDecision returns a Solution with SolverMs set to zero, so callers receive misleading solver timing metadata instead of the elapsed solver time expected from SolveConstraintsCtx.",
      "kind": "blocker"
    }
  ],
  "merge_risk": "medium",
  "Model": "opus",
  "model": "codex",
  "effort": "high",
  "tokens": {
    "input_tokens": 0,
    "output_tokens": 0
  },
  "same_verdict_count": 1
}

[telleroutlook]

Summary

The PR appears safe to merge, with one minor cache-isolation concern.

Severity

low

Blocking findings

1. internal/symbolic/cache/cache.go:161 cloneDecision copies the Model map only shallowly, so nested maps or slices stored as values can still be mutated through a retrieved decision and alter cached state.

Verdict

✅ Approved

Merge risk

low

Audit

• model: opus
• effort: high
• tokens: input=0, output=0

{
  "approved": true,
  "severity": "low",
  "summary": "The PR appears safe to merge, with one minor cache-isolation concern.",
  "findings": [
    {
      "file": "internal/symbolic/cache/cache.go",
      "line": 161,
      "issue": "cloneDecision copies the Model map only shallowly, so nested maps or slices stored as values can still be mutated through a retrieved decision and alter cached state.",
      "kind": "suggestion"
    }
  ],
  "merge_risk": "low",
  "Model": "opus",
  "model": "codex",
  "effort": "high",
  "tokens": {
    "input_tokens": 0,
    "output_tokens": 0
  },
  "same_verdict_count": 1
}