alt-ergo
alt-ergo copied to clipboard
OCamlPro
OCamlPro public development repository for Alt-Ergo
FYI, we worked a little bit on porting Frama-C to Windows in Opam 2.2. We had to fix zlib and gmp which are also necessary for Alt-Ergo but we could...
As discussed at the user's club meeting. Off the top of my head this is: - Shostak primitives (records, enums, addition/subtraction/scaling/comparison for arithmetic, extract/concat for BV) - Multiplication (through interval...
Following discussion at the user's club we should implement a soft timeout at least for optimization to return the best model so far when the soft timeout is reached. The...
See #1133: > Currently, the --strict option only disables optimization. It should also disable extensions such as ae.round and bv2nat / int2bv.
There seems to be an issue with how binary releases are produced, in that the `--version` they return is the hash of the corresponding git commit, instead of a version...
I'm trying to install alt-ergo and meet the following problem: ``` #=== ERROR while compiling alt-ergo.2.5.3 =====================================# Processing actions 🐫 ⬇ retrieved alt-ergo.2.5.3 (cached) [ERROR] The compilation of alt-ergo.2.5.3 failed...
Hello, [repr.ae.txt](https://github.com/OCamlPro/alt-ergo/files/15304733/repr.ae.txt) On the attached reproducer, Alt-Ergo runs for a long time, despite specifying a low steps number: ``` $ alt-ergo repr.ae --steps-bound=200 ... runs for several minutes ... ```...
The semantic splitting functionality introduced in #1027 is currently unused due to regressions in the arithmetic theory. Some of the problems it solves (notably the ability to have more communication...
None of the versions on opam alt-ergo-free or the branches marked -free in github are licensed under CeCILL-C, but the license section of the documentation did not reflect this. Additionally...
