Fix Origins

Author: rcosta358

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

@@ -25,8 +25,7 @@ public static VCImplication apply(VCImplication implication) {
         Expression expression = implication.getRefinement().getExpression();
         Expression simplified = simplify(expression);
         if (!expression.equals(simplified)) {
-            VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified),
-                    implication.getOrigin());
+            VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), implication);
             result.setNext(implication.getNext() == null ? null : implication.getNext().clone());
             return result;
         }

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

@@ -87,13 +87,13 @@ void recordsOriginWhenSimplifyingLaterImplication() {
                 chain(expect("x > 0", "x > 0"), expect("y", "y || false")));
 
         SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
-        assertEquals("y || false", simplifiedNext.getOrigin().getRefinement().toString());
+        assertEquals("y || false", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString());
     }
 
     @Test
-    void preservesOriginFromExistingSimplifiedImplication() {
+    void recordsCurrentImplicationAsOriginWhenSimplifyingExistingSimplifiedImplication() {
         VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == y", "x == x"));
 
-        assertSimplificationSteps(VCLogicalSimplification::apply, substituted, chain(expect("true", "∀x:int. x == x")));
+        assertSimplificationSteps(VCLogicalSimplification::apply, substituted, chain(expect("true", "y == y")));
     }
 }

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

@@ -64,7 +64,7 @@ void simplifyOnceAppliesArithmeticBeforeLogicalSimplification() {
         VCImplication implication = vc("x + 0 == x");
 
         assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x == x", "x + 0 == x")),
-                chain(expect("true", "x + 0 == x")));
+                chain(expect("true", "x == x")));
     }
 
     @Test
@@ -79,7 +79,7 @@ void simplifyAppliesLogicalStepsUntilFixedPoint() {
         VCImplication implication = vc("x && true && true");
 
         assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
-                chain(expect("x && true", "x && true && true")), chain(expect("x", "x && true && true")));
+                chain(expect("x && true", "x && true && true")), chain(expect("x", "x && true")));
     }
 
     @Test