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

Alan Schmitt alan.schmitt at polytechnique.org
Wed Mar 19 11:39:41 CET 2014


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



More information about the Why3-club mailing list