Substitute this in Parameter Refinements

rcosta358 · rcosta358 · commit 589437b92cdb · 2025-10-23T15:40:05.000+01:00
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java
@@ -374,6 +374,10 @@ private <R> void checkParameters(CtElement invocation, List<CtExpression<?>> arg
             for (String s : vars)
                 if (map.containsKey(s))
                     c = c.substituteVariable(s, map.get(s));
+            if (invocation.getMetadata(rtc.TARGET_KEY) != null) {
+                VariableInstance vi = (VariableInstance) invocation.getMetadata(rtc.TARGET_KEY);
+                c = c.substituteVariable(rtc.THIS, vi.getName());
+            }
             rtc.checkSMT(c, invocation);
         }
     }

Original file line number	Diff line number	Diff line change
`@@ -374,6 +374,10 @@ private <R> void checkParameters(CtElement invocation, List<CtExpression<?>> arg`
`374`	`374`	`for (String s : vars)`
`375`	`375`	`if (map.containsKey(s))`
`376`	`376`	`c = c.substituteVariable(s, map.get(s));`
	`377`	`+ if (invocation.getMetadata(rtc.TARGET_KEY) != null) {`
	`378`	`+ VariableInstance vi = (VariableInstance) invocation.getMetadata(rtc.TARGET_KEY);`
	`379`	`+ c = c.substituteVariable(rtc.THIS, vi.getName());`
	`380`	`+ }`
`377`	`381`	`rtc.checkSMT(c, invocation);`
`378`	`382`	`}`
`379`	`383`	`}`