3 files changed, 5 insertions, 82 deletions

diff --git a/math/z3/Makefile b/math/z3/Makefile
index 0df189d2514f..5a42937e41d7 100644
--- a/math/z3/Makefile
+++ b/math/z3/Makefile
@@ -1,6 +1,6 @@
 PORTNAME=	z3
 DISTVERSIONPREFIX=	z3-
-DISTVERSION=	4.10.2
+DISTVERSION=	4.12.1
 CATEGORIES=	math
 
 MAINTAINER=	arrowd@FreeBSD.org
@@ -18,7 +18,7 @@ HAS_CONFIGURE=		yes
 CONFIGURE_ARGS=		--prefix=${PREFIX}
 USE_LDCONFIG=		yes
 
-OPTIONS_DEFINE=		DEBUG STATIC GMP
+OPTIONS_DEFINE=		STATIC GMP
 
 OPTIONS_SUB=		yes
 
diff --git a/math/z3/distinfo b/math/z3/distinfo
index c1d82694683f..9fec410ddec3 100644
--- a/math/z3/distinfo
+++ b/math/z3/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1660222509
-SHA256 (Z3Prover-z3-z3-4.10.2_GH0.tar.gz) = 889fd035b833775c8cd2eb4723eb011bf916a3e9bf08ce66b31c548acee7a321
-SIZE (Z3Prover-z3-z3-4.10.2_GH0.tar.gz) = 5367336
+TIMESTAMP = 1676206397
+SHA256 (Z3Prover-z3-z3-4.12.1_GH0.tar.gz) = a3735fabf00e1341adcc70394993c05fd3e2ae167a3e9bb46045e33084eb64a3
+SIZE (Z3Prover-z3-z3-4.12.1_GH0.tar.gz) = 5470095
diff --git a/math/z3/files/patch-src_util_memory__manager.cpp b/math/z3/files/patch-src_util_memory__manager.cpp
deleted file mode 100644
index 8616f05b8f5a..000000000000
--- a/math/z3/files/patch-src_util_memory__manager.cpp
+++ /dev/null
@@ -1,77 +0,0 @@
-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