let's try using this discussion board instead of starting an email thread, other people might find this useful as well.
So, I was wondering recently whether Boogie cleans up (i.e. removes) empty blocks before doing VC generation. I found the /noRemoveEmptyBlocks switch in Boogie help, so my guess was that it is doing some empty block optimizations. I wanted to learn what
exactly is going on, so I run Boogie on this simple bpl code:
However, the generated VC still contains formulas for all of the blocks in this example, although they are empty.
Is generating error traces the only reason why these empty blocks are still part of the VC?
Is there a switch that would still remove them?