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



> 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.