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/examples/CMakeLists.txt b/contrib/cmake/examples/CMakeLists.txt
index 49ea72fdc..e596ed3dd 100644
--- a/contrib/cmake/examples/CMakeLists.txt
+++ b/contrib/cmake/examples/CMakeLists.txt
@@ -1,3 +1,4 @@
 add_subdirectory(c)
 add_subdirectory(c++)
 add_subdirectory(tptp)
+add_subdirectory(python)
diff --git a/contrib/cmake/examples/python/CMakeLists.txt b/contrib/cmake/examples/python/CMakeLists.txt
new file mode 100644
index 000000000..fdbb7891f
--- /dev/null
+++ b/contrib/cmake/examples/python/CMakeLists.txt
@@ -0,0 +1,24 @@
+set(python_example_files
+  example.py
+  visitor.py
+)
+
+set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}/python")
+
+set(build_z3_python_examples_target_depends "")
+foreach (example_file ${python_example_files})
+  add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${example_file}"
+    COMMAND "${CMAKE_COMMAND}" "-E" "copy"
+      "${CMAKE_CURRENT_SOURCE_DIR}/${example_file}"
+      "${z3py_bindings_build_dest}/${example_file}"
+    DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${example_file}"
+    COMMENT "Copying \"${example_file}\" to ${z3py_bindings_build_dest}/${example_file}"
+  )
+  list(APPEND build_z3_python_examples_target_depends "${z3py_bindings_build_dest}/${example_file}")
+endforeach()
+
+add_custom_target(build_z3_python_examples
+  ALL
+  DEPENDS
+    ${build_z3_python_examples_target_depends}
+)
diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/contrib/cmake/src/api/python/CMakeLists.txt
index 555333c9f..dcd6f09e0 100644
--- a/contrib/cmake/src/api/python/CMakeLists.txt
+++ b/contrib/cmake/src/api/python/CMakeLists.txt
@@ -4,32 +4,34 @@ message(STATUS "Emitting rules to build Z3 python bindings")
 ###############################################################################
 # This allows the python bindings to be used directly from the build directory
 set(z3py_files
-  z3.py
-  z3num.py
-  z3poly.py
-  z3printer.py
-  z3rcf.py
-  z3test.py
-  z3types.py
-  z3util.py
+  z3/__init__.py
+  z3/z3.py
+  z3/z3num.py
+  z3/z3poly.py
+  z3/z3printer.py
+  z3/z3rcf.py
+  z3/z3types.py
+  z3/z3util.py
 )
 
-set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}")
+set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}/python")
+file(MAKE_DIRECTORY "${z3py_bindings_build_dest}")
+file(MAKE_DIRECTORY "${z3py_bindings_build_dest}/z3")
 
 set(build_z3_python_bindings_target_depends "")
 foreach (z3py_file ${z3py_files})
   add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${z3py_file}"
     COMMAND "${CMAKE_COMMAND}" "-E" "copy"
       "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
-      "${z3py_bindings_build_dest}"
+      "${z3py_bindings_build_dest}/${z3py_file}"
     DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
-    COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}"
+    COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}/${z3py_file}"
   )
   list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/${z3py_file}")
 endforeach()
 
 # Generate z3core.py
-add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3core.py"
+add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py"
   COMMAND "${PYTHON_EXECUTABLE}"
     "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
@@ -44,10 +46,10 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3core.py"
   COMMENT "Generating z3core.py"
   ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
 )
-list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3core.py")
+list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3core.py")
 
 # Generate z3consts.py
-add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3consts.py"
+add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3consts.py"
   COMMAND "${PYTHON_EXECUTABLE}"
     "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
@@ -60,13 +62,29 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3consts.py"
   COMMENT "Generating z3consts.py"
   ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
 )
-list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3consts.py")
+list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3consts.py")
+
+if (UNIX)
+  set(LINK_COMMAND "create_symlink")
+else()
+  set(LINK_COMMAND "copy")
+endif()
+
+# Link libz3 into the python directory so bindings work out of the box
+add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+  COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
+    "${CMAKE_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+    "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+  DEPENDS libz3
+  COMMENT "Linking libz3 into python directory"
+)
 
 # Convenient top-level target
 add_custom_target(build_z3_python_bindings
   ALL
   DEPENDS
     ${build_z3_python_bindings_target_depends}
+    "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
 )
 
 ###############################################################################
@@ -117,7 +135,7 @@ if (INSTALL_PYTHON_BINDINGS)
   # Using DESTDIR still seems to work even if we use an absolute path
   message(STATUS "Python bindings will be installed to \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"")
   install(FILES ${build_z3_python_bindings_target_depends}
-    DESTINATION "${CMAKE_INSTALL_PYTHON_PKG_DIR}"
+    DESTINATION "${CMAKE_INSTALL_PYTHON_PKG_DIR}/z3"
   )
 else()
   message(STATUS "Not emitting rules to install Z3 python bindings")
diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py
index cbeb8a82d..7e7cb5584 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_project.py b/scripts/mk_project.py
index 78bc290f8..00b5cdef5 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -87,7 +87,8 @@ def init_project_def():
                               reexports=['api'],
                               dll_name='libz3',
                               static=build_static_lib(),
-                              export_files=API_files)
+                              export_files=API_files,
+                              staging_link='python')
     add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties', default_key_file='src/api/dotnet/Microsoft.Z3.snk')
     add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.microsoft.z3", manifest_file='manifest')
     add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml')
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 66191e160..305f94609 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1230,7 +1230,7 @@ def get_so_ext():
         return 'dll'
 
 class DLLComponent(Component):
-    def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static):
+    def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static, staging_link=None):
         Component.__init__(self, name, path, deps)
         if dll_name is None:
             dll_name = name
@@ -1239,6 +1239,7 @@ class DLLComponent(Component):
         self.reexports = reexports
         self.install = install
         self.static = static
+        self.staging_link = staging_link    # link a copy of the shared object into this directory on build
 
     def get_link_name(self):
         if self.static:
@@ -1294,6 +1295,11 @@ class DLLComponent(Component):
         out.write(' $(SLINK_EXTRA_FLAGS)')
         if IS_WINDOWS:
             out.write(' /DEF:%s.def' % os.path.join(self.to_src_dir, self.name))
+        if self.staging_link:
+            if IS_WINDOWS or IS_OSX:
+                out.write('\n\tcp %s %s' % (self.dll_file(), self.staging_link))
+            else:
+                out.write('\n\tln -f -s %s %s' % (os.path.join(reverse_path(self.staging_link), self.dll_file()), self.staging_link))
         out.write('\n')
         if self.static:
             if IS_WINDOWS:
@@ -1432,13 +1438,18 @@ class PythonInstallComponent(Component):
     def mk_install(self, out):
         if not is_python_install_enabled():
             return
-        MakeRuleCmd.make_install_directory(out, self.pythonPkgDir, in_prefix=self.in_prefix_install)
+        MakeRuleCmd.make_install_directory(out,
+                                           os.path.join(self.pythonPkgDir, 'z3'),
+                                           in_prefix=self.in_prefix_install)
+        MakeRuleCmd.make_install_directory(out,
+                                           os.path.join(self.pythonPkgDir, 'z3', 'lib'),
+                                           in_prefix=self.in_prefix_install)
 
         # Sym-link or copy libz3 into python package directory
         if IS_WINDOWS or IS_OSX:
             MakeRuleCmd.install_files(out,
                                       self.libz3Component.dll_file(),
-                                      os.path.join(self.pythonPkgDir,
+                                      os.path.join(self.pythonPkgDir, 'z3', 'lib',
                                                    self.libz3Component.dll_file()),
                                       in_prefix=self.in_prefix_install
                                      )
@@ -1449,34 +1460,29 @@ class PythonInstallComponent(Component):
             # staged installs that use DESTDIR).
             MakeRuleCmd.create_relative_symbolic_link(out,
                                                       self.libz3Component.install_path(),
-                                                      os.path.join(self.pythonPkgDir,
+                                                      os.path.join(self.pythonPkgDir, 'z3', 'lib',
                                                                    self.libz3Component.dll_file()
                                                                   ),
                                                      )
 
-        MakeRuleCmd.install_files(out, 'z3*.py', self.pythonPkgDir,
+        MakeRuleCmd.install_files(out, os.path.join('python', 'z3', '*.py'),
+                                  os.path.join(self.pythonPkgDir, 'z3'),
                                   in_prefix=self.in_prefix_install)
         if sys.version >= "3":
-            pythonPycacheDir = os.path.join(self.pythonPkgDir, '__pycache__')
+            pythonPycacheDir = os.path.join(self.pythonPkgDir, 'z3', '__pycache__')
             MakeRuleCmd.make_install_directory(out,
                                                pythonPycacheDir,
                                                in_prefix=self.in_prefix_install)
             MakeRuleCmd.install_files(out,
-                                      '{}*.pyc'.format(os.path.join('__pycache__', 'z3')),
+                                      os.path.join('python', 'z3', '__pycache__', '*.pyc'),
                                       pythonPycacheDir,
                                       in_prefix=self.in_prefix_install)
         else:
             MakeRuleCmd.install_files(out,
-                                      'z3*.pyc',
+                                      os.path.join('python', 'z3', '*.pyc'),
                                       self.pythonPkgDir,
                                       in_prefix=self.in_prefix_install)
         if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
-            if os.uname()[0] == 'Darwin':
-                LD_LIBRARY_PATH = "DYLD_LIBRARY_PATH"
-            else:
-                LD_LIBRARY_PATH = "LD_LIBRARY_PATH"
-            out.write('\t@echo Z3 shared libraries were installed at \'%s\', make sure this directory is in your %s environment variable.\n' %
-                      (os.path.join(PREFIX, INSTALL_LIB_DIR), LD_LIBRARY_PATH))
             out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
 
     def mk_uninstall(self, out):
@@ -1488,13 +1494,13 @@ class PythonInstallComponent(Component):
                                            in_prefix=self.in_prefix_install
                                           )
         MakeRuleCmd.remove_installed_files(out,
-                                           '{}*.py'.format(os.path.join(self.pythonPkgDir, 'z3')),
+                                           os.path.join(self.pythonPkgDir, 'z3', '*.py'),
                                            in_prefix=self.in_prefix_install)
         MakeRuleCmd.remove_installed_files(out,
-                                           '{}*.pyc'.format(os.path.join(self.pythonPkgDir, 'z3')),
+                                           os.path.join(self.pythonPkgDir, 'z3', '*.pyc'),
                                            in_prefix=self.in_prefix_install)
         MakeRuleCmd.remove_installed_files(out,
-                                           '{}*.pyc'.format(os.path.join(self.pythonPkgDir, '__pycache__', 'z3')),
+                                           os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'),
                                            in_prefix=self.in_prefix_install
                                           )
 
@@ -2157,9 +2163,9 @@ class PythonExampleComponent(ExampleComponent):
     def mk_makefile(self, out):
         full = os.path.join(EXAMPLE_DIR, self.path)
         for py in filter(lambda f: f.endswith('.py'), os.listdir(full)):
-            shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, py))
+            shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, 'python', py))
             if is_verbose():
-                print("Copied Z3Py example '%s' to '%s'" % (py, BUILD_DIR))
+                print("Copied Z3Py example '%s' to '%s'" % (py, os.path.join(BUILD_DIR, 'python')))
         out.write('_ex_%s: \n\n' % self.name)
 
 
@@ -2189,8 +2195,8 @@ def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True):
     c = ExtraExeComponent(name, exe_name, path, deps, install)
     reg_component(name, c)
 
-def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False):
-    c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static)
+def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False, staging_link=None):
+    c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static, staging_link)
     reg_component(name, c)
     return c
 
@@ -2519,9 +2525,9 @@ def mk_makefile():
         if c.main_component():
             out.write(' %s' % c.name)
     out.write('\n\t@echo Z3 was successfully built.\n')
-    out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % BUILD_DIR)
+    out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % os.path.join(BUILD_DIR, 'python'))
     pathvar = "DYLD_LIBRARY_PATH" if IS_OSX else "PATH" if IS_WINDOWS else "LD_LIBRARY_PATH"
-    out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH and %s environment variables.\"\n" % (BUILD_DIR, pathvar))
+    out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH environment variable and the \'%s\' directory is added to the %s environment variable.\"\n" % (os.path.join(BUILD_DIR, 'python'), BUILD_DIR, pathvar))
     if not IS_WINDOWS:
         out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n")
         out.write('\t@echo "    sudo make install"\n\n')
@@ -2737,33 +2743,40 @@ def mk_def_files():
 
 def cp_z3py_to_build():
     mk_dir(BUILD_DIR)
+    mk_dir(os.path.join(BUILD_DIR, 'python'))
+    z3py_dest = os.path.join(BUILD_DIR, 'python', 'z3')
+    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:
             if f.endswith('.pyc'):
                 rmf(os.path.join(root, f))
     # Compile Z3Py files
-    if compileall.compile_dir(Z3PY_SRC_DIR, force=1) != 1:
+    if compileall.compile_dir(z3py_src, force=1) != 1:
         raise MKException("failed to compile Z3Py sources")
+    if is_verbose:
+        print("Generated python bytecode")
     # 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))
+    mk_dir(z3py_dest)
+    for py in filter(lambda f: f.endswith('.py'), os.listdir(z3py_src)):
+        shutil.copyfile(os.path.join(z3py_src, py), os.path.join(z3py_dest, py))
         if is_verbose():
             print("Copied '%s'" % py)
     # 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)
+            print("Copied '%s'" % pyc)
     # Python 3.x support
-    src_pycache = os.path.join(Z3PY_SRC_DIR, '__pycache__')
+    src_pycache = os.path.join(z3py_src, '__pycache__')
+    target_pycache = os.path.join(z3py_dest, '__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__')
             mk_dir(target_pycache)
             shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc))
             if is_verbose():
-                print("Generated '%s'" % pyc)
+                print("Copied '%s'" % pyc)
 
 def mk_bindings(api_files):
     if not ONLY_MAKEFILES:
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 733d5b1fa..d8b2bec58 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1600,27 +1600,25 @@ def write_core_py_preamble(core_py):
   core_py.write('# Automatically generated file\n')
   core_py.write('import sys, os\n')
   core_py.write('import ctypes\n')
-  core_py.write('from z3types import *\n')
-  core_py.write('from z3consts import *\n')
+  core_py.write('import pkg_resources\n')
+  core_py.write('from .z3types import *\n')
+  core_py.write('from .z3consts import *\n')
   core_py.write(
 """
+_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
+
 _lib = None
 def lib():
   global _lib
-  if _lib == None:
-    _dir = os.path.dirname(os.path.abspath(__file__))
-    for ext in ['dll', 'so', 'dylib']:
+  if _lib is None:
+    _dirs = ['.', pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), '']
+    for _dir in _dirs:
       try:
-        init('libz3.%s' % ext)
+        init(_dir)
         break
       except:
         pass
-      try:
-        init(os.path.join(_dir, 'libz3.%s' % ext))
-        break
-      except:
-        pass
-    if _lib == None:
+    if _lib is None:
         raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
   return _lib
 
@@ -1643,6 +1641,10 @@ else:
         return ""
 
 def init(PATH):
+  PATH = os.path.realpath(PATH)
+  if os.path.isdir(PATH):
+    PATH = os.path.join(PATH, 'libz3.%s' % _ext)
+
   global _lib
   _lib = ctypes.CDLL(PATH)
 """
@@ -1706,7 +1708,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, os.path.join('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/.gitignore b/src/api/python/.gitignore
new file mode 100644
index 000000000..86e4bc9ce
--- /dev/null
+++ b/src/api/python/.gitignore
@@ -0,0 +1,8 @@
+MANIFEST
+dist
+core
+build
+*.egg-info
+bin
+z3/lib
+z3/include
diff --git a/src/api/python/MANIFEST.in b/src/api/python/MANIFEST.in
new file mode 100644
index 000000000..209e0cfa3
--- /dev/null
+++ b/src/api/python/MANIFEST.in
@@ -0,0 +1,4 @@
+include core/LICENSE.txt
+recursive-include core/src *
+recursive-include core/scripts *
+recursive-include core/examples *
diff --git a/src/api/python/setup.py b/src/api/python/setup.py
new file mode 100644
index 000000000..c6d7d8824
--- /dev/null
+++ b/src/api/python/setup.py
@@ -0,0 +1,155 @@
+import os
+import sys
+import shutil
+import platform
+import subprocess
+import multiprocessing
+from setuptools import setup
+from distutils.errors import LibError
+from distutils.command.build import build as _build
+from distutils.command.sdist import sdist as _sdist
+from setuptools.command.develop import develop as _develop
+from setuptools.command.bdist_egg import bdist_egg as _bdist_egg
+
+
+build_env = dict(os.environ)
+build_env['PYTHON'] = sys.executable
+build_env['CXXFLAGS'] = "-std=c++11"
+
+ROOT_DIR = os.path.abspath(os.path.dirname(__file__))
+SRC_DIR_LOCAL = os.path.join(ROOT_DIR, 'core')
+SRC_DIR_REPO = os.path.join(ROOT_DIR, '..', '..', '..')
+SRC_DIR = SRC_DIR_LOCAL if os.path.exists(SRC_DIR_LOCAL) else SRC_DIR_REPO
+BUILD_DIR = os.path.join(SRC_DIR, 'build') # implicit in configure script
+LIBS_DIR = os.path.join(ROOT_DIR, 'z3', 'lib')
+HEADERS_DIR = os.path.join(ROOT_DIR, 'z3', 'include')
+BINS_DIR = os.path.join(ROOT_DIR, 'bin')
+
+if sys.platform == 'darwin':
+    LIBRARY_FILE = "libz3.dylib"
+elif sys.platform in ('win32', 'cygwin'):
+    LIBRARY_FILE = "libz3.dll"
+else:
+    LIBRARY_FILE = "libz3.so"
+
+def _clean_bins():
+    """
+    Clean up the binary files and headers that are installed along with the bindings
+    """
+    shutil.rmtree(LIBS_DIR, ignore_errors=True)
+    shutil.rmtree(BINS_DIR, ignore_errors=True)
+    shutil.rmtree(HEADERS_DIR, ignore_errors=True)
+
+def _configure_z3():
+    # bail out early if we don't need to do this - it forces a rebuild every time otherwise
+    if os.path.exists(BUILD_DIR):
+        return
+    args = [sys.executable, os.path.join(SRC_DIR, 'scripts', 'mk_make.py')]
+
+    if sys.platform == 'win32' and platform.architecture()[0] == '64bit':
+        args += ['-x']
+
+    if subprocess.call(args, env=build_env, cwd=SRC_DIR) != 0:
+        raise LibError("Unable to configure Z3.")
+
+def _build_z3():
+    if sys.platform == 'win32':
+        if subprocess.call(['nmake'], env=build_env,
+                           cwd=BUILD_DIR) != 0:
+            raise LibError("Unable to build Z3.")
+    else:   # linux and osx
+        if subprocess.call(['make', '-j', str(multiprocessing.cpu_count())],
+                    env=build_env, cwd=BUILD_DIR) != 0:
+            raise LibError("Unable to build Z3.")
+
+def _copy_bins():
+    """
+    Copy the library and header files into their final destinations
+    """
+    # STEP 1: If we're performing a build from a copied source tree,
+    # copy the generated python files into the package
+
+    _clean_bins()
+
+    if SRC_DIR == SRC_DIR_LOCAL:
+        shutil.copy(os.path.join(SRC_DIR, 'src', 'api', 'python', 'z3', 'z3core.py'), os.path.join(ROOT_DIR, 'z3'))
+        shutil.copy(os.path.join(SRC_DIR, 'src', 'api', 'python', 'z3', 'z3consts.py'), os.path.join(ROOT_DIR, 'z3'))
+
+    # STEP 2: Copy the shared library, the executable and the headers
+
+    os.mkdir(LIBS_DIR)
+    os.mkdir(BINS_DIR)
+    os.mkdir(HEADERS_DIR)
+    os.mkdir(os.path.join(HEADERS_DIR, 'c++'))
+    shutil.copy(os.path.join(BUILD_DIR, 'libz3.so'), LIBS_DIR)
+    shutil.copy(os.path.join(BUILD_DIR, 'z3'), BINS_DIR)
+    for fname in ('z3.h', 'z3_v1.h', 'z3_macros.h', 'z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h', 'z3_fpa.h', os.path.join('c++', 'z3++.h')):
+        shutil.copy(os.path.join(SRC_DIR, 'src', 'api', fname), os.path.join(HEADERS_DIR, fname))
+
+def _copy_sources():
+    """
+    Prepare for a source distribution by assembling a minimal set of source files needed
+    for building
+    """
+    shutil.rmtree(SRC_DIR_LOCAL, ignore_errors=True)
+    os.mkdir(SRC_DIR_LOCAL)
+
+    shutil.copy(os.path.join(SRC_DIR_REPO, 'LICENSE.txt'), SRC_DIR_LOCAL)
+    shutil.copytree(os.path.join(SRC_DIR_REPO, 'scripts'), os.path.join(SRC_DIR_LOCAL, 'scripts'))
+    shutil.copytree(os.path.join(SRC_DIR_REPO, 'examples'), os.path.join(SRC_DIR_LOCAL, 'examples'))
+    shutil.copytree(os.path.join(SRC_DIR_REPO, 'src'), os.path.join(SRC_DIR_LOCAL, 'src'),
+            ignore=lambda src, names: ['python'] if 'api' in src else [])
+
+    # stub python dir to make build happy
+    os.mkdir(os.path.join(SRC_DIR_LOCAL, 'src', 'api', 'python'))
+    os.mkdir(os.path.join(SRC_DIR_LOCAL, 'src', 'api', 'python', 'z3'))
+    open(os.path.join(SRC_DIR_LOCAL, 'src', 'api', 'python', 'z3', '.placeholder'), 'w').close()
+
+class build(_build):
+    def run(self):
+        self.execute(_configure_z3, (), msg="Configuring Z3")
+        self.execute(_build_z3, (), msg="Building Z3")
+        self.execute(_copy_bins, (), msg="Copying binaries")
+        _build.run(self)
+
+class develop(_develop):
+    def run(self):
+        self.execute(_configure_z3, (), msg="Configuring Z3")
+        self.execute(_build_z3, (), msg="Building Z3")
+        self.execute(_copy_bins, (), msg="Copying binaries")
+        _develop.run(self)
+
+class bdist_egg(_bdist_egg):
+    def run(self):
+        self.run_command('build')
+        _bdist_egg.run(self)
+
+class sdist(_sdist):
+    def run(self):
+        self.execute(_clean_bins, (), msg="Cleaning binary files")
+        self.execute(_copy_sources, (), msg="Copying source files")
+        _sdist.run(self)
+
+# the build directory needs to exist
+#try: os.makedirs(os.path.join(ROOT_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'],
+    packages=['z3'],
+    include_package_data=True,
+    package_data={
+        'z3': [os.path.join('lib', '*'), os.path.join('include', '*')]
+    },
+    scripts=[os.path.join('bin', 'z3')],
+    cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_egg': bdist_egg},
+)
diff --git a/src/api/python/z3/__init__.py b/src/api/python/z3/__init__.py
new file mode 100644
index 000000000..f7aa29ab1
--- /dev/null
+++ b/src/api/python/z3/__init__.py
@@ -0,0 +1,12 @@
+from .z3 import *
+
+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.py b/src/api/python/z3/z3.py
similarity index 99%
rename from src/api/python/z3.py
rename to src/api/python/z3/z3.py
index 83e9eaae9..d7571a3c7 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3/z3.py
@@ -41,10 +41,10 @@ Z3 exceptions:
 ...   print("failed: %s" % ex)
 failed: sort mismatch
 """
-from z3core import *
-from z3types import *
-from z3consts import *
-from z3printer import *
+from .z3core import *
+from .z3types import *
+from .z3consts import *
+from .z3printer import *
 from fractions import Fraction
 import sys
 import io
diff --git a/src/api/python/z3num.py b/src/api/python/z3/z3num.py
similarity index 99%
rename from src/api/python/z3num.py
rename to src/api/python/z3/z3num.py
index b219829d3..14d8550e6 100644
--- a/src/api/python/z3num.py
+++ b/src/api/python/z3/z3num.py
@@ -5,9 +5,9 @@
 #
 # Author: Leonardo de Moura (leonardo)
 ############################################
-from z3 import *
-from z3core import *
-from z3printer import *
+from .z3 import *
+from .z3core import *
+from .z3printer import *
 from fractions import Fraction
 
 def _to_numeral(num, ctx=None):
diff --git a/src/api/python/z3poly.py b/src/api/python/z3/z3poly.py
similarity index 97%
rename from src/api/python/z3poly.py
rename to src/api/python/z3/z3poly.py
index 0b8bf9457..169944291 100644
--- a/src/api/python/z3poly.py
+++ b/src/api/python/z3/z3poly.py
@@ -5,7 +5,8 @@
 #
 # Author: Leonardo de Moura (leonardo)
 ############################################
-from z3 import *
+
+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/z3printer.py b/src/api/python/z3/z3printer.py
similarity index 99%
rename from src/api/python/z3printer.py
rename to src/api/python/z3/z3printer.py
index c8d69900a..e02c28a96 100644
--- a/src/api/python/z3printer.py
+++ b/src/api/python/z3/z3printer.py
@@ -6,8 +6,8 @@
 # Author: Leonardo de Moura (leonardo)
 ############################################
 import sys, io, z3
-from z3consts import *
-from z3core import *
+from .z3consts import *
+from .z3core import *
 from ctypes import *
 
 ##############################
diff --git a/src/api/python/z3rcf.py b/src/api/python/z3/z3rcf.py
similarity index 98%
rename from src/api/python/z3rcf.py
rename to src/api/python/z3/z3rcf.py
index 84c724910..9d6f2f6ad 100644
--- a/src/api/python/z3rcf.py
+++ b/src/api/python/z3/z3rcf.py
@@ -9,9 +9,9 @@
 #
 # Author: Leonardo de Moura (leonardo)
 ############################################
-from z3 import *
-from z3core import *
-from z3printer import *
+from .z3 import *
+from .z3core import *
+from .z3printer import *
 from fractions import Fraction
 
 def _to_rcfnum(num, ctx=None):
diff --git a/src/api/python/z3types.py b/src/api/python/z3/z3types.py
similarity index 99%
rename from src/api/python/z3types.py
rename to src/api/python/z3/z3types.py
index 44b19d33a..7cf61f49e 100644
--- a/src/api/python/z3types.py
+++ b/src/api/python/z3/z3types.py
@@ -6,7 +6,7 @@
 # Author: Leonardo de Moura (leonardo)
 ############################################
 
-import ctypes, z3core
+import ctypes
 
 class Z3Exception(Exception):
     def __init__(self, value):
@@ -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
-
diff --git a/src/api/python/z3util.py b/src/api/python/z3/z3util.py
similarity index 99%
rename from src/api/python/z3util.py
rename to src/api/python/z3/z3util.py
index 2494461cf..fe7e76b86 100644
--- a/src/api/python/z3util.py
+++ b/src/api/python/z3/z3util.py
@@ -11,7 +11,7 @@ Usage:
 import common_z3 as CM_Z3
 """
 
-from z3 import *
+from .z3 import *
 
 def vset(seq, idfun=None, as_list=True):
     # This functions preserves the order of arguments while removing duplicates.