wip: extraction fix?

Inria-Prosecco · Apr 4, 2024 · 9a342f6 · 9a342f6
1 parent e8c6d99
commit 9a342f6
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/src/Main.Meta.fst b/src/Main.Meta.fst
@@ -145,16 +145,20 @@ 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
     arena_sizes.x
     arena_sizes.y
     arena_sizes.z
     arena_sizes.w
-    nb_arenas
+    nb_arenas)
     slab_region
     md_bm_region
     md_bm_region_b