@StateSet({"closed", "open"})
class Door {
    @StateRefinement(to = "closed(this)") Door() {}
    @StateRefinement(from = "closed(this)", to = "open(this)") void open() {}
    @StateRefinement(from = "open(this)", to = "closed(this)") void close() {}
}

class NestedBreak {
    // Every path opens the door before leaving the switch, so close() is fine
    static void enter(int k, boolean fast) {
        Door d = new Door();
        switch (k) {
            case 1:
                if (fast) {
                    d.open();
                    break;
                }
                d.open();
                break;
            default:
                d.open();
        }
        d.close();
    }
}

State Refinement Error: found k == 1 ? true : open(d) but expected open(d)
31 |         d.close();
Hints:
  - d can be in closed or open here, depending on the path taken, and no sequence of calls moves all of them to open. Make d reach this line in the same state on every path