--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on October 2012 ---
Hello, the code below doesn't verify with Jessie because 0.8 * x > 0.0 can't be verified. #pragma JessieFloatModel(math) //@ requires 1 <= x < 10; void foo(int x) { double y = 1.0 / (0.8 * x); } If I add //@ lemma pos: \forall integer x; x > 0 ==> 0.8 * x > 0.0; then this lemma can't be verified. This happens with Alt-Ergo and Simplify and both the why2 and the why3-backend. -- Best regards, Boris