Verifier crash on match within assert by within function

[erniecohen]

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.<<VerifyUnverifiedSymbol>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)