--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on October 2012 ---
On 08.10.2012 11:36, Guillaume Melquiond wrote: > that make it a problem with jessie and float division? In fact, cvc3, > z3, and gappa, succeed in proving your program. Indeed, CVC3 proves the code, even without the lemma, but only if I use the why3-backend. However, Z3 runs in a time out. I don't understand why because Z3 and Simplify generally perform well on arithmetics. I haven't installed gappa. I read http://gappa.gforge.inria.fr/doc/ch06s01.html, but I don't know how to install it in a way so that why can use it. In what order do gappa, jessie, why3 have to be compiled and installed? Does gappa work with why3? Is gappa independent of Frama-C? -- Best regards, Boris