From ee06439c43fdcafbecf098e7d7f8ce1e06da09ac Mon Sep 17 00:00:00 2001
From: sempiternal-aurora
 <78790545+sempiternal-aurora@users.noreply.github.com>
Date: Thu, 5 Feb 2026 22:03:20 +0800
Subject: [PATCH] z3: version macos compat patches

patches fix a bug only present in the latest versions of z3
fixes the vampire build, which requires an older version of z3
---
 pkgs/by-name/z3/z3/package.nix | 47 ++++++++++++++++++----------------
 1 file changed, 25 insertions(+), 22 deletions(-)

diff --git a/pkgs/by-name/z3/z3/package.nix b/pkgs/by-name/z3/z3/package.nix
index 3b93c40f9bc7..c68a8dfeb7b1 100644
--- a/pkgs/by-name/z3/z3/package.nix
+++ b/pkgs/by-name/z3/z3/package.nix
@@ -38,28 +38,31 @@ stdenv.mkDerivation (finalAttrs: {
     hash = "sha256-eyF3ELv81xEgh9Km0Ehwos87e4VJ82cfsp53RCAtuTo=";
   };
 
-  patches = lib.optionals useCmakeBuild [
-    ./fix-pkg-config-paths.patch
-    # fix Segmentation fault. See https://github.com/Z3Prover/z3/pull/8264 and
-    # https://github.com/NixOS/nixpkgs/issues/486491
-    (fetchpatch2 {
-      name = "preserve-the-initial-state-of-the-solver.patch";
-      url = "https://github.com/Z3Prover/z3/commit/850a3236adab92f9f6f569ac66ffbb69be179f4c.patch?full_index=1";
-      hash = "sha256-C6p+dj3i3DpOnd2wr+R8ZwClHoMFfk5i5/+JRhTDNcs=";
-    })
-    # needs to include a cosmetic change to apply patch for memory corruption
-    (fetchpatch2 {
-      name = "cosmetic-changes-to-i.patch";
-      url = "https://github.com/Z3Prover/z3/commit/243694379475d983605f87578452a330f3e3b28f.patch?full_index=1";
-      includes = [ "src/api/api_polynomial.cpp" ];
-      hash = "sha256-huo5S73WrFrEEUcaP+1LDQwGwo+n2iYT4x/OjK5rmqQ=";
-    })
-    (fetchpatch2 {
-      name = "fix-memory-corruption.patch";
-      url = "https://github.com/Z3Prover/z3/commit/e7b6f3f33bcc6c88a0f2ace47ff2f09b59239433.patch?full_index=1";
-      hash = "sha256-kEEeod4s8i9SI2e2TFD2U4yd1qEPoGnJOfE0y+1Cq6M=";
-    })
-  ];
+  patches =
+    lib.optionals useCmakeBuild [
+      ./fix-pkg-config-paths.patch
+    ]
+    ++ lib.optionals (lib.versionAtLeast finalAttrs.version "4.15.4") [
+      # fix Segmentation fault. See https://github.com/Z3Prover/z3/pull/8264 and
+      # https://github.com/NixOS/nixpkgs/issues/486491
+      (fetchpatch2 {
+        name = "preserve-the-initial-state-of-the-solver.patch";
+        url = "https://github.com/Z3Prover/z3/commit/850a3236adab92f9f6f569ac66ffbb69be179f4c.patch?full_index=1";
+        hash = "sha256-C6p+dj3i3DpOnd2wr+R8ZwClHoMFfk5i5/+JRhTDNcs=";
+      })
+      # needs to include a cosmetic change to apply patch for memory corruption
+      (fetchpatch2 {
+        name = "cosmetic-changes-to-i.patch";
+        url = "https://github.com/Z3Prover/z3/commit/243694379475d983605f87578452a330f3e3b28f.patch?full_index=1";
+        includes = [ "src/api/api_polynomial.cpp" ];
+        hash = "sha256-huo5S73WrFrEEUcaP+1LDQwGwo+n2iYT4x/OjK5rmqQ=";
+      })
+      (fetchpatch2 {
+        name = "fix-memory-corruption.patch";
+        url = "https://github.com/Z3Prover/z3/commit/e7b6f3f33bcc6c88a0f2ace47ff2f09b59239433.patch?full_index=1";
+        hash = "sha256-kEEeod4s8i9SI2e2TFD2U4yd1qEPoGnJOfE0y+1Cq6M=";
+      })
+    ];
 
   strictDeps = true;