Fix #290: [milestone Milestone 12] bench/symbolic/ — Symbolic execution benchmark suite: run against curated WA...

[telleroutlook]

Fixes #290

Generated by claude-bot-go worker.

[telleroutlook]

Summary

The changes appear merge-safe, but the substantive fixture tests are skipped when Z3 is unavailable.

Severity

low

Blocking findings

1. bench/symbolic/symbolic_test.go:56 All fixture execution tests skip when z3 is not on PATH, so CI can pass without validating module instantiation, solver results, or cache behavior unless the environment explicitly installs Z3.

Verdict

✅ Approved

Merge risk

low

Audit

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

{
  "approved": true,
  "severity": "low",
  "summary": "The changes appear merge-safe, but the substantive fixture tests are skipped when Z3 is unavailable.",
  "findings": [
    {
      "file": "bench/symbolic/symbolic_test.go",
      "line": 56,
      "issue": "All fixture execution tests skip when z3 is not on PATH, so CI can pass without validating module instantiation, solver results, or cache behavior unless the environment explicitly installs Z3.",
      "kind": "suggestion"
    }
  ],
  "merge_risk": "low",
  "Model": "opus",
  "model": "codex",
  "effort": "high",
  "tokens": {
    "input_tokens": 0,
    "output_tokens": 0
  },
  "same_verdict_count": 1
}

[telleroutlook]

Summary

The benchmark silently treats solver-unknown results as infeasible paths, producing incorrect path counts and potentially passing misleading results.

Severity

high

Blocking findings

1. bench/symbolic/symbolic.go:164 solvePaths increments the feasible count only for Sat == "sat" and silently treats "unknown" as unsatisfiable, so cancellations, timeouts, or unsupported queries undercount explored paths without returning an error.

Verdict

❌ Rejected

Merge risk

high

Audit

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

{
  "approved": false,
  "severity": "high",
  "summary": "The benchmark silently treats solver-unknown results as infeasible paths, producing incorrect path counts and potentially passing misleading results.",
  "findings": [
    {
      "file": "bench/symbolic/symbolic.go",
      "line": 164,
      "issue": "solvePaths increments the feasible count only for Sat == \"sat\" and silently treats \"unknown\" as unsatisfiable, so cancellations, timeouts, or unsupported queries undercount explored paths without returning an error.",
      "kind": "blocker"
    }
  ],
  "merge_risk": "high",
  "Model": "opus",
  "model": "codex",
  "effort": "high",
  "tokens": {
    "input_tokens": 0,
    "output_tokens": 0
  },
  "same_verdict_count": 1
}

[telleroutlook]

Summary

The new benchmark assertions can all be skipped when Z3 is unavailable, allowing CI to pass without exercising the PR's core behavior.

Severity

high

Blocking findings

1. bench/symbolic/symbolic_test.go:76 runNamedFixture skips every fixture assertion when z3 is not on PATH, so environments without an explicitly provisioned Z3 executable silently bypass the new benchmark coverage.

Verdict

❌ Rejected

Merge risk

high

Audit

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

{
  "approved": false,
  "severity": "high",
  "summary": "The new benchmark assertions can all be skipped when Z3 is unavailable, allowing CI to pass without exercising the PR's core behavior.",
  "findings": [
    {
      "file": "bench/symbolic/symbolic_test.go",
      "line": 76,
      "issue": "runNamedFixture skips every fixture assertion when z3 is not on PATH, so environments without an explicitly provisioned Z3 executable silently bypass the new benchmark coverage.",
      "kind": "blocker"
    }
  ],
  "merge_risk": "high",
  "Model": "opus",
  "model": "codex",
  "effort": "high",
  "tokens": {
    "input_tokens": 0,
    "output_tokens": 0
  },
  "same_verdict_count": 2
}

[telleroutlook]

Summary

The benchmark can report cache lookup time as solver work because the global decision cache is never cleared before the first measurement pass.

Severity

high

Blocking findings

1. bench/symbolic/symbolic.go:50 The documented first pass does not guarantee uncached solver work: decisionCache is global and may already contain these queries from earlier fixture tests or benchmark iterations, so SolverTime can measure only cache lookup latency and the reported benchmark metrics become incorrect.

Verdict

❌ Rejected

Merge risk

high

Audit

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

{
  "approved": false,
  "severity": "high",
  "summary": "The benchmark can report cache lookup time as solver work because the global decision cache is never cleared before the first measurement pass.",
  "findings": [
    {
      "file": "bench/symbolic/symbolic.go",
      "line": 50,
      "issue": "The documented first pass does not guarantee uncached solver work: decisionCache is global and may already contain these queries from earlier fixture tests or benchmark iterations, so SolverTime can measure only cache lookup latency and the reported benchmark metrics become incorrect.",
      "kind": "blocker"
    }
  ],
  "merge_risk": "high",
  "Model": "opus",
  "model": "codex",
  "effort": "high",
  "tokens": {
    "input_tokens": 0,
    "output_tokens": 0
  },
  "same_verdict_count": 3
}

[telleroutlook]

Summary

The benchmark tests can all pass without exercising Z3, allowing invalid solver queries or fixture behavior into CI.

Severity

high

Blocking findings

1. bench/symbolic/symbolic_test.go:64 The fixture tests silently skip when z3 is unavailable, so CI can report success without running the benchmark's core solver validation.
2. bench/symbolic/symbolic_test.go:112 The benchmark is also skipped when z3 is unavailable, leaving performance and cache behavior entirely unverified in such CI environments.
3. bench/symbolic/symbolic.go:107 Potential-path calculation uses int, so branch_points values of 31 or greater overflow on 32-bit platforms and can produce zero or invalid rates.

Verdict

❌ Rejected

Merge risk

high

Audit

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

{
  "approved": false,
  "severity": "high",
  "summary": "The benchmark tests can all pass without exercising Z3, allowing invalid solver queries or fixture behavior into CI.",
  "findings": [
    {
      "file": "bench/symbolic/symbolic_test.go",
      "line": 64,
      "issue": "The fixture tests silently skip when z3 is unavailable, so CI can report success without running the benchmark's core solver validation.",
      "kind": "blocker"
    },
    {
      "file": "bench/symbolic/symbolic_test.go",
      "line": 112,
      "issue": "The benchmark is also skipped when z3 is unavailable, leaving performance and cache behavior entirely unverified in such CI environments.",
      "kind": "blocker"
    },
    {
      "file": "bench/symbolic/symbolic.go",
      "line": 107,
      "issue": "Potential-path calculation uses int, so branch_points values of 31 or greater overflow on 32-bit platforms and can produce zero or invalid rates.",
      "kind": "suggestion"
    }
  ],
  "merge_risk": "high",
  "Model": "opus",
  "model": "codex",
  "effort": "high",
  "tokens": {
    "input_tokens": 0,
    "output_tokens": 0
  },
  "same_verdict_count": 4
}

[telleroutlook]

Summary

The PR appears merge-safe, with minor benchmark correctness and validation gaps.

Severity

low

Blocking findings

1. bench/symbolic/symbolic.go:155 The concrete WebAssembly return values are discarded, so the benchmark does not verify the fixture's expected execution result despite claiming to validate concrete execution.
2. bench/symbolic/symbolic.go:93 SolverTime is measured without clearing or isolating the global decision cache, so repeated benchmark runs can report cache lookup time instead of solver work.

Verdict

✅ Approved

Merge risk

low

Audit

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

{
  "approved": true,
  "severity": "low",
  "summary": "The PR appears merge-safe, with minor benchmark correctness and validation gaps.",
  "findings": [
    {
      "file": "bench/symbolic/symbolic.go",
      "line": 155,
      "issue": "The concrete WebAssembly return values are discarded, so the benchmark does not verify the fixture's expected execution result despite claiming to validate concrete execution.",
      "kind": "suggestion"
    },
    {
      "file": "bench/symbolic/symbolic.go",
      "line": 93,
      "issue": "SolverTime is measured without clearing or isolating the global decision cache, so repeated benchmark runs can report cache lookup time instead of solver work.",
      "kind": "suggestion"
    }
  ],
  "merge_risk": "low",
  "Model": "opus",
  "model": "codex",
  "effort": "high",
  "tokens": {
    "input_tokens": 0,
    "output_tokens": 0
  },
  "same_verdict_count": 1
}