{{include:instructions/contract-path-analysis}}

Map the paths that establish the changed invariant and their counterexamples to observable test obligations. In a test-only step, do not edit production code; retain existing contracts outside the requested change and do not expand into improvements for a different invariant or responsible source.