chore: update F*

Inria-Prosecco · Nov 9, 2023 · 191476e · 191476e
1 parent e4ab9fa
commit 191476e
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 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
@@ -101,6 +101,8 @@ assume
 val int64_to_int128: a:Int64.t -> b:Int128.t{Int128.v b == Int64.v a}
 //let int64_to_int128 a = Int128.int_to_t (v a)
 
+#push-options "--z3rlimit 1000"
+
 val uint64_to_int128: a:UInt64.t -> b:Int128.t{Int128.v b == UInt64.v a}
 let uint64_to_int128 a = uint128_to_int128 (Int.Cast.Full.uint64_to_uint128 a)
 
@@ -110,7 +112,6 @@ let int64_to_uint128 a = int128_to_uint128 (int64_to_int128 a)
 val int128_to_uint64: a:Int128.t -> b:UInt64.t{UInt64.v b == Int128.v a % pow2 64}
 let int128_to_uint64 a = Int.Cast.Full.uint128_to_uint64 (int128_to_uint128 a)
 
-#push-options "--z3rlimit 1000"
 
 [@(strict_on_arguments [0;2])]
 let cast #t #l t' l' u =