diff --git a/src/Main.Meta.fst b/src/Main.Meta.fst
index 8c0a1cdc..d51c47d6 100644
--- a/src/Main.Meta.fst
+++ b/src/Main.Meta.fst
@@ -145,8 +145,12 @@ let init
   let md_bm_region_b = mmap_bool_init (US.mul arena_sizes.z nb_arenas) in
   let md_region = mmap_cell_status_init (US.mul arena_sizes.w nb_arenas) in
   let size_classes = mmap_sc_init (US.mul nb_size_classes nb_arenas) in
+  Pervasives.norm
+  [
+    zeta; delta_only [`%init_n_first_arenas]
 
-  init_all_arenas
+  ]
+  (init_all_arenas
     sc_list_sc sc_list_ex
     nb_size_classes_sc nb_size_classes_sc_ex
     nb_size_classes
@@ -154,7 +158,7 @@ let init
     arena_sizes.y
     arena_sizes.z
     arena_sizes.w
-    nb_arenas
+    nb_arenas)
     slab_region
     md_bm_region
     md_bm_region_b