Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2026-08-06 16:22:58 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new.16738 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Thu Aug 6 16:22:58 2026 rev:45 rq:1369669 version:5.0.0 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2025-05-30 17:28:12.322414028 +0200 +++ /work/SRC/openSUSE:Factory/.z3.new.16738/z3.changes 2026-08-06 16:24:22.088977746 +0200 @@ -1,0 +2,131 @@ +Thu Jul 23 10:24:45 UTC 2026 - Jiri Slaby <[email protected]> + +- update to 5.0.0: + * see: https://github.com/Z3Prover/z3/releases/tag/z3-5.0.0 + +------------------------------------------------------------------- +Thu Mar 12 17:56:50 UTC 2026 - Matej Cepl <[email protected]> + +- Update to 4.16.0: + - Add Go bindings to supported APIs +- Update to 4.15.8: + - Fix release pipeline to publish all supported python + wheels properly. + - Re-enable npm tokens for publishing npm pacages. +- Update to 4.15.7: + - Bug fix release +- Update to 4.15.6: + - Optimize mpz (multi-precision integer) implementation + using pointer tagging to reduce memory footprint and + improve performance. #8447, thanks to Nuno Lopes. + - Fix macOS install_name_tool issue by adding + -Wl,-headerpad_max_install_names linker flag to all dylib + builds. Resolves "larger updated load commands do not fit" + errors when modifying library install names on macOS. + #8535, fixes #7623 + - Optimize parameter storage by storing rational values + directly in variant instead of using pointers. Thanks to + Nuno Lopes. #8518 +- Update to 4.15.5: + - NLSAT now uses the Level wise algorithm for projection. + https://arxiv.org/abs/2212.09309 + - Add RCF (Real Closed Field) API to TypeScript bindings, + achieving feature parity with Python, Java, C++, and C# + implementations. The API includes 38 functions for exact + real arithmetic with support for π, e, algebraic roots, + and infinitesimals. #8225 + - Add sequence higher-order functions (map, fold) to Java, + C#, and TypeScript APIs. Functions include SeqMap, + SeqMapi, SeqFoldl, and SeqFoldli for functional + programming patterns over sequences. + Java API: #8226 + C# API: #8227 + TypeScript API included in #8228 + - Add benchmark export functionality to C# and TypeScript + APIs for exporting solver problems as SMTLIB2 benchmarks. + #8228 + - Fix UNKNOWN bug in search tree with inconsistent end state + during nonchronological backjumping. The fix ensures all + node closing occurs in backtrack to maintain consistency + between search tree and batch manager state. Thanks to + Ilana Shapiro. #8214 + - Fix segmentation fault in dioph_eq.cpp when processing + UFNIRA problems without explicit set-logic declarations. + Added bounds checks before accessing empty column vectors. + #8218, fixes #8208 + - Migrate build and release infrastructure from Azure + Pipelines to GitHub Actions, including CI workflows, + nightly builds, and release packaging. + - Bug fixes including #8195 + - Add functional datatype update operation to language + bindings. The datatype_update_field function enables + immutable updates to datatype fields, returning a modified + copy while preserving the original datatype value. #8500 + - Add comprehensive regex support to TypeScript API with 21 + functions including Re, Loop, Range, Union, Intersect, + Complement, and character class operations. Enables + pattern matching and regular expression constraints in + TypeScript applications. #8499 + - Add move constructor and move assignment operator to + z3::context class for efficient resource transfer. Enables + move semantics for context objects while maintaining + safety with explicit checks against moved-from usage. + #8508 + - Add solve_for and import_model_converter functions to C++ + solver API, achieving parity with Python API for LRA + variable solving. #8465 + - Add missing solver APIs to Java and C# bindings including + add_string, set_phase, get_units, get_non_units, and + get_levels methods. #8464 + - Add polymorphic datatype APIs to Java and ML bindings for + creating and manipulating parameterized datatypes. #8438, + #8378 #8507, #8467, #8494 + - Add SLS (Stochastic Local Search) tactic as a separate + worker thread for parallel solving. Thanks to Ilana + Shapiro. #8263 + - Add Windows ARM64 platform support for Python wheels, + expanding platform coverage for ARM-based Windows systems. + #8280 + - Optimize bitvector operations for large bitwidths by + avoiding unnecessary power-of-two computations in + has_sign_bit and mod2k operations. Thanks to Nuno Lopes. + - Optimize linear arithmetic solver with throttled + patch_basic_columns() calls, especially beneficial for + unsatisfiable cases. Thanks to Lev Nachmanson. + - Fix memory leak in undo_fixed_column when handling big + number cleanup. Thanks to Lev Nachmanson. + - Fix assertion violation in mpzzp_manager::eq from + non-normalized values during fresh variable peeking. #8439 + - Fix memory corruption in Z3_polynomial_subresultants API + where allocating result vector corrupted internal + converter mappings. Restructured to complete polynomial + computation before allocation. #8264, thanks to Lev + Nachmanson. + - Fix missing newline after attributes in + benchmark_to_smtlib_string output formatting. Thanks to + Josh Berdine. #8276 + - Fix NuGet packaging to handle dynamic glibc versions + across different Linux distributions. #8474 + - Preserve initial solver state with push/pop operations for + multiple objectives optimization. Thanks to Lev + Nachmanson. #8264 + +------------------------------------------------------------------- +Wed Mar 11 22:27:30 UTC 2026 - Matej Cepl <[email protected]> + +- Add support for generating of multiple versions of Python + subpackages (using %python_subpackage_only). +- Add python-z3-pyproject.toml and python-z3-setup.py for that. + +------------------------------------------------------------------- +Tue Feb 24 08:05:44 UTC 2026 - Jiri Slaby <[email protected]> + +- add _constraints as ppc64le failed with "No space left on device" + +------------------------------------------------------------------- +Sat Jan 3 20:34:28 UTC 2026 - Dirk Müller <[email protected]> + +- update to 4.15.4: + * see: https://github.com/Z3Prover/z3/releases/tag/z3-4.15.4 + +------------------------------------------------------------------- Old: ---- z3-4.15.0.tar.gz New: ---- _constraints python-z3-pyproject.toml python-z3-setup.py z3-5.0.0.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.q8RWEv/_old 2026-08-06 16:24:22.712999540 +0200 +++ /var/tmp/diff_new_pack.q8RWEv/_new 2026-08-06 16:24:22.716999680 +0200 @@ -1,7 +1,7 @@ # # spec file for package z3 # -# Copyright (c) 2025 SUSE LLC +# Copyright (c) 2026 SUSE LLC and contributors # # All modifications and additions to the file contributed by third parties # remain the property of their copyright owners, unless otherwise agreed @@ -16,36 +16,54 @@ # -%define sover %(echo %version | sed 's@\\([0-9]*\\)\\.\\([0-9]*\\)\\..*@\\1_\\2@') +%define python_subpackage_only 1 +%define sover %(echo %{version} | sed 's@\\([0-9]*\\)\\.\\([0-9]*\\)\\..*@\\1_\\2@') Name: z3 -Version: 4.15.0 +Version: 5.0.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 +Source0: https://github.com/Z3Prover/z3/archive/refs/tags/%{name}-%{version}.tar.gz +Source1: python-z3-pyproject.toml +Source2: python-z3-setup.py +# PATCH-FIX-UPSTREAM python-use-non-devel-so.patch bsc#1243028 [email protected] +# load libz3 with soversion (from gh#Z3Prover/z3#7518) Patch0: python-use-non-devel-so.patch -%if 0%{suse_version} < 1600 +BuildRequires: %{python_module devel} +BuildRequires: %{python_module pip} +BuildRequires: %{python_module setuptools >= 44} +BuildRequires: %{python_module wheel} +BuildRequires: cmake +BuildRequires: doxygen +BuildRequires: fdupes +BuildRequires: gcc-c++ +BuildRequires: graphviz +BuildRequires: help2man +BuildRequires: ninja +BuildRequires: pkgconfig +BuildRequires: python-rpm-macros +%{?python_enable_dependency_generator} +%if 0%{?suse_version} < 1600 BuildRequires: gcc13-c++ %else BuildRequires: c++_compiler %endif -BuildRequires: cmake -BuildRequires: ninja -BuildRequires: pkgconfig -BuildRequires: python3 %if 0%{?suse_version} > 1600 BuildRequires: pkgconfig(gmpxx) %else BuildRequires: gmp-devel %endif +%python_subpackages %description -Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates -several decision procedures: Linear real and integer arithmetic, -fixed-size bit vectors, uninterpreted functions, extensional arrays, -quantifiers and model generation. +Z3 is a satisfiability modulo theories (SMT) solver; given a set of +constraints with variables, it reports a set of values for those +variables that would meet the constraints. The Z3 input format is an +extension of the one defined by the SMT-LIB 2.0 standard. Z3 supports +arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, +uninterpreted functions, and quantifiers. %package -n libz3-%{sover} Summary: Library for the Z3 SMT theorem prover @@ -66,28 +84,33 @@ %description devel Development files for the Z3 library. -%package -n python3-%{name} -Summary: Python bindings for Z3 +%package -n python-%{name} +Summary: Python bindings for %{name} Group: Development/Languages/Python Requires: libz3-%{sover} = %{version} +Provides: python3-z3 = %{version}-%{release} +Obsoletes: python3-z3 < %{version}-%{release} BuildArch: noarch -%description -n python3-%{name} -Python bindings for the Z3 library. +%description -n python-%{name} +Z3 is a theorem prover from Microsoft Research. + +Python bindings for the module. %prep -%autosetup -p1 -n %{name}-%{name}-%{version} +%autosetup -p1 -n z3-z3-%{version} %build %define __builder ninja -%if 0%{suse_version} < 1600 +%if 0%{?suse_version} < 1600 export CXX=g++-13 %endif + %cmake \ -DZ3_BUILD_LIBZ3_SHARED=true \ -DZ3_USE_LIB_GMP=true \ -DZ3_BUILD_PYTHON_BINDINGS=true \ - -DZ3_INSTALL_PYTHON_BINDINGS=true \ + -DZ3_INSTALL_PYTHON_BINDINGS=false \ -DZ3_ENABLE_EXAMPLE_TARGETS=false \ %if 0%{?suse_version} >= 1550 -DZ3_LINK_TIME_OPTIMIZATION=true @@ -97,8 +120,23 @@ %cmake_build +mkdir -p python-wheel +cp %{SOURCE1} python-wheel/pyproject.toml +cp %{SOURCE2} python-wheel/setup.py +cp -a python/z3 python-wheel/ + +pushd python-wheel +export Z3_VERSION=%{version} +%pyproject_wheel +popd + %install %cmake_install +pushd build/python-wheel +%pyproject_install +popd + +%python_expand %fdupes %{buildroot}%{$python_sitelib} %check %ctest @@ -124,8 +162,9 @@ %{_libdir}/cmake/z3/Z3ConfigVersion.cmake %{_libdir}/cmake/z3/Z3Targets* -%files -n python3-%{name} +%files %{python_files z3} +%doc README.md %license LICENSE.txt -%dir %{python3_sitelib}/%{name} -%{python3_sitelib}/%{name}/*py +%{python_sitelib}/z3/ +%{python_sitelib}/z3_solver-%{version}*.dist-info/ ++++++ _constraints ++++++ <?xml version="1.0"?> <constraints> <hardware> <disk> <size unit="G">6</size> </disk> </hardware> </constraints> ++++++ _scmsync.obsinfo ++++++ --- /var/tmp/diff_new_pack.q8RWEv/_old 2026-08-06 16:24:22.765001356 +0200 +++ /var/tmp/diff_new_pack.q8RWEv/_new 2026-08-06 16:24:22.769001495 +0200 @@ -1,5 +1,5 @@ -mtime: 1748593522 -commit: f27a69259b39165def31925e884c2f7b7bbdfa7c4645c49d19800e91666f0f98 +mtime: 1784802467 +commit: 6751e9699520e43ef4c2781e2daa6262c7dfacaa7b90071847cf0bf8dfc709e3 url: https://src.opensuse.org/jirislaby/d-t-s-z3.git revision: factory ++++++ build.specials.obscpio ++++++ ++++++ build.specials.obscpio ++++++ diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/.gitignore new/.gitignore --- old/.gitignore 1970-01-01 01:00:00.000000000 +0100 +++ new/.gitignore 2026-07-23 12:27:47.000000000 +0200 @@ -0,0 +1 @@ +.osc ++++++ python-z3-pyproject.toml ++++++ [build-system] requires = ["setuptools>=40"] build-backend = "setuptools.build_meta" ++++++ python-z3-setup.py ++++++ import os from setuptools import setup setup( name="z3-solver", version=os.environ["Z3_VERSION"], description="Python bindings for the Z3 theorem prover", license="MIT", packages=["z3"], include_package_data=False, ) ++++++ z3-4.15.0.tar.gz -> z3-5.0.0.tar.gz ++++++ /work/SRC/openSUSE:Factory/z3/z3-4.15.0.tar.gz /work/SRC/openSUSE:Factory/.z3.new.16738/z3-5.0.0.tar.gz differ: char 12, line 1
