rlimit bump on a pure lemma in Quicksort.Base

FStarLang · Feb 19, 2024 · 248a967 · 248a967
1 parent e54dc0d
commit 248a967
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/share/pulse/examples/Quicksort.Base.fst b/share/pulse/examples/Quicksort.Base.fst
@@ -305,6 +305,7 @@ let transfer_larger_slice
   assert (forall (k: int). l - shift <= k /\ k < r - shift ==> (lb <= Seq.index s k));
   ()
 
+#push-options "--z3rlimit_factor 4 --split_queries no"
 let transfer_smaller_slice
   (s : Seq.seq int)
   (shift : nat)
@@ -321,6 +322,7 @@ let transfer_smaller_slice
   assert (forall (k: int). l - shift <= k /\ k < r - shift ==> (Seq.index s k <= rb));
   ()
 #pop-options
+#pop-options
 
 let transfer_equal_slice
   (s : Seq.seq int)