Failing code

datatype D = D 
function f(d:D):bool {
  assert true by {
    match d {
      case _ => assert true;
    }
  }
  true
}

Steps to reproduce the issue

• Dafny version: 4.7.0.0
• Dafny VSCode extension version: 3.3.1

Expected behavior

Actual behavior

Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
cce+UnreachableException: Exception of type 'cce+UnreachableException' was thrown.
at Microsoft.Dafny.Substituter.SubstStmt(Statement stmt)
at System.Collections.Generic.List1.ConvertAll[TOutput](Converter2 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.BoogieGenerator.GetFunctionAxiom(Function f, Expression body, List1 lits) at Microsoft.Dafny.BoogieGenerator.AddFunctionAxiom(Function boogieFunction, Function f, Expression body) at Microsoft.Dafny.BoogieGenerator.AddClassMember_Function(Function f) at Microsoft.Dafny.BoogieGenerator.AddFunction_Top(Function f, Boolean includeAllMethods) at Microsoft.Dafny.BoogieGenerator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType) at Microsoft.Dafny.BoogieGenerator.DoTranslation(Program p, ModuleDefinition forModule) at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.<>c__DisplayClass3_0.<GetVerificationTasksAsync>b__0() at System.Threading.Tasks.Task1.InnerInvoke()
at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
--- End of stack trace from previous location ---
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass54_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)