Re: [update] math/z3: update to 4.13.0

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