--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on October 2010 ---
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