@@ -2,7 +2,7 @@
 
 import liquidjava.specification.Refinement;
 
-// a write to another object's field is checked against the field's refinement under that object's name (#457)
+// writes to another object's field are checked as on main; only their display names the object (#457)
 public class ErrorOtherObjectFieldWrite {
     @Refinement("_ >= 0")
     int level;
@@ -11,10 +11,26 @@ void setOther(ErrorOtherObjectFieldWrite other) {
         other.level = -1; // Expect: Refinement Error
     }
 
+    void incrementOther(ErrorOtherObjectFieldWrite other) {
+        other.level++;
+    }
+
+    void addToOther(ErrorOtherObjectFieldWrite other) {
+        other.level += 1;
+    }
+
     void decrementOther(ErrorOtherObjectFieldWrite other) {
         other.level--; // Expect: Refinement Error
     }
 
+    void writeThroughAlias() {
+        level = 7;
+        ErrorOtherObjectFieldWrite other = this;
+        other.level = 3;
+        @Refinement("_ == 7")
+        int k = level; // Expect: Refinement Error
+    }
+
     void setOwn() {
         this.level = -1; // Expect: Refinement Error
     }
 
@@ -267,7 +267,7 @@ private <T, A extends T> void visitAssignment(CtAssignment<T, A> assignment) thr
         } else if (ex instanceof CtFieldWrite<?> fw) {
             CtFieldReference<?> cr = fw.getVariable();
             CtField<?> f = fw.getVariable().getDeclaration();
-            String updatedVarName = Utils.writtenFieldName(fw);
+            String updatedVarName = Utils.qualifyFieldName(cr);
             // a field declared outside the analyzed sources (e.g. a library field) has no declared refinement: the
             // write stands in for its declaration
             checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment,
 
@@ -23,6 +23,7 @@
 import liquidjava.processor.state_machine.StateMachineBuilder;
 import liquidjava.processor.state_machine.StateSolver;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.smt.SMTEvaluator;
 import liquidjava.smt.SMTResult;
@@ -382,6 +383,8 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
         Predicate cet = cEt.substituteVariable(Keys.WILDCARD, simpleName);
 
         String newName = String.format(Formats.INSTANCE, simpleName, context.getCounter());
+        Utils.untrackedWriteReceiver(usage)
+                .ifPresent(receiver -> VariableFormatter.registerReceiver(newName, receiver));
         Predicate correctNewRefinement = refinementFound.substituteVariable(Keys.WILDCARD, newName);
         correctNewRefinement = correctNewRefinement.substituteVariable(Keys.THIS, newName);
         cEt = cEt.substituteVariable(simpleName, newName);
 
@@ -179,7 +179,7 @@ public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws LJErro
         if (ex instanceof CtVariableWrite<T> w) {
             name = w.getVariable().getSimpleName();
             if (w instanceof CtFieldWrite<?> fieldWrite)
-                name = Utils.writtenFieldName(fieldWrite);
+                name = Utils.qualifyFieldName(fieldWrite.getVariable());
             all = getRefinementUnaryVariableWrite(ex, operator, w, name);
             rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration());
             return;
@@ -498,8 +498,6 @@ private <T> Predicate getRefinementUnaryVariableWrite(CtExpression<T> ex, CtUnar
         String newName = String.format(Formats.INSTANCE, name, rtc.getContext().getCounter());
 
         Predicate metadada = rtc.getContext().getVariableRefinements(name);
-        if (metadada == null) // a field of another object, whose current value is not tracked
-            metadada = new Predicate();
         metadada = metadada.substituteVariable(Keys.WILDCARD, newName);
         metadada = metadada.substituteVariable(name, newName);
 
 
@@ -635,7 +635,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre
      */
     public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws LJError {
         CtField<?> field = fw.getVariable().getDeclaration();
-        String updatedVarName = Utils.writtenFieldName(fw);
+        String updatedVarName = Utils.qualifyFieldName(fw.getVariable());
         String targetClass = field.getDeclaringType().getQualifiedName();
 
         // state transition annotation construction
 
@@ -1,5 +1,6 @@
 package liquidjava.rj_language.ast.formatter;
 
+import java.util.Map;
 import java.util.Set;
 import java.util.concurrent.ConcurrentHashMap;
 import java.util.regex.Matcher;
@@ -10,11 +11,11 @@
  */
 public final class VariableFormatter {
     private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$");
-    // <object>#<declaring type>.<field>: a field of the current object (this) or of the object in a local variable
-    private static final Pattern FIELD_PATTERN = Pattern.compile("^([A-Za-z_$][\\w$]*)#([\\w.$]+)\\.([\\w$]+)$");
+    // this#<declaring type>.<field>
+    private static final Pattern FIELD_PATTERN = Pattern.compile("^this#([\\w.$]+)\\.([\\w$]+)$");
     private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' };
-    private static final String THIS = "this";
     private static final Set<String> STATIC_FIELDS = ConcurrentHashMap.newKeySet();
+    private static final Map<String, String> WRITE_RECEIVERS = new ConcurrentHashMap<>();
 
     public static String format(String name) {
         if (name == null)
@@ -26,6 +27,9 @@ public static String format(String name) {
 
         String baseName = matcher.group(1);
         String counter = matcher.group(2);
+        String receiver = WRITE_RECEIVERS.get(name);
+        if (receiver != null && isField(baseName))
+            return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + toSuperscript(counter);
         String prefix = isSpecialIdentifier(baseName) ? "#" : "";
         return prefix + formatField(baseName) + toSuperscript(counter);
     }
@@ -36,7 +40,7 @@ public static String withoutInstance(String name) {
     }
 
     /**
-     * Whether a name is that of a field, {@code <object>#<declaring type>.<field>}, possibly with an instance counter
+     * Whether a name is that of a field, {@code this#<declaring type>.<field>}, possibly with an instance counter
      */
     public static boolean isField(String name) {
         return FIELD_PATTERN.matcher(withoutInstance(name)).matches();
@@ -51,27 +55,40 @@ public static void registerStaticField(String name) {
     }
 
     /**
-     * Forgets the static fields recorded by the previous verification
+     * Records that an instance of a field ({@code #this#<declaring type>.<field>_<n>}) was created by a write through
+     * another object ({@code receiver.field = v}), so that it is displayed as {@code receiver.field} instead of
+     * {@code this.field}; an empty receiver displays the bare field name. Only the display changes
+     */
+    public static void registerReceiver(String instanceName, String receiver) {
+        WRITE_RECEIVERS.put(instanceName, receiver);
+    }
+
+    /**
+     * Forgets the static fields and write receivers recorded by the previous verification
      */
     public static void clearStaticFields() {
         STATIC_FIELDS.clear();
+        WRITE_RECEIVERS.clear();
     }
 
     /**
-     * Writes a field name as it is written in code: {@code this.field} or {@code other.field} for an instance field and
-     * {@code Class.field} for a static one, leaving any other name unchanged; the internal name keeps the declaring
-     * type to tell fields of different classes apart
+     * Writes a field name as it is written in code: {@code this.field} for an instance field and {@code Class.field}
+     * for a static one, leaving any other name unchanged; the internal name keeps the declaring type to tell fields of
+     * different classes apart
      */
     private static String formatField(String name) {
         Matcher matcher = FIELD_PATTERN.matcher(name);
         if (!matcher.matches())
             return name;
 
-        String object = matcher.group(1);
-        String field = matcher.group(3);
-        if (object.equals(THIS) && STATIC_FIELDS.contains(name))
-            return simpleTypeName(matcher.group(2)) + "." + field;
-        return object + "." + field;
+        if (STATIC_FIELDS.contains(name))
+            return simpleTypeName(matcher.group(1)) + "." + matcher.group(2);
+        return "this." + matcher.group(2);
+    }
+
+    private static String fieldOf(String name) {
+        Matcher matcher = FIELD_PATTERN.matcher(name);
+        return matcher.matches() ? matcher.group(2) : name;
     }
 
     private static String simpleTypeName(String qualifiedName) {
 
@@ -5,6 +5,7 @@
 import static liquidjava.rj_language.opt.VCSimplificationUtils.splitConjuncts;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.termsOf;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.valueVariablesOf;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.variablesOf;
 
 import java.util.ArrayList;
 import java.util.HashSet;
@@ -60,19 +61,32 @@ private static NeededVariables of(Predicate expected, boolean keepExpected) {
 
     /**
      * Variables whose binder refined only by true the chain keeps: those whose own value a fact linked to expected
-     * constrains. A variable named only as the object of a ghost or state application ({@code x} in
-     * {@code b == size(x)}) has no value of its own there, so its row would say nothing
+     * constrains. A variable of an object type that a fact names only as the argument of a ghost or state application
+     * ({@code x} in {@code b == size(x)}) has no value of its own there, so its row would say nothing; a primitive
+     * argument ({@code k} in {@code y == f(k)}) has one
      */
     public Set<String> trueBindersToKeep(VCImplication chain) {
         List<Expression> facts = new ArrayList<>();
-        for (VCImplication current = chain; current != null; current = current.getNext())
+        Set<String> primitives = new HashSet<>();
+        for (VCImplication current = chain; current != null; current = current.getNext()) {
+            if (current.hasBinder() && current.getType().isPrimitive())
+                primitives.add(current.getName());
             if (!isTrue(current.getRefinement().getExpression()))
                 facts.addAll(splitConjuncts(current.getRefinement().getExpression()));
+        }
 
-        Set<String> keep = new HashSet<>(keepExpected ? expectedValues : Set.of());
-        for (Expression fact : linkedConjuncts(facts, VCSimplificationUtils::termsOf, expectedTerms))
-            for (String name : valueVariablesOf(fact))
-                if (!expectedTerms.contains(name))
+        Set<String> keep = new HashSet<>();
+        if (keepExpected)
+            keep.addAll(expectedValues);
+        for (Expression fact : linkedConjuncts(facts, VCSimplificationUtils::termsOf, expectedTerms)) {
+            List<String> values = valueVariablesOf(fact);
+            for (String name : variablesOf(fact))
+                if ((values.contains(name) || primitives.contains(name)) && !expectedTerms.contains(name))
+                    keep.add(name);
+        }
+        if (keepExpected)
+            for (String name : expectedTerms)
+                if (primitives.contains(name))
                     keep.add(name);
         return keep;
     }
 
@@ -3,20 +3,25 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Objects;
+import java.util.Optional;
 import java.util.Scanner;
 import java.util.Set;
 import java.util.stream.Stream;
 
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.utils.constants.Types;
+import spoon.reflect.code.CtAssignment;
 import spoon.reflect.code.CtBlock;
+import spoon.reflect.code.CtExpression;
 import spoon.reflect.code.CtFieldAccess;
+import spoon.reflect.code.CtFieldWrite;
 import spoon.reflect.code.CtFor;
 import spoon.reflect.code.CtForEach;
 import spoon.reflect.code.CtIf;
 import spoon.reflect.code.CtSuperAccess;
 import spoon.reflect.code.CtThisAccess;
 import spoon.reflect.code.CtTry;
+import spoon.reflect.code.CtUnaryOperator;
 import spoon.reflect.code.CtVariableRead;
 import spoon.reflect.code.CtWhile;
 import spoon.reflect.cu.SourcePosition;
@@ -67,17 +72,17 @@ public static String qualifyFieldName(CtFieldReference<?> field) {
     }
 
     /**
-     * Name of the context variable that a field write updates: the tracked field ({@link #qualifyFieldName}) for a
-     * static field or a field of the current object, and otherwise a variable of its own for that field of the other
-     * object, {@code <object>#<declaring type>.<field>}, named after the variable holding the object when there is one
+     * The object through which a write updates a field of another object ({@code other} in {@code other.f = v} or
+     * {@code other.f++}), used only to display that write; empty when the write is to a tracked field (see
+     * {@link #accessesTrackedField}) or not a field write, and an empty string when the object is not in a variable
      */
-    public static String writtenFieldName(CtFieldAccess<?> access) {
-        String name = qualifyFieldName(access.getVariable());
-        if (accessesTrackedField(access))
-            return name;
-        String object = access.getTarget()instanceof CtVariableRead<?> read ? read.getVariable().getSimpleName()
-                : "other";
-        return object + name.substring("this".length());
+    public static Optional<String> untrackedWriteReceiver(CtElement usage) {
+        CtExpression<?> written = usage instanceof CtAssignment<?, ?> assignment ? assignment.getAssigned()
+                : usage instanceof CtUnaryOperator<?> unary ? unary.getOperand() : null;
+        if (!(written instanceof CtFieldWrite<?> write) || accessesTrackedField(write))
+            return Optional.empty();
+        return Optional
+                .of(write.getTarget()instanceof CtVariableRead<?> read ? read.getVariable().getSimpleName() : "");
     }
 
     public static String getFile(CtElement element) {
 
@@ -165,13 +165,19 @@ void trueRowDecidingAPathDependentStateIsKept() {
         assertEquals(List.of("∀ready true", "∀f ready ? open(f) : created(f)"), shown.rows());
     }
 
+    @Test
+    void writesToAnotherObjectsFieldAreCheckedAsOnMain() {
+        // other.level++ and other.level += 1 verify, other.level-- and the write through an alias of this are reported
+        assertEquals(List.of(11, 23, 31, 35), new ArrayList<>(otherObjectWrite.keySet()));
+        assertEquals("k == 7", otherObjectWrite.get(31).message().replaceAll(".* is not a subtype of ", ""));
+    }
+
     @Test
     void writeToAnotherObjectsFieldIsWrittenWithThatObject() {
-        assertEquals(List.of(11, 15, 19), new ArrayList<>(otherObjectWrite.keySet()));
         assertEquals("other.level == -1 is not a subtype of other.level >= 0", otherObjectWrite.get(11).message());
-        assertEquals(List.of("∀other.level true", "∀other.level other.level == other.level - 1"),
-                otherObjectWrite.get(15).rows());
-        assertEquals("this.level == -1 is not a subtype of this.level >= 0", otherObjectWrite.get(19).message());
+        assertEquals(List.of("∀this.level this.level >= 0", "∀other.level other.level == this.level - 1"),
+                otherObjectWrite.get(23).rows());
+        assertEquals("this.level == -1 is not a subtype of this.level >= 0", otherObjectWrite.get(35).message());
     }
 
     @Test
 
@@ -50,16 +50,22 @@ void forgetsStaticFieldsOfThePreviousVerification() {
     }
 
     @Test
-    void writesFieldsOfAnotherObjectWithThatObject() {
-        assertEquals("other.level", VariableFormatter.format("other#otherwrite.W.level"));
-        assertEquals("other.level¹", VariableFormatter.format("#other#otherwrite.W.level_1"));
+    void writesAnInstanceCreatedByAWriteThroughAnotherObjectWithThatObject() {
+        VariableFormatter.registerReceiver("#this#otherwrite.W.level_1", "other");
+        VariableFormatter.registerReceiver("#this#otherwrite.W.level_2", "");
+        assertEquals("other.level¹", VariableFormatter.format("#this#otherwrite.W.level_1"));
+        assertEquals("level²", VariableFormatter.format("#this#otherwrite.W.level_2"));
+        assertEquals("this.level³", VariableFormatter.format("#this#otherwrite.W.level_3"));
+        assertEquals("this.level", VariableFormatter.format("this#otherwrite.W.level"));
+        VariableFormatter.clearStaticFields();
+        assertEquals("this.level¹", VariableFormatter.format("#this#otherwrite.W.level_1"));
     }
 
     @Test
     void recognisesFieldNames() {
         assertTrue(VariableFormatter.isField("this#shop.Basket.items"));
         assertTrue(VariableFormatter.isField("#this#shop.Basket.items_4"));
-        assertTrue(VariableFormatter.isField("other#otherwrite.W.level"));
+        assertFalse(VariableFormatter.isField("other#otherwrite.W.level"));
         assertFalse(VariableFormatter.isField("this#Basket"));
         assertFalse(VariableFormatter.isField("#this_4"));
         assertFalse(VariableFormatter.isField("items"));