Expression Oversimplification

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

@@ -20,7 +20,7 @@ public static ValDerivationNode simplify(Expression exp) {
 
     /**
      * Recursively applies propagation and folding until the expression stops changing (fixed point) Stops early if the
-     * expression simplifies to 'true', which means we've simplified too much
+     * expression simplifies to a boolean literal, which means we've simplified too much
      */
     private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, Expression prevExp) {
         // apply propagation and folding
@@ -34,6 +34,11 @@ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current,
             return current;
         }
 
+        // prevent oversimplification
+        if (current != null && currExp instanceof LiteralBoolean && !(current.getValue() instanceof LiteralBoolean)) {
+            return current;
+        }
+
         // continue simplifying
         return simplifyToFixedPoint(simplified, simplified.getValue());
     }

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

@@ -550,6 +550,36 @@ void testTransitive() {
         assertEquals("a == 1", result.getValue().toString(), "Expected result to be a == 1");
     }
 
+    @Test
+    void testShouldNotOversimplifyToTrue() {
+        // Given: x > 5 && x == y && y == 10
+        // Iteration 1: resolves y == 10, substitutes y -> 10: x > 5 && x == 10
+        // Iteration 2: resolves x == 10, substitutes x -> 10: 10 > 5 && 10 == 10 -> true
+        // Expected: x > 5 && x == 10 (should NOT simplify to true)
+
+        Expression varX = new Var("x");
+        Expression varY = new Var("y");
+        Expression five = new LiteralInt(5);
+        Expression ten = new LiteralInt(10);
+
+        Expression xGreater5 = new BinaryExpression(varX, ">", five);
+        Expression xEqualsY = new BinaryExpression(varX, "==", varY);
+        Expression yEquals10 = new BinaryExpression(varY, "==", ten);
+
+        Expression firstAnd = new BinaryExpression(xGreater5, "&&", xEqualsY);
+        Expression fullExpression = new BinaryExpression(firstAnd, "&&", yEquals10);
+
+        // When
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        // Then
+        assertNotNull(result, "Result should not be null");
+        assertFalse(result.getValue() instanceof LiteralBoolean,
+                "Should not oversimplify to a boolean literal, but got: " + result.getValue());
+        assertEquals("x > 5 && x == 10", result.getValue().toString(),
+                "Should stop simplification before collapsing to true");
+    }
+
     /**
      * Helper method to compare two derivation nodes recursively
      */