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-11-11 16:29:13 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new.3759290 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Wed Nov 11 16:29:13 2026 rev:50 rq:1396668 version:5.4.0 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2026-10-30 18:22:54.021891697 +0100 +++ /work/SRC/openSUSE:Factory/.z3.new.3759290/z3.changes 2026-11-11 16:29:38.296716605 +0100 @@ -1,0 +2,24 @@ +Wed Nov 11 07:51:50 UTC 2026 - Jiri Slaby <[email protected]> + +- Update to 5.4.0 + * Add SMT-LIB integer exponentiation and refine total real power + semantics. + * Prevent model evaluation loops on symbolic division and modulo. + * Fix root comparisons for overlapping intervals and simplify bounds. + * Support Pareto optimization on real fronts and pre-optimize QE. + * Fix MaxSMT/pd-maxres soft weight accumulation and objective bounds. + * Improve FiniteSet simplification and reject oversized cardinalities. + * Fix recursive datatype cycles, recognizers, and sequence handling. + * Add smt.case_split_relevant_first and fix delayed-heap crashes. + * Fix small-format FP FMA significand extraction (e.g. FP(2,3)). + * Fix incremental SAT unsat cores and level-zero assumption tracking. + * Fix Spacer null models, query lifetime, and QBMC proof traces. + * Skip unsupported stages in proof pipelines without failing runs. + * Expand Lean and F*/Pulse proof reconstruction (arrays, sets, cuts). + * Fix empty input handling in Python PbEq, PbLe, and PbGe bindings. + * Saturate AST/API reference counts to avoid overflow under sharing. + * Java: add Linux ARM64, improve Maven/JAR bundling and lib caching. + * Release OCaml runtime lock during heavy checks and tactics. + * Build fixes for static libraries, CMake rules, and Windows paths. + +------------------------------------------------------------------- Old: ---- z3-5.3.3.tar.gz New: ---- z3-5.4.0.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.O3v7Sr/_old 2026-11-11 16:29:39.310759153 +0100 +++ /var/tmp/diff_new_pack.O3v7Sr/_new 2026-11-11 16:29:39.314759320 +0100 @@ -19,7 +19,7 @@ %define python_subpackage_only 1 %define sover %(echo %{version} | sed 's@\\([0-9]*\\)\\.\\([0-9]*\\)\\..*@\\1_\\2@') Name: z3 -Version: 5.3.3 +Version: 5.4.0 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT ++++++ _scmsync.obsinfo ++++++ --- /var/tmp/diff_new_pack.O3v7Sr/_old 2026-11-11 16:29:39.381762132 +0100 +++ /var/tmp/diff_new_pack.O3v7Sr/_new 2026-11-11 16:29:39.386762342 +0100 @@ -1,5 +1,5 @@ -mtime: 1793343356 -commit: fd688370ce8ae9f826e96019ea990824783506d9ca24b66e0ef3b3b7cc58eddb +mtime: 1794383668 +commit: 6194fa67f4142ff0dbbedf71c925499e84b5f01dc71b5ec29e3a667cbf70eea3 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-11-11 08:54:28.000000000 +0100 @@ -0,0 +1 @@ +.osc ++++++ z3-5.3.3.tar.gz -> z3-5.4.0.tar.gz ++++++ /work/SRC/openSUSE:Factory/z3/z3-5.3.3.tar.gz /work/SRC/openSUSE:Factory/.z3.new.3759290/z3-5.4.0.tar.gz differ: char 27, line 1
