mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

update release notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-04-23 20:02:07 +01:00
parent bd6b3027cd
commit 39f57fb7ca
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
RELEASE_NOTES
View file

@ -10,6 +10,20 @@ Version 4.8.next
- native word level bit-vector solving. - native word level bit-vector solving.
- 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.
Version 4.8.16
==============
- initial support for Darwin Arm64 (for M1, M2, .. users) thanks to zwimer and Anja Petkovi'c
Komel for updates.
Java is not yet supported, pypi native arm64 distributions are not yet supported.
cmake dependency added to enable users to build for not-yet-supported platforms directly;
specifically M1 seems to come up.
- added functionality to user propagator decisions. Thanks to Clemens Eisenhofer.
- added options for rc2 and maxres-bin to maxsat (note that there was no real difference measured
from maxres on MaxSAT unweighted so default option is unchanged)
- improved search for mutex constraints (at-most-1 constraints) among soft
constraints for maxsat derived from approach used in rc2 sample.
- multiple merges
Version 4.8.15 Version 4.8.15
============== ==============
- elaborate user propagator API. Change id based scheme to expressions - elaborate user propagator API. Change id based scheme to expressions