ID0001251: **This issue was created automatically from Mantis Issue 1251. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001251 | Frama-C | Plug-in > jessie | public | 2012-07-31 | 2013-03-27 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | boris | **Assigned To** | cmarche | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 | ### Description : After upgarding to why 2.31 and why3 0.73, my binary search program doesn't verify with Alt-Ergo, Z3, and CVC3 and a timeout of 10s. In particular, the loop invariant \forall integer i; 0 <= i < low ==> a[i] < val; doesn't verify. The code did verify with the previous version of Jessie and it verifies with wp. The same is true for another program, mismatch.c. This is a show stopper as the binary search is frequently used to demonstrate formal verification. ## Attachments - [mismatch.c](/uploads/4320a88edd8fb85721d47271710ae268/mismatch.c) - [binary-search.c](/uploads/f6575182f052d42e79ad5cac523ac149/binary-search.c) - [bts1251.html](/uploads/98d0c3757b60649cd5b9c7e271d608b6/bts1251.html) -  - [.why3.conf](/uploads/3489ba396baf87ca0c55f7023d4eb3c6/.why3.conf) - [.whyrc](/uploads/1cf1b161dad8f15a812136d5829e36de/.whyrc) - [why3.conf](/uploads/ad0d3a626d740d5121800e8ae16e2037/why3.conf) - [binary-search.html](/uploads/3b38eb4a65cee5dbf209591cefe25890/binary-search.html)