mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

update release notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-16 10:21:06 -08:00
parent cbac860387
commit 2bf595cb8f
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
RELEASE_NOTES
View file

@ -1,11 +1,27 @@
RELEASE NOTES RELEASE NOTES
Version 4.8.next
================
- Planned features
- rewritten NIA (non-linear integer arithmetic) core solver
- self-contained character theory, direct support for UTF8, Unicode character sets
- recursive function representation without hoisting ite expressions. Issue #2601
- specialized solver support for QF_ABV and ABV based on lazy SMT and dual reduction
- model-based interpolation for quantifier-free UF, arithmetic, arrays
- circuit optimization techniques for BV pre-processing
Version 4.8.7 Version 4.8.7
=============
- New features - New features
- setting parameter on solver over the API by - setting parameter on solver over the API by
solver.smtlib2_log=<filename> solver.smtlib2_log=<filename>
enables tracing calls into the solver as SMTLIB2 commands. enables tracing calls into the solver as SMTLIB2 commands.
It traces, assert, push, pop, check_sat, get_consequences. It traces, assert, push, pop, check_sat, get_consequences.
- Notes
- various bug fixes
- rewmove model_compress. Use model.compact
- print weights with quantifiers when weight is != 1
Version 4.8.6 Version 4.8.6
============= =============