[tlaplus] Removing a label in a PlusCal algorithm changes the verification outcome

----------------------------- MODULE OneBitNProcMutex -----------------------------
EXTENDS Integers, TLC

CONSTANT N
ASSUME N \in Nat

Procs == 0..(N-1)

(*
--algorithm 1BitNProcMutex {
variables can_enter_critical_region = [i \in Procs |-> FALSE] ;
process (P \in Procs)
variable higher_priority = {}; lower_priority = {}; proc = self;
{ ncs: while (TRUE) {
skip ;
enter: while ( ~ can_enter_critical_region[self] ) {
can_enter_critical_region[self] := TRUE ;
higher_priority := { i \in Procs : i < self } ;
e1: while ( higher_priority /= {} /\ can_enter_critical_region[self] ) {
e2: with ( q \in higher_priority ) {
proc := q;
};
e3: if ( can_enter_critical_region[proc] ) {
e4: can_enter_critical_region[self] := FALSE ;
e5: higher_priority := { i \in Procs : i < self } ;
await ~ can_enter_critical_region[proc] ;
} else e6: {
higher_priority := higher_priority \ {proc} ;
} ;
};
} ;
lower_priority := { i \in Procs : i > self } ;
e7: while ( lower_priority /= {} ) {
e8: with ( q \in lower_priority ) {
proc := q ;
} ;
e9: await ~ can_enter_critical_region[proc] ;
lower_priority := lower_priority \ {proc};
} ;
cs: skip ;
exit: can_enter_critical_region[self] := FALSE ;
}
}
}

When removing the label e5, the TLA+ toolbox report a violation of the MutualExclusion invariant. I would expect that the presence of labels did not affect the correctness of invariance properties. Am I missing something, or is this a bug?