--- layout: fc_discuss_archives title: Message 73 from Frama-C-discuss on December 2009 ---
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