Dafny formatter produces incorrect indentation with match statement and :|

[ymherklotz]

Dafny version

4.0.0

Code to produce this issue

lemma Try(i: int)
{
  match i {
    case i' =>
      var x :| x == i';
      assert x == i';
  }
}

Command to run and resulting output

dafny format file.dfy

What happened?

When running dafny format, one gets the following result:

lemma Try(i: int)
{
  match i {
    case i' =>
      var x :| x == i';
  assert x == i';
  }
}

Instead it shouldn't change the indentation.

When adding curly braces around the case statement body, then the indentation is correct, and correctly produces the following:

lemma Try(i: int)
{
  match i {
    case i' => {
      var x :| x == i';
      assert x == i';
    }
  }
}

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

Mac

[stefan-aws]

Thanks for reporting, we will look at it.

[MikaelMayer]

Until the formatter get fixes, here is a workaround:

lemma Try(i: int)
{
  match i {
    case i' =>
      var x :| x == i';
  /**/assert x == i';
  }
}