Fix Origins

Author: rcosta358

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

@@ -36,8 +36,7 @@ private static VCImplication apply(VCImplication implication, List<Expression> n
         Expression expression = implication.getRefinement().getExpression();
         Expression simplified = simplify(expression, nonZeroExpressions);
         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/VCArithmeticSimplificationTest.java

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