From 07daa6c39632d6bf0e604f3a4fbc46ffc056f6b6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 24 Apr 2026 16:23:07 -0700
Subject: [PATCH 1/5] Add Z3 4.16.0 and default to it

---
 .github/workflows/nightly-ci.yml               |  4 ++--
 .nix/z3.nix                                    |  2 ++
 .nix/z3_4_16_0.nix                             | 11 +++++++++++
 .scripts/get_fstar_z3.sh                       |  7 ++++++-
 .scripts/package_z3.sh                         |  2 +-
 INSTALL.md                                     | 12 ++++++------
 fstar.opam                                     |  2 +-
 pulse/src/checker/PulseChecker.fst.config.json |  2 --
 src/basic/FStarC.Find.Z3.fst                   |  2 +-
 src/basic/FStarC.Options.fst                   |  4 ++--
 10 files changed, 32 insertions(+), 16 deletions(-)
 create mode 100644 .nix/z3_4_16_0.nix

diff --git a/.github/workflows/nightly-ci.yml b/.github/workflows/nightly-ci.yml
index be89802baba..a2e8df1498e 100644
--- a/.github/workflows/nightly-ci.yml
+++ b/.github/workflows/nightly-ci.yml
@@ -34,7 +34,7 @@ jobs:
       # don't include Z3.
       - uses: cda-tum/setup-z3@main
         with:
-          version: 4.13.3
+          version: 4.16.0
 
       - run: tar xzf fstar.tar.gz
 
@@ -59,7 +59,7 @@ jobs:
     steps:
       - uses: cda-tum/setup-z3@main
         with:
-          version: 4.13.3
+          version: 4.16.0
 
       - name: Get fstar package
         uses: actions/download-artifact@v8
diff --git a/.nix/z3.nix b/.nix/z3.nix
index 5a2d38a7bef..eee0de9c72e 100644
--- a/.nix/z3.nix
+++ b/.nix/z3.nix
@@ -4,6 +4,7 @@ let
   z3_4_8_5 = callPackage (import ./z3_4_8_5.nix) { };
   z3_4_13_3 = callPackage (import ./z3_4_13_3.nix) { };
   z3_4_15_3 = callPackage (import ./z3_4_15_3.nix) { };
+  z3_4_16_0 = callPackage (import ./z3_4_16_0.nix) { };
 in
 stdenv.mkDerivation {
   pname = "fstar-z3";
@@ -16,5 +17,6 @@ stdenv.mkDerivation {
     ln -s ${z3_4_8_5}/bin/z3 $out/bin/z3-4.8.5
     ln -s ${z3_4_13_3}/bin/z3 $out/bin/z3-4.13.3
     ln -s ${z3_4_15_3}/bin/z3 $out/bin/z3-4.15.3
+    ln -s ${z3_4_16_0}/bin/z3 $out/bin/z3-4.16.0
   '';
 }
diff --git a/.nix/z3_4_16_0.nix b/.nix/z3_4_16_0.nix
new file mode 100644
index 00000000000..afcced7dce3
--- /dev/null
+++ b/.nix/z3_4_16_0.nix
@@ -0,0 +1,11 @@
+{ fetchFromGitHub, z3 }:
+
+z3.overrideAttrs (old: rec {
+  version = "4.16.0";
+  src = fetchFromGitHub {
+    owner = "z3prover";
+    repo = "z3";
+    rev = "z3-${version}";
+    sha256 = "sha256-DnhX3kxggnFmyYwXEPBsBA1rh4oor1oIJR5TMJk/jvc=";
+  };
+})
diff --git a/.scripts/get_fstar_z3.sh b/.scripts/get_fstar_z3.sh
index 8fc82f697bf..5bf736f1aa0 100755
--- a/.scripts/get_fstar_z3.sh
+++ b/.scripts/get_fstar_z3.sh
@@ -27,6 +27,11 @@ release_url=(
   "Darwin-x86_64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-x64-osx-13.7.6.zip"
   "Darwin-aarch64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-arm64-osx-13.7.6.zip"
   "Windows-x86_64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-x64-win.zip"
+  "Linux-x86_64-4.16.0":"https://github.com/Z3Prover/z3/releases/download/z3-4.16.0/z3-4.16.0-x64-glibc-2.39.zip"
+  "Linux-aarch64-4.16.0":"https://github.com/Z3Prover/z3/releases/download/z3-4.16.0/z3-4.16.0-arm64-glibc-2.38.zip"
+  "Darwin-x86_64-4.16.0":"https://github.com/Z3Prover/z3/releases/download/z3-4.16.0/z3-4.16.0-x64-osx-15.7.3.zip"
+  "Darwin-aarch64-4.16.0":"https://github.com/Z3Prover/z3/releases/download/z3-4.16.0/z3-4.16.0-arm64-osx-15.7.3.zip"
+  "Windows-x86_64-4.16.0":"https://github.com/Z3Prover/z3/releases/download/z3-4.16.0/z3-4.16.0-x64-win.zip"
 )
 
 get_url() {
@@ -146,7 +151,7 @@ fi
 
 mkdir -p "$dest_dir"
 
-for z3_ver in 4.8.5 4.13.3 4.15.3; do
+for z3_ver in 4.8.5 4.13.3 4.15.3 4.16.0; do
   destination_file_name="$dest_dir/z3-$z3_ver"
   if [ "$kernel" = Windows ]; then destination_file_name="$destination_file_name.exe"; fi
 
diff --git a/.scripts/package_z3.sh b/.scripts/package_z3.sh
index fea51d174b8..d83891cad71 100755
--- a/.scripts/package_z3.sh
+++ b/.scripts/package_z3.sh
@@ -19,7 +19,7 @@ inst1 () {
 	cp "$1" "$TGT"
 }
 
-for dir in z3-4.8.5 z3-4.13.3 z3-4.15.3; do
+for dir in z3-4.8.5 z3-4.13.3 z3-4.15.3 z3-4.16.0; do
   inst1 ./$dir/bin/z3
   inst1 ./$dir/LICENSE.txt
   for dll in ./$dir/bin/*dll; do
diff --git a/INSTALL.md b/INSTALL.md
index c866301516b..852c973b55a 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -28,14 +28,14 @@ using the [online F\* editor] that's part of the [F\* tutorial].
 
 F\* requires specific versions of Z3 to work correctly,
 and will refuse to run if the version string does not match.
-You should have `z3-4.8.5` and `z3-4.13.3` in your `$PATH`:
+You should have `z3-4.13.3` and `z3-4.16.0` in your `$PATH`:
 
 ```
-❯ z3-4.8.5 --version
-Z3 version 4.8.5 - 64 bit
-
 ❯ z3-4.13.3 --version
 Z3 version 4.13.3 - 64 bit
+
+❯ z3-4.16.0 --version
+Z3 version 4.16.0 - 64 bit
 ```
 
 On Linux you can install these two versions with the following command:
@@ -93,8 +93,8 @@ need to perform the following step before your first use:
         compiler=OCaml 4.14.0
         date=yyyy-mm-ddThh:nn:ss+02:00
         commit=xxxxxxxx
-        $ z3-4.13.3 --version
-        Z3 version 4.13.3 - 64 bit
+        $ z3-4.16.0 --version
+        Z3 version 4.16.0 - 64 bit
 
    Note: if you are using the binary package and extracted it to, say, the
    `/path/to/fstar` directory, then both `fstar.exe` and the right version of
diff --git a/fstar.opam b/fstar.opam
index ae4807e9ec7..16e5c303557 100644
--- a/fstar.opam
+++ b/fstar.opam
@@ -37,7 +37,7 @@ install: [
 post-messages: [
   """
 F* requires specific versions of Z3 to work correctly, and will refuse to run
-if the version string does not match. You should have z3-4.8.5 and z3-4.13.3
+if the version string does not match. You should have z3-4.13.3 and z3-4.16.0
 in your $PATH. For details, see
 https://github.com/FStarLang/FStar/blob/master/INSTALL.md#runtime-dependency-particular-version-of-z3.
 """ {success}
diff --git a/pulse/src/checker/PulseChecker.fst.config.json b/pulse/src/checker/PulseChecker.fst.config.json
index 3d3aadee744..0889ad75e6b 100644
--- a/pulse/src/checker/PulseChecker.fst.config.json
+++ b/pulse/src/checker/PulseChecker.fst.config.json
@@ -6,8 +6,6 @@
     "optimize_let_vc",
     "--ext",
     "fly_deps",
-    "--z3version",
-    "4.13.3",
     "--smtencoding.elim_box",
     "true",
     "--z3smtopt",
diff --git a/src/basic/FStarC.Find.Z3.fst b/src/basic/FStarC.Find.Z3.fst
index c626fefe151..253c9569b4a 100644
--- a/src/basic/FStarC.Find.Z3.fst
+++ b/src/basic/FStarC.Find.Z3.fst
@@ -25,7 +25,7 @@ open FStarC.Class.Show
 
 let z3url = "https://github.com/Z3Prover/z3/releases"
 
-let packaged_z3_versions = ["4.8.5"; "4.13.3"; "4.15.3"]
+let packaged_z3_versions = ["4.8.5"; "4.13.3"; "4.15.3"; "4.16.0"]
 
 let z3_install_suggestion (v : string) : list Pprint.document =
   let open FStarC.Errors.Msg in
diff --git a/src/basic/FStarC.Options.fst b/src/basic/FStarC.Options.fst
index e75873a3ee2..d564776b57c 100644
--- a/src/basic/FStarC.Options.fst
+++ b/src/basic/FStarC.Options.fst
@@ -328,7 +328,7 @@ let defaults = [
   ("z3rlimit"                                  , Int 5);
   ("z3seed"                                    , Int 0);
   ("z3smtopt"                                  , List []);
-  ("z3version"                                 , String "4.13.3");
+  ("z3version"                                 , String "4.16.0");
 ]
 
 let init () =
@@ -1584,7 +1584,7 @@ let specs_with_types warn_unsafe : ML (list (char & string & opt_type & Pprint.d
   ( noshort,
     "z3version",
     SimpleStr "version",
-    text "Set the version of Z3 that is to be used. Default: 4.13.3");
+    text "Set the version of Z3 that is to be used. Default: 4.16.0");
 
   ( noshort,
     "__no_positivity",

From 4e461730acc0583d343b669b58cf440c2c15560a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 24 Apr 2026 16:47:11 -0700
Subject: [PATCH 2/5] Fix SMT regressions

---
 examples/layeredeffects/Sec2.HIFC.fst             |  2 ++
 pulse/lib/core/PulseCore.IndirectionTheorySep.fst |  6 ++++--
 pulse/lib/pulse/lib/Pulse.Lib.Swap.Array.fst      |  2 +-
 ulib/FStar.BitVector.fst                          | 11 ++++-------
 ulib/FStar.UInt128.fst                            |  2 ++
 5 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/examples/layeredeffects/Sec2.HIFC.fst b/examples/layeredeffects/Sec2.HIFC.fst
index f5e9e31b8ea..ff680a60475 100644
--- a/examples/layeredeffects/Sec2.HIFC.fst
+++ b/examples/layeredeffects/Sec2.HIFC.fst
@@ -837,8 +837,10 @@ let test8 (l:lref) (h:href)
     write l (x + 1)
 
 effect IFC (a:Type) (w r:label) (fs:flows) = HIFC a w r fs (fun _ -> True) (fun _ _ _ -> True)
+
 let test_cond (l:lref) (h:href) (b:bool)
   : IFC unit (union (single h) (single l)) (single l) [single h, single l]
+    by (Tactics.compute()) // Weird that this is now needed
   = if b then write l (read h) else write l (read l + 1)
 
 //But, using the Hoare refinements, we can recover precision and remove
diff --git a/pulse/lib/core/PulseCore.IndirectionTheorySep.fst b/pulse/lib/core/PulseCore.IndirectionTheorySep.fst
index b5573af68f7..45e770551cf 100644
--- a/pulse/lib/core/PulseCore.IndirectionTheorySep.fst
+++ b/pulse/lib/core/PulseCore.IndirectionTheorySep.fst
@@ -108,9 +108,11 @@ let slprop = p:mem_pred { slprop_ok p }
 let mk_slprop (p: premem -> prop { slprop_ok' p }) : slprop =
   reveal_slprop_ok (); F.on_dom _ p
 
+#push-options "--z3rlimit 30"
 let age_to (m: mem) (n: erased nat) : mem =
   reveal_mem_le (); reveal_slprop_ok ();
   age_to_ m n
+#pop-options
 
 irreducible [@@"opaque_to_smt"]
 let reveal_mem (m: erased premem) (h: B.mem { h == timeless_heap_of m }) : m': premem { m' == reveal m } =
@@ -362,7 +364,7 @@ let star_elim (p1 p2: slprop) (w: premem { star p1 p2 w }) :
   star__elim p1 p2 w
 
 #restart-solver
-#push-options "--split_queries always"
+#push-options "--split_queries always --z3rlimit 20"
 irreducible
 let star_elim' (p1 p2: slprop) (w: mem { star p1 p2 w }) :
     GTot (w':(mem & mem) { disjoint_mem w'._1 w'._2 /\ w == join_premem w'._1 w'._2 /\ p1 w'._1 /\ p2 w'._2 }) =
@@ -1453,4 +1455,4 @@ let implies' (p q: slprop) : prop =
 let loeb (p: slprop { implies' (later p) p }) : squash (implies' emp p) =
   let rec aux (m: premem) : Lemma (ensures p m) (decreases level_ m) =
     if level_ m > 0 then aux (age1_ m) else () in
-  introduce forall m. p m with aux m
\ No newline at end of file
+  introduce forall m. p m with aux m
diff --git a/pulse/lib/pulse/lib/Pulse.Lib.Swap.Array.fst b/pulse/lib/pulse/lib/Pulse.Lib.Swap.Array.fst
index fe5eb6b0732..f7ac6da8e4d 100644
--- a/pulse/lib/pulse/lib/Pulse.Lib.Swap.Array.fst
+++ b/pulse/lib/pulse/lib/Pulse.Lib.Swap.Array.fst
@@ -48,7 +48,7 @@ let size_sub
 
 #restart-solver
 
-#push-options "--z3rlimit_factor 8"
+#push-options "--z3rlimit_factor 12"
 
 inline_for_extraction noextract [@@noextract_to "krml"]
 
diff --git a/ulib/FStar.BitVector.fst b/ulib/FStar.BitVector.fst
index 3527e33e4a0..ddf176ade52 100644
--- a/ulib/FStar.BitVector.fst
+++ b/ulib/FStar.BitVector.fst
@@ -122,18 +122,15 @@ let rotate_left_vec_lemma (#n: pos) (a: bv_t n) (s: nat) (i: nat{i < n})
     : Lemma (ensures index (rotate_left_vec #n a s) i = index a ((i + s) % n))
       [SMTPat (index (rotate_left_vec #n a s) i)] =
   let s' = s % n in
-  if s' = 0 then ()
-  else if i < n - s' then ()
-  else ()
+  Math.Lemmas.modulo_add n i s' s;
+  ()
 
 (** Relating the indexes of the rotated right vector to the original *)
 let rotate_right_vec_lemma (#n: pos) (a: bv_t n) (s: nat) (i: nat{i < n})
     : Lemma (ensures index (rotate_right_vec #n a s) i = index a ((i + n - (s % n)) % n))
       [SMTPat (index (rotate_right_vec #n a s) i)] =
-  let s' = s % n in
-  if s' = 0 then ()
-  else if i < s' then ()
-  else ()
+  (* Somehow trivial, unlike the above? *)
+  ()
 
 (** Rotate left by n is identity *)
 let rotate_left_vec_full_identity (#n: pos) (a: bv_t n)
diff --git a/ulib/FStar.UInt128.fst b/ulib/FStar.UInt128.fst
index 68f9cc9f8dc..d6e71c0c498 100644
--- a/ulib/FStar.UInt128.fst
+++ b/ulib/FStar.UInt128.fst
@@ -181,6 +181,7 @@ let carry (a b: U64.t) : Pure U64.t
 let carry_sum_ok (a b:U64.t) :
   Lemma (U64.v (carry (U64.add_mod a b) b) == (U64.v a + U64.v b) / (pow2 64)) = ()
 
+#push-options "--z3rlimit 20"
 let add (a b: t) : Pure t
   (requires (v a + v b < pow2 128))
   (ensures (fun r -> v a + v b = v r)) =
@@ -188,6 +189,7 @@ let add (a b: t) : Pure t
   carry_sum_ok a.low b.low;
   { low = l;
     high = U64.add (U64.add a.high b.high) (carry l b.low); }
+#pop-options
 
 let add_underspec (a b: t) =
     let l = U64.add_mod a.low b.low in

From 8e3bd840b04526ca2f7c9f92b726264798653b8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 24 Apr 2026 17:13:43 -0700
Subject: [PATCH 3/5] Stop shipping 4.8.5

---
 .nix/z3.nix                  |  1 -
 .nix/z3_4_8_5.nix            | 46 ------------------------------------
 .scripts/get_fstar_z3.sh     | 14 +----------
 .scripts/package_z3.sh       |  2 +-
 src/basic/FStarC.Find.Z3.fst |  2 +-
 5 files changed, 3 insertions(+), 62 deletions(-)
 delete mode 100644 .nix/z3_4_8_5.nix

diff --git a/.nix/z3.nix b/.nix/z3.nix
index eee0de9c72e..a3cb65037d3 100644
--- a/.nix/z3.nix
+++ b/.nix/z3.nix
@@ -14,7 +14,6 @@ stdenv.mkDerivation {
 
   buildPhase = ''
     mkdir -p $out/bin
-    ln -s ${z3_4_8_5}/bin/z3 $out/bin/z3-4.8.5
     ln -s ${z3_4_13_3}/bin/z3 $out/bin/z3-4.13.3
     ln -s ${z3_4_15_3}/bin/z3 $out/bin/z3-4.15.3
     ln -s ${z3_4_16_0}/bin/z3 $out/bin/z3-4.16.0
diff --git a/.nix/z3_4_8_5.nix b/.nix/z3_4_8_5.nix
deleted file mode 100644
index 00bd45387ca..00000000000
--- a/.nix/z3_4_8_5.nix
+++ /dev/null
@@ -1,46 +0,0 @@
-{
-  autoPatchelfHook,
-  fetchzip,
-  fixDarwinDylibNames,
-  lib,
-  stdenv,
-}:
-
-let
-  platform = if stdenv.isDarwin then "osx-10.14.2" else "ubuntu-16.04";
-  hash =
-    if stdenv.isDarwin then
-      "sha256-Bz5Bsg+0Bsshne/VN0dGeesOibI6yUfh3s+wiDNhwHM="
-    else
-      "sha256-dgG4L77Y3+g10tO2pygmJ+XeGOhJrzuDxIzuZyJvMf0=";
-
-in
-stdenv.mkDerivation rec {
-  pname = "z3";
-  version = "4.8.5";
-
-  src = fetchzip {
-    inherit hash;
-    url = "https://github.com/Z3Prover/z3/releases/download/Z3-${version}/z3-${version}-x64-${platform}.zip";
-  };
-
-  nativeBuildInputs =
-    lib.optionals stdenv.hostPlatform.isLinux [ autoPatchelfHook ]
-    ++ lib.optionals stdenv.hostPlatform.isDarwin [ fixDarwinDylibNames ];
-
-  buildInputs = [ stdenv.cc.cc.lib ];
-
-  installPhase = ''
-    runHook preInstall
-    mkdir -p $out
-    cp -r bin $out
-    runHook postInstall
-  '';
-
-  meta = with lib; {
-    description = "High-performance theorem prover and SMT solver";
-    mainProgram = "z3";
-    homepage = "https://github.com/Z3Prover/z3";
-    platforms = platforms.unix;
-  };
-}
diff --git a/.scripts/get_fstar_z3.sh b/.scripts/get_fstar_z3.sh
index 5bf736f1aa0..e94fda9a597 100755
--- a/.scripts/get_fstar_z3.sh
+++ b/.scripts/get_fstar_z3.sh
@@ -151,7 +151,7 @@ fi
 
 mkdir -p "$dest_dir"
 
-for z3_ver in 4.8.5 4.13.3 4.15.3 4.16.0; do
+for z3_ver in 4.13.3 4.15.3 4.16.0; do
   destination_file_name="$dest_dir/z3-$z3_ver"
   if [ "$kernel" = Windows ]; then destination_file_name="$destination_file_name.exe"; fi
 
@@ -159,18 +159,6 @@ for z3_ver in 4.8.5 4.13.3 4.15.3 4.16.0; do
     echo ">>> Z3 $z3_ver already downloaded to $destination_file_name"
   else
     key="$kernel-$arch-$z3_ver"
-
-    case "$key" in
-      Linux-aarch64-4.8.5)
-        echo ">>> Z3 4.8.5 is not available for aarch64, downloading x86_64 version.  You need to install qemu-user (and shared libraries) to execute it."
-        key="$kernel-x86_64-$z3_ver"
-        ;;
-      Darwin-aarch64-4.8.5)
-        echo ">>> Z3 4.8.5 is not available for aarch64, downloading x86_64 version.  You need to install Rosetta 2 to execute it."
-        key="$kernel-x86_64-$z3_ver"
-        ;;
-    esac
-
     url="$(get_url "$key")"
 
     if [ -z "$url" ]; then
diff --git a/.scripts/package_z3.sh b/.scripts/package_z3.sh
index d83891cad71..527158bf1f3 100755
--- a/.scripts/package_z3.sh
+++ b/.scripts/package_z3.sh
@@ -19,7 +19,7 @@ inst1 () {
 	cp "$1" "$TGT"
 }
 
-for dir in z3-4.8.5 z3-4.13.3 z3-4.15.3 z3-4.16.0; do
+for dir in z3-4.13.3 z3-4.15.3 z3-4.16.0; do
   inst1 ./$dir/bin/z3
   inst1 ./$dir/LICENSE.txt
   for dll in ./$dir/bin/*dll; do
diff --git a/src/basic/FStarC.Find.Z3.fst b/src/basic/FStarC.Find.Z3.fst
index 253c9569b4a..2a7813933f8 100644
--- a/src/basic/FStarC.Find.Z3.fst
+++ b/src/basic/FStarC.Find.Z3.fst
@@ -25,7 +25,7 @@ open FStarC.Class.Show
 
 let z3url = "https://github.com/Z3Prover/z3/releases"
 
-let packaged_z3_versions = ["4.8.5"; "4.13.3"; "4.15.3"; "4.16.0"]
+let packaged_z3_versions = ["4.13.3"; "4.15.3"; "4.16.0"]
 
 let z3_install_suggestion (v : string) : list Pprint.document =
   let open FStarC.Errors.Msg in

From 0775edafb0565bab0c6374387360818c4dc0a58d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 24 Apr 2026 17:18:20 -0700
Subject: [PATCH 4/5] get_fstar_z3: remove hardcoded table, query releases

---
 .scripts/get_fstar_z3.sh | 54 +++++++++++++++++++---------------------
 1 file changed, 25 insertions(+), 29 deletions(-)

diff --git a/.scripts/get_fstar_z3.sh b/.scripts/get_fstar_z3.sh
index e94fda9a597..ad7b844bb58 100755
--- a/.scripts/get_fstar_z3.sh
+++ b/.scripts/get_fstar_z3.sh
@@ -11,37 +11,34 @@ esac
 arch="$(uname -m)"
 case "$arch" in
   arm64) arch=aarch64 ;;
+  # ^ normalize macOS arm64 to Linux's aarch64
 esac
 
-release_url=(
-  "Linux-x86_64-4.8.5":"https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip"
-  "Darwin-x86_64-4.8.5":"https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-osx-10.14.2.zip"
-  "Windows-x86_64-4.8.5":"https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-win.zip"
-  "Linux-x86_64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-glibc-2.35.zip"
-  "Linux-aarch64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-arm64-glibc-2.34.zip"
-  "Darwin-x86_64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-osx-13.7.zip"
-  "Darwin-aarch64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-arm64-osx-13.7.zip"
-  "Windows-x86_64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-win.zip"
-  "Linux-x86_64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-x64-glibc-2.39.zip"
-  "Linux-aarch64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-arm64-glibc-2.34.zip"
-  "Darwin-x86_64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-x64-osx-13.7.6.zip"
-  "Darwin-aarch64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-arm64-osx-13.7.6.zip"
-  "Windows-x86_64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-x64-win.zip"
-  "Linux-x86_64-4.16.0":"https://github.com/Z3Prover/z3/releases/download/z3-4.16.0/z3-4.16.0-x64-glibc-2.39.zip"
-  "Linux-aarch64-4.16.0":"https://github.com/Z3Prover/z3/releases/download/z3-4.16.0/z3-4.16.0-arm64-glibc-2.38.zip"
-  "Darwin-x86_64-4.16.0":"https://github.com/Z3Prover/z3/releases/download/z3-4.16.0/z3-4.16.0-x64-osx-15.7.3.zip"
-  "Darwin-aarch64-4.16.0":"https://github.com/Z3Prover/z3/releases/download/z3-4.16.0/z3-4.16.0-arm64-osx-15.7.3.zip"
-  "Windows-x86_64-4.16.0":"https://github.com/Z3Prover/z3/releases/download/z3-4.16.0/z3-4.16.0-x64-win.zip"
-)
-
 get_url() {
-  local key elem
-  key="$1"
+  local version="$1" z3_arch os_pattern
+
+  case "$arch" in
+    x86_64)  z3_arch="x64" ;;
+    aarch64) z3_arch="arm64" ;;
+    *)       z3_arch="$arch" ;;
+  esac
+
+  case "$kernel" in
+    Linux)   os_pattern="(glibc|ubuntu)" ;;
+    Darwin)  os_pattern="osx" ;;
+    Windows) os_pattern="win" ;;
+    *)       return ;;
+  esac
 
-  for elem in "${release_url[@]}"; do
-    if [ "${elem%%:*}" = "$key" ]; then
-      echo -n "${elem#*:}"
-      break
+  local tag url
+  for tag in "z3-$version" "Z3-$version"; do
+    url=$(curl -s "https://api.github.com/repos/Z3Prover/z3/releases/tags/$tag" \
+      | grep -oP '"browser_download_url":\s*"\K[^"]+' \
+      | grep -E "z3-${version}-${z3_arch}-${os_pattern}[^/]*\.zip$" \
+      | tail -1)
+    if [ -n "$url" ]; then
+      echo -n "$url"
+      return
     fi
   done
 }
@@ -158,8 +155,7 @@ for z3_ver in 4.13.3 4.15.3 4.16.0; do
   if [ -f "$destination_file_name" ]; then
     echo ">>> Z3 $z3_ver already downloaded to $destination_file_name"
   else
-    key="$kernel-$arch-$z3_ver"
-    url="$(get_url "$key")"
+    url="$(get_url "$z3_ver")"
 
     if [ -z "$url" ]; then
       echo ">>> Z3 $z3_ver not available for this architecture, skipping..."

From 3942890d08b651bc82c752026ce3fd988cc4e09c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 24 Apr 2026 17:56:25 -0700
Subject: [PATCH 5/5] Update ci.yml

---
 .github/workflows/ci.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 425541268a7..013e3cc55f9 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -30,6 +30,9 @@ jobs:
           path: FStar
           submodules: true
 
+      - name: Install Z3 from script
+        run: sudo ./FStar/.scripts/get_fstar_z3.sh /usr/local/bin
+
       - name: Run CI
         run: make -skj$(nproc) ci
         working-directory: FStar