GeezerVison

Fixes #494

The verifier had no switch handling, so the cases ran one after another as straight-line code: break was ignored and the case label never entered the path condition. A switch is now checked like the if / else if chain over its labels:

• each case starts from the state before the switch and knows selector == label (grouped labels: any of them; default: none of the other labels)
• a case without break falls through into the next one
• the states of the cases that reach the end are joined after the switch, as after an if
• return / throw / continue in a case drop that path, as in an if
• switch expressions (->, yield) are checked the same way; selectors may be enums, ints or strings (a string label has no known value, so it adds no path condition)

Two forms are handled conservatively:

• pattern or guarded cases (case String s ->, when): checked as before (Verifier crashes on a type-pattern switch (case String s ->) #345 is unchanged)
• a break / yield nested inside a case (e.g. if (c) { ...; break; }): the state at that jump is not followed, so what those cases change is forgotten on that path after the switch (shown as true in Found)

Study exercise A1_09 (litiengine), the partial fix else if (newMode == BORDERLESS) host.dispose();

Before, the same error at the same line, though BORDERLESS is now disposed:

State Refinement Error: found previousMode == BORDERLESS && newMode != BORDERLESS ? notDisplayable(host) : (newMode == BORDERLESS ? notDisplayable(host) : displayable(host)) but expected notDisplayable(host)
49 |         host.setUndecorated(true);

After, the error moves to the remaining bug, the full-screen fallback:

State Refinement Error: found newMode == FULLSCREEN && (previousMode == BORDERLESS && newMode != BORDERLESS ? notDisplayable(host) : (newMode == BORDERLESS ? notDisplayable(host) : displayable(host))) but expected notDisplayable(host)
62 |           host.setUndecorated(true);

Study exercise A1_56 (JabRef), only redo() guarded

Before, the UNDO case saw what the REDO case did:

State Refinement Error: found (#canRedo_result ? redoable(undoManager@70) : notRedoable(undoManager@70)) && state2(undoManager@70) == state2(#getUndoManager_result) && limit(undoManager@70) == limit(#getUndoManager_result) && (#canRedo_result ? undoable(undoManager) && notRedoable(undoManager) && ... : ...) but expected undoable(undoManager)

After, only what holds on the UNDO path:

State Refinement Error: expected undoable(undoManager) but could not prove it
72 |                     case UNDO -> undoManager.undo();
Hints:
  - The state of undoManager is unknown here, and this call needs it to be undoable
  - Guard this call with if (undoManager.canUndo()): when it returns true, undoManager is undoable

The six study exercises still report their error at the same line. A1_09's Found now starts with the case's label: found newMode == BORDERLESS && (...). The other study variants report the same as before, apart from A1_09's first-only fix: same line (63), but its Found was displayable(host), the state the BORDERLESS case left, and is now the full-screen path's newMode == FULLSCREEN && (...), longer than before.

Tests: CorrectEnumUsage (state and label of each case, switch statement and expression), ErrorEnumUsage (an error that was missed in a case reached directly and by fall-through, and the nested break). TestStateHints now expects A1_56's UNDO hints above. Each fails on main.

🤖 Generated with Claude Code