--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case



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