diff --git a/liquidjava-example/src/main/java/testSuite/CorrectNestedIfCallComparison.java b/liquidjava-example/src/main/java/testSuite/CorrectNestedIfCallComparison.java
new file mode 100644
index 00000000..c1a3163c
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/CorrectNestedIfCallComparison.java
@@ -0,0 +1,29 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class CorrectNestedIfDoor {
+    @StateRefinement(to = "open(this)")
+    public CorrectNestedIfDoor() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}
+
+public class CorrectNestedIfCallComparison {
+    static CorrectNestedIfDoor current() {
+        return new CorrectNestedIfDoor();
+    }
+
+    static void compareInNestedIf(boolean b) {
+        CorrectNestedIfDoor d = new CorrectNestedIfDoor();
+        if (b) {
+            if (current() == d) {
+                System.out.println("same");
+            }
+        }
+        d.close();
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java b/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java
new file mode 100644
index 00000000..248db689
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java
@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class ErrorIfReferenceDoor {
+    @StateRefinement(to = "open(this)")
+    public ErrorIfReferenceDoor() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}
+
+public class ErrorIfReferenceComparison {
+    static void closeTwice(ErrorIfReferenceDoor other) {
+        ErrorIfReferenceDoor d = new ErrorIfReferenceDoor();
+        if (other == d) {
+            d.close();
+        }
+        d.close(); // Expect: State Refinement Error
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java b/liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java
new file mode 100644
index 00000000..dbcb14e6
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java
@@ -0,0 +1,29 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class ErrorNestedIfDoor {
+    @StateRefinement(to = "open(this)")
+    public ErrorNestedIfDoor() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}
+
+public class ErrorNestedIfCallComparison {
+    static ErrorNestedIfDoor current() {
+        return new ErrorNestedIfDoor();
+    }
+
+    static void closeTwice(boolean b) {
+        ErrorNestedIfDoor d = new ErrorNestedIfDoor();
+        if (b) {
+            if (current() == d) {
+                d.close();
+            }
+        }
+        d.close(); // Expect: State Refinement Error
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
index 7fcbc31d..c4dfa63b 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
@@ -500,6 +500,10 @@ public void visitCtIf(CtIf ifElement) {
         }
 
         Predicate branchGuard = valueIsCondition ? Predicate.createVar(pathVarName) : expRefs;
+        // The joined instances are read after the if, where a variable's name stands for its latest instance; the
+        // guard must name the instances the condition read (`other == d` would otherwise compare the joined d)
+        Predicate joinGuard = valueIsCondition ? branchGuard : lastExpRefs;
+        keepFreshValues(joinGuard);
         Predicate thenRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard) : branchGuard;
         Predicate elseRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard.negate())
                 : branchGuard.negate();
@@ -547,10 +551,28 @@ public void visitCtIf(CtIf ifElement) {
             context.newRefinementToVariableInContext(pathVarName, thenCompletes ? thenRefs : elseRefs);
         }
         context.exitContext();
-        context.variablesCombineFromIf(branchGuard);
+        context.variablesCombineFromIf(joinGuard);
         context.variablesFinishIfCombination();
     }
 
+    /**
+     * The fresh values a condition creates (such as a call's result) belong to the enclosing block, but the branch
+     * guard ends up in the joined instances of the variables changed in the if, which can outlive that block (an if
+     * nested in another if's branch). Keeps those values, and the fresh values their refinements use, in the context.
+     */
+    private void keepFreshValues(Predicate predicate) {
+        String freshPrefix = Formats.FRESH.substring(0, Formats.FRESH.indexOf('%'));
+        for (String name : predicate.getVariableNames()) {
+            if (!name.startsWith(freshPrefix))
+                continue;
+            RefinedVariable value = context.getVariableByName(name);
+            if (value != null && !context.getCtxInstanceVars().contains(value)) {
+                context.addInstanceVariable(value);
+                keepFreshValues(value.getRefinement());
+            }
+        }
+    }
+
     /**
      * A condition is uninformative when its refinement is the trivial {@code true} predicate yet the expression itself
      * is not a boolean literal — i.e. the verifier has no symbolic information to relate the branch to. Treating such a