--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on May 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] RE : Loop invariants with imbricated loops.



Hi Benjamin,
Thanks for communication.


On Wed, May 20, 2009 at 7:56 PM, MONATE Benjamin 205998 <
Benjamin.MONATE at cea.fr> wrote:

> Hi,
> Thanks for your full z3 howto. It probably needs to be written to the Wiki
> on http://bts.fram-c.com.
>
    Unfortunately http://bts.fram-c.com/ doesn't works.


> As esc/java2, AFAIK the associated prover is Simplify and they intend to
> use other SMT provers.

   So which prover do you have in mind?In any case support for new provers
is a feature request for Why itself.
   Agreed. My false, sorry.
   Best Regards
   Dragan.



>
> Cheers,
> --
> Benjamin Monate
> CEA LIST
> Head of Software Safety Lab.
>
>
> _______________________________________________
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090520/c9c205ac/attachment.htm