[CatarinaGamboa]

Stacked on #413.

Description

Building a state machine takes about 25 SMT checks for a small class, and each check creates its own Z3 context. The machine only depends on specifications, which are all registered in the first pass, so TypeChecker now builds it on the first state error and reuses it for every later error in the same checker. Finding the receiver's current states still runs at each error.

Other options considered:

• Eagerly, after the first pass, for every class with @StateSet: correct programs would pay the SMT cost too. Only worth it once something needs machines without an error, e.g. the fsm diagram.
• Once per run, cached in Context: Context would depend on state_machine, which depends on context (a package cycle). The other way is a static cache that tracks when specifications change. Neither seemed worth it for the extra hits across classes.

Cost

Extra time of TestExamples on the 269 cases that exist on main (summed per case, one run each; main takes 80.3 s):

• List the calls that reach an allowed state when the state is unknown #413, without the cache: +29.5 s
• with this PR: +10.6 s, spread over the 54 files with state errors

Type of change

• Code refactoring

Checklist

• mvn test passes locally

🤖 Generated with Claude Code