bump rlimits, hints

cryspen · Feb 1, 2024 · 4f584c0 · 4f584c0
1 parent 4e198b0
commit 4f584c0
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Serialize.fst.hints b/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Serialize.fst.hints
@@ -1,5 +1,5 @@
 [
-  "\u0006�\\u�\u0016%\u0018\u001b\u0002w\u0006��v)",
+  "[1\u001d-p\u001a69��5z\u00106��",
   [
     [
       "Libcrux.Kem.Kyber.Serialize.int_arr_bitwise_eq",
@@ -8011,7 +8011,7 @@
         "typing_tok_Lib.IntTypes.U8@tok"
       ],
       0,
-      "a6b0fff7dfca38a6f6126a4623df7712"
+      "cf4275373c55a87f388b992affdd1fd4"
     ],
     [
       "Libcrux.Kem.Kyber.Serialize.serialize_uncompressed_ring_element",

diff --git a/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Serialize.fst b/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Serialize.fst
@@ -1284,7 +1284,7 @@ let deserialize_then_decompress_ring_element_v v_COMPRESSION_FACTOR serialized =
   admit(); //P-F
   res
 
-#push-options "--z3rlimit 160"
+#push-options "--z3rlimit 220"
 let deserialize_to_uncompressed_ring_element (serialized: t_Slice u8) = 
   let _:Prims.unit = () <: Prims.unit in
   let re:Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement =
@@ -1335,7 +1335,7 @@ let deserialize_to_uncompressed_ring_element (serialized: t_Slice u8) =
   in
   re
 #pop-options
-  
+
 #push-options "--z3rlimit 100"
 let serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement) =
   let serialized:t_Array u8 (sz 384) = Rust_primitives.Hax.repeat 0uy (sz 384) in