verifies

cryspen · Sep 29, 2024 · de52651 · de52651
1 parent 101ed40
commit de52651
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst
@@ -85,7 +85,7 @@ let sub (lhs rhs: Libcrux_intrinsics.Avx2_extract.t_Vec256) =
   in
   result
 
-#push-options "--z3rlimit 200"
+#push-options "--z3rlimit 200 --split_queries always"
 
 let barrett_reduce (vector: Libcrux_intrinsics.Avx2_extract.t_Vec256) =
   let t0:Libcrux_intrinsics.Avx2_extract.t_Vec256 =