rlimit

src/3d/prelude/Actions.fst

@@ -1321,6 +1321,8 @@ let validate_string
   LP.parser_kind_prop_equiv k p;
   validate_weaken (validate_list_up_to v r terminator (fun _ _ _ -> ())) _
 
+#restart-solver
+
 inline_for_extraction noextract
 let validate_all_bytes2 : validate_with_action_t parse_all_bytes true_inv eloc_none true =
   fun #inputLength input startPosition ->

src/3d/prelude/EverParse3d.Readable.fst

@@ -161,6 +161,8 @@ let unreadable_split_1
   ()
 #pop-options
 
+#push-options "--z3rlimit 16"
+#restart-solver
 let unreadable_split_2
   (h: HS.mem)
   (#t: _) (#b: B.buffer t) (p: perm b)
@@ -172,6 +174,7 @@ let unreadable_split_2
   (ensures (unreadable h p from to))
 = Seq.lemma_split (B.as_seq h (B.gsub b from (to `U32.sub` from))) (U32.v mid - U32.v from);
   if F.model then Seq.lemma_split (B.as_seq h (B.gsub (p <: perm' b) from (to `U32.sub` from))) (U32.v mid - U32.v from)
+#pop-options
 
 let unreadable_split h #t #b p from mid to =
   Classical.move_requires (unreadable_split_1 h p from mid) to;