From e081e5e686ad15badb5f0f3653f54f56fd9f0484 Mon Sep 17 00:00:00 2001
From: Ricardo Costa <rcosta.ms358@gmail.com>
Date: Mon, 27 Jul 2026 15:05:43 +0100
Subject: [PATCH] Fix Instance Variable Leak Between Methods

---
 .../ErrorRecursiveSiblingParameter.java         | 17 +++++++++++++++++
 .../liquidjava/processor/context/Context.java   |  4 ++++
 .../RefinementTypeChecker.java                  |  2 ++
 3 files changed, 23 insertions(+)
 create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorRecursiveSiblingParameter.java

diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursiveSiblingParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursiveSiblingParameter.java
new file mode 100644
index 000000000..8e48a2fb4
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorRecursiveSiblingParameter.java
@@ -0,0 +1,17 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorRecursiveSiblingParameter {
+
+    int fibonacci(@Refinement("_ > 0") int n) {
+        if (n == 1)
+            return 1;
+        else
+            return fibonacci(n - 1) + fibonacci(n - 2); // Refinement Error
+    }
+
+    int factorial(@Refinement("_ > 0") int n) {
+        return n * factorial(n - 1); // Refinement Error
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
index 864d65924..ddb55cf37 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
@@ -40,6 +40,10 @@ public static Context getInstance() {
     public void reinitializeContext() {
         ctxVars = new Stack<>();
         ctxVars.add(new ArrayList<>()); // global vars
+        clearInstanceVariables();
+    }
+
+    public void clearInstanceVariables() {
         ctxInstanceVars = new ArrayList<>();
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
index 33b5198c8..ed88d6f74 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
@@ -105,6 +105,7 @@ public <A extends Annotation> void visitCtAnnotationType(CtAnnotationType<A> ann
 
     @Override
     public <T> void visitCtConstructor(CtConstructor<T> constructor) {
+        context.clearInstanceVariables();
         context.enterContext();
         mfc.loadFunctionInfo(constructor);
         try {
@@ -117,6 +118,7 @@ public <T> void visitCtConstructor(CtConstructor<T> constructor) {
     }
 
     public <R> void visitCtMethod(CtMethod<R> method) {
+        context.clearInstanceVariables();
         context.enterContext();
         if (!method.getSignature().equals("main(java.lang.String[])")) {
             mfc.loadFunctionInfo(method);