cce+UnreachableException in Microsoft.Dafny.Substituter.SubstStmt

[alex-chew]

Verifying the following Dafny code under version nightly-2022-10-24-cd54451:

datatype D = D(x: int)

function Foo(): ()
  ensures assert true by { var D(x) := D(0); } true
{ () }

fails with the following stack trace:

Parsing <snip>/bug.dfy
Unhandled exception. System.AggregateException: One or more errors occurred. (Exception of type 'cce+UnreachableException' was thrown.)
 ---> cce+UnreachableException: Exception of type 'cce+UnreachableException' was thrown.
   at Microsoft.Dafny.Substituter.SubstStmt(Statement stmt)
   at System.Collections.Generic.List`1.ConvertAll[TOutput](Converter`2 converter)
   at Microsoft.Dafny.Substituter.SubstBlockStmt(BlockStmt stmt)
   at Microsoft.Dafny.Substituter.SubstStmt(Statement stmt)
   at Microsoft.Dafny.Substituter.Substitute(Expression expr)
   at Microsoft.Dafny.Translator.AddFunctionConsequenceAxiom(Function boogieFunction, Function f, List`1 ens)
   at Microsoft.Dafny.Translator.AddClassMember_Function(Function f)
   at Microsoft.Dafny.Translator.AddFunction_Top(Function f, Boolean includeAllMethods)
   at Microsoft.Dafny.Translator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType)
   at Microsoft.Dafny.Translator.AddTypeDecl(RevealableTypeDecl d)
   at Microsoft.Dafny.Translator.DoTranslation(Program p, ModuleDefinition forModule)
   at Microsoft.Dafny.Translator.Translate(Program p, ErrorReporter reporter, TranslatorFlags flags)+MoveNext()
   at Microsoft.Dafny.DafnyDriver.Translate(ExecutionEngineOptions options, Program dafnyProgram)+MoveNext()
   at System.Collections.Generic.List`1..ctor(IEnumerable`1 collection)
   at System.Linq.Enumerable.ToList[TSource](IEnumerable`1 source)
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args)
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0()
   at System.Threading.Thread.StartCallback()
Abort trap: 6

It seems important that the assert by block contains a pattern destructuring. Changing var D(x) := D(0); to var x := D(0); allows verification to pass as expected.