Inconsistent verification performance with simple arithmetics

[dirtybytes]

Dafny version

4.11.0

Code to produce this issue

lemma MulDiv(a: nat, b: nat)
  requires 0 < a
  requires 0 < b
  ensures a * b / b == a
{
}

Command to run and resulting output

Verification in VSCode times out after 20 seconds.

What happened?

I expect the verification to go through.

You can make it verify by running Dafny with /arith:0 or /arith:3 (although these flags are marked as deprecated).

You can also make it verify by constraining the values:

lemma MulDivConstrained(a: nat, b: nat)
  requires 0 < a < 1000
  requires 0 < b < 7000
  ensures a * b / b == a
{
  // ok
}

But it's inconsistent, and replacing b < 7000 with b < 1000 makes it fail again, though it no longer times out:

lemma MulDivConstrained(a: nat, b: nat)
  requires 0 < a < 1000
  requires 0 < b < 1000
  ensures a * b / b == a
{
  // a postcondition could not be proved on this return path
}

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

Windows