--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on July 2017 ---
-- Julien Signoles (2017-07-18) > 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. Since Why3 has a translation to Alt-Ergo as well, it would be easy to check, by using this path with Alt-Ergo on a run. -- Yannick Moy, Senior Software Engineer, AdaCore -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170718/83609479/attachment.html>