--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on November 2011 ---
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