Labels should not prevent the VC generator from decomposing an invariant

[konnov]

Normally, the VC generator decomposes an invariant into two smaller invariants:

Inv ==
  /\ A
  /\ B

Inv is decomposed into:

Inv_0 == A
Inv_1 == B

However, if we annotate the invariant with a label, which is quite useful to see what has been violated, then the VC generator does not go inside the expression under the label:

Inv ==
  InInv ::
    /\ A
    /\ B

This should be quite easy to fix.