diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml
index 65b45140..1484744f 100644
--- a/liquidjava-verifier/pom.xml
+++ b/liquidjava-verifier/pom.xml
@@ -11,7 +11,7 @@
 
 	<groupId>io.github.liquid-java</groupId>
 	<artifactId>liquidjava-verifier</artifactId>
-	<version>0.0.12</version>
+	<version>0.0.13</version>
 	<name>liquidjava-verifier</name>
 	<description>LiquidJava Verifier</description>
 	<url>https://github.com/liquid-java/liquidjava</url>
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java
index ba8d268a..6eb4b724 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java
@@ -1,8 +1,5 @@
 package liquidjava.processor;
 
-import java.util.ArrayList;
-import java.util.List;
-
 import liquidjava.diagnostics.Diagnostics;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.processor.ann_generation.FieldGhostsGeneration;
@@ -17,7 +14,6 @@
 /** Finds circular dependencies between packages */
 public class RefinementProcessor extends AbstractProcessor<CtPackage> {
 
-    List<CtPackage> visitedPackages = new ArrayList<>();
     Factory factory;
     Diagnostics diagnostics = Diagnostics.getInstance();
 
@@ -25,29 +21,40 @@ public RefinementProcessor(Factory factory) {
         this.factory = factory;
     }
 
+    @Override
+    public boolean isToBeProcessed(CtPackage pkg) {
+        // Only let Spoon invoke us for the root package;
+        // we handle sub-packages ourselves to guarantee parent-before-child order.
+        return pkg.isUnnamedPackage();
+    }
+
     @Override
     public void process(CtPackage pkg) {
-        if (!visitedPackages.contains(pkg)) {
-            visitedPackages.add(pkg);
-            Context c = Context.getInstance();
-            c.reinitializeAllContext();
-
-            try {
-                // process types in this package only, not sub-packages
-                // first pass: gather refinements
-                pkg.getTypes().forEach(type -> {
-                    type.accept(new FieldGhostsGeneration(c, factory)); // generate annotations for field ghosts
-                    type.accept(new ExternalRefinementTypeChecker(c, factory)); // process external refinements
-                    type.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers)
-                });
-
-                // second pass: check refinements
-                pkg.getTypes().forEach(type -> {
-                    type.accept(new RefinementTypeChecker(c, factory));
-                });
-            } catch (LJError e) {
-                diagnostics.add(e);
+        Context c = Context.getInstance();
+        c.reinitializeAllContext();
+        processPackage(pkg, c);
+    }
+
+    private void processPackage(CtPackage pkg, Context c) {
+        try {
+            // first pass: gather refinements
+            pkg.getTypes().forEach(type -> {
+                type.accept(new FieldGhostsGeneration(c, factory));
+                type.accept(new ExternalRefinementTypeChecker(c, factory));
+                type.accept(new MethodsFirstChecker(c, factory));
+            });
+
+            // second pass: check refinements
+            pkg.getTypes().forEach(type -> {
+                type.accept(new RefinementTypeChecker(c, factory));
+            });
+
+            // recurse into sub-packages (inheriting context)
+            for (CtPackage subPkg : pkg.getPackages()) {
+                processPackage(subPkg, c);
             }
+        } catch (LJError e) {
+            diagnostics.add(e);
         }
     }
 }