--- layout: fc_discuss_archives title: Message 92 from Frama-C-discuss on December 2009 ---
Hello, I somehow do not understand what this option is exactly doing. I tried to find more information in the manual, but unfortunately I couldn't. In the help-page I found even more VC transformation options like --exp all or eval-goals... I am wondering now, if it is sufficient if a VC can be proved with the option -exp goal, but not without (timeout). Especially as it seems to be a default option in batch mode. To answer this I'd like to understand better what is meant by "expand definitions of predicates in the generated goals". Maybe someone can help with this. Thank you in advance, Kerstin >> 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 -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/ms-tnef Size: 3375 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091209/6c0566bd/attachment.bin