--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on November 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Code doesn't verify anymore with new Frama-C/Jessie release



On Fri, 2011-11-04 at 12:56 +0100, Claude Marche wrote:

> Then now, using why3ide, and "split" button, is everything proved or not?

All goals that didn't verify with alt-ergo are proved with alt-ergo
after splitting.

However, I don't understand the concept of splitting. Is it possible
that goal a && b can't be proved, but it can be proved with the same
prover after splitting it in two goals? It would make sense for
different provers.
-- 
Best regards,
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111105/f51acf8c/attachment.htm>