assertion of map values fails when same postcondition succeeds (or if preceded by Keys assertion) #5527
Labels
incompleteness
Things that Dafny should be able to prove, but can't
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: verifier
Translation from Dafny to Boogie (translator)
priority: not yet
Will reconsider working on this when we're looking for work
Dafny version
4.6.0.0 nightly
Code to produce this issue
Steps to reproduce the issue
Expected behavior
Actual behavior
Command to run and resulting output
What happened?
I'd kind of hope it verifies...
Note I lodged this by pressing the IDE button, not realising that would put it in the wrong place: dafny-lang/ide-vscode#478
What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered: