Merge

13 files changed, 713 insertions, 587 deletions

diff --git a/.hgignore b/.hgignore
index 9fc841bd..a52bee3a 100644
--- a/.hgignore
+++ b/.hgignore
@@ -1,6 +1,6 @@
 syntax: regexp

 ^Source/.*\.(user|suo|cache|vs10x)$

-^Binaries/.*\.(dll|pdb|exe|manifest|config|smt2|vsix|vsixmanifest|bpl|pkgdef)$

+^Binaries/.*\.(dll|pdb|exe|manifest|config|smt2|vsix|vsixmanifest|bpl|pkgdef|xml)$

 ^Source/.*\.(smt2|bpl)$

 ^.*(bin|obj)/([^/]*/)?(Debug|Release|Checked|Debug All|DEBUG ALL)/.*$

 Test/.*/Output

@@ -21,4 +21,6 @@ syntax: glob
 *.tmp

 *.tmp.dfy

 Source/DafnyExtension/DafnyRuntime.cs

+Source/DafnyExtension/Z3-LICENSE.txt

 Test/failing.lst

+packages/*

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index aa4ca3ec..f992d6c0 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -14,18 +14,11 @@ using System.Text;
 

 namespace Microsoft.Dafny {

   public class Compiler {

-    public Compiler(TextWriter wr) {

-      Contract.Requires(wr != null);

-      this.wr = wr;

+    public Compiler() {

+  

     }

 

-    [ContractInvariantMethod]

-    void ObjectInvariant()

-    {

-      Contract.Invariant(wr!=null);

-    }

-

-    TextWriter wr;

+    StringBuilder copyInstrWriter = new StringBuilder(); // a buffer that stores copy instructions generated by letExpr that uses out param.

     Method enclosingMethod;  // non-null when a method body is being translated

 

     FreshIdGenerator idGenerator = new FreshIdGenerator();

@@ -50,7 +43,7 @@ namespace Microsoft.Dafny {
     public int ErrorCount;

     public TextWriter ErrorWriter = Console.Out;

 

-    void Error(string msg, params object[] args) {

+    void Error(string msg, TextWriter wr, params object[] args) {

       Contract.Requires(msg != null);

       Contract.Requires(args != null);

 

@@ -60,7 +53,7 @@ namespace Microsoft.Dafny {
       ErrorCount++;

     }

 

-    void ReadRuntimeSystem() {

+    void ReadRuntimeSystem(TextWriter wr) {

       string codebase = cce.NonNull( System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));

       string path = System.IO.Path.Combine(codebase, "DafnyRuntime.cs");

       using (TextReader rd = new StreamReader(new FileStream(path, System.IO.FileMode.Open, System.IO.FileAccess.Read)))

@@ -75,16 +68,16 @@ namespace Microsoft.Dafny {
     }

 

     readonly int IndentAmount = 2;

-    void Indent(int ind) {

+    void Indent(int ind, TextWriter wr) {

       Contract.Requires(0 <= ind);

       string spaces = "          ";

       for (; spaces.Length < ind; ind -= spaces.Length) {

         wr.Write(spaces);

       }

-      wr.Write(spaces.Substring(0, ind));

+     wr.Write(spaces.Substring(0, ind));

     }

 

-    public void Compile(Program program) {

+    public void Compile(Program program, TextWriter wr) {

       Contract.Requires(program != null);

       wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);

       wr.WriteLine("// To recompile, use 'csc' with: /r:System.Numerics.dll");

@@ -92,8 +85,8 @@ namespace Microsoft.Dafny {
       wr.WriteLine("// You might also want to include compiler switches like:");

       wr.WriteLine("//     /debug /nowarn:0164 /nowarn:0219");

       wr.WriteLine();

-      ReadRuntimeSystem();

-      CompileBuiltIns(program.BuiltIns);

+      ReadRuntimeSystem(wr);

+      CompileBuiltIns(program.BuiltIns, wr);

 

       foreach (ModuleDefinition m in program.CompileModules) {

         if (m.IsAbstract) {

@@ -117,33 +110,33 @@ namespace Microsoft.Dafny {
           wr.WriteLine();

           if (d is OpaqueTypeDecl) {

             var at = (OpaqueTypeDecl)d;

-            Error("Opaque type ('{0}') cannot be compiled", at.FullName);

+            Error("Opaque type ('{0}') cannot be compiled", wr, at.FullName);

           } else if (d is TypeSynonymDecl) {

             // do nothing, just bypass type synonyms in the compiler

           } else if (d is NewtypeDecl) {

             var nt = (NewtypeDecl)d;

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("public class @{0} {{", nt.CompileName);

             if (nt.NativeType != null) {

-              Indent(indent + IndentAmount);

+              Indent(indent + IndentAmount, wr);

               wr.WriteLine("public static System.Collections.Generic.IEnumerable<{0}> IntegerRange(BigInteger lo, BigInteger hi) {{", nt.NativeType.Name);

-              Indent(indent + 2 * IndentAmount);

+              Indent(indent + 2 * IndentAmount, wr);

               wr.WriteLine("for (var j = lo; j < hi; j++) {{ yield return ({0})j; }}", nt.NativeType.Name);

-              Indent(indent + IndentAmount);

+              Indent(indent + IndentAmount, wr);

               wr.WriteLine("}");

             }

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("}");

           } else if (d is DatatypeDecl) {

             var dt = (DatatypeDecl)d;

-            Indent(indent);

+            Indent(indent, wr);

             wr.Write("public abstract class Base_{0}", dt.CompileName);

             if (dt.TypeArgs.Count != 0) {

               wr.Write("<{0}>", TypeParameters(dt.TypeArgs));

             }

             wr.WriteLine(" { }");

-            CompileDatatypeConstructors(dt, indent);

-            CompileDatatypeStruct(dt, indent);

+            CompileDatatypeConstructors(dt, indent, wr);

+            CompileDatatypeStruct(dt, indent, wr);

           } else if (d is IteratorDecl) {

             var iter = (IteratorDecl)d;

             // An iterator is compiled as follows:

@@ -169,7 +162,7 @@ namespace Microsoft.Dafny {
             //     }

             //   }

 

-            Indent(indent);

+            Indent(indent, wr);

             wr.Write("public class @{0}", iter.CompileName);

             if (iter.TypeArgs.Count != 0) {

               wr.Write("<{0}>", TypeParameters(iter.TypeArgs));

@@ -181,58 +174,58 @@ namespace Microsoft.Dafny {
             foreach (var member in iter.Members) {

               var f = member as Field;

               if (f != null && !f.IsGhost) {

-                Indent(ind);

-                wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));

+                Indent(ind, wr);

+                wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type, wr), f.CompileName, DefaultValue(f.Type, wr));

               } else if (member is Constructor) {

                 Contract.Assert(ct == null);  // we're expecting just one constructor

                 ct = (Constructor)member;

               }

             }

             Contract.Assert(ct != null);  // we do expect a constructor

-            Indent(ind); wr.WriteLine("System.Collections.Generic.IEnumerator<object> __iter;");

+            Indent(ind, wr); wr.WriteLine("System.Collections.Generic.IEnumerator<object> __iter;");

 

             // here's the initializer method

-            Indent(ind); wr.Write("public void @{0}(", ct.CompileName);

+            Indent(ind, wr); wr.Write("public void @{0}(", ct.CompileName);

             string sep = "";

             foreach (var p in ct.Ins) {

               if (!p.IsGhost) {

                 // here we rely on the parameters and the corresponding fields having the same names

-                wr.Write("{0}{1} @{2}", sep, TypeName(p.Type), p.CompileName);

+                wr.Write("{0}{1} @{2}", sep, TypeName(p.Type, wr), p.CompileName);

                 sep = ", ";

               }

             }

             wr.WriteLine(") {");

             foreach (var p in ct.Ins) {

               if (!p.IsGhost) {

-                Indent(ind + IndentAmount);

+                Indent(ind + IndentAmount, wr);

                 wr.WriteLine("this.@{0} = @{0};", p.CompileName);

               }

             }

-            Indent(ind + IndentAmount); wr.WriteLine("__iter = TheIterator();");

-            Indent(ind);  wr.WriteLine("}");

+            Indent(ind + IndentAmount, wr); wr.WriteLine("__iter = TheIterator();");

+            Indent(ind, wr);  wr.WriteLine("}");

             // here are the enumerator methods

-            Indent(ind); wr.WriteLine("public void MoveNext(out bool more) { more = __iter.MoveNext(); }");

-            Indent(ind); wr.WriteLine("private System.Collections.Generic.IEnumerator<object> TheIterator() {");

+            Indent(ind, wr); wr.WriteLine("public void MoveNext(out bool more) { more = __iter.MoveNext(); }");

+            Indent(ind, wr); wr.WriteLine("private System.Collections.Generic.IEnumerator<object> TheIterator() {");

             if (iter.Body == null) {

-              Error("Iterator {0} has no body", iter.FullName);

+              Error("Iterator {0} has no body", wr, iter.FullName);

             } else {

-              TrStmt(iter.Body, ind + IndentAmount);

+              wr.Write(TrStmt(iter.Body, ind + IndentAmount).ToString());

             }

-            Indent(ind + IndentAmount); wr.WriteLine("yield break;");

-            Indent(ind); wr.WriteLine("}");

+            Indent(ind + IndentAmount, wr); wr.WriteLine("yield break;");

+            Indent(ind, wr); wr.WriteLine("}");

             // end of the class

-            Indent(indent); wr.WriteLine("}");

+            Indent(indent, wr); wr.WriteLine("}");

 

           }

           else if (d is TraitDecl)

           {

               //writing the trait

               var trait = (TraitDecl)d;

-              Indent(indent);

+              Indent(indent, wr);

               wr.Write("public interface @{0}", trait.CompileName);

               wr.WriteLine(" {");

-              CompileClassMembers(trait, false, indent + IndentAmount);

-              Indent(indent); wr.WriteLine("}");

+              CompileClassMembers(trait, false, indent + IndentAmount, wr);

+              Indent(indent, wr); wr.WriteLine("}");

 

               //writing the _Companion class

               List<MemberDecl> members = new List<MemberDecl>();

@@ -252,27 +245,27 @@ namespace Microsoft.Dafny {
                       }

                   }

               }

-              Indent(indent);

+              Indent(indent, wr);

               wr.Write("public class @_Companion_{0}", trait.CompileName);

               wr.WriteLine(" {");

-              CompileClassMembers(trait, true, indent + IndentAmount);

-              Indent(indent); wr.WriteLine("}");

+              CompileClassMembers(trait, true, indent + IndentAmount, wr);

+              Indent(indent, wr); wr.WriteLine("}");

           }

           else if (d is ClassDecl) {

             var cl = (ClassDecl)d;

-            Indent(indent);

+            Indent(indent, wr);

             wr.Write("public class @{0}", cl.CompileName);

             if (cl.TypeArgs.Count != 0) {

               wr.Write("<{0}>", TypeParameters(cl.TypeArgs));

             }

             string sep = " : ";

             foreach (var trait in cl.TraitsTyp) {

-              wr.Write("{0}{1}", sep, TypeName(trait));

+              wr.Write("{0}{1}", sep, TypeName(trait, wr));

               sep = ", ";

             }

             wr.WriteLine(" {");

-            CompileClassMembers(cl, false, indent+IndentAmount);

-            Indent(indent);  wr.WriteLine("}");

+            CompileClassMembers(cl, false, indent+IndentAmount, wr);

+            Indent(indent, wr);  wr.WriteLine("}");

           } else if (d is ModuleDecl) {

             // nop

           } else { Contract.Assert(false); }

@@ -283,15 +276,15 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void CompileBuiltIns(BuiltIns builtIns) {

+    void CompileBuiltIns(BuiltIns builtIns, TextWriter wr) {

       wr.WriteLine("namespace Dafny {");

-      Indent(IndentAmount);

+      Indent(IndentAmount, wr);

       wr.WriteLine("public partial class Helpers {");

       foreach (var decl in builtIns.SystemModule.TopLevelDecls) {

         if (decl is ArrayClassDecl) {

           int dims = ((ArrayClassDecl)decl).Dims;

           // public static T[,] InitNewArray2<T>(BigInteger size0, BigInteger size1) {

-          Indent(3 * IndentAmount);

+          Indent(3 * IndentAmount, wr);

           wr.Write("public static T[");

           RepeatWrite(wr, dims, "", ",");

           wr.Write("] InitNewArray{0}<T>(", dims);

@@ -299,52 +292,52 @@ namespace Microsoft.Dafny {
           wr.WriteLine(") {");

           // int s0 = (int)size0;

           for (int i = 0; i < dims; i++) {

-            Indent(4 * IndentAmount);

+            Indent(4 * IndentAmount, wr);

             wr.WriteLine("int s{0} = (int)size{0};", i);

           }

           // T[,] a = new T[s0, s1];

-          Indent(4 * IndentAmount);

+          Indent(4 * IndentAmount, wr);

           wr.Write("T[");

           RepeatWrite(wr, dims, "", ",");

           wr.Write("] a = new T[");

           RepeatWrite(wr, dims, "s{0}", ",");

           wr.WriteLine("];");

           // BigInteger[,] b = a as BigInteger[,];

-          Indent(4 * IndentAmount);

+          Indent(4 * IndentAmount, wr);

           wr.Write("BigInteger[");

           RepeatWrite(wr, dims, "", ",");

           wr.Write("] b = a as BigInteger[");

           RepeatWrite(wr, dims, "", ",");

           wr.WriteLine("];");

           // if (b != null) {

-          Indent(4 * IndentAmount);

+          Indent(4 * IndentAmount, wr);

           wr.WriteLine("if (b != null) {");

           // BigInteger z = new BigInteger(0);

-          Indent(5 * IndentAmount);

+          Indent(5 * IndentAmount, wr);

           wr.WriteLine("BigInteger z = new BigInteger(0);");

           // for (int i0 = 0; i0 < s0; i0++)

           //   for (int i1 = 0; i1 < s1; i1++)

           for (int i = 0; i < dims; i++) {

-            Indent((5+i) * IndentAmount);

+            Indent((5+i) * IndentAmount, wr);

             wr.WriteLine("for (int i{0} = 0; i{0} < s{0}; i{0}++)", i);

           }

           // b[i0,i1] = z;

-          Indent((5+dims) * IndentAmount);

+          Indent((5+dims) * IndentAmount, wr);

           wr.Write("b[");

           RepeatWrite(wr, dims, "i{0}", ",");

           wr.WriteLine("] = z;");

           // }

-          Indent(4 * IndentAmount);

+          Indent(4 * IndentAmount, wr);

           wr.WriteLine("}");

           // return a;

-          Indent(4 * IndentAmount);

+          Indent(4 * IndentAmount, wr);

           wr.WriteLine("return a;");

           // }

-          Indent(3 * IndentAmount);

+          Indent(3 * IndentAmount, wr);

           wr.WriteLine("}");  // end of method

         }

       }

-      Indent(IndentAmount);

+      Indent(IndentAmount, wr);

       wr.WriteLine("}");  // end of class Helpers

       wr.WriteLine("}");  // end of namespace

     }

@@ -359,7 +352,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void CompileDatatypeConstructors(DatatypeDecl dt, int indent)

+    void CompileDatatypeConstructors(DatatypeDecl dt, int indent, TextWriter wr)

     {

       Contract.Requires(dt != null);

 

@@ -372,20 +365,20 @@ namespace Microsoft.Dafny {
         //   public Dt__Lazy(Computer c) { this.c = c; }

         //   public Base_Dt<T> Get() { return c(); }

         // }

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("public class {0}__Lazy{1} : Base_{0}{1} {{", dt.CompileName, typeParams);

         int ind = indent + IndentAmount;

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public delegate Base_{0}{1} Computer();", dt.CompileName, typeParams);

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public delegate Computer ComputerComputer();");

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("Computer c;");

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public {0}__Lazy(Computer c) {{ this.c = c; }}", dt.CompileName);

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public Base_{0}{1} Get() {{ return c(); }}", dt.CompileName, typeParams);

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("}");

       }

 

@@ -407,7 +400,7 @@ namespace Microsoft.Dafny {
         //     // ...

         //   }

         // }

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("public class {0}", DtCtorDeclarationName(ctor, dt.TypeArgs));

         wr.WriteLine(" : Base_{0}{1} {{", dt.CompileName, typeParams);

         int ind = indent + IndentAmount;

@@ -415,32 +408,32 @@ namespace Microsoft.Dafny {
         int i = 0;

         foreach (Formal arg in ctor.Formals) {

           if (!arg.IsGhost) {

-            Indent(ind);

-            wr.WriteLine("public readonly {0} @{1};", TypeName(arg.Type), FormalName(arg, i));

+            Indent(ind, wr);

+            wr.WriteLine("public readonly {0} @{1};", TypeName(arg.Type, wr), FormalName(arg, i));

             i++;

           }

         }

 

-        Indent(ind);

+        Indent(ind, wr);

         wr.Write("public {0}(", DtCtorDeclartionName(ctor));

-        WriteFormals("", ctor.Formals);

+        WriteFormals("", ctor.Formals, wr);

         wr.WriteLine(") {");

         i = 0;

         foreach (Formal arg in ctor.Formals) {

           if (!arg.IsGhost) {

-            Indent(ind + IndentAmount);

+            Indent(ind + IndentAmount, wr);

             wr.WriteLine("this.@{0} = @{0};", FormalName(arg, i));

             i++;

           }

         }

-        Indent(ind);  wr.WriteLine("}");

+        Indent(ind, wr);  wr.WriteLine("}");

 

         // Equals method

-        Indent(ind); wr.WriteLine("public override bool Equals(object other) {");

-        Indent(ind + IndentAmount);

+        Indent(ind, wr); wr.WriteLine("public override bool Equals(object other) {");

+        Indent(ind + IndentAmount, wr);

         wr.Write("var oth = other as {0}", DtCtorName(ctor, dt.TypeArgs));

         wr.WriteLine(";");

-        Indent(ind + IndentAmount);

+        Indent(ind + IndentAmount, wr);

         wr.Write("return oth != null");

         i = 0;

         foreach (Formal arg in ctor.Formals) {

@@ -455,56 +448,56 @@ namespace Microsoft.Dafny {
           }

         }

         wr.WriteLine(";");

-        Indent(ind); wr.WriteLine("}");

+        Indent(ind, wr); wr.WriteLine("}");

 

         // GetHashCode method (Uses the djb2 algorithm)

-        Indent(ind); wr.WriteLine("public override int GetHashCode() {");

-        Indent(ind + IndentAmount); wr.WriteLine("ulong hash = 5381;");

-        Indent(ind + IndentAmount); wr.WriteLine("hash = ((hash << 5) + hash) + {0};", constructorIndex);

+        Indent(ind, wr); wr.WriteLine("public override int GetHashCode() {");

+        Indent(ind + IndentAmount, wr); wr.WriteLine("ulong hash = 5381;");

+        Indent(ind + IndentAmount, wr); wr.WriteLine("hash = ((hash << 5) + hash) + {0};", constructorIndex);

         i = 0;

         foreach (Formal arg in ctor.Formals) {

           if (!arg.IsGhost) {

             string nm = FormalName(arg, i);

-            Indent(ind + IndentAmount); wr.WriteLine("hash = ((hash << 5) + hash) + ((ulong)this.@{0}.GetHashCode());", nm);

+            Indent(ind + IndentAmount, wr); wr.WriteLine("hash = ((hash << 5) + hash) + ((ulong)this.@{0}.GetHashCode());", nm);

             i++;

           }

         }

-        Indent(ind + IndentAmount); wr.WriteLine("return (int) hash;");

-        Indent(ind); wr.WriteLine("}");

+        Indent(ind + IndentAmount, wr); wr.WriteLine("return (int) hash;");

+        Indent(ind, wr); wr.WriteLine("}");

 

         if (dt is IndDatatypeDecl) {

-          Indent(ind); wr.WriteLine("public override string ToString() {");

+          Indent(ind, wr); wr.WriteLine("public override string ToString() {");

           string nm;

           if (dt is TupleTypeDecl) {

             nm = "";

           } else {

             nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName;

           }

-          Indent(ind + IndentAmount); wr.WriteLine("string s = \"{0}\";", nm);

+          Indent(ind + IndentAmount, wr); wr.WriteLine("string s = \"{0}\";", nm);

           if (ctor.Formals.Count != 0) {

-            Indent(ind + IndentAmount); wr.WriteLine("s += \"(\";");

+            Indent(ind + IndentAmount, wr); wr.WriteLine("s += \"(\";");

             i = 0;

             foreach (var arg in ctor.Formals) {

               if (!arg.IsGhost) {

                 if (i != 0) {

-                  Indent(ind + IndentAmount); wr.WriteLine("s += \", \";");

+                  Indent(ind + IndentAmount, wr); wr.WriteLine("s += \", \";");

                 }

-                Indent(ind + IndentAmount); wr.WriteLine("s += @{0}.ToString();", FormalName(arg, i));

+                Indent(ind + IndentAmount, wr); wr.WriteLine("s += @{0}.ToString();", FormalName(arg, i));

                 i++;

               }

             }

-            Indent(ind + IndentAmount); wr.WriteLine("s += \")\";");

+            Indent(ind + IndentAmount, wr); wr.WriteLine("s += \")\";");

           }

-          Indent(ind + IndentAmount); wr.WriteLine("return s;");

-          Indent(ind); wr.WriteLine("}");

+          Indent(ind + IndentAmount, wr); wr.WriteLine("return s;");

+          Indent(ind, wr); wr.WriteLine("}");

         }

 

-        Indent(indent);  wr.WriteLine("}");

+        Indent(indent, wr); wr.WriteLine("}");

       }

       constructorIndex++;

     }

 

-    void CompileDatatypeStruct(DatatypeDecl dt, int indent) {

+    void CompileDatatypeStruct(DatatypeDecl dt, int indent, TextWriter wr) {

       Contract.Requires(dt != null);

 

       // public struct Dt<T> : IDatatype{

@@ -548,46 +541,46 @@ namespace Microsoft.Dafny {
         DtT += DtT_TypeArgs;

       }

 

-      Indent(indent);

+      Indent(indent, wr);

       wr.WriteLine("public struct @{0} {{", DtT);

       int ind = indent + IndentAmount;

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("Base_{0} _d;", DtT);

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("public Base_{0} _D {{", DtT);

-      Indent(ind + IndentAmount);

+      Indent(ind + IndentAmount, wr);

       wr.WriteLine("get {");

-      Indent(ind + 2 * IndentAmount);

+      Indent(ind + 2 * IndentAmount, wr);

       wr.WriteLine("if (_d == null) {");

-      Indent(ind + 3 * IndentAmount);

+      Indent(ind + 3 * IndentAmount, wr);

       wr.WriteLine("_d = Default;");

       if (dt is CoDatatypeDecl) {

         string typeParams = dt.TypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeParameters(dt.TypeArgs));

-        Indent(ind + 2 * IndentAmount);

+        Indent(ind + 2 * IndentAmount, wr);

         wr.WriteLine("}} else if (_d is {0}__Lazy{1}) {{", dt.CompileName, typeParams);

-        Indent(ind + 3 * IndentAmount);

+        Indent(ind + 3 * IndentAmount, wr);

         wr.WriteLine("_d = (({0}__Lazy{1})_d).Get();", dt.CompileName, typeParams);

       }

-      Indent(ind + 2 * IndentAmount);  wr.WriteLine("}");

-      Indent(ind + 2 * IndentAmount);  wr.WriteLine("return _d;");

-      Indent(ind + IndentAmount);  wr.WriteLine("}");

-      Indent(ind);  wr.WriteLine("}");

+      Indent(ind + 2 * IndentAmount, wr); wr.WriteLine("}");

+      Indent(ind + 2 * IndentAmount, wr); wr.WriteLine("return _d;");

+      Indent(ind + IndentAmount, wr); wr.WriteLine("}");

+      Indent(ind, wr); wr.WriteLine("}");

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("public @{0}(Base_{1} d) {{ this._d = d; }}", dt.CompileName, DtT);

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("static Base_{0} theDefault;", DtT);

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("public static Base_{0} Default {{", DtT);

-      Indent(ind + IndentAmount);

+      Indent(ind + IndentAmount, wr);

       wr.WriteLine("get {");

-      Indent(ind + 2 * IndentAmount);

+      Indent(ind + 2 * IndentAmount, wr);

       wr.WriteLine("if (theDefault == null) {");

-      Indent(ind + 3 * IndentAmount);

+      Indent(ind + 3 * IndentAmount, wr);

       wr.Write("theDefault = ");

 

       DatatypeCtor defaultCtor;

@@ -601,55 +594,55 @@ namespace Microsoft.Dafny {
       string sep = "";

       foreach (Formal f in defaultCtor.Formals) {

         if (!f.IsGhost) {

-          wr.Write("{0}{1}", sep, DefaultValue(f.Type));

+          wr.Write("{0}{1}", sep, DefaultValue(f.Type, wr));

           sep = ", ";

         }

       }

       wr.Write(")");

 

       wr.WriteLine(";");

-      Indent(ind + 2 * IndentAmount);

+      Indent(ind + 2 * IndentAmount, wr);

       wr.WriteLine("}");

-      Indent(ind + 2 * IndentAmount);

+      Indent(ind + 2 * IndentAmount, wr);

       wr.WriteLine("return theDefault;");

-      Indent(ind + IndentAmount); wr.WriteLine("}");

+      Indent(ind + IndentAmount, wr); wr.WriteLine("}");

 

-      Indent(ind);  wr.WriteLine("}");

+      Indent(ind, wr); wr.WriteLine("}");

 

-      Indent(ind);  wr.WriteLine("public override bool Equals(object other) {");

-      Indent(ind + IndentAmount);

+      Indent(ind, wr); wr.WriteLine("public override bool Equals(object other) {");

+      Indent(ind + IndentAmount, wr);

       wr.WriteLine("return other is @{0} && _D.Equals(((@{0})other)._D);", DtT);

-      Indent(ind);  wr.WriteLine("}");

+      Indent(ind, wr); wr.WriteLine("}");

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("public override int GetHashCode() { return _D.GetHashCode(); }");

       if (dt is IndDatatypeDecl) {

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public override string ToString() { return _D.ToString(); }");

       }

 

       // query properties

       foreach (var ctor in dt.Ctors) {

         //   public bool is_Ctor0 { get { return _D is Dt_Ctor0; } }

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public bool is_{0} {{ get {{ return _D is {1}_{0}{2}; }} }}", ctor.CompileName, dt.CompileName, DtT_TypeArgs);

       }

       if (dt.HasFinitePossibleValues) {

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public static System.Collections.Generic.IEnumerable<@{0}> AllSingletonConstructors {{", DtT);

-        Indent(ind + IndentAmount);

+        Indent(ind + IndentAmount, wr);

         wr.WriteLine("get {");

         foreach (var ctr in dt.Ctors) {

           if (ctr.Formals.Count == 0) {

-            Indent(ind + IndentAmount + IndentAmount);

+            Indent(ind + IndentAmount + IndentAmount, wr);

             wr.WriteLine("yield return new @{0}(new {2}_{1}());", DtT, ctr.CompileName, dt.CompileName);

           }

         }

-        Indent(ind + IndentAmount + IndentAmount);

+        Indent(ind + IndentAmount + IndentAmount, wr);

         wr.WriteLine("yield break;");

-        Indent(ind + IndentAmount);

+        Indent(ind + IndentAmount, wr);

         wr.WriteLine("}");

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("}");

       }

 

@@ -658,17 +651,17 @@ namespace Microsoft.Dafny {
         foreach (var arg in ctor.Formals) {

           if (!arg.IsGhost && arg.HasName) {

             //   public T0 @Dtor0 { get { return ((DT_Ctor)_D).@Dtor0; } }

-            Indent(ind);

-            wr.WriteLine("public {0} dtor_{1} {{ get {{ return (({2}_{3}{4})_D).@{1}; }} }}", TypeName(arg.Type), arg.CompileName, dt.CompileName, ctor.CompileName, DtT_TypeArgs);

+            Indent(ind, wr);

+            wr.WriteLine("public {0} dtor_{1} {{ get {{ return (({2}_{3}{4})_D).@{1}; }} }}", TypeName(arg.Type, wr), arg.CompileName, dt.CompileName, ctor.CompileName, DtT_TypeArgs);

           }

         }

       }

 

-      Indent(indent);

+      Indent(indent, wr);

       wr.WriteLine("}");

     }

 

-    int WriteFormals(string sep, List<Formal/*!*/>/*!*/ formals)

+    int WriteFormals(string sep, List<Formal/*!*/>/*!*/ formals, TextWriter wr)

     {

       Contract.Requires(sep != null);

       Contract.Requires(cce.NonNullElements(formals));

@@ -676,7 +669,7 @@ namespace Microsoft.Dafny {
       foreach (Formal arg in formals) {

         if (!arg.IsGhost) {

           string name = FormalName(arg, i);

-          wr.Write("{0}{1}{2} @{3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type), name);

+          wr.Write("{0}{1}{2} @{3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type, wr), name);

           sep = ", ";

           i++;

         }

@@ -732,13 +725,13 @@ namespace Microsoft.Dafny {
       return s;

     }

 

-    string DtCtorName(DatatypeCtor ctor, List<Type> typeArgs) {

+    string DtCtorName(DatatypeCtor ctor, List<Type> typeArgs, TextWriter wr) {

       Contract.Requires(ctor != null);

       Contract.Ensures(Contract.Result<string>() != null);

 

       var s = DtCtorName(ctor);

       if (typeArgs != null && typeArgs.Count != 0) {

-        s += "<" + TypeNames(typeArgs) + ">";

+        s += "<" + TypeNames(typeArgs, wr) + ">";

       }

       return s;

     }

@@ -776,7 +769,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void CompileClassMembers(ClassDecl c, bool forCompanionClass, int indent) {

+    void CompileClassMembers(ClassDecl c, bool forCompanionClass, int indent, TextWriter wr) {

       Contract.Requires(c != null);

       Contract.Requires(!forCompanionClass || c is TraitDecl);

       Contract.Requires(0 <= indent);

@@ -785,9 +778,9 @@ namespace Microsoft.Dafny {
         if (member is Field) {

           var f = (Field)member;

           // every field is inherited

-          Indent(indent);

-          wr.WriteLine("public {0} @_{1};", TypeName(f.Type), f.CompileName);

-          wr.Write("public {0} @{1}", TypeName(f.Type), f.CompileName);

+          Indent(indent, wr);

+          wr.WriteLine("public {0} @_{1};", TypeName(f.Type, wr), f.CompileName);

+          wr.Write("public {0} @{1}", TypeName(f.Type, wr), f.CompileName);

           wr.WriteLine(" {");

           wr.WriteLine(" get { ");

           wr.Write("return this.@_{0};", f.CompileName);

@@ -799,11 +792,11 @@ namespace Microsoft.Dafny {
         } else if (member is Function) {

           var f = (Function)member;

           Contract.Assert(f.Body != null);

-          CompileFunction(indent, f);

+          CompileFunction(indent, f, wr);

         } else if (member is Method) {

           var method = (Method)member;

           Contract.Assert(method.Body != null);

-          CompileMethod(c, indent, method);

+          CompileMethod(c, indent, method, wr);

         } else {

           Contract.Assert(false);  // unexpected member

         }

@@ -814,12 +807,12 @@ namespace Microsoft.Dafny {
           if (f.IsGhost || forCompanionClass) {

             // emit nothing

           } else if (c is TraitDecl) {

-            Indent(indent);

-            wr.Write("{0} @{1}", TypeName(f.Type), f.CompileName);

+            Indent(indent, wr);

+            wr.Write("{0} @{1}", TypeName(f.Type, wr), f.CompileName);

             wr.WriteLine(" { get; set; }");

           } else {

-            Indent(indent);

-            wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));

+            Indent(indent, wr);

+            wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type, wr), f.CompileName, DefaultValue(f.Type, wr));

           }

         } else if (member is Function) {

           var f = (Function)member;

@@ -828,29 +821,29 @@ namespace Microsoft.Dafny {
             if (forCompanionClass || Attributes.Contains(f.Attributes, "axiom")) {

               // suppress error message (in the case of "forCompanionClass", the non-forCompanionClass call will produce the error message)

             } else {

-              Error("Function {0} has no body", f.FullName);

+              Error("Function {0} has no body", wr, f.FullName);

             }

           } else if (f.IsGhost) {

             // nothing to compile, but we do check for assumes

             if (f.Body == null) {

               Contract.Assert(c is TraitDecl && !f.IsStatic);

             } else {

-              var v = new CheckHasNoAssumes_Visitor(this);

+              var v = new CheckHasNoAssumes_Visitor(this, wr);

               v.Visit(f.Body);

             }

           } else if (c is TraitDecl && !forCompanionClass) {

             // include it, unless it's static

             if (!f.IsStatic) {

-              Indent(indent);

-              wr.Write("{0} @{1}", TypeName(f.ResultType), f.CompileName);

+              Indent(indent, wr);

+              wr.Write("{0} @{1}", TypeName(f.ResultType, wr), f.CompileName);

               wr.Write("(");

-              WriteFormals("", f.Formals);

+              WriteFormals("", f.Formals, wr);

               wr.WriteLine(");");

             }

           } else if (forCompanionClass && !f.IsStatic) {

             // companion classes only has static members

           } else {

-            CompileFunction(indent, f);

+            CompileFunction(indent, f, wr);

           }

         } else if (member is Method) {

           var m = (Method)member;

@@ -859,30 +852,30 @@ namespace Microsoft.Dafny {
             if (forCompanionClass || Attributes.Contains(m.Attributes, "axiom")) {

               // suppress error message (in the case of "forCompanionClass", the non-forCompanionClass call will produce the error message)

             } else {

-              Error("Method {0} has no body", m.FullName);

+              Error("Method {0} has no body", wr, m.FullName);

             }

           } else if (m.IsGhost) {

             // nothing to compile, but we do check for assumes

             if (m.Body == null) {

               Contract.Assert(c is TraitDecl && !m.IsStatic);

             } else {

-              var v = new CheckHasNoAssumes_Visitor(this);

+              var v = new CheckHasNoAssumes_Visitor(this, wr);

               v.Visit(m.Body);

             }

           } else if (c is TraitDecl && !forCompanionClass) {

             // include it, unless it's static

             if (!m.IsStatic) {

-              Indent(indent);

+              Indent(indent, wr);

               wr.Write("void @{0}", m.CompileName);

               wr.Write("(");

-              int nIns = WriteFormals("", m.Ins);

-              WriteFormals(nIns == 0 ? "" : ", ", m.Outs);

+              int nIns = WriteFormals("", m.Ins, wr);

+              WriteFormals(nIns == 0 ? "" : ", ", m.Outs, wr);

               wr.WriteLine(");");

             }

           } else if (forCompanionClass && !m.IsStatic) {

             // companion classes only has static members

           } else {

-            CompileMethod(c, indent, m);

+            CompileMethod(c, indent, m, wr);

           }

         } else {

           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member

@@ -890,59 +883,59 @@ namespace Microsoft.Dafny {
       }

     }

 

-    private void CompileFunction(int indent, Function f) {

-      Indent(indent);

-      wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.CompileName);

+    private void CompileFunction(int indent, Function f, TextWriter wr) {

+      Indent(indent, wr);

+      wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType, wr), f.CompileName);

       if (f.TypeArgs.Count != 0) {

         wr.Write("<{0}>", TypeParameters(f.TypeArgs));

       }

       wr.Write("(");

-      WriteFormals("", f.Formals);

+      WriteFormals("", f.Formals, wr);

       wr.WriteLine(") {");

-      CompileReturnBody(f.Body, indent + IndentAmount);

-      Indent(indent); wr.WriteLine("}");

+      CompileReturnBody(f.Body, indent + IndentAmount, wr);

+      Indent(indent, wr); wr.WriteLine("}");

     }

 

-    private void CompileMethod(ClassDecl c, int indent, Method m) {

-      Indent(indent);

+    private void CompileMethod(ClassDecl c, int indent, Method m, TextWriter wr) {

+      Indent(indent, wr);

       wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.CompileName);

       if (m.TypeArgs.Count != 0) {

         wr.Write("<{0}>", TypeParameters(m.TypeArgs));

       }

       wr.Write("(");

-      int nIns = WriteFormals("", m.Ins);

-      WriteFormals(nIns == 0 ? "" : ", ", m.Outs);

+      int nIns = WriteFormals("", m.Ins, wr);

+      WriteFormals(nIns == 0 ? "" : ", ", m.Outs, wr);

       wr.WriteLine(")");

-      Indent(indent); wr.WriteLine("{");

+      Indent(indent, wr); wr.WriteLine("{");

       foreach (Formal p in m.Outs) {

         if (!p.IsGhost) {

-          Indent(indent + IndentAmount);

-          wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type));

+          Indent(indent + IndentAmount, wr);

+          wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type, wr));

         }

       }

       if (m.Body == null) {

-        Error("Method {0} has no body", m.FullName);

+        Error("Method {0} has no body", wr, m.FullName);

       } else {

         if (m.IsTailRecursive) {

-          Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");

+          Indent(indent, wr); wr.WriteLine("TAIL_CALL_START: ;");

           if (!m.IsStatic) {

-            Indent(indent + IndentAmount); wr.WriteLine("var _this = this;");

+            Indent(indent + IndentAmount, wr); wr.WriteLine("var _this = this;");

           }

         }

         Contract.Assert(enclosingMethod == null);

         enclosingMethod = m;

-        TrStmtList(m.Body.Body, indent);

+        TrStmtList(m.Body.Body, indent, wr);

         Contract.Assert(enclosingMethod == m);

         enclosingMethod = null;

       }

-      Indent(indent); wr.WriteLine("}");

+      Indent(indent, wr); wr.WriteLine("}");

 

       // allow the Main method to be an instance method

       if (!m.IsStatic && IsMain(m)) {

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("public static void Main(string[] args) {");

         Contract.Assert(m.EnclosingClass == c);

-        Indent(indent + IndentAmount);

+        Indent(indent + IndentAmount, wr);

         wr.Write("@{0} b = new @{0}", c.CompileName);

         if (c.TypeArgs.Count != 0) {

           // instantiate every parameter, it doesn't particularly matter how

@@ -955,12 +948,12 @@ namespace Microsoft.Dafny {
           wr.Write(">");

         }

         wr.WriteLine("();");

-        Indent(indent + IndentAmount); wr.WriteLine("b.@Main();");

-        Indent(indent); wr.WriteLine("}");

+        Indent(indent + IndentAmount, wr); wr.WriteLine("b.@Main();");

+        Indent(indent, wr); wr.WriteLine("}");

       }

     }

 

-    void TrCasePatternOpt(CasePattern pat, Expression rhs, string rhs_string, int indent) {

+    void TrCasePatternOpt(CasePattern pat, Expression rhs, string rhs_string, int indent, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(pat != null);

       Contract.Requires(pat.Var != null || rhs != null);

       if (pat.Var != null) {

@@ -970,10 +963,10 @@ namespace Microsoft.Dafny {
         // var x := G;

         var bv = pat.Var;

         if (!bv.IsGhost) {

-          Indent(indent);

-          wr.Write("{0} {1} = ", TypeName(bv.Type), "@" + bv.CompileName);

+          Indent(indent, wr);

+          wr.Write("{0} {1} = ", TypeName(bv.Type, wr), "@" + bv.CompileName);

           if (rhs != null) {

-            TrExpr(rhs);

+            TrExpr(rhs, wr, inLetExprBody);

           } else {

             wr.Write(rhs_string);

           }

@@ -992,9 +985,9 @@ namespace Microsoft.Dafny {
 

         // Create the temporary variable to hold G

         var tmp_name = idGenerator.FreshId("_let_tmp_rhs");

-        Indent(indent);

-        wr.Write("{0} {1} = ", TypeName(rhs.Type), tmp_name);

-        TrExpr(rhs);

+        Indent(indent, wr);

+        wr.Write("{0} {1} = ", TypeName(rhs.Type, wr), tmp_name);

+        TrExpr(rhs, wr, inLetExprBody);

         wr.WriteLine(";");

 

         var k = 0;  // number of non-ghost formals processed

@@ -1005,21 +998,21 @@ namespace Microsoft.Dafny {
             // nothing to compile, but do a sanity check

             Contract.Assert(!Contract.Exists(arg.Vars, bv => !bv.IsGhost));

           } else {            

-            TrCasePatternOpt(arg, null, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs), tmp_name, FormalName(formal, k)), indent);

+            TrCasePatternOpt(arg, null, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs, wr), tmp_name, FormalName(formal, k)), indent, wr, inLetExprBody);

             k++;

           }

         }

       }

     }

 

-    void ReturnExpr(Expression expr, int indent) {

-      Indent(indent);

+    void ReturnExpr(Expression expr, int indent, TextWriter wr, bool inLetExprBody) {

+      Indent(indent, wr);

       wr.Write("return ");

-      TrExpr(expr);

+      TrExpr(expr, wr, inLetExprBody);

       wr.WriteLine(";");

     }

 

-    void TrExprOpt(Expression expr, int indent) {

+    void TrExprOpt(Expression expr, int indent, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(expr != null);

       if (expr is LetExpr) {

         var e = (LetExpr)expr;

@@ -1027,25 +1020,25 @@ namespace Microsoft.Dafny {
           for (int i = 0; i < e.LHSs.Count; i++) {

             var lhs = e.LHSs[i];

             if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) {

-              TrCasePatternOpt(lhs, e.RHSs[i], null, indent);

+              TrCasePatternOpt(lhs, e.RHSs[i], null, indent, wr, inLetExprBody);

             }            

           }

-          TrExprOpt(e.Body, indent);

+          TrExprOpt(e.Body, indent, wr, inLetExprBody);

         } else {

           // We haven't optimized the other cases, so fallback to normal compilation

-          ReturnExpr(e, indent);

+          ReturnExpr(e, indent, wr, inLetExprBody);

         }

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("if (");

-        TrExpr(e.Test);

+        TrExpr(e.Test, wr, inLetExprBody);

         wr.Write(") {\n");

-        TrExprOpt(e.Thn, indent + IndentAmount);

-        Indent(indent);

+        TrExprOpt(e.Thn, indent + IndentAmount, wr, inLetExprBody);

+        Indent(indent, wr);

         wr.WriteLine("} else {");

-        TrExprOpt(e.Els, indent + IndentAmount);

-        Indent(indent);

+        TrExprOpt(e.Els, indent + IndentAmount, wr, inLetExprBody);

+        Indent(indent, wr);

         wr.WriteLine("}");

       } else if (expr is MatchExpr) {

         var e = (MatchExpr)expr;   

@@ -1060,9 +1053,9 @@ namespace Microsoft.Dafny {
         //     ...

         //   }

         string source = idGenerator.FreshId("_source");

-        Indent(indent);

-        wr.Write("{0} {1} = ", TypeName(e.Source.Type), source);

-        TrExpr(e.Source);

+        Indent(indent, wr);

+        wr.Write("{0} {1} = ", TypeName(e.Source.Type, wr), source);

+        TrExpr(e.Source, wr, inLetExprBody);

         wr.WriteLine(";");        

 

         if (e.Cases.Count == 0) {

@@ -1073,28 +1066,28 @@ namespace Microsoft.Dafny {
           var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand();

           foreach (MatchCaseExpr mc in e.Cases) {

             //Indent(indent);

-            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, indent);

-            TrExprOpt(mc.Body, indent + IndentAmount);

+            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, indent, wr);

+            TrExprOpt(mc.Body, indent + IndentAmount, wr, inLetExprBody);

             i++;

           }

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("}");

         }        

       }  else if (expr is StmtExpr) {

         var e = (StmtExpr)expr;

-        TrExprOpt(e.E, indent);

+        TrExprOpt(e.E, indent, wr, inLetExprBody);

       } else {

         // We haven't optimized any other cases, so fallback to normal compilation

-        ReturnExpr(expr, indent);

+        ReturnExpr(expr, indent, wr, inLetExprBody);

       }

     }

 

-    void CompileReturnBody(Expression body, int indent) {

+    void CompileReturnBody(Expression body, int indent, TextWriter wr) {

       Contract.Requires(0 <= indent);

       body = body.Resolved;

       //Indent(indent);

       //wr.Write("return ");

-      TrExprOpt(body, indent);

+      TrExprOpt(body, indent, wr, false);

       //wr.WriteLine(";");

     }

 

@@ -1113,23 +1106,23 @@ namespace Microsoft.Dafny {
       return null;

     }

 

-    string TypeName_Companion(Type type) {

+    string TypeName_Companion(Type type, TextWriter wr) {

       Contract.Requires(type != null);

       var udt = type as UserDefinedType;

       if (udt != null && udt.ResolvedClass is TraitDecl) {

         string s = udt.FullCompanionCompileName;

         if (udt.TypeArgs.Count != 0) {

           if (udt.TypeArgs.Exists(argType => argType is ObjectType)) {

-            Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");

+            Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost", wr);

           }

-          s += "<" + TypeNames(udt.TypeArgs) + ">";

+          s += "<" + TypeNames(udt.TypeArgs, wr) + ">";

         }

         return s;

       } else {

-        return TypeName(type);

+        return TypeName(type, wr);

       }

     }

-    string TypeName(Type type)

+    string TypeName(Type type, TextWriter wr)

     {

       Contract.Requires(type != null);

       Contract.Ensures(Contract.Result<string>() != null);

@@ -1153,14 +1146,14 @@ namespace Microsoft.Dafny {
         if (nativeType != null) {

           return nativeType.Name;

         }

-        return TypeName(xType.AsNewtype.BaseType);

+        return TypeName(xType.AsNewtype.BaseType, wr);

       } else if (xType is ObjectType) {

         return "object";

       } else if (xType.IsArrayType) {

         ArrayClassDecl at = xType.AsArrayType;

         Contract.Assert(at != null);  // follows from type.IsArrayType

         Type elType = UserDefinedType.ArrayElementType(xType);

-        string name = TypeName(elType) + "[";

+        string name = TypeName(elType, wr) + "[";

         for (int i = 1; i < at.Dims; i++) {

           name += ",";

         }

@@ -1184,54 +1177,60 @@ namespace Microsoft.Dafny {
           }

           s = rc.FullCompileName;

         }

-        return TypeName_UDT(s, udt.TypeArgs);

+        return TypeName_UDT(s, udt.TypeArgs, wr);

       } else if (xType is SetType) {

         Type argType = ((SetType)xType).Arg;

         if (argType is ObjectType) {

-          Error("compilation of set<object> is not supported; consider introducing a ghost");

+          Error("compilation of set<object> is not supported; consider introducing a ghost", wr);

         }

-        return DafnySetClass + "<" + TypeName(argType) + ">";

+        return DafnySetClass + "<" + TypeName(argType, wr) + ">";

       } else if (xType is SeqType) {

         Type argType = ((SeqType)xType).Arg;

         if (argType is ObjectType) {

-          Error("compilation of seq<object> is not supported; consider introducing a ghost");

+          Error("compilation of seq<object> is not supported; consider introducing a ghost", wr);

         }

-        return DafnySeqClass + "<" + TypeName(argType) + ">";

+        return DafnySeqClass + "<" + TypeName(argType, wr) + ">";

       } else if (xType is MultiSetType) {

         Type argType = ((MultiSetType)xType).Arg;

         if (argType is ObjectType) {

-          Error("compilation of seq<object> is not supported; consider introducing a ghost");

+          Error("compilation of seq<object> is not supported; consider introducing a ghost", wr);

         }

-        return DafnyMultiSetClass + "<" + TypeName(argType) + ">";

+        return DafnyMultiSetClass + "<" + TypeName(argType, wr) + ">";

       } else if (xType is MapType) {

         Type domType = ((MapType)xType).Domain;

         Type ranType = ((MapType)xType).Range;

         if (domType is ObjectType || ranType is ObjectType) {

-          Error("compilation of map<object, _> or map<_, object> is not supported; consider introducing a ghost");

+          Error("compilation of map<object, _> or map<_, object> is not supported; consider introducing a ghost", wr);

         }

-        return DafnyMapClass + "<" + TypeName(domType) + "," + TypeName(ranType) + ">";

+        return DafnyMapClass + "<" + TypeName(domType, wr) + "," + TypeName(ranType, wr) + ">";

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

     }

 

-    string TypeName_UDT(string fullCompileName, List<Type> typeArgs) {

+    string TypeName_UDT(string fullCompileName, List<Type> typeArgs, TextWriter wr) {

       Contract.Requires(fullCompileName != null);

       Contract.Requires(typeArgs != null);

       string s = "@" + fullCompileName;

       if (typeArgs.Count != 0) {

         if (typeArgs.Exists(argType => argType is ObjectType)) {

-          Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");

+          Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost", wr);

         }

-        s += "<" + TypeNames(typeArgs) + ">";

+        s += "<" + TypeNames(typeArgs, wr) + ">";

       }

       return s;

     }

 

-    string/*!*/ TypeNames(List<Type/*!*/>/*!*/ types) {

+    string/*!*/ TypeNames(List<Type/*!*/>/*!*/ types, TextWriter wr) {

       Contract.Requires(cce.NonNullElements(types));

       Contract.Ensures(Contract.Result<string>() != null);

-      return Util.Comma(types, TypeName);

+      string res = "";

+      string c = "";

+      foreach (var t in types) {

+        res += c + TypeName(t, wr);

+        c = ",";

+      }

+      return res;

     }

 

     string/*!*/ TypeParameters(List<TypeParameter/*!*/>/*!*/ targs) {

@@ -1241,7 +1240,7 @@ namespace Microsoft.Dafny {
       return Util.Comma(targs, tp => "@" + tp.CompileName);

     }

 

-    string DefaultValue(Type type)

+    string DefaultValue(Type type, TextWriter wr)

     {

       Contract.Requires(type != null);

       Contract.Ensures(Contract.Result<string>() != null);

@@ -1264,9 +1263,9 @@ namespace Microsoft.Dafny {
         if (xType.AsNewtype.NativeType != null) {

           return "0";

         }

-        return DefaultValue(xType.AsNewtype.BaseType);

+        return DefaultValue(xType.AsNewtype.BaseType, wr);

       } else if (xType.IsRefType) {

-        return string.Format("({0})null", TypeName(xType));

+        return string.Format("({0})null", TypeName(xType, wr));

       } else if (xType.IsDatatype) {

         var udt = (UserDefinedType)xType;

         var s = "@" + udt.FullCompileName;

@@ -1287,7 +1286,7 @@ namespace Microsoft.Dafny {
           s = "@" + rc.FullCompileName;

         }

         if (udt.TypeArgs.Count != 0) {

-          s += "<" + TypeNames(udt.TypeArgs) + ">";

+          s += "<" + TypeNames(udt.TypeArgs, wr) + ">";

         }

         return string.Format("new {0}()", s);

       } else if (xType.IsTypeParameter) {

@@ -1295,18 +1294,18 @@ namespace Microsoft.Dafny {
         string s = "default(@" + udt.FullCompileName;

         if (udt.TypeArgs.Count != 0)

         {

-          s += "<" + TypeNames(udt.TypeArgs) + ">";

+          s += "<" + TypeNames(udt.TypeArgs, wr) + ">";

         }

         s += ")";

         return s;

       } else if (xType is SetType) {

-        return DafnySetClass + "<" + TypeName(((SetType)xType).Arg) + ">.Empty";

+        return DafnySetClass + "<" + TypeName(((SetType)xType).Arg, wr) + ">.Empty";

       } else if (xType is MultiSetType) {

-        return DafnyMultiSetClass + "<" + TypeName(((MultiSetType)xType).Arg) + ">.Empty";

+        return DafnyMultiSetClass + "<" + TypeName(((MultiSetType)xType).Arg, wr) + ">.Empty";

       } else if (xType is SeqType) {

-        return DafnySeqClass + "<" + TypeName(((SeqType)xType).Arg) + ">.Empty";

+        return DafnySeqClass + "<" + TypeName(((SeqType)xType).Arg, wr) + ">.Empty";

       } else if (xType is MapType) {

-        return TypeName(xType)+".Empty";

+        return TypeName(xType, wr) + ".Empty";

       } else if (xType is ArrowType) {

         return "null";

       } else {

@@ -1319,59 +1318,61 @@ namespace Microsoft.Dafny {
     public class CheckHasNoAssumes_Visitor : BottomUpVisitor

     {

       readonly Compiler compiler;

-      public CheckHasNoAssumes_Visitor(Compiler c) {

+      TextWriter wr;

+      public CheckHasNoAssumes_Visitor(Compiler c, TextWriter wr) {

         Contract.Requires(c != null);

         compiler = c;

+        this.wr = wr;

       }

       protected override void VisitOneStmt(Statement stmt) {

         if (stmt is AssumeStmt) {

-          compiler.Error("an assume statement cannot be compiled (line {0})", stmt.Tok.line);

+          compiler.Error("an assume statement cannot be compiled (line {0})", wr, stmt.Tok.line);

         } else if (stmt is AssignSuchThatStmt) {

           var s = (AssignSuchThatStmt)stmt;

           if (s.AssumeToken != null) {

-            compiler.Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);

+            compiler.Error("an assume statement cannot be compiled (line {0})", wr, s.AssumeToken.line);

           }

         } else if (stmt is ForallStmt) {

           var s = (ForallStmt)stmt;

           if (s.Body == null) {

-            compiler.Error("a forall statement without a body cannot be compiled (line {0})", stmt.Tok.line);

+            compiler.Error("a forall statement without a body cannot be compiled (line {0})", wr, stmt.Tok.line);

           }

         } else if (stmt is WhileStmt) {

           var s = (WhileStmt)stmt;

           if (s.Body == null) {

-            compiler.Error("a while statement without a body cannot be compiled (line {0})", stmt.Tok.line);

+            compiler.Error("a while statement without a body cannot be compiled (line {0})", wr, stmt.Tok.line);

           }

         }

       }

     }

 

-    void TrStmt(Statement stmt, int indent)

+    TextWriter TrStmt(Statement stmt, int indent)

     {

       Contract.Requires(stmt != null);

+      TextWriter wr = new StringWriter();

       if (stmt.IsGhost) {

-        var v = new CheckHasNoAssumes_Visitor(this);

+        var v = new CheckHasNoAssumes_Visitor(this, wr);

         v.Visit(stmt);

-        Indent(indent); wr.WriteLine("{ }");

-        return;

+        Indent(indent, wr); wr.WriteLine("{ }");

+        return wr;

       }

-

       if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

         foreach (var arg in s.Args) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.Write("System.Console.Write(");

-          TrExpr(arg);

+          TrExpr(arg, wr, false);

           wr.WriteLine(");");

         }

       } else if (stmt is BreakStmt) {

         var s = (BreakStmt)stmt;

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.Data.AssignUniqueId("after_", idGenerator));

       } else if (stmt is ProduceStmt) {

         var s = (ProduceStmt)stmt;

         if (s.hiddenUpdate != null)

-          TrStmt(s.hiddenUpdate, indent);

-        Indent(indent);

+          wr.Write(TrStmt(s.hiddenUpdate, indent).ToString());

+        Indent(indent, wr);

         if (s is YieldStmt) {

           wr.WriteLine("yield return null;");

         } else {

@@ -1381,7 +1382,7 @@ namespace Microsoft.Dafny {
         var s = (UpdateStmt)stmt;

         var resolved = s.ResolvedStatements;

         if (resolved.Count == 1) {

-          TrStmt(resolved[0], indent);

+          wr.Write(TrStmt(resolved[0], indent).ToString());

         } else {

           // multi-assignment

           Contract.Assert(s.Lhss.Count == resolved.Count);

@@ -1393,17 +1394,17 @@ namespace Microsoft.Dafny {
               var lhs = s.Lhss[i];

               var rhs = s.Rhss[i];

               if (!(rhs is HavocRhs)) {

-                lvalues.Add(CreateLvalue(lhs, indent));

+                lvalues.Add(CreateLvalue(lhs, indent, wr));

 

                 string target = idGenerator.FreshId("_rhs");

                 rhss.Add(target);

-                TrRhs("var " + target, null, rhs, indent);

+                TrRhs("var " + target, null, rhs, indent, wr);

               }

             }

           }

           Contract.Assert(lvalues.Count == rhss.Count);

           for (int i = 0; i < lvalues.Count; i++) {

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("{0} = {1};", lvalues[i], rhss[i]);

           }

         }

@@ -1411,32 +1412,32 @@ namespace Microsoft.Dafny {
       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

         Contract.Assert(!(s.Lhs is SeqSelectExpr) || ((SeqSelectExpr)s.Lhs).SelectOne);  // multi-element array assignments are not allowed

-        TrRhs(null, s.Lhs, s.Rhs, indent);

+        TrRhs(null, s.Lhs, s.Rhs, indent, wr);

 

       } else if (stmt is AssignSuchThatStmt) {

         var s = (AssignSuchThatStmt)stmt;

         if (s.AssumeToken != null) {

           // Note, a non-ghost AssignSuchThatStmt may contain an assume

-          Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);

+          Error("an assume statement cannot be compiled (line {0})", wr, s.AssumeToken.line);

         } else if (s.MissingBounds != null) {

           foreach (var bv in s.MissingBounds) {

-            Error("this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", bv.Name, s.Tok.line);

+            Error("this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", wr, bv.Name, s.Tok.line);

           }

         } else {

           Contract.Assert(s.Bounds != null);  // follows from s.MissingBounds == null

           TrAssignSuchThat(indent,

             s.Lhss.ConvertAll(lhs => ((IdentifierExpr)lhs.Resolved).Var),  // the resolver allows only IdentifierExpr left-hand sides

-            s.Expr, s.Bounds, s.Tok.line);

+            s.Expr, s.Bounds, s.Tok.line, wr, false);

         }

 

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

-        TrCallStmt(s, null, indent);

+        wr.Write(TrCallStmt(s, null, indent).ToString());

 

       } else if (stmt is BlockStmt) {

-        Indent(indent);  wr.WriteLine("{");

-        TrStmtList(((BlockStmt)stmt).Body, indent);

-        Indent(indent);  wr.WriteLine("}");

+        Indent(indent, wr); wr.WriteLine("{");

+        TrStmtList(((BlockStmt)stmt).Body, indent, wr);

+        Indent(indent, wr); wr.WriteLine("}");

 

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

@@ -1445,45 +1446,45 @@ namespace Microsoft.Dafny {
           if (s.Els == null) {

             // let's compile the "else" branch, since that involves no work

             // (still, let's leave a marker in the source code to indicate that this is what we did)

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("if (!false) { }");

           } else {

             // let's compile the "then" branch

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("if (true)");

-            TrStmt(s.Thn, indent);

+            wr.Write(TrStmt(s.Thn, indent).ToString());

           }

         } else {

-          Indent(indent);  wr.Write("if (");

-          TrExpr(s.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)s.Guard, "eg_d", new Translator(null)) : s.Guard);

+          Indent(indent, wr); wr.Write("if (");

+          TrExpr(s.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)s.Guard, "eg_d", new Translator(null)) : s.Guard, wr, false);

           wr.WriteLine(")");

 

           // We'd like to do "TrStmt(s.Thn, indent)", except we want the scope of any existential variables to come inside the block

-          Indent(indent); wr.WriteLine("{");

+          Indent(indent, wr); wr.WriteLine("{");

           if (s.IsExistentialGuard) {

-            IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)s.Guard);

+            IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)s.Guard, wr);

           }

-          TrStmtList(s.Thn.Body, indent);

-          Indent(indent); wr.WriteLine("}");

+          TrStmtList(s.Thn.Body, indent, wr);

+          Indent(indent, wr); wr.WriteLine("}");

 

           if (s.Els != null) {

-            Indent(indent);  wr.WriteLine("else");

-            TrStmt(s.Els, indent);

+            Indent(indent, wr); wr.WriteLine("else");

+            wr.Write(TrStmt(s.Els, indent).ToString());

           }

         }

 

       } else if (stmt is AlternativeStmt) {

         var s = (AlternativeStmt)stmt;

-        Indent(indent);

+        Indent(indent, wr);

         foreach (var alternative in s.Alternatives) {

           wr.Write("if (");

-          TrExpr(alternative.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)alternative.Guard, "eg_d", new Translator(null)) : alternative.Guard);

+          TrExpr(alternative.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)alternative.Guard, "eg_d", new Translator(null)) : alternative.Guard, wr, false);

           wr.WriteLine(") {");

           if (alternative.IsExistentialGuard) {

-            IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)alternative.Guard);

+            IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)alternative.Guard, wr);

           }

-          TrStmtList(alternative.Body, indent);

-          Indent(indent);

+          TrStmtList(alternative.Body, indent, wr);

+          Indent(indent, wr);

           wr.Write("} else ");

         }

         wr.WriteLine("{ /*unreachable alternative*/ }");

@@ -1491,38 +1492,38 @@ namespace Microsoft.Dafny {
       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

         if (s.Body == null) {

-          return;

+          return wr;

         }

         if (s.Guard == null) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("while (false) { }");

         } else {

-          Indent(indent);

+          Indent(indent, wr);

           wr.Write("while (");

-          TrExpr(s.Guard);

+          TrExpr(s.Guard, wr, false);

           wr.WriteLine(")");

-          TrStmt(s.Body, indent);

+          wr.Write(TrStmt(s.Body, indent).ToString());

         }

 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

         if (s.Alternatives.Count != 0) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("while (true) {");

           int ind = indent + IndentAmount;

           foreach (var alternative in s.Alternatives) {

           }

-          Indent(ind);

+          Indent(ind, wr);

           foreach (var alternative in s.Alternatives) {

             wr.Write("if (");

-            TrExpr(alternative.Guard);

+            TrExpr(alternative.Guard, wr, false);

             wr.WriteLine(") {");

-            TrStmtList(alternative.Body, ind);

-            Indent(ind);

+            TrStmtList(alternative.Body, ind, wr);

+            Indent(ind, wr);

             wr.Write("} else ");

           }

           wr.WriteLine("{ break; }");

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("}");

         }

 

@@ -1530,17 +1531,17 @@ namespace Microsoft.Dafny {
         var s = (ForallStmt)stmt;

         if (s.Kind != ForallStmt.ParBodyKind.Assign) {

           // Call and Proof have no side effects, so they can simply be optimized away.

-          return;

+          return wr;

         } else if (s.BoundVars.Count == 0) {

           // the bound variables just spell out a single point, so the forall statement is equivalent to one execution of the body

-          TrStmt(s.Body, indent);

-          return;

+          wr.Write(TrStmt(s.Body, indent).ToString());

+          return wr;

         }

         var s0 = (AssignStmt)s.S0;

         if (s0.Rhs is HavocRhs) {

           // The forall statement says to havoc a bunch of things.  This can be efficiently compiled

           // into doing nothing.

-          return;

+          return wr;

         }

         var rhs = ((ExprRhs)s0.Rhs).Expr;

 

@@ -1584,29 +1585,29 @@ namespace Microsoft.Dafny {
         if (s0.Lhs is MemberSelectExpr) {

           var lhs = (MemberSelectExpr)s0.Lhs;

           L = 2;

-          tupleTypeArgs = TypeName(lhs.Obj.Type);

+          tupleTypeArgs = TypeName(lhs.Obj.Type, wr);

         } else if (s0.Lhs is SeqSelectExpr) {

           var lhs = (SeqSelectExpr)s0.Lhs;

           L = 3;

           // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple

-          tupleTypeArgs = TypeName(lhs.Seq.Type) + ",int";

+          tupleTypeArgs = TypeName(lhs.Seq.Type, wr) + ",int";

         } else {

           var lhs = (MultiSelectExpr)s0.Lhs;

           L = 2 + lhs.Indices.Count;

           if (8 < L) {

-            Error("compiler currently does not support assignments to more-than-6-dimensional arrays in forall statements");

-            return;

+            Error("compiler currently does not support assignments to more-than-6-dimensional arrays in forall statements", wr);

+            return wr;

           }

-          tupleTypeArgs = TypeName(lhs.Array.Type);

+          tupleTypeArgs = TypeName(lhs.Array.Type, wr);

           for (int i = 0; i < lhs.Indices.Count; i++) {

             // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple

             tupleTypeArgs += ",int";

           }

         }

-        tupleTypeArgs += "," + TypeName(rhs.Type);

+        tupleTypeArgs += "," + TypeName(rhs.Type, wr);

 

         // declare and construct "ingredients"

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("var {0} = new System.Collections.Generic.List<System.Tuple<{1}>>();", ingredients, tupleTypeArgs);

 

         var n = s.BoundVars.Count;

@@ -1616,38 +1617,38 @@ namespace Microsoft.Dafny {
           var bound = s.Bounds[i];

           var bv = s.BoundVars[i];

           if (bound is ComprehensionExpr.BoolBoundedPool) {

-            Indent(ind);

+            Indent(ind, wr);

             wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);

           } else if (bound is ComprehensionExpr.CharBoundedPool) {

-            Indent(ind);

+            Indent(ind, wr);

             wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);

           } else if (bound is ComprehensionExpr.IntBoundedPool) {

             var b = (ComprehensionExpr.IntBoundedPool)bound;

-            Indent(ind);

+            Indent(ind, wr);

             if (AsNativeType(bv.Type) != null) {

               wr.Write("foreach (var @{0} in @{1}.IntegerRange(", bv.CompileName, bv.Type.AsNewtype.FullCompileName);

             } else {

               wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName);

             }

-            TrExpr(b.LowerBound);

+            TrExpr(b.LowerBound, wr, false);

             wr.Write(", ");

-            TrExpr(b.UpperBound);

+            TrExpr(b.UpperBound, wr, false);

             wr.Write(")) { ");

           } else if (bound is ComprehensionExpr.SetBoundedPool) {

             var b = (ComprehensionExpr.SetBoundedPool)bound;

-            Indent(ind);

+            Indent(ind, wr);

             wr.Write("foreach (var @{0} in (", bv.CompileName);

-            TrExpr(b.Set);

+            TrExpr(b.Set, wr, false);

             wr.Write(").Elements) { ");

           } else if (bound is ComprehensionExpr.SeqBoundedPool) {

             var b = (ComprehensionExpr.SeqBoundedPool)bound;

-            Indent(ind);

+            Indent(ind, wr);

             wr.Write("foreach (var @{0} in (", bv.CompileName);

-            TrExpr(b.Seq);

+            TrExpr(b.Seq, wr, false);

             wr.Write(").UniqueElements) { ");

           } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

             var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

-            wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));

+            wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type, wr));

           } else {

             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

           }

@@ -1657,55 +1658,55 @@ namespace Microsoft.Dafny {
         // if (range) {

         //   ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) ));

         // }

-        Indent(indent + n * IndentAmount);

+        Indent(indent + n * IndentAmount, wr);

         wr.Write("if (");

         foreach (var bv in s.BoundVars) {

           if (bv.Type.NormalizeExpand() is NatType) {

             wr.Write("0 <= {0} && ", bv.CompileName);

           }

         }

-        TrExpr(s.Range);

+        TrExpr(s.Range, wr, false);

         wr.WriteLine(") {");

 

         var indFinal = indent + (n + 1) * IndentAmount;

-        Indent(indFinal);

+        Indent(indFinal, wr);

         wr.Write("{0}.Add(new System.Tuple<{1}>(", ingredients, tupleTypeArgs);

         if (s0.Lhs is MemberSelectExpr) {

           var lhs = (MemberSelectExpr)s0.Lhs;

-          TrExpr(lhs.Obj);

+          TrExpr(lhs.Obj, wr, false);

         } else if (s0.Lhs is SeqSelectExpr) {

           var lhs = (SeqSelectExpr)s0.Lhs;

-          TrExpr(lhs.Seq);

+          TrExpr(lhs.Seq, wr, false);

           wr.Write(", (int)(");

-          TrExpr(lhs.E0);

+          TrExpr(lhs.E0, wr, false);

           wr.Write(")");

         } else {

           var lhs = (MultiSelectExpr)s0.Lhs;

-          TrExpr(lhs.Array);

+          TrExpr(lhs.Array, wr, false);

           for (int i = 0; i < lhs.Indices.Count; i++) {

             wr.Write(", (int)(");

-            TrExpr(lhs.Indices[i]);

+            TrExpr(lhs.Indices[i], wr, false);

             wr.Write(")");

           }

         }

         wr.Write(", ");

-        TrExpr(rhs);

+        TrExpr(rhs, wr, false);

         wr.WriteLine("));");

 

-        Indent(indent + n * IndentAmount);

+        Indent(indent + n * IndentAmount, wr);

         wr.WriteLine("}");

 

         for (int i = n; 0 <= --i; ) {

-          Indent(indent + i * IndentAmount);

+          Indent(indent + i * IndentAmount, wr);

           wr.WriteLine("}");

         }

 

         //   foreach (L-Tuple l in ingredients) {

         //     LHS[ l0, l1, l2, ..., l(L-2) ] = l(L-1);

         //   }

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("foreach (var {0} in {1}) {{", tup, ingredients);

-        Indent(indent + IndentAmount);

+        Indent(indent + IndentAmount, wr);

         if (s0.Lhs is MemberSelectExpr) {

           var lhs = (MemberSelectExpr)s0.Lhs;

           wr.WriteLine("{0}.Item1.@{1} = {0}.Item2;", tup, lhs.MemberName);

@@ -1722,7 +1723,7 @@ namespace Microsoft.Dafny {
           }

           wr.WriteLine("] = {0}.Item{1};", tup, L);

         }

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("}");

 

       } else if (stmt is MatchStmt) {

@@ -1739,54 +1740,56 @@ namespace Microsoft.Dafny {
         // }

         if (s.Cases.Count != 0) {

           string source = idGenerator.FreshId("_source");

-          Indent(indent);

-          wr.Write("{0} {1} = ", TypeName(cce.NonNull(s.Source.Type)), source);

-          TrExpr(s.Source);

+          Indent(indent, wr);

+          wr.Write("{0} {1} = ", TypeName(cce.NonNull(s.Source.Type), wr), source);

+          TrExpr(s.Source, wr, false);

           wr.WriteLine(";");

 

           int i = 0;

           var sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand();

           foreach (MatchCaseStmt mc in s.Cases) {

-            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent);

-            TrStmtList(mc.Body, indent);

+            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent, wr);

+            TrStmtList(mc.Body, indent, wr);

             i++;

           }

-          Indent(indent); wr.WriteLine("}");

+          Indent(indent, wr); wr.WriteLine("}");

         }

 

       } else if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

         foreach (var local in s.Locals) {

-          TrLocalVar(local, true, indent);

+          TrLocalVar(local, true, indent, wr);

         }

         if (s.Update != null) {

-          TrStmt(s.Update, indent);

+          wr.Write(TrStmt(s.Update, indent).ToString());

         }

 

       } else if (stmt is ModifyStmt) {

         var s = (ModifyStmt)stmt;

         if (s.Body != null) {

-          TrStmt(s.Body, indent);

+          wr.Write(TrStmt(s.Body, indent).ToString());

         }

 

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement

       }

+

+      return wr;

     }

 

-    private void IntroduceAndAssignBoundVars(int indent, ExistsExpr exists) {

+    private void IntroduceAndAssignBoundVars(int indent, ExistsExpr exists, TextWriter wr) {

       Contract.Requires(0 <= indent);

       Contract.Requires(exists != null);

       Contract.Assume(exists.Bounds != null);  // follows from successful resolution

       Contract.Assert(exists.Range == null);  // follows from invariant of class IfStmt

       foreach (var bv in exists.BoundVars) {

-        TrLocalVar(bv, false, indent);

+        TrLocalVar(bv, false, indent, wr);

       }

       var ivars = exists.BoundVars.ConvertAll(bv => (IVariable)bv);

-      TrAssignSuchThat(indent, ivars, exists.Term, exists.Bounds, exists.tok.line);

+      TrAssignSuchThat(indent, ivars, exists.Term, exists.Bounds, exists.tok.line, wr, false);

     }

 

-    private void TrAssignSuchThat(int indent, List<IVariable> lhss, Expression constraint, List<ComprehensionExpr.BoundedPool> bounds, int debuginfoLine) {

+    private void TrAssignSuchThat(int indent, List<IVariable> lhss, Expression constraint, List<ComprehensionExpr.BoundedPool> bounds, int debuginfoLine, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(0 <= indent);

       Contract.Requires(lhss != null);

       Contract.Requires(constraint != null);

@@ -1828,7 +1831,7 @@ namespace Microsoft.Dafny {
       int ind = indent;

       bool needIterLimit = lhss.Count != 1 && bounds.Exists(bnd => !bnd.IsFinite);

       if (needIterLimit) {

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("for (var {0} = new BigInteger(5); ; {0} *= 2) {{", iterLimit);

         ind += IndentAmount;

       }

@@ -1837,11 +1840,11 @@ namespace Microsoft.Dafny {
         var bound = bounds[i];

         var bv = lhss[i];

         if (needIterLimit) {

-          Indent(ind);

+          Indent(ind, wr);

           wr.WriteLine("var {0}_{1} = {0};", iterLimit, i);

         }

         var tmpVar = idGenerator.FreshId("_assign_such_that_");

-        Indent(ind);

+        Indent(ind, wr);

         if (bound is ComprehensionExpr.BoolBoundedPool) {

           wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllBooleans) {{ @{1} = {0};", tmpVar, bv.CompileName);

         } else if (bound is ComprehensionExpr.CharBoundedPool) {

@@ -1856,13 +1859,13 @@ namespace Microsoft.Dafny {
           if (b.LowerBound == null) {

             wr.Write("null");

           } else {

-            TrExpr(b.LowerBound);

+            TrExpr(b.LowerBound, wr, inLetExprBody);

           }

           wr.Write(", ");

           if (b.UpperBound == null) {

             wr.Write("null");

           } else {

-            TrExpr(b.UpperBound);

+            TrExpr(b.UpperBound, wr, inLetExprBody);

           }

           wr.WriteLine(")) {{ @{1} = {0};", tmpVar, bv.CompileName);

         } else if (bound is AssignSuchThatStmt.WiggleWaggleBound) {

@@ -1870,54 +1873,54 @@ namespace Microsoft.Dafny {
         } else if (bound is ComprehensionExpr.SetBoundedPool) {

           var b = (ComprehensionExpr.SetBoundedPool)bound;

           wr.Write("foreach (var {0} in (", tmpVar);

-          TrExpr(b.Set);

+          TrExpr(b.Set, wr, inLetExprBody);

           wr.WriteLine(").Elements) {{ @{0} = {1};", bv.CompileName, tmpVar);

         } else if (bound is ComprehensionExpr.SubSetBoundedPool) {

           var b = (ComprehensionExpr.SubSetBoundedPool)bound;

           wr.Write("foreach (var {0} in (", tmpVar);

-          TrExpr(b.UpperBound);

+          TrExpr(b.UpperBound, wr, inLetExprBody);

           wr.WriteLine(").AllSubsets) {{ @{0} = {1};", bv.CompileName, tmpVar);

         } else if (bound is ComprehensionExpr.MapBoundedPool) {

           var b = (ComprehensionExpr.MapBoundedPool)bound;

           wr.Write("foreach (var {0} in (", tmpVar);

-          TrExpr(b.Map);

+          TrExpr(b.Map, wr, inLetExprBody);

           wr.WriteLine(").Domain) {{ @{0} = {1};", bv.CompileName, tmpVar);

         } else if (bound is ComprehensionExpr.SeqBoundedPool) {

           var b = (ComprehensionExpr.SeqBoundedPool)bound;

           wr.Write("foreach (var {0} in (", tmpVar);

-          TrExpr(b.Seq);

+          TrExpr(b.Seq, wr, inLetExprBody);

           wr.WriteLine(").Elements) {{ @{0} = {1};", bv.CompileName, tmpVar);

         } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

           var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

-          wr.WriteLine("foreach (var {0} in {1}.AllSingletonConstructors) {{ @{2} = {0};", tmpVar, TypeName(bv.Type), bv.CompileName);

+          wr.WriteLine("foreach (var {0} in {1}.AllSingletonConstructors) {{ @{2} = {0};", tmpVar, TypeName(bv.Type, wr), bv.CompileName);

         } else {

           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

         }

         if (needIterLimit) {

-          Indent(ind + IndentAmount);

+          Indent(ind + IndentAmount, wr);

           wr.WriteLine("if ({0}_{1} == 0) {{ break; }}  {0}_{1}--;", iterLimit, i);

         }

       }

-      Indent(ind);

+      Indent(ind, wr);

       wr.Write("if (");

-      TrExpr(constraint);

+      TrExpr(constraint, wr, inLetExprBody);

       wr.WriteLine(") {");

-      Indent(ind + IndentAmount);

+      Indent(ind + IndentAmount, wr);

       wr.WriteLine("goto {0};", doneLabel);

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("}");

-      Indent(indent);

+      Indent(indent, wr);

       for (int i = 0; i < n; i++) {

         wr.Write(i == 0 ? "}" : " }");

       }

       wr.WriteLine(needIterLimit ? " }" : "");

-      Indent(indent);

+      Indent(indent, wr);

       wr.WriteLine("throw new System.Exception(\"assign-such-that search produced no value (line {0})\");", debuginfoLine);

-      Indent(indent);

+      Indent(indent, wr);

       wr.WriteLine("{0}: ;", doneLabel);

     }

 

-    string CreateLvalue(Expression lhs, int indent) {

+    string CreateLvalue(Expression lhs, int indent, TextWriter wr) {

       lhs = lhs.Resolved;

       if (lhs is IdentifierExpr) {

         var ll = (IdentifierExpr)lhs;

@@ -1925,9 +1928,9 @@ namespace Microsoft.Dafny {
       } else if (lhs is MemberSelectExpr) {

         var ll = (MemberSelectExpr)lhs;

         string obj = idGenerator.FreshId("_obj");

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("var {0} = ", obj);

-        TrExpr(ll.Obj);

+        TrExpr(ll.Obj, wr, false);

         wr.WriteLine(";");

         return string.Format("{0}.@{1}", obj, ll.Member.CompileName);

       } else if (lhs is SeqSelectExpr) {

@@ -1935,31 +1938,31 @@ namespace Microsoft.Dafny {
         var c = idGenerator.FreshNumericId("_arr+_index");

         string arr = "_arr" + c;

         string index = "_index" + c;

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("var {0} = ", arr);

-        TrExpr(ll.Seq);

+        TrExpr(ll.Seq, wr, false);

         wr.WriteLine(";");

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("var {0} = ", index);

-        TrExpr(ll.E0);

+        TrExpr(ll.E0, wr, false);

         wr.WriteLine(";");

         return string.Format("{0}[(int){1}]", arr, index);

       } else {

         var ll = (MultiSelectExpr)lhs;

         var c = idGenerator.FreshNumericId("_arr+_index");

         string arr = "_arr" + c;

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("var {0} = ", arr);

-        TrExpr(ll.Array);

+        TrExpr(ll.Array, wr, false);

         wr.WriteLine(";");

         string fullString = arr + "[";

         string sep = "";

         int i = 0;

         foreach (var idx in ll.Indices) {

           string index = "_index" + i + "_" + c;

-          Indent(indent);

+          Indent(indent, wr);

           wr.Write("var {0} = ", index);

-          TrExpr(idx);

+          TrExpr(idx, wr, false);

           wr.WriteLine(";");

           fullString += sep + "(int)" + index;

           sep = ", ";

@@ -1969,21 +1972,21 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void TrRhs(string target, Expression targetExpr, AssignmentRhs rhs, int indent) {

+    void TrRhs(string target, Expression targetExpr, AssignmentRhs rhs, int indent, TextWriter wr) {

       Contract.Requires((target == null) != (targetExpr == null));

       var tRhs = rhs as TypeRhs;

       if (tRhs != null && tRhs.InitCall != null) {

         string nw = idGenerator.FreshId("_nw");

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("var {0} = ", nw);

-        TrAssignmentRhs(rhs);  // in this case, this call will not require us to spill any let variables first

+        TrAssignmentRhs(rhs, wr);  // in this case, this call will not require us to spill any let variables first

         wr.WriteLine(";");

-        TrCallStmt(tRhs.InitCall, nw, indent);

-        Indent(indent);

+        wr.Write(TrCallStmt(tRhs.InitCall, nw, indent).ToString());

+        Indent(indent, wr);

         if (target != null) {

           wr.Write(target);

         } else {

-          TrExpr(targetExpr);

+          TrExpr(targetExpr, wr, false);

         }

         wr.WriteLine(" = {0};", nw);

       } else if (rhs is HavocRhs) {

@@ -1994,22 +1997,23 @@ namespace Microsoft.Dafny {
           foreach (Expression dim in tRhs.ArrayDimensions) {

           }

         }

-        Indent(indent);

+        Indent(indent, wr);

         if (target != null) {

           wr.Write(target);

         } else {

-          TrExpr(targetExpr);

+          TrExpr(targetExpr, wr, false);

         }

         wr.Write(" = ");

-        TrAssignmentRhs(rhs);

+        TrAssignmentRhs(rhs, wr);

         wr.WriteLine(";");

       }

     }

 

-    void TrCallStmt(CallStmt s, string receiverReplacement, int indent) {

+    TextWriter TrCallStmt(CallStmt s, string receiverReplacement, int indent) {

       Contract.Requires(s != null);

       Contract.Assert(s.Method != null);  // follows from the fact that stmt has been successfully resolved

 

+      StringWriter wr = new StringWriter();

       if (s.Method == enclosingMethod && enclosingMethod.IsTailRecursive) {

         // compile call as tail-recursive

 

@@ -2026,9 +2030,9 @@ namespace Microsoft.Dafny {
 

           string inTmp = idGenerator.FreshId("_in");

           inTmps.Add(inTmp);

-          Indent(indent);

+          Indent(indent, wr);

           wr.Write("var {0} = ", inTmp);

-          TrExpr(s.Receiver);

+          TrExpr(s.Receiver, wr, false);

           wr.WriteLine(";");

         }

         for (int i = 0; i < s.Method.Ins.Count; i++) {

@@ -2036,29 +2040,29 @@ namespace Microsoft.Dafny {
           if (!p.IsGhost) {

             string inTmp = idGenerator.FreshId("_in");

             inTmps.Add(inTmp);

-            Indent(indent);

+            Indent(indent, wr);

             wr.Write("var {0} = ", inTmp);

-            TrExpr(s.Args[i]);

+            TrExpr(s.Args[i], wr, false);

             wr.WriteLine(";");

           }

         }

         // Now, assign to the formals

         int n = 0;

         if (!s.Method.IsStatic) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("_this = {0};", inTmps[n]);

           n++;

         }

         foreach (var p in s.Method.Ins) {

           if (!p.IsGhost) {

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("{0} = {1};", p.CompileName, inTmps[n]);

             n++;

           }

         }

         Contract.Assert(n == inTmps.Count);

         // finally, the jump back to the head of the method

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("goto TAIL_CALL_START;");

 

       } else {

@@ -2069,7 +2073,7 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < s.Method.Outs.Count; i++) {

           Formal p = s.Method.Outs[i];

           if (!p.IsGhost) {

-            lvalues.Add(CreateLvalue(s.Lhs[i], indent));

+            lvalues.Add(CreateLvalue(s.Lhs[i], indent, wr));

           }

         }

         var outTmps = new List<string>();

@@ -2078,8 +2082,8 @@ namespace Microsoft.Dafny {
           if (!p.IsGhost) {

             string target = idGenerator.FreshId("_out");

             outTmps.Add(target);

-            Indent(indent);

-            wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type), target);

+            Indent(indent, wr);

+            wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type, wr), target);

           }

         }

         Contract.Assert(lvalues.Count == outTmps.Count);

@@ -2090,14 +2094,14 @@ namespace Microsoft.Dafny {
           }

         }

         if (receiverReplacement != null) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.Write("@" + receiverReplacement);

         } else if (s.Method.IsStatic) {

-          Indent(indent);

-          wr.Write(TypeName_Companion(s.Receiver.Type));

+          Indent(indent, wr);

+          wr.Write(TypeName_Companion(s.Receiver.Type, wr));

         } else {

-          Indent(indent);

-          TrParenExpr(s.Receiver);

+          Indent(indent, wr);

+          TrParenExpr(s.Receiver, wr, false);

         }

         wr.Write(".@{0}(", s.Method.CompileName);

 

@@ -2106,7 +2110,7 @@ namespace Microsoft.Dafny {
           Formal p = s.Method.Ins[i];

           if (!p.IsGhost) {

             wr.Write(sep);

-            TrExpr(s.Args[i]);

+            TrExpr(s.Args[i], wr, false);

             sep = ", ";

           }

         }

@@ -2119,44 +2123,45 @@ namespace Microsoft.Dafny {
 

         // assign to the actual LHSs

         for (int j = 0; j < lvalues.Count; j++) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("{0} = {1};", lvalues[j], outTmps[j]);

         }

       }

+      return wr;

     }

 

     /// <summary>

     /// Before calling TrAssignmentRhs(rhs), the caller must have spilled the let variables declared in "rhs".

     /// </summary>

-    void TrAssignmentRhs(AssignmentRhs rhs) {

+    void TrAssignmentRhs(AssignmentRhs rhs, TextWriter wr) {

       Contract.Requires(rhs != null);

       Contract.Requires(!(rhs is HavocRhs));

       if (rhs is ExprRhs) {

         ExprRhs e = (ExprRhs)rhs;

-        TrExpr(e.Expr);

+        TrExpr(e.Expr, wr, false);

 

       } else {

         TypeRhs tp = (TypeRhs)rhs;

         if (tp.ArrayDimensions == null) {

-          wr.Write("new {0}()", TypeName(tp.EType));

+          wr.Write("new {0}()", TypeName(tp.EType, wr));

         } else {

           if (tp.EType.IsIntegerType || tp.EType.IsTypeParameter) {

             // Because the default constructor for BigInteger does not generate a valid BigInteger, we have

             // to excplicitly initialize the elements of an integer array.  This is all done in a helper routine.

-            wr.Write("Dafny.Helpers.InitNewArray{0}<{1}>", tp.ArrayDimensions.Count, TypeName(tp.EType));

+            wr.Write("Dafny.Helpers.InitNewArray{0}<{1}>", tp.ArrayDimensions.Count, TypeName(tp.EType, wr));

             string prefix = "(";

             foreach (Expression dim in tp.ArrayDimensions) {

               wr.Write(prefix);

-              TrParenExpr(dim);

+              TrParenExpr(dim, wr, false);

               prefix = ", ";

             }

             wr.Write(")");

           } else {

-            wr.Write("new {0}", TypeName(tp.EType));

+            wr.Write("new {0}", TypeName(tp.EType, wr));

             string prefix = "[";

             foreach (Expression dim in tp.ArrayDimensions) {

               wr.Write("{0}(int)", prefix);

-              TrParenExpr(dim);

+              TrParenExpr(dim, wr, false);

               prefix = ", ";

             }

             wr.Write("]");

@@ -2165,34 +2170,43 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void TrStmtList(List<Statement/*!*/>/*!*/ stmts, int indent) {Contract.Requires(cce.NonNullElements(stmts));

+    void TrStmtList(List<Statement/*!*/>/*!*/ stmts, int indent, TextWriter writer) {Contract.Requires(cce.NonNullElements(stmts));

       foreach (Statement ss in stmts) {

-        TrStmt(ss, indent + IndentAmount);

+        copyInstrWriter.Clear();

+        TextWriter wr = TrStmt(ss, indent + IndentAmount);

+        // write out any copy instructions that copies the out param

+        // used in letexpr to a local

+        string copyInstr = copyInstrWriter.ToString();

+        if (copyInstr != "") {

+          Indent(indent + IndentAmount, writer);

+          writer.Write(copyInstrWriter.ToString());

+        }

+        writer.Write(wr.ToString());

         if (ss.Labels != null) {

-          Indent(indent);  // labels are not indented as much as the statements

-          wr.WriteLine("after_{0}: ;", ss.Labels.Data.AssignUniqueId("after_", idGenerator));

+          Indent(indent, writer);  // labels are not indented as much as the statements

+          writer.WriteLine("after_{0}: ;", ss.Labels.Data.AssignUniqueId("after_", idGenerator));

         }

       }

     }

 

-    void TrLocalVar(IVariable v, bool alwaysInitialize, int indent) {

+    void TrLocalVar(IVariable v, bool alwaysInitialize, int indent, TextWriter wr) {

       Contract.Requires(v != null);

       if (v.IsGhost) {

         // only emit non-ghosts (we get here only for local variables introduced implicitly by call statements)

         return;

       }

 

-      Indent(indent);

-      wr.Write("{0} @{1}", TypeName(v.Type), v.CompileName);

+      Indent(indent, wr);

+      wr.Write("{0} @{1}", TypeName(v.Type, wr), v.CompileName);

       if (alwaysInitialize) {

         // produce a default value

-        wr.WriteLine(" = {0};", DefaultValue(v.Type));

+        wr.WriteLine(" = {0};", DefaultValue(v.Type, wr));

       } else {

         wr.WriteLine(";");

       }

     }

 

-    void MatchCasePrelude(string source, UserDefinedType sourceType, DatatypeCtor ctor, List<BoundVar/*!*/>/*!*/ arguments, int caseIndex, int caseCount, int indent) {

+    void MatchCasePrelude(string source, UserDefinedType sourceType, DatatypeCtor ctor, List<BoundVar/*!*/>/*!*/ arguments, int caseIndex, int caseCount, int indent, TextWriter wr) {

       Contract.Requires(source != null);

       Contract.Requires(sourceType != null);

       Contract.Requires(ctor != null);

@@ -2201,7 +2215,7 @@ namespace Microsoft.Dafny {
       // if (source.is_Ctor0) {

       //   FormalType f0 = ((Dt_Ctor0)source._D).a0;

       //   ...

-      Indent(indent);

+      Indent(indent, wr);

       wr.Write("{0}if (", caseIndex == 0 ? "" : "} else ");

       if (caseIndex == caseCount - 1) {

         wr.Write("true");

@@ -2216,9 +2230,9 @@ namespace Microsoft.Dafny {
         if (!arg.IsGhost) {

           BoundVar bv = arguments[m];

           // FormalType f0 = ((Dt_Ctor0)source._D).a0;

-          Indent(indent + IndentAmount);

+          Indent(indent + IndentAmount, wr);

           wr.WriteLine("{0} @{1} = (({2}){3}._D).@{4};",

-            TypeName(bv.Type), bv.CompileName, DtCtorName(ctor, sourceType.TypeArgs), source, FormalName(arg, k));

+            TypeName(bv.Type, wr), bv.CompileName, DtCtorName(ctor, sourceType.TypeArgs, wr), source, FormalName(arg, k));

           k++;

         }

       }

@@ -2229,51 +2243,51 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// Before calling TrParenExpr(expr), the caller must have spilled the let variables declared in "expr".

     /// </summary>

-    void TrParenExpr(string prefix, Expression expr) {

+    void TrParenExpr(string prefix, Expression expr, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(prefix != null);

       Contract.Requires(expr != null);

       wr.Write(prefix);

-      TrParenExpr(expr);

+      TrParenExpr(expr, wr, inLetExprBody);

     }

 

     /// <summary>

     /// Before calling TrParenExpr(expr), the caller must have spilled the let variables declared in "expr".

     /// </summary>

-    void TrParenExpr(Expression expr) {

+    void TrParenExpr(Expression expr, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(expr != null);

       wr.Write("(");

-      TrExpr(expr);

+      TrExpr(expr, wr, inLetExprBody);

       wr.Write(")");

     }

 

     /// <summary>

     /// Before calling TrExprList(exprs), the caller must have spilled the let variables declared in expressions in "exprs".

     /// </summary>

-    void TrExprList(List<Expression/*!*/>/*!*/ exprs) {

+    void TrExprList(List<Expression/*!*/>/*!*/ exprs, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(cce.NonNullElements(exprs));

       wr.Write("(");

       string sep = "";

       foreach (Expression e in exprs) {

         wr.Write(sep);

-        TrExpr(e);

+        TrExpr(e, wr, inLetExprBody);

         sep = ", ";

       }

       wr.Write(")");

     }

-    void TrExprPairList(List<ExpressionPair/*!*/>/*!*/ exprs) {

+    void TrExprPairList(List<ExpressionPair/*!*/>/*!*/ exprs, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(cce.NonNullElements(exprs));

       wr.Write("(");

       string sep = "";

       foreach (ExpressionPair p in exprs) {

         wr.Write(sep);

         wr.Write("new Dafny.Pair<");

-        wr.Write(TypeName(p.A.Type));

+        wr.Write(TypeName(p.A.Type, wr));

         wr.Write(",");

-        wr.Write(TypeName(p.B.Type));

+        wr.Write(TypeName(p.B.Type, wr));

         wr.Write(">(");

-        TrExpr(p.A);

+        TrExpr(p.A, wr, inLetExprBody);

         wr.Write(",");

-        TrExpr(p.B);

+        TrExpr(p.B, wr, inLetExprBody);

         wr.Write(")");

         sep = ", ";

       }

@@ -2283,13 +2297,13 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// Before calling TrExpr(expr), the caller must have spilled the let variables declared in "expr".

     /// </summary>

-    void TrExpr(Expression expr)

+    void TrExpr(Expression expr, TextWriter wr, bool inLetExprBody)

     {

       Contract.Requires(expr != null);

       if (expr is LiteralExpr) {

         LiteralExpr e = (LiteralExpr)expr;

         if (e.Value == null) {

-          wr.Write("({0})null", TypeName(e.Type));

+          wr.Write("({0})null", TypeName(e.Type, wr));

         } else if (e.Value is bool) {

           wr.Write((bool)e.Value ? "true" : "false");

         } else if (e is CharLiteralExpr) {

@@ -2330,41 +2344,49 @@ namespace Microsoft.Dafny {
 

       } else if (expr is IdentifierExpr) {

         var e = (IdentifierExpr)expr;

-        wr.Write("@" + e.Var.CompileName);

-

+        if (e.Var is Formal && inLetExprBody && !((Formal)e.Var).InParam) {

+          // out param in letExpr body, need to copy it to a temp since

+          // letExpr body is translated to an anonymous function that doesn't

+          // allow out parameters

+          var name = string.Format("_pat_let_tv{0}", GetUniqueAstNumber(e));

+          wr.Write("@" + name);

+          copyInstrWriter.Append("var @" + name + "= @" + e.Var.CompileName + ";\n");

+        } else {

+          wr.Write("@" + e.Var.CompileName);

+        }

       } else if (expr is SetDisplayExpr) {

         var e = (SetDisplayExpr)expr;

         var elType = e.Type.AsSetType.Arg;

-        wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType));

-        TrExprList(e.Elements);

+        wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType, wr));

+        TrExprList(e.Elements, wr, inLetExprBody);

 

       } else if (expr is MultiSetDisplayExpr) {

         var e = (MultiSetDisplayExpr)expr;

         var elType = e.Type.AsMultiSetType.Arg;

-        wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType));

-        TrExprList(e.Elements);

+        wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType, wr));

+        TrExprList(e.Elements, wr, inLetExprBody);

 

       } else if (expr is SeqDisplayExpr) {

         var e = (SeqDisplayExpr)expr;

         var elType = e.Type.AsSeqType.Arg;

-        wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));

-        TrExprList(e.Elements);

+        wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType, wr));

+        TrExprList(e.Elements, wr, inLetExprBody);

 

       } else if (expr is MapDisplayExpr) {

         MapDisplayExpr e = (MapDisplayExpr)expr;

-        wr.Write("{0}.FromElements", TypeName(e.Type));

-        TrExprPairList(e.Elements);

+        wr.Write("{0}.FromElements", TypeName(e.Type, wr));

+        TrExprPairList(e.Elements, wr, inLetExprBody);

 

       } else if (expr is MemberSelectExpr) {

         MemberSelectExpr e = (MemberSelectExpr)expr;

         SpecialField sf = e.Member as SpecialField;

         if (sf != null) {

           wr.Write(sf.PreString);

-          TrParenExpr(e.Obj);

+          TrParenExpr(e.Obj, wr, inLetExprBody);

           wr.Write(".@{0}", sf.CompiledName);

           wr.Write(sf.PostString);

         } else {

-          TrParenExpr(e.Obj);

+          TrParenExpr(e.Obj, wr, inLetExprBody);

           wr.Write(".@{0}", e.Member.CompileName);

         }

 

@@ -2374,50 +2396,50 @@ namespace Microsoft.Dafny {
         if (e.Seq.Type.IsArrayType) {

           if (e.SelectOne) {

             Contract.Assert(e.E0 != null && e.E1 == null);

-            TrParenExpr(e.Seq);

+            TrParenExpr(e.Seq, wr, inLetExprBody);

             wr.Write("[(int)");

-            TrParenExpr(e.E0);

+            TrParenExpr(e.E0, wr, inLetExprBody);

             wr.Write("]");

           } else {

-            TrParenExpr("Dafny.Helpers.SeqFromArray", e.Seq);

+            TrParenExpr("Dafny.Helpers.SeqFromArray", e.Seq, wr, inLetExprBody);

             if (e.E1 != null) {

-              TrParenExpr(".Take", e.E1);

+              TrParenExpr(".Take", e.E1, wr, inLetExprBody);

             }

             if (e.E0 != null) {

-              TrParenExpr(".Drop", e.E0);

+              TrParenExpr(".Drop", e.E0, wr, inLetExprBody);

             }

           }

         } else if (e.SelectOne) {

           Contract.Assert(e.E0 != null && e.E1 == null);

-          TrParenExpr(e.Seq);

-          TrParenExpr(".Select", e.E0);

+          TrParenExpr(e.Seq, wr, inLetExprBody);

+          TrParenExpr(".Select", e.E0, wr, inLetExprBody);

         } else {

-          TrParenExpr(e.Seq);

+          TrParenExpr(e.Seq, wr, inLetExprBody);

           if (e.E1 != null) {

-            TrParenExpr(".Take", e.E1);

+            TrParenExpr(".Take", e.E1, wr, inLetExprBody);

           }

           if (e.E0 != null) {

-            TrParenExpr(".Drop", e.E0);

+            TrParenExpr(".Drop", e.E0, wr, inLetExprBody);

           }

         }

       } else if (expr is MultiSetFormingExpr) {

         var e = (MultiSetFormingExpr)expr;

-        wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(e.E.Type.AsCollectionType.Arg));

+        wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(e.E.Type.AsCollectionType.Arg, wr));

         var eeType = e.E.Type.NormalizeExpand();

         if (eeType is SeqType) {

-          TrParenExpr(".FromSeq", e.E);

+          TrParenExpr(".FromSeq", e.E, wr, inLetExprBody);

         } else if (eeType is SetType) {

-          TrParenExpr(".FromSet", e.E);

+          TrParenExpr(".FromSet", e.E, wr, inLetExprBody);

         } else {

           Contract.Assert(false); throw new cce.UnreachableException();

         }

       } else if (expr is MultiSelectExpr) {

         MultiSelectExpr e = (MultiSelectExpr)expr;

-        TrParenExpr(e.Array);

+        TrParenExpr(e.Array, wr, inLetExprBody);

         string prefix = "[";

         foreach (Expression idx in e.Indices) {

           wr.Write("{0}(int)", prefix);

-          TrParenExpr(idx);

+          TrParenExpr(idx, wr, inLetExprBody);

           prefix = ", ";

         }

         wr.Write("]");

@@ -2426,47 +2448,47 @@ namespace Microsoft.Dafny {
         SeqUpdateExpr e = (SeqUpdateExpr)expr;

         if (e.ResolvedUpdateExpr != null)

         {

-          TrExpr(e.ResolvedUpdateExpr);

+          TrExpr(e.ResolvedUpdateExpr, wr, inLetExprBody);

         }

         else

         {

-          TrParenExpr(e.Seq);

+          TrParenExpr(e.Seq, wr, inLetExprBody);

           wr.Write(".Update(");

-          TrExpr(e.Index);

+          TrExpr(e.Index, wr, inLetExprBody);

           wr.Write(", ");

-          TrExpr(e.Value);

+          TrExpr(e.Value, wr, inLetExprBody);

           wr.Write(")");

         }

 

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

-        CompileFunctionCallExpr(e, wr, TrExpr);

+        CompileFunctionCallExpr(e, wr, wr, inLetExprBody, TrExpr);

 

       } else if (expr is ApplyExpr) {

         var e = expr as ApplyExpr;

         wr.Write("Dafny.Helpers.Id<");

-        wr.Write(TypeName(e.Function.Type));

+        wr.Write(TypeName(e.Function.Type, wr));

         wr.Write(">(");

-        TrExpr(e.Function);

+        TrExpr(e.Function, wr, inLetExprBody);

         wr.Write(")");

-        TrExprList(e.Args);

+        TrExprList(e.Args, wr, inLetExprBody);

 

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved

-        var typeParams = dtv.InferredTypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeNames(dtv.InferredTypeArgs));

+        var typeParams = dtv.InferredTypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeNames(dtv.InferredTypeArgs, wr));

 

         wr.Write("new {0}{1}(", DtName(dtv.Ctor.EnclosingDatatype), typeParams);

         if (!dtv.IsCoCall) {

           // For an ordinary constructor (that is, one that does not guard any co-recursive calls), generate:

           //   new Dt_Cons<T>( args )

-          wr.Write("new {0}(", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs));

+          wr.Write("new {0}(", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs, wr));

           string sep = "";

           for (int i = 0; i < dtv.Arguments.Count; i++) {

             Formal formal = dtv.Ctor.Formals[i];

             if (!formal.IsGhost) {

               wr.Write(sep);

-              TrExpr(dtv.Arguments[i]);

+              TrExpr(dtv.Arguments[i], wr, inLetExprBody);

               sep = ", ";

             }

           }

@@ -2495,17 +2517,17 @@ namespace Microsoft.Dafny {
                 arg = varName;

 

                 wr.Write("var {0} = ", varName);

-                TrExpr(actual);

+                TrExpr(actual, wr, inLetExprBody);

                 wr.Write("; ");

               } else {

                 var sw = new StringWriter();

-                CompileFunctionCallExpr(fce, sw, (exp) => {

+                CompileFunctionCallExpr(fce, sw, wr, inLetExprBody, (exp, wrr, inLetExpr) => {

                   string varName = idGenerator.FreshId("_ac");

                   sw.Write(varName);

 

-                  wr.Write("var {0} = ", varName);

-                  TrExpr(exp);

-                  wr.Write("; ");

+                  wrr.Write("var {0} = ", varName);

+                  TrExpr(exp, wrr, inLetExpr);

+                  wrr.Write("; ");

 

                 });

                 arg = sw.ToString();

@@ -2517,7 +2539,7 @@ namespace Microsoft.Dafny {
 

           wr.Write("return () => { return ");

 

-          wr.Write("new {0}({1}", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs), args);

+          wr.Write("new {0}({1}", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs, wr), args);

           wr.Write("); }; })())");

         }

         wr.Write(")");

@@ -2530,11 +2552,11 @@ namespace Microsoft.Dafny {
         switch (e.Op) {

           case UnaryOpExpr.Opcode.Not:

             wr.Write("!");

-            TrParenExpr(e.E);

+            TrParenExpr(e.E, wr, inLetExprBody);

             break;

           case UnaryOpExpr.Opcode.Cardinality:

             wr.Write("new BigInteger(");

-            TrParenExpr(e.E);

+            TrParenExpr(e.E, wr, inLetExprBody);

             wr.Write(".Length)");

             break;

           default:

@@ -2552,7 +2574,7 @@ namespace Microsoft.Dafny {
           if (AsNativeType(e.E.Type) != null) {

             wr.Write("new BigInteger");

           }

-          TrParenExpr(e.E);

+          TrParenExpr(e.E, wr, inLetExprBody);

         };

         Action toIntCast = () => {

           Contract.Assert(toInt);

@@ -2568,7 +2590,7 @@ namespace Microsoft.Dafny {
         } else if (!fromInt && toInt) {

           // real -> int

           toIntCast();

-          TrParenExpr(e.E);

+          TrParenExpr(e.E, wr, inLetExprBody);

           wr.Write(".ToBigInteger()");

         } else if (AsNativeType(e.ToType) != null) {

           toIntCast();

@@ -2580,14 +2602,14 @@ namespace Microsoft.Dafny {
             wr.Write("(" + (BigInteger)lit.Value + AsNativeType(e.ToType).Suffix + ")");

           } else if ((u != null && u.Op == UnaryOpExpr.Opcode.Cardinality) || (m != null && m.MemberName == "Length" && m.Obj.Type.IsArrayType)) {

             // Optimize .Length to avoid intermediate BigInteger

-            TrParenExpr((u != null) ? u.E : m.Obj);

+            TrParenExpr((u != null) ? u.E : m.Obj, wr, inLetExprBody);

             if (AsNativeType(e.ToType).UpperBound <= new BigInteger(0x80000000U)) {

               wr.Write(".Length");

             } else {

               wr.Write(".LongLength");

             }

           } else {

-            TrParenExpr(e.E);

+            TrParenExpr(e.E, wr, inLetExprBody);

           }

         } else if (e.ToType.IsIntegerType && AsNativeType(e.E.Type) != null) {

           fromIntAsBigInteger();

@@ -2595,7 +2617,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(fromInt == toInt);

           Contract.Assert(AsNativeType(e.ToType) == null);

           Contract.Assert(AsNativeType(e.E.Type) == null);

-          TrParenExpr(e.E);

+          TrParenExpr(e.E, wr, inLetExprBody);

         }

 

       } else if (expr is BinaryExpr) {

@@ -2664,9 +2686,9 @@ namespace Microsoft.Dafny {
             if (expr.Type.IsIntegerType || (AsNativeType(expr.Type) != null && AsNativeType(expr.Type).LowerBound < BigInteger.Zero)) {

               string suffix = AsNativeType(expr.Type) != null ? ("_" + AsNativeType(expr.Type).Name) : "";

               wr.Write("Dafny.Helpers.EuclideanDivision" + suffix + "(");

-              TrParenExpr(e.E0);

+              TrParenExpr(e.E0, wr, inLetExprBody);

               wr.Write(", ");

-              TrExpr(e.E1);

+              TrExpr(e.E1, wr, inLetExprBody);

               wr.Write(")");

             } else {

               opString = "/";  // for reals

@@ -2676,9 +2698,9 @@ namespace Microsoft.Dafny {
             if (expr.Type.IsIntegerType || (AsNativeType(expr.Type) != null && AsNativeType(expr.Type).LowerBound < BigInteger.Zero)) {

               string suffix = AsNativeType(expr.Type) != null ? ("_" + AsNativeType(expr.Type).Name) : "";

               wr.Write("Dafny.Helpers.EuclideanModulus" + suffix + "(");

-              TrParenExpr(e.E0);

+              TrParenExpr(e.E0, wr, inLetExprBody);

               wr.Write(", ");

-              TrExpr(e.E1);

+              TrExpr(e.E1, wr, inLetExprBody);

               wr.Write(")");

             } else {

               opString = "%";  // for reals

@@ -2713,18 +2735,18 @@ namespace Microsoft.Dafny {
           case BinaryExpr.ResolvedOpcode.InSet:

           case BinaryExpr.ResolvedOpcode.InMultiSet:

           case BinaryExpr.ResolvedOpcode.InMap:

-            TrParenExpr(e.E1);

+            TrParenExpr(e.E1, wr, inLetExprBody);

             wr.Write(".Contains(");

-            TrExpr(e.E0);

+            TrExpr(e.E0, wr, inLetExprBody);

             wr.Write(")");

             break;

           case BinaryExpr.ResolvedOpcode.NotInSet:

           case BinaryExpr.ResolvedOpcode.NotInMultiSet:

           case BinaryExpr.ResolvedOpcode.NotInMap:

             wr.Write("!");

-            TrParenExpr(e.E1);

+            TrParenExpr(e.E1, wr, inLetExprBody);

             wr.Write(".Contains(");

-            TrExpr(e.E0);

+            TrExpr(e.E0, wr, inLetExprBody);

             wr.Write(")");

             break;

           case BinaryExpr.ResolvedOpcode.Union:

@@ -2744,16 +2766,16 @@ namespace Microsoft.Dafny {
           case BinaryExpr.ResolvedOpcode.Concat:

             callString = "Concat";  break;

           case BinaryExpr.ResolvedOpcode.InSeq:

-            TrParenExpr(e.E1);

+            TrParenExpr(e.E1, wr, inLetExprBody);

             wr.Write(".Contains(");

-            TrExpr(e.E0);

+            TrExpr(e.E0, wr, inLetExprBody);

             wr.Write(")");

             break;

           case BinaryExpr.ResolvedOpcode.NotInSeq:

             wr.Write("!");

-            TrParenExpr(e.E1);

+            TrParenExpr(e.E1, wr, inLetExprBody);

             wr.Write(".Contains(");

-            TrExpr(e.E0);

+            TrExpr(e.E0, wr, inLetExprBody);

             wr.Write(")");

             break;

 

@@ -2767,17 +2789,17 @@ namespace Microsoft.Dafny {
             wr.Write("(" + nativeType.Name + ")(");

           }

           wr.Write(preOpString);

-          TrParenExpr(e.E0);

+          TrParenExpr(e.E0, wr, inLetExprBody);

           wr.Write(" {0} ", opString);

-          TrParenExpr(e.E1);

+          TrParenExpr(e.E1, wr, inLetExprBody);

           if (needsCast) {

             wr.Write(")");

           }

         } else if (callString != null) {

           wr.Write(preOpString);

-          TrParenExpr(e.E0);

+          TrParenExpr(e.E0, wr, inLetExprBody);

           wr.Write(".@{0}(", callString);

-          TrExpr(e.E1);

+          TrExpr(e.E1, wr, inLetExprBody);

           wr.Write(")");

         }

 

@@ -2800,17 +2822,18 @@ namespace Microsoft.Dafny {
             if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) {

               var rhsName = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i);

               wr.Write("Dafny.Helpers.Let<");

-              wr.Write(TypeName(e.RHSs[i].Type) + "," + TypeName(e.Body.Type));

+              wr.Write(TypeName(e.RHSs[i].Type, wr) + "," + TypeName(e.Body.Type, wr));

               wr.Write(">(");

-              TrExpr(e.RHSs[i]);

+              TrExpr(e.RHSs[i], wr, inLetExprBody);

               wr.Write(", " + rhsName + " => ");

               neededCloseParens++;

-              var c = TrCasePattern(lhs, rhsName, e.Body.Type);

+              var c = TrCasePattern(lhs, rhsName, e.Body.Type, wr);

               Contract.Assert(c != 0);  // we already checked that there's at least one non-ghost

               neededCloseParens += c;

             }

           }

-          TrExpr(e.Body);

+          

+          TrExpr(e.Body, wr, true);

           for (int i = 0; i < neededCloseParens; i++) {

             wr.Write(")");

           }

@@ -2819,7 +2842,7 @@ namespace Microsoft.Dafny {
           //    ghost var x,y :| Constraint; E

           // is compiled just like E is, because the resolver has already checked that x,y (or other ghost variables, for that matter) don't

           // occur in E (moreover, the verifier has checked that values for x,y satisfying Constraint exist).

-          TrExpr(e.Body);

+          TrExpr(e.Body, wr, inLetExprBody);

         } else {

           // The Dafny "let" expression

           //    var x,y :| Constraint; E

@@ -2834,17 +2857,17 @@ namespace Microsoft.Dafny {
           Contract.Assert(e.RHSs.Count == 1);  // checked by resolution

           if (e.Constraint_MissingBounds != null) {

             foreach (var bv in e.Constraint_MissingBounds) {

-              Error("this let-such-that expression is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", bv.Name, e.tok.line);

+              Error("this let-such-that expression is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", wr, bv.Name, e.tok.line);

             }

           } else {

-            wr.Write("Dafny.Helpers.Let<int," + TypeName(e.Body.Type) + ">(0, _let_dummy_" + GetUniqueAstNumber(e) + " => {");

+            wr.Write("Dafny.Helpers.Let<int," + TypeName(e.Body.Type, wr) + ">(0, _let_dummy_" + GetUniqueAstNumber(e) + " => {");

             foreach (var bv in e.BoundVars) {

-              wr.Write("{0} @{1}", TypeName(bv.Type), bv.CompileName);

-              wr.WriteLine(" = {0};", DefaultValue(bv.Type));

+              wr.Write("{0} @{1}", TypeName(bv.Type, wr), bv.CompileName);

+              wr.WriteLine(" = {0};", DefaultValue(bv.Type, wr));

             }

-            TrAssignSuchThat(0, new List<IVariable>(e.BoundVars).ConvertAll(bv => (IVariable)bv), e.RHSs[0], e.Constraint_Bounds, e.tok.line);

+            TrAssignSuchThat(0, new List<IVariable>(e.BoundVars).ConvertAll(bv => (IVariable)bv), e.RHSs[0], e.Constraint_Bounds, e.tok.line, wr, inLetExprBody);

             wr.Write(" return ");

-            TrExpr(e.Body);

+            TrExpr(e.Body, wr, true);

             wr.Write("; })");

           }

         }

@@ -2864,7 +2887,7 @@ namespace Microsoft.Dafny {
         // }(src)

 

         string source = idGenerator.FreshId("_source");

-        wr.Write("new Dafny.Helpers.Function<{0}, {1}>(delegate ({0} {2}) {{ ", TypeName(e.Source.Type), TypeName(e.Type), source);

+        wr.Write("new Dafny.Helpers.Function<{0}, {1}>(delegate ({0} {2}) {{ ", TypeName(e.Source.Type, wr), TypeName(e.Type, wr), source);

 

         if (e.Cases.Count == 0) {

           // the verifier would have proved we never get here; still, we need some code that will compile

@@ -2873,9 +2896,9 @@ namespace Microsoft.Dafny {
           int i = 0;

           var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand();

           foreach (MatchCaseExpr mc in e.Cases) {

-            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, 0);

+            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, 0, wr);

             wr.Write("return ");

-            TrExpr(mc.Body);

+            TrExpr(mc.Body, wr, inLetExprBody);

             wr.Write("; ");

             i++;

           }

@@ -2883,7 +2906,7 @@ namespace Microsoft.Dafny {
         }

         // We end with applying the source expression to the delegate we just built

         wr.Write("})(");

-        TrExpr(e.Source);

+        TrExpr(e.Source, wr, inLetExprBody);

         wr.Write(")");

 

       } else if (expr is QuantifierExpr) {

@@ -2905,24 +2928,24 @@ namespace Microsoft.Dafny {
           } else if (bound is ComprehensionExpr.IntBoundedPool) {

             var b = (ComprehensionExpr.IntBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantInt(");

-            TrExpr(b.LowerBound);

+            TrExpr(b.LowerBound, wr, inLetExprBody);

             wr.Write(", ");

-            TrExpr(b.UpperBound);

+            TrExpr(b.UpperBound, wr, inLetExprBody);

             wr.Write(", ");

           } else if (bound is ComprehensionExpr.SetBoundedPool) {

             var b = (ComprehensionExpr.SetBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantSet(");

-            TrExpr(b.Set);

+            TrExpr(b.Set, wr, inLetExprBody);

             wr.Write(", ");

           } else if (bound is ComprehensionExpr.MapBoundedPool) {

             var b = (ComprehensionExpr.MapBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantMap(");

-            TrExpr(b.Map);

+            TrExpr(b.Map, wr, inLetExprBody);

             wr.Write(", ");

           } else if (bound is ComprehensionExpr.SeqBoundedPool) {

             var b = (ComprehensionExpr.SeqBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantSeq(");

-            TrExpr(b.Seq);

+            TrExpr(b.Seq, wr, inLetExprBody);

             wr.Write(", ");

           } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

             var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

@@ -2935,7 +2958,7 @@ namespace Microsoft.Dafny {
           wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");

           wr.Write("@{0} => ", bv.CompileName);

         }

-        TrExpr(e.LogicalBody(true));

+        TrExpr(e.LogicalBody(true), wr, inLetExprBody);

         for (int i = 0; i < n; i++) {

           wr.Write(")");

         }

@@ -2959,7 +2982,7 @@ namespace Microsoft.Dafny {
         //   return Dafny.Set<G>.FromCollection(_coll);

         // })()

         Contract.Assert(e.Bounds != null);  // the resolver would have insisted on finding bounds

-        var typeName = TypeName(e.Type.AsSetType.Arg);

+        var typeName = TypeName(e.Type.AsSetType.Arg, wr);

         wr.Write("((Dafny.Helpers.ComprehensionDelegate<{0}>)delegate() {{ ", typeName);

         wr.Write("var _coll = new System.Collections.Generic.List<{0}>(); ", typeName);

         var n = e.BoundVars.Count;

@@ -2978,36 +3001,36 @@ namespace Microsoft.Dafny {
             } else {

               wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName);

             }

-            TrExpr(b.LowerBound);

+            TrExpr(b.LowerBound, wr, inLetExprBody);

             wr.Write(", ");

-            TrExpr(b.UpperBound);

+            TrExpr(b.UpperBound, wr, inLetExprBody);

             wr.Write(")) { ");

           } else if (bound is ComprehensionExpr.SetBoundedPool) {

             var b = (ComprehensionExpr.SetBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

-            TrExpr(b.Set);

+            TrExpr(b.Set, wr, inLetExprBody);

             wr.Write(").Elements) { ");

           } else if (bound is ComprehensionExpr.MapBoundedPool) {

             var b = (ComprehensionExpr.MapBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

-            TrExpr(b.Map);

+            TrExpr(b.Map, wr, inLetExprBody);

             wr.Write(").Domain) { ");

           } else if (bound is ComprehensionExpr.SeqBoundedPool) {

             var b = (ComprehensionExpr.SeqBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

-            TrExpr(b.Seq);

+            TrExpr(b.Seq, wr, inLetExprBody);

             wr.Write(").Elements) { ");

           } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

             var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

-            wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));

+            wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type, wr));

           } else {

             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

           }

         }

         wr.Write("if (");

-        TrExpr(e.Range);

+        TrExpr(e.Range, wr, inLetExprBody);

         wr.Write(") { _coll.Add(");

-        TrExpr(e.Term);

+        TrExpr(e.Term, wr, inLetExprBody);

         wr.Write("); }");

         for (int i = 0; i < n; i++) {

           wr.Write("}");

@@ -3034,8 +3057,8 @@ namespace Microsoft.Dafny {
         //   return Dafny.Map<U, V>.FromElements(_coll);

         // })()

         Contract.Assert(e.Bounds != null);  // the resolver would have insisted on finding bounds

-        var domtypeName = TypeName(e.Type.AsMapType.Domain);

-        var rantypeName = TypeName(e.Type.AsMapType.Range);

+        var domtypeName = TypeName(e.Type.AsMapType.Domain, wr);

+        var rantypeName = TypeName(e.Type.AsMapType.Range, wr);

         wr.Write("((Dafny.Helpers.MapComprehensionDelegate<{0},{1}>)delegate() {{ ", domtypeName, rantypeName);

         wr.Write("var _coll = new System.Collections.Generic.List<Dafny.Pair<{0},{1}>>(); ", domtypeName, rantypeName);

         var n = e.BoundVars.Count;

@@ -3053,34 +3076,34 @@ namespace Microsoft.Dafny {
           } else {

             wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName);

           }

-          TrExpr(b.LowerBound);

+          TrExpr(b.LowerBound, wr, inLetExprBody);

           wr.Write(", ");

-          TrExpr(b.UpperBound);

+          TrExpr(b.UpperBound, wr, inLetExprBody);

           wr.Write(")) { ");

         } else if (bound is ComprehensionExpr.SetBoundedPool) {

           var b = (ComprehensionExpr.SetBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

-          TrExpr(b.Set);

+          TrExpr(b.Set, wr, inLetExprBody);

           wr.Write(").Elements) { ");

         } else if (bound is ComprehensionExpr.MapBoundedPool) {

           var b = (ComprehensionExpr.MapBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

-          TrExpr(b.Map);

+          TrExpr(b.Map, wr, inLetExprBody);

           wr.Write(").Domain) { ");

         } else if (bound is ComprehensionExpr.SeqBoundedPool) {

           var b = (ComprehensionExpr.SeqBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

-          TrExpr(b.Seq);

+          TrExpr(b.Seq, wr, inLetExprBody);

           wr.Write(").Elements) { ");

         } else {

           // TODO: handle ComprehensionExpr.SubSetBoundedPool

           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

         }

         wr.Write("if (");

-        TrExpr(e.Range);

+        TrExpr(e.Range, wr, inLetExprBody);

         wr.Write(") { ");

         wr.Write("_coll.Add(new Dafny.Pair<{0},{1}>(@{2},", domtypeName, rantypeName, bv.CompileName);

-        TrExpr(e.Term);

+        TrExpr(e.Term, wr, inLetExprBody);

         wr.Write(")); }");

         wr.Write("}");

         wr.Write("return Dafny.Map<{0},{1}>.FromCollection(_coll); ", domtypeName, rantypeName);

@@ -3109,46 +3132,46 @@ namespace Microsoft.Dafny {
 

         var su = new Translator.Substituter(null, sm, new Dictionary<TypeParameter, Type>(), null);

 

-        BetaRedex(bvars, fexprs, expr.Type, () => {

+        BetaRedex(bvars, fexprs, expr.Type, wr, inLetExprBody, () => {

           wr.Write("(");

           wr.Write(Util.Comma(e.BoundVars, bv => "@" + bv.CompileName));

           wr.Write(") => ");

-          TrExpr(su.Substitute(e.Body));

+          TrExpr(su.Substitute(e.Body), wr, inLetExprBody);

         });

 

       } else if (expr is StmtExpr) {

         var e = (StmtExpr)expr;

-        TrExpr(e.E);

+        TrExpr(e.E, wr, inLetExprBody);

 

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         wr.Write("(");

-        TrExpr(e.Test);

+        TrExpr(e.Test, wr, inLetExprBody);

         wr.Write(") ? (");

-        TrExpr(e.Thn);

+        TrExpr(e.Thn, wr, inLetExprBody);

         wr.Write(") : (");

-        TrExpr(e.Els);

+        TrExpr(e.Els, wr, inLetExprBody);

         wr.Write(")");

 

       } else if (expr is ConcreteSyntaxExpression) {

         var e = (ConcreteSyntaxExpression)expr;

-        TrExpr(e.ResolvedExpression);

+        TrExpr(e.ResolvedExpression, wr, inLetExprBody);

 

       } else if (expr is NamedExpr) {

-        TrExpr(((NamedExpr)expr).Body);

+        TrExpr(((NamedExpr)expr).Body, wr, inLetExprBody);

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

       }

     }

 

-    int TrCasePattern(CasePattern pat, string rhsString, Type bodyType) {

+    int TrCasePattern(CasePattern pat, string rhsString, Type bodyType, TextWriter wr) {

       Contract.Requires(pat != null);

       Contract.Requires(rhsString != null);

       int c = 0;

       if (pat.Var != null) {

         var bv = pat.Var;

         if (!bv.IsGhost) {

-          wr.Write("Dafny.Helpers.Let<" + TypeName(bv.Type) + "," + TypeName(bodyType) + ">");

+          wr.Write("Dafny.Helpers.Let<" + TypeName(bv.Type, wr) + "," + TypeName(bodyType, wr) + ">");

           wr.Write("(" + rhsString + ", @" + bv.CompileName + " => ");

           c++;

         }

@@ -3164,7 +3187,7 @@ namespace Microsoft.Dafny {
             // nothing to compile, but do a sanity check

             Contract.Assert(!Contract.Exists(arg.Vars, bv => !bv.IsGhost));

           } else {

-            c += TrCasePattern(arg, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs), rhsString, FormalName(formal, k)), bodyType);

+            c += TrCasePattern(arg, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs, wr), rhsString, FormalName(formal, k)), bodyType, wr);

             k++;

           }

         }

@@ -3172,40 +3195,40 @@ namespace Microsoft.Dafny {
       return c;

     }

 

-    delegate void FCE_Arg_Translator(Expression e);

+    delegate void FCE_Arg_Translator(Expression e, TextWriter wr, bool inLetExpr=false);

 

-    void CompileFunctionCallExpr(FunctionCallExpr e, TextWriter twr, FCE_Arg_Translator tr) {

+   void CompileFunctionCallExpr(FunctionCallExpr e, TextWriter twr, TextWriter wr, bool inLetExprBody, FCE_Arg_Translator tr) {

       Function f = cce.NonNull(e.Function);

       if (f.IsStatic) {

-        twr.Write(TypeName_Companion(e.Receiver.Type));

+        twr.Write(TypeName_Companion(e.Receiver.Type, wr));

       } else {

         twr.Write("(");

-        tr(e.Receiver);

+        tr(e.Receiver, wr, inLetExprBody);

         twr.Write(")");

       }

       twr.Write(".@{0}", f.CompileName);

       if (f.TypeArgs.Count != 0) {

           List<Type> typeArgs = f.TypeArgs.ConvertAll(ta => e.TypeArgumentSubstitutions[ta]);

-          twr.Write("<" + TypeNames(typeArgs) + ">");

+          twr.Write("<" + TypeNames(typeArgs, wr) + ">");

       }

       twr.Write("(");

       string sep = "";

       for (int i = 0; i < e.Args.Count; i++) {

         if (!e.Function.Formals[i].IsGhost) {

           twr.Write(sep);

-          tr(e.Args[i]);

+          tr(e.Args[i], wr);

           sep = ", ";

         }

       }

       twr.Write(")");

     }

 

-    void BetaRedex(List<BoundVar> bvars, List<Expression> exprs, Type bodyType, Action makeBody) {

+    void BetaRedex(List<BoundVar> bvars, List<Expression> exprs, Type bodyType, TextWriter wr, bool inLetExprBody, Action makeBody) {

       Contract.Requires(bvars != null);

       Contract.Requires(exprs != null);

       Contract.Requires(bvars.Count == exprs.Count);

       wr.Write("Dafny.Helpers.Id<");

-      wr.Write(TypeName_UDT(ArrowType.Arrow_FullCompileName, Util.Snoc(bvars.ConvertAll(bv => bv.Type), bodyType)));

+      wr.Write(TypeName_UDT(ArrowType.Arrow_FullCompileName, Util.Snoc(bvars.ConvertAll(bv => bv.Type), bodyType), wr));

       wr.Write(">((");

       wr.Write(Util.Comma(bvars, bv => "@" + bv.CompileName));

       wr.Write(") => ");

@@ -3213,7 +3236,7 @@ namespace Microsoft.Dafny {
       makeBody();

 

       wr.Write(")");

-      TrExprList(exprs);

+      TrExprList(exprs, wr, inLetExprBody);

     }

 

   }

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 16b29c2b..fdbd484e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -7800,9 +7800,15 @@ namespace Microsoft.Dafny {
 

     public override IEnumerable<Expression> SubExpressions {

       get {

-        yield return Root;

-        foreach (var update in Updates) {

-          yield return update.Item3;

+        if (ResolvedExpression == null) {

+          yield return Root;

+          foreach (var update in Updates) {

+            yield return update.Item3;

+          }

+        } else {

+          foreach (var e in ResolvedExpression.SubExpressions) {

+            yield return e;

+          }

         }

       }

     }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 74ff60e7..21476ede 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -9715,8 +9715,28 @@ namespace Microsoft.Dafny
         var c = GetImpliedTypeConstraint(bv, bv.Type, null);

         expr = polarity ? Expression.CreateAnd(c, expr) : Expression.CreateImplies(c, expr);

       }

-      var all = DiscoverAllBounds_Aux_MultipleVars(bvars, expr, polarity);

-      var bests = all.ConvertAll(tup => ComprehensionExpr.BoundedPool.GetBest(tup.Item2, onlyFiniteBounds));

+      List<ComprehensionExpr.BoundedPool> knownBounds = null;

+      var orgCount = bvars.Count;

+      var bests = new List<ComprehensionExpr.BoundedPool>();

+      bool changed = true;

+      // compute the bounds of the BV until no new information is obtained.

+      while (changed) {

+        changed = false;

+        var all = DiscoverAllBounds_Aux_MultipleVars(bvars, expr, polarity, knownBounds);

+        bests = all.ConvertAll(tup => ComprehensionExpr.BoundedPool.GetBest(tup.Item2, onlyFiniteBounds));

+        // check to see if we found new bounds in this iteration

+        int count = 0;

+        for (int i = 0; i < bests.Count; i++) {

+          if (bests[i] == null) {

+            count++;

+          }

+        }

+        if (count >0 && count != orgCount) {

+          changed = true;

+          knownBounds = bests;

+          orgCount = count;

+        }

+      }

       missingBounds = new List<VT>();

       for (var i = 0; i < bvars.Count; i++) {

         if (bests[i] == null) {

@@ -9728,24 +9748,24 @@ namespace Microsoft.Dafny
 

     public static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_SingleVar<VT>(VT v, Expression expr) where VT : IVariable {

       expr = Expression.CreateAnd(GetImpliedTypeConstraint(v, v.Type, null), expr);

-      return DiscoverAllBounds_Aux_SingleVar(new List<VT> { v }, 0, expr, true);

+      return DiscoverAllBounds_Aux_SingleVar(new List<VT> { v }, 0, expr, true, null);

     }

 

-    private static List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>> DiscoverAllBounds_Aux_MultipleVars<VT>(List<VT> bvars, Expression expr, bool polarity) where VT : IVariable {

+    private static List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>> DiscoverAllBounds_Aux_MultipleVars<VT>(List<VT> bvars, Expression expr, bool polarity, List<ComprehensionExpr.BoundedPool> knownBounds) where VT : IVariable {

       Contract.Requires(bvars != null);

       Contract.Requires(expr != null);

       var bb = new List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>>();

       for (var j = 0; j < bvars.Count; j++) {

-        var bounds = DiscoverAllBounds_Aux_SingleVar(bvars, j, expr, polarity);

+        var bounds = DiscoverAllBounds_Aux_SingleVar(bvars, j, expr, polarity, knownBounds);

         bb.Add(new Tuple<VT, List<ComprehensionExpr.BoundedPool>>(bvars[j], bounds));

       }

       return bb;

     }

 

     /// <summary>

-    /// Returns a list of (possibly partial) bounds for "bvars[j]", each of which can be written without mentioning any variable in "bvars[j..]".

+    /// Returns a list of (possibly partial) bounds for "bvars[j]", each of which can be written without mentioning any variable in "bvars[j..]" that is not bounded.

     /// </summary>

-    private static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_Aux_SingleVar<VT>(List<VT> bvars, int j, Expression expr, bool polarity) where VT : IVariable {

+    private static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_Aux_SingleVar<VT>(List<VT> bvars, int j, Expression expr, bool polarity, List<ComprehensionExpr.BoundedPool> knownBounds) where VT : IVariable {

       Contract.Requires(bvars != null);

       Contract.Requires(0 <= j && j < bvars.Count);

       Contract.Requires(expr != null);

@@ -9774,7 +9794,7 @@ namespace Microsoft.Dafny
         }

         var e0 = c.E0;

         var e1 = c.E1;

-        int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, ref e0, ref e1);

+        int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, knownBounds, ref e0, ref e1);

         if (whereIsBv < 0) {

           continue;

         }

@@ -9870,7 +9890,7 @@ namespace Microsoft.Dafny
     /// The other of "e0" and "e1" is an expression whose free variables are not among "boundVars[bvi..]".

     /// Ensures that the resulting "e0" and "e1" are not ConcreteSyntaxExpression's.

     /// </summary>

-    static int SanitizeForBoundDiscovery<VT>(List<VT> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) where VT : IVariable {

+    static int SanitizeForBoundDiscovery<VT>(List<VT> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, List<ComprehensionExpr.BoundedPool> knownBounds, ref Expression e0, ref Expression e1) where VT : IVariable {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

       Contract.Requires(boundVars != null);

@@ -9965,10 +9985,10 @@ namespace Microsoft.Dafny
       }

 

       // Finally, check that the other side does not contain "bv" or any of the bound variables

-      // listed after "bv" in the quantifier.

+      // listed after "bv" in the quantifier that is not bounded.

       var fv = FreeVariables(thatSide);

       for (int i = bvi; i < boundVars.Count; i++) {

-        if (fv.Contains(boundVars[i])) {

+        if (fv.Contains(boundVars[i]) && (knownBounds == null || knownBounds[i] == null)) {

           return -1;

         }

       }

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 8282edc7..6cfbe7e1 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -300,14 +300,14 @@ namespace Microsoft.Dafny
 

       // Compile the Dafny program into a string that contains the C# program

       StringWriter sw = new StringWriter();

-      Dafny.Compiler compiler = new Dafny.Compiler(sw);

+      Dafny.Compiler compiler = new Dafny.Compiler();

       compiler.ErrorWriter = outputWriter;

       var hasMain = compiler.HasMain(dafnyProgram);

       if (DafnyOptions.O.RunAfterCompile && !hasMain) {

         // do no more

         return;

       }

-      compiler.Compile(dafnyProgram);

+      compiler.Compile(dafnyProgram, sw);

       var csharpProgram = sw.ToString();

       bool completeProgram = compiler.ErrorCount == 0;

 

diff --git a/Test/dafny0/NonGhostQuantifiers.dfy.expect b/Test/dafny0/NonGhostQuantifiers.dfy.expect
index 6b737add..0abf0b6c 100644
--- a/Test/dafny0/NonGhostQuantifiers.dfy.expect
+++ b/Test/dafny0/NonGhostQuantifiers.dfy.expect
@@ -11,11 +11,7 @@ NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be
 NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'

 NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'd'

 NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i'

-NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'

 NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'y'

 NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'x'

 NonGhostQuantifiers.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-20 resolution/type errors detected in NonGhostQuantifiers.dfy

+16 resolution/type errors detected in NonGhostQuantifiers.dfy

diff --git a/Test/dafny4/Bug104.dfy b/Test/dafny4/Bug104.dfy
new file mode 100644
index 00000000..ffabbb92
--- /dev/null
+++ b/Test/dafny4/Bug104.dfy
@@ -0,0 +1,12 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+datatype PartRealPartGhost = PartRealPartGhost(x:int, ghost y:int) 

+

+method UpdateField() 

+{

+ var v := PartRealPartGhost(3, 4);

+ ghost var g := 5;

+ v := v[y := g];

+ v := v.(y := g);

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug104.dfy.expect b/Test/dafny4/Bug104.dfy.expect
new file mode 100644
index 00000000..1cc43cbf
--- /dev/null
+++ b/Test/dafny4/Bug104.dfy.expect
@@ -0,0 +1,3 @@
+Bug104.dfy(10,7): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/dafny4/Bug89.dfy b/Test/dafny4/Bug89.dfy
new file mode 100644
index 00000000..12aec5f4
--- /dev/null
+++ b/Test/dafny4/Bug89.dfy
@@ -0,0 +1,15 @@
+// RUN: %dafny  /compile:3 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+method F() returns(x:int)

+  ensures x == 6;

+{

+  x := 5;

+  x := (var y := 1; y + x);

+}

+

+method Main()

+{

+  var x := F();

+  print x;

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug89.dfy.expect b/Test/dafny4/Bug89.dfy.expect
new file mode 100644
index 00000000..5221a5d1
--- /dev/null
+++ b/Test/dafny4/Bug89.dfy.expect
@@ -0,0 +1,6 @@
+

+Dafny program verifier finished with 4 verified, 0 errors

+Program compiled successfully

+Running...

+

+6
\ No newline at end of file
diff --git a/Test/dafny4/Bug91.dfy b/Test/dafny4/Bug91.dfy
new file mode 100644
index 00000000..53e5d5b2
--- /dev/null
+++ b/Test/dafny4/Bug91.dfy
@@ -0,0 +1,40 @@
+// RUN: %dafny /compile:0  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+type SendState = map<int, seq<int>>

+

+function UnAckedMessages(s:SendState) : set<int>

+{

+    set m,dst | dst in s && m in s[dst] :: m

+}

+

+function UnAckedMessagesForDst(s:SendState, dst:int) : set<int>

+    requires dst in s;

+{

+    set m | m in s[dst] :: m

+}

+

+function UnAckedMessages3(s:SendState) : set<int>

+{

+    set m,dst | dst in s && m in UnAckedMessagesForDst(s, dst) :: m

+}

+

+function SeqToSet<T>(s:seq<T>) : set<T>

+{

+    set i | i in s 

+}

+

+function UnAckedMessages4(s:SendState) : set<int>

+{

+		set m,dst | dst in s && m in SeqToSet(s[dst]) :: m

+}

+

+function UnAckedLists(s:SendState) : set<seq<int>>

+{

+    set dst | dst in s :: s[dst]

+}

+

+function UnAckedMessages5(s:SendState) : set<int>

+{

+    set m, list | list in UnAckedLists(s) && m in list :: m

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug91.dfy.expect b/Test/dafny4/Bug91.dfy.expect
new file mode 100644
index 00000000..76f19e0d
--- /dev/null
+++ b/Test/dafny4/Bug91.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 7 verified, 0 errors

diff --git a/Test/pydiff.py b/Test/pydiff.py
index 407fe251..94267960 100644
--- a/Test/pydiff.py
+++ b/Test/pydiff.py
@@ -75,7 +75,8 @@ def preProcess(openFile, stripTrailingCR=False, ignoreAllSpace=False):
     # newline characters because this will create a mess when outputting the
     # diff. Is this the right behaviour?
     deleteChars=' \t'
-    translationTable = str.maketrans('','', deleteChars)
+    if sys.version_info.major  >= 3:
+        translationTable = str.maketrans('','', deleteChars)
 
     copy = [ ]
     for line in original: