Some verification iterations are successful, some fail?

[hmijail]

Dafny version

4.7

Code to produce this issue

See attached file, which for convenience for this issue, was generated with 
dafny resolve src/weth_0_main.dfy --print preprocessed.dfy --print-mode Everything

(from the repo https://github.com/Consensys/WrappedEther.dfy )

Command to run and resulting output

$ dafny measure-complexity preprocessed.dfy --iterations 10 --filter-symbol 0a59 --resource-limit 100000000 --random-seed 1 

preprocessed.dfy(3066,24): Warning: The {:verify false} attribute should only be used during development. Consider using a bodyless lemma together with the {:axiom} attribute instead
preprocessed.dfy(4265,24): Warning: The {:verify false} attribute should only be used during development. Consider using a bodyless lemma together with the {:axiom} attribute instead
preprocessed.dfy(4270,24): Warning: The {:verify false} attribute should only be used during development. Consider using a bodyless lemma together with the {:axiom} attribute instead
preprocessed.dfy(4275,24): Warning: The {:verify false} attribute should only be used during development. Consider using a bodyless lemma together with the {:axiom} attribute instead
preprocessed.dfy(4280,24): Warning: The {:verify false} attribute should only be used during development. Consider using a bodyless lemma together with the {:axiom} attribute instead
Starting verification of iteration 0 with seed 1
preprocessed.dfy(588,24): Error: a precondition for this call could not be proved
preprocessed.dfy(597,67): Related location: this is the precondition that could not be proved
Starting verification of iteration 1 with seed 534011718
preprocessed.dfy(572,9): Error: Verification out of resource (main.block_0_0x0a59)
Starting verification of iteration 2 with seed 237820880
Starting verification of iteration 3 with seed 1002897798
Starting verification of iteration 4 with seed 1657007234
preprocessed.dfy(588,24): Error: a precondition for this call could not be proved
preprocessed.dfy(597,67): Related location: this is the precondition that could not be proved
Starting verification of iteration 5 with seed 1412011072
preprocessed.dfy(572,9): Error: Verification out of resource (main.block_0_0x0a59)
Starting verification of iteration 6 with seed 929393559
preprocessed.dfy(572,9): Error: Verification out of resource (main.block_0_0x0a59)
Starting verification of iteration 7 with seed 760389092
preprocessed.dfy(588,24): Error: a precondition for this call could not be proved
preprocessed.dfy(597,67): Related location: this is the precondition that could not be proved
Starting verification of iteration 8 with seed 2026928803
preprocessed.dfy(572,9): Error: Verification out of resource (main.block_0_0x0a59)
Starting verification of iteration 9 with seed 217468053

Dafny program verifier finished with 13 verified, 3 errors, 4 out of resource

What happened?

Ignoring the iterations that are out of resources: some iterations are successful, and some fail in a consistent position. Of course the proportion changes with the random seed used.

Is this a bug in Dafny? If not, how to think about this?

Relatedly: the FAQ in the Dafny repo wiki says

Dafny is designed to be sound but incomplete.

If a verification result caused a false alarm, would it look like this case: flip-flopping between reporting an issue and not reporting it? Or would it be a consistent false alarm?
preprocessed.dfy.zip

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

Mac

[atomb]

This is almost certainly a case of incompleteness. If Dafny succeeds on some iterations, you should treat that as an overall verification success, but perhaps an indication that some refactoring is warranted.

Since the SMT solver takes a slightly different path to verification depending on the random, it can fail to find a proof in various different ways, some which result in exceeding resource or time limits and some of which fail earlier. The behavior you're seeing is something that happens somewhat regularly for complex code. There are approaches you can take to optimize verification to make it less likely. Some of those are documented here, though that's due for a bit of an update based on recent experience we've gathered.

[atomb]

Closing, since it's fundamentally an issue we'll never be able to fully resolve due to undecidability.