--- layout: fc_discuss_archives title: Message 105 from Frama-C-discuss on December 2009 ---
Thanks a lot for your answers, I now understand what -exp goal is doing. I'm very interested in that, because I have several (bigger) examples, whose results I want to evaluate by creating tables.(with the number of total, valid, timeout..VC) For that consistency between batch and gui mode is kind of important. For yices the results of the gui (with option -exp goal) and commandline (default setting) are consistent now. Results obtained with Simplify and Z3 are consistent anyway. But I found discrepancies using cvc3, which are a bit unexpected. Batch mode (with and without specifically setting the option -exp goal) returns the same result as gui-mode (default). But gui-mode with option -exp goal is not equal to the other results. This is a bit disturbing, as at least the results of gui-mode (-exp goal) and batch-mode (-exp goal) should be consistent. Is it possible there are other options set by default which were not mentioned yet? or what might be the reason for that kind of behavior? Regards, Kerstin (I am using mac os, beryllium2, why 2.23) -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/ms-tnef Size: 3683 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091210/51439714/attachment.bin