diff --git a/liquidjava-example/src/main/java/testSuite/CorrectOuterFieldAfterNestedClass.java b/liquidjava-example/src/main/java/testSuite/CorrectOuterFieldAfterNestedClass.java
new file mode 100644
index 00000000..7c994eb2
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/CorrectOuterFieldAfterNestedClass.java
@@ -0,0 +1,12 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+class CorrectOuterFieldAfterNestedClass {
+    @Refinement("_ > 0") int x = 1;
+
+    static class Inner { int y; }
+
+    @Refinement("_ > 0")
+    public int get() { return x; }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNestedFieldLeak.java b/liquidjava-example/src/main/java/testSuite/ErrorNestedFieldLeak.java
new file mode 100644
index 00000000..3ff32b16
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorNestedFieldLeak.java
@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+class ErrorNestedFieldLeak {
+    int x = 1;
+
+    static class Inner {
+        @Refinement("_ < 0") int x = -1;
+    }
+
+    @Refinement("_ < 0")
+    public int get() { return x; } // Expect: Refinement Error
+}
diff --git a/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java b/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java
new file mode 100644
index 00000000..4f7190cf
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java
@@ -0,0 +1,17 @@
+package testSuite.classes.forward_field_read_correct;
+
+import liquidjava.specification.Refinement;
+
+public class ReadBefore {
+    private final Job job = new Job();
+
+    @Refinement("_ >= 0")
+    public int get() {
+        return job.port;
+    }
+
+    static class Job {
+        @Refinement("_ >= 0")
+        int port;
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
index 298179e6..b1d30f5f 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
@@ -47,6 +47,27 @@ public void reinitializeContext() {
         clearInstanceVariables();
     }
 
+    public ClassScope enterClassScope() {
+        ClassScope scope = new ClassScope(ctxVars, ctxInstanceVars);
+        reinitializeContext();
+        return scope;
+    }
+
+    public void exitClassScope(ClassScope scope) {
+        ctxVars = scope.variables;
+        ctxInstanceVars = scope.instances;
+    }
+
+    public static class ClassScope {
+        private final Stack<List<RefinedVariable>> variables;
+        private final List<RefinedVariable> instances;
+
+        private ClassScope(Stack<List<RefinedVariable>> variables, List<RefinedVariable> instances) {
+            this.variables = variables;
+            this.instances = instances;
+        }
+    }
+
     public void clearInstanceVariables() {
         ctxInstanceVars = new ArrayList<>();
     }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java
index 3dda3881..fcfdea18 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java
@@ -32,41 +32,45 @@ public MethodsFirstChecker(Context context, Factory factory) {
 
     @Override
     public <T> void visitCtClass(CtClass<T> ctClass) {
-        context.reinitializeContext();
         if (visitedClasses.contains(ctClass.getQualifiedName()))
             return;
         else
             visitedClasses.add(ctClass.getQualifiedName());
-        // visitInterfaces
-        if (!ctClass.getSuperInterfaces().isEmpty())
-            for (CtTypeReference<?> t : ctClass.getSuperInterfaces()) {
-                if (t.isInterface()) {
-                    CtType<?> ct = t.getDeclaration();
-                    if (ct instanceof CtInterface)
-                        visitCtInterface((CtInterface<?>) ct);
+        Context.ClassScope scope = context.enterClassScope();
+        try {
+            // visitInterfaces
+            if (!ctClass.getSuperInterfaces().isEmpty())
+                for (CtTypeReference<?> t : ctClass.getSuperInterfaces()) {
+                    if (t.isInterface()) {
+                        CtType<?> ct = t.getDeclaration();
+                        if (ct instanceof CtInterface)
+                            visitCtInterface((CtInterface<?>) ct);
+                    }
                 }
+            // visitSubclasses
+            CtTypeReference<?> sup = ctClass.getSuperclass();
+            if (sup != null && sup.isClass()) {
+                CtType<?> ct = sup.getDeclaration();
+                if (ct instanceof CtClass)
+                    visitCtClass((CtClass<?>) ct);
             }
-        // visitSubclasses
-        CtTypeReference<?> sup = ctClass.getSuperclass();
-        if (sup != null && sup.isClass()) {
-            CtType<?> ct = sup.getDeclaration();
-            if (ct instanceof CtClass)
-                visitCtClass((CtClass<?>) ct);
-        }
-        // first try-catch: process class-level annotations)
-        // errors here should not prevent visiting methods, constructors or fields of the class
-        try {
-            getRefinementFromAnnotation(ctClass);
-            handleStateSetsFromAnnotation(ctClass);
-        } catch (LJError e) {
-            diagnostics.add(e);
-        }
-        // second try-catch: visit class children (methods, constructors, fields)
-        // errors from one child should not prevent visiting sibling elements
-        try {
-            super.visitCtClass(ctClass);
-        } catch (LJError e) {
-            diagnostics.add(e);
+            // first try-catch: process class-level annotations)
+            // errors here should not prevent visiting methods, constructors or fields of the class
+            try {
+                getRefinementFromAnnotation(ctClass);
+                handleStateSetsFromAnnotation(ctClass);
+            } catch (LJError e) {
+                diagnostics.add(e);
+            }
+            // second try-catch: visit class children (methods, constructors, fields)
+            // errors from one child should not prevent visiting sibling elements
+            try {
+                super.visitCtClass(ctClass);
+            } catch (LJError e) {
+                diagnostics.add(e);
+            }
+        } finally {
+            context.exitClassScope(scope);
         }
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
index bf6dcc99..4ec745b2 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
@@ -74,15 +74,14 @@ public RefinementTypeChecker(Context context, Factory factory) {
 
     @Override
     public <T> void visitCtClass(CtClass<T> ctClass) {
-        // System.out.println("CTCLASS:"+ctClass.getSimpleName());
-        context.reinitializeContext();
-
+        Context.ClassScope scope = context.enterClassScope();
         try {
             super.visitCtClass(ctClass);
         } catch (LJError e) {
             diagnostics.add(e);
+        } finally {
+            context.exitClassScope(scope);
         }
-
     }
 
     @Override
@@ -308,6 +307,10 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
                     Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(enumLiteral)));
         } else if (tryStaticFinalConstantRefinement(fieldRead)) {
             // refinement metadata set by helper
+        } else if (fieldRead.getVariable().getDeclaration() != null) {
+            Predicate declared = getRefinementFromAnnotation(fieldRead.getVariable().getDeclaration())
+                    .orElseGet(Predicate::new);
+            fieldRead.putMetadata(Keys.REFINEMENT, declared.substituteVariable(fieldName, Keys.WILDCARD));
         } else {
             fieldRead.putMetadata(Keys.REFINEMENT, new Predicate());
             // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE?