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

-- 
Regards,
Boris