Only Flatten Same Instance Variables

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java

@@ -9,6 +9,7 @@
 import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import liquidjava.rj_language.opt.derivation_node.VarDerivationNode;
+import liquidjava.utils.Utils;
 
 import java.util.HashMap;
 import java.util.Map;
@@ -139,11 +140,10 @@ private static void extractVarOrigins(ValDerivationNode node, Map<String, Deriva
     }
 
     /**
-     * Flattens variable derivations to avoid redundancy by collapsing var -> var chains If the origin is a
-     * VarDerivationNode, we use its variable name and origin instead
+     * Flattens same instance variable derivations to avoid redundancy by collapsing var -> var chains
      */
     private static VarDerivationNode flattenVarOrigin(String varName, DerivationNode origin) {
-        if (origin instanceof VarDerivationNode varOrigin) {
+        if (origin instanceof VarDerivationNode varOrigin && Utils.isSameVariable(varOrigin.getVar(), varName)) {
             return flattenVarOrigin(varOrigin.getVar(), varOrigin.getOrigin()); // recursively flatten
         }
         return origin != null ? new VarDerivationNode(varName, origin) : new VarDerivationNode(varName);

liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

@@ -42,4 +42,10 @@ public static SourcePosition getRefinementAnnotationPosition(CtElement element,
             return unquoted.equals(refinement);
         }).findFirst().map(CtElement::getPosition).orElse(element.getPosition());
     }
+
+    public static boolean isSameVariable(String var1, String var2) {
+        String name1 = var1.substring(0, var1.lastIndexOf('_'));
+        String name2 = var2.substring(0, var2.lastIndexOf('_'));
+        return name1.equals(name2);
+    }
 }