Fix up z3test to a) exist and b) work

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:

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},

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 *

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)
 

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)