--- layout: fc_discuss_archives title: Message 63 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New Frama-C version: Fluorine



Hi Lo?c,

Here is an example: http://pastebin.com/jzq4Qg0r

thanks!


2013/4/24 Lo?c Correnson <loic.correnson at cea.fr>

> This is because other provers are not fair enough to find a contradiction.
> Can you send us your example ?
>         L.
>
> > Indeed inserting an //@assert \false; results it being proved. Why does
> this happen with Z3 and not other provers?.
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>



-- 
Cumprimentos,
Cristiano Sousa
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130424/55482798/attachment.html>