Verification hang apparently caused by Std import

[nverhaaren]

Dafny version

4.6.0.0

Code to produce this issue

module {:disable_nonlinear_arithmetic} ImportRepro {
    import Std.Arithmetic.DivMod

    datatype DivAnalysis = DivAnalysis(dividend: int, divisor: int, quotient: int, remainder: int, near_multiple: int) {
        static function Abs(x: int): int { if x < 0 then -x else x }

        predicate {:opaque} Valid?() {
            divisor != 0 && quotient * divisor == near_multiple && near_multiple + remainder == dividend && 0 <= remainder < Abs(divisor)
        }

        static function Witness(): (result: DivAnalysis)
        ensures result.Valid?()
        {
            reveal Valid?();
            DivAnalysis(0, 1, 0, 0, 0)
        }
    }
}

Command to run and resulting output

.\Dafny.exe verify --standard-libraries Repro.dfy

(No output)

What happened?

I'd expect this to verify. Instead, it just hangs.
If I remove the import, this verifies for me.
Also, if I remove the && 0 <= remainder < Abs(divisor) part of Valid?() this verifies. But all of this together does not.

I'd be interested in learning more about how Dafny works internally, so I'd be happy to try to debug into to the cause of this more if anyone can give me pointers on how to do that.

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

Windows

[nverhaaren]

Also let me know if this is expected behavior (and ideally how to work around it) - I'm just not sure how an import would cause this to happen, and it seems like a potential bug.

[stefan-aws]

I can confirm the behaviour. The problematic part seems to be 0 <= remainder, which should verify for remainder == 0, but doesn't if import Std.Arithmetic.DivMod is used. It does verify if you replace it with e.g. -1 <= remainder or any other number below 0.

[nverhaaren]

One thing that's confusing to me is how that import - which seems unused - affects the verification at all. Am I just missing something, or is that strange? Is there some way I try can figure out for myself at what stage of verification that import is having an effect?