Stevendeo

Results 21 issues of Stevendeo

### `pilat.1.6` Polynomial invariant generator --- * Homepage: https://github.com/Stevendeo/Pilat/ * Source repo: git://github.com/Stevendeo/Pilat.git * Bug tracker: https://github.com/Stevendeo/Pilat/issues --- :camel: Pull-request generated by opam-publish v2.0.3

The preprocessing of a formula sometimes allow Alt-Ergo to discard useless patterns (especially on ite where the condition is trivial). Three options are included in this PR: - `-simplify [y|n]`...

The error message "alt-ergo: algebraic datatype are not supported" does not come from Alt-Ergo but from Why3 (here: https://gitlab.inria.fr/why3/why3/-/blob/master/src/printer/alt_ergo.ml#L366). But ```omg``` still doesn't pass the type checking in Alt-Ergo: ```...

Handles #52