2.5.4

CHANGES:

• Fix a long-standing soundness issue in the FPA module (#1122, originally
  reported in #1111)
• Dolmen frontend incorrectly allowed semantic triggers outside of theory
  extensions (#1122)

2.5.3

CHANGES:

Build

• Require dolmen 0.9 #1050
• Test compatibility for OCaml 5.2 #1059

2.5.2

Bug fixes

• Hot fix for a soundness bug related with the distinct statement (#890)
• Treat missing values in models as abstract (#860)

2.5.1

Bug fixes

• fix a critical soundness bug with bvnot primitive (#819)

2.5.0

!!!!!!!!!!!!! WARNING !!!!!!!!!!!!!
This release contains a critical soundness bug with the bvnot primitive (see #819). We recommend to use a newer release.

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)

2.4.3

v2.4.3 (2023-04-27)

Build

• Restrict the requirement version of Ocplib-simplex (PR #573)
• Dune 3.0 or above is required, see ocaml/dune#5563 (PR #575)
• Zarith 1.4 or above is required
• Using js_of_ocaml with a version between 4.0.1 and 5.0.1 is required for
  the new package alt-ergo-js (PR #575)

Bug fixes

• Fix soundness issues in the arithmetic reasoner #476, #477, #479 (PR #573)

Regression fixes

• Remove flattening, see issues #505, #567 (PR #573)
• Using a weak table for the Shostak.combine cache to prevent some regressions (PR #573)

2.4.2

• Migrating to lablgtk3

• Update of CI

• Compatibility with dune.3+

• Miscellaneous bug fixes (type unification, term purification, ...)

2.4.1

• Improvement of term purification

• Implementation of a semantic term construction cache

• Replacement of Travis-CI by GitHub actions

• Improvement of documentation

• Unsoundness fixes

2.3.0-free

Prepare release of Alt-Ergo-Free 2.3.0

Release 2.4.0

Fix cmdliner man (#429) (#431)

* Fix error in parse_command for profiling option documentation

* Use with-stdout-to instead of with-outputs-to in dune command for manpage generation

* Fix Gui configuration file initialisation