From 4801a27c2df48162c771aa94fe395253b989a3bc Mon Sep 17 00:00:00 2001
From: Andrew Dutcher <andrew@andrewdutcher.com>
Date: Wed, 21 Sep 2016 16:55:24 -0700
Subject: [PATCH] Fix up z3test to a) exist and b) work

---
 scripts/mk_util.py         |  2 ++
 src/api/python/setup.py    |  2 +-
 src/api/python/z3/z3.py    |  1 +
 src/api/python/z3/z3num.py |  5 -----
 src/api/python/z3test.py   | 13 ++++++++++---
 5 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 1e91c2d0d..57f2c7ad1 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2779,6 +2779,8 @@ def cp_z3py_to_build():
             shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc))
             if is_verbose():
                 print("Copied '%s'" % pyc)
+    # Copy z3test.py
+    shutil.copyfile(os.path.join(Z3PY_SRC_DIR, 'z3test.py'), os.path.join(BUILD_DIR, 'python', 'z3test.py'))
 
 def mk_bindings(api_files):
     if not ONLY_MAKEFILES:
diff --git a/src/api/python/setup.py b/src/api/python/setup.py
index c6d7d8824..45da4d085 100644
--- a/src/api/python/setup.py
+++ b/src/api/python/setup.py
@@ -148,7 +148,7 @@ setup(
     packages=['z3'],
     include_package_data=True,
     package_data={
-        'z3': [os.path.join('lib', '*'), os.path.join('include', '*')]
+        'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')]
     },
     scripts=[os.path.join('bin', 'z3')],
     cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_egg': bdist_egg},
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index d7571a3c7..4ee5883ed 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -41,6 +41,7 @@ Z3 exceptions:
 ...   print("failed: %s" % ex)
 failed: sort mismatch
 """
+from . import z3core
 from .z3core import *
 from .z3types import *
 from .z3consts import *
diff --git a/src/api/python/z3/z3num.py b/src/api/python/z3/z3num.py
index 14d8550e6..c8f15e7b8 100644
--- a/src/api/python/z3/z3num.py
+++ b/src/api/python/z3/z3num.py
@@ -572,9 +572,4 @@ def isolate_roots(p, vs=[]):
         _vs[i] = vs[i].ast
     _roots = AstVector(Z3_algebraic_roots(p.ctx_ref(), p.as_ast(), num, _vs), p.ctx)
     return [ Numeral(r) for r in _roots ]
-        
-if __name__ == "__main__":
-    import doctest
-    if doctest.testmod().failed:
-        exit(1)
 
diff --git a/src/api/python/z3test.py b/src/api/python/z3test.py
index 38939cebf..9c544f623 100644
--- a/src/api/python/z3test.py
+++ b/src/api/python/z3test.py
@@ -5,9 +5,16 @@
 #
 # Author: Leonardo de Moura (leonardo)
 ############################################
-import z3, doctest
+import z3, doctest, sys
+
+if len(sys.argv) < 2 or sys.argv[1] == 'z3':
+    r = doctest.testmod(z3.z3)
+elif sys.argv[1] == 'z3num':
+    r = doctest.testmod(z3.z3num)
+else:
+    print 'Usage: z3test.py (z3 | z3num)'
+    sys.exit(1)
 
-r = doctest.testmod(z3)
 if r.failed != 0:
-    exit(1)
+    sys.exit(1)