Depending on the assert position, the verifier freezes

[henry-hz]

Dafny version

4.7.0+769d1572fdd799c7bf76b78a3bc9cb94d18aac59

Code to produce this issue

module Math {

    const WAD:      nat := 1_000_000_000_000_000_000 // 18 zeros
    const RAY:      nat := 1_000_000_000_000_000_000_000_000_000 // 27
    const PERCENT:  nat := 1_000_000_000_000_000_000 // 18 zeros
    const YEAR: nat := 30758400 // year in seconds

    function Max(x: nat, y: nat) : nat {
        if x > y then x
                 else y
    }

    function Min(x:nat, y: nat) : nat {
        if x < y then x
                 else y
    }

    /// Returns `ceil(x * y / d)`. [arredonda para cima]
    /// Reverts if `x * y` overflows, or `d` is zero.
    //  z := add(iszero(iszero(mod(mul(x, y), d))), div(mul(x, y), d))
    function MulDivUp(x:nat, y:nat, z:nat) : (r: nat)
    requires z > 0
    ensures r == (x * y + z - 1) / z{
        (x * y + z - 1) / z
    }

    /// @dev Returns `floor(x * y / d)`. [arredonda para baixo]
    /// Reverts if `x * y` overflows, or `d` is zero.
    function MulDivDown(x:nat, y:nat, z:nat) : (r: nat)
    requires z > 0
    ensures r == (x * y) / z {
        (x * y) / z
    }

    function ToWad(x:nat) : nat {
        x * WAD
    }


    //rounds to zero if x*y < WAD / 2
    function Wmul(x: nat, y: nat) : nat {
        var m: nat := x * y;
        var w: nat := WAD / 2;
        (m + w)/WAD
    }

    //rounds to zero if x*y < WAD / 2
    function Wdiv(x: nat, y:nat) : (r: nat)
    requires y != 0 {
        var m: nat := x * WAD;
        var w: nat := y / 2;
        var z: nat := m + w;
        z / y
    }

}

// -------  TESTS


import opened Math
method TestDiv1() {                    // ----> it freezes
    assert MulDivUp(7, 3, 4) == 6;
    assert MulDivUp(3, 5, 4) == 4;
    assert MulDivUp(4, 5, 4) == 5;
    assert MulDivUp(10, 5, 2) == 25;   // to fix you have to move this to TestDiv2()
}
method TestDiv2() {
    assert MulDivUp(15, 1, 2) == 8;
}
method TestDiv3() {
    assert MulDivDown(7, 3, 4) == 5;
    assert MulDivDown(3, 5, 4) == 3;
    assert MulDivDown(4, 5, 4) == 5;
}

Command to run and resulting output

dafny verify ./src/math.dfy

What happened?

TestDiv1() method freezes on verifier

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

Linux