chore: update F*, fix random breakage

Inria-Prosecco · Dec 19, 2023 · f0b3d59 · f0b3d59
1 parent 191476e
commit f0b3d59
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 6 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/hacl-star-snapshot/lib/Lib.IntTypes.fst b/hacl-star-snapshot/lib/Lib.IntTypes.fst
@@ -1010,6 +1010,7 @@ let conditional_subtract #t #l t' a =
   logand_lemma mask pow2_bits;
   a3 `add` (mask `logand` pow2_bits)
 
+#push-options "--z3rlimit 500 --quake 1/25"
 let cast_mod #t #l t' l' a =
   assert_norm (pow2 7 = 128);
   assert_norm (pow2 15 = 32768);
@@ -1022,6 +1023,7 @@ let cast_mod #t #l t' l' a =
     let b = conditional_subtract t' (a `logand` mod_mask m) in
     cast t' l' b
     end
+#pop-options
 
 #pop-options