Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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