--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on December 2009 ---
Hollas Boris (CR/AEY1) wrote: > Oops, sorry I meant > > //@ lemma mean_property: \forall int l, h; l <= h ==> l <= l + (h-l)/2 <= h; > > still doesn't verify. I haven't tried the latest version of why however. I have AltErgo 0.7.3 and Z3 1.3. > > -Boris > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > As far as I know, SMT provers do not know the division operator, so it is not surpriseing they don't verify these. For Alt Ergo 0.9, a few set of axioms for div are known, so these lemma verify. But the way, for using these lemmas in your codes, PLEASE USE TYPE integer INSTEAD OF TYPE int /@ lemma mean_property: \forall integer l, h; l <= h ==> l <= l + (h-l)/2 <= h; - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |