--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on January 2015 ---
Ah, much clearer. Thanks! -- Khairul On Tue, Jan 27, 2015 at 11:37 PM, Claude Marche <Claude.Marche at inria.fr> wrote: > > > 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 | > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150128/d508cd04/attachment.html>