Accepting request 1281304 from devel:tools:statica

- add python-use-non-devel-so.patch (bsc#1243028)

- update to 4.15.0
  * see: https://github.com/Z3Prover/z3/releases/tag/z3-4.15.0

OBS-URL: https://build.opensuse.org/request/show/1281304
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/z3?expand=0&rev=44

_scmsync.obsinfo

@@ -0,0 +1,4 @@
+mtime: 1748593522
+commit: f27a69259b39165def31925e884c2f7b7bbdfa7c4645c49d19800e91666f0f98
+url: https://src.opensuse.org/jirislaby/d-t-s-z3.git
+revision: factory

build.specials.obscpio

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:bac0291b60e44a08accae8da3f51f4ed1153ecfbd2d6389a3bb16aeb9fcf2c10
+size 256

python-use-non-devel-so.patch

@@ -0,0 +1,135 @@
+From: https://github.com/sertonix
+Patch-mainline: submitted https://github.com/Z3Prover/z3/issues/7518
+Subject: Use sover for python bindings
+
+Don't use libz3.so, but use versioned lib like libz3.so.4.15.0
+
+---
+ scripts/update_api.py         |   33 +++++++++++++++++++++++++--------
+ src/api/python/CMakeLists.txt |    2 ++
+ 2 files changed, 27 insertions(+), 8 deletions(-)
+
+--- a/scripts/update_api.py
++++ b/scripts/update_api.py
+@@ -1823,9 +1823,10 @@ del _lib
+ del _default_dirs
+ del _all_dirs
+ del _ext
++del _sover
+ """)
+ 
+-def write_core_py_preamble(core_py):
++def write_core_py_preamble(core_py, z3py_soversion):
+   core_py.write(
+ """
+ # Automatically generated file
+@@ -1842,6 +1843,11 @@ from .z3consts import *
+ 
+ _file_manager = contextlib.ExitStack()
+ atexit.register(_file_manager.close)
++"""
++  )
++  core_py.write("_sover=\"%s\"\n" % z3py_soversion)
++  core_py.write(
++"""
+ _ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
+ _lib = None
+ _z3_lib_resource = importlib_resources.files('z3').joinpath('lib')
+@@ -1877,7 +1883,7 @@ for d in _all_dirs:
+   try:
+     d = os.path.realpath(d)
+     if os.path.isdir(d):
+-      d = os.path.join(d, 'libz3.%s' % _ext)
++      d = os.path.join(d, 'libz3.%s.%s' % (_ext, _sover))
+       if os.path.isfile(d):
+         _lib = ctypes.CDLL(d)
+         break
+@@ -1888,24 +1894,24 @@ for d in _all_dirs:
+ if _lib is None:
+   # If all else failed, ask the system to find it.
+   try:
+-    _lib = ctypes.CDLL('libz3.%s' % _ext)
++    _lib = ctypes.CDLL('libz3.%s.%s' % (_ext, _sover))
+   except Exception as e:
+     _failures += [e]
+     pass
+ 
+ if _lib is None:
+-  print("Could not find libz3.%s; consider adding the directory containing it to" % _ext)
++  print("Could not find libz3.%s.%s; consider adding the directory containing it to" % (_ext, _sover))
+   print("  - your system's PATH environment variable,")
+   print("  - the Z3_LIBRARY_PATH environment variable, or ")
+   print("  - to the custom Z3_LIB_DIRS Python-builtin before importing the z3 module, e.g. via")
+   if sys.version < '3':
+     print("    import __builtin__")
+-    print("    __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s" % _ext)
++    print("    __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s.%s" % (_ext, _sover))
+   else:
+     print("    import builtins")
+-    print("    builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s" % _ext)
++    print("    builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s.%s" % (_ext, _sover))
+   print(_failures)
+-  raise Z3Exception("libz3.%s not found." % _ext)
++  raise Z3Exception("libz3.%s.%s not found." % (_ext, _sover))
+ 
+ 
+ if sys.version < '3':
+@@ -1970,6 +1976,7 @@ core_py = None
+ def generate_files(api_files,
+                    api_output_dir=None,
+                    z3py_output_dir=None,
++                   z3py_soversion=None,
+                    dotnet_output_dir=None,
+                    java_input_dir=None,
+                    java_output_dir=None,
+@@ -2026,7 +2033,7 @@ def generate_files(api_files,
+           write_log_h_preamble(log_h)
+           write_log_c_preamble(log_c)
+           write_exe_c_preamble(exe_c)
+-          write_core_py_preamble(core_py)
++          write_core_py_preamble(core_py, z3py_soversion)
+ 
+           # FIXME: these functions are awful
+           apiTypes.def_Types(api_files)
+@@ -2069,6 +2076,10 @@ def main(args):
+                       dest="z3py_output_dir",
+                       default=None,
+                       help="Directory to emit z3py files. If not specified no files are emitted.")
++  parser.add_argument("--z3py-soversion",
++                      dest="z3py_soversion",
++                      default=None,
++                      help="SOVERSION for loading libz3 library.")
+   parser.add_argument("--dotnet-output-dir",
+                       dest="dotnet_output_dir",
+                       default=None,
+@@ -2095,6 +2106,11 @@ def main(args):
+                       help="Directory to emit OCaml files. If not specified no files are emitted.")
+   pargs = parser.parse_args(args)
+ 
++  if pargs.z3py_output_dir:
++    if pargs.z3py_soversion is None:
++      logging.error('--z3py-soversion must be specified')
++      return 1
++
+   if pargs.java_output_dir:
+     if pargs.java_package_name == None:
+       logging.error('--java-package-name must be specified')
+@@ -2116,6 +2132,7 @@ def main(args):
+   generate_files(api_files=pargs.api_files,
+                  api_output_dir=pargs.api_output_dir,
+                  z3py_output_dir=pargs.z3py_output_dir,
++                 z3py_soversion=pargs.z3py_soversion,
+                  dotnet_output_dir=pargs.dotnet_output_dir,
+                  java_input_dir=pargs.java_input_dir,
+                  java_output_dir=pargs.java_output_dir,
+--- a/src/api/python/CMakeLists.txt
++++ b/src/api/python/CMakeLists.txt
+@@ -36,6 +36,8 @@ add_custom_command(OUTPUT "${z3py_bindin
+   COMMAND "${Python3_EXECUTABLE}"
+     "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
+     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
++    "--z3py-soversion"
++    ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}
+     "--z3py-output-dir"
+     "${z3py_bindings_build_dest}"
+   DEPENDS

z3-4.13.3.tar.gz

@@ -1,3 +0,0 @@
-version https://git-lfs.github.com/spec/v1
-oid sha256:f59c9cf600ea57fb64ffeffbffd0f2d2b896854f339e846f48f069d23bc14ba0
-size 5583533

z3.changes

@@ -1,3 +1,35 @@
+-------------------------------------------------------------------
+Fri May 30 08:22:16 UTC 2025 - Jiri Slaby <jslaby@suse.cz>
+
+- add python-use-non-devel-so.patch (bsc#1243028)
+
+-------------------------------------------------------------------
+Fri May 30 07:12:24 UTC 2025 - Jiri Slaby <jslaby@suse.cz>
+
+- update to 4.15.0
+  * see: https://github.com/Z3Prover/z3/releases/tag/z3-4.15.0
+
+-------------------------------------------------------------------
+Fri Mar 28 09:24:36 UTC 2025 - Jiri Slaby <jslaby@suse.cz>
+
+- update to 4.14.1
+  * Add ubv_to_int, sbv_to_int, int_to_bv to SMTLIB2 API.
+  * Fix nuget package regression omitting Microsoft.Z3.* files
+  * SLS modulo theories engine v1 release.
+  * API for accessing term depth and groundness.
+  * Two fixes to relevancy propagation.
+  * A new API for solving LRA variables modulo constraints.
+  * Performance and bug fixes.
+  * several updates to emscripten including #7473
+  * add preliminary pyodie build
+  * address issues with Java bindings
+  * Include start of sls-smt functionality SLS modulo theories
+
+-------------------------------------------------------------------
+Mon Oct 14 09:42:25 UTC 2024 - Jiri Slaby <jslaby@suse.cz>
+
+- build with g++-13 on < 1600 (z3 needs c++20)
+
 -------------------------------------------------------------------
 Sat Oct 12 15:35:21 UTC 2024 - Andrea Manzini <andrea.manzini@suse.com>
 

z3.spec

@@ -1,7 +1,7 @@
 #
 # spec file for package z3
 #
-# Copyright (c) 2024 SUSE LLC
+# Copyright (c) 2025 SUSE LLC
 #
 # All modifications and additions to the file contributed by third parties
 # remain the property of their copyright owners, unless otherwise agreed
@@ -16,20 +16,25 @@
 #
 
 
-%define sover 4_13
+%define sover %(echo %version | sed 's@\\([0-9]*\\)\\.\\([0-9]*\\)\\..*@\\1_\\2@')
 Name:           z3
-Version:        4.13.3
+Version:        4.15.0
 Release:        0
 Summary:        Theorem prover from Microsoft Research
 License:        MIT
 Group:          Productivity/Scientific/Other
 URL:            https://github.com/Z3Prover/z3/wiki
 Source0:        https://github.com/Z3Prover/z3/archive/z3-%{version}.tar.gz
+Patch0:         python-use-non-devel-so.patch
+%if 0%{suse_version} < 1600
+BuildRequires:  gcc13-c++
+%else
 BuildRequires:  c++_compiler
+%endif
 BuildRequires:  cmake
 BuildRequires:  ninja
 BuildRequires:  pkgconfig
-BuildRequires:  python3-devel
+BuildRequires:  python3
 %if 0%{?suse_version} > 1600
 BuildRequires:  pkgconfig(gmpxx)
 %else
@@ -75,8 +80,10 @@ Python bindings for the Z3 library.
 
 %build
 %define __builder ninja
+%if 0%{suse_version} < 1600
+export CXX=g++-13
+%endif
 %cmake \
-  -DPYTHON_EXECUTABLE=%{_bindir}/python3 \
   -DZ3_BUILD_LIBZ3_SHARED=true \
   -DZ3_USE_LIB_GMP=true \
   -DZ3_BUILD_PYTHON_BINDINGS=true \