Running out of memory - VCC vs VCC /t + boogie

Editor
Nov 20, 2009 at 1:21 PM

Hi all,

I am currently playing the verification game dangerously close to Z3's limits, and I am observing a strange behaviour from VCC. When running VCC directly on my annotated .c file, it reports that it runs out of memory. In previous versions of my code, I identified that it was due to Z3, so I am not expecting anyone to tell me how to fix that particular bit.

My issue here is that outputting the BoogiePL code using vcc /t and running Boogie on the resulting file does not give rise to the memory error. I expect it is due to the way boogie gets called from the vcc binary. My question is: is there a way to tell vcc to behave as if it was using the intermediate file (and thus not run out of memory) but still benefit from the source-level error reporting?

Cheers,
Francois

Coordinator
Nov 20, 2009 at 5:27 PM

Hi Francois,

  I think the different behavior can be explained by the default options that VCC passes to Boogie. This set of default has changed some times in the past. Currently, VCC passes the default options "/errorLimit:10 /typeEncoding:m /proverMemoryLimit:0 /proverWarnings:1" to Boogie. Please try to give those options when you directly start Boogie. Also, I'd suggest to try different random seeds from VCC (/z:/rs:X) as wells as from Boogie (/z3opt:/rs:X, I think).

  Best, Mark