9.4. A debugging order🔗

When something fails, working outward in this order avoids most wasted effort:

1. laurelParse — is it a syntax problem?

2. laurelToCore — is it a resolution or lowering problem?

3. laurelAnalyze --keep-all-files out — did a pass transform the construct in a way you did not expect?

4. Read the final Core program before looking at any SMT.

5. Only then, --vc-directory vcs --no-solve to inspect the query.

For a failing obligation specifically, the usual moves are to weaken the goal until it passes — which tells you which conjunct is at fault — and to add asserts at intermediate points, since a proof that fails at the end often fails because a fact you assumed was available never was. When an obligation times out rather than fails, suspect a quantifier: check whether a forall needs a trigger, or whether one it has is firing far too often.