Added returns with parameters to printer.

1 files changed, 11 insertions, 1 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 9970d61a..e49ce6e9 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -424,7 +424,17 @@ namespace Microsoft.Dafny {
         }

         

       } else if (stmt is ReturnStmt) {

-        wr.Write("return;");

+        var s = (ReturnStmt) stmt;

+        wr.Write("return");

+        if (s.rhss != null) {

+          var sep = " ";

+          foreach (var rhs in s.rhss) {

+            wr.Write(sep);

+            PrintRhs(rhs);

+            sep = ", ";

+          }

+        }

+          wr.Write(";");

         

       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;