diff --git a/lib_avl_mono/Impl.Trees.Types.fst b/lib_avl_mono/Impl.Trees.Types.fst
index 6b89a1a..d8605ba 100644
--- a/lib_avl_mono/Impl.Trees.Types.fst
+++ b/lib_avl_mono/Impl.Trees.Types.fst
@@ -57,6 +57,7 @@ val init_avl_scs (slab_region: array U8.t)
   )
 
 open Mman
+#push-options "--z3rlimit 20"
 let init_avl_scs (slab_region: array U8.t)
   =
   let md_bm_region_size = US.mul metadata_max 4sz in
@@ -65,6 +66,7 @@ let init_avl_scs (slab_region: array U8.t)
   let md_region = mmap_cell_status_init md_region_size in
   let scs = init_struct_aux sc_avl slab_region md_bm_region md_region in
   return scs
+#pop-options
 
 module L = Steel.SpinLock
 
diff --git a/src/Main.Meta.fst b/src/Main.Meta.fst
index 923d6d1..f7a4515 100644
--- a/src/Main.Meta.fst
+++ b/src/Main.Meta.fst
@@ -394,7 +394,7 @@ let mod_lemma
 #pop-options
 
 
-#push-options "--fuel 1 --ifuel 1 --z3rlimit 200"
+#push-options "--fuel 1 --ifuel 1 --z3rlimit 250"
 /// `slab_aligned_alloc` works in a very similar way as `slab_malloc_i`
 /// The key difference lies in the condition of the if-branch: we only
 /// attempt to allocate in this size class if it satisfies the alignment