diff --git a/proof/Makefile b/proof/Makefile
index 18d4a5c84..c5b2f8a89 100644
--- a/proof/Makefile
+++ b/proof/Makefile
@@ -23,7 +23,7 @@ report-regression:
 #
 
 # Refine heaps.
-HEAPS += AInvs BaseRefine Refine
+HEAPS += AInvs BaseRefine BaseRefine2 Refine
 
 # CRefine heaps.
 HEAPS += CKernel CSpec CBaseRefine CRefine
diff --git a/proof/ROOT b/proof/ROOT
index 2ee3414ec..12be36a06 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -37,6 +37,15 @@ session Refine = BaseRefine +
   theories
     "refine/$L4V_ARCH/Refine"
 
+session BaseRefine2 = BaseRefine +
+  description {* Intermediate point in refinement proof. Useful for machines with small RAM. *}
+  theories [condition = "SKIP_INVS_PROOFS", quick_and_dirty, skip_proofs]
+    "refine/$L4V_ARCH/Untyped_R"
+    "refine/$L4V_ARCH/Schedule_R"
+  theories
+   "refine/$L4V_ARCH/Untyped_R"
+   "refine/$L4V_ARCH/Schedule_R"
+
 session BaseRefine = AInvs +
   description {* Background theory and libraries for refinement proof. *}
   theories [condition = "SKIP_INVS_PROOFS", quick_and_dirty, skip_proofs]