diff --git a/math/z3/Makefile b/math/z3/Makefile
index 529069510a96..ef4734375840 100644
--- a/math/z3/Makefile
+++ b/math/z3/Makefile
@@ -1,45 +1,45 @@
 PORTNAME=	z3
 DISTVERSIONPREFIX=	z3-
-DISTVERSION=	4.8.16
+DISTVERSION=	4.8.17
 CATEGORIES=	math
 
 MAINTAINER=	arrowd@FreeBSD.org
 COMMENT=	Z3 Theorem Prover
 
 LICENSE=	MIT
 LICENSE_FILE=	${WRKSRC}/LICENSE.txt
 
 USES=		compiler:c++11-lang python:build
 USE_GITHUB=	yes
 GH_ACCOUNT=	Z3Prover
 
 HAS_CONFIGURE=		yes
 CONFIGURE_ARGS=		--prefix=${PREFIX}
 USE_LDCONFIG=		yes
 
 OPTIONS_DEFINE=		DEBUG STATIC GMP
 
 OPTIONS_SUB=		yes
 
 DEBUG_CONFIGURE_ON=	--debug
 DEBUG_VARS=		with_debug=yes
 
 STATIC_DESC=		Build static z3 library
 STATIC_CONFIGURE_ON=	--staticlib
 
 GMP_DESC=		Use GMP library for AP arithmetic
 GMP_CONFIGURE_ON=	--gmp
 GMP_USES=		localbase:ldflags
 GMP_LIB_DEPENDS=	libgmp.so:math/gmp
 
 CXXFLAGS_powerpc=	-fPIC
 LDFLAGS_i386=		-Wl,-znotext
 BUILD_WRKSRC=		${WRKSRC}/build
 INSTALL_WRKSRC=		${WRKSRC}/build
 
 post-install:
 	${STRIP_CMD} ${STAGEDIR}${PREFIX}/bin/z3
 	${STRIP_CMD} ${STAGEDIR}${PREFIX}/lib/libz3.so
 	${LN} -s libz3.so ${STAGEDIR}${PREFIX}/lib/libz3.so.0
 
 .include <bsd.port.mk>
diff --git a/math/z3/distinfo b/math/z3/distinfo
index f5d61a2521c8..d1a05ca2b821 100644
--- a/math/z3/distinfo
+++ b/math/z3/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1651515677
-SHA256 (Z3Prover-z3-z3-4.8.16_GH0.tar.gz) = 75f95e09f3f35fef746e571d5ec88a4efba27f1bc8f1a0ef1117167486ec3dc6
-SIZE (Z3Prover-z3-z3-4.8.16_GH0.tar.gz) = 5223980
+TIMESTAMP = 1653058564
+SHA256 (Z3Prover-z3-z3-4.8.17_GH0.tar.gz) = 1e57637ce8d5212fd38453df28e2730a18e0a633f723682267be87f5b858a126
+SIZE (Z3Prover-z3-z3-4.8.17_GH0.tar.gz) = 5232392
diff --git a/math/z3/files/patch-scripts_mk__util.py b/math/z3/files/patch-scripts_mk__util.py
index 43e8bd1f6537..0d3cfd52b146 100644
--- a/math/z3/files/patch-scripts_mk__util.py
+++ b/math/z3/files/patch-scripts_mk__util.py
@@ -1,13 +1,22 @@
---- scripts/mk_util.py.orig	2019-09-19 23:43:06 UTC
+--- scripts/mk_util.py.orig	2022-05-05 00:16:30 UTC
 +++ scripts/mk_util.py
-@@ -2508,8 +2508,8 @@ def mk_config():
+@@ -2543,8 +2543,8 @@ def mk_config():
          check_ar()
          CXX = find_cxx_compiler()
          CC  = find_c_compiler()
 -        SLIBEXTRAFLAGS = ''
 -#       SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS
 +#       SLIBEXTRAFLAGS = ''
 +        SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS
          EXE_EXT = ''
          LIB_EXT = '.a'
          if GPROF:
+@@ -2632,7 +2632,7 @@ def mk_config():
+         if is64():
+             if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
+                 CXXFLAGS     = '%s -fPIC' % CXXFLAGS
+-            if sysname == 'Linux':
++            if sysname == 'Linux' or sysname == 'FreeBSD':
+                 CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS
+         elif not LINUX_X64:
+             CXXFLAGS     = '%s -m32' % CXXFLAGS
diff --git a/math/z3/files/patch-src_util_memory__manager.cpp b/math/z3/files/patch-src_util_memory__manager.cpp
new file mode 100644
index 000000000000..8616f05b8f5a
--- /dev/null
+++ b/math/z3/files/patch-src_util_memory__manager.cpp
@@ -0,0 +1,77 @@
+Z3 memory manager stores actual data along with its size, which causes the
+memory to be 8-byte aligned. Use malloc non-portable functions to obtain
+memory region size instead.
+
+https://github.com/Z3Prover/z3/issues/6015
+
+--- src/util/memory_manager.cpp.orig	2022-05-05 00:16:30 UTC
++++ src/util/memory_manager.cpp
+@@ -13,6 +13,7 @@ --*/
+ #include "util/error_codes.h"
+ #include "util/debug.h"
+ #include "util/scoped_timer.h"
++#include <malloc_np.h>
+ // The following two function are automatically generated by the mk_make.py script.
+ // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
+ // For example, rational.h contains
+@@ -258,52 +259,43 @@ void memory::deallocate(void * p) {
+ }
+ 
+ void memory::deallocate(void * p) {
+-    size_t * sz_p  = reinterpret_cast<size_t*>(p) - 1;
+-    size_t sz      = *sz_p;
+-    void * real_p  = reinterpret_cast<void*>(sz_p);
+-    g_memory_thread_alloc_size -= sz;
+-    free(real_p);
++    g_memory_thread_alloc_size -= malloc_usable_size(p);
++    if (g_memory_thread_alloc_size < 0) g_memory_thread_alloc_size = 0;
++    free(p);
+     if (g_memory_thread_alloc_size < -SYNCH_THRESHOLD) {
+         synchronize_counters(false);
+     }
+ }
+ 
+ void * memory::allocate(size_t s) {
+-    s = s + sizeof(size_t); // we allocate an extra field!
+     void * r = malloc(s);
+     if (r == 0) {
+         throw_out_of_memory();
+         return nullptr;
+     }
+-    *(static_cast<size_t*>(r)) = s;
+     g_memory_thread_alloc_size += s;
+     g_memory_thread_alloc_count += 1;
+     if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
+         synchronize_counters(true);
+     }
+ 
+-    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
++    return r; // we return a pointer to the location after the extra field
+ }
+ 
+ void* memory::reallocate(void *p, size_t s) {
+-    size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
+-    size_t sz = *sz_p;
+-    void *real_p = reinterpret_cast<void*>(sz_p);
+-    s = s + sizeof(size_t); // we allocate an extra field!
+-
+-    g_memory_thread_alloc_size += s - sz;
++    g_memory_thread_alloc_size += s - malloc_usable_size(p);
++    if (g_memory_thread_alloc_size < 0) g_memory_thread_alloc_size = 0;
+     g_memory_thread_alloc_count += 1;
+     if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
+         synchronize_counters(true);
+     }
+ 
+-    void *r = realloc(real_p, s);
++    void *r = realloc(p, s);
+     if (r == 0) {
+         throw_out_of_memory();
+         return nullptr;
+     }
+-    *(static_cast<size_t*>(r)) = s;
+-    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
++    return r;
+ }
+ 
+ #else