Fix this Resolution in Parameter Refinements

liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/ArrayListRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.index_out_of_bounds_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+@Ghost("int size")
+public interface ArrayListRefinements<E> {
+
+    public void ArrayList();
+
+	@StateRefinement(to = "size(this) == size(old(this)) + 1")
+	public boolean add(E elem);
+
+	public E get(@Refinement("_ < size(this)") int index);
+}

liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/Test.java

@@ -0,0 +1,11 @@
+package testSuite.classes.index_out_of_bounds_correct;
+
+import java.util.ArrayList;
+
+public class Test {
+    public static void main(String[] args) {
+        ArrayList<Integer> l = new ArrayList<>();
+        l.add(1);
+        l.get(0);
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/ArrayListRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.index_out_of_bounds_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+@Ghost("int size")
+public interface ArrayListRefinements<E> {
+
+    public void ArrayList();
+
+	@StateRefinement(to = "size(this) == size(old(this)) + 1")
+	public boolean add(E elem);
+
+	public E get(@Refinement("_ < size(this)") int index);
+}

liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/Test.java

@@ -0,0 +1,10 @@
+package testSuite.classes.index_out_of_bounds_error;
+
+import java.util.ArrayList;
+
+public class Test {
+    public static void main(String[] args) {
+        ArrayList<Integer> l = new ArrayList<>();
+        l.get(0); // index out of bounds
+    }
+}

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);
         }
     }