--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on July 2017 ---
Hi, Le 18/07/2017 12:53, Gerlach, Jens a écrit : > I donât think we had a bias towards Alt-Ergo because for a long time we > have used CVC4 and Z3 in our > verification pipeline before Alt-Ergo. > > I suspect, however, that the Alt-Ergo development follows WP and Why3 > more closely than the other provers. Actually, the WP plug-in has a dedicated Alt-Ergo output, while it relies on Why3 for the other provers. It may explain Jens's results. -- Julien