Fixed bug in compiler relating to returns with parameters.

1 files changed, 3 insertions, 3 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 1f9208db..920105a9 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -642,9 +642,9 @@ namespace Microsoft.Dafny {
         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;");

+        if (s.hiddenUpdate != null)

+          TrStmt(s.hiddenUpdate, indent);

+        Indent(indent); wr.WriteLine("return;");

       } else if (stmt is UpdateStmt) {

         var s = (UpdateStmt)stmt;

         var resolved = s.ResolvedStatements;