cce+UnreachableException in Microsoft.Dafny.Substituter.SubstStmt #2920
Labels
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: verifier
Translation from Dafny to Boogie (translator)
Verifying the following Dafny code under version nightly-2022-10-24-cd54451:
fails with the following stack trace:
It seems important that the
assert by
block contains a pattern destructuring. Changingvar D(x) := D(0);
tovar x := D(0);
allows verification to pass as expected.The text was updated successfully, but these errors were encountered: