--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on July 2017 ---
Hello Loïc, > Just to mention it, the appendix A.3 of this document shows the individual results of _each_ provers and for each algorithm. > It is interesting to observe that, in most cases, Alt-Ergo, CVC4, CVC4, and Z3 have very *closed* results, and Eprover is significantly aside. > In the table provided by Jens, most provers (except Eprover) completely verify all the verification conditions but a few. Your observation is right. Eprover looks better than Z3 in my statistics because it works very well on the many small âstack*â examples. On the more complex examples, Eprover is not particular good, except (interestingly) on the numeric algorithms. > A possible next step would be to extract the « difficult » verification conditions and understand what is going wrong with them for each prover. Letâs looks for a project!-) > Second remark, regarding WP, it would be interesting to compare the results obtained with its native support of Alt-Ergo, or via > the Why-3 translation. > Namely, comparing -wp-prover alt-ergo and -wp-prover why3:alt-ergo in order to understand the impact of Why-3 translation. The Alt-Ergo data in Appendix A.3 were obtained using Why3. The Alt-Ergo data in Appendix A.2 were obtained using -wp-prover alt-ergo. Jens