alt-ergo
alt-ergo copied to clipboard
OCamlPro
OCamlPro public development repository for Alt-Ergo
From the [Debian build logs](https://buildd.debian.org/status/package.php?p=alt-ergo), there are failures on many architectures with the same error: ``` File "src/plugins/AB-Why3/dune", line 24, characters 5-22: 24 | (ABWhy3Plugin.cmxs as plugins/AB-Why3-plugin.cmxs) ^^^^^^^^^^^^^^^^^ Error: No...
It looks like `libgtksourceview2.0-dev`, needed to build `conf-gtksourceview`, is not available anymore on Ubuntu 22.04: ```bash $ opam install altgr-ergo [ERROR] Package conflict! * Missing dependency: - conf-gtksourceview depends on...
I found a bunch of regressions while migrating my tutorial about C program proofs with Frama-C from Alt-Ergo 2.4.0 to 2.4.1 (the same happens with the master branch). They seem...
Hi. I have a strange error this morning. See https://github.com/Deducteam/lambdapi/runs/4332121191?check_suite_focus=true. Alt-ergo fails when menhir is upgraded from 20211012 to 20211125 but opam info menhir mentions no 20211125 version for menhir...
While working on the Debian alt-ergo package, the tools complained: ``` E: alt-ergo: arch-dependent-file-in-usr-share usr/share/alt-ergo/plugins/AB-Why3-plugin.cmxs E: alt-ergo: arch-dependent-file-in-usr-share usr/share/alt-ergo/plugins/fm-simplex-plugin.cmxs ``` and indeed, if those files are arch-dependent, they should go...
Hi, I'm using alt-ergo (2.4.0). AE fails to prove, at least in a reasonable amount of time, the following simple case generated by Why3 (the goal is an axiom). After...
[co_2096_l.ae.txt](https://github.com/OCamlPro/alt-ergo/files/7032249/co_2096_l.ae.txt) Running Alt-Ergo on the attached file with: ``` alt-ergo --sat-solver CDCL co_2096_l.ae ``` causes a stack overflow in the call to Zarith's gcd function. The problem is probably in...
[c_651_l_bis.smt2.txt](https://github.com/OCamlPro/alt-ergo/files/6992216/c_651_l_bis.smt2.txt) [c_651_l_bis.ae.txt](https://github.com/OCamlPro/alt-ergo/files/6992217/c_651_l_bis.ae.txt) Alt-Ergo responds with "Valid" on the ".ae" file with the four solvers. And "I don't know" on the ".smt2" file when the CDCL solver is used, and "Valid"...
[c_735_l_bis.smt2.txt](https://github.com/OCamlPro/alt-ergo/files/6998557/c_735_l_bis.smt2.txt) [c_735_l_bis.ae.txt](https://github.com/OCamlPro/alt-ergo/files/6998558/c_735_l_bis.ae.txt) Responses: | | .smt2 | .ae | |-----------|-----------|-----------| | AE(T) | Valid | Valid | | AE(T-C) | Valid | Valid | | AE(C-T) | Valid |...