LiquidJava correctly reports a refinement error in the following method, since the return value x is not guaranteed to satisfy the return refinement _ > 0:

@Refinement("_ > 0")
int example(int x) {
    return x; // Refinement Error: #ret_62 == x is not a subtype of #ret_62 > 0
}

However, when a simple assignment x = x + 1 is added before the return, LiquidJava no longer reports an error:

@Refinement("_ > 0")
int example(int x) {
    x = x + 1;
    return x; // no error
}

However, the refinement _ > 0 is still not guaranteed. An error should still be reported because any negative number plus one does not satisfy the return refinement.