Verification failures only with --isolating-assertions?

[hmijail]

I have a lemma which consistently verifies correctly with random seeds.
However, when I use --isolating-assertions, it fails about 75% of the time.
Note that this is a hard fail with a resource count well under the limit:

Error: a postcondition could not be proved on this return path

I am not sure how to think about this.

• Is it a bug in Dafny?
• It's the only case I have found in our repo, so doesn't seem common. But, is it "acceptable"?
• Would it be good in any way to try to make it fail less, given that "normal" verification works?

Dafny 4.6

[stefan-aws]

Is this related to #5424? Is it possible to share the file that fails to verify?

[hmijail]

No, I guess it's not really related... though to my mind this is a good example of verify turning into a dead end (because it just fails) while measure-complexity allows me to poke at the problem to see what's going on.

The code is gas.dfy. Sorry that I didn't include it earlier, I assumed it might be something easily dismissible.

This verifies correctly:

$ dafny measure-complexity --random-seed 1715571600 --iterations 10 gas.dfy
Starting verification of iteration 0 with seed 1715571600
Starting verification of iteration 1 with seed 1868733242
Starting verification of iteration 2 with seed 141932388
Starting verification of iteration 3 with seed 2088285157
Starting verification of iteration 4 with seed 1055107221
Starting verification of iteration 5 with seed 327767518
Starting verification of iteration 6 with seed 12461784
Starting verification of iteration 7 with seed 1027665046
Starting verification of iteration 8 with seed 159801794
Starting verification of iteration 9 with seed 1403650583

Dafny program verifier finished with 650 verified, 0 errors

Add --isolate-assertions to see it fail 8 out of 10 iterations.

$ dafny measure-complexity --random-seed 1715571600 --iterations 10 --isolate-assertions gas.dfy
Starting verification of iteration 0 with seed 1715571600
Starting verification of iteration 1 with seed 1868733242
gas.dfy(89,4): Error: a postcondition could not be proved on this return path
gas.dfy(88,40): Related location: this is the postcondition that could not be proved
Starting verification of iteration 2 with seed 141932388
Starting verification of iteration 3 with seed 2088285157
gas.dfy(89,4): Error: a postcondition could not be proved on this return path
gas.dfy(88,40): Related location: this is the postcondition that could not be proved
Starting verification of iteration 4 with seed 1055107221
gas.dfy(89,4): Error: a postcondition could not be proved on this return path
gas.dfy(88,40): Related location: this is the postcondition that could not be proved
Starting verification of iteration 5 with seed 327767518
gas.dfy(89,4): Error: a postcondition could not be proved on this return path
gas.dfy(88,40): Related location: this is the postcondition that could not be proved
Starting verification of iteration 6 with seed 12461784
gas.dfy(89,4): Error: a postcondition could not be proved on this return path
gas.dfy(88,40): Related location: this is the postcondition that could not be proved
Starting verification of iteration 7 with seed 1027665046
gas.dfy(89,4): Error: a postcondition could not be proved on this return path
gas.dfy(88,40): Related location: this is the postcondition that could not be proved
Starting verification of iteration 8 with seed 159801794
gas.dfy(89,4): Error: a postcondition could not be proved on this return path
gas.dfy(88,40): Related location: this is the postcondition that could not be proved
Starting verification of iteration 9 with seed 1403650583
gas.dfy(89,4): Error: a postcondition could not be proved on this return path
gas.dfy(88,40): Related location: this is the postcondition that could not be proved

Dafny program verifier finished with 3052 verified, 8 errors

Note that with many other random seeds it fails the 10 iterations in a row.

[keyboardDrummer]

I think it's uncommon that --isolate-assertions makes a proof less stable, but it's not unimaginable. If you have assert A; assert B, then the solver might learn things when proving A that it then uses to prove B. --isolate-assertions will turn the program into two proofs, one assert A and another assume A; assert B, so then the learning of proving A can no longer be used when proving B. There might be some property C that is useful both for proving A and for B, that if you assert it as well, will make your proof stable even when using --isolate-assertions.