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

update release notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-10 04:05:08 -07:00
parent 1c7d27bdf3
commit ee00542e76
1 changed files with 14 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
RELEASE_NOTES
View file

@ -5,7 +5,6 @@ Version 4.8.next
- Planned features - Planned features
- rewritten arithmetic solver replacing legacy arithmetic solver and on by default - rewritten arithmetic solver replacing legacy arithmetic solver and on by default
- self-contained character theory, direct support for UTF8, Unicode character sets - self-contained character theory, direct support for UTF8, Unicode character sets
- improvements to regular expression processing
- specialized solver support for QF_ABV and ABV based on lazy SMT and dual reduction - 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. - the smtfd solver and tactic implement this strategy, but is not prime for users.
- introduction of simple induction lemmas to handle a limited repertoire of induction proofs. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
@ -13,6 +12,20 @@ Version 4.8.next
option, but at this point does not translate into benefits. It is currently option, but at this point does not translate into benefits. It is currently
turned off by default. turned off by default.
Version 4.8.9
=============
- New features
- significant improvements to regular expression solving
- expose user theory plugin. It is a leaner user theory plugin that was once available.
It allows for registering callbacks that react to when bit-vector and Boolean variables
receive fixed values.
- Bug fixes
- many
- Notes
- the new arithmetic theory is turned on by default. It _does_ introduce regressions on
several scenarios, but has its own advantages. Users can turn on the old solver by setting smt.arith.solver=2.
Depending on feedback, we may turn toggle this default setting again back to smt.arith.solver=2.
Version 4.8.8 Version 4.8.8
============= =============
- New features - New features