[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
suggestion!

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.

Thanks,

Alan



More information about the Why3-club mailing list