Dafny: Fixed an assertion violation in the "Checked" configuration.

1 files changed, 3 insertions, 1 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a1058786..17df4e06 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1069,9 +1069,11 @@ namespace Microsoft.Dafny {
         stmts = builder.Collect(m.tok);

       }

 

+      QKeyValue kv = etran.TrAttributes(m.Attributes);

+

       Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,

         typeParams, inParams, outParams,

-        localVariables, stmts, etran.TrAttributes(m.Attributes));

+        localVariables, stmts, kv);

       sink.TopLevelDeclarations.Add(impl);

 

       currentMethod = null;