False Negative on Recursive Call with Sibling Method with Same Parameter Name

[rcosta358]

Description
In the following example, when both the fibonacci and factorial methods are present, LiquidJava fails to report an expected verification error on the recursive call inside factorial.

Removing the fibonacci method or renaming one of the n parameters causes the expected error to be reported correctly.

Minimal reproducer

int wrongFibonacci(@Refinement("_ > 0") int n) {
    if (n == 1) return 1;
    else return fibonacci(n - 1) + fibonacci(n - 2); // reports error ✅
}

int wrongFactorial(@Refinement("_ > 0") int n) {   
    return n * factorial(n - 1); // does not report error ❌
}

Expected behavior
Recursive call of factorial should report an error because when n == 1, on the next call n == 0, which violates the parameter refinement.

Actual behavior
Does not report the error.

Environment

• LiquidJava version / commit: 0.0.27
• Java version (java -version): 20
• OS: MacOS 26