From: Kirill A. Korinsky <kirill@korins.ky>
Subject: Re: [update] math/z3: update to 4.13.0
To: Klemens Nanni <kn@openbsd.org>
Cc: OpenBSD ports <ports@openbsd.org>
Date: Fri, 30 Aug 2024 21:17:35 +0200

On Tue, 27 Aug 2024 21:59:25 +0200,
Klemens Nanni <kn@openbsd.org> wrote:
> 
> New diff including all the feedback above, you can now hack on the port and
> iterate over 'make retest' until it no longer crashes (or you give up)  ;-)
> 

Here an updated version based on yours. Changes:
 - improved testing to use smt2 models from examples;
 - switching to gcc to build it.

By some reason gcc produces z3 which works quite stable.

I suggest to keep it that way.

The diff:

diff --git math/z3/Makefile math/z3/Makefile
index e498cc1fd76..817b6a763de 100644
--- math/z3/Makefile
+++ math/z3/Makefile
@@ -1,16 +1,12 @@
 COMMENT =	Z3 theorem prover
 
-VERSION =	4.12.2
-REVISION =	1
-
 GH_ACCOUNT =	Z3Prover
 GH_PROJECT =	z3
-GH_TAGNAME =	${GH_PROJECT}-${VERSION}
+GH_TAGNAME =	${GH_PROJECT}-4.13.0
 
 DISTNAME =	${GH_TAGNAME}
-PKGNAME =	${DISTNAME:L}
 
-SHARED_LIBS =	z3			4.0 # 4.10
+SHARED_LIBS =	z3	4.1
 
 CATEGORIES =	math
 
@@ -19,25 +15,31 @@ WANTLIB +=	c m pthread ${COMPILER_LIBCXX}
 # MIT
 PERMIT_PACKAGE =	Yes
 
-# c++11
-COMPILER =	base-clang ports-gcc
+# C++17, clang lead to segfaults
+# See: https://github.com/Z3Prover/z3/issues/6902
+COMPILER =	ports-gcc
 
 MODULES =	devel/cmake \
 		lang/python
 
-CONFIGURE_ARGS +=	-DZ3_ENABLE_EXAMPLE_TARGETS=ON \
-			-DZ3_INCLUDE_GIT_HASH=OFF \
+MODPY_RUNDEP =	No
+
+CONFIGURE_ARGS =	-DZ3_BUILD_PYTHON_BINDINGS=ON \
+			-DZ3_ENABLE_EXAMPLE_TARGETS=ON \
 			-DZ3_INCLUDE_GIT_DESCRIBE=OFF \
-			-DZ3_BUILD_PYTHON_BINDINGS=ON \
+			-DZ3_INCLUDE_GIT_HASH=OFF \
 			-DZ3_USE_LIB_GMP=OFF
 
 DEBUG_PACKAGES = ${BUILD_PACKAGES}
 
 WRKDIST =	${WRKDIR}/z3-${DISTNAME}
 
-NO_TEST =	Yes
-
 pre-configure:
 	${SUBST_CMD} ${WRKSRC}/scripts/mk_util.py
 
+post-test:
+	@find ${WRKSRC}/examples/SMT-LIB2 \
+		-type f -name "*.smt2" \
+		-exec ${WRKBUILD}/z3 {} \;
+
 .include <bsd.port.mk>
diff --git math/z3/distinfo math/z3/distinfo
index 369d2943b90..eba5129710c 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
\ No newline at end of file
diff --git math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake
index e44cf3bdeae..04496bb1443 100644
--- math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake
+++ math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake
@@ -1,3 +1,5 @@
+Removed hardcoded optimizations
+
 Index: cmake/cxx_compiler_flags_overrides.cmake
 --- cmake/cxx_compiler_flags_overrides.cmake.orig
 +++ cmake/cxx_compiler_flags_overrides.cmake
diff --git math/z3/patches/patch-scripts_mk_util_py math/z3/patches/patch-scripts_mk_util_py
index c2470b83b54..ce6155a9cad 100644
--- math/z3/patches/patch-scripts_mk_util_py
+++ math/z3/patches/patch-scripts_mk_util_py
@@ -1,7 +1,11 @@
+- Remove hardcoded optimizations
+- Fix .so versioning
+- use -fPIC to build shared libs on all archs
+
 Index: scripts/mk_util.py
 --- scripts/mk_util.py.orig
 +++ scripts/mk_util.py
-@@ -2607,7 +2607,6 @@ def mk_config():
+@@ -2609,7 +2609,6 @@ def mk_config():
              EXAMP_DEBUG_FLAG = '-g'
              CPPFLAGS     = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
          else:
@@ -9,7 +13,7 @@ Index: scripts/mk_util.py
              if GPROF:
                  CXXFLAGS     += '-fomit-frame-pointer'
              CPPFLAGS     = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
-@@ -2632,7 +2631,7 @@ def mk_config():
+@@ -2634,7 +2633,7 @@ def mk_config():
              SO_EXT         = '.so'
              SLIBFLAGS      = '-shared'
          elif sysname == 'OpenBSD':
@@ -18,15 +22,12 @@ Index: scripts/mk_util.py
              SLIBFLAGS      = '-shared'
          elif sysname  == 'SunOS':
              SO_EXT         = '.so'
-@@ -2648,9 +2647,8 @@ def mk_config():
+@@ -2650,7 +2649,7 @@ def mk_config():
              LIB_EXT        = '.lib'
          else:
              raise MKException('Unsupported platform: %s' % sysname)
 -        if is64():
--            if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
--                CXXFLAGS     = '%s -fPIC' % CXXFLAGS
-+        if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
-+            CXXFLAGS     = '%s -fPIC' % CXXFLAGS
++        if true:
+             if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
+                 CXXFLAGS     = '%s -fPIC' % CXXFLAGS
          elif not LINUX_X64:
-             CXXFLAGS     = '%s -m32' % CXXFLAGS
-             LDFLAGS      = '%s -m32' % LDFLAGS
diff --git math/z3/pkg/PLIST math/z3/pkg/PLIST
index d152c2d5254..fd2b1201eaa 100644
--- math/z3/pkg/PLIST
+++ math/z3/pkg/PLIST
@@ -1,4 +1,4 @@
-@conflict py3-z3-solver-*
+@conflict ${MODPY_PY_PREFIX}z3-solver-*
 @bin bin/z3
 include/z3++.h
 include/z3.h


-- 
wbr, Kirill