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

@ExternalRefinementsFor("java.lang.Throwable")
@StateSet({"withThrowable", "noThrowable"})
interface ThrowableRefinements {
    @StateRefinement(to = "noThrowable(this)")
    void Throwable(String message);

    @StateRefinement(to = "withThrowable(this)")
    void Throwable(String message, Throwable cause);

    @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
    Throwable initCause(Throwable cause);
}

public class Repro {
    static void load() throws Exception { throw new Exception("x"); }

    static void m() {
        Throwable t = new Throwable("start");
        try {
            load();
            t = new Throwable("try", new RuntimeException()); // withThrowable
        } catch (Exception e) {
            t = new Throwable("catch");                       // noThrowable
        }
        t.initCause(new RuntimeException()); // not reported, but t is withThrowable if load() returns
    }
}

static void m() {
    int y = 0;
    try {
        load();
        y = -5;
    } catch (Exception e) {
        y = 7;
    }
    @Refinement("_ > 0")
    int z = y; // not reported, but y == -5 if load() returns
}