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-17 16:59:32 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new.1258 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Mon Aug 17 16:59:32 2026 rev:46 rq:1371532 version:5.1.0 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2026-08-06 16:24:22.088977746 +0200 +++ /work/SRC/openSUSE:Factory/.z3.new.1258/z3.changes 2026-08-17 17:02:54.512333002 +0200 @@ -1,0 +2,45 @@ +Mon Aug 17 07:39:34 UTC 2026 - Martin Pluskal <[email protected]> + +- Update to 5.1.0: + * New monadic regex solver, enabled by default + (smt.seq.regex_monadic=true): live-state traversal and + interval-refinement products, with semilinear length + abstraction for regular expressions + * seq_monadic gained a configurable read orientation for regex + memberships, a light Antimirov cofactor mode, depth-first + DNF replacement and unsat-core extraction + * Soundness fixes for intblast on array-derived bit-vector + equalities (smt.bv.solver=2), str.at inside regular + expressions, ill-sorted UF rewriting in fpa2bv for + quantified Float32 arrays, and the elim-term-ite simplifier + * Arithmetic: LP-based nonlinear bound optimization for + cross-nested conflicts, re-linearization of violated + monomials at final check, fixes to mod divisibility lemmas + and to algebraic root accessors + * Fixed strict optimization objectives losing strict-real + suprema on the LRA path, smtlib2_compliant mode answering + unknown instead of unsat, and parallel mode giving up + immediately on QF_BV + * Performance: cheaper per-cell bignum allocation in HNF + pivoting, no full-column rescan per delta halving in + lar_solver model init, object-local arithmetic parameters + in Optimize + * Python bindings now load the versioned libz3 and fall back + to the unversioned name +- Rename the library subpackage libz3-5_0 to libz3-5_1, + following the upstream SONAME change from libz3.so.5.0 to + libz3.so.5.1; PrusaSlicer links libz3 and needs a rebuild +- Drop python-use-non-devel-so.patch: upstream 5.1.0 implements + the same soversion-aware library loading in the generated + Python bindings (bsc#1243028) +- Run the upstream unit test suite in the check section - it + registers no ctest tests, so the previous ctest call tested + nothing +- Spec cleanup: + * Drop the dead suse_version < 1600 conditionals - Leap 15.6 + is EOL and its repository is disabled for this package + * Drop the unused doxygen, graphviz and help2man + BuildRequires - no documentation target is built + * Declare the cmake >= 3.16 floor that upstream requires + +------------------------------------------------------------------- Old: ---- python-use-non-devel-so.patch z3-5.0.0.tar.gz New: ---- z3-5.1.0.tar.gz ----------(Old B)---------- Old: libz3.so.5.1; PrusaSlicer links libz3 and needs a rebuild - Drop python-use-non-devel-so.patch: upstream 5.1.0 implements the same soversion-aware library loading in the generated ----------(Old E)---------- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.pAvxQD/_old 2026-08-17 17:02:55.284360231 +0200 +++ /var/tmp/diff_new_pack.pAvxQD/_new 2026-08-17 17:02:55.288360372 +0200 @@ -19,37 +19,25 @@ %define python_subpackage_only 1 %define sover %(echo %{version} | sed 's@\\([0-9]*\\)\\.\\([0-9]*\\)\\..*@\\1_\\2@') Name: z3 -Version: 5.0.0 +Version: 5.1.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/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 BuildRequires: %{python_module devel} BuildRequires: %{python_module pip} BuildRequires: %{python_module setuptools >= 44} BuildRequires: %{python_module wheel} -BuildRequires: cmake -BuildRequires: doxygen +BuildRequires: c++_compiler +BuildRequires: cmake >= 3.16 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 %if 0%{?suse_version} > 1600 BuildRequires: pkgconfig(gmpxx) %else @@ -67,7 +55,6 @@ %package -n libz3-%{sover} Summary: Library for the Z3 SMT theorem prover -Group: System/Libraries %description -n libz3-%{sover} Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates @@ -78,7 +65,6 @@ %package devel Summary: Development files for Z3 -Group: Development/Languages/C and C++ Requires: libz3-%{sover} = %{version} %description devel @@ -86,7 +72,6 @@ %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} @@ -102,21 +87,13 @@ %build %define __builder ninja -%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=false \ -DZ3_ENABLE_EXAMPLE_TARGETS=false \ -%if 0%{?suse_version} >= 1550 -DZ3_LINK_TIME_OPTIMIZATION=true -%else - -DZ3_LINK_TIME_OPTIMIZATION=false -%endif %cmake_build @@ -139,7 +116,16 @@ %python_expand %fdupes %{buildroot}%{$python_sitelib} %check -%ctest +# Upstream calls neither enable_testing() nor add_test(), so %%ctest finds no +# tests at all. The unit tests live in the EXCLUDE_FROM_ALL target test-z3, +# which has to be built and invoked explicitly ("/a" = run all of them). +# The Python singlespec macros stash the CMake build directory away as +# _build.tmp while they switch flavours in %%install, so restore it first. +[ -d %{__builddir} ] || mv _build.tmp %{__builddir} +pushd %{__builddir} +%cmake_build test-z3 +./test-z3 /a +popd %ldconfig_scriptlets -n libz3-%{sover} ++++++ _scmsync.obsinfo ++++++ --- /var/tmp/diff_new_pack.pAvxQD/_old 2026-08-17 17:02:55.364363052 +0200 +++ /var/tmp/diff_new_pack.pAvxQD/_new 2026-08-17 17:02:55.370363264 +0200 @@ -1,5 +1,5 @@ -mtime: 1784802467 -commit: 6751e9699520e43ef4c2781e2daa6262c7dfacaa7b90071847cf0bf8dfc709e3 +mtime: 1786955373 +commit: 525b4d585d28ee8e998e2c11e9e314f751f5a9fe73e9c2650985a933ad082808 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-08-17 10:29:33.000000000 +0200 @@ -0,0 +1 @@ +.osc ++++++ z3-5.0.0.tar.gz -> z3-5.1.0.tar.gz ++++++ /work/SRC/openSUSE:Factory/z3/z3-5.0.0.tar.gz /work/SRC/openSUSE:Factory/.z3.new.1258/z3-5.1.0.tar.gz differ: char 15, line 1
