alt-ergo
alt-ergo copied to clipboard
OCamlPro
OCamlPro public development repository for Alt-Ergo
[c_685_l.smt2.txt](https://github.com/OCamlPro/alt-ergo/files/6992923/c_685_l.smt2.txt) [c_685_l.ae.txt](https://github.com/OCamlPro/alt-ergo/files/6992924/c_685_l.ae.txt) The .ae and .smt2 files are supposed to be equivalent. Alt-Ergo responds with "Valid" (on both the ".ae" and the ".smt2" files) when the Tableaux or the Tableaux-CDCL...
[c_1130_l_bis.ae.txt](https://github.com/OCamlPro/alt-ergo/files/6982313/c_1130_l_bis.ae.txt) Running the command: ``` ./alt-ergo --sat-solver CDCL c_1130_l_bis.ae ``` Causes the following error: ``` Fatal error: exception File "src/lib/reasoners/satml_frontend.ml", line 1019, characters 13-19: Assertion failed ``` And when the...
Assertion failure in "src/lib/reasoners/intervalCalculus.ml", line 1175, when using the CDCL solver
[c_262_0_ae_bis.ae.txt](https://github.com/OCamlPro/alt-ergo/files/6955011/c_262_0_ae_bis.ae.txt) Running Alt-Ergo (built from the "next" branch) on the attached file with the command: ``` ./alt-ergo --sat-solver CDCL c_262_0_ae_bis.ae ``` Causes the following error: ``` Fatal error: exception File...
Commit ID: ac84c736c27b1f1d3ede360d0a36e9b40d8899b2 File: AE-format/why3-no-split/binary_multiplication-BinaryMultiplication63-VC_binary_mult.ae.zip Reason: case-split for an integer expression extracted from the simplex is a non-integer constant, although it's equal to min/max bound.
Add an artifact section in both the README and the Alt-Ergo website. This section should automatically recover artifacts created by the CI (webworker, windows binary ...). This could ease the...
As a first step to organize debug messages in Alt-Ergo, here is a first handling log messages.
On timeout, SAT solvers (probably) return `Unknown {env; timeout_reason}`, where `timeout_reason` is one of {Assume, ProofSearch, ModelGen} ``` type timeout_reason = | NoTimeout | Assume | ProofSearch | ModelGen ```...