--- layout: fc_discuss_archives title: Message 66 from Frama-C-discuss on May 2009 ---
Hi Claude, Somehow I haven't seen setup for Z3 prover. Thanks a lot for notice. To be honest, I have just prepared why - Z3 prover, for a coming tasks in project. I didn't try. Thanks again. Dragan On Fri, May 22, 2009 at 12:55 PM, Claude March? <Claude.Marche at inria.fr>wrote: > > The wiki already contains a link to the prover tips page of Why. > > http://why.lri.fr/provers.html > > Could you elaborate on the difference between your way of using Z3 under > linux and what is proposed at the Why prover tips page ? > > - Claude > > MONATE Benjamin 205998 wrote: > > Hi, > > > > Thanks for your full z3 howto. It probably needs to be written to the > Wiki on http://bts.fram-c.com. > > > > As esc/java2, AFAIK the associated prover is Simplify and they intend to > use other SMT provers. > > So which prover do you have in mind? In any case support for new provers > is a feature request for Why itself. > > > > Cheers, > > -- > > Benjamin Monate > > CEA LIST > > Head of Software Safety Lab. > > > > > > > > ------------------------------------------------------------------------ > > > > _______________________________________________ > > 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 <http://www.lri.fr/%7Emarche/%0AF-91893> ORSAY Cedex > | > > > > > > > > _______________________________________________ > 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 > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090524/ab397865/attachment.htm