Skip to content

2.5.0
Compare
Choose a tag to compare
@Halbaroth Halbaroth released this 06 Sep 15:18
· 337 commits to next since this release
v2.5.0
a5ce941
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.

!!!!!!!!!!!!! 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)
Assets 3
Loading