search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
442 stars 40 forks source link

Labels should not prevent the VC generator from decomposing an invariant #3019

Open konnov opened 1 month ago

konnov commented 1 month ago

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.