--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on December 2009 ---
Hello, we experience a discrepancy between the verification results in the Jessie-GUI versus those of the command line. (I am talking about Beryllium-20090901 with why version 2.19 on Mac OS X.) When verifying the following function. /*@ requires \valid(p); requires \valid(q); assigns *p; assigns *q; ensures *p == \old(*q); ensures *q == \old(*p); */ void swap(int* p, int* q) { int save = *p; *p = *q; *q = save; } The results of the command line frama-c -jessie -jessie-no-regions -jessie-atp yices sw.c yields ... total : 6 valid : 6 (100%) ... total wallclock time : 0.78 sec However, when calling the gui with frama-c -jessie -jessie-no-regions sw.c we obtain a timeout ("scissors") on the third precondition. I cannot understand why there is a timeout in the gui when the total wallclock time for yices is less than a second. Can other people confirm this on their respective installations? Regards Jens Gerlach