Minor Changes

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java

@@ -3,6 +3,7 @@
 import java.util.Objects;
 
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.opt.VCSimplification;
 import liquidjava.utils.Utils;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -85,6 +86,10 @@ public String toString() {
             return String.format("%-20s %s", "", refinement.toString());
     }
 
+    public VCImplication simplify() {
+        return VCSimplification.simplifyToFixedPoint(this);
+    }
+
     public Predicate toConjunctions() {
         Predicate c = new Predicate();
         if (name == null && type == null && next == null)

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

@@ -8,7 +8,7 @@
 public class VCSimplification {
 
     /**
-     * Applies all available simplification steps to a VC chain
+     * Applies all available simplification steps to a VC chain until a fixed point is reached
      */
     public static VCImplication simplifyToFixedPoint(VCImplication implication) {
         if (implication == null)
@@ -18,8 +18,8 @@ public static VCImplication simplifyToFixedPoint(VCImplication implication) {
         VCImplication current = implication.clone();
         while (true) {
             VCImplication simplified = simplifyOnce(current);
-            if (current.equals(simplified)) // fixed point reached
-                return simplified;
+            if (current.equals(simplified))
+                return simplified; // fixed point reached
             current = simplified;
         }
     }