When `--isolate-assertions` is used, experiment with combining consecutive assertions into a single VC

[keyboardDrummer]

trafficstars

Consecutive assertions meaning there are no assumptions in between.

It seems arbitrary that assert P && Q would lead to one VC while assert P; assert Q; would not. Also, it seems wasteful to have two VCs in this case, since the assumptions, not considering assumption pruning, are the same.