mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 00:07:36 +00:00
Code Activity

Merge pull request #8714 from Z3Prover/copilot/update-release-notes

Browse source 
Add release notes for Version 4.17.0 (Python API, perf, bug fixes)
This commit is contained in:
Nikolaj Bjorner 2026-02-20 19:24:35 -08:00 • committed by GitHub
commit 14b88cc583
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
RELEASE_NOTES.md
View file

@ -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
==============