Resource Limit hides subsequent assertion failures within a method #5805
Labels
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
misc: brittleness
When Dafny sometimes proves something, and sometimes doesn't
part: verifier
Translation from Dafny to Boogie (translator)
priority: next
Will consider working on this after in progress work is done
Dafny version
4.8.1
Code to produce this issue
Command to run and resulting output
What happened?
The example contains 3 methods with identical bodies. Dafny gives different results based on the provided resource limit.
I was surprised by dafny's behavior on the first method.
F
(moderate resources): Only the second assertion is marked as failing, implying that the other 2 are ok.F1
(unlimited resources): All three assertions are detected as failingF2
(almost no resources): A "out of resource" message is reportedThe same happens in VSCode, see screenshot.
Using timeouts, the same behavior can be observed, but less repeatable.
Discussed with @RustanLeino in-person a few weeks ago.
What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered: