Regression in integer arithmetic reasoning

[fpl-uca]

The following method would verify in previous versions of Dafny, but it now fails to verify without the commented out intermediate assertion:

method mul(x: nat, y: nat) returns (z: nat)
  ensures z == x * y
{
  var a: nat, b := x, y;
  var c := 0;
  while a != 0
    invariant x * y == a * b + c
  {
    if a % 2 != 0 {
      c := c + b;
    }
    // assert x * y == a * b - b * (a % 2) + c;
    a, b := a / 2, b * 2;
  }
  z := c;
}

[fpl-uca]

No progress on this. Checked on Dafny 2.3 (CLI on a fresh Ubuntu 22.04) and Dafny 3.10 (on VS Code). Verification succeeds in version 2.3, but fails in the latest stable version, 3.10.

[atomb]

I just tried this with commit 74b47b551dede1c45e2ce815fcb8e02bc6ef11ea, and it continues not to be solvable using Z3 4.8.5, which is currently distributed with Dafny. However, Z3 4.11.2, which we plan to start including with Dafny 4, can solve it once again.