--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on October 2010 ---
> the prover timeout for gWhy doesn't work on my system. I set it to 1 s > in the GUI, yet it still takes 10 s for alt-ergo to timeout. Is there a > fix for that? > > Also, is it possible to set the timeout permanently? gWhy forgets the > setting upon the next start. For me (Max OS X distribution from http://frama-c.com/ with alt-ergo 0.92.1 installed by hand) the timeout setting works and is remembered across executions of gWhy. > BTW, have you considered using iterative deepening instead? This way, > the user could very quickly see which VCs may not verify and start I believe that under some (almost true) assumptions on the hardware you are doing proofs on, this "iterative deepening" is subsumed by the parallel execution of proofs that will be available with the next version of Why. Simply trick Why into launching more of them than you have execution threads, and if your system is fair/robust enough, the result will be the same, only more efficient. Pascal