This project is read-only.

Aggressive pruning

May 3, 2010 at 4:14 PM

Hi,

when running "vcc /help" there is this switch "/a" (/agressivepruning) to "Remove unreferenced items when verifying specific functions" (it generally speeds things up a little, e.g. just to back this by some real-life number 42.5% on today's verification target regression test). When I have a file that verifies without "/a" but does not verify with "/a" is that something for the Issue Tracker or is it this expected behavior?

(In case anyone is interested in the greater picture, my current preferred setting is "vcc /st /z3:/T:180 /a /b:/errorLimit:1 /ps:32 /b:/smoke $@" where "/st" is "give times", "/z3:/T:180" is a three-minute per-function timeout to z3, "/a" the above-mentioned aggressive pruning, "/b:/errorLimit:1" causes to quit after the forst error, "/ps:32" is for 32-bit system, "/b:/smoke" is smoke testing and "$@" is bash for passing through all other arguments).

Cheers, Holger

May 3, 2010 at 4:18 PM

Hi Holger,

  it might be "just instability". Can you try a number of random seeds (/z:/rs:0, /z:/rs:1, /z:rs:2, ...) with and without /a? If the problem consistently persists with /a, we should have a closer look indeed.

  Best, Mark

May 3, 2010 at 4:40 PM

Hi Mark,

quick feedback: you are right that when using other seeds in {0,1,2,3} other than "/z:/rs:0" the proof also fails without the "/a". Hmm ...

May 3, 2010 at 5:12 PM

As, in addition, we also found a soundness warning by playing a bit more now filed to:

http://vcc.codeplex.com/WorkItem/View.aspx?WorkItemId=4409