alt-ergo
alt-ergo copied to clipboard
OCamlPro
OCamlPro public development repository for Alt-Ergo
This issue is a remainder to unlock the version of Dolmen before the next release. See #893
This issue is a reminder to all things we have to do to get a clean `check-all-sat` feature. - [ ] supporting `check-all-sat` with the solver `FunSAT`. As I explained...
This PR adds the support for the `check-all-sat` support. I think we can merge the PR without clean-up its implementation as the feature doesn't break the classical model generation. Please...
After many months, I realize my `gentest` script doesn't fit our demands well. I plan to rewrite a simpler one soon.
See PR https://github.com/OCamlPro/alt-ergo/pull/747
The `cut` and `check` primitives are not supported with the Dolmen frontend. Part of the reason is that Dolmen does not type `cut` and `check`. ```shell $ cat check_cut.ae goal...
When we have (dis|in)equalities between `int2bv` / `bv2nat` terms we should propagate the relevant information to the other theory. For instance, if we have `bv2nat(x) = bv2nat(y)`, we should be...
While I was porting the documentation of AE from Sphinx to odoc, I noticed there is no support for the `ac` modifier in the SMT-LIB input format. I create this...