--- layout: fc_discuss_archives title: Message 85 from Frama-C-discuss on November 2009 ---
Hello Boris, Le mer. 25 nov. 2009 15:20:57 CET, "Hollas Boris (CR/AEY1)" <Boris.Hollas at de.bosch.com> a ?crit : > //@ 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, Oops, thanks for spotting that. I guess it would be better to write examples of properties that are true in the documentation. > > //@ 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 and without the constraint that l<=h ? If that's the case, there is a problem. If the real formula is \forall int l, h; l<=h ==> l <= l + (h-l)/2 <= h; it is proved (as well as the variant using (x+y)/2) by alt-ergo 0.9, the latest available version. Z3 v2.0 (the version for linux on why.lri.fr) fails to prove them indeed. > assume that Z3 knows about this fact. How does Jessie handle such > formulas, are they passed to the SMT solver? My guess would be that VCC/Boogie produces formulas in z3's own language, while alt-ergo uses the smt language. I suspect that this is due to the fact that smt's int theory does not contain division and that z3 fails to interpret the div_int symbol chosen by Why to represent it (Why not providing axioms over div_int doesn't help either). Hope this helps, -- E tutto per oggi, a la prossima volta. Virgile