diff --git a/math/Makefile b/math/Makefile
index e812be2c5af7..26e46b5b1b2e 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -736,6 +736,7 @@
     SUBDIR += py-uncertainties
     SUBDIR += py-viper
     SUBDIR += py-yt
+    SUBDIR += py-z3-solver
     SUBDIR += qalculate
     SUBDIR += qd
     SUBDIR += qhull
diff --git a/math/py-z3-solver/Makefile b/math/py-z3-solver/Makefile
new file mode 100644
index 000000000000..d2106bd49e55
--- /dev/null
+++ b/math/py-z3-solver/Makefile
@@ -0,0 +1,25 @@
+# $FreeBSD$
+
+PORTNAME=	z3-solver
+DISTVERSIONPREFIX=	z3-
+DISTVERSION=	4.7.1
+CATEGORIES=	math
+PKGNAMEPREFIX=	${PYTHON_PKGNAMEPREFIX}
+
+MAINTAINER=	yuri@FreeBSD.org
+COMMENT=	Python binding for Z3 Theorem Prover
+
+LICENSE=	MIT
+LICENSE_FILE=	${WRKSRC}/../../../LICENSE.txt
+
+# CAVEAT: It should have LIB_DEPENDS=libz3.so:math/z3, but currently it rebuilds all code, see https://github.com/Z3Prover/z3/issues/1767
+
+USES=		python
+USE_GITHUB=	yes
+GH_ACCOUNT=	Z3Prover
+GH_PROJECT=	z3
+USE_PYTHON=	distutils autoplist
+
+WRKSRC_SUBDIR=	src/api/python
+
+.include <bsd.port.mk>
diff --git a/math/py-z3-solver/distinfo b/math/py-z3-solver/distinfo
new file mode 100644
index 000000000000..3e54a3a9cce4
--- /dev/null
+++ b/math/py-z3-solver/distinfo
@@ -0,0 +1,3 @@
+TIMESTAMP = 1529241358
+SHA256 (Z3Prover-z3-z3-4.7.1_GH0.tar.gz) = a353e3da00cdaffd258052cc1406efc854606855222ab4bfd5679c58af5c11c7
+SIZE (Z3Prover-z3-z3-4.7.1_GH0.tar.gz) = 4015416
diff --git a/math/py-z3-solver/files/patch-setup.py b/math/py-z3-solver/files/patch-setup.py
new file mode 100644
index 000000000000..af13eec6c882
--- /dev/null
+++ b/math/py-z3-solver/files/patch-setup.py
@@ -0,0 +1,12 @@
+--- setup.py.orig	2018-07-21 19:34:29 UTC
++++ setup.py
+@@ -161,9 +161,5 @@ setup(
+     keywords=['z3', 'smt', 'sat', 'prover', 'theorem'],
+     packages=['z3'],
+     include_package_data=True,
+-    package_data={
+-        'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')]
+-    },
+-    data_files=[('bin',[os.path.join('bin',EXECUTABLE_FILE)])],
+     cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_egg': bdist_egg},
+ )
diff --git a/math/py-z3-solver/pkg-descr b/math/py-z3-solver/pkg-descr
new file mode 100644
index 000000000000..9bddb9d30bec
--- /dev/null
+++ b/math/py-z3-solver/pkg-descr
@@ -0,0 +1,4 @@
+Python binding for Z3, a high-performance theorem prover developed
+at Microsoft Research.
+
+WWW: https://github.com/Z3Prover/z3
diff --git a/math/z3/Makefile b/math/z3/Makefile
index b3bee277e150..48a97ff18401 100644
--- a/math/z3/Makefile
+++ b/math/z3/Makefile
@@ -3,6 +3,7 @@
 PORTNAME=	z3
 DISTVERSIONPREFIX=	${PORTNAME}-
 DISTVERSION=	4.7.1
+PORTREVISION=	1
 CATEGORIES=	math
 
 MAINTAINER=	arrowd@FreeBSD.org
@@ -11,25 +12,17 @@ COMMENT=	Z3 Theorem Prover
 LICENSE=	MIT
 LICENSE_FILE=	${WRKSRC}/LICENSE.txt
 
-# compiler picks ${LOCALBASE}/include/dictionary.h from iniparser
-CONFLICTS=		iniparser-*
-
+USES=		python:2.7,build
 USE_GITHUB=	yes
 GH_ACCOUNT=	Z3Prover
 
-OPTIONS_DEFINE=		DEBUG STATIC PYTHON GMP
+OPTIONS_DEFINE=		DEBUG STATIC GMP
 
-OPTIONS_DEFAULT=	STATIC PYTHON
+OPTIONS_DEFAULT=	STATIC
 OPTIONS_SUB=		yes
 
 DEBUG_CONFIGURE_ON=	--debug
 
-PYTHON_DESC=		Enable python bindings
-PYTHON_CONFIGURE_ON=	--python
-PYTHON_USES=		python:2.7
-PYTHON_USES_OFF=	python:2.7,build
-PYTHON_RUN_DEPENDS=	${PYTHON_PKGNAMEPREFIX}setuptools>0:devel/py-setuptools@${PY_FLAVOR}
-
 STATIC_DESC=		Build static z3 library
 STATIC_CONFIGURE_ON=	--staticlib
 
diff --git a/math/z3/pkg-plist b/math/z3/pkg-plist
index 67095dc03f5c..44cb7828d1db 100644
--- a/math/z3/pkg-plist
+++ b/math/z3/pkg-plist
@@ -16,24 +16,3 @@ include/z3_v1.h
 %%STATIC%%lib/libz3.a
 lib/libz3.so
 lib/libz3.so.0
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/__init__.py
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/__init__.pyc
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/lib/libz3.so
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3.py
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3.pyc
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3consts.py
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3consts.pyc
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3core.py
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3core.pyc
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3num.py
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3num.pyc
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3poly.py
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3poly.pyc
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3printer.py
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3printer.pyc
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3rcf.py
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3rcf.pyc
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3types.py
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3types.pyc
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3util.py
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/z3/z3util.pyc