1 files changed, 2 insertions, 0 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 35f81605..1f9208db 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -641,7 +641,9 @@ namespace Microsoft.Dafny {
         Indent(indent);
         wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.UniqueId);
       } else if (stmt is ReturnStmt) {
+        var s = (ReturnStmt)stmt;
         Indent(indent);
+        TrStmt(s.hiddenUpdate, indent);
         wr.WriteLine("return;");
       } else if (stmt is UpdateStmt) {
         var s = (UpdateStmt)stmt;