mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

updated release notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-02-18 15:03:24 -08:00
parent fb6ec7d5e7
commit dda60737dc
1 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
RELEASE_NOTES.md
View file

@ -4,17 +4,13 @@ Version 4.next
================ ================
- Planned features - Planned features
- sat.euf - sat.euf
- a new CDCL core for SMT queries. It extends the SAT engine with theory solver plugins. - CDCL core for SMT queries. It extends the SAT engine with theory solver plugins.
the current state is unstable. It lacks efficient ematching. - add global incremental pre-processing for the legacy core.
- polysat
- native word level bit-vector solving.
- introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
Version 4.14.1 Version 4.14.1
============== ==============
- Improved integer cut algorithms for linear integer arithmetic. - Improved integer cut algorithms for linear integer arithmetic.
Version 4.14.0 Version 4.14.0
============== ==============
- [SLS modulo theories](https://microsoft.github.io/z3guide/programming/Local%20Search/) engine v1 release. - [SLS modulo theories](https://microsoft.github.io/z3guide/programming/Local%20Search/) engine v1 release.