ArgumentNullException in resolver (ProgramTraverser.Traverse)

[cpitclaudel]

Input:

method test() returns (a: bool, b: int) {
  return (true, 0);
}

Output:

Unhandled exception. System.AggregateException: One or more errors occurred. (Value cannot be null. (Parameter 'source'))
 ---> System.ArgumentNullException: Value cannot be null. (Parameter 'source')
   at System.Linq.ThrowHelper.ThrowArgumentNullException(ExceptionArgument argument)
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.ProgramTraverser.Traverse(Expression expr, String field, Object parent) in C:\dafny\Source\DafnyCore\Util.cs:line 783
   at Microsoft.Dafny.SubsetConstraintGhostChecker.Traverse(Expression expr, String field, Object parent) in C:\dafny\Source\DafnyCore\Resolver.cs:line 18218
   at Microsoft.Dafny.ProgramTraverser.<>c__DisplayClass17_0.<Traverse>b__0(Expression subExpr) in C:\dafny\Source\DafnyCore\Util.cs:line 767
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.ProgramTraverser.Traverse(Statement stmt, String field, Object parent) in C:\dafny\Source\DafnyCore\Util.cs:line 767
   at Microsoft.Dafny.ProgramTraverser.<>c__DisplayClass17_0.<Traverse>b__2(Statement subStmt) in C:\dafny\Source\DafnyCore\Util.cs:line 769
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.ProgramTraverser.Traverse(Statement stmt, String field, Object parent) in C:\dafny\Source\DafnyCore\Util.cs:line 767
   at Microsoft.Dafny.ProgramTraverser.Traverse(MemberDecl memberDeclaration, String field, Object parent) in C:\dafny\Source\DafnyCore\Util.cs:line 749
   at Microsoft.Dafny.ProgramTraverser.<>c__DisplayClass15_0.<Traverse>b__0(MemberDecl memberDecl) in C:\dafny\Source\DafnyCore\Util.cs:line 623
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.ProgramTraverser.Traverse(TopLevelDecl topd) in C:\dafny\Source\DafnyCore\Util.cs:line 623
   at Microsoft.Dafny.ProgramTraverser.Traverse(List`1 topLevelDecls) in C:\dafny\Source\DafnyCore\Util.cs:line 564
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in C:\dafny\Source\DafnyCore\Resolver.cs:line 3546
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in C:\dafny\Source\DafnyCore\Resolver.cs:line 1032
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in C:\dafny\Source\DafnyCore\Resolver.cs:line 504
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in C:\dafny\Source\DafnyCore\DafnyMain.cs:line 210
   at Microsoft.Dafny.Main.ParseCheck(IList`1 files, String programName, ErrorReporter reporter, Program& program) in C:\dafny\Source\DafnyCore\DafnyMain.cs:line 161
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in C:\dafny\Source\DafnyDriver\DafnyDriver.cs:line 305
   --- 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) in C:\dafny\Source\DafnyDriver\DafnyDriver.cs:line 116
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass9_0.<Main>b__0() in C:\dafny\Source\DafnyDriver\DafnyDriver.cs:line 92
   at System.Threading.Thread.StartCallback()

[alex-chew]

It seems that this occurs even if the values in the tuple don't match up with the declared return types. For example, the same error occurs if you write:

method test() returns (a: bool, b: int) {
  return (0, true);
}

(version nightly-2022-10-28-f2664b7)