diff --git a/RELEASE_NOTES b/RELEASE_NOTES index e85e3d8d6a2..4f10cad26d7 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -2,6 +2,7 @@ RELEASE NOTES Version 4.6.0 ============= + - New requirements: - C++11 capable compiler to build Z3. - 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 multiple (check-sat) calls until it returns unsat. +- Removed features: + - Removed support for SMT-LIB 1.x + + Version 4.5.0 ============= @@ -49,10 +54,9 @@ Version 4.5.0 over compound formulas, introduce a fresh predicate whose 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. - - 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 - cores produced by these modules are minimized. - + cores produced by these modules are minimized. - A multitude of bugs has been fixed.