diff --git a/pkgs/applications/science/logic/z3/0001-fix-2131.patch b/pkgs/applications/science/logic/z3/0001-fix-2131.patch
deleted file mode 100644
index 0b21b8fffd40..000000000000
--- a/pkgs/applications/science/logic/z3/0001-fix-2131.patch
+++ /dev/null
@@ -1,66 +0,0 @@
-From c5df6ce96e068eceb77019e48634721c6a5bb607 Mon Sep 17 00:00:00 2001
-From: Nikolaj Bjorner <nbjorner@microsoft.com>
-Date: Sun, 10 Feb 2019 10:07:24 -0800
-Subject: [PATCH 1/1] fix #2131
-
-Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
----
- src/api/python/README.txt    | 10 +++-------
- src/api/python/setup.py      |  2 +-
- src/ast/recfun_decl_plugin.h |  2 +-
- 3 files changed, 5 insertions(+), 9 deletions(-)
-
-diff --git a/src/api/python/README.txt b/src/api/python/README.txt
-index 9312b1119..561b8dedc 100644
---- a/src/api/python/README.txt
-+++ b/src/api/python/README.txt
-@@ -1,8 +1,4 @@
--You can learn more about Z3Py at:
--http://rise4fun.com/Z3Py/tutorial/guide
--
--On Windows, you must build Z3 before using Z3Py.
--To build Z3, you should executed the following command
-+On Windows, to build Z3, you should executed the following command
- in the Z3 root directory at the Visual Studio Command Prompt
- 
-        msbuild /p:configuration=external
-@@ -12,8 +8,8 @@ If you are using a 64-bit Python interpreter, you should use
-        msbuild /p:configuration=external /p:platform=x64
- 
- 
--On Linux and macOS, you must install Z3Py, before trying example.py.
--To install Z3Py on Linux and macOS, you should execute the following
-+On Linux and macOS, you must install python bindings, before trying example.py.
-+To install python on Linux and macOS, you should execute the following
- command in the Z3 root directory
- 
-         sudo make install-z3py
-diff --git a/src/api/python/setup.py b/src/api/python/setup.py
-index 2a750fee6..063680e2b 100644
---- a/src/api/python/setup.py
-+++ b/src/api/python/setup.py
-@@ -178,7 +178,7 @@ setup(
-     name='z3-solver',
-     version=_z3_version(),
-     description='an efficient SMT solver library',
--    long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compiliation, or installation, please submit issues to https://github.com/angr/angr-z3',
-+    long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compilation, or installation, please submit issues to https://github.com/angr/angr-z3',
-     author="The Z3 Theorem Prover Project",
-     maintainer="Audrey Dutcher",
-     maintainer_email="audrey@rhelmot.io",
-diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
-index 0247335e8..b294cdfce 100644
---- a/src/ast/recfun_decl_plugin.h
-+++ b/src/ast/recfun_decl_plugin.h
-@@ -56,7 +56,7 @@ namespace recfun {
-         friend class def;
-         func_decl_ref       m_pred; //<! predicate used for this case
-         expr_ref_vector     m_guards; //<! conjunction that is equivalent to this case
--        expr_ref            m_rhs; //<! if guard is true, `f(t1…tn) = rhs` holds
-+        expr_ref            m_rhs; //<! if guard is true, `f(t1...tn) = rhs` holds
-         def *               m_def; //<! definition this is a part of
-         bool                m_immediate; //<! does `rhs` contain no defined_fun/case_pred?
- 
--- 
-2.19.2
-
diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix
index 8c1c0ca23024..14f75fb68b5e 100644
--- a/pkgs/applications/science/logic/z3/default.nix
+++ b/pkgs/applications/science/logic/z3/default.nix
@@ -1,20 +1,16 @@
 { stdenv, fetchFromGitHub, python, fixDarwinDylibNames }:
 
 stdenv.mkDerivation rec {
-  name = "z3-${version}";
-  version = "4.8.4";
+  pname = "z3";
+  version = "4.8.5";
 
   src = fetchFromGitHub {
     owner  = "Z3Prover";
-    repo   = "z3";
-    rev    = name;
-    sha256 = "014igqm5vwswz0yhz0cdxsj3a6dh7i79hvhgc3jmmmz3z0xm1gyn";
+    repo   = pname;
+    rev    = "Z3-${version}";
+    sha256 = "11sy98clv7ln0a5vqxzvh6wwqbswsjbik2084hav5kfws4xvklfa";
   };
 
-  patches = [
-    ./0001-fix-2131.patch
-  ];
-
   buildInputs = [ python fixDarwinDylibNames ];
   propagatedBuildInputs = [ python.pkgs.setuptools ];
   enableParallelBuilding = true;