--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on July 2009 ---
for me: //*@ lemma test1 : \forall integer x; x/1 == x; */ /*@ lemma test1b : \forall integer x; x != 0 ==> x/x == 1; */ /*@ lemma test2 : \forall integer x; x/x == 1; */ /*@ lemma mean1 : \forall integer x,y; x <= y ==> x <= (x+y)/2 <= y; */ test1, mean1 are proved by Alt-Ergo 0.9, which will hopefully be released very soon. test2 is not proved, which is fortunate since it is wrong. But test1b is also not proved. That's true that division is very poorly supported by SMT provers. E.g there is no SMT-LIB category involving division. - Claude Kerstin Hartig wrote: > On Christoph Weber's request I forward the following mail: > ----------------------------- > > Hello, > > I am exploring the possibilitys of lemmas to assist proofs. > > As I allready mentioned before, I cannot proof the lemma (mean) you provided > with any prover. > > It seems to me, that the division within prevents a solution. > For example the following: > > /*@ lemma test1 : \forall int x; x/1 == x; */ > /*@ lemma test2 : \forall int x; x/x == 1; */ > > The computations would result in unknowns. > > I would like to know if this is a general problem and if there is a way to > circumvent it. > > Sincerely > > Christoph > > > _______________________________________________ > 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 > -- 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 |