Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Jessie: Timeout for Simplify broken?
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Wed, 2 Mar 2011 18:56:17 +0100
  • In-reply-to: <1299076237.31590.27.camel@iti27>
  • References: <1299076237.31590.27.camel@iti27>
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