You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Instance Variables Leak Between Sibling Methods #270
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.
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.
Likely cause
Instance variables with the same name leak between sibling methods.
changed the title [-]False Negative on Recursive Call with Sibling Method with Same Parameter Name[/-][+]Instance Variables Leak Between Sibling Methods[/+]on Jul 27, 2026
Activity
[-]False Negative on Recursive Call with Sibling Method with Same Parameter Name[/-][+]Instance Variables Leak Between Sibling Methods[/+]