--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on May 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin



> /*@ lemma sq_double: \forall real x; x*x - .2 * x + 0.01 >= 0.; */

This lemma is definitely wrong in WP with Real model (not float there).
At least, it is not provable in the forthcoming release of Frama-C.
Is there a bug in some existing release?
	L.