Update math/z3 to version 4.5.0

From the release notes:

    New features:
    - New theories of strings and sequences.
    - Incremental consequence finder for finite domains.
    - CMake build system (thanks @delcypher).
    - Updated and improved OCaml API (thanks @martin-neuhaeusser).
    - Updated and improved Java API (thanks @cheshire).
    - New resource limit facilities to avoid non-deterministic timeout behaviour.
    - New bit-vector simplification and ackermannization tactics (thanks @MikolasJanota, @nunoplopes).
    - QSAT: a new solver for quantified arithmetic problems. See:
      Bjorner, Janota: Playing with Quantified Satisfaction, LPAR 2016.

    A multitude of bugs has been fixed.

I am about to commit a separate package for the Python bindings.

Coordinated with dholland@

11 files changed, 304 insertions, 113 deletions

diff --git a/math/z3/Makefile b/math/z3/Makefile
index 7aad1438af4..afe8928e34e 100644
--- a/math/z3/Makefile
+++ b/math/z3/Makefile
@@ -1,32 +1,9 @@
-# $NetBSD: Makefile,v 1.7 2018/02/27 08:34:16 wiz Exp $
+# $NetBSD: Makefile,v 1.8 2018/03/13 00:31:16 khorben Exp $
 
-DISTNAME=	z3-4.4.1
-GITHUB_TAG=	${DISTNAME}
-PKGREVISION=	5
-CATEGORIES=	math
-MASTER_SITES=	${MASTER_SITE_GITHUB:=Z3Prover/}
-PATCHFILES+=	z3-jumbo-patch-20151123.gz
-SITES.z3-jumbo-patch-20151123.gz=\
-			http://www.NetBSD.org/~dholland/patchkits/z3/
-PATCH_DIST_STRIP=	-p1
+.include "Makefile.common"
 
-MAINTAINER=	dholland@NetBSD.org
-HOMEPAGE=	https://github.com/Z3Prover/z3/
 COMMENT=	The Z3 theorem prover / SMT solver
-LICENSE=	mit
-
-WRKSRC=		${WRKDIR}/z3-${DISTNAME}
-HAS_CONFIGURE=	yes
-USE_LANGUAGES=	c c++
-BUILD_DIRS=	build
-PY_PATCHPLIST=	yes
-
-PYTHON_VERSIONS_ACCEPTED=	27
-
-CONFIGURE_ENV+=		PYTHON=${PYTHONBIN}
-CONFIGURE_ARGS+=	--destdir=${DESTDIR} --prefix=${PREFIX}
 
 .include "options.mk"
 
-.include "../../lang/python/extension.mk"
 .include "../../mk/bsd.pkg.mk"
diff --git a/math/z3/Makefile.common b/math/z3/Makefile.common
new file mode 100644
index 00000000000..a8db949668a
--- /dev/null
+++ b/math/z3/Makefile.common
@@ -0,0 +1,26 @@
+# $NetBSD: Makefile.common,v 1.1 2018/03/13 00:31:16 khorben Exp $
+#
+# used by wip/py-z3/Makefile
+# used by wip/z3/Makefile
+
+DISTNAME=	z3-4.5.0
+GITHUB_TAG=	${DISTNAME}
+CATEGORIES=	math
+MASTER_SITES=	${MASTER_SITE_GITHUB:=Z3Prover/}
+DISTINFO_FILE=	${.CURDIR}/../../wip/z3/distinfo
+PATCHDIR?=	${.CURDIR}/../../wip/z3/patches
+
+MAINTAINER=	dholland@NetBSD.org
+HOMEPAGE=	https://github.com/Z3Prover/z3/
+LICENSE=	mit
+
+WRKSRC=		${WRKDIR}/z3-${DISTNAME}
+HAS_CONFIGURE=	yes
+USE_LANGUAGES=	c c++
+BUILD_DIRS=	build
+
+CONFIGURE_ENV+=		PYTHON=${PYTHONBIN}
+CONFIGURE_ARGS+=	--destdir=${DESTDIR}
+CONFIGURE_ARGS+=	--prefix=${PREFIX}
+
+.include "../../lang/python/tool.mk"
diff --git a/math/z3/PLIST b/math/z3/PLIST
index 866184fe592..3074ed3dcd5 100644
--- a/math/z3/PLIST
+++ b/math/z3/PLIST
@@ -1,34 +1,32 @@
-@comment $NetBSD: PLIST,v 1.1 2015/11/24 05:45:58 dholland Exp $
+@comment $NetBSD: PLIST,v 1.2 2018/03/13 00:31:16 khorben Exp $
 bin/z3
 include/z3++.h
 include/z3.h
 include/z3_algebraic.h
 include/z3_api.h
+include/z3_ast_containers.h
+include/z3_fixedpoint.h
 include/z3_fpa.h
 include/z3_interp.h
 include/z3_macros.h
+include/z3_optimization.h
 include/z3_polynomial.h
 include/z3_rcf.h
 include/z3_v1.h
 lib/libz3.so
-${PYSITELIB}/libz3.so
-${PYSITELIB}/z3.py
-${PYSITELIB}/z3.pyc
-${PYSITELIB}/z3consts.py
-${PYSITELIB}/z3consts.pyc
-${PYSITELIB}/z3core.py
-${PYSITELIB}/z3core.pyc
-${PYSITELIB}/z3num.py
-${PYSITELIB}/z3num.pyc
-${PYSITELIB}/z3poly.py
-${PYSITELIB}/z3poly.pyc
-${PYSITELIB}/z3printer.py
-${PYSITELIB}/z3printer.pyc
-${PYSITELIB}/z3rcf.py
-${PYSITELIB}/z3rcf.pyc
-${PYSITELIB}/z3test.py
-${PYSITELIB}/z3test.pyc
-${PYSITELIB}/z3types.py
-${PYSITELIB}/z3types.pyc
-${PYSITELIB}/z3util.py
-${PYSITELIB}/z3util.pyc
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/META
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/dllz3ml.so
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/libz3ml.a
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.cmi
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.cmx
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.mli
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.cmi
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.cmx
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.mli
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.a
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cma
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cmxa
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cmxs
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.cmi
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.cmx
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.mli
diff --git a/math/z3/buildlink3.mk b/math/z3/buildlink3.mk
new file mode 100644
index 00000000000..98a2363a7cc
--- /dev/null
+++ b/math/z3/buildlink3.mk
@@ -0,0 +1,13 @@
+# $NetBSD: buildlink3.mk,v 1.1 2018/03/13 00:31:16 khorben Exp $
+
+BUILDLINK_TREE+=	z3
+
+.if !defined(Z3_BUILDLINK3_MK)
+Z3_BUILDLINK3_MK:=
+
+BUILDLINK_API_DEPENDS.z3+=	z3>=4.5.0
+BUILDLINK_PKGSRCDIR.z3?=	../../wip/z3
+
+.endif  # Z3_BUILDLINK3_MK
+
+BUILDLINK_TREE+=	-z3
diff --git a/math/z3/distinfo b/math/z3/distinfo
index 2b415d9876b..4029b25d2a6 100644
--- a/math/z3/distinfo
+++ b/math/z3/distinfo
@@ -1,13 +1,9 @@
-$NetBSD: distinfo,v 1.3 2018/02/23 17:04:43 khorben Exp $
+$NetBSD: distinfo,v 1.4 2018/03/13 00:31:16 khorben Exp $
 
-SHA1 (z3-4.4.1.tar.gz) = 60094acaa53459ec694899aca9f17aa830875610
-RMD160 (z3-4.4.1.tar.gz) = 2c891e115a5d097dbbda53c1b322c65bc5b679f7
-SHA512 (z3-4.4.1.tar.gz) = 76991a24f47f2b53ceb8d7a9a6be19913c57994ffb6cf6acfe30f61b2e73959cf02a99f656053594fccb5aaf4d1f44b3ae7e51f1c8953b213d738ceeeaea74f8
-Size (z3-4.4.1.tar.gz) = 3347371 bytes
-SHA1 (z3-jumbo-patch-20151123.gz) = d31b8840575536104680bb624b15cc1c2084a7fb
-RMD160 (z3-jumbo-patch-20151123.gz) = eb74bd41125e1b07a7f873774a2c354e3c8ca378
-SHA512 (z3-jumbo-patch-20151123.gz) = c23d363bf53b40c3ccbfc10d03ef3621d6abfa9cf86375e7e853e85a0971db70992173df04df1a895e16d4a9b533e955953455a7533889963d2920a4b48d0056
-Size (z3-jumbo-patch-20151123.gz) = 4395 bytes
-SHA1 (patch-scripts_mk__util.py) = 84ccd3fa33a3fcffa53af6f838f6caacdfec40a8
-SHA1 (patch-src_util_debug.cpp) = 607ea4e078884920a3034cf00779dce25fc8e623
-SHA1 (patch-src_util_mpz.cpp) = 69988bec1472df14209ae0dbfdc8a94c9e71cc82
+SHA1 (z3-4.5.0.tar.gz) = 6f4e94e025fcc2fa2896524d8fbb9de0b3033854
+RMD160 (z3-4.5.0.tar.gz) = 81121307ac83f42989da49efda31964a94f7f5d5
+SHA512 (z3-4.5.0.tar.gz) = 1ebc2c908d90b6b879f1e819c864ff894613276af47a440f27cf94968c195656952434754c3eb20f4bdbdd8497d227d22e1b4821c0d320b11052b5648d9e2dc7
+Size (z3-4.5.0.tar.gz) = 3573695 bytes
+SHA1 (patch-configure) = 8d5fe787f15fe781c3c23cee27058f898de8c95e
+SHA1 (patch-scripts_mk__util.py) = f0a7cfabdbf9b6c1eb92e75f381d8a3f8a088d35
+SHA1 (patch-src_util_stopwatch.h) = dbeab175ed4f507d5378f1966f8ed173c4c9a9a7
diff --git a/math/z3/options.mk b/math/z3/options.mk
index 28697db4e70..fce4c441833 100644
--- a/math/z3/options.mk
+++ b/math/z3/options.mk
@@ -1,4 +1,4 @@
-# $NetBSD: options.mk,v 1.2 2018/03/11 06:14:45 dholland Exp $
+# $NetBSD: options.mk,v 1.3 2018/03/13 00:31:16 khorben Exp $
 
 PKG_OPTIONS_VAR=	PKG_OPTIONS.z3
 PKG_SUPPORTED_OPTIONS=	ocaml java
@@ -6,10 +6,12 @@ PKG_SUGGESTED_OPTIONS=	ocaml
 
 .include "../../mk/bsd.options.mk"
 
+PLIST_VARS+=		ocaml
 .if !empty(PKG_OPTIONS:Mocaml)
 CONFIGURE_ARGS+=	--ml
 .include "../../math/ocaml-num/buildlink3.mk"
 .include "../../lang/ocaml/buildlink3.mk"
+PLIST.ocaml=		yes
 .endif
 
 .if !empty(PKG_OPTIONS:Mjava)
diff --git a/math/z3/patches/patch-configure b/math/z3/patches/patch-configure
new file mode 100644
index 00000000000..78b4d967076
--- /dev/null
+++ b/math/z3/patches/patch-configure
@@ -0,0 +1,12 @@
+$NetBSD: patch-configure,v 1.1 2018/03/13 00:31:16 khorben Exp $
+
+Fix parameter expansion when configuring Z3.
+
+--- configure.orig	2016-11-07 22:02:30.000000000 +0000
++++ configure
+@@ -14,4 +14,4 @@ if ! $PYTHON -c "print('testing')" > /de
+    exit 1
+ fi
+ 
+-$PYTHON scripts/mk_make.py $*
++$PYTHON scripts/mk_make.py "$@"
diff --git a/math/z3/patches/patch-scripts_mk__util.py b/math/z3/patches/patch-scripts_mk__util.py
index 1b6b6f9f95b..939445db604 100644
--- a/math/z3/patches/patch-scripts_mk__util.py
+++ b/math/z3/patches/patch-scripts_mk__util.py
@@ -1,28 +1,209 @@
-$NetBSD: patch-scripts_mk__util.py,v 1.2 2018/02/23 17:04:43 khorben Exp $
+$NetBSD: patch-scripts_mk__util.py,v 1.3 2018/03/13 00:31:16 khorben Exp $
 
-For pkgsrc, use site-packages rather than dist-packages.
-Add support for DESTDIR.
-
-diff -r 59247c69b92d scripts/mk_util.py
---- scripts/mk_util.py.orig	2018-02-22 23:06:23.490379838 +0000
+--- scripts/mk_util.py.orig	2016-11-07 22:02:30.000000000 +0000
 +++ scripts/mk_util.py
-@@ -637,7 +637,7 @@ def parse_options():
+@@ -69,6 +69,7 @@ IS_WINDOWS=False
+ IS_LINUX=False
+ IS_OSX=False
+ IS_FREEBSD=False
++IS_NETBSD=False
+ IS_OPENBSD=False
+ IS_CYGWIN=False
+ IS_CYGWIN_MINGW=False
+@@ -95,6 +96,7 @@ VER_MINOR=None
+ VER_BUILD=None
+ VER_REVISION=None
+ PREFIX=sys.prefix
++DESTDIR=""
+ GMP=False
+ FOCI2=False
+ FOCI2LIB=''
+@@ -139,6 +141,9 @@ def is_linux():
+ def is_freebsd():
+     return IS_FREEBSD
+ 
++def is_netbsd():
++    return IS_NETBSD
++
+ def is_openbsd():
+     return IS_OPENBSD
+ 
+@@ -607,6 +612,8 @@ elif os.name == 'posix':
+         IS_LINUX=True
+     elif os.uname()[0] == 'FreeBSD':
+         IS_FREEBSD=True
++    elif os.uname()[0] == 'NetBSD':
++        IS_NETBSD=True
+     elif os.uname()[0] == 'OpenBSD':
+         IS_OPENBSD=True
+     elif os.uname()[0][:6] == 'CYGWIN':
+@@ -623,6 +630,7 @@ def display_help(exit_code):
+     print("  -s, --silent                  do not print verbose messages.")
+     if not IS_WINDOWS:
+         print("  -p <dir>, --prefix=<dir>      installation prefix (default: %s)." % PREFIX)
++	print("  -D <dir>, --destdir=<dir>     installation chroot (default: none).")
+     else:
+         print("  --parallel=num                use cl option /MP with 'num' parallel processes")
+     print("  --pypkgdir=<dir>              Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR)
+@@ -677,13 +685,13 @@ def display_help(exit_code):
+ # Parse configuration option for mk_make script
+ def parse_options():
+     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
+-    global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
++    global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, DESTDIR, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
+     global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
+     try:
+         options, remainder = getopt.gnu_getopt(sys.argv[1:],
+                                                'b:df:sxhmcvtnp:gj',
+                                                ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
+-                                                'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
++                                                'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'destdir=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
+                                                 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin'])
+     except:
+         print("ERROR: Invalid command line option")
+@@ -727,6 +735,8 @@ def parse_options():
              SLOW_OPTIMIZE = True
          elif not IS_WINDOWS and opt in ('-p', '--prefix'):
              PREFIX = arg
--            PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages')
-+            PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'site-packages')
-             mk_dir(DESTDIR + PYTHON_PACKAGE_DIR)
-             if sys.version >= "3":
-                 mk_dir(os.path.join(DESTDIR + PYTHON_PACKAGE_DIR, '__pycache__'))
-@@ -1506,8 +1506,8 @@ class MLComponent(Component):
-                         get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)',
-                         os.path.join(sub_dir, 'z3ml.cmxa'),
-                         os.path.join(sub_dir, 'META')))
--                out.write('\t%s remove Z3\n' % (OCAMLFIND))
--                out.write('\t%s install Z3 %s' % (OCAMLFIND, (os.path.join(sub_dir, 'META'))))
-+                out.write('\t%s remove -destdir $(DESTDIR)/ -ldconf ignore Z3\n' % (OCAMLFIND))
-+                out.write('\t%s install -destdir $(DESTDIR)/ -ldconf ignore Z3 %s' % (OCAMLFIND, (os.path.join(sub_dir, 'META'))))
-                 for m in modules:
-                     out.write(' %s.cma' % (os.path.join(sub_dir, m)))
-                     out.write(' %s.cmx' % (os.path.join(sub_dir, m)))
++        elif not IS_WINDOWS and opt in ('-D', '--destdir'):
++            DESTDIR = arg
+         elif opt in ('--pypkgdir'):
+             PYTHON_PACKAGE_DIR = arg
+         elif IS_WINDOWS and opt == '--parallel':
+@@ -1208,9 +1218,9 @@ class ExeComponent(Component):
+ 
+     def mk_unix_dist(self, build_path, dist_path):
+         if self.install:
+-            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
++            mk_dir(os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR))
+             shutil.copy(os.path.join(build_path, self.exe_name),
+-                        os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))
++                        os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.exe_name))
+ 
+ 
+ class ExtraExeComponent(ExeComponent):
+@@ -1227,7 +1237,7 @@ def get_so_ext():
+     sysname = os.uname()[0]
+     if sysname == 'Darwin':
+         return 'dylib'
+-    elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD':
++    elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'NetBSD' or sysname == 'OpenBSD':
+         return 'so'
+     elif sysname == 'CYGWIN':
+         return 'dll'
+@@ -1381,12 +1391,12 @@ class DLLComponent(Component):
+ 
+     def mk_unix_dist(self, build_path, dist_path):
+         if self.install:
+-            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
++            mk_dir(os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR))
+             so = get_so_ext()
+             shutil.copy('%s.%s' % (os.path.join(build_path, self.dll_name), so),
+-                        '%s.%s' % (os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name), so))
++                        '%s.%s' % (os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.dll_name), so))
+             shutil.copy('%s.a' % os.path.join(build_path, self.dll_name),
+-                        '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
++                        '%s.a' % os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.dll_name))
+ 
+ class PythonComponent(Component): 
+     def __init__(self, name, libz3Component):
+@@ -1403,7 +1413,7 @@ class PythonComponent(Component): 
+             return
+ 
+         src = os.path.join(build_path, 'python', 'z3')
+-        dst = os.path.join(dist_path, INSTALL_BIN_DIR, 'python', 'z3')
++        dst = os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, 'python', 'z3')
+         if os.path.exists(dst):
+             shutil.rmtree(dst)
+         shutil.copytree(src, dst)
+@@ -1701,11 +1711,11 @@ class DotNetDLLComponent(Component):
+ 
+     def mk_unix_dist(self, build_path, dist_path):
+         if is_dotnet_enabled():
+-            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
++            mk_dir(os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR))
+             shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
+-                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
++                        '%s.dll' % os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.dll_name))
+             shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
+-                        '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
++                        '%s.xml' % os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.dll_name))
+ 
+     def mk_install_deps(self, out):
+         if not is_dotnet_enabled():
+@@ -1776,6 +1786,8 @@ class JavaDLLComponent(Component):
+                 t = t.replace('PLATFORM', 'linux')
+             elif IS_FREEBSD:
+                 t = t.replace('PLATFORM', 'freebsd')
++            elif IS_NETBSD:
++                t = t.replace('PLATFORM', 'netbsd')
+             elif IS_OPENBSD:
+                 t = t.replace('PLATFORM', 'openbsd')
+             elif IS_CYGWIN:
+@@ -1827,12 +1839,12 @@ class JavaDLLComponent(Component):
+ 
+     def mk_unix_dist(self, build_path, dist_path):
+         if JAVA_ENABLED:
+-            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
++            mk_dir(os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR))
+             shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
+-                        '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name))
++                        '%s.jar' % os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.package_name))
+             so = get_so_ext()
+             shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
+-                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.%s' % so))
++                        os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, 'libz3java.%s' % so))
+ 
+     def mk_install(self, out):
+         if is_java_enabled() and self.install:
+@@ -2451,6 +2463,13 @@ def mk_config():
+             LDFLAGS        = '%s -lrt' % LDFLAGS
+             SLIBFLAGS      = '-shared'
+             SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
++        elif sysname == 'NetBSD':
++            CXXFLAGS       = '%s -fno-strict-aliasing -D_NETBSD_' % CXXFLAGS
++            OS_DEFINES     = '-D_NETBSD_'
++            SO_EXT         = '.so'
++            LDFLAGS        = '%s -lrt' % LDFLAGS
++            SLIBFLAGS      = '-shared'
++            SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
+         elif sysname == 'OpenBSD':
+             CXXFLAGS       = '%s -fno-strict-aliasing -D_OPENBSD_' % CXXFLAGS
+             OS_DEFINES     = '-D_OPENBSD_'
+@@ -2486,6 +2505,7 @@ def mk_config():
+             LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS
+                         
+         config.write('PREFIX=%s\n' % PREFIX)
++        config.write('DESTDIR=%s\n' % DESTDIR)
+         config.write('CC=%s\n' % CC)
+         config.write('CXX=%s\n' % CXX)
+         config.write('CXXFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS))
+@@ -2520,6 +2540,7 @@ def mk_config():
+             print('Arithmetic:     %s' % ARITH)
+             print('OpenMP:         %s' % HAS_OMP)
+             print('Prefix:         %s' % PREFIX)
++            print('Destdir:        %s' % DESTDIR)
+             print('64-bit:         %s' % is64())
+             print('FP math:        %s' % FPMATH)
+             print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR)
+@@ -2580,7 +2601,10 @@ def mk_makefile():
+     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 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 Use the following command to install Z3 at prefix $(PREFIX)")
++	if DESTDIR != "":
++	    out.write(" under destdir $(DESTDIR)")
++	out.write(".\n")
+         out.write('\t@echo "    sudo make install"\n\n')
+         # out.write("\t@echo If you are doing a staged install you can use DESTDIR.\n")
+         # out.write('\t@echo "    make DESTDIR=/some/temp/directory install"\n')
+@@ -3283,7 +3307,7 @@ def mk_unix_dist(build_path, dist_path):
+     # Add Z3Py to bin directory
+     for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
+         shutil.copy(os.path.join(build_path, pyc),
+-                    os.path.join(dist_path, INSTALL_BIN_DIR, pyc))
++                    os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, pyc))
+ 
+ class MakeRuleCmd(object):
+     """
diff --git a/math/z3/patches/patch-src_util_debug.cpp b/math/z3/patches/patch-src_util_debug.cpp
deleted file mode 100644
index 687509d9357..00000000000
--- a/math/z3/patches/patch-src_util_debug.cpp
+++ /dev/null
@@ -1,15 +0,0 @@
-$NetBSD: patch-src_util_debug.cpp,v 1.1 2016/07/16 04:02:13 markd Exp $
-
-gcc6 fix
-
---- src/util/debug.cpp.orig	2015-10-05 12:07:19.000000000 +0000
-+++ src/util/debug.cpp
-@@ -76,7 +76,7 @@ void invoke_gdb() {
-     for (;;) {
-         std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n";
-         char result;
--        bool ok = (std::cin >> result);
-+        bool ok = bool(std::cin >> result);
-         if (!ok) exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or unattached.
-         switch(result) {
-         case 'C':
diff --git a/math/z3/patches/patch-src_util_mpz.cpp b/math/z3/patches/patch-src_util_mpz.cpp
deleted file mode 100644
index d78ea9ecbc0..00000000000
--- a/math/z3/patches/patch-src_util_mpz.cpp
+++ /dev/null
@@ -1,15 +0,0 @@
-$NetBSD: patch-src_util_mpz.cpp,v 1.1 2016/07/16 04:02:13 markd Exp $
-
-gcc6 fix
-
---- src/util/mpz.cpp.orig	2015-10-05 12:07:19.000000000 +0000
-+++ src/util/mpz.cpp
-@@ -134,7 +134,7 @@ mpz_manager<SYNCH>::mpz_manager():
- #endif
-     
-     mpz one(1);
--    set(m_two64, UINT64_MAX);
-+    set(m_two64, (uint64)UINT64_MAX);
-     add(m_two64, one, m_two64);
- }
- 
diff --git a/math/z3/patches/patch-src_util_stopwatch.h b/math/z3/patches/patch-src_util_stopwatch.h
new file mode 100644
index 00000000000..e4ed347a72c
--- /dev/null
+++ b/math/z3/patches/patch-src_util_stopwatch.h
@@ -0,0 +1,16 @@
+$NetBSD: patch-src_util_stopwatch.h,v 1.1 2018/03/13 00:31:16 khorben Exp $
+
+--- src/util/stopwatch.h.orig	2016-11-07 22:02:30.000000000 +0000
++++ src/util/stopwatch.h
+@@ -130,6 +130,11 @@ public:
+ 
+ #include<ctime>
+ 
++#ifndef CLOCK_PROCESS_CPUTIME_ID
++/* BSD */
++# define CLOCK_PROCESS_CPUTIME_ID CLOCK_MONOTONIC
++#endif
++
+ class stopwatch {
+     unsigned long long m_time; // elapsed time in ns
+     bool               m_running;