diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index 7ee7455d38..7edddd6163 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -1367,7 +1367,7 @@ private ConcreteSyntaxTree CreateSubroutine(string name, List { + method Bar(ghost x: T, y: T) returns (z: T) +} + +class MyClass extends MyTrait { + constructor() {} + method Bar(ghost x: int, y: int) returns (z: int) { + return y; + } +} + +method Main() { + var c := new MyClass(); + var z := c.Bar(7, 42); + expect z == 42; +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-5814.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-5814.dfy.expect new file mode 100644 index 0000000000..e69de29bb2