--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie + simplify broken?




On 12/10/2010 07:24, Boris Hollas wrote:
> On Mon, 2010-10-11 at 17:19 +0200, Claude Marche wrote:
>
>> When the "tools" icon shows up for a prover, please select Proof/Debug
>> mode in the menu
>> and replay the same proof by double-clicking on it. Debug info should
>> print on the standard error, so that you can figure out what is the problem.
>
> That's what i get:
>
> oblig : get2_safety_po_1
> calling Simplify on /tmp/gwhyb915b2_why.sx
> command line: simplify   /tmp/gwhyb915b2_why.sx
> Calldp : Command output : why-cpulimit: simplify:command not found

Dear Boris: please note that I said "so that *you* can figure out the 
problem" ;-)

What do you think about "simplify:command not found" ?

> Debug: not removing temporary file '/tmp/gwhyb915b2_why.sx'
>
>
> CVC3 works. There's even a package for Ubuntu.
>
>> Apart from that, I confirm that the time limit setting of Gwhy should be
>> stored permanently between sessions, so you have a specific problem with
>
> I can reproduce the following:
> - if I quit gwhy with Ctrl-Q, the timeout is stored
> - if I quit gwhy by clicking on the close-gadget in the window, the
> timeout is not stored

So if you quit by Ctrl-Q at least once, the timeout is stored, good.

Please fill in a bug report for this bad behavior when exiting from the 
window manager button.

- Claude