z3: Upgrade to 4.8.3

Eliminate merged patches.
Improve java support.

Patch by Michal Gorny.

Upstream changelog
==================
z3-4.8.3
This release covers
    bug fixes since 4.8.1
    .NET bindings for dotnet standard 1.4 on windows and 64 bit Linux systems and MacOs

z3-4.8.1
    New requirements:
        A breaking change to the API is that parsers for SMT-LIB2 formulas return a vector of
        formulas as opposed to a conjunction of formulas. The vector of formulas correspond to
        the set of "assert" instructions in the SMT-LIB input.

    New features
        A parallel mode is available for select theories, including QF_BV.
        By setting parallel.enable=true Z3 will spawn a number of worker threads proportional to the
        number of available CPU cores to apply cube and conquer solving on the goal.
        The SAT solver by default handle cardinality and PB constraints using a custom plugin
        that operates directly on cardinality and PB constraints.
        A "cube" interface is exposed over the solver API.
        Model conversion is first class over the textual API, such that subgoals created from running a
        solver can be passed in text files and a model for the original formula can be recreated from the result.
        This has also led to changes in how models are tracked over tactic subgoals. The API for
        extracting models from apply_result have been replaced.
        An optional mode handles xor constraints using a custom xor propagator.
        It is off by default and its value not demonstrated.
        The SAT solver includes new inprocessing techniques that are available during simplification.
        It performs asymmetric tautology elimination by default, and one can turn on more powerful inprocessing techniques
        (known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs.
        Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged
        as lemmas (redundant) and are garbage collected if their glue level is high.
        Substantial overhaul of the spacer horn clause engine.
        Added basic features to support Lambda bindings.
        Added model compression to eliminate local function definitions in models when
        inlining them does not incur substantial overhead. The old behavior, where models are left
        uncompressed can be replayed by setting the top-level parameter model_compress=false.
        Integration of a new solver for linear integer arithmetic and mixed linear integer arithmetic by Lev Nachmanson.
        It incorporates several improvements to QF_LIA solving based on
        . using a better LP engine, which is already the foundation for QF_LRA
        . including cuts based on Hermite Normal Form (thanks to approaches described
        in "cuts from proofs" and "cutting the mix").
        . extracting integer solutions from LP solutions by tightening bounds selectively.
        We use a generalization of Bromberger and Weidenbach that allows avoiding selected
        bounds tighthenings (https://easychair.org/publications/paper/qGfG).
        It solves significantly more problems in the QF_LIA category and may at this point also
        be the best solver for your problem as well.
        The new solver is enabled only for select SMT-LIB logics. These include QF_LIA, QF_IDL, and QF_UFLIA.
        Other theories (still) use the legacy solver for arithmetic. You can enable the new solver by setting
        the parameter smt.arith.solver=6 to give it a spin.

    Removed features:
        interpolation API
        duality engine for constrained Horn clauses.
        pdr engine for constrained Horn clauses. The engine's functionality has been
        folded into spacer as one of optional strategies.
        long deprecated API functions have been removed from z3_api.h

Z3 4.7.1. official release

    cumulative bug fix since 4.6.0
    minor version incremented as API now uses stdbool and stdint: bool and int64_t, uint64_t

Official release Z3 4.6.0.

11 files changed, 48 insertions, 352 deletions

diff --git a/math/z3/Makefile b/math/z3/Makefile
index b732c5dacdc..b1d40de8c34 100644
--- a/math/z3/Makefile
+++ b/math/z3/Makefile
@@ -1,8 +1,7 @@
-# $NetBSD: Makefile,v 1.12 2018/11/12 16:10:24 jaapb Exp $
+# $NetBSD: Makefile,v 1.13 2018/12/18 06:46:39 kamil Exp $
 
 .include "Makefile.common"
 
-PKGREVISION=	4
 COMMENT=	The Z3 theorem prover / SMT solver
 
 .include "options.mk"
diff --git a/math/z3/Makefile.common b/math/z3/Makefile.common
index 6e14c6dc3a5..90c69150aa7 100644
--- a/math/z3/Makefile.common
+++ b/math/z3/Makefile.common
@@ -1,9 +1,9 @@
-# $NetBSD: Makefile.common,v 1.3 2018/03/13 00:36:04 khorben Exp $
+# $NetBSD: Makefile.common,v 1.4 2018/12/18 06:46:39 kamil Exp $
 #
 # used by math/py-z3/Makefile
 # used by math/z3/Makefile
 
-DISTNAME=	z3-4.5.0
+DISTNAME=	z3-4.8.3
 GITHUB_TAG=	${DISTNAME}
 CATEGORIES=	math
 MASTER_SITES=	${MASTER_SITE_GITHUB:=Z3Prover/}
@@ -20,7 +20,5 @@ 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 3074ed3dcd5..5064ad012c0 100644
--- a/math/z3/PLIST
+++ b/math/z3/PLIST
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.2 2018/03/13 00:31:16 khorben Exp $
+@comment $NetBSD: PLIST,v 1.3 2018/12/18 06:46:39 kamil Exp $
 bin/z3
 include/z3++.h
 include/z3.h
@@ -7,12 +7,13 @@ 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_spacer.h
 include/z3_v1.h
+include/z3_version.h
 lib/libz3.so
 ${PLIST.ocaml}lib/ocaml/site-lib/Z3/META
 ${PLIST.ocaml}lib/ocaml/site-lib/Z3/dllz3ml.so
@@ -30,3 +31,5 @@ ${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
+${PLIST.java}lib/com.microsoft.z3.jar
+${PLIST.java}lib/libz3java.so
diff --git a/math/z3/buildlink3.mk b/math/z3/buildlink3.mk
index f382763f7cb..79e1566ebbb 100644
--- a/math/z3/buildlink3.mk
+++ b/math/z3/buildlink3.mk
@@ -1,11 +1,11 @@
-# $NetBSD: buildlink3.mk,v 1.2 2018/03/13 00:34:02 khorben Exp $
+# $NetBSD: buildlink3.mk,v 1.3 2018/12/18 06:46:39 kamil Exp $
 
 BUILDLINK_TREE+=	z3
 
 .if !defined(Z3_BUILDLINK3_MK)
 Z3_BUILDLINK3_MK:=
 
-BUILDLINK_API_DEPENDS.z3+=	z3>=4.5.0
+BUILDLINK_API_DEPENDS.z3+=	z3>=4.8.3
 BUILDLINK_PKGSRCDIR.z3?=	../../math/z3
 
 .endif  # Z3_BUILDLINK3_MK
diff --git a/math/z3/distinfo b/math/z3/distinfo
index 816b6cf26ee..302345a9410 100644
--- a/math/z3/distinfo
+++ b/math/z3/distinfo
@@ -1,11 +1,7 @@
-$NetBSD: distinfo,v 1.7 2018/10/01 11:21:03 jperkin Exp $
+$NetBSD: distinfo,v 1.8 2018/12/18 06:46:39 kamil Exp $
 
-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) = f3c6f13daeffb31e01f0ad50ca2c0dab2cdb87a2
-SHA1 (patch-src_interp_iz3interp.cpp) = d646a78e8469ea83829ad2f4b8bb2c4a9155e6f1
-SHA1 (patch-src_util_scoped__timer.cpp) = 68e0bdee94d54c93f3d493bf71abebcdccd921ba
-SHA1 (patch-src_util_stopwatch.h) = dbeab175ed4f507d5378f1966f8ed173c4c9a9a7
+SHA1 (z3-4.8.3.tar.gz) = bc713372c9be6808306a8e0844caf27c0a10ee2c
+RMD160 (z3-4.8.3.tar.gz) = 3b8bc18719725c0d110ca52f7e692519cbac341e
+SHA512 (z3-4.8.3.tar.gz) = 34a2dca0083ed469fdaf5ac062dda26248633245607ddd9ef90629c5f76ae30f87bfa4191c04ba9be7a617bf182a1bd00b59fd2274699e12ece69b86088c8044
+Size (z3-4.8.3.tar.gz) = 4119116 bytes
+SHA1 (patch-scripts_mk__util.py) = 59c17bbcd05be21089a89ae304662b69bd2a571d
diff --git a/math/z3/options.mk b/math/z3/options.mk
index fce4c441833..08bd7d057cc 100644
--- a/math/z3/options.mk
+++ b/math/z3/options.mk
@@ -1,4 +1,4 @@
-# $NetBSD: options.mk,v 1.3 2018/03/13 00:31:16 khorben Exp $
+# $NetBSD: options.mk,v 1.4 2018/12/18 06:46:39 kamil Exp $
 
 PKG_OPTIONS_VAR=	PKG_OPTIONS.z3
 PKG_SUPPORTED_OPTIONS=	ocaml java
@@ -6,7 +6,7 @@ PKG_SUGGESTED_OPTIONS=	ocaml
 
 .include "../../mk/bsd.options.mk"
 
-PLIST_VARS+=		ocaml
+PLIST_VARS+=		ocaml java
 .if !empty(PKG_OPTIONS:Mocaml)
 CONFIGURE_ARGS+=	--ml
 .include "../../math/ocaml-num/buildlink3.mk"
@@ -19,4 +19,5 @@ PLIST.ocaml=		yes
 USE_JAVA=	yes
 CONFIGURE_ARGS+=	--java
 .include "../../mk/java-vm.mk"
+PLIST.java=		yes
 .endif
diff --git a/math/z3/patches/patch-configure b/math/z3/patches/patch-configure
deleted file mode 100644
index 78b4d967076..00000000000
--- a/math/z3/patches/patch-configure
+++ /dev/null
@@ -1,12 +0,0 @@
-$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 870a6609405..67c64545952 100644
--- a/math/z3/patches/patch-scripts_mk__util.py
+++ b/math/z3/patches/patch-scripts_mk__util.py
@@ -1,230 +1,31 @@
-$NetBSD: patch-scripts_mk__util.py,v 1.4 2018/06/15 15:11:35 jperkin Exp $
+$NetBSD: patch-scripts_mk__util.py,v 1.5 2018/12/18 06:46:39 kamil Exp $
 
---- scripts/mk_util.py.orig	2016-11-07 22:02:30.000000000 +0000
+--- scripts/mk_util.py.orig	2018-12-15 09:28:53.381588998 +0000
 +++ scripts/mk_util.py
-@@ -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
- 
-@@ -603,16 +608,18 @@ elif os.name == 'posix':
-     if os.uname()[0] == 'Darwin':
-         IS_OSX=True
-         PREFIX="/usr/local"
--    elif os.uname()[0] == 'Linux':
--        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':
-         IS_CYGWIN=True
-         if (CC != None and "mingw" in CC):
-             IS_CYGWIN_MINGW=True
-+    else:
-+        IS_LINUX=True
- 
- def display_help(exit_code):
-     print("mk_make.py: Z3 Makefile generator\n")
-@@ -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
-+        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:
-@@ -2437,7 +2449,7 @@ def mk_config():
-         if sysname == 'Darwin':
-             SO_EXT    = '.dylib'
-             SLIBFLAGS = '-dynamiclib'
--        elif sysname == 'Linux':
-+        elif sysname == 'Linux' or sysname == 'SunOS':
-             CXXFLAGS       = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS
-             OS_DEFINES     = '-D_LINUX_'
-             SO_EXT         = '.so'
-@@ -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):
-     """
+@@ -2001,7 +2001,7 @@ class JavaDLLComponent(Component):
+                 out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' %
+                           os.path.join('api', 'java', 'Native'))
+             else:
+-                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
++                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) $(JAVA_LINK_EXTRA_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
+                           os.path.join('api', 'java', 'Native'))
+             out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
+             deps = ''
+@@ -2694,7 +2694,8 @@ def mk_config():
+         check_ar()
+         CXX = find_cxx_compiler()
+         CC  = find_c_compiler()
+-        SLIBEXTRAFLAGS = ''
++        SLIBEXTRAFLAGS = LDFLAGS
++        JAVALIBEXTRAFLAGS = LDFLAGS
+         EXE_EXT = ''
+         LIB_EXT = '.a'
+         if GPROF:
+@@ -2822,6 +2823,7 @@ def mk_config():
+         config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)
+         config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS)
+         config.write('SLINK_OUT_FLAG=-o \n')
++        config.write('JAVA_LINK_EXTRA_FLAGS=%s\n' % JAVALIBEXTRAFLAGS)
+         config.write('OS_DEFINES=%s\n' % OS_DEFINES)
+         if is_verbose():
+             print('Host platform:  %s' % sysname)
diff --git a/math/z3/patches/patch-src_interp_iz3interp.cpp b/math/z3/patches/patch-src_interp_iz3interp.cpp
deleted file mode 100644
index 31c9714d1f9..00000000000
--- a/math/z3/patches/patch-src_interp_iz3interp.cpp
+++ /dev/null
@@ -1,15 +0,0 @@
-$NetBSD: patch-src_interp_iz3interp.cpp,v 1.1 2018/10/01 11:21:03 jperkin Exp $
-
-rlim_t fixes.
-
---- src/interp/iz3interp.cpp.orig	2016-11-07 22:02:30.000000000 +0000
-+++ src/interp/iz3interp.cpp
-@@ -582,7 +582,7 @@ void interpolation_options_struct::apply
- class iz3stack_unlimiter {
- public:
-     iz3stack_unlimiter() {
--        struct rlimit rl = {RLIM_INFINITY, RLIM_INFINITY};
-+        struct rlimit rl = {(rlim_t)RLIM_INFINITY, (rlim_t)RLIM_INFINITY};
-         setrlimit(RLIMIT_STACK, &rl);
-         // nothing to be done if above fails
-     }
diff --git a/math/z3/patches/patch-src_util_scoped__timer.cpp b/math/z3/patches/patch-src_util_scoped__timer.cpp
deleted file mode 100644
index a8a93201b6f..00000000000
--- a/math/z3/patches/patch-src_util_scoped__timer.cpp
+++ /dev/null
@@ -1,59 +0,0 @@
-$NetBSD: patch-src_util_scoped__timer.cpp,v 1.1 2018/03/13 21:20:34 khorben Exp $
-
-Add support for NetBSD.
-
---- src/util/scoped_timer.cpp.orig	2016-11-07 22:02:30.000000000 +0000
-+++ src/util/scoped_timer.cpp
-@@ -33,8 +33,8 @@ Revision History:
- #include<sys/time.h>
- #include<sys/errno.h>
- #include<pthread.h>
--#elif defined(_LINUX_) || defined(_FREEBSD_)
--// Linux
-+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
-+// Linux & FreeBSD & NetBSD
- #include<errno.h>
- #include<pthread.h>
- #include<sched.h>
-@@ -66,8 +66,8 @@ struct scoped_timer::imp {
-     pthread_mutex_t  m_mutex;
-     pthread_cond_t   m_condition_var;
-     struct timespec  m_end_time;
--#elif defined(_LINUX_) || defined(_FREEBSD_)
--    // Linux & FreeBSD
-+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
-+    // Linux & FreeBSD & NetBSD
-     pthread_t       m_thread_id;
-     pthread_mutex_t m_mutex;
-     pthread_cond_t  m_cond;
-@@ -103,7 +103,7 @@ struct scoped_timer::imp {
- 
-         return st;
-     }
--#elif defined(_LINUX_) || defined(_FREEBSD_)
-+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
-     static void* thread_func(void *arg) {
-         scoped_timer::imp *st = static_cast<scoped_timer::imp*>(arg);
- 
-@@ -166,8 +166,8 @@ struct scoped_timer::imp {
- 
-         if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0)
-             throw default_exception("failed to start timer thread");
--#elif defined(_LINUX_) || defined(_FREEBSD_)
--        // Linux & FreeBSD
-+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
-+        // Linux & FreeBSD & NetBSD
-         m_ms = ms;
-         m_initialized = false;
-         ENSURE(pthread_mutex_init(&m_mutex, NULL) == 0);
-@@ -206,8 +206,8 @@ struct scoped_timer::imp {
-             throw default_exception("failed to destroy pthread condition variable");
-         if (pthread_attr_destroy(&m_attributes) != 0)
-             throw default_exception("failed to destroy pthread attributes object");
--#elif defined(_LINUX_) || defined(_FREEBSD_)
--        // Linux & FreeBSD
-+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
-+        // Linux & FreeBSD & NetBSD
-         bool init = false;
- 
-         // spin until timer thread has been created
diff --git a/math/z3/patches/patch-src_util_stopwatch.h b/math/z3/patches/patch-src_util_stopwatch.h
deleted file mode 100644
index e4ed347a72c..00000000000
--- a/math/z3/patches/patch-src_util_stopwatch.h
+++ /dev/null
@@ -1,16 +0,0 @@
-$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;