[Why3-club] additional invariants cause proven ones to fail?

Alan Schmitt alan.schmitt at polytechnique.org
Wed Mar 19 12:13:44 CET 2014

Cláudio Amaral <coa at dcc.fc.up.pt> writes:

> Yes, I managed to prove everything. That was why I assumed you had not,
> sorry about the assumption.

Great, thanks.

> After splitting there were two VCs that alt-ergo did not prove (7 and 9)
> sorted_sub a !ls (length a)
> and
> a[j] <= a[k]
> as in forall j k : int. 0 <= j <= !ls <= k < length a -> a[j] <= a[k]

These are the same ones that I cannot prove (although they are proven
when the permutation ones are commented out).

> I have several provers, even old ones and sometimes these are the ones
> doing the trick
> of the three Z3 i have (2.19, 3.2, 4.1), only 3.2 proved them. Some
> other provers may have as well

I confirm that Z3 3.2 proves these remaining goals. Thank you for the

I guess I have a feature request for why3: would it be possible to
declare some invariants to be independents (as in: do not include
information from an independent invariant when doing the proof). It
seems there is too much stuff in the context for the provers.



More information about the Why3-club mailing list