[Why3-club] additional invariants cause proven ones to fail?
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)
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
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
> Thanks a lot for your help,
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club