Fix Method Check Ordering

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -286,16 +286,22 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
             return new HashMap<>();
         Map<String, String> map = mapInvocation(arguments, f);
 
-        if (target != null) {
-            AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation);
-        }
+        if (target != null)
+            AuxStateHandler.prepareInvocationTarget(rtc, target, invocation);
+
         if (f.allRefinementsTrue()) {
+            if (target != null)
+                AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation);
+
             invocation.putMetadata(Keys.REFINEMENT, new Predicate());
             return map;
         }
 
         checkParameters(invocation, arguments, f, map);
 
+        if (target != null)
+            AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation);
+
         // -- Part 2: Apply changes
         // applyRefinementsToArguments(element, arguments, f, map);
         Predicate methodRef = f.getRefReturn();

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -359,7 +359,7 @@ public static void addStateRefinements(TypeChecker tc, String varName, CtExpress
      */
     public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpression<?> target2,
             Map<String, String> map, CtElement invocation) throws LJError {
-        String parentTargetName = searchFistVariableTarget(tc, target2, invocation);
+        String parentTargetName = prepareInvocationTarget(tc, target2, invocation);
         VariableInstance target = getTarget(invocation);
         if (target != null) {
             if (f.hasStateChange() && !f.getFromStates().isEmpty()) {
@@ -576,7 +576,7 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin
      *
      * @return the name of the parent target
      */
-    static String searchFistVariableTarget(TypeChecker tc, CtElement target2, CtElement invocation) {
+    public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, CtElement invocation) {
         if (target2 instanceof CtVariableRead<?> v) {
             // v--------- field read
             // means invocation is in a form of `t.method(args)`