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

[Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices



Dear Claude,

thanks for your reply.
I tried the additional option and the discrepancies are gone now.

Jens

Am 08.12.2009 um 09:53 schrieb Claude Marche:

>
> I confirm I get the same behavior.
>
> After investigating, I found that this because in batch mode, the
> generation of goals for smt solvers (yices, z3, cvc3)
> is done with the why option "-exp goal" which ask to automatically
> expand definitions of predicates in the generated goals.
>
> Thus to obtain the same behavior in the gui, you need to do
>
> frama-c -jessie  -jessie-why-opt " -exp goal" sw.c
>
> (Do not forget the space before the -exp, because of the frama-c model
> for options parsing...)
>
> Thanks for pointing the difference, we will try to fix that.
>
> - Claude
>



-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091208/023ceee9/attachment.htm