Scope the type of return in state refinement checks

liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/AVectorRefinements.java

@@ -0,0 +1,16 @@
+package testSuite.classes.state_return_type_scope_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// Checked before BUndoManagerRefinements: its return type (E) must not become the type of `return` there
+@StateSet({"empty", "nonEmpty"})
+@ExternalRefinementsFor("java.util.Vector")
+public interface AVectorRefinements<E> {
+    @StateRefinement(to = "empty(this)")
+    public void Vector();
+
+    @StateRefinement(to = "nonEmpty(this)")
+    public E set(int index, E element);
+}

liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/BUndoManagerRefinements.java

@@ -0,0 +1,15 @@
+package testSuite.classes.state_return_type_scope_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"start", "canEdit"})
+@ExternalRefinementsFor("javax.swing.undo.UndoManager")
+public interface BUndoManagerRefinements {
+    @StateRefinement(to = "start(this)")
+    public void UndoManager();
+
+    @StateRefinement(from = "start(this)", to = "!return && start(this)")
+    public boolean canUndo();
+}

liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/SimpleTest.java

@@ -0,0 +1,10 @@
+package testSuite.classes.state_return_type_scope_correct;
+
+import javax.swing.undo.UndoManager;
+
+public class SimpleTest {
+    public static void main(String[] args) {
+        UndoManager manager = new UndoManager();
+        boolean b = manager.canUndo();
+    }
+}

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

@@ -309,22 +309,28 @@ private static Predicate createStatePredicate(Predicate p, String value, String
             }
         }
         CtTypeReference<?> r = tc.getFactory().Type().createReference(targetClass);
-        String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
-        String name = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
-        tc.getContext().addVarToContext(Keys.THIS, r, new Predicate(), e);
-        tc.getContext().addVarToContext(name, r, new Predicate(), e);
-        tc.getContext().addVarToContext(nameOld, r, new Predicate(), e);
-        if (returnType != null && !tc.getContext().hasVariable(Keys.WILDCARD))
-            tc.getContext().addVarToContext(Keys.WILDCARD, returnType, new Predicate(), e);
-        // TODO REVIEW!!
-        // what is it for?
-        Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p;
-        Predicate c = c1.substituteVariable(Keys.THIS, name);
-        c = c.changeOldMentions(nameOld, name);
-        boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), position, true);
-        if (ok)
-            tc.throwStateConflictError(position, p);
-        return c1;
+        tc.getContext().enterContext();
+        try {
+            String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
+            String name = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
+            tc.getContext().addVarToContext(Keys.THIS, r, new Predicate(), e);
+            tc.getContext().addVarToContext(name, r, new Predicate(), e);
+            tc.getContext().addVarToContext(nameOld, r, new Predicate(), e);
+            // in this scope, so that each method's `return` has its own type
+            if (returnType != null)
+                tc.getContext().addVarToContext(Keys.WILDCARD, returnType, new Predicate(), e);
+            // TODO REVIEW!!
+            // what is it for?
+            Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p;
+            Predicate c = c1.substituteVariable(Keys.THIS, name);
+            c = c.changeOldMentions(nameOld, name);
+            boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), position, true);
+            if (ok)
+                tc.throwStateConflictError(position, p);
+            return c1;
+        } finally {
+            tc.getContext().exitContext();
+        }
     }
 
     /**