From 335e6f78e921f26ef5d229275f5f7984e5bbc5dd Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 21 Feb 2026 03:20:33 +0000 Subject: [PATCH 1/2] Initial plan From 611cd12faa2c9d881aa90b644d57b7686aa81252 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 21 Feb 2026 03:22:07 +0000 Subject: [PATCH 2/2] Add recommended release notes to RELEASE_NOTES.md for Version 4.17.0 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- RELEASE_NOTES.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 0e6acba9c..727013284 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -12,6 +12,15 @@ Version 4.17.0 It is possible to map a function over elements of a set using set.map. Support for set.range, set.map is partial. Support for set.size exists, but is without any optimization. The source code contains comments on ways to make it more efficient. File a GitHub issue if you want to contribute.s +- Add Python API convenience methods for improved usability. Thanks to Daniel Tang. + - Solver.solutions(t) method for finding all solutions to constraints, https://github.com/Z3Prover/z3/pull/8633 + - ArithRef.__abs__ alias to integrate with Python's abs() builtin, https://github.com/Z3Prover/z3/pull/8623 + - Improved error message in ModelRef.__getitem__ to suggest using eval(), https://github.com/Z3Prover/z3/pull/8626 + - Documentation example for Solver.sexpr(), https://github.com/Z3Prover/z3/pull/8631 +- Performance improvements by replacing unnecessary copy operations with std::move semantics for better efficiency. + Thanks to Nuno Lopes, https://github.com/Z3Prover/z3/pull/8583 +- Fix spurious sort error with nested quantifiers in model finder. `Fixes #8563` +- NLSAT optimizations including improvements to handle_nullified_poly and levelwise algorithm. Thanks to Lev Nachmanson. Version 4.16.0 ==============