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