--- layout: fc_discuss_archives title: Message 105 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



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