-
Notifications
You must be signed in to change notification settings - Fork 49
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
Upgrade testsuite to alt-ergo 2.5.3 #978
Comments
(currently looking at this... there are a few quirks related to creusot setup that need solving, but no fundamental blocker afaict) |
Implemented in #1005 (using some manual transformations in red_black_tree that could be removed after https://gitlab.inria.fr/why3/why3/-/issues/854 is fixed). |
Do you want to close this issue now? Or after the why3 issue is closed? |
I'll close this now, and open a different issue to remember to clean up the red_black_tree session eventually. |
Thanks to @bclement-ocp we'll soon have redistribuable binary builds of alt-ergo to use in
creusot setup
. (cf OCamlPro/alt-ergo#1045).Before that we need to upgrade creusot's testsuite to use the latest alt-ergo version, 2.5.3.
Xavier has a tool to do this kind of solver upgrade in batch: https://github.com/xldenis/why3-tools/ (https://github.com/xldenis/why3-tools/blob/master/bin/upgrade.ml)
invocation example:
dune exec why3_tools -- upgrade -L/Users/xavier/Code/creusot/prelude/ --upgrade=Alt-Ergo,2.4.1=Alt-Ergo,2.4.2 ~/Code/creusot/creusot/tests/should_succeed/bug/271.mlcfg
The text was updated successfully, but these errors were encountered: