--- layout: fc_discuss_archives title: Message 21 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 05/11/2011 13:14, Boris Hollas wrote:
> 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?

Yes, as you can see on your example. Remember that automatic provers are 
difficult beasts to tame.

> It would make sense for
> different provers.

Indeed, but not only.

- Claude