--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on March 2009 ---
On Thu, Mar 19, 2009 at 09:40, David MENTRE <dmentre at linux-france.org> wrote: >> loop invariant \forall integer j; 0<=j<i ==> total >= counters[j]; > > Thank you. I'll try that. That worked (on both the small example and my real code)! Many thanks, david