--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on May 2016 ---
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 |