alt-ergo
alt-ergo copied to clipboard
OCamlPro
OCamlPro public development repository for Alt-Ergo
The following example is not proved without the axiomatisation of Why3 over the modulo operator ( [test_mod.zip](https://github.com/OCamlPro/alt-ergo/files/5282161/test_mod.zip)) ``` goal G1 : (forall a:int. forall b:int. (((0
Running Alt-Ergo 2.3.2 on the attached file raises the following error : `Fatal error: exception File "lib/reasoners/shostak.ml", line 491, characters 12-18: Assertion failed`. [bug.zip](https://github.com/OCamlPro/alt-ergo/files/4982722/bug.zip)
I think this is already the case for goals name (when we have more than one goal per file, To be checked), but not for axioms: - forbid having more...
This is not a bug. But when options `--no-theory` or `--no-ematching` are set, the E-matching engine should not query/use theories to find substitutions modulo. With the following command: ``` alt-ergo...
In the first iteration: - extension of Alt-Ergo's native input language - support of ADTs in the frontend (parsing, typechecking, hashconsed structure) via native language and via PSMT2 - basic...
The graphical interface of alt-ergo (i.e. altgr-ergo), is relatively heavy to maintain and imposes many restrictions on development, so we are currently considering removing it entirely from the project. Before...
Following the recent addition of [Gbury/dolmen](https://github.com/Gbury/dolmen) (that will allow alt-ergo to more input languages such as smtlib, tptp, etc...), we are considering potentially removing the support for dynlinked parsers, as...
As I user I would like a windows/linux/MacOS installer, such that I can just download, install, and use the alt-ergo problem solver. The current way to use alt-ergo force me...
