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

@StateSet({"open", "closed"})
class Res {
    @StateRefinement(to = "open(this)")
    public Res() {}

    @StateRefinement(from = "open(this)")
    public void read() {}

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

public class Repro {
    void f(Res[] rs) {
        Res r = rs[0];
        r.close();
        r.read();
    }
}

Error: class com.microsoft.z3.Expr cannot be cast to class com.microsoft.z3.BoolExpr (com.microsoft.z3.Expr and com.microsoft.z3.BoolExpr are in unnamed module of loader 'app')
17 |     void f(Res[] rs) {
18 |         Res r = rs[0];
19 |         r.close();
   |         ^^^^^^^^^^
20 |         r.read();
21 |     }

State Refinement Error: found true but expected open(r⁹)

import liquidjava.specification.Refinement;

public class Repro {
    static void positive(@Refinement("_ > 0") int x) {}

    void f(int[] xs) {
        int c = xs[0];
        positive(c);
    }
}

Error: class com.microsoft.z3.IntExpr cannot be cast to class com.microsoft.z3.BoolExpr (com.microsoft.z3.IntExpr and com.microsoft.z3.BoolExpr are in unnamed module of loader 'app')
 6 |     void f(int[] xs) {
 7 |         int c = xs[0];
 8 |         positive(c);
   |         ^^^^^^^^^^^^