From e311bd583b4f0a26885eae36b7cd9eb58452d8eb Mon Sep 17 00:00:00 2001
From: Rodrigo Martins <rodrigomartinsroger2006@gmail.com>
Date: Thu, 9 Jul 2026 20:21:46 +0100
Subject: [PATCH] changed variable name convention for
 TypeChecker:checkVariableRefinements, instead of using global counter, now
 we're using variable lines. If there's more than one variable with the same
 name on the same line we use a counter to identify each variable, to use the
 same variable name for different methods and for better tracking on files we
 also include the method name

---
 .../liquidjava/processor/context/Context.java | 31 +++++++++++++++++++
 .../refinement_checker/TypeChecker.java       |  3 +-
 2 files changed, 32 insertions(+), 2 deletions(-)

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..40c250111 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
@@ -2,7 +2,9 @@
 
 import java.util.*;
 import liquidjava.rj_language.Predicate;
+import liquidjava.utils.constants.Formats;
 import spoon.reflect.declaration.CtElement;
+import spoon.reflect.declaration.CtMethod;
 import spoon.reflect.reference.CtTypeReference;
 
 public class Context {
@@ -18,6 +20,8 @@ public class Context {
     private int counter;
     private static Context instance;
 
+    private Map<Integer, Map<String, Integer>> lineVariables;
+
     private Context() {
         ctxVars = new Stack<>();
         ctxVars.add(new ArrayList<>());
@@ -29,6 +33,7 @@ private Context() {
         ghosts = new ArrayList<>();
         classStates = new HashMap<>();
         counter = 0;
+        lineVariables = new HashMap<>();
     }
 
     public static Context getInstance() {
@@ -50,6 +55,7 @@ public void reinitializeAllContext() {
         ghosts = new ArrayList<>();
         classStates = new HashMap<>();
         counter = 0;
+        lineVariables = new HashMap<>();
     }
 
     public void enterContext() {
@@ -363,6 +369,31 @@ public List<AliasWrapper> getAliases() {
         return aliases;
     }
 
+    // ---------------------- Variable Name ----------------------
+    public String getVariableName(String varName, CtElement element) {
+        boolean isValidPosition = element.getPosition().isValidPosition();
+        int line = isValidPosition ? element.getPosition().getLine() : getCounter();
+        CtMethod<?> method = element.getParent(CtMethod.class);
+
+        if (!isValidPosition) {
+            return String.format(Formats.INSTANCE, method != null ? method.getSimpleName() + "_" + varName : varName,
+                    line);
+        }
+
+        Map<String, Integer> variables = lineVariables.getOrDefault(line, new HashMap<>());
+
+        String key = method != null ? method.getSimpleName() + varName + line : varName + line;
+
+        int count = variables.getOrDefault(varName, 0);
+        variables.put(key, count + 1);
+
+        return count == 0
+                ? String.format(Formats.INSTANCE, method != null ? method.getSimpleName() + "_" + varName : varName,
+                        line)
+                : String.format(Formats.INSTANCE + "_%d",
+                        method != null ? method.getSimpleName() + "_" + varName : varName, line, count);
+    }
+
     @Override
     public String toString() {
         StringBuilder sb = new StringBuilder();
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
index 4935b4579..ddd38961d 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
@@ -21,7 +21,6 @@
 import liquidjava.smt.SMTEvaluator;
 import liquidjava.smt.SMTResult;
 import liquidjava.utils.Utils;
-import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Types;
 import spoon.reflect.code.CtExpression;
@@ -351,7 +350,7 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
         cEt = cEt.substituteVariable(Keys.WILDCARD, simpleName);
         Predicate cet = cEt.substituteVariable(Keys.WILDCARD, simpleName);
 
-        String newName = String.format(Formats.INSTANCE, simpleName, context.getCounter());
+        String newName = context.getVariableName(simpleName, usage);
         Predicate correctNewRefinement = refinementFound.substituteVariable(Keys.WILDCARD, newName);
         correctNewRefinement = correctNewRefinement.substituteVariable(Keys.THIS, newName);
         cEt = cEt.substituteVariable(simpleName, newName);