--- layout: fc_discuss_archives title: Message 84 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Lemma from ACSL doc doesn't verify



This is from the ACSL documentation, 2.6.2:

//@ lemma mean_property: \forall integer x,y; x <= (x+y)/2 <= y;

It doesn't verify with Alt-Ergo or Z3, which is correct since the lemma doesn't hold. However,

//@ lemma mean_property: \forall integer x,y; x <= y  ==>  x <= (x+y)/2 <= y;

still doesn't verify, as well as

//@ lemma mean_property: \forall int l, h; l <= l + (h-l)/2 <= h;

The latter is known by VCC without explicit specification. I therefore assume that Z3 knows about this fact. How does Jessie handle such formulas, are they passed to the SMT solver?

I use Beryllium 1.

-Boris