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-10-30 18:16:05 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new.1255 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Fri Oct 30 18:16:05 2026 rev:49 rq:1393811 version:5.3.3 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2026-10-29 16:11:25.048836848 +0100 +++ /work/SRC/openSUSE:Factory/.z3.new.1255/z3.changes 2026-10-30 18:22:54.021891697 +0100 @@ -1,0 +2,21 @@ +Fri Oct 30 06:53:41 UTC 2026 - Jiri Slaby <[email protected]> + +- Update to 5.3.3 + * Packaging/Java: Add bundled-native and universal JARs; improve Bazel/CMake + packaging + * MaxSMT: Improve performance via LP relaxation of hard constraints + (opt.maxres.lp_relaxation) + * Core/Arithmetic: Fix transcendental soundness, Real-to-FP rounding, and + modular inverse rewrites + * Theories: Fixes for BV modulus/rotations, datatypes, finite-set + cardinality, and sequence limits + * Robustness: Harden C API validation against crashes; fix division-by-zero + on zero parameters + * Spacer: Fix min-cut loops and preserve negated bounds in bound-expansion + generalizer + * Proofs: Expand F*/Pulse proof checking (finite fields, BV, arrays) and Lean + reconstruction + * Bindings: Fix JS/Wasm static registrations, OCaml link inputs, and Python + install paths + +------------------------------------------------------------------- Old: ---- z3-5.3.2.tar.gz New: ---- z3-5.3.3.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.cf8QTT/_old 2026-10-30 18:22:55.315945869 +0100 +++ /var/tmp/diff_new_pack.cf8QTT/_new 2026-10-30 18:22:55.320946078 +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.2 +Version: 5.3.3 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT ++++++ _scmsync.obsinfo ++++++ --- /var/tmp/diff_new_pack.cf8QTT/_old 2026-10-30 18:22:55.435950892 +0100 +++ /var/tmp/diff_new_pack.cf8QTT/_new 2026-10-30 18:22:55.440951101 +0100 @@ -1,5 +1,5 @@ -mtime: 1793254678 -commit: f492d66e91143ff84cfc5f10c18494490aa8f696ff59569c3b101291d770f486 +mtime: 1793343356 +commit: fd688370ce8ae9f826e96019ea990824783506d9ca24b66e0ef3b3b7cc58eddb 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-10-30 07:55:56.000000000 +0100 @@ -0,0 +1 @@ +.osc ++++++ z3-5.3.2.tar.gz -> z3-5.3.3.tar.gz ++++++ /work/SRC/openSUSE:Factory/z3/z3-5.3.2.tar.gz /work/SRC/openSUSE:Factory/.z3.new.1255/z3-5.3.3.tar.gz differ: char 28, line 1
