--- layout: fc_discuss_archives title: Message 84 from Frama-C-discuss on November 2009 ---
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