From: Kirill A. Korinsky <kirill@korins.ky>
Subject: Re: [update] math/z3: update to 4.13.0
To: OpenBSD ports <ports@openbsd.org>
Cc: Klemens Nanni <kn@openbsd.org>
Date: Mon, 26 Aug 2024 20:45:16 +0200

ports@,

Here an update version of this diff

On Wed, 21 Aug 2024 00:30:09 +0200,
Kirill A. Korinsky <kirill@korins.ky> wrote:
> 
> ports@,
> 
> Here is a clean update of math/z3 to the latest release.
> 
> Changelog:
>  https://github.com/Z3Prover/z3/releases/tag/z3-4.13.0
> 
> Tested on -current/amd64.
> 
> So the crashing problem is still here, see:
> https://github.com/Z3Prover/z3/issues/6902
> 
> But it exists on the current version in ports, which means the update
> doesn't break anything new.
>

After spending some time to dig into the issue which lead to crash, I had
discovered that such crash doesn't reproduced if I build z3 wihtout
optimization (-O0).

During that time I had noticed and fixed a few cases with broken stack...
Unfortently it doesn't help with the crash.

So, here an updated diff which builds z3 without optimization. It, probably,
works slower but I can't crash it anymore.

I suggest to keep it that way, until it's fixed.

An updated diff:

diff --git math/z3/Makefile math/z3/Makefile
index e498cc1fd76..5aa42b953cc 100644
--- math/z3/Makefile
+++ math/z3/Makefile
@@ -1,7 +1,6 @@
 COMMENT =	Z3 theorem prover
 
-VERSION =	4.12.2
-REVISION =	1
+VERSION =	4.13.0
 
 GH_ACCOUNT =	Z3Prover
 GH_PROJECT =	z3
@@ -10,7 +9,7 @@ GH_TAGNAME =	${GH_PROJECT}-${VERSION}
 DISTNAME =	${GH_TAGNAME}
 PKGNAME =	${DISTNAME:L}
 
-SHARED_LIBS =	z3			4.0 # 4.10
+SHARED_LIBS =	z3			4.1 # 4.13
 
 CATEGORIES =	math
 
@@ -31,6 +30,10 @@ CONFIGURE_ARGS +=	-DZ3_ENABLE_EXAMPLE_TARGETS=ON \
 			-DZ3_BUILD_PYTHON_BINDINGS=ON \
 			-DZ3_USE_LIB_GMP=OFF
 
+# Debug build, optimized build crashes
+# See: https://github.com/Z3Prover/z3/issues/6902
+MODCMAKE_DEBUG =	Yes
+
 DEBUG_PACKAGES = ${BUILD_PACKAGES}
 
 WRKDIST =	${WRKDIR}/z3-${DISTNAME}
diff --git math/z3/distinfo math/z3/distinfo
index 369d2943b90..22c9ca84d8a 100644
--- math/z3/distinfo
+++ math/z3/distinfo
@@ -1,2 +1,2 @@
-SHA256 (z3-4.12.2.tar.gz) = n1jzcQvSCUCFlRp1eRVQ9UeQPXX+fi/LNzxfA/x2G48=
-SIZE (z3-4.12.2.tar.gz) = 5401038
+SHA256 (z3-4.13.0.tar.gz) = AbzGHINi43u4n9JDD34zheht95FQGb0s5F3p2b2TRQI=
+SIZE (z3-4.13.0.tar.gz) = 5520232


-- 
wbr, Kirill