[Why3-club] additional invariants cause proven ones to fail?
alan.schmitt at polytechnique.org
Wed Mar 19 11:39:41 CET 2014
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,
More information about the Why3-club