What Does Formal Structure in Counterexample Feedback Buy?

Counterexample-guided repair asks a synthesizer to fix a program given a description of how it failed. When that synthesizer is a large language model, the description can range from a raw execution trace to a formal certificate carrying a violated predicate, a signed robustness value, a minimized falsifying input and the program location responsible. None of that structure is free, and the intuition that more of it repairs better is usually settled by assumption. We test it: holding the falsifier, the program, the counterexample corpus, the token budget and the evaluation suite fixed, we vary only the rendering of the failure across five conditions and run 300 repair attempts against an interpretable behaviour-tree policy for an unprotected left turn in CARLA. Structure buys control over what repair is attempted. Structural edits account for $59/60$ attempts under a raw trace against $13/60$ under a natural-language summary, a difference of $76.7$ points with $95\%$ interval $[+61.7, +90.0]$. It did not buy a detectable improvement in whether repair succeeds: after excluding refusals, every paired interval contains zero. Pursuing that second question surfaced a third result. Contract satisfaction on a failing scenario is trivially achievable by refusing to act, $72\%$ of apparent repairs were exactly that, and exactly one attempt in three hundred repaired the failure, completed the manoeuvre and broke nothing --- a repair that generalises to all twenty counterexamples, including the nineteen it was never shown. The binding constraint is the search rather than the vocabulary, and a specification rewarding only safety makes the degenerate answer the easier one to find.