--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on May 2016 ---
> 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. No it is not. The generated lemma for Why3 is: (* ---------------------------------------------------------- *) (* --- Global Definitions --- *) (* ---------------------------------------------------------- *) theory Axiomatic use import bool.Bool use import int.Int use import int.ComputerDivision use import real.RealInfix use import Qed.Qed use import int.Abs as IAbs use import map.Map lemma Q_POS: forall x : real. (2.0e0 *. x) <=. (1.0e0 +. (x *. x)) end None of CVC4, Z3 and Alt-Ergo is able to prove it â but in Coq it is. L.