From af93729d6fb923b6be2e7835b57e9aa3712bfedd Mon Sep 17 00:00:00 2001
From: Ricardo Costa <rcosta.ms358@gmail.com>
Date: Thu, 6 Aug 2026 23:03:55 +0100
Subject: [PATCH] Fix NPE When Invoking Methods on Object Fields

---
 .../refinement_checker/object_checkers/AuxStateHandler.java     | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
index c4da97d87..e8f515d20 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
@@ -594,6 +594,8 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
             // v--------- field read
             // means invocation is in a form of `t.method(args)`
             String name = v.getVariable().getSimpleName();
+            if (v instanceof CtFieldRead<?>)
+                name = String.format(Formats.THIS, name);
             Optional<VariableInstance> invocationCallee = tc.getContext().getLastVariableInstance(name);
             if (invocationCallee.isPresent()) {
                 invocation.putMetadata(Keys.TARGET, invocationCallee.get());