Substitute Internal Variables by Counter

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java

@@ -70,4 +70,15 @@ public boolean equals(Object obj) {
             return name.equals(other.name);
         }
     }
+
+    public boolean isInternal() {
+        return name.startsWith("#");
+    }
+
+    public int getCounter() {
+        if (!isInternal())
+            throw new IllegalStateException("Cannot get counter of non-internal variable");
+        int lastUnderscore = name.lastIndexOf('_');
+        return Integer.parseInt(name.substring(lastUnderscore + 1));
+    }
 }

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

@@ -58,6 +58,12 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
                     map.put(leftVar.getName(), right.clone());
                 } else if (rightVar.isInternal() && !leftVar.isInternal()) {
                     map.put(rightVar.getName(), left.clone());
+                } else if (leftVar.isInternal() && rightVar.isInternal()) {
+                    // substitute the lower-counter variable with the higher-counter one
+                    boolean isLeftCounterLower = leftVar.getCounter() <= rightVar.getCounter();
+                    Var lowerVar = isLeftCounterLower ? leftVar : rightVar;
+                    Var higherVar = isLeftCounterLower ? rightVar : leftVar;
+                    map.putIfAbsent(lowerVar.getName(), higherVar.clone());
                 }
             }
         }