--- layout: fc_discuss_archives title: Message 12 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




Le 04/05/2016 15:36, Loïc Correnson a écrit :
> 
> PS: it is still a mystery for me why Z3 succeed into proving this, but
> fails into proving (x2 - 2x + 1) >= 0… :-)

Just a guess : if you write 2.0 and 1.0 instead of 2 and 1 does it work?
If yes, then it is an issue with conversion from integer to real.

- Claude


-- 
Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - ÃŽle-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |