CEGAR-Harness: Regression-Aware Context Compaction and Witness Replay for Long-Horizon Coding Agents

Long-horizon coding agents rely on context compaction to remain within token budgets and avoid quadratic attention degradation. However, lossy compaction discards historical test failure traces, inducing Post-Compaction Regression Loops where an agent re-introduces previously refuted bugs. We present CEGAR-Harness, a Counterexample-Guided Abstraction Refinement middleware that couples context compaction with a versioned SQLite Counterexample Ledger and a 3-state Regression Gate (PASS, REGRESSION_DETECTED, INCONCLUSIVE) combining canonical AST pre-filtering and isolated Witness Replay. Evaluated across a 30-task controlled multi-turn benchmark (4-way ablation), a live Llama-3-8B GPU repair loop (achieving a 4x resolution gain: 66.7% vs. 16.7% with 0% unblocked regressions), and 6 multi-file Git repositories (100% atomic rollback in 29.4 ms), CEGAR-Harness eliminates post-compaction regressions while preserving 48.3% token compression.