Claude Marché

Associated types not supported in declarations

2

On the code ``` extern crate creusot_contracts; use creusot_contracts::{std::vec::Vec}; fn main() { let mut door_open : Vec = Vec::with_capacity(100); for pass in 1..101 { let mut door = pass; while...

Fatal Error when step limit reached

4

When Alt-Ergo reaches the given step bound, an uncaught exception is signaled. It is desirable to display a proper information message and not an error message, this is a perfectly...

JS worker does not compile

4

First of all, let me emphasize that the page [Try Alt-Ergo](https://try-alt-ergo.ocamlpro.com/) referenced under [button new try-alt-ergo](https://alt-ergo.ocamlpro.com/) does not work anymore. Second, we need to compile a JS Alt-Ergo worker for...

Extra functions supported by Alt-Ergo (SMT input) / documentation

4

Following a patch to Why3 proposed by @bclement-ocp, Why3 makes use of extra functions `ae.pow` and `ae.sqrt_real`. However, when I test it seems that `ae.sqrt_real` is not recognized. I had...