diff --git a/flake.lock b/flake.lock
index aacd9821..61dd4b88 100644
--- a/flake.lock
+++ b/flake.lock
@@ -10,11 +10,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1701726077,
-        "narHash": "sha256-Jl9/L/kUyDlW944pbBNC54CRY6IR/STw3kJaEhSesIw=",
+        "lastModified": 1726600332,
+        "narHash": "sha256-JYYCFIR4MgjGjpxnp/2Yr2fySTj/d/hTlCAwxhtFacM=",
         "owner": "TWal",
         "repo": "comparse",
-        "rev": "717b7d127b4ec6a63c347f3ac78820cf6838ea52",
+        "rev": "66471ca6f8d31c33c02e96684468121e920f1460",
         "type": "github"
       },
       "original": {
@@ -46,11 +46,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1721552334,
-        "narHash": "sha256-FDfp4JquvP5e4obYdG7hpe5hwMOTxYwe4ArtNXKHvcY=",
+        "lastModified": 1727737011,
+        "narHash": "sha256-B875NYwASSMUvVEieG7aXm1xQ/z7I9rCSSwaJlzT1A4=",
         "owner": "FStarLang",
         "repo": "FStar",
-        "rev": "e5cef6f266ece8a8b55ef4cd9b61cdf103520d38",
+        "rev": "061fcdf98085ac5e195773a3f20764637cc7cab3",
         "type": "github"
       },
       "original": {
diff --git a/src/core/DY.Core.Bytes.fst b/src/core/DY.Core.Bytes.fst
index 6128b8e2..b97cea46 100644
--- a/src/core/DY.Core.Bytes.fst
+++ b/src/core/DY.Core.Bytes.fst
@@ -2173,6 +2173,7 @@ let dh_pk_preserves_publishability tr sk =
 
 /// Lemma for attacker knowledge theorem.
 
+#push-options "--z3rlimit 25"
 val dh_preserves_publishability:
   {|crypto_invariants|} -> tr:trace ->
   sk:bytes -> pk:bytes ->
@@ -2187,6 +2188,7 @@ let dh_preserves_publishability tr sk pk =
   reveal_opaque (`%dh) (dh);
   normalize_term_spec bytes_invariant;
   normalize_term_spec get_label
+#pop-options
 
 /// User lemma (dh_pk well-formedness)
 
@@ -2642,6 +2644,7 @@ let kem_pk_preserves_publishability #ci tr sk =
 
 /// Lemma for attacker knowledge theorem.
 
+#push-options "--z3rlimit 25"
 val kem_encap_preserves_publishability:
   {|crypto_invariants|} -> tr:trace ->
   pk:bytes -> nonce:bytes ->
@@ -2660,6 +2663,7 @@ let kem_encap_preserves_publishability #ci tr pk nonce =
   normalize_term_spec bytes_invariant;
   normalize_term_spec get_label;
   assert(is_publishable tr (KemSecretShared nonce))
+#pop-options
 
 /// Lemma for attacker knowledge theorem.
 
diff --git a/src/lib/hpke/DY.Lib.HPKE.Lemmas.fst b/src/lib/hpke/DY.Lib.HPKE.Lemmas.fst
index 42064a7c..beb05330 100644
--- a/src/lib/hpke/DY.Lib.HPKE.Lemmas.fst
+++ b/src/lib/hpke/DY.Lib.HPKE.Lemmas.fst
@@ -236,7 +236,7 @@ let get_hpke_sk_label_hpke_pk #cu tr sk = ()
 /// It is a bit more complex than `DY.Core.Bytes.bytes_invariant_pk_enc`,
 /// the additional complexity is explained in the comments.
 
-#push-options "--ifuel 2"
+#push-options "--ifuel 2 --z3rlimit 25"
 val bytes_invariant_hpke_enc:
   {|crypto_invariants|} -> {|hpke_crypto_invariants|} ->
   tr:trace ->