python3Packages.z3-solver: rename from z3

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;
     };

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;

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

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"
   ];

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

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 {

pkgs/tools/security/amoco/default.nix

@@ -36,7 +36,7 @@ python3.pkgs.buildPythonApplication rec {
       prompt-toolkit
       pygments
       # pyside6
-      z3
+      z3-solver
     ];
   };
 

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";

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 { };