Binary search doesn't verify anymore after upgrade
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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information