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);
                 });
     }