From: A Tammy <openbsd.ports@aisha.cc>
Subject: Re: [update] math/z3: update to 4.13.0
To: OpenBSD ports <ports@openbsd.org>
Date: Mon, 26 Aug 2024 15:36:45 -0400


On 8/26/24 2:45 PM, Kirill A. Korinsky wrote:
> 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).


This sounds like a bug worthy of telling upstream about.


> 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
>
>