Soundness: if/else-if assignment followed by a guard hides a state violation #304

import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

@StateSet({"off", "on"})
class Encoder {
    @StateRefinement(to = "off(this)")
    public Encoder() {}

    @StateRefinement(to = "mode == 2 ? on(this) : off(this)")
    public void setMode(int mode) {}

    @StateRefinement(from = "on(this)")
    public void setQuality() {}
}

public class Repro {
    static void configure(boolean keep, boolean lossless) {
        Encoder e = new Encoder();
        int mode = 2;
        if (keep) {
            mode = 3;
        } else if (lossless) {
            mode = 0;
        }
        boolean fromSource = mode == 3;
        if (!fromSource) {
            e.setMode(mode);
            e.setQuality();         // expected error when lossless (mode == 0), but it verifies
        }
    }
}