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

Cláudio Amaral coa at dcc.fc.up.pt
Wed Mar 19 11:49:40 CET 2014


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

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]

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

Also using why 0.82, forgot to mention

/Cláudio


On Wed, Mar 19, 2014 at 10:39 AM, Alan Schmitt <
alan.schmitt at polytechnique.org> wrote:

> Hi Cláudio,
>
> Cláudio Amaral <coa at dcc.fc.up.pt> writes:
>
> > I have tried your file.
> >
> > the VC for onebubble was not proven right away and neither the more
> > complete VC for bubble
> >
> > splitting the VCs (why3ide split button)
>
> Sorry, I should have made clear I had to split as well.
>
> > I was able to prove everything automatically with my setup (needed
> > a combination of alt-ergo 0.95.1 and Z3 3.2, funny that it worked
> > better than 4.1)
>
> Were you able to prove everything when uncommenting the two lines about
> permutation?
>
> Thanks a lot for your help,
>
> Alan
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20140319/6cfdcde7/attachment-0001.html>


More information about the Why3-club mailing list