Binary search doesn't verify anymore after upgrade
ID0001251: This issue was created automatically from Mantis Issue 1251. Further discussion may take place here.
|ID0001251||Frama-C||Plug-in > jessie||public||2012-07-31||2013-03-27|
|Product Version||Frama-C Nitrogen-20111001||Target Version||-||Fixed in Version||Frama-C Oxygen-20120901|
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.