Verification issue

[Laurence-Hallo]

Failing code

method Caller() {
  var s, m := MaxSum(1928, 1);
  assert s == 1929;
  assert m == 1928;
}

method MaxSum(x : int, y : int) returns(s : int, m : int)
  ensures s == x + y
  ensures m >= x && m >= y
  ensures m == x || m == y
{
  s := x + y;


  m := if y > x then y else x;
}

Steps to reproduce the issue

• Dafny version: 4.4.0.0
• Dafny VSCode extension version: 3.2.2
• Move line 13 a line down with enter

Expected behavior

Verified

Actual behavior

Keeps on resolving without an end until hitting the time limit.