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

update release notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-18 11:21:51 -08:00
parent 5351640e97
commit 41a5b930b6
1 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

14
RELEASE_NOTES
View file

@ -3,14 +3,18 @@ RELEASE NOTES
Version 4.8.next
================
- Planned features
- specialized solver support for QF_ABV and ABV based on lazy SMT and dual reduction
- the smtfd solver and tactic implement this strategy, but is not prime for users.
- sat.euf
- a new CDCL core for SMT queries. It extends the SAT engine with theory solver plugins.
the current state is unstable. It lacks efficient ematching.
- polysat
- native word level bit-vector solving.
- introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
- circuit optimization techniques for BV in-processing are available as the sat.cut
option, but at this point does not translate into benefits. It is currently
turned off by default.
Version 4.8.13
==============
The release integrates various bug fixes and tuning.
Version 4.8.12
==============
Release provided to fix git tag discrepancy issues with 4.8.11