what is wrong with this pluscal spec?

[Michal Jaszczyk]

Below is a distilled version of something I ran into while writing my spec. PlusCal complains that a label is missing. It is a minimal reproduction, in the sense that changing almost anything is enough to fix this:

* insert a label before the `if` statement

* insert a label after the `assert` statement

* remove the `assert` statement

* replace `with` statement with a simpler `x := x + 1`

I believe that the spec is correct with respect to the rules about where labels are required. This is corroborated by the fact that simply removing the assert is enough to fix it.

What is going on - am I doing something wrong, or is this a bug in PlusCal?

My PlusCal version is: pcal.trans Version 1.9 of 10 July 2019

---- MODULE foo ----

EXTENDS TLC

(* --algorithm foo

variables

x = 0;

begin
 A:
  x := x + 1;
  if x # 0
  then
 B:
    assert TRUE;
    with
      new_x = x + 1
    do
      x := new_x;
    end with;
  end if;
end algorithm; *)

====

Cheers,

M.