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

@ExternalRefinementsFor("java.lang.Throwable")
@StateSet({"withThrowable", "noThrowable"})
public 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 record Repro(int attempts) {
    void fail(String summary) {
        Throwable exception = new Throwable(summary, new RuntimeException("first"));
        exception.initCause(new RuntimeException("second"));   // JVM: Can't overwrite cause
    }
}

Warning: Java compilation encountered issues. Verification may be affected.
Correct! Passed Verification.

public class Control {
    void fail(String summary) {
        Throwable exception = new Throwable(summary, new RuntimeException("first"));
        exception.initCause(new RuntimeException("second"));   // the same method in a class: reported
    }
}

State Refinement Error: found withThrowable(exception⁹) but expected noThrowable(exception⁹)
2 |     void fail(String summary) {
3 |         Throwable exception = new Throwable(summary, new RuntimeException("first"));
4 |         exception.initCause(new RuntimeException("second"));   // the same method in a class: reported
  |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
5 |     }