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

Updated release notes

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-12-18 14:18:30 +00:00
parent c3add4eeda
commit b0aaa4c6d7
1 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
RELEASE_NOTES
View file

@ -2,6 +2,7 @@ RELEASE NOTES
Version 4.6.0 Version 4.6.0
============= =============
- New requirements: - New requirements:
- C++11 capable compiler to build Z3. - C++11 capable compiler to build Z3.
- C++ API now requires C++11 or newer. - C++ API now requires C++11 or newer.
@ -14,6 +15,10 @@ Version 4.6.0
issuing the command (get-objectives). Pareto front objectives are accessed by issuing the command (get-objectives). Pareto front objectives are accessed by
issuing multiple (check-sat) calls until it returns unsat. issuing multiple (check-sat) calls until it returns unsat.
- Removed features:
- Removed support for SMT-LIB 1.x
Version 4.5.0 Version 4.5.0
============= =============
@ -49,11 +54,10 @@ Version 4.5.0
over compound formulas, introduce a fresh predicate whose over compound formulas, introduce a fresh predicate whose
arguments are the relevant free variables in the formula and add a rule arguments are the relevant free variables in the formula and add a rule
that uses the fresh predicate in the head and formula in the body. that uses the fresh predicate in the head and formula in the body.
- minimization of unsat cores is avaialble as an option for the SAT and SMT cores. - Minimization of unsat cores is available as an option for the SAT and SMT cores.
By setting smt.core.minimize=true resp. sat.core.minimize=true By setting smt.core.minimize=true resp. sat.core.minimize=true
cores produced by these modules are minimized. cores produced by these modules are minimized.
- A multitude of bugs has been fixed. - A multitude of bugs has been fixed.