Incomplete regression for Dafny 4.0

[muchang]

Dafny version

4.0.0.50303

Code to produce this issue

method test(x: int, y: int){
    var tmp_1 := false;
    var tmp_2 := 2830 * x;
    var tmp_3 := 2451 - y;
    if (0 < tmp_2 * tmp_3) {
        var tmp_4 := 2830 * x;
        var tmp_5 := 2451 - y;
        if (tmp_4 * tmp_5 <= 9) {
            var tmp_6 := 2831 + x;
            var tmp_7 := 2450 * y;
            if (1 >= tmp_6 * tmp_7) {
                var tmp_8 := 2831 + x;
                var tmp_9 := 2450 * y;
                if (tmp_8 - tmp_9 <= 10) {
                    tmp_1 := true; 
                }
            }
        }
    }

    if (tmp_1) {
        assert false;
    }
}

Command to run and resulting output

$ dafny-3.13/dafny/dafny verify test.dfy
Dafny program verifier finished with 1 verified, 0 errors

$ dafny-4/dafny/dafny verify test.dfy
test.dfy(22,15):  Error: assertion might not hold

Dafny program verifier finished with 0 verified, 1 error

What happened?

Dafny4 reports the assertion might not hold while Dafny can successfully verify this.

If I substitute tmp_1 := true with assert false; or any variable with its assignment (like substituting tmp_2 with 2830 * x), Dafny4 can also verify this.

Are there any reasons about why such a substitution affects the verification result and why this regression happens in Dafny4?

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

Linux

[alex-chew]

Thanks for the report. I've been able to reproduce your results where the program verifies under Dafny 3.13.1.50302 but not under Dafny 4.0.0.50303. We'll investigate further.

[alex-chew]

Ah, note that in Dafny 4.0.0, the default version of Z3 changed from 4.8.5 to 4.12.1. It's unfortunate, though expected, that this may cause proof regressions - though it can also cause previously failing proofs to succeed.

Noting that your code snippet involves arithmetic, this issue may be related: #3501

[muchang]

Thanks for the investigation! It helps a lot. I am actually still wondering why the change of Z3's version will cause Dafny's failing proof.

I can imagine that it may happen if two versions produce different results (which means there was/is a soundness bug in Z3) or the current version of Z3 produces an unknown or timeout. But it would be surprising that Z3 has a soundness bug or timeout on this simple program. Do you have any idea about it? Is the failing proof due to the incorrect or unknown result of Z3 or there are some other reasons?

[atomb]

Due to the heavy use of quantifiers by Dafny, Z3 is almost always working in the space of undecidable theories, and therefore it is usually able to prove only "valid" or "unknown". The error that shows up with Dafny 4 is because Z3 is returning "unknown" when it previously returned "valid". It looks like the solution suggested in #3501, setting /proverOpt:O:smt.arith.solver=6, allows Z3 to easily prove the assertion. We've considered making that the default, but doing so unfortunately also causes many other proofs not to go through.

[muchang]

I see, it makes sense. I will consider using /proverOpt:O:smt.arith.solver=6 to have a better performance of Dafny, when it cannot give a proof in default. Thanks!