From 95fc7fddbf0b8c98d776e150034385a624f2fa7c Mon Sep 17 00:00:00 2001
From: Ricardo Costa <rcosta.ms358@gmail.com>
Date: Fri, 7 Aug 2026 00:20:17 +0100
Subject: [PATCH] Fix Field Increment

---
 .../testSuite/field_updates/CorrectFieldIncrement.java | 10 ++++++++++
 .../general_checkers/OperationsChecker.java            |  7 ++++---
 2 files changed, 14 insertions(+), 3 deletions(-)
 create mode 100644 liquidjava-example/src/main/java/testSuite/field_updates/CorrectFieldIncrement.java

diff --git a/liquidjava-example/src/main/java/testSuite/field_updates/CorrectFieldIncrement.java b/liquidjava-example/src/main/java/testSuite/field_updates/CorrectFieldIncrement.java
new file mode 100644
index 000000000..9a23772cc
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/field_updates/CorrectFieldIncrement.java
@@ -0,0 +1,10 @@
+package testSuite.field_updates;
+
+public class CorrectFieldIncrement {
+
+    private int field;
+
+    public void increment() {
+        field++;
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java
index 5e98d65b0..2bb7a3ee7 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java
@@ -25,6 +25,7 @@
 import spoon.reflect.code.CtBinaryOperator;
 import spoon.reflect.code.CtExpression;
 import spoon.reflect.code.CtFieldRead;
+import spoon.reflect.code.CtFieldWrite;
 import spoon.reflect.code.CtIf;
 import spoon.reflect.code.CtInvocation;
 import spoon.reflect.code.CtLiteral;
@@ -39,7 +40,6 @@
 import spoon.reflect.declaration.CtClass;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtExecutable;
-import spoon.reflect.declaration.CtVariable;
 import spoon.reflect.declaration.ParentNotInitializedException;
 import spoon.reflect.reference.CtVariableReference;
 import spoon.support.reflect.code.CtIfImpl;
@@ -123,6 +123,8 @@ public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws LJErro
         Predicate all;
         if (ex instanceof CtVariableWrite<T> w) {
             name = w.getVariable().getSimpleName();
+            if (w instanceof CtFieldWrite<?>)
+                name = String.format(Formats.THIS, name);
             all = getRefinementUnaryVariableWrite(ex, operator, w, name);
             rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration());
             return;
@@ -389,9 +391,8 @@ private Predicate createFreshValue(CtExpression<?> element, Predicate refinement
     private <T> Predicate getRefinementUnaryVariableWrite(CtExpression<T> ex, CtUnaryOperator<T> operator,
             CtVariableWrite<T> w, String name) throws LJError {
         String newName = String.format(Formats.INSTANCE, name, rtc.getContext().getCounter());
-        CtVariable<T> varDecl = w.getVariable().getDeclaration();
 
-        Predicate metadada = rtc.getContext().getVariableRefinements(varDecl.getSimpleName());
+        Predicate metadada = rtc.getContext().getVariableRefinements(name);
         metadada = metadada.substituteVariable(Keys.WILDCARD, newName);
         metadada = metadada.substituteVariable(name, newName);