Boogie

Add `/warnVacuousProofs` option (#1016)

This option enables `/trackVerificationCoverage` and automatically warns
if it detects vacuous proofs. This is intended for the less-common case
where a front end doesn't add IDs to program elements and then
post-process the results.