diff --git a/ulib/FStar.ModifiesGen.fst b/ulib/FStar.ModifiesGen.fst
index dbbf9505fc4..aff7d02cb6b 100644
--- a/ulib/FStar.ModifiesGen.fst
+++ b/ulib/FStar.ModifiesGen.fst
@@ -1799,7 +1799,7 @@ let union_loc_of_loc_addresses #al c b preserve_liveness r n =
 let union_loc_of_loc_regions #al c b preserve_liveness r =
   assert (loc_equal #_ #(cls_union c) (union_loc_of_loc c b (loc_regions #_ #(c b) preserve_liveness r)) (loc_regions #_ #(cls_union c) preserve_liveness r))
 
-#push-options "--z3rlimit 25"
+#push-options "--z3rlimit 30"
 let union_loc_of_loc_includes_intro
   (#al: (bool -> HS.rid -> nat -> Tot Type))
   (c: ((b: bool) -> Tot (cls (al b))))