René's URL Explorer Experiment

{"@context":"https://schema.org","@type":"DiscussionForumPosting","headline":"False Negative on Recursive Call with Sibling Method with Same Parameter Name","articleBody":"**Description**\nIn 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`.\n\nRemoving the `fibonacci` method or renaming one of the `n` parameters causes the expected error to be reported correctly.\n\n**Minimal reproducer**\n```java\nint wrongFibonacci(@Refinement(\"_ \u003e 0\") int n) {\n    if (n == 1) return 1;\n    else return fibonacci(n - 1) + fibonacci(n - 2); // reports error ✅\n}\n\nint wrongFactorial(@Refinement(\"_ \u003e 0\") int n) {   \n    return n * factorial(n - 1); // does not report error ❌\n}\n```\n\n**Expected behavior**\nRecursive call of `factorial` should report an error because when `n == 1`, on the next call `n == 0`, which violates the parameter refinement.\n\n**Actual behavior**\nDoes not report the error.\n\n**Environment**\n- LiquidJava version / commit: 0.0.27\n- Java version (`java -version`): 20\n- OS: MacOS 26","author":{"url":"https://github.com/rcosta358","@type":"Person","name":"rcosta358"},"datePublished":"2026-06-26T16:10:14.000Z","interactionStatistic":{"@type":"InteractionCounter","interactionType":"https://schema.org/CommentAction","userInteractionCount":0},"url":"https://github.com/270/liquidjava/issues/270"}