[CatarinaGamboa]

Fixes #440.

Problem. AuxStateHandler.createStatePredicate checks the to of a non-void method by renaming return to _ and declaring _ with the method's return type. That declaration (and the this variables) went into the current context, outside any scope, and only when _ didn't exist yet. So the first non-void method with a to fixed the type of return for every spec checked after it. A later to = "!return && ..." on a boolean method then crashed with Expr cannot be cast to BoolExpr (or IntExpr ... when the earlier method returned int). Which specs crash depends on the order the packages are checked in.

Change. Declare these variables in their own scope (enterContext / exitContext in a finally), and always declare _ with this method's return type. An inner declaration shadows an outer one in the SMT translation.

Test. testSuite/classes/state_return_type_scope_correct: a Vector spec whose set returns E, checked before an UndoManager spec with !return in canUndo. It fails on main with the crash and passes with this change. mvn test passes.

Also checked on a six-exercise study project (Vector, UndoManager, ImageWriteParam, JFrame, Random, Socket specs in one source folder): before the change, the UndoManager exercise's real error turned into this crash. After it, all six report their intended error lines.

🤖 Generated with Claude Code

[CatarinaGamboa]

[Codex review] I checked the scope change in createStatePredicate, including the finally exit on errors and the regression with two different return types. It keeps the temporary this and _ declarations local to each check, and the verifier suite passes locally at this head (./mvnw -q -pl liquidjava-verifier -am test). I found no further issue with this PR.

[CatarinaGamboa]

[Claude] Thanks for checking. No changes needed.