function-by-method crash

[seanmcl]

Dafny correctly notices a duplicate method name, but then crashes. This is unlike regular functions and methods.

method f(x: seq<int>) returns (res: seq<int>)
  ensures x == res
{
  var y := [];
  for i := 0 to |x|
    invariant |y| == i
    invariant x[..i] == y[..i]
  {
    y := y + [x[i]];
  }
  return y;
}

function f(x: seq<int>): seq<int> {
  x
} by method {
  var y := [];
  for i := 0 to |x|
    invariant |y| == i
    invariant x[..i] == y[..i]
  {
    y := y + [x[i]];
  }
  return y;
}

$ dafny /compile:0 /tmp/foo.dfy
/tmp/foo.dfy(14,9): Error: Duplicate member name: f
Unhandled exception. System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.Resolver.ResolveMethod(Method m) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 10254
   at Microsoft.Dafny.Resolver.ResolveFunction(Function f) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 10164
   at Microsoft.Dafny.Resolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 9559
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 2811
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 1024
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 497
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/DafnyMain.cs:line 161
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(ExecutionEngineOptions options, IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyDriver/DafnyDriver.cs:line 290
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyDriver/DafnyDriver.cs:line 57
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass1_0.<Main>b__0() in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyDriver/DafnyDriver.cs:line 37
   at System.Threading.Thread.StartCallback()
[3]    36446 abort