Internal error: Unhandled exception: System.NullReferenceException

[wiegerw]

Dafny version

4.11.0.0

Code to produce this issue

git clone https://github.com/wiegerw/minimax.git
cd minimax/dafny
dafny verify negamax-ttw.dfy

Command to run and resulting output

/home/user/.vscode/extensions/dafny-lang.ide-vscode-3.5.2/out/resources/4.11.0/github/dafny/dafny verify negamax-ttw.dfy
Encountered internal compilation exception: Object reference not set to an instance of an object.
Unhandled exception: System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.FunctionCallExpr.get_SubExpressions()+MoveNext()
   at Microsoft.Boogie.CollectionExtensions.ForEach[T](IEnumerable`1 coll, Action`1 action)
   at Microsoft.Dafny.TopDownVisitor`1.Visit(Expression expr, State st)
   at Microsoft.Dafny.TopDownVisitor`1.<>c__DisplayClass3_0.<Visit>b__2(Expression e)
   at Microsoft.Boogie.CollectionExtensions.ForEach[T](IEnumerable`1 coll, Action`1 action)
   at Microsoft.Dafny.TopDownVisitor`1.Visit(Expression expr, State st)
   at Microsoft.Dafny.TopDownVisitor`1.<>c__DisplayClass4_0.<Visit>b__2(Expression e)
   at Microsoft.Boogie.CollectionExtensions.ForEach[T](IEnumerable`1 coll, Action`1 action)
   at Microsoft.Dafny.TopDownVisitor`1.Visit(Statement stmt, State st)
   at Microsoft.Dafny.TopDownVisitor`1.<>c__DisplayClass4_0.<Visit>b__3(Statement s)
   at Microsoft.Boogie.CollectionExtensions.ForEach[T](IEnumerable`1 coll, Action`1 action)
   at Microsoft.Dafny.TopDownVisitor`1.Visit(Statement stmt, State st)
   at Microsoft.Dafny.TopDownVisitor`1.<>c__DisplayClass4_0.<Visit>b__3(Statement s)
   at Microsoft.Boogie.CollectionExtensions.ForEach[T](IEnumerable`1 coll, Action`1 action)
   at Microsoft.Dafny.TopDownVisitor`1.Visit(Statement stmt, State st)
   at Microsoft.Dafny.TopDownVisitor`1.Visit(MethodOrConstructor method, State st)
   at Microsoft.Dafny.TopDownVisitor`1.Visit(ICallable decl, State st)
   at Microsoft.Dafny.PrecedenceLinter.PreResolve(ModuleDefinition moduleDefinition)
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation)
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.Compilation.ResolveAsync()
   at Microsoft.Dafny.VerifyCommand.HandleVerification(DafnyOptions options)
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass5_0.<<SetHandlerUsingDafnyOptionsContinuation>g__Handle|0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Invocation.AnonymousCommandHandler.InvokeAsync(InvocationContext context)
   at System.CommandLine.Invocation.InvocationPipeline.<>c__DisplayClass4_0.<<BuildInvocationChain>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass17_0.<<UseParseErrorReporting>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass12_0.<<UseHelp>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass17_0.<<AddDeveloperHelp>b__1>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass22_0.<<UseVersionOption>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass19_0.<<UseTypoCorrections>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<UseSuggestDirective>b__18_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass16_0.<<UseParseDirective>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<RegisterWithDotnetSuggest>b__5_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass8_0.<<UseExceptionHandler>b__0>d.MoveNext()

What happened?

The code runs fine in VSCode with Dafny 4.10. After moving to Dafny 4.11.0 I get an internal compiler error in two files in the repository. The code above shows that the error can be reproduced without VSCode.

For completeness, I have checked out the repository at commit 7d842fb85a0275a4a8e4d7e040d2625abbf7f084 (the current version).

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

Linux