Fix Usage Detection for Repeated Equalities

Author: rcosta358

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

@@ -27,7 +27,7 @@ public static Map<String, Expression> resolve(Expression exp) {
         resolveRecursive(exp, map);
 
         // remove variables that were not used in the expression
-        map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey(), entry.getValue()));
+        map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey(), entry.getValue(), true));
 
         // transitively resolve variables
         return resolveTransitive(map);
@@ -136,12 +136,14 @@ private static Expression lookup(Expression exp, Map<String, Expression> map, Se
      *
      * @param exp
      * @param name
+     * @param value
+     * @param canExcludeDefinition
      *
      * @return true if used, false otherwise
      */
-    private static boolean hasUsage(Expression exp, String name, Expression value) {
+    private static boolean hasUsage(Expression exp, String name, Expression value, boolean canExcludeDefinition) {
         // exclude own definitions
-        if (exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) {
+        if (canExcludeDefinition && exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) {
             Expression left = binary.getFirstOperand();
             Expression right = binary.getSecondOperand();
             if (left instanceof Var v && v.getName().equals(name) && right.equals(value)
@@ -167,8 +169,10 @@ && isConstant(left))
 
         // recurse children
         if (exp.hasChildren()) {
+            boolean childCanExcludeDefinition = exp instanceof BinaryExpression binary
+                    && "&&".equals(binary.getOperator());
             for (Expression child : exp.getChildren())
-                if (hasUsage(child, name, value))
+                if (hasUsage(child, name, value, childCanExcludeDefinition))
                     return true;
         }
 

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java

@@ -658,4 +658,12 @@ void testEnumConstantsPropagateIntoTernaryCondition() {
 
         assertEquals("start(param)", result.getValue().toString());
     }
+
+    @Test
+    void testRepeatedEqualDefinitionPropagatesIntoTernaryCondition() {
+        Expression expression = parse("mode == 2 && (mode == 2 ? explicit(param) : start(param))");
+        ValDerivationNode result = ExpressionSimplifier.simplify(expression);
+
+        assertEquals("explicit(param)", result.getValue().toString());
+    }
 }

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java

@@ -99,6 +99,15 @@ void testDifferentEqualityInIteConditionCountsAsUsage() {
         assertEquals("1", result.get("mode").toString());
     }
 
+    @Test
+    void testRepeatedEqualDefinitionCountsAsUsage() {
+        Expression expression = parse("mode == 2 && (mode == 2 ? explicit(param) : start(param))");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertEquals(1, result.size(), "Repeated equalities should keep one definition and treat the other as usage");
+        assertEquals("2", result.get("mode").toString());
+    }
+
     @Test
     void testReturnVariableIsNotSubstituted() {
         Expression expression = parse("x > 0 && #ret_1 == x");