False Positive With Early Return

[rcosta358]

The type checker fails to recognize that an early return can satisfy a refinement condition.

public class Example {

    public static int divide(int a, @Refinement("b != 0") int b) {
        return a / b;
    }

    public static void example1(int x, int y) {
        if (y == 0) {
            System.out.println("division by zero");
        } else {
            divide(x, y); // correct (no error)
        }
    }

    public static void example2(int x, int y) {
        if (y == 0) {
            System.out.println("division by zero");
            return; // early return
        }
        divide(x, y); // should also be correct but isnt
    }
}

In this example, the refinement b != 0 should be considered satisfied in both cases, since after the if (y == 0) branch returns, the only reachable path ensures y != 0.

Possible Fix

Convert early-exit branches into ternary (explicit if-else).