This project is read-only.

Function verifies with /f:, but fails when verifying the whole file

Oct 15, 2012 at 4:06 PM

Hi guys,

Is there be any good reason why a function that verifies when verified on its own (using /f or Alt+V Alt+T) would fail to verify when the whole file is fed through VCC (with /ii)? _(def) and _(abstract) functions are involved, but all the declarations and definitions are in an included header, so that should not change VCC's behaviour.

To be clear, Z3 isn't running out of memory (although it may in fact be timing out), and all other functions, even those proved after the affected one verify in exactly the same way (including verification time) in both cases.

I don't have a minimal example, but I'd like to know if this is a known and expected behaviour of VCC/Z3, or if it is weird and requires a bug report before I go ahead and try to reduce my couple of thousand lines of stuff to something edible.

Cheers,
Francois

Oct 15, 2012 at 7:36 PM

Hi Francois,

  I guess this can happen for unstable verifications. The context that prover gets to can vary for the /f and the /ii case (unless, I guess, the function is the first in the file to verify). You can try to remedy the situation by specifying /b:/restartProver (that will get the prover restarted for every function) or by putting _(isolate_proof) on the function (in addition, that will make sure to generate a separate Boogie file for the function with aggressive pruning, /a, to try removing irrelevant definitions). To validate that your current proof is unstable, you can try with /f against a number of randome seeds (/z:/rs:0, /z:/rs:1, etc.). If that always succeeds (and the /ii one likewise always fails), there might still be something wrong.

  Best, Mark

Oct 16, 2012 at 11:02 AM

Thanks for the hints, Mark.

I do know that verification is unstable (I have carefully hand-crafted guidance assertions to make it go through), so I don't think we need to look any further. I'll still give it some more thought, and run some tests with the flags you suggest, just to make sure it's not something weirder.

Francois