<div dir="ltr">Yes, I managed to prove everything. That was why I assumed you had not, sorry about the assumption.<div><br></div><div>After splitting there were two VCs that alt-ergo did not prove (7 and 9)</div><div>sorted_sub a !ls (length a)<br>
</div><div>and</div><div>a[j] <= a[k]</div><div>as in†forall j k : int. 0 <= j <= !ls <= k < length a -> a[j] <= a[k]<br></div><div><br></div><div>I have several provers, even old ones and sometimes these are the ones doing the trick</div>
<div>of the three Z3 i have (2.19, 3.2, 4.1), only 3.2 proved them. Some other provers may have as well</div><div><br></div><div>Also using why 0.82, forgot to mention</div><div><br></div><div>/ClŠudio</div></div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Wed, Mar 19, 2014 at 10:39 AM, Alan Schmitt <span dir="ltr"><<a href="mailto:alan.schmitt@polytechnique.org" target="_blank">alan.schmitt@polytechnique.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi ClŠudio,<br>
<div class=""><br>
ClŠudio Amaral <<a href="mailto:coa@dcc.fc.up.pt">coa@dcc.fc.up.pt</a>> writes:<br>
<br>
> I have tried your file.<br>
><br>
> the VC for onebubble was not proven right away and neither the more<br>
> complete VC for bubble<br>
><br>
> splitting the VCs (why3ide split button)<br>
<br>
</div>Sorry, I should have made clear I had to split as well.<br>
<div class=""><br>
> I was able to prove everything automatically with my setup (needed<br>
> a combination of alt-ergo 0.95.1 and Z3 3.2, funny that it worked<br>
> better than 4.1)<br>
<br>
</div>Were you able to prove everything when uncommenting the two lines about<br>
permutation?<br>
<br>
Thanks a lot for your help,<br>
<br>
Alan<br>
</blockquote></div><br></div>