Pierre Villemot
Pierre Villemot
This umbrella issue tracks the progression of the BV theory reasoning. Please add related issue here and what we plan to improve in the future. - [X] Support of `bvnot`...
I open this issue because I was trying to solve properly the issue #778 yesterday and I got stuck with the SAT solver API. We know that Alt-Ergo produces partial...
The current style used in the codebase is very inconsistent. Basile and I want to switch to ocamlformat. I know some of you dislike it but we can configure it...
Alt-Ergo supports a subset of the why3 format as input through the plugin AB-why3, see https://ocamlpro.github.io/alt-ergo/Plugins/index.html#ab-why3-plugins. This feature can be activated by using the option `--add-solver` in order to add...
The PR https://github.com/OCamlPro/alt-ergo/commit/fb6b7f27ff047d0236be1fd70b9c7f2add783fa7 fixes a cache in `Shostak.ml` that prevents to recreate semantic values. We don't know if this cache improves the performances. We should test it.
The current situation of the output management in AE is a bit of a mess. Basically, the Alt-Ergo library should never print anything by itself. Such behaviour isn't expected from...
This issue follows the clean-up of the documentation. - [ ] Porting the Sphinx documentation to Odoc format. - [ ] Write a complete ebnf description of the Alt-Ergo native...
After #584, we stop building and testing Alt-Ergo on Windows with Cygwin. It seems that we have users on Windows. We should build and test AE on Windows again.