--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on January 2010 ---
David A. Wheeler a ?crit : > Gappa 0.12.3 cannot handle most of the VCs. Seeing that there isn't even a single floating-point number in your code, the contrary would have been surprising. (In fact, it comes as a good surprise to me that Gappa is able to prove 30% of the VCs on your example.) Gappa is not a generic (SMT) prover like Alt-Ergo, CVC3, Z3, Simplify, etc. It is a specialized prover dedicated to proving properties on floating-point expressions, as they are usually out of reach of the above tools. It comes as a complement to the other tools, not as a replacement. Best regards, Guillaume