-
Notifications
You must be signed in to change notification settings - Fork 33
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Finalize release 2.5.0 #754
Conversation
CHANGES.md
Outdated
* 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) | ||
* use Dune >= 3.5. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Wait, do we?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I thought we chose to stay on 3.0 in #729
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
CHANGES.md
Outdated
### New features | ||
* add context reinitialisation (PR #490) | ||
* add Dolmen frontend (PR #491,#541,#545) | ||
* add model generation (PR #530) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
CHANGES.md
Outdated
* 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 ground reasoning with some bitvector primitives (PR #730, #733, #745). |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not "some" bitvector primitives -- this should be titled "Support the QF_BV and BV smtlib2 logic" or something similar
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sorry for the two passes, I got distracted while doing the first pass.
This PR contains the new change log for the release 2.5.0.