From 191476e387bc921d5501a9a5b903cc391c280bd4 Mon Sep 17 00:00:00 2001
From: TWal <theophile@wallez.net>
Date: Thu, 9 Nov 2023 13:47:30 +0100
Subject: [PATCH] chore: update F*

---
 flake.lock                              | 6 +++---
 hacl-star-snapshot/lib/Lib.IntTypes.fst | 3 ++-
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/flake.lock b/flake.lock
index 721002d..2eb7c96 100644
--- a/flake.lock
+++ b/flake.lock
@@ -62,11 +62,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1699461354,
-        "narHash": "sha256-zlsXb3fgPXivG60P5QcKXZlckyCCtZDCqqgUyEgqiqc=",
+        "lastModified": 1699492431,
+        "narHash": "sha256-cvvHenyduboy7s+dO0h2WR2GwgEIMLtMXgrkYv/kY8o=",
         "owner": "FStarLang",
         "repo": "FStar",
-        "rev": "2a40e707d8a81ad3add6598b17d9050c1e78f22f",
+        "rev": "e27ee69276e9385eb9080ac4c8f5f6a7f37e72da",
         "type": "github"
       },
       "original": {
diff --git a/hacl-star-snapshot/lib/Lib.IntTypes.fst b/hacl-star-snapshot/lib/Lib.IntTypes.fst
index ad7959e..59aaedb 100644
--- 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 =