@@ -3,7 +3,6 @@
 import java.util.ArrayList;
 import java.util.Comparator;
 import java.util.HashSet;
-import java.util.Iterator;
 import java.util.List;
 import java.util.Set;
 import java.util.stream.Collectors;
@@ -15,9 +14,6 @@
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Enum;
 import liquidjava.rj_language.ast.Expression;
-import liquidjava.rj_language.ast.FunctionInvocation;
-import liquidjava.rj_language.ast.LiteralBoolean;
-import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.rj_language.opt.VCSimplificationResult;
@@ -27,7 +23,12 @@
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 
+import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedTerms;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.termName;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.termsOf;
 
 /**
  * Error indicating that a refinement constraint either was violated or cannot be proven
@@ -72,21 +73,6 @@ private static String message(Predicate expected, VCSimplificationResult found)
                 expected.getExpression().toDisplayString());
     }
 
-    /**
-     * The facts of found linked to the terms of expected, as a conjunction, or true when there are none; found as
-     * written when every fact is linked
-     */
-    static Expression linkedToExpected(Expression found, Expression expected) {
-        List<Expression> facts = factsOf(found);
-        Set<String> linked = linkedTerms(facts, termsOf(expected));
-        List<Expression> linkedFacts = facts.stream().filter(fact -> termsOf(fact).stream().anyMatch(linked::contains))
-                .toList();
-        if (linkedFacts.size() == facts.size())
-            return found;
-        return linkedFacts.stream().reduce((first, second) -> new BinaryExpression(first, "&&", second))
-                .orElse(new LiteralBoolean(true));
-    }
-
     /** Unknown when what was found says nothing about the values the expected refinement constrains */
     private static ErrorCategory categoryOf(Predicate expected, VCSimplificationResult found) {
         List<String> foundVariables = found.getImplication().toPredicate().getVariableNames();
@@ -138,47 +124,6 @@ private Counterexample filterCounterexample(Counterexample counterexample) {
                 .toList());
     }
 
-    // Conjuncts of found, also splitting negated disjunctions (!(a || b) is !a && !b) and dropping double negations, so
-    // each fact links only the terms it relates
-    private static List<Expression> factsOf(Expression expression) {
-        List<Expression> facts = new ArrayList<>();
-        if (expression instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) {
-            facts.addAll(factsOf(binary.getFirstOperand()));
-            facts.addAll(factsOf(binary.getSecondOperand()));
-        } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp())
-                && not.getExpression()instanceof BinaryExpression binary && "||".equals(binary.getOperator())) {
-            facts.addAll(factsOf(new UnaryExpression("!", binary.getFirstOperand())));
-            facts.addAll(factsOf(new UnaryExpression("!", binary.getSecondOperand())));
-        } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp())
-                && not.getExpression()instanceof UnaryExpression inner && "!".equals(inner.getOp())) {
-            facts.addAll(factsOf(inner.getExpression()));
-        } else {
-            facts.add(expression);
-        }
-        return facts;
-    }
-
-    // Terms of expected plus those of every fact sharing a term with them, directly or through other facts. The
-    // remaining facts constrain other values only, so any values satisfying them make the same counterexample
-    private static Set<String> linkedTerms(List<Expression> facts, List<String> expectedTerms) {
-        Set<String> linked = new HashSet<>(expectedTerms);
-        List<List<String>> unlinked = facts.stream().map(RefinementError::termsOf)
-                .collect(Collectors.toCollection(ArrayList::new));
-        boolean changed = true;
-        while (changed) {
-            changed = false;
-            for (Iterator<List<String>> it = unlinked.iterator(); it.hasNext();) {
-                List<String> terms = it.next();
-                if (terms.stream().anyMatch(linked::contains)) {
-                    linked.addAll(terms);
-                    it.remove();
-                    changed = true;
-                }
-            }
-        }
-        return linked;
-    }
-
     // Whether a fact of found is term == value, which the counterexample would only repeat
     private static boolean isKnown(Pair<String, String> assignment, List<Expression> facts) {
         return facts.stream()
@@ -209,32 +154,4 @@ private static int relevance(String term, List<String> expectedTerms, List<Strin
             return foundTerms.contains(term) ? 1 : 0;
         return GeneratedNames.isGenerated(term) ? 3 : 2;
     }
-
-    // Variables and ghost applications of an expression, named as in the SMT model
-    private static List<String> termsOf(Expression expression) {
-        List<String> terms = new ArrayList<>();
-        expression.getVariableNames(terms);
-        addGhostApplications(expression, terms);
-        return terms;
-    }
-
-    private static void addGhostApplications(Expression expression, List<String> terms) {
-        String term = expression instanceof FunctionInvocation ? termName(expression) : null;
-        if (term != null && !terms.contains(term))
-            terms.add(term);
-        for (Expression child : expression.getChildren())
-            addGhostApplications(child, terms);
-    }
-
-    // Name of a variable, or of a ghost application over variables, as in the SMT model; null for other expressions
-    private static String termName(Expression expression) {
-        if (expression instanceof Var var)
-            return var.getName();
-        if (expression instanceof FunctionInvocation invocation
-                && invocation.getArgs().stream().allMatch(Var.class::isInstance)) {
-            String args = invocation.getArgs().stream().map(Expression::toString).collect(Collectors.joining(", "));
-            return Utils.getSimpleName(invocation.getName()) + "(" + args + ")";
-        }
-        return null;
-    }
 }
@@ -1,6 +1,7 @@
 package liquidjava.diagnostics.errors;
 
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected;
 
 import java.util.List;
 
@@ -44,7 +45,7 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP
     // Only the facts of found about the objects of expected, and only when one of them tells a state: an alias or a
     // guard on another value says nothing about the state expected needs
     private static String message(Predicate expected, VCSimplificationResult found) {
-        Expression shown = RefinementError.linkedToExpected(found.getImplication().toPredicate().getExpression(),
+        Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(),
                 expected.getExpression());
         if (!appliesGhost(shown))
             return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString());
 
@@ -1,10 +1,13 @@
 package liquidjava.rj_language.opt;
 
 import static liquidjava.rj_language.opt.VCSimplificationUtils.containsVar;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedTerms;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.termsOf;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.valueVariablesOf;
 
 import java.util.HashSet;
+import java.util.List;
 import java.util.Set;
 
 import liquidjava.processor.VCImplication;
@@ -15,7 +18,8 @@
  * Decides which binders refined only by {@code true} a simplified VC chain keeps for an error. Such a binder states no
  * fact, and a variable that another row mentions is already shown there, so its row would only read as if its value
  * were true. It is kept only when the error shows a counterexample, expected constrains the variable's value and no
- * other row mentions it: the row then shows that nothing is known about a value the error depends on
+ * other row mentions it: the row then shows that nothing is known about a value the error depends on. It also tells
+ * which binders expected does not depend on, such as path conditions over other values
  *
  * @param expectedTerms
  *            variables and ghost applications of the expected refinement
@@ -68,6 +72,35 @@ public Set<String> trueBindersToKeep(VCImplication chain) {
         return keep;
     }
 
+    /**
+     * Binders that share no term with expected, neither their variable nor a term of their refinement, directly or
+     * through other facts of the chain, and whose variable no other row mentions: expected does not depend on them.
+     * None without expected terms
+     */
+    public Set<String> unlinkedBinders(VCImplication chain) {
+        Set<String> unlinked = new HashSet<>();
+        if (expectedTerms.isEmpty())
+            return unlinked;
+        List<Expression> facts = factsOf(chain.toPredicate().getExpression());
+        Set<String> linked = linkedTerms(facts, expectedTerms);
+        for (VCImplication row = chain; row != null; row = row.getNext())
+            if (row.hasBinder() && !isLinked(row, linked) && !mentionedByOtherRows(chain, row))
+                unlinked.add(row.getName());
+        return unlinked;
+    }
+
+    private static boolean isLinked(VCImplication row, Set<String> linked) {
+        return linked.contains(row.getName())
+                || termsOf(row.getRefinement().getExpression()).stream().anyMatch(linked::contains);
+    }
+
+    private static boolean mentionedByOtherRows(VCImplication chain, VCImplication row) {
+        for (VCImplication other = chain; other != null; other = other.getNext())
+            if (other != row && containsVar(other.getRefinement().getExpression(), row.getName()))
+                return true;
+        return false;
+    }
+
     private static Set<String> primitiveBinders(VCImplication chain) {
         Set<String> primitives = new HashSet<>();
         for (VCImplication current = chain; current != null; current = current.getNext())
 
@@ -34,24 +34,25 @@ public VCBinderSimplification(NeededVariables needed) {
     @Override
     public VCImplication apply(VCImplication implication) {
         VCImplication cloned = implication.clone();
-        VCImplication simplified = simplify(cloned, needed.trueBindersToKeep(cloned));
+        VCImplication simplified = simplify(cloned, needed.trueBindersToKeep(cloned), needed.unlinkedBinders(cloned));
         return simplified == null ? cloned : simplified;
     }
 
     /**
      * Simplifies the first applicable binder in a VC chain
      */
-    private VCImplication simplify(VCImplication implication, Set<String> keptTrueBinders) {
+    private VCImplication simplify(VCImplication implication, Set<String> keptTrueBinders,
+            Set<String> unlinkedBinders) {
         if (implication == null)
             return null;
 
         if (isFalseBinder(implication))
             return collapseFalseBinder(implication);
 
-        if (isRemovableBinder(implication, keptTrueBinders))
+        if (isRemovableBinder(implication, keptTrueBinders, unlinkedBinders))
             return removeBinder(implication);
 
-        VCImplication next = simplify(implication.getNext(), keptTrueBinders);
+        VCImplication next = simplify(implication.getNext(), keptTrueBinders, unlinkedBinders);
         if (next == null)
             return null;
 
@@ -87,29 +88,39 @@ private VCImplication removeBinder(VCImplication implication) {
     /**
      * Checks whether a binder can be removed without changing the VC conclusion or hiding what explains the error. A
      * binder refined only by true states no fact, so it is removed even when a later implication uses its variable,
-     * unless the error needs it
+     * unless the error needs it. A generated path condition that expected does not depend on is removed too
      */
-    private boolean isRemovableBinder(VCImplication implication, Set<String> keptTrueBinders) {
+    private boolean isRemovableBinder(VCImplication implication, Set<String> keptTrueBinders,
+            Set<String> unlinkedBinders) {
         if (!implication.hasBinder())
             return false;
 
         if (isTrueBinder(implication))
             return !keptTrueBinders.contains(implication.getName());
+        if (isGeneratedBooleanBinder(implication) && unlinkedBinders.contains(implication.getName()))
+            return true;
         return !containsVar(implication.getNext(), implication.getName()) && isUnusedFreshPathBinder(implication);
     }
 
     /**
      * Checks for a generated boolean path binder refined exactly by itself
      */
     private boolean isUnusedFreshPathBinder(VCImplication implication) {
-        if (!implication.hasNext() || !GeneratedNames.isGenerated(implication.getName())
-                || !"boolean".equals(implication.getType().getQualifiedName()))
+        if (!implication.hasNext() || !isGeneratedBooleanBinder(implication))
             return false;
 
         return implication.getRefinement().getExpression()instanceof Var var
                 && implication.getName().equals(var.getName());
     }
 
+    /**
+     * Checks for a binder of a generated boolean, such as a path condition
+     */
+    private boolean isGeneratedBooleanBinder(VCImplication implication) {
+        return GeneratedNames.isGenerated(implication.getName())
+                && "boolean".equals(implication.getType().getQualifiedName());
+    }
+
     /**
      * Replaces a false binder implication with true
      */