This page describes some command line options useful when verifying.

Boogie

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

/subsumption:0

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.

/causalImplies

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.