This page describes some command line options useful when verifying.


These are passed on VCC command line with the /b:<option> syntax.


The VC generated from assert P; assert Q; will normally be P && P ==> Q , in other words, the assert P is really treated as assert P; assume P . The /subsumption:0 switch disables that, which might limit the number of quantifier instantiations.

VCC automatically turns user-supplied assert(X) statements into pairs or assert(X); assume(X), therefore this switch has no effect on user-supplied assertions. It has effect on compiler-generated things (writability, thread locality, invariant checks) and on "requires" of functions you call.

Adding this switch might cause your program to no longer verify because of triggering.


This will make Boogie treat all formulas of the form P ==> Q as if they were P ==> P && Q, which might, but also might not improve performance.

Last edited Dec 15, 2009 at 6:43 PM by MarkHillebrand, version 3


No comments yet.