Making assertions explicit fails for nested statements

[MikaelMayer]

Dafny version

4.1.0

Code to produce this issue

datatype D = C(value: int) | N

function Test(e: D, inputs: map<int, int>): bool {
  match e
  case N => true
  case C(index) => inputs[index] == index
}

Command to run and resulting output

Paste this code in VSCode, click on input[index], select "Insert explicit failing assertion", it will modify the code incorrectly.

What happened?

Here is the wrong result. index#Z should be replaced by index

datatype D = C(value: int) | N

function Test(e: D, inputs: map<int, int>): bool {
  match e
  case N => true
  case C(index) => assert index#Z in inputs;
                   inputs[index] == index
}

What type of operating system are you experiencing the problem on?

Windows