diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java
index 39a155d3..228a318a 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java
@@ -252,20 +252,6 @@ private VCImplication joinPredicates(Predicate expectedType, List<RefinedVariabl
 
         VCImplication firstSi = null;
         VCImplication lastSi = null;
-        // Check
-        for (RefinedVariable var : mainVars) { // join main refinements of mainVars
-            addMap(var, map);
-            VCImplication si = new VCImplication(var.getName(), var.getType(), var.getMainRefinement());
-            if (lastSi != null) {
-                lastSi.setNext(si);
-                lastSi = si;
-            }
-            if (firstSi == null) {
-                firstSi = si;
-                lastSi = si;
-            }
-        }
-
         for (RefinedVariable var : vars) { // join refinements of vars
             addMap(var, map);
 
@@ -289,6 +275,19 @@ && hasDependencyCycle(lastInst.get(), var.getName(), vars, new HashSet<>()))
                 lastSi = si;
             }
         }
+
+        for (RefinedVariable var : mainVars) { // join main refinements of mainVars
+            addMap(var, map);
+            VCImplication si = new VCImplication(var.getName(), var.getType(), var.getMainRefinement());
+            if (lastSi != null) {
+                lastSi.setNext(si);
+                lastSi = si;
+            }
+            if (firstSi == null) {
+                firstSi = si;
+                lastSi = si;
+            }
+        }
         VCImplication cSMT = new VCImplication(new Predicate());
         if (firstSi != null) {
             cSMT = firstSi.clone();
@@ -331,6 +330,8 @@ private void getVariablesFromContext(List<String> lvars, List<RefinedVariable> a
                 .filter(rv -> !allVars.contains(rv)).forEach(rv -> {
                     allVars.add(rv);
                     recAuxGetVars(rv, allVars);
+                    allVars.remove(rv);
+                    allVars.add(rv);
                 });
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java
new file mode 100644
index 00000000..de2f34b8
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java
@@ -0,0 +1,109 @@
+package liquidjava.rj_language;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Objects;
+
+import spoon.reflect.reference.CtTypeReference;
+
+public class SimplifiedPredicate extends Predicate {
+
+    private final Predicate simplified;
+    private final Predicate origin;
+    private final List<Binder> binders;
+
+    public SimplifiedPredicate(Predicate simplified, Predicate origin) {
+        this(simplified, origin, List.of());
+    }
+
+    public SimplifiedPredicate(Predicate simplified, Predicate origin, List<Binder> binders) {
+        super(simplified.getExpression());
+        this.simplified = simplified;
+        this.origin = origin;
+        this.binders = new ArrayList<>(binders);
+    }
+
+    public Predicate getSimplifiedPredicate() {
+        return simplified;
+    }
+
+    public Predicate getOrigin() {
+        return origin;
+    }
+
+    public List<Binder> getBinders() {
+        return binders;
+    }
+
+    @Override
+    public boolean isBooleanTrue() {
+        return getSimplifiedPredicate().isBooleanTrue();
+    }
+
+    @Override
+    public SimplifiedPredicate clone() {
+        return new SimplifiedPredicate(getSimplifiedPredicate().clone(), origin.clone(), binders);
+    }
+
+    @Override
+    public String toString() {
+        return getSimplifiedPredicate().toString();
+    }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(getSimplifiedPredicate(), origin, binders);
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        if (obj == null)
+            return false;
+        if (getClass() != obj.getClass())
+            return false;
+        SimplifiedPredicate other = (SimplifiedPredicate) obj;
+        return getSimplifiedPredicate().equals(other.getSimplifiedPredicate()) && origin.equals(other.origin)
+                && binders.equals(other.binders);
+    }
+
+    public static class Binder {
+        private final String name;
+        private final String type;
+
+        public Binder(String name, String type) {
+            this.name = name;
+            this.type = type;
+        }
+
+        public Binder(String name, CtTypeReference<?> type) {
+            this(name, type.getQualifiedName());
+        }
+
+        public String getName() {
+            return name;
+        }
+
+        public String getType() {
+            return type;
+        }
+
+        @Override
+        public int hashCode() {
+            return Objects.hash(name, type);
+        }
+
+        @Override
+        public boolean equals(Object obj) {
+            if (this == obj)
+                return true;
+            if (obj == null)
+                return false;
+            if (getClass() != obj.getClass())
+                return false;
+            Binder other = (Binder) obj;
+            return name.equals(other.name) && type.equals(other.type);
+        }
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java
index cf6e4fdc..2135f41d 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java
@@ -61,8 +61,10 @@ private String formatArguments(List<Expression> args) {
     }
 
     private Expression unwrapGroup(Expression expression) {
-        while (expression instanceof GroupExpression group)
-            expression = group.getExpression();
+        while (expression instanceof GroupExpression) {
+            if (expression instanceof GroupExpression group)
+                expression = group.getExpression();
+        }
         return expression;
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java
index 0fa965cd..59cd6a0f 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java
@@ -57,7 +57,6 @@ else if (e instanceof FunctionInvocation)
             return functionType(ctx, (FunctionInvocation) e);
         else if (e instanceof AliasInvocation)
             return boolType(factory);
-
         return Optional.empty();
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java
index 904690a7..24d030fc 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java
@@ -44,4 +44,4 @@ public interface ExpressionVisitor<T> {
     T visitEnum(Enum en) throws LJError;
 
     T visitVar(Var var) throws LJError;
-}
\ No newline at end of file
+}