How to instruct Boogie to only generate the VCs?

[alexthomasv]

Is there a way for Boogie to just generate the VCs? I have tried running

boogie /print:output.bpl /noVerify /trace a.bpl
But this just only just outputs the Boogie code.

Any help is appreciated. Thank you!

[shazqadeer]

Try the option /proverLog:output.smt2.

[alexthomasv]

Thanks, this helps. Is there a pretty print version where its easier to visualize which VCs map to specific boogie code?

[shazqadeer]

Boogie generates a VC for each procedure. In the generated file, search for strings like:

(set-info :boogie-vc-id Civl_GatePreservationChecker_atomic_release_AtomicInit)

For example, in the above Civl_GatePreservationChecker_atomic_release_AtomicInit is the name of the procedure for which the verification condition is being generated.

[alexthomasv]

Thank you, is there a guide to understanding the labels? For example, here's on generated label: bb7#1_correct

I know bb7 is a basic block from Boogie, but what does the 1_correct mean? There's also $i9@0, which I'm guessing i9 is a register, but what does the 0 mean?