Verifier crash when dereferencing map constant/function

[erniecohen]

Dafny version

4.10.0

Code to produce this issue

function c():map<nat,nat>
function f(v:nat):nat { c()[v]}

Command to run and resulting output

vscode

What happened?

Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.ArgumentException: Boogie program had 8 resolution errors:
Microsoft.Dafny.SourceOrigin: undeclared identifier: smt.lc.Env$V
Microsoft.Dafny.SourceOrigin: undeclared identifier: smt.lc.Env$V
Microsoft.Dafny.SourceOrigin: undeclared identifier: smt.lc.Env$V
Microsoft.Dafny.SourceOrigin: undeclared identifier: smt.lc.Env$V
Microsoft.Dafny.SourceOrigin: undeclared identifier: smt.lc.Env$V
Microsoft.Dafny.SourceOrigin: undeclared identifier: smt.lc.Env$V
Microsoft.Dafny.SourceOrigin: undeclared identifier: smt.lc.Env$V
Microsoft.Dafny.SourceOrigin: undeclared identifier: smt.lc.Env$V
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_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)
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)

What type of operating system are you experiencing the problem on?

Mac

[erniecohen]

Same problem occurs if c is a constant, and/or it is given a definition.