strange assertion failure

[toNanjingnan]

Dafny version

4.6.0

Code to produce this issue

method Main(){
    var lift_5 := {false, false};
    var lift_1 := {true, true, true};
    assert (((2 == |((lift_1 * lift_1) + (lift_1 + lift_5 + lift_1))|)));
}

Command to run and resulting output

// verify dfy file
$ dafny test.dfy
 
output:
test.dfy(8,11): Error: assertion might not hold

Dafny program verifier finished with 0 verified, 1 error

What happened?

the assertion fails but it should be true. Print the expression in the assertion and the result is true. when I add some assertion using the component of expression in the failed assertion, it suddenly stops failing.

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

Windows

[robin-aws]

This is a classic symptom of the fact that Dafny verification is extremely powerful but fundamentally incomplete: there will always be assertions that are in fact true but where Dafny cannot prove they are true without help.

https://dafny.org/dafny/DafnyRef/DafnyRef#sec-verification has lots of information about how to debug failing verification and add assertions as necessary to fix it (as you did by accident when trying to debug it :)

[MikaelMayer]

If we had changed "assertion might not hold" to "assertion could not be proved", how would you have reacted? Same or differently?