Malformed triggers #2593
Labels
crash
Dafny crashes on this input, or generates malformed code that can not be executed
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: verifier
Translation from Dafny to Boogie (translator)
The following Dafny program has a
old
in a less-than-commendable, but legal, position:Alas, the program causes Dafny to generate malformed Boogie code, because of the trigger Dafny generates for the quantifier.
Additional trigger information:
The text was updated successfully, but these errors were encountered: