diff --git a/CHANGES.md b/CHANGES.md index 7f502a09c..96aef1432 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,26 @@ ## unreleased +## v2.5.0 + +### New features +* add context reinitialisation (PR #490) +* add Dolmen frontend (PR #491,#541,#545) +* modernize the support for model generation (PR #530, #614, #659, #703, #614, #609, #755) +* support mutually recursive definitions in the native language (PR #549, #550) +* support of some options of the SMT-LIB statement (set-option) (PR #608) +* support for the (get-model) statement (required the Dolmen frontend) (PR #614) +* support the QF_BV and BV smtlib2 logic (PR #730, #733, #745). +* improve the ite preprocessing (simplification of some ites) (PR #731) + +### Build +* update to the new version of ocplib-simplex (0.5) +* remove the support of the deprecated library num. Alt-Ergo only uses Zarith (PR #600) +* remove the deprecated graphical interface (PR #601) + +### Bug fixes +* issue 475 -- Catch the exception I_dont_known in instantiation pass of SatML (PR #478) +* fix a memory leak in the vector module (PR #606) + ## v2.4.3 (2023-04-14) ### Build