3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00

Added release notes for the upcoming 4.5.0 release

This commit is contained in:
Christoph M. Wintersteiger 2016-11-04 19:39:53 +00:00
parent 856cf7d4f9
commit 19858c44b2

View file

@ -1,5 +1,22 @@
RELEASE NOTES
Version 4.5.0
=============
- New features:
- New theories of strings and sequences.
- Incremental consequence finder for finite domains.
- CMake build system (thanks @delcypher).
- Updated and improved OCaml API (thanks @martin-neuhaeusser).
- Updated and improved Java API (thanks @cheshire).
- New resource limit facilities to avoid non-deterministic timeout behaviour.
- New bit-vector simplification and ackermannization tactics (thanks @MikolasJanota, @nunoplopes).
- QSAT: a new solver for quantified arithmetic problems. See:
Bjorner, Janota: Playing with Quantified Satisfaction, LPAR 2016.
- A multitude of bugs has been fixed.
Version 4.4.1
=============