Fix Origins

Author: rcosta358

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

@@ -32,7 +32,14 @@ private VCImplication apply(VCImplication implication, C context) {
         Expression expression = implication.getRefinement().getExpression();
         Expression simplified = simplify(expression, context);
         if (!expression.equals(simplified)) {
-            VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), implication);
+            VCImplication origin = implication.copyWithRefinement(implication.getRefinement().clone());
+            VCImplication previousOrigin = implication.getOrigin();
+            if (previousOrigin != null) {
+                VCImplication displayed = new VCImplication(implication, implication.getRefinement().clone());
+                if (displayed.toString().equals(previousOrigin.toString()))
+                    origin = previousOrigin;
+            }
+            VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), origin);
             result.setNext(implication.getNext() == null ? null : implication.getNext().clone());
             return result;
         }

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

@@ -64,7 +64,9 @@ private VCImplication substituteNode(VCImplication implication, VCImplication no
             return implication.copyWithRefinement(new Predicate(exp));
 
         Expression substituted = exp.substitute(new Var(node.getName()), replacement.clone());
-        VCImplication origin = new VCImplication(node.getName(), node.getType(), implication.getOriginRefinement());
+        VCImplication origin = new VCImplication(node, implication.getRefinement().clone());
+        if (implication.getOrigin() != null)
+            origin = new SimplifiedVCImplication(origin, origin.getRefinement(), implication.getOrigin());
         return new SimplifiedVCImplication(implication, new Predicate(substituted), origin);
     }
 

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

@@ -129,7 +129,7 @@ void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() {
 
         assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
                 chain(expect("y == 3 + 1", "∀x:int. y == x + 1"), expect("y > 3", "∀x:int. y > x")),
-                chain(expect("3 + 1 > 3", "∀y:int. y > x")), chain(expect("4 > 3", "3 + 1 > 3")),
+                chain(expect("3 + 1 > 3", "∀y:int. y > 3")), chain(expect("4 > 3", "3 + 1 > 3")),
                 chain(expect("true", "4 > 3")));
     }
 

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

@@ -1,6 +1,7 @@
 package liquidjava.rj_language.opt;
 
 import static liquidjava.utils.VCTestUtils.*;
+import static org.junit.jupiter.api.Assertions.assertEquals;
 
 import liquidjava.processor.VCImplication;
 import org.junit.jupiter.api.Test;
@@ -86,9 +87,13 @@ void substitutesInnerKnownValueAcrossNestedImplications() {
     void substitutesOuterKnownValueIntoNestedBinderRefinements() {
         VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x");
 
-        assertSimplificationSteps(substitution::apply, implication,
+        VCImplication result = assertSimplificationSteps(substitution::apply, implication,
                 chain(expect("y == 3 + 1", "∀x:int. y == x + 1"), expect("y > 3", "∀x:int. y > x")),
-                chain(expect("3 + 1 > 3", "∀y:int. y > x")));
+                chain(expect("3 + 1 > 3", "∀y:int. y > 3")));
+
+        VCImplication previousOrigin = result.getOrigin().getOrigin();
+        assertEquals("x", previousOrigin.getName());
+        assertEquals("y > x", previousOrigin.getRefinement().getExpression().toDisplayString());
     }
 
     @Test