--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on March 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie: Timeout for Simplify broken?



Hello Boris,

Le mer. 02 mars 2011 15:30:37 CET,
Boris Hollas <hollas at informatik.htw-dresden.de> a ?crit :

> I have the prover timeout set to 60s in gWhy. Still, Simplify 1.5.4.
> spends only a few seconds on each VC and fails to prove some arithmetic
> overflow VCs that can be proved with alt-ergo. Is there something wrong
> with the timeout? I use why-2.29.

There are two ways in which a prover can fail to discharge a PO: either
it is killed by Why after an certain amount of time (timeout,
represented by the scissors in Gwhy), or it can decide by itself that it
can't decide that the goal is true (represented by an interrogation
mark in Gwhy). In the latter case, increasing the timeout won't help:
the prover will still consider that the goal is out of its scope. From
my experience, Simplify is pretty quick at deciding whether it has a
chance of finding a proof or not, and is not that good when it comes to
big numbers (which are pretty common in overflow POs).

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile