Pierre Villemot
Pierre Villemot
In fact the incompleteness has no relation with the ADT theory. If you run `Alt-Ergo` without model generation on the input file: ```smt2 (set-logic ALL) (declare-datatype Data ( (cons1 (d1...
We may add a special function in `Relation` to perform case-split for boolean values as we do for the solver in `Shostak`.
We'll remove this feature when we get rid of the legacy parser. As the legacy parser is deprecated in `v2.6.0` and this feature works only with the legacy parser, we...
Finally, this PR is ready for a first review! I rewrote the algorithm for sorting constructors, see the new module `Nest`. As I explained offline, it's not easy to avoid...
There is a bug in the module `Nest`. I will investigate later.
I fixed the bug.
> Waiting for an updated version to give formal approval; the Nest module looks OK. As discussed offline, if we can adapt the code to store priorities for types rather...
@bclement-ocp is it good for you?
This PR adds a pin on Ocplib-simplex (see issue #1077). We have to add this pin because the latest release of Ocplib-simplex prints some debugging messages at the `App` level.
Can you rebase this PR please? I will review it today :)