diff --git a/.gitignore b/.gitignore
index fcff2132d..cc1c2a754 100644
--- a/.gitignore
+++ b/.gitignore
@@ -59,8 +59,8 @@ src/api/dotnet/Enumerations.cs
 src/api/dotnet/Native.cs
 src/api/dotnet/Properties/AssemblyInfo.cs
 src/api/dotnet/Microsoft.Z3.xml
-src/api/python/z3consts.py
-src/api/python/z3core.py
+src/api/python/z3/z3consts.py
+src/api/python/z3/z3core.py
 src/ast/pattern/database.h
 src/util/version.h
 src/api/java/Native.cpp
diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/contrib/cmake/src/api/python/CMakeLists.txt
index 555333c9f..6babb2069 100644
--- a/contrib/cmake/src/api/python/CMakeLists.txt
+++ b/contrib/cmake/src/api/python/CMakeLists.txt
@@ -9,7 +9,6 @@ set(z3py_files
   z3poly.py
   z3printer.py
   z3rcf.py
-  z3test.py
   z3types.py
   z3util.py
 )
@@ -18,12 +17,12 @@ set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}")
 
 set(build_z3_python_bindings_target_depends "")
 foreach (z3py_file ${z3py_files})
-  add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${z3py_file}"
+  add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/${z3py_file}"
     COMMAND "${CMAKE_COMMAND}" "-E" "copy"
-      "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
-      "${z3py_bindings_build_dest}"
-    DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
-    COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}"
+      "${CMAKE_CURRENT_SOURCE_DIR}/z3/${z3py_file}"
+      "${z3py_bindings_build_dest}/z3.py"
+    DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/z3/${z3py_file}"
+    COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}/z3.py/${z3py_file}"
   )
   list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/${z3py_file}")
 endforeach()
diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py
index cbeb8a82d..2ecb06776 100644
--- a/scripts/mk_genfile_common.py
+++ b/scripts/mk_genfile_common.py
@@ -98,7 +98,7 @@ def mk_z3consts_py_internal(api_files, output_dir):
     openbrace_pat  = re.compile("{ *")
     closebrace_pat = re.compile("}.*;")
 
-    z3consts  = open(os.path.join(output_dir, 'z3consts.py'), 'w')
+    z3consts  = open(os.path.join(output_dir, 'z3/z3consts.py'), 'w')
     z3consts_output_path = z3consts.name
     z3consts.write('# Automatically generated file\n\n')
     for api_file in api_files:
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 66191e160..0d1555e5b 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2737,6 +2737,8 @@ def mk_def_files():
 
 def cp_z3py_to_build():
     mk_dir(BUILD_DIR)
+    z3py_dest = os.path.join(BUILD_DIR, 'z3.py')
+    z3py_src = os.path.join(Z3PY_SRC_DIR, 'z3')
     # Erase existing .pyc files
     for root, dirs, files in os.walk(Z3PY_SRC_DIR):
         for f in files:
@@ -2746,20 +2748,19 @@ def cp_z3py_to_build():
     if compileall.compile_dir(Z3PY_SRC_DIR, force=1) != 1:
         raise MKException("failed to compile Z3Py sources")
     # Copy sources to build
-    for py in filter(lambda f: f.endswith('.py'), os.listdir(Z3PY_SRC_DIR)):
-        shutil.copyfile(os.path.join(Z3PY_SRC_DIR, py), os.path.join(BUILD_DIR, py))
-        if is_verbose():
-            print("Copied '%s'" % py)
+    shutil.copytree(z3py_src, z3py_dest)
+    if is_verbose():
+        print("Copied python bindings")
     # Python 2.x support
-    for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(Z3PY_SRC_DIR)):
-        shutil.copyfile(os.path.join(Z3PY_SRC_DIR, pyc), os.path.join(BUILD_DIR, pyc))
+    for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(z3py_src)):
+        shutil.copyfile(os.path.join(z3py_src, pyc), os.path.join(z3py_dest, pyc))
         if is_verbose():
             print("Generated '%s'" % pyc)
     # Python 3.x support
-    src_pycache = os.path.join(Z3PY_SRC_DIR, '__pycache__')
+    src_pycache = os.path.join(z3py_src, '__pycache__')
     if os.path.exists(src_pycache):
         for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(src_pycache)):
-            target_pycache = os.path.join(BUILD_DIR, '__pycache__')
+            target_pycache = os.path.join(z3py_dest, '__pycache__')
             mk_dir(target_pycache)
             shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc))
             if is_verbose():
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 5295b19b1..047564cde 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1706,7 +1706,7 @@ def generate_files(api_files,
   with mk_file_or_temp(api_output_dir, 'api_log_macros.h') as log_h:
     with mk_file_or_temp(api_output_dir, 'api_log_macros.cpp') as log_c:
       with mk_file_or_temp(api_output_dir, 'api_commands.cpp') as exe_c:
-        with mk_file_or_temp(z3py_output_dir, 'z3core.py') as core_py:
+        with mk_file_or_temp(z3py_output_dir, 'z3/z3core.py') as core_py:
           # Write preambles
           write_log_h_preamble(log_h)
           write_log_c_preamble(log_c)
diff --git a/src/api/python/setup.py b/src/api/python/setup.py
new file mode 100644
index 000000000..9d17f431f
--- /dev/null
+++ b/src/api/python/setup.py
@@ -0,0 +1,88 @@
+import os
+import sys
+import platform
+import subprocess
+import multiprocessing
+from setuptools import setup
+from distutils.errors import LibError
+from distutils.command.build import build as _build
+from setuptools.command.develop import develop as _develop
+
+
+build_env = dict(os.environ)
+build_env['PYTHON'] = sys.executable
+build_env['CXXFLAGS'] = "-std=c++11"
+
+build_dir = os.path.abspath(os.path.dirname(__file__))
+
+if sys.platform == 'darwin':
+    library_file = "libz3.dylib"
+elif sys.platform == 'win32':
+    library_file = "libz3.dll"
+else:
+    library_file = "libz3.so"
+
+def _configure_z3():
+    if sys.platform == 'win32':
+        args = [sys.executable, os.path.join(build_dir, 'scripts',
+                                             'mk_make.py')]
+        if platform.architecture()[0] == '64bit':
+            args += ['-x']
+
+        if subprocess.call(args, env=build_env, cwd=build_dir) != 0:
+            raise LibError("Unable to configure Z3.")
+    else:   # linux and osx
+        if subprocess.call([os.path.join(build_dir, 'configure')],
+                    env=build_env, cwd=build_dir) != 0:
+            raise LibError("Unable to configure Z3.")
+
+def _build_z3():
+    if sys.platform == 'win32':
+        if subprocess.call(['nmake'], env=build_env,
+                           cwd=os.path.join(build_dir, 'build')) != 0:
+            raise LibError("Unable to build Z3.")
+    else:   # linux and osx
+        if subprocess.call(['make', '-C', os.path.join(build_dir, 'build'),
+                            '-j', str(multiprocessing.cpu_count())],
+                    env=build_env, cwd=build_dir) != 0:
+            raise LibError("Unable to build Z3.")
+
+class build(_build):
+    def run(self):
+        self.execute(_configure_z3, (), msg="Configuring Z3")
+        self.execute(_build_z3, (), msg="Building Z3")
+
+class develop(_develop):
+    def run(self):
+        self.execute(_configure_z3, (), msg="Configuring Z3")
+        self.execute(_build_z3, (), msg="Building Z3")
+
+# the build directory needs to exist
+try: os.makedirs(os.path.join(build_dir, 'build'))
+except OSError: pass
+
+setup(
+    name='angr-only-z3-custom',
+    version='4.4.1.post4',
+    description='pip installable distribution of The Z3 Theorem Prover, for use with angr. Please send all support requests to angr@lists.cs.ucsb.edu!',
+    long_description='Z3 is a theorem prover from Microsoft Research. This version is slightly modified by the angr project to enable installation via pip, making it unsupportable by the Z3 project. Please direct all support requests to angr@lists.cs.ucsb.edu!',
+    author="The Z3 Theorem Prover Project",
+    maintainer="Yan Shoshitaishvili",
+    maintainer_email="yans@yancomm.net",
+    url='https://github.com/angr/angr-z3',
+    license='MIT License',
+    keywords=['z3', 'smt', 'sat', 'prover', 'theorem'],
+    package_dir={'': 'build'},
+    packages=[''],
+    data_files=[
+        ('lib', (os.path.join(build_dir, 'build', library_file),)),
+        ('include', tuple(os.path.join(build_dir, f) for f in ('src/api/z3.h',
+                     'src/api/z3_v1.h', 'src/api/z3_macros.h',
+                     'src/api/z3_api.h', 'src/api/z3_algebraic.h',
+                     'src/api/z3_polynomial.h', 'src/api/z3_rcf.h',
+                     'src/api/z3_interp.h', 'src/api/z3_fpa.h',
+                     'src/api/c++/z3++.h') )),
+    ],
+    #scripts=[os.path.join(build_dir, 'build', 'z3')] if sys.version_info[0] == 2 else [],
+    cmdclass={'build': build, 'develop': develop},
+)
diff --git a/src/api/python/z3/__init__.py b/src/api/python/z3/__init__.py
index c4f08371f..f7aa29ab1 100644
--- a/src/api/python/z3/__init__.py
+++ b/src/api/python/z3/__init__.py
@@ -1,10 +1,12 @@
 from .z3 import *
 
-from . import z3core
 from . import z3num
 from . import z3poly
 from . import z3printer
 from . import z3rcf
 from . import z3types
 from . import z3util
+
+# generated files
+from . import z3core
 from . import z3consts
diff --git a/src/api/python/z3/z3poly.py b/src/api/python/z3/z3poly.py
index 4a5cac46c..169944291 100644
--- a/src/api/python/z3/z3poly.py
+++ b/src/api/python/z3/z3poly.py
@@ -5,6 +5,7 @@
 #
 # Author: Leonardo de Moura (leonardo)
 ############################################
+
 from .z3 import *
 
 def subresultants(p, q, x):
@@ -32,6 +33,3 @@ if __name__ == "__main__":
     import doctest
     if doctest.testmod().failed:
         exit(1)
-
-
-    
diff --git a/src/api/python/z3/z3types.py b/src/api/python/z3/z3types.py
index 8b585e0ee..7cf61f49e 100644
--- a/src/api/python/z3/z3types.py
+++ b/src/api/python/z3/z3types.py
@@ -121,4 +121,3 @@ class FuncEntryObj(ctypes.c_void_p):
 class RCFNumObj(ctypes.c_void_p):
   def __init__(self, e): self._as_parameter_ = e
   def from_param(obj): return obj
-