From d25878d52a97c535732f7a5424a2ee25dcded8b7 Mon Sep 17 00:00:00 2001
From: Antonin Reitz <antonin.reitz@inria.fr>
Date: Fri, 5 Jul 2024 11:56:38 +0200
Subject: [PATCH] CI: bump rlimit

---
 src/SizeClassSelection.fst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/SizeClassSelection.fst b/src/SizeClassSelection.fst
index 860f706..21623c8 100644
--- a/src/SizeClassSelection.fst
+++ b/src/SizeClassSelection.fst
@@ -761,7 +761,7 @@ let inv_exact_log2 (k: nat)
   assert (r < pow2 (k1 + 6 + 1));
   log2u64_spec_eq_lemma r (k1 + 6)
 
-#push-options "--z3rlimit 30"
+#push-options "--z3rlimit 50"
 let inv_exact_aux2 (k: nat)
   : Lemma
   (requires 1 <= k /\ k <= 24)