--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on January 2015 ---
On 01/27/2015 01:14 PM, Khairul Azhar Kasmiran wrote: > Aha! So the problem was because the solvers did not receive any > information on the lower bound of j. Hmm, okay. Still unclear to me as > to why it's needed, since the invariant doesn't state that j == 1 is > false after any iteration of the loop. Any loop iteration increments j by 1, no ? then if j >= 1 before the iteration, then j >= 2 after. And consequently j == 1 is false. Qed. - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |