Fix VC Substitution (#259)

Author: rcosta358

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

@@ -75,7 +75,8 @@ private Optional<Substitution> findSubstitution(VCImplication implication) {
         if (implication == null)
             return Optional.empty();
 
-        Optional<Substitution> current = getSubstitution(implication);
+        Optional<Substitution> current = containsVar(implication.getNext(), implication.getName())
+                ? getSubstitution(implication) : Optional.empty();
         if (current.isPresent())
             return current;
 
@@ -120,4 +121,15 @@ private boolean containsVar(Expression expression, String name) {
         expression.getVariableNames(names);
         return names.contains(name);
     }
+
+    /**
+     * Checks whether a VC suffix contains a variable name
+     */
+    private boolean containsVar(VCImplication implication, String name) {
+        for (VCImplication current = implication; current != null; current = current.getNext()) {
+            if (containsVar(current.getRefinement().getExpression(), name))
+                return true;
+        }
+        return false;
+    }
 }

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

@@ -53,10 +53,17 @@ void preservesRemainingBinderAfterSubstitution() {
     }
 
     @Test
-    void removesSourceNodeWhenItIsLastInChain() {
+    void keepsSourceNodeWhenItIsLastInChain() {
         VCImplication implication = vc("x > 0", "∀y:int. y == 1");
 
-        assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 0")));
+        assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 0"), expect("y == 1")));
+    }
+
+    @Test
+    void keepsReturnBinderWhenConclusionIsSeparate() {
+        VCImplication implication = vc("∀x:int. true", "∀#ret_8:int. #ret_8 == x + 1");
+
+        assertSimplificationSteps(substitution::apply, implication, chain(expect("true"), expect("#ret⁸ == x + 1")));
     }
 
     @Test