9 files changed, 16 insertions, 21 deletions
diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix
index 6165cfe8bd22..26848e1397aa 100644
--- a/pkgs/applications/science/logic/z3/default.nix
+++ b/pkgs/applications/science/logic/z3/default.nix
@@ -24,7 +24,7 @@ let common = { version, sha256, patches ? [ ], tag ? "z3" }:
     inherit version sha256 patches;
     src = fetchFromGitHub {
       owner = "Z3Prover";
-      repo = pname;
+      repo = "z3";
       rev = "${tag}-${version}";
       sha256 = sha256;
     };
diff --git a/pkgs/development/compilers/solc/default.nix b/pkgs/development/compilers/solc/default.nix
index 986f6f169e8b..0603706164ae 100644
--- a/pkgs/development/compilers/solc/default.nix
+++ b/pkgs/development/compilers/solc/default.nix
@@ -86,7 +86,7 @@ let
     buildInputs = [ boost ]
       ++ lib.optionals z3Support [ z3 ]
       ++ lib.optionals cvc4Support [ cvc4 cln gmp ];
-    nativeCheckInputs = [ jq ncurses (python3.withPackages (ps: with ps; [ colorama deepdiff devtools docopt docutils requests sphinx tabulate z3 ])) ]; # contextlib2 glob2 textwrap3 traceback2 urllib3
+    nativeCheckInputs = [ jq ncurses (python3.withPackages (ps: with ps; [ colorama deepdiff devtools docopt docutils requests sphinx tabulate z3-solver ])) ]; # contextlib2 glob2 textwrap3 traceback2 urllib3
 
     # tests take 60+ minutes to complete, only run as part of passthru tests
     doCheck = false;
diff --git a/pkgs/development/interpreters/acl2/default.nix b/pkgs/development/interpreters/acl2/default.nix
index 9953eaa3144c..bf37d19cd8c4 100644
--- a/pkgs/development/interpreters/acl2/default.nix
+++ b/pkgs/development/interpreters/acl2/default.nix
@@ -50,7 +50,7 @@ in stdenv.mkDerivation rec {
     which perl hostname
     # Some of the books require one or more of these external tools:
     glucose minisat abc-verifier libipasir
-    z3 (python3.withPackages (ps: [ ps.z3 ]))
+    z3 (python3.withPackages (ps: [ ps.z3-solver ]))
   ];
 
   # NOTE: Parallel building can be memory-intensive depending on the number of
diff --git a/pkgs/development/python-modules/claripy/default.nix b/pkgs/development/python-modules/claripy/default.nix
index c343f7f3e872..fb0c8dbdf297 100644
--- a/pkgs/development/python-modules/claripy/default.nix
+++ b/pkgs/development/python-modules/claripy/default.nix
@@ -8,7 +8,7 @@
 , pysmt
 , pythonOlder
 , pytestCheckHook
-, z3
+, z3-solver
 }:
 
 buildPythonPackage rec {
@@ -34,19 +34,13 @@ buildPythonPackage rec {
     decorator
     future
     pysmt
-    z3
+    z3-solver
   ];
 
   nativeCheckInputs = [
     pytestCheckHook
   ];
 
-  postPatch = ''
-    # Use upstream z3 implementation
-    substituteInPlace setup.cfg \
-      --replace "z3-solver==4.10.2.0" ""
-  '';
-
   pythonImportsCheck = [
     "claripy"
   ];
diff --git a/pkgs/development/python-modules/deal-solver/default.nix b/pkgs/development/python-modules/deal-solver/default.nix
index 5c91d6d92559..28eee72a99d2 100644
--- a/pkgs/development/python-modules/deal-solver/default.nix
+++ b/pkgs/development/python-modules/deal-solver/default.nix
@@ -3,7 +3,7 @@
 , fetchFromGitHub
 , pythonOlder
 , flit-core
-, z3
+, z3-solver
 , astroid
 , pytestCheckHook
 , hypothesis
@@ -28,9 +28,7 @@ buildPythonPackage rec {
   ];
 
   postPatch = ''
-    # Use upstream z3 implementation
     substituteInPlace pyproject.toml \
-      --replace "\"z3-solver\"," "" \
       --replace "\"--cov=deal_solver\"," "" \
       --replace "\"--cov-report=html\"," "" \
       --replace "\"--cov-report=xml\"," "" \
@@ -39,9 +37,9 @@ buildPythonPackage rec {
   '';
 
   propagatedBuildInputs = [
-    z3
+    z3-solver
     astroid
-  ] ++ z3.requiredPythonModules;
+  ] ++ z3-solver.requiredPythonModules;
 
   nativeCheckInputs = [
     pytestCheckHook
diff --git a/pkgs/development/python-modules/qiskit-terra/default.nix b/pkgs/development/python-modules/qiskit-terra/default.nix
index 2c290493b063..0bd411883627 100644
--- a/pkgs/development/python-modules/qiskit-terra/default.nix
+++ b/pkgs/development/python-modules/qiskit-terra/default.nix
@@ -33,7 +33,7 @@
 , seaborn
   # Crosstalk-adaptive layout pass
 , withCrosstalkPass ? false
-, z3
+, z3-solver
   # test requirements
 , ddt
 , hypothesis
@@ -53,7 +53,7 @@ let
     pylatexenc
     seaborn
   ];
-  crosstalkPackages = [ z3 ];
+  crosstalkPackages = [ z3-solver ];
 in
 
 buildPythonPackage rec {
diff --git a/pkgs/tools/security/amoco/default.nix b/pkgs/tools/security/amoco/default.nix
index a9c182ca4cbc..fe16ad9596dd 100644
--- a/pkgs/tools/security/amoco/default.nix
+++ b/pkgs/tools/security/amoco/default.nix
@@ -36,7 +36,7 @@ python3.pkgs.buildPythonApplication rec {
       prompt-toolkit
       pygments
       # pyside6
-      z3
+      z3-solver
     ];
   };
 
diff --git a/pkgs/top-level/python-aliases.nix b/pkgs/top-level/python-aliases.nix
index 39ba30a93b7d..b76adc80e765 100644
--- a/pkgs/top-level/python-aliases.nix
+++ b/pkgs/top-level/python-aliases.nix
@@ -462,6 +462,7 @@ mapAliases ({
   xenomapper = throw "xenomapper was moved to pkgs.xenomapper"; # added 2021-12-31
   XlsxWriter = xlsxwriter; # added 2023-02-19
   Yapsy = yapsy; # added 2023-02-19
+  z3 = z3-solver; # added 2023-12-03
   zake = throw "zake has been removed because it is abandoned"; # added 2023-06-20
   zc-buildout221 = zc-buildout; # added 2021-07-21
   zc_buildout_nix = throw "zc_buildout_nix was pinned to a version no longer compatible with other modules";
diff --git a/pkgs/top-level/python-packages.nix b/pkgs/top-level/python-packages.nix
index d285a37393a6..27f8fa89b5d9 100644
--- a/pkgs/top-level/python-packages.nix
+++ b/pkgs/top-level/python-packages.nix
@@ -16113,9 +16113,11 @@ self: super: with self; {
 
   z3c-checkversions = callPackage ../development/python-modules/z3c-checkversions { };
 
-  z3 = (toPythonModule (pkgs.z3.override {
+  z3-solver = (toPythonModule ((pkgs.z3.override {
     inherit python;
-  })).python;
+  }).overrideAttrs (_: {
+    pname = "z3-solver";
+  }))).python;
 
   zadnegoale = callPackage ../development/python-modules/zadnegoale { };