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

[Frama-c-discuss] gWhy timeout



> 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