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

[Frama-c-discuss] Lemma from ACSL doc doesn't verify



Oops, sorry I meant

//@ lemma mean_property: \forall int l, h; l <= h  ==>  l <= l + (h-l)/2 <= h;

still doesn't verify. I haven't tried the latest version of why however. I have AltErgo 0.7.3 and Z3 1.3.

-Boris