From d844ae4047f8a4cd9aa8729fd1132155beaf5d8d Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 15 Jul 2011 15:02:52 +0200
Subject: Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and
 removed some trailing whitespace.

---
 Source/Dafny/Compiler.cs          | 116 +++++------
 Source/Dafny/Dafny.atg            | 149 ++------------
 Source/Dafny/DafnyAst.cs          |  20 +-
 Source/Dafny/DafnyMain.cs         |  14 +-
 Source/Dafny/DafnyPipeline.csproj |   6 +-
 Source/Dafny/Parser.cs            | 209 +++++++++----------
 Source/Dafny/Printer.cs           | 122 +++++------
 Source/Dafny/Resolver.cs          | 262 ++++++++++++------------
 Source/Dafny/Scanner.cs           | 111 +++++-----
 Source/Dafny/SccGraph.cs          |  54 ++---
 Source/Dafny/Translator.cs        | 420 +++++++++++++++++++-------------------
 11 files changed, 679 insertions(+), 804 deletions(-)

(limited to 'Source/Dafny')

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index d61d653d..0653fe2e 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -19,13 +19,13 @@ namespace Microsoft.Dafny {
     }
 
     [ContractInvariantMethod]
-    void ObjectInvariant() 
+    void ObjectInvariant()
     {
       Contract.Invariant(wr!=null);
     }
 
     TextWriter wr;
-    
+
     public int ErrorCount;
     void Error(string msg, params object[] args) {Contract.Requires(msg != null);
       string s = string.Format("Compilation error: " + msg, args);
@@ -33,7 +33,7 @@ namespace Microsoft.Dafny {
       wr.WriteLine("/* {0} */", s);
       ErrorCount++;
     }
-    
+
     void ReadRuntimeSystem() {
       string codebase = cce.NonNull( System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
       string path = System.IO.Path.Combine(codebase, "DafnyRuntime.cs");
@@ -226,7 +226,7 @@ namespace Microsoft.Dafny {
         Indent(indent);  wr.WriteLine("}");
       }
     }
-    
+
     void CompileDatatypeStruct(DatatypeDecl dt, int indent) {
       Contract.Requires(dt != null);
 
@@ -254,23 +254,23 @@ namespace Microsoft.Dafny {
       if (dt.TypeArgs.Count != 0) {
         DtT += "<" + TypeParameters(dt.TypeArgs) + ">";
       }
-      
+
       Indent(indent);
       wr.WriteLine("public struct @{0} {{", DtT);
       int ind = indent + IndentAmount;
-      
+
       Indent(ind);
       wr.WriteLine("Base_{0} d;", DtT);
-      
+
       Indent(ind);
       wr.WriteLine("public Base_{0} _D {{", DtT);
       Indent(ind + IndentAmount);
       wr.WriteLine("get { if (d == null) { d = Default; } return d; }");
       Indent(ind);  wr.WriteLine("}");
-      
+
       Indent(ind);
       wr.WriteLine("public @{0}(Base_{1} d) {{ this.d = d; }}", dt.Name, DtT);
-      
+
       Indent(ind);
       wr.WriteLine("public static Base_{0} Default {{", DtT);
       Indent(ind + IndentAmount);
@@ -320,7 +320,7 @@ namespace Microsoft.Dafny {
       Indent(indent);
       wr.WriteLine("}");
     }
-    
+
     int WriteFormals(string sep, List<Formal/*!*/>/*!*/ formals)
     {
       Contract.Requires(sep != null);
@@ -336,20 +336,20 @@ namespace Microsoft.Dafny {
       }
       return i;  // the number of formals written
     }
-    
+
     string FormalName(Formal formal, int i) {
       Contract.Requires(formal != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
       return formal.HasName ? formal.Name : "_a" + i;
     }
-    
+
     string DtCtorName(DatatypeCtor ctor) {
       Contract.Requires(ctor != null);Contract.Ensures(Contract.Result<string>() != null);
 
       return cce.NonNull(ctor.EnclosingDatatype).Name + "_" + ctor.Name;
     }
-        
+
     void CompileClassMembers(ClassDecl c, int indent)
     {
       Contract.Requires(c != null);
@@ -360,7 +360,7 @@ namespace Microsoft.Dafny {
             Indent(indent);
             wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.Name, DefaultValue(f.Type));
           }
-          
+
         } else if (member is Function) {
           Function f = (Function)member;
           if (f.IsGhost) {
@@ -379,7 +379,7 @@ namespace Microsoft.Dafny {
             CompileReturnBody(f.Body, indent);
             Indent(indent);  wr.WriteLine("}");
           }
-          
+
         } else if (member is Method) {
           Method m = (Method)member;
           if (!m.IsGhost) {
@@ -483,10 +483,10 @@ namespace Microsoft.Dafny {
     }
 
     // ----- Type ---------------------------------------------------------------------------------
-    
+
     readonly string DafnySetClass = "Dafny.Set";
     readonly string DafnySeqClass = "Dafny.Sequence";
-    
+
     string TypeName(Type type)
     {
       Contract.Requires(type != null);
@@ -503,7 +503,7 @@ namespace Microsoft.Dafny {
           type = tp.T;
         }
       }
-      
+
       if (type is BoolType) {
         return "bool";
       } else if (type is IntType) {
@@ -558,7 +558,7 @@ namespace Microsoft.Dafny {
       }
       return s;
     }
-    
+
     string/*!*/ TypeParameters(List<TypeParameter/*!*/>/*!*/ targs) {
       Contract.Requires(cce.NonNullElements(targs));
       Contract.Ensures(Contract.Result<string>() != null);
@@ -571,7 +571,7 @@ namespace Microsoft.Dafny {
       }
       return s;
     }
-    
+
     string DefaultValue(Type type)
     {
       Contract.Requires(type != null);
@@ -588,7 +588,7 @@ namespace Microsoft.Dafny {
           type = tp.T;
         }
       }
-      
+
       if (type is BoolType) {
         return "false";
       } else if (type is IntType) {
@@ -613,16 +613,16 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type
       }
     }
-    
+
     // ----- Stmt ---------------------------------------------------------------------------------
-    
+
     void TrStmt(Statement stmt, int indent)
     {
       Contract.Requires(stmt != null);
       if (stmt.IsGhost) {
         return;
       }
-      
+
       if (stmt is PrintStmt) {
         PrintStmt s = (PrintStmt)stmt;
         foreach (Attributes.Argument arg in s.Args) {
@@ -723,19 +723,19 @@ namespace Microsoft.Dafny {
         } else {
           TrRhs(null, s.Lhs, s.Rhs, indent);
         }
-        
+
       } else if (stmt is VarDecl) {
         TrVarDecl((VarDecl)stmt, true, indent);
-        
+
       } else if (stmt is CallStmt) {
         CallStmt s = (CallStmt)stmt;
         TrCallStmt(s, null, indent);
-        
+
       } else if (stmt is BlockStmt) {
         Indent(indent);  wr.WriteLine("{");
         TrStmtList(((BlockStmt)stmt).Body, indent);
         Indent(indent);  wr.WriteLine("}");
-        
+
       } else if (stmt is IfStmt) {
         IfStmt s = (IfStmt)stmt;
         Indent(indent);
@@ -746,7 +746,7 @@ namespace Microsoft.Dafny {
           TrExpr(s.Guard);
           wr.WriteLine(")");
         }
-        
+
         TrStmt(s.Thn, indent);
         if (s.Els != null && s.Guard != null) {
           Indent(indent);  wr.WriteLine("else");
@@ -816,20 +816,20 @@ namespace Microsoft.Dafny {
         tmpVarCount++;
         string TType = TypeName(s.BoundVar.Type);
         string RhsType = TypeName(cce.NonNull(s.BodyAssign.Lhs.Type));
-        
+
         Indent(indent);
         wr.WriteLine("List<Pair<{0},{1}>> {2} = new List<Pair<{0},{1}>>();", TType, RhsType, pu);
-        
+
         Indent(indent);
         wr.Write("foreach ({0} @{1} in (", TType, s.BoundVar.Name);
         TrExpr(s.Collection);
         wr.WriteLine(").Elements) {");
-        
+
         Indent(indent + IndentAmount);
         wr.Write("if (");
         TrExpr(s.Range);
         wr.WriteLine(") {");
-        
+
         foreach (PredicateStmt p in s.BodyPrefix) {
           TrStmt(p, indent + 2*IndentAmount);
         }
@@ -842,7 +842,7 @@ namespace Microsoft.Dafny {
           wr.Write(DefaultValue(s.BodyAssign.Lhs.Type));
         }
         wr.WriteLine("))");
-        
+
         Indent(indent + IndentAmount);  wr.WriteLine("}");
         Indent(indent);  wr.WriteLine("}");
 
@@ -851,7 +851,7 @@ namespace Microsoft.Dafny {
         FieldSelectExpr fse = (FieldSelectExpr)s.BodyAssign.Lhs;
         wr.WriteLine("{0}.Car.{1} = {0}.Cdr;", pr, fse.FieldName);
         Indent(indent);  wr.WriteLine("}");
-        
+
       } else if (stmt is MatchStmt) {
         MatchStmt s = (MatchStmt)stmt;
         // Type source = e;
@@ -1035,16 +1035,16 @@ namespace Microsoft.Dafny {
       }
       Contract.Assert(j == outTmps.Count);
     }
-    
+
     int tmpVarCount = 0;
-    
+
     void TrAssignmentRhs(AssignmentRhs rhs) {
       Contract.Requires(rhs != null);
       Contract.Requires(!(rhs is HavocRhs));
       if (rhs is ExprRhs) {
         ExprRhs e = (ExprRhs)rhs;
         TrExpr(e.Expr);
-        
+
       } else {
         TypeRhs tp = (TypeRhs)rhs;
         if (tp.ArrayDimensions == null) {
@@ -1074,7 +1074,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     void TrStmtList(List<Statement/*!*/>/*!*/ stmts, int indent) {Contract.Requires(cce.NonNullElements(stmts));
       foreach (Statement ss in stmts) {
         TrStmt(ss, indent + IndentAmount);
@@ -1131,7 +1131,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-        
+
     // ----- Expression ---------------------------------------------------------------------------
 
     void TrParenExpr(string prefix, Expression expr) {
@@ -1147,7 +1147,7 @@ namespace Microsoft.Dafny {
       TrExpr(expr);
       wr.Write(")");
     }
-    
+
     void TrExprList(List<Expression/*!*/>/*!*/ exprs) {
       Contract.Requires(cce.NonNullElements(exprs));
       wr.Write("(");
@@ -1179,26 +1179,26 @@ namespace Microsoft.Dafny {
         } else {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected literal
         }
-        
+
       } else if (expr is ThisExpr) {
         wr.Write("this");
-        
+
       } else if (expr is IdentifierExpr) {
         IdentifierExpr e = (IdentifierExpr)expr;
         wr.Write("@" + e.Var.Name);
-      
+
       } else if (expr is SetDisplayExpr) {
         SetDisplayExpr e = (SetDisplayExpr)expr;
         Type elType = cce.NonNull((SetType)e.Type).Arg;
         wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType));
         TrExprList(e.Elements);
-        
+
       } else if (expr is SeqDisplayExpr) {
         SeqDisplayExpr e = (SeqDisplayExpr)expr;
         Type elType = cce.NonNull((SeqType)e.Type).Arg;
         wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));
         TrExprList(e.Elements);
-      
+
       } else if (expr is FieldSelectExpr) {
         FieldSelectExpr e = (FieldSelectExpr)expr;
         SpecialField sf = e.Field as SpecialField;
@@ -1211,7 +1211,7 @@ namespace Microsoft.Dafny {
           TrParenExpr(e.Obj);
           wr.Write(".@{0}", e.Field.Name);
         }
-        
+
       } else if (expr is SeqSelectExpr) {
         SeqSelectExpr e = (SeqSelectExpr)expr;
         TrParenExpr(e.Seq);
@@ -1233,7 +1233,7 @@ namespace Microsoft.Dafny {
             TrParenExpr(".Drop", e.E0);
           }
         }
-      
+
       } else if (expr is MultiSelectExpr) {
         MultiSelectExpr e = (MultiSelectExpr)expr;
         TrParenExpr(e.Array);
@@ -1253,7 +1253,7 @@ namespace Microsoft.Dafny {
         wr.Write(", ");
         TrExpr(e.Value);
         wr.Write(")");
-      
+
       } else if (expr is FunctionCallExpr) {
         FunctionCallExpr e = (FunctionCallExpr)expr;
         Function f = cce.NonNull(e.Function);
@@ -1273,7 +1273,7 @@ namespace Microsoft.Dafny {
           }
         }
         wr.Write(")");
-      
+
       } else if (expr is DatatypeValue) {
         DatatypeValue dtv = (DatatypeValue)expr;
         Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved
@@ -1292,13 +1292,13 @@ namespace Microsoft.Dafny {
           }
         }
         wr.Write("))");
-          
+
       } else if (expr is OldExpr) {
         Contract.Assert(false); throw new cce.UnreachableException();  // 'old' is always a ghost (right?)
-      
+
       } else if (expr is FreshExpr) {
         Contract.Assert(false); throw new cce.UnreachableException();  // 'fresh' is always a ghost
-      
+
       } else if (expr is UnaryExpr) {
         UnaryExpr e = (UnaryExpr)expr;
         switch (e.Op) {
@@ -1323,13 +1323,13 @@ namespace Microsoft.Dafny {
           default:
             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected unary expression
         }
-      
+
       } else if (expr is BinaryExpr) {
         BinaryExpr e = (BinaryExpr)expr;
         string opString = null;
         string preOpString = "";
         string callString = null;
-        
+
         switch (e.ResolvedOp) {
           case BinaryExpr.ResolvedOpcode.Iff:
             opString = "==";  break;
@@ -1339,7 +1339,7 @@ namespace Microsoft.Dafny {
             opString = "||";  break;
           case BinaryExpr.ResolvedOpcode.And:
             opString = "&&";  break;
-            
+
           case BinaryExpr.ResolvedOpcode.EqCommon: {
             Type t = cce.NonNull(e.E0.Type);
             if (t.IsDatatype || t.IsTypeParameter) {
@@ -1359,7 +1359,7 @@ namespace Microsoft.Dafny {
             }
             break;
           }
-            
+
           case BinaryExpr.ResolvedOpcode.Lt:
             opString = "<";  break;
           case BinaryExpr.ResolvedOpcode.Le:
@@ -1460,7 +1460,7 @@ namespace Microsoft.Dafny {
           TrExpr(e.E1);
           wr.Write(")");
         }
-      
+
       } else if (expr is QuantifierExpr) {
         var e = (QuantifierExpr)expr;
         Contract.Assert(e.Bounds != null);  // for non-ghost quantifiers, the resolver would have insisted on finding bounds
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 15d39460..c0aae345 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -3,39 +3,29 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
 //
 //-----------------------------------------------------------------------------*/
-
 /*---------------------------------------------------------------------------
 // Dafny
 // Rustan Leino, first created 25 January 2008
 //--------------------------------------------------------------------------*/
-
 using System.Collections.Generic;
 using System.Numerics;
 using Microsoft.Boogie;
 using System.IO;
 using System.Text;
-
-
 COMPILER Dafny
-
 /*--------------------------------------------------------------------------*/
-
 static List<ModuleDecl/*!*/> theModules;
 static BuiltIns theBuiltIns;
-
-
 static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
 static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
 static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
 static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");
 static int anonymousIds = 0;
-
 struct MemberModifiers {
   public bool IsGhost;
   public bool IsStatic;
   public bool IsUnlimited;
 }
-
 // helper routine for parsing call statements
 private static Expression/*!*/ ConvertToLocal(Expression/*!*/ e)
 {
@@ -47,7 +37,6 @@ Contract.Ensures(Contract.Result<Expression>() != null);
   }
   return e;  // cannot convert to IdentifierExpr (or is already an IdentifierExpr)
 }
-
 ///<summary>
 /// Parses top-level things (modules, classes, datatypes, class members) from "filename"
 /// and appends them in appropriate form to "modules".
@@ -68,7 +57,6 @@ public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ module
     }
   }
 }
-
 ///<summary>
 /// Parses top-level things (modules, classes, datatypes, class members)
 /// and appends them in appropriate form to "modules".
@@ -82,7 +70,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   Errors errors = new Errors();
   return Parse(s, filename, modules, builtIns, errors);
 }
-
 ///<summary>
 /// Parses top-level things (modules, classes, datatypes, class members)
 /// and appends them in appropriate form to "modules".
@@ -108,7 +95,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   theBuiltIns = oldBuiltIns;
   return parser.errors.count;
 }
-
 /*--------------------------------------------------------------------------*/
 CHARACTERS
   letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
@@ -116,25 +102,20 @@ CHARACTERS
   posDigit = "123456789".
   special = "'_?\\".
   glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
-
   cr        = '\r'.
   lf        = '\n'.
   tab       = '\t'.
-
   space = ' '.
   quote = '"'.
-
   nondigit = letter + special.
   idchar = nondigit + digit.
   nonquote = letter + digit + space + glyph.
-
   /* exclude the characters in 'array' */
   nondigitMinusA = nondigit - 'a'.
   idcharMinusA = idchar - 'a'.
   idcharMinusR = idchar - 'r'.
   idcharMinusY = idchar - 'y'.
   idcharMinusPosDigit = idchar - posDigit.
-
 /*------------------------------------------------------------------------*/
 TOKENS
   ident =  nondigitMinusA {idchar}            /* if char 0 is not an 'a', then anything else is fine */
@@ -147,23 +128,16 @@ TOKENS
   digits = digit {digit}.
   arrayToken = 'a' 'r' 'r' 'a' 'y' [posDigit {digit}].
   string = quote {nonquote} quote.
-
 COMMENTS FROM "/*" TO "*/" NESTED
 COMMENTS FROM "//" TO lf
-
 IGNORE cr + lf + tab
-
-
 /*------------------------------------------------------------------------*/
 PRODUCTIONS
-
 Dafny
 = (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
      Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;
-
      List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();
      ModuleDecl module;
-     
      // to support multiple files, create a default module only if theModules doesn't already contain one
      DefaultModuleDecl defaultModule = null;
      foreach (ModuleDecl mdecl in theModules) {
@@ -206,7 +180,6 @@ Dafny
   .)
   EOF
   .
-
 ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
 = (. Contract.Requires(module != null);
      Contract.Ensures(Contract.ValueAtReturn(out c) != null);
@@ -227,16 +200,15 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
   "{"                                            (. bodyStart = t; .)
   { ClassMemberDecl<members, true>
   }
-  "}"                                      
-  (. if (optionalId == null)        
+  "}"
+  (. if (optionalId == null)
        c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
-     else 
+     else
        c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
      c.BodyStartTok = bodyStart;
      c.BodyEndTok = t;
   .)
   .
-
 ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
 = (. Contract.Requires(cce.NonNullElements(mm));
      Method/*!*/ m;
@@ -247,13 +219,12 @@ ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
   | "static"                               (. mmod.IsStatic = true; .)
   | "unlimited"                            (. mmod.IsUnlimited = true; .)
   }
-  ( FieldDecl<mmod, mm>  
+  ( FieldDecl<mmod, mm>
   | FunctionDecl<mmod, out f>                   (. mm.Add(f); .)
   | MethodDecl<mmod, allowConstructors, out m>  (. mm.Add(m); .)
-  | CouplingInvDecl<mmod, mm> 
+  | CouplingInvDecl<mmod, mm>
   )
   .
-
 DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
 = (. Contract.Requires(module != null);
      Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);
@@ -276,7 +247,6 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
      dt.BodyEndTok = t;
   .)
   .
-
 DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
 = (. Contract.Requires(cce.NonNullElements(ctors));
      Attributes attrs = null;
@@ -288,7 +258,6 @@ DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
   [ FormalsOptionalIds<formals> ]
   (. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .)
   .
-
 FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
 = (. Contract.Requires(cce.NonNullElements(mm));
      Attributes attrs = null;
@@ -304,7 +273,6 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
   }
   ";"
   .
-
 CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
 = (. Contract.Requires(cce.NonNullElements(mm));
      Attributes attrs = null;
@@ -317,17 +285,15 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
      if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }
      if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }
   .)
-  { Attribute<ref attrs> }  
+  { Attribute<ref attrs> }
   Ident<out id>                                     (. ids.Add(id); .)
   { "," Ident<out id>                               (. ids.Add(id); .)
   }
-  "by"    
+  "by"
   Expression<out e>
   ";"
-  (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)  
+  (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)
   .
-
-
 GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>
 /* isGhost always returns as false if allowGhostKeyword is false */
 = (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
@@ -337,14 +303,12 @@ GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out boo
   ]
   IdentType<out id, out ty>
   .
-
 IdentType<out IToken/*!*/ id, out Type/*!*/ ty>
 = (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
   Ident<out id>
   ":"
   Type<out ty>
   .
-
 LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
 = (. IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;
   .)
@@ -353,7 +317,6 @@ LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
   ]
   (. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
   .
-
 IdentTypeOptional<out BoundVar/*!*/ var>
 = (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;
   .)
@@ -362,7 +325,6 @@ IdentTypeOptional<out BoundVar/*!*/ var>
   ]
   (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
   .
-
 TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ ty, out bool isGhost>
 = (.Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
      Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
@@ -389,9 +351,7 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t
      }
   .)
   .
-
 /*------------------------------------------------------------------------*/
-
 GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
 = (. Contract.Requires(cce.NonNullElements(typeArgs));
      IToken/*!*/ id; .)
@@ -401,9 +361,7 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
   }
   ">"
   .
-
 /*------------------------------------------------------------------------*/
-
 MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
 = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
      IToken/*!*/ id;
@@ -447,11 +405,9 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   [ "returns"                                 (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
     Formals<false, !mmod.IsGhost, outs>
   ]
-
   { MethodSpec<req, mod, ens, dec> }
   [ BlockStmt<out bb, out bodyStart, out bodyEnd>    (. body = (BlockStmt)bb; .)
   ]
-  
   (. if (isRefinement)
        m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
      else if (isConstructor)
@@ -462,7 +418,6 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
      m.BodyEndTok = bodyEnd;
  .)
   .
-
 MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,
            List<Expression/*!*/>/*!*/ decreases.>
 = (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
@@ -480,8 +435,7 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
   | "decreases" DecreasesList<decreases, false> ";"
   )
   .
-
-Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.> 
+Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
 = (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; .)
   "("
   [
@@ -491,8 +445,7 @@ Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
   ]
   ")"
   .
-
-FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.> 
+FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
 = (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; .)
   "("
   [
@@ -502,14 +455,11 @@ FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
   ]
   ")"
   .
-
 /*------------------------------------------------------------------------*/
-
 Type<out Type/*!*/ ty>
 = (. Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; .)
   TypeAndToken<out tok, out ty>
   .
-
 TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
 = (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/
      List<Type/*!*/>/*!*/ gt;
@@ -523,7 +473,6 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
                                        }
                                        ty = new SetType(gt[0]);
                                     .)
-    
   | "seq"                           (. tok = t;  gt = new List<Type/*!*/>(); .)
     GenericInstantiation<gt>        (. if (gt.Count != 1) {
                                          SemErr("seq type expects exactly one type argument");
@@ -533,7 +482,6 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
   | ReferenceType<out tok, out ty>
   )
   .
-
 ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
 = (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
      tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/
@@ -554,7 +502,6 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
     [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt); .)
   )
   .
-
 GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
 = (. Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; .)
   "<"
@@ -563,9 +510,7 @@ GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
     }
   ">"
   .
-
 /*------------------------------------------------------------------------*/
-
 FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
 = (. Contract.Ensures(Contract.ValueAtReturn(out f)!=null);
      Attributes attrs = null;
@@ -588,7 +533,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
   .)
   { Attribute<ref attrs> }
-  Ident<out id> 
+  Ident<out id>
   [ GenericParameters<typeArgs> ]
   Formals<true, isFunctionMethod, formals>
   ":"
@@ -601,7 +546,6 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
      f.BodyEndTok = bodyEnd;
   .)
   .
-
 FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases.>
 = (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
      Expression/*!*/ e;  FrameExpression/*!*/ fe; .)
@@ -614,7 +558,6 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r
   | "decreases" DecreasesList<decreases, false> ";"
   )
   .
-
 PossiblyWildExpression<out Expression/*!*/ e>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
      e = dummyExpr; .)
@@ -625,7 +568,6 @@ PossiblyWildExpression<out Expression/*!*/ e>
   | Expression<out e>
   )
   .
-
 PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>
 = (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; .)
   /* A reads clause can list a wildcard, which allows the enclosing function to
@@ -638,7 +580,6 @@ PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>
   | FrameExpression<out fe>
   )
   .
-
 FrameExpression<out FrameExpression/*!*/ fe>
 = (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e;  IToken/*!*/ id;  string fieldName = null; .)
   Expression<out e>
@@ -646,16 +587,13 @@ FrameExpression<out FrameExpression/*!*/ fe>
   ]
   (. fe = new FrameExpression(e, fieldName); .)
   .
-
 FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)
   "{"                         (. bodyStart = t; .)
   Expression<out e>
   "}"                         (. bodyEnd = t; .)
   .
-  
 /*------------------------------------------------------------------------*/
-
 BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
 = (. Contract.Ensures(Contract.ValueAtReturn(out block) != null);
      List<Statement/*!*/> body = new List<Statement/*!*/>();
@@ -666,13 +604,11 @@ BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
   "}"                                  (. bodyEnd = t;
                                           block = new BlockStmt(bodyStart, body); .)
   .
-
 Stmt<.List<Statement/*!*/>/*!*/ ss.>
 = (. Statement/*!*/ s;
   .)
   OneStmt<out s>                                (. ss.Add(s); .)
   .
-
 OneStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  IToken/*!*/ id;  string label = null;
      s = dummyStmt;  /* to please the compiler */
@@ -702,7 +638,6 @@ OneStmt<out Statement/*!*/ s>
   | ReturnStmt<out s>
   )
   .
-
 ReturnStmt<out Statement/*!*/ s>
 = (.
    IToken returnTok = null;
@@ -738,7 +673,6 @@ UpdateStmt<out Statement/*!*/ s>
   )
   (. s = new UpdateStmt(x, lhss, rhss); .)
   .
-
 Rhs<out AssignmentRhs r, Expression receiverForInitCall>
 = (. IToken/*!*/ x, newToken;  Expression/*!*/ e;
      List<Expression> ee = null;
@@ -766,17 +700,13 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
          r = new TypeRhs(newToken, ty, initCall);
        }
     .)
-    
   /* One day, the choose expression should be treated just as a special case of a method call. */
   | "choose"                           (. x = t; .)
     Expression<out e>                  (. r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); .)
-
   | "*"                                (. r = new HavocRhs(t); .)
-
   | Expression<out e>                  (. r = new ExprRhs(e); .)
   )
   .
-
 VarDeclStatement<.out Statement/*!*/ s.>
 = (. IToken x = null, assignTok = null;  bool isGhost = false;
      VarDecl/*!*/ d;
@@ -810,7 +740,6 @@ VarDeclStatement<.out Statement/*!*/ s.>
      s = new VarDeclStmt(x, lhss, update);
   .)
   .
-
 IfStmt<out Statement/*!*/ ifStmt>
 = (. Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x;
      Expression guard;
@@ -836,7 +765,6 @@ IfStmt<out Statement/*!*/ ifStmt>
     (. ifStmt = new AlternativeStmt(x, alternatives); .)
   )
   .
-
 AlternativeBlock<.out List<GuardedAlternative> alternatives.>
 = (. alternatives = new List<GuardedAlternative>();
      IToken x;
@@ -853,7 +781,6 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives.>
   }
   "}"
   .
-
 WhileStmt<out Statement/*!*/ stmt>
 = (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
      Expression guard;
@@ -877,7 +804,6 @@ WhileStmt<out Statement/*!*/ stmt>
     (. stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); .)
   )
   .
-
 LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>
 = (. bool isFree;  Expression/*!*/ e; FrameExpression/*!*/ fe;
      invariants = new List<MaybeFreeExpression/*!*/>();
@@ -898,7 +824,6 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
                ] ";"
   }
   .
-
 DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
 = (. Expression/*!*/ e; .)
   PossiblyWildExpression<out e>          (. if (!allowWildcard && e is WildcardExpr) {
@@ -915,7 +840,6 @@ DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
                                          .)
   }
   .
-
 Guard<out Expression e>   /* null represents demonic-choice */
 = (. Expression/*!*/ ee;  e = null; .)
   "("
@@ -924,7 +848,6 @@ Guard<out Expression e>   /* null represents demonic-choice */
   )
   ")"
   .
-
 MatchStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
      Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;
@@ -937,7 +860,6 @@ MatchStmt<out Statement/*!*/ s>
   "}"
   (. s = new MatchStmt(x, e, cases); .)
   .
-
 CaseStatement<out MatchCaseStmt/*!*/ c>
 = (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
      IToken/*!*/ x, id, arg;
@@ -955,9 +877,7 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
     { Stmt<body> }
   (. c = new MatchCaseStmt(x, id.val, arguments, body); .)
   .
-
 /*------------------------------------------------------------------------*/
-
 ForeachStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
      IToken/*!*/ x, boundVar;
@@ -988,19 +908,16 @@ ForeachStmt<out Statement/*!*/ s>
                                                   }
                                                .)
   .
-
 AssertStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; .)
   "assert"                                     (. x = t; .)
   Expression<out e> ";"                        (. s = new AssertStmt(x, e); .)
   .
-
 AssumeStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; .)
   "assume"                                     (. x = t; .)
   Expression<out e> ";"                        (. s = new AssumeStmt(x, e); .)
   .
-
 PrintStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;
      List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
@@ -1011,13 +928,11 @@ PrintStmt<out Statement/*!*/ s>
   }
   ";"                                          (. s = new PrintStmt(x, args); .)
   .
-
 /*------------------------------------------------------------------------*/
 Expression<out Expression/*!*/ e>
 =
   EquivExpression<out e>
   .
-
 /*------------------------------------------------------------------------*/
 EquivExpression<out Expression/*!*/ e0>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
@@ -1026,9 +941,7 @@ EquivExpression<out Expression/*!*/ e0>
     ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)
   }
   .
-
 EquivOp = "<==>" | '\u21d4'.
-
 /*------------------------------------------------------------------------*/
 ImpliesExpression<out Expression/*!*/ e0>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
@@ -1037,9 +950,7 @@ ImpliesExpression<out Expression/*!*/ e0>
     ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
   ]
   .
-
 ImpliesOp = "==>" | '\u21d2'.
-
 /*------------------------------------------------------------------------*/
 LogicalExpression<out Expression/*!*/ e0>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
@@ -1056,10 +967,8 @@ LogicalExpression<out Expression/*!*/ e0>
     }
   ]
   .
-
 AndOp = "&&" | '\u2227'.
 OrOp = "||" | '\u2228'.
-
 /*------------------------------------------------------------------------*/
 RelationalExpression<out Expression/*!*/ e>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
@@ -1143,7 +1052,6 @@ RelationalExpression<out Expression/*!*/ e>
      }
   .)
   .
-
 RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
 = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
   ( "=="           (. x = t;  op = BinaryExpr.Opcode.Eq; .)
@@ -1160,7 +1068,6 @@ RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
   | '\u2265'       (. x = t;  op = BinaryExpr.Opcode.Ge; .)
   )
   .
-
 /*------------------------------------------------------------------------*/
 Term<out Expression/*!*/ e0>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; .)
@@ -1169,14 +1076,12 @@ Term<out Expression/*!*/ e0>
     Factor<out e1>                             (. e0 = new BinaryExpr(x, op, e0, e1); .)
   }
   .
-
 AddOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
 =          (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; .)
   ( "+"            (. x = t;  op = BinaryExpr.Opcode.Add; .)
   | "-"            (. x = t;  op = BinaryExpr.Opcode.Sub; .)
   )
   .
-
 /*------------------------------------------------------------------------*/
 Factor<out Expression/*!*/ e0>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; .)
@@ -1185,7 +1090,6 @@ Factor<out Expression/*!*/ e0>
     UnaryExpression<out e1>                    (. e0 = new BinaryExpr(x, op, e0, e1); .)
   }
   .
-
 MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
 = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
   ( "*"            (. x = t;  op = BinaryExpr.Opcode.Mul; .)
@@ -1193,7 +1097,6 @@ MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
   | "%"            (. x = t;  op = BinaryExpr.Opcode.Mod; .)
   )
   .
-
 /*------------------------------------------------------------------------*/
 UnaryExpression<out Expression/*!*/ e>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; .)
@@ -1209,7 +1112,6 @@ UnaryExpression<out Expression/*!*/ e>
     { Suffix<ref e> }
   )
   .
-
 Lhs<out Expression e>
 = (. e = null;  // to please the compiler
   .)
@@ -1220,9 +1122,7 @@ Lhs<out Expression e>
     { Suffix<ref e> }
   )
   .
-
 NegOp = "!" | '\u00ac'.
-
 /* A ConstAtomExpression is never an l-value.  Also, a ConstAtomExpression is never followed by
  * an open paren (but could very well have a suffix that starts with a period or a square bracket).
  * (The "Also..." part may change if expressions in Dafny could yield functions.)
@@ -1251,7 +1151,6 @@ ConstAtomExpression<out Expression/*!*/ e>
     ")"
   )
   .
-
 DisplayExpr<out Expression e>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
      IToken/*!*/ x;  List<Expression/*!*/>/*!*/ elements;
@@ -1265,7 +1164,6 @@ DisplayExpr<out Expression e>
     "]"
   )
   .
-
 EndlessExpression<out Expression e>
 = (. IToken/*!*/ x;
      Expression e0, e1;
@@ -1280,7 +1178,6 @@ EndlessExpression<out Expression e>
   | ComprehensionExpr<out e>
   )
   .
-
 MatchExpression<out Expression/*!*/ e>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;
      List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
@@ -1294,7 +1191,6 @@ MatchExpression<out Expression/*!*/ e>
   }
   (. e = new MatchExpr(x, e, cases); .)
   .
-
 CaseExpression<out MatchCaseExpr/*!*/ c>
 = (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;
      List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
@@ -1310,9 +1206,7 @@ CaseExpression<out MatchCaseExpr/*!*/ c>
   "=>"
   Expression<out body>       (. c = new MatchCaseExpr(x, id.val, arguments, body); .)
   .
-
 /*------------------------------------------------------------------------*/
-
 DottedIdentifiersAndFunction<out Expression e>
 = (. IToken id;  IToken openParen = null;
      List<Expression> args = null;
@@ -1328,7 +1222,6 @@ DottedIdentifiersAndFunction<out Expression e>
   ]
   (. e = new IdentifierSequence(idents, openParen, args); .)
   .
-
 Suffix<ref Expression/*!*/ e>
 = (. Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x;  List<Expression/*!*/>/*!*/ args;
      Expression e0 = null;  Expression e1 = null;  Expression/*!*/ ee;  bool anyDots = false;
@@ -1341,7 +1234,6 @@ Suffix<ref Expression/*!*/ e>
         [ Expressions<args> ]
       ")"                                      (. e = new FunctionCallExpr(id, id.val, e, args); .)
     ]                                          (. if (!func) { e = new FieldSelectExpr(id, e, id.val); } .)
-    
   | "["                                        (. x = t; .)
       ( Expression<out ee>                     (. e0 = ee; .)
         ( ".."                                 (. anyDots = true; .)
@@ -1384,9 +1276,7 @@ Suffix<ref Expression/*!*/ e>
     "]"
   )
   .
-
 /*------------------------------------------------------------------------*/
-
 QuantifierGuts<out Expression/*!*/ q>
 = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;
      bool univ = false;
@@ -1417,11 +1307,9 @@ QuantifierGuts<out Expression/*!*/ q>
      }
   .)
   .
-
 Forall = "forall" | '\u2200'.
 Exists = "exists" | '\u2203'.
 QSep = "::" | '\u2022'.
-
 ComprehensionExpr<out Expression/*!*/ q>
 = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);
      IToken/*!*/ x = Token.NoToken;
@@ -1444,22 +1332,18 @@ ComprehensionExpr<out Expression/*!*/ q>
      q = new SetComprehension(x, bvars, range, body);
   .)
   .
-
 Expressions<.List<Expression/*!*/>/*!*/ args.>
 = (. Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; .)
   Expression<out e>                            (. args.Add(e); .)
   { "," Expression<out e>                      (. args.Add(e); .)
   }
   .
-
 /*------------------------------------------------------------------------*/
-
 Attribute<ref Attributes attrs>
 = "{"
     AttributeBody<ref attrs>
   "}"
   .
-
 AttributeBody<ref Attributes attrs>
 = (. string aName;
      List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();
@@ -1471,14 +1355,12 @@ AttributeBody<ref Attributes attrs>
     }
   ]                                    (. attrs = new Attributes(aName, aArgs, attrs); .)
   .
-
 AttributeArg<out Attributes.Argument/*!*/ arg>
 = (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e;  arg = dummyAttrArg; .)
   ( string                             (. arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); .)
   | Expression<out e>                  (. arg = new Attributes.Argument(e); .)
   )
   .
-
 AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>
 = (. List<Expression/*!*/> es = new List<Expression/*!*/>();
   .)
@@ -1489,21 +1371,17 @@ AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>
     )
   "}"
   .
-
 /*------------------------------------------------------------------------*/
-
 Idents<.List<string/*!*/>/*!*/ ids.>
 = (. IToken/*!*/ id; .)
   Ident<out id>                            (. ids.Add(id.val); .)
   { "," Ident<out id>                      (. ids.Add(id.val); .)
   }
   .
-
 Ident<out IToken/*!*/ x>
 = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
   ident            (. x = t; .)
   .
-
 Nat<out BigInteger n>
 =
   digits
@@ -1513,7 +1391,6 @@ Nat<out BigInteger n>
        SemErr("incorrectly formatted number");
        n = BigInteger.Zero;
      }
-  .) 
+  .)
   .
-
-END Dafny.
\ No newline at end of file
+END Dafny.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 4868be10..8bb381ea 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -400,13 +400,13 @@ namespace Microsoft.Dafny {
 
   /// <summary>
   /// This proxy stands for any type.
-  /// </summary>  
+  /// </summary>
   public class InferredTypeProxy : UnrestrictedTypeProxy {
   }
 
   /// <summary>
   /// This proxy stands for any type, but it originates from an instantiated type parameter.
-  /// </summary>  
+  /// </summary>
   public class ParamTypeProxy : UnrestrictedTypeProxy {
     TypeParameter orig;
     [ContractInvariantMethod]
@@ -432,7 +432,7 @@ namespace Microsoft.Dafny {
 
   /// <summary>
   /// This proxy stands for any datatype.
-  /// </summary>  
+  /// </summary>
   public class DatatypeProxy : RestrictedTypeProxy {
     public override int OrderID {
       get {
@@ -443,7 +443,7 @@ namespace Microsoft.Dafny {
 
   /// <summary>
   /// This proxy stands for object or any class/array type.
-  /// </summary>  
+  /// </summary>
   public class ObjectTypeProxy : RestrictedTypeProxy {
     public override int OrderID {
       get {
@@ -491,7 +491,7 @@ namespace Microsoft.Dafny {
   /// if AllowSeq, or:
   ///     int or set
   /// if !AllowSeq.
-  /// </summary>  
+  /// </summary>
   public class OperationTypeProxy : RestrictedTypeProxy {
     public readonly bool AllowSeq;
     public OperationTypeProxy(bool allowSeq) {
@@ -675,7 +675,7 @@ namespace Microsoft.Dafny {
 
   public class ClassRefinementDecl : ClassDecl {
     public readonly IToken/*!*/ RefinedClass;
-    public ClassDecl Refined; // filled in during resolution 
+    public ClassDecl Refined; // filled in during resolution
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(RefinedClass != null);
@@ -720,7 +720,7 @@ namespace Microsoft.Dafny {
       Dims = dims;
     }
   }
-  
+
   public class DatatypeDecl : TopLevelDecl {
     public readonly List<DatatypeCtor/*!*/>/*!*/ Ctors;
     [ContractInvariantMethod]
@@ -1685,7 +1685,7 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Mod == null || cce.NonNullElements(Mod));
     }
     public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod)
-    : base(tok) 
+    : base(tok)
     {
       Contract.Requires(tok != null);
       Contract.Requires(cce.NonNullElements(invariants));
@@ -2511,7 +2511,7 @@ namespace Microsoft.Dafny {
 
     public List<BoundedPool> Bounds;  // initialized and filled in by resolver
     // invariant Bounds == null || Bounds.Count == BoundVars.Count;
-    public List<BoundVar> MissingBounds;  // filled in during resolution; remains "null" if bounds can be found 
+    public List<BoundVar> MissingBounds;  // filled in during resolution; remains "null" if bounds can be found
     // invariant Bounds == null || MissingBounds == null;
 
     public ComprehensionExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression/*!*/ term, Attributes attrs)
@@ -2529,7 +2529,7 @@ namespace Microsoft.Dafny {
     public override IEnumerable<Expression> SubExpressions {
       get {
         if (Range != null) { yield return Range; }
-        yield return Term; 
+        yield return Term;
       }
     }
   }
diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index a18ea938..3f0b6e97 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -27,21 +27,21 @@ namespace Microsoft.Dafny {
         if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {
           Bpl.CommandLineOptions.Clo.XmlSink.WriteFileFragment(dafnyFileName);
         }
-        if (Bpl.CommandLineOptions.Clo.Trace) 
+        if (Bpl.CommandLineOptions.Clo.Trace)
         {
           Console.WriteLine("Parsing " + dafnyFileName);
         }
 
         int errorCount;
-        try 
+        try
         {
           errorCount = Dafny.Parser.Parse(dafnyFileName, modules, builtIns);
-          if (errorCount != 0) 
+          if (errorCount != 0)
           {
             return string.Format("{0} parse errors detected in {1}", errorCount, dafnyFileName);
           }
-        } 
-        catch (IOException e) 
+        }
+        catch (IOException e)
         {
           return string.Format("Error opening file \"{0}\": {1}", dafnyFileName, e.Message);
         }
@@ -61,7 +61,7 @@ namespace Microsoft.Dafny {
           }
         }
       }
-      
+
       if (Bpl.CommandLineOptions.Clo.NoResolve || Bpl.CommandLineOptions.Clo.NoTypecheck) { return null; }
 
       Dafny.Resolver r = new Dafny.Resolver(program);
@@ -73,4 +73,4 @@ namespace Microsoft.Dafny {
       return null;  // success
     }
   }
-}
\ No newline at end of file
+}
diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index 7f063c2c..6a15b1f7 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
   <PropertyGroup>
     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -147,11 +147,11 @@
     </BootstrapperPackage>
   </ItemGroup>
   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 
+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
        Other similar extension points exist, see Microsoft.Common.targets.
   <Target Name="BeforeBuild">
   </Target>
   <Target Name="AfterBuild">
   </Target>
   -->
-</Project>
\ No newline at end of file
+</Project>
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 42014762..8fcb6bb0 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -5,8 +5,6 @@ using System.IO;
 using System.Text;
 
 
-
-
 using System;
 using System.Diagnostics.Contracts;
 
@@ -25,7 +23,7 @@ public class Parser {
 	const bool T = true;
 	const bool x = false;
 	const int minErrDist = 2;
-	
+
 	public Scanner/*!*/ scanner;
 	public Errors/*!*/  errors;
 
@@ -35,20 +33,16 @@ public class Parser {
 
 static List<ModuleDecl/*!*/> theModules;
 static BuiltIns theBuiltIns;
-
-
 static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
 static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
 static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
 static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");
 static int anonymousIds = 0;
-
 struct MemberModifiers {
   public bool IsGhost;
   public bool IsStatic;
   public bool IsUnlimited;
 }
-
 // helper routine for parsing call statements
 private static Expression/*!*/ ConvertToLocal(Expression/*!*/ e)
 {
@@ -60,7 +54,6 @@ Contract.Ensures(Contract.Result<Expression>() != null);
   }
   return e;  // cannot convert to IdentifierExpr (or is already an IdentifierExpr)
 }
-
 ///<summary>
 /// Parses top-level things (modules, classes, datatypes, class members) from "filename"
 /// and appends them in appropriate form to "modules".
@@ -81,7 +74,6 @@ public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ module
     }
   }
 }
-
 ///<summary>
 /// Parses top-level things (modules, classes, datatypes, class members)
 /// and appends them in appropriate form to "modules".
@@ -95,7 +87,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   Errors errors = new Errors();
   return Parse(s, filename, modules, builtIns, errors);
 }
-
 ///<summary>
 /// Parses top-level things (modules, classes, datatypes, class members)
 /// and appends them in appropriate form to "modules".
@@ -121,7 +112,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   theBuiltIns = oldBuiltIns;
   return parser.errors.count;
 }
-
 /*--------------------------------------------------------------------------*/
 
 
@@ -144,10 +134,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (errDist >= minErrDist) errors.SemErr(t, msg);
 		errDist = 0;
 	}
-	
-    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
-      Contract.Requires(tok != null);
-      Contract.Requires(msg != null);
+
+	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+	  Contract.Requires(tok != null);
+	  Contract.Requires(msg != null);
 	  errors.SemErr(tok, msg);
 	}
 
@@ -160,15 +150,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			la = t;
 		}
 	}
-	
+
 	void Expect (int n) {
 		if (la.kind==n) Get(); else { SynErr(n); }
 	}
-	
+
 	bool StartOf (int s) {
 		return set[s, la.kind];
 	}
-	
+
 	void ExpectWeak (int n, int follow) {
 		if (la.kind == n) Get();
 		else {
@@ -192,26 +182,24 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}
 	}
 
-	
+
 	void Dafny() {
 		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
 		Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;
+		List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();
+		ModuleDecl module;
+		// to support multiple files, create a default module only if theModules doesn't already contain one
+		DefaultModuleDecl defaultModule = null;
+		foreach (ModuleDecl mdecl in theModules) {
+		 defaultModule = mdecl as DefaultModuleDecl;
+		 if (defaultModule != null) { break; }
+		}
+		bool defaultModuleCreatedHere = false;
+		if (defaultModule == null) {
+		 defaultModuleCreatedHere = true;
+		 defaultModule = new DefaultModuleDecl();
+		}
 		
-		     List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();
-		     ModuleDecl module;
-		     
-		     // to support multiple files, create a default module only if theModules doesn't already contain one
-		     DefaultModuleDecl defaultModule = null;
-		     foreach (ModuleDecl mdecl in theModules) {
-		       defaultModule = mdecl as DefaultModuleDecl;
-		       if (defaultModule != null) { break; }
-		     }
-		     bool defaultModuleCreatedHere = false;
-		     if (defaultModule == null) {
-		       defaultModuleCreatedHere = true;
-		       defaultModule = new DefaultModuleDecl();
-		     }
-		  
 		while (StartOf(1)) {
 			if (la.kind == 5) {
 				Get();
@@ -253,14 +241,14 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		 defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
 		 theModules.Add(defaultModule);
 		} else {
-		  // find the default class in the default module, then append membersDefaultClass to its member list
-		  foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
-		    DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;
-		    if (defaultClass != null) {
-		      defaultClass.Members.AddRange(membersDefaultClass);
-		      break;
-		    }
-		  }
+		 // find the default class in the default module, then append membersDefaultClass to its member list
+		 foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
+		   DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;
+		   if (defaultClass != null) {
+		     defaultClass.Members.AddRange(membersDefaultClass);
+		     break;
+		   }
+		 }
 		}
 		
 		Expect(0);
@@ -319,10 +307,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			ClassMemberDecl(members, true);
 		}
 		Expect(8);
-		if (optionalId == null)        
+		if (optionalId == null)
 		 c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
-		else 
-		  c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
+		else
+		 c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
 		c.BodyStartTok = bodyStart;
 		c.BodyEndTok = t;
 		
@@ -496,7 +484,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			if (allowConstructor) {
 			 isConstructor = true;
 			} else {
-			  SemErr(t, "constructors are only allowed in classes");
+			 SemErr(t, "constructors are only allowed in classes");
 			}
 			
 		} else if (la.kind == 10) {
@@ -505,12 +493,12 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		} else SynErr(106);
 		if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
 		if (isConstructor) {
-		  if (mmod.IsGhost) {
-		    SemErr(t, "constructors cannot be declared 'ghost'");
-		  }
-		  if (mmod.IsStatic) {
-		    SemErr(t, "constructors cannot be declared 'static'");
-		  }
+		 if (mmod.IsGhost) {
+		   SemErr(t, "constructors cannot be declared 'ghost'");
+		 }
+		 if (mmod.IsStatic) {
+		   SemErr(t, "constructors cannot be declared 'static'");
+		 }
 		}
 		
 		while (la.kind == 7) {
@@ -536,9 +524,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (isRefinement)
 		 m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
 		else if (isConstructor)
-		  m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);
+		 m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);
 		else
-		  m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
+		 m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
 		m.BodyStartTok = bodyStart;
 		m.BodyEndTok = bodyEnd;
 		
@@ -668,9 +656,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Get();
 			UserDefinedType udt = ty as UserDefinedType;
 			if (udt != null && udt.TypeArgs.Count == 0) {
-			  name = udt.Name;
+			 name = udt.Name;
 			} else {
-			  SemErr(id, "invalid formal-parameter name in datatype constructor");
+			 SemErr(id, "invalid formal-parameter name in datatype constructor");
 			}
 			
 			Type(out ty);
@@ -678,7 +666,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (name != null) {
 		 identName = name;
 		} else {
-		  identName = "#" + anonymousIds++;
+		 identName = "#" + anonymousIds++;
 		}
 		
 	}
@@ -819,7 +807,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (!allowWildcard && e is WildcardExpr) {
 		 SemErr(e.tok, "'decreases *' is only allowed on loops");
 		} else {
-		  decreases.Add(e);
+		 decreases.Add(e);
 		}
 		
 		while (la.kind == 19) {
@@ -828,7 +816,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (!allowWildcard && e is WildcardExpr) {
 			 SemErr(e.tok, "'decreases *' is only allowed on loops");
 			} else {
-			  decreases.Add(e);
+			 decreases.Add(e);
 			}
 			
 		}
@@ -864,7 +852,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}
 			int dims = 1;
 			if (tok.val.Length != 5) {
-			  dims = int.Parse(tok.val.Substring(5));
+			 dims = int.Parse(tok.val.Substring(5));
 			}
 			ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
 			
@@ -1132,13 +1120,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(17);
 		UpdateStmt update;
 		if (rhss.Count == 0) {
-		  update = null;
+		 update = null;
 		} else {
-		  var ies = new List<Expression>();
-		  foreach (var lhs in lhss) {
-		    ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
-		  }
-		  update = new UpdateStmt(assignTok, ies, rhss);
+		 var ies = new List<Expression>();
+		 foreach (var lhs in lhss) {
+		   ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
+		 }
+		 update = new UpdateStmt(assignTok, ies, rhss);
 		}
 		s = new VarDeclStmt(x, lhss, update);
 		
@@ -1261,7 +1249,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (bodyAssign != null) {
 		 s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
 		} else {
-		  s = dummyStmt;  // some error occurred in parsing the bodyAssign
+		 s = dummyStmt;  // some error occurred in parsing the bodyAssign
 		}
 		
 	}
@@ -1322,7 +1310,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (ee != null) {
 			 r = new TypeRhs(newToken, ty, ee);
 			} else {
-			  r = new TypeRhs(newToken, ty, initCall);
+			 r = new TypeRhs(newToken, ty, initCall);
 			}
 			
 		} else if (la.kind == 53) {
@@ -1551,10 +1539,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Expression> chain = null;
 		List<BinaryExpr.Opcode> ops = null;
 		int kind = 0;  // 0 ("uncommitted") indicates chain of ==, possibly with one !=
-		               // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=
-		               // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=
-		               // 3 ("illegal")     indicates illegal chain
-		               // 4 ("disjoint")    indicates chain of disjoint set operators
+		              // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=
+		              // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=
+		              // 3 ("illegal")     indicates illegal chain
+		              // 4 ("disjoint")    indicates chain of disjoint set operators
 		bool hasSeenNeq = false;
 		
 		Term(out e0);
@@ -1565,7 +1553,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Term(out e1);
 			e = new BinaryExpr(x, op, e0, e1);
 			if (op == BinaryExpr.Opcode.Disjoint)
-			  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
+			 acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
 			
 			while (StartOf(14)) {
 				if (chain == null) {
@@ -1621,11 +1609,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Term(out e1);
 				ops.Add(op); chain.Add(e1);
 				if (op == BinaryExpr.Opcode.Disjoint) {
-				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
-				  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
+				 e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
+				 acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
 				}
 				else
-				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
+				 e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
 				
 			}
 		}
@@ -1918,21 +1906,21 @@ List<Expression/*!*/>/*!*/ decreases) {
 			 // make sure an array class with this dimensionality exists
 			 UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true);
 			} else {
-			  if (!anyDots && e0 == null) {
-			    /* a parsing error occurred */
-			    e0 = dummyExpr;
-			  }
-			  Contract.Assert(anyDots || e0 != null);
-			  if (anyDots) {
-			    Contract.Assert(e0 != null || e1 != null);
-			    e = new SeqSelectExpr(x, false, e, e0, e1);
-			  } else if (e1 == null) {
-			    Contract.Assert(e0 != null);
-			    e = new SeqSelectExpr(x, true, e, e0, null);
-			  } else {
-			    Contract.Assert(e0 != null);
-			    e = new SeqUpdateExpr(x, e, e0, e1);
-			  }
+			 if (!anyDots && e0 == null) {
+			   /* a parsing error occurred */
+			   e0 = dummyExpr;
+			 }
+			 Contract.Assert(anyDots || e0 != null);
+			 if (anyDots) {
+			   Contract.Assert(e0 != null || e1 != null);
+			   e = new SeqSelectExpr(x, false, e, e0, e1);
+			 } else if (e1 == null) {
+			   Contract.Assert(e0 != null);
+			   e = new SeqSelectExpr(x, true, e, e0, null);
+			 } else {
+			   Contract.Assert(e0 != null);
+			   e = new SeqUpdateExpr(x, e, e0, e1);
+			 }
 			}
 			
 			Expect(51);
@@ -2046,8 +2034,8 @@ List<Expression/*!*/>/*!*/ decreases) {
 		try {
 		 n = BigInteger.Parse(t.val);
 		} catch (System.FormatException) {
-		  SemErr("incorrectly formatted number");
-		  n = BigInteger.Zero;
+		 SemErr("incorrectly formatted number");
+		 n = BigInteger.Zero;
 		}
 		
 	}
@@ -2102,7 +2090,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (univ) {
 		 q = new ForallExpr(x, bvars, range, body, trigs, attrs);
 		} else {
-		  q = new ExistsExpr(x, bvars, range, body, trigs, attrs);
+		 q = new ExistsExpr(x, bvars, range, body, trigs, attrs);
 		}
 		
 	}
@@ -2221,13 +2209,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 
 	public void Parse() {
 		la = new Token();
-		la.val = "";		
+		la.val = "";
 		Get();
 		Dafny();
+		Expect(0);
 
-    Expect(0);
+		Expect(0);
 	}
-	
+
 	static readonly bool[,]/*!*/ set = {
 		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
 		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
@@ -2254,18 +2243,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 public class Errors {
 	public int count = 0;                                    // number of errors detected
 	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream
-  public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
-  public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-  
+	public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+	public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
 	public void SynErr(string filename, int line, int col, int n) {
-    SynErr(filename, line, col, GetSyntaxErrorString(n));
-  }
-	public virtual void SynErr(string filename, int line, int col, string msg) {
-	  Contract.Requires(msg != null);
+		SynErr(filename, line, col, GetSyntaxErrorString(n));
+	}
+
+	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
+		Contract.Requires(msg != null);
 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
 		count++;
-  }
-  string GetSyntaxErrorString(int n) {
+	}
+
+	string GetSyntaxErrorString(int n) {
 		string s;
 		switch (n) {
 			case 0: s = "EOF expected"; break;
@@ -2415,7 +2406,7 @@ public class Errors {
 
 			default: s = "error " + n; break;
 		}
-    return s;
+		return s;
 	}
 
 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors
@@ -2423,8 +2414,9 @@ public class Errors {
 		Contract.Requires(msg != null);
 		SemErr(tok.filename, tok.line, tok.col, msg);
 	}
+
 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
-	  Contract.Requires(msg != null);
+		Contract.Requires(msg != null);
 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
 		count++;
 	}
@@ -2440,4 +2432,5 @@ public class FatalError: Exception {
 	public FatalError(string m): base(m) {}
 }
 
+
 }
\ No newline at end of file
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index b9c8601e..ba9963c7 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -14,7 +14,7 @@ namespace Microsoft.Dafny {
   class Printer {
     TextWriter wr;
     [ContractInvariantMethod]
-    void ObjectInvariant() 
+    void ObjectInvariant()
     {
       Contract.Invariant(wr!=null);
     }
@@ -23,7 +23,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(wr != null);
       this.wr = wr;
     }
-    
+
     public void PrintProgram(Program prog) {
       Contract.Requires(prog != null);
       if (Bpl.CommandLineOptions.Clo.ShowEnv != Bpl.CommandLineOptions.ShowEnvironment.Never) {
@@ -56,7 +56,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     public void PrintTopLevelDecls(List<TopLevelDecl> classes, int indent) {
       Contract.Requires(classes!= null);
       int i = 0;
@@ -79,7 +79,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     public void PrintClass(ClassDecl c, int indent) {
       Contract.Requires(c != null);
       Indent(indent);
@@ -97,12 +97,12 @@ namespace Microsoft.Dafny {
         wr.WriteLine("}");
       }
     }
-    
+
     public void PrintClass_Members(ClassDecl c, int indent)
     {
       Contract.Requires(c != null);
       Contract.Requires( c.Members.Count != 0);
-    
+
       int state = 0;  // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field
       foreach (MemberDecl m in c.Members) {
         if (m is Method) {
@@ -126,7 +126,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     void PrintClassMethodHelper(string kind, Attributes attrs, string name, List<TypeParameter> typeArgs) {
       Contract.Requires(kind != null);
       Contract.Requires(name != null);
@@ -147,7 +147,7 @@ namespace Microsoft.Dafny {
         wr.Write(">");
       }
     }
-    
+
     public void PrintDatatype(DatatypeDecl dt, int indent) {
       Contract.Requires(dt != null);
       Indent(indent);
@@ -164,17 +164,17 @@ namespace Microsoft.Dafny {
       }
       wr.WriteLine(";");
     }
-    
+
     public void PrintAttributes(Attributes a) {
       if (a != null) {
         PrintAttributes(a.Prev);
-        
+
         wr.Write("{{:{0}", a.Name);
         PrintAttributeArgs(a.Args);
         wr.Write("} ");
       }
     }
-    
+
     public void PrintAttributeArgs(List<Attributes.Argument> args) {
       Contract.Requires(args != null);
       string prefix = " ";
@@ -190,7 +190,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     public void PrintField(Field field, int indent) {
       Contract.Requires(field != null);
       Indent(indent);
@@ -203,7 +203,7 @@ namespace Microsoft.Dafny {
       PrintType(field.Type);
       wr.WriteLine(";");
     }
-    
+
     public void PrintCouplingInvariant(CouplingInvariant inv, int indent) {
       Contract.Requires(inv != null);
       Indent(indent);
@@ -218,7 +218,7 @@ namespace Microsoft.Dafny {
       PrintExpression(inv.Expr);
       wr.WriteLine(";");
     }
-    
+
     public void PrintFunction(Function f, int indent) {
       Contract.Requires(f != null);
       Indent(indent);
@@ -245,20 +245,20 @@ namespace Microsoft.Dafny {
         wr.WriteLine("}");
       }
     }
-    
+
     // ----------------------------- PrintMethod -----------------------------
 
     const int IndentAmount = 2;
     const string BunchaSpaces = "                                ";
     void Indent(int amount)
     {  Contract.Requires( 0 <= amount);
-    
+
       while (0 < amount) {
         wr.Write(BunchaSpaces.Substring(0, amount));
         amount -= BunchaSpaces.Length;
       }
     }
-    
+
     public void PrintMethod(Method method, int indent) {
       Contract.Requires(method != null);
       Indent(indent);
@@ -284,14 +284,14 @@ namespace Microsoft.Dafny {
       PrintFrameSpecLine("modifies", method.Mod, ind);
       PrintSpec("ensures", method.Ens, ind);
       PrintSpecLine("decreases", method.Decreases, ind);
-      
+
       if (method.Body != null) {
         Indent(indent);
         PrintStatement(method.Body, indent);
         wr.WriteLine();
       }
     }
-    
+
     void PrintFormals(List<Formal> ff) {
       Contract.Requires(ff!=null);
       wr.Write("(");
@@ -304,7 +304,7 @@ namespace Microsoft.Dafny {
       }
       wr.Write(")");
     }
-    
+
     void PrintFormal(Formal f) {
       Contract.Requires(f != null);
       if (f.IsGhost) {
@@ -315,7 +315,7 @@ namespace Microsoft.Dafny {
       }
       PrintType(f.Type);
     }
-    
+
     void PrintSpec(string kind, List<Expression> ee, int indent) {
       Contract.Requires(kind != null);
       Contract.Requires(ee != null);
@@ -363,7 +363,7 @@ namespace Microsoft.Dafny {
     }
 
     // ----------------------------- PrintType -----------------------------
-    
+
     public void PrintType(Type ty) {
       Contract.Requires(ty != null);
       wr.Write(ty.ToString());
@@ -379,7 +379,7 @@ namespace Microsoft.Dafny {
     }
 
     // ----------------------------- PrintStatement -----------------------------
-    
+
     /// <summary>
     /// Prints from the current position of the current line.
     /// If the statement requires several lines, subsequent lines are indented at "indent".
@@ -393,23 +393,23 @@ namespace Microsoft.Dafny {
           Indent(indent);
         }
       }
-        
+
       if (stmt is AssertStmt) {
         wr.Write("assert ");
         PrintExpression(((AssertStmt)stmt).Expr);
         wr.Write(";");
-        
+
       } else if (stmt is AssumeStmt) {
         wr.Write("assume ");
         PrintExpression(((AssumeStmt)stmt).Expr);
         wr.Write(";");
-        
+
       } else if (stmt is PrintStmt) {
         PrintStmt s = (PrintStmt)stmt;
         wr.Write("print");
         PrintAttributeArgs(s.Args);
         wr.Write(";");
-        
+
       } else if (stmt is BreakStmt) {
         BreakStmt s = (BreakStmt)stmt;
         if (s.TargetLabel != null) {
@@ -422,7 +422,7 @@ namespace Microsoft.Dafny {
           }
           wr.Write(";");
         }
-        
+
       } else if (stmt is ReturnStmt) {
         var s = (ReturnStmt) stmt;
         wr.Write("return");
@@ -435,14 +435,14 @@ namespace Microsoft.Dafny {
           }
         }
           wr.Write(";");
-        
+
       } else if (stmt is AssignStmt) {
         AssignStmt s = (AssignStmt)stmt;
         PrintExpression(s.Lhs);
         wr.Write(" := ");
         PrintRhs(s.Rhs);
         wr.Write(";");
-        
+
       } else if (stmt is VarDecl) {
         VarDecl s = (VarDecl)stmt;
         if (s.IsGhost) {
@@ -451,7 +451,7 @@ namespace Microsoft.Dafny {
         wr.Write("var {0}", s.Name);
         PrintType(": ", s.OptionalType);
         wr.Write(";");
-      
+
       } else if (stmt is CallStmt) {
         CallStmt s = (CallStmt)stmt;
         wr.Write("call ");
@@ -471,7 +471,7 @@ namespace Microsoft.Dafny {
         wr.Write("{0}(", s.MethodName);
         PrintExpressionList(s.Args);
         wr.Write(");");
-        
+
       } else if (stmt is BlockStmt) {
         wr.WriteLine("{");
         int ind = indent + IndentAmount;
@@ -482,7 +482,7 @@ namespace Microsoft.Dafny {
         }
         Indent(indent);
         wr.Write("}");
-        
+
       } else if (stmt is IfStmt) {
         IfStmt s = (IfStmt)stmt;
         while (true) {
@@ -508,7 +508,7 @@ namespace Microsoft.Dafny {
         PrintAlternatives(indent, s.Alternatives);
         Indent(indent);
         wr.Write("}");
-      
+
       } else if (stmt is WhileStmt) {
         WhileStmt s = (WhileStmt)stmt;
         wr.Write("while (");
@@ -556,7 +556,7 @@ namespace Microsoft.Dafny {
         wr.WriteLine();
         Indent(indent);
         wr.Write("}");
-        
+
       } else if (stmt is MatchStmt) {
         MatchStmt s = (MatchStmt)stmt;
         wr.Write("match ");
@@ -644,7 +644,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     void PrintRhs(AssignmentRhs rhs) {
       Contract.Requires(rhs != null);
       if (rhs is ExprRhs) {
@@ -673,7 +673,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS
       }
     }
-    
+
     void PrintGuard(Expression guard) {
       if (guard == null) {
         wr.Write("*");
@@ -681,7 +681,7 @@ namespace Microsoft.Dafny {
         PrintExpression(guard);
       }
     }
-    
+
     // ----------------------------- PrintExpression -----------------------------
 
     public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen) {
@@ -739,12 +739,12 @@ namespace Microsoft.Dafny {
         wr.WriteLine(endWithCloseParen ? ")" : "");
       }
     }
-    
+
     public void PrintExpression(Expression expr) {
       Contract.Requires(expr != null);
       PrintExpr(expr, 0, false, true, -1);
     }
-    
+
     /// <summary>
     /// An indent of -1 means print the entire expression on one line.
     /// </summary>
@@ -752,7 +752,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);
       PrintExpr(expr, 0, false, true, indent);
     }
-    
+
     /// <summary>
     /// An indent of -1 means print the entire expression on one line.
     /// </summary>
@@ -770,13 +770,13 @@ namespace Microsoft.Dafny {
         } else {
           wr.Write((BigInteger)e.Value);
         }
-      
+
       } else if (expr is ThisExpr) {
         wr.Write("this");
-  
+
       } else if (expr is IdentifierExpr) {
         wr.Write(((IdentifierExpr)expr).Name);
-      
+
       } else if (expr is DatatypeValue) {
         DatatypeValue dtv = (DatatypeValue)expr;
         wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName);
@@ -785,13 +785,13 @@ namespace Microsoft.Dafny {
           PrintExpressionList(dtv.Arguments);
           wr.Write(")");
         }
-        
+
       } else if (expr is DisplayExpression) {
         DisplayExpression e = (DisplayExpression)expr;
         wr.Write(e is SetDisplayExpr ? "{" : "[");
         PrintExpressionList(e.Elements);
         wr.Write(e is SetDisplayExpr ? "}" : "]");
-        
+
       } else if (expr is FieldSelectExpr) {
         FieldSelectExpr e = (FieldSelectExpr)expr;
         // determine if parens are needed
@@ -799,7 +799,7 @@ namespace Microsoft.Dafny {
         bool parensNeeded = !(e.Obj is ImplicitThisExpr) &&
           opBindingStrength < contextBindingStrength ||
           (fragileContext && opBindingStrength == contextBindingStrength);
-        
+
         if (parensNeeded) { wr.Write("("); }
         if (!(e.Obj is ImplicitThisExpr)) {
           PrintExpr(e.Obj, opBindingStrength, false, false, -1);
@@ -814,7 +814,7 @@ namespace Microsoft.Dafny {
         int opBindingStrength = 0x70;
         bool parensNeeded = opBindingStrength < contextBindingStrength ||
           (fragileContext && opBindingStrength == contextBindingStrength);
-        
+
         if (parensNeeded) { wr.Write("("); }
         PrintExpr(e.Seq, 0x00, false, false, indent);  // BOGUS: fix me
         wr.Write("[");
@@ -858,7 +858,7 @@ namespace Microsoft.Dafny {
         int opBindingStrength = 0x70;
         bool parensNeeded = opBindingStrength < contextBindingStrength ||
           (fragileContext && opBindingStrength == contextBindingStrength);
-        
+
         if (parensNeeded) { wr.Write("("); }
         PrintExpr(e.Seq, 00, false, false, indent);  // BOGUS: fix me
         wr.Write("[");
@@ -867,7 +867,7 @@ namespace Microsoft.Dafny {
         PrintExpression(e.Value);
         wr.Write("]");
         if (parensNeeded) { wr.Write(")"); }
-      
+
       } else if (expr is FunctionCallExpr) {
         FunctionCallExpr e = (FunctionCallExpr)expr;
         // determine if parens are needed
@@ -875,7 +875,7 @@ namespace Microsoft.Dafny {
         bool parensNeeded = !(e.Receiver is ImplicitThisExpr) &&
           opBindingStrength < contextBindingStrength ||
           (fragileContext && opBindingStrength == contextBindingStrength);
-        
+
         if (parensNeeded) { wr.Write("("); }
         if (!(e.Receiver is ImplicitThisExpr)) {
           PrintExpr(e.Receiver, opBindingStrength, false, false, -1);
@@ -886,12 +886,12 @@ namespace Microsoft.Dafny {
         PrintExpressionList(e.Args);
         wr.Write(")");
         if (parensNeeded) { wr.Write(")"); }
-      
+
       } else if (expr is OldExpr) {
         wr.Write("old(");
         PrintExpression(((OldExpr)expr).E);
         wr.Write(")");
-      
+
       } else if (expr is FreshExpr) {
         wr.Write("fresh(");
         PrintExpression(((FreshExpr)expr).E);
@@ -929,14 +929,14 @@ namespace Microsoft.Dafny {
           PrintExpr(e.E, opBindingStrength, false, parensNeeded || isRightmost, -1);
           if (parensNeeded) { wr.Write(")"); }
         }
-      
+
       } else if (expr is BinaryExpr) {
         BinaryExpr e = (BinaryExpr)expr;
         // determine if parens are needed
         int opBindingStrength;
         bool fragileLeftContext = false;  // false means "allow same binding power on left without parens"
         bool fragileRightContext = false;  // false means "allow same binding power on right without parens"
-        switch (e.Op) 
+        switch (e.Op)
         {
           case BinaryExpr.Opcode.Add:
             opBindingStrength = 0x40; break;
@@ -1064,7 +1064,7 @@ namespace Microsoft.Dafny {
 
       } else if (expr is WildcardExpr) {
         wr.Write("*");
-        
+
       } else if (expr is ITEExpr) {
         ITEExpr ite = (ITEExpr)expr;
         bool parensNeeded = !isRightmost;
@@ -1076,7 +1076,7 @@ namespace Microsoft.Dafny {
         wr.Write(" else ");
         PrintExpression(ite.Els);
         if (parensNeeded) { wr.Write(")"); }
-        
+
       } else if (expr is ParensExpression) {
         var e = (ParensExpression)expr;
         // printing of parentheses is done optimally, not according to the parentheses in the given program
@@ -1094,24 +1094,24 @@ namespace Microsoft.Dafny {
           PrintExpressionList(e.Arguments);
           wr.Write(")");
         }
-        
+
       } else if (expr is MatchExpr) {
         Contract.Assert(false); throw new cce.UnreachableException();  // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression
       }
     }
-    
+
     void PrintTriggers(Triggers trigs) {
       if (trigs != null) {
         PrintTriggers(trigs.Prev);
-        
+
         wr.Write("{ ");
         PrintExpressionList(trigs.Terms);
         wr.Write(" } ");
       }
     }
-    
+
     void PrintExpressionList(List<Expression> exprs) {
       Contract.Requires(exprs != null);
       string sep = "";
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 197a603e..8ec5d4c1 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -67,7 +67,7 @@ namespace Microsoft.Dafny {
     }
 
     bool checkRefinements = true; // used to indicate a cycle in refinements
-      
+
     public void ResolveProgram(Program prog) {
       Contract.Requires(prog != null);
       // register modules
@@ -119,15 +119,15 @@ namespace Microsoft.Dafny {
         }
       }
 
-      // resolve top-level declarations of refinements      
-      foreach (ModuleDecl m in prog.Modules) 
-        foreach (TopLevelDecl decl in m.TopLevelDecls) 
+      // resolve top-level declarations of refinements
+      foreach (ModuleDecl m in prog.Modules)
+        foreach (TopLevelDecl decl in m.TopLevelDecls)
           if (decl is ClassRefinementDecl) {
             ClassRefinementDecl rdecl = (ClassRefinementDecl) decl;
             ResolveTopLevelRefinement(rdecl);
             if (rdecl.Refined != null) refines.AddEdge(rdecl, rdecl.Refined);
           }
-      
+
       // attempt finding refinement cycles
       List<TopLevelDecl> refinesCycle = refines.TryFindCycle();
       if (refinesCycle != null) {
@@ -139,8 +139,8 @@ namespace Microsoft.Dafny {
         }
         Error(refinesCycle[0], "Detected a cyclic refinement declaration: {0}", cy);
         checkRefinements = false;
-      } 
-      
+      }
+
       // resolve top-level declarations
       Graph<DatatypeDecl> datatypeDependencies = new Graph<DatatypeDecl>();
       foreach (ModuleDecl m in prog.Modules) {
@@ -168,7 +168,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     public void RegisterTopLevelDecls(List<TopLevelDecl> declarations) {
       Contract.Requires(declarations != null);
       foreach (TopLevelDecl d in declarations) {
@@ -209,7 +209,7 @@ namespace Microsoft.Dafny {
           // ... and of the other members
           Dictionary<string, MemberDecl> members = new Dictionary<string, MemberDecl>();
           datatypeMembers.Add(dt, members);
-        
+
           foreach (DatatypeCtor ctor in dt.Ctors) {
             if (ctor.Name.EndsWith("?")) {
               Error(ctor, "a datatype constructor name is not allowed to end with '?'");
@@ -224,7 +224,7 @@ namespace Microsoft.Dafny {
               query.EnclosingClass = dt;  // resolve here
               members.Add(queryName, query);
               ctor.QueryField = query;
-                
+
               // also register the constructor name globally
               Tuple<DatatypeCtor, bool> pair;
               if (allDatatypeCtors.TryGetValue(ctor.Name, out pair)) {
@@ -268,9 +268,9 @@ namespace Microsoft.Dafny {
         }
         decl.Refined = cce.NonNull((ClassDecl) a);
         // TODO: copy over remaining members of a
-      }        
-    }  
-      
+      }
+    }
+
     public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
       Contract.Requires(declarations != null);
       Contract.Requires(cce.NonNullElements(datatypeDependencies));
@@ -286,7 +286,7 @@ namespace Microsoft.Dafny {
         allTypeParameters.PopMarker();
       }
     }
-    
+
     public void ResolveTopLevelDecls_Meat(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
       Contract.Requires(declarations != null);
       Contract.Requires(cce.NonNullElements(datatypeDependencies));
@@ -306,7 +306,7 @@ namespace Microsoft.Dafny {
         allTypeParameters.PopMarker();
       }
     }
-    
+
     ClassDecl currentClass;
     Function currentFunction;
     readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();
@@ -314,7 +314,7 @@ namespace Microsoft.Dafny {
     readonly Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();
     readonly List<Statement> loopStack = new List<Statement>();  // the enclosing loops (from which it is possible to break out)
     readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>();  // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"
-    
+
     /// <summary>
     /// Assumes type parameters have already been pushed
     /// </summary>
@@ -323,13 +323,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(cl != null);
       Contract.Requires(currentClass == null);
       Contract.Ensures(currentClass == null);
-    
+
       currentClass = cl;
       foreach (MemberDecl member in cl.Members) {
         member.EnclosingClass = cl;
         if (member is Field) {
           ResolveType(member.tok, ((Field)member).Type);
-          
+
         } else if (member is Function) {
           Function f = (Function)member;
           allTypeParameters.PushMarker();
@@ -343,15 +343,15 @@ namespace Microsoft.Dafny {
           ResolveTypeParameters(m.TypeArgs, true, m);
           ResolveMethodSignature(m);
           allTypeParameters.PopMarker();
-          
+
         } else if (member is CouplingInvariant) {
           CouplingInvariant inv = (CouplingInvariant)member;
-          if (currentClass is ClassRefinementDecl) {      
+          if (currentClass is ClassRefinementDecl) {
             ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
             if (refined != null) {
               Contract.Assert(classMembers.ContainsKey(refined));
               Dictionary<string,MemberDecl> members = classMembers[refined];
-            
+
               // resolve abstracted fields in the refined class
               List<Field> fields = new List<Field>();
               foreach (IToken tok in inv.Toks) {
@@ -359,29 +359,29 @@ namespace Microsoft.Dafny {
                   Error(tok, "Refined class does not declare a field: {0}", tok.val);
                 else {
                   MemberDecl field = members[tok.val];
-                  if (!(field is Field)) 
+                  if (!(field is Field))
                     Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);
                   else if (fields.Contains(cce.NonNull((Field)field)))
                     Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);
                   else
                     fields.Add(cce.NonNull((Field)field));
-                }                  
-              }            
+                }
+              }
               inv.Refined = fields;
             }
-            
+
           } else {
             Error(member, "Coupling invariants can only be declared in refinement classes");
           }
         } else {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member type
         }
-        
-        if (currentClass is ClassRefinementDecl) {          
+
+        if (currentClass is ClassRefinementDecl) {
           ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
           if (refined != null) {
             Contract.Assert(classMembers.ContainsKey(refined));
-          
+
             // there is a member with the same name in refined class if and only if the member is a refined method
             if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))
               Error(member, "Refined class has a member with the same name as in the refinement class: {0}", member.Name);
@@ -399,14 +399,14 @@ namespace Microsoft.Dafny {
       Contract.Requires(cl != null);
       Contract.Requires(currentClass == null);
       Contract.Ensures(currentClass == null);
-    
+
       ResolveAttributes(cl.Attributes, false);
       currentClass = cl;
       foreach (MemberDecl member in cl.Members) {
         ResolveAttributes(member.Attributes, false);
         if (member is Field) {
           // nothing more to do
-          
+
         } else if (member is Function) {
           Function f = (Function)member;
           allTypeParameters.PushMarker();
@@ -420,13 +420,13 @@ namespace Microsoft.Dafny {
           ResolveTypeParameters(m.TypeArgs, false, m);
           ResolveMethod(m);
           allTypeParameters.PopMarker();
-          
+
           // check if signature of the refined method matches the refinement method
           if (member is MethodRefinement) {
             MethodRefinement mf = (MethodRefinement)member;
             if (currentClass is ClassRefinementDecl) {
               // should have already been resolved
-              if (((ClassRefinementDecl)currentClass).Refined != null) { 
+              if (((ClassRefinementDecl)currentClass).Refined != null) {
                 MemberDecl d = classMembers[((ClassRefinementDecl)currentClass).Refined][mf.Name];
                 if (d is Method) {
                   mf.Refined = (Method)d;
@@ -434,18 +434,18 @@ namespace Microsoft.Dafny {
                     Error(mf, "Different number of input variables");
                   if (mf.Outs.Count != mf.Refined.Outs.Count)
                     Error(mf, "Different number of output variables");
-                  if (mf.IsStatic || mf.Refined.IsStatic) 
+                  if (mf.IsStatic || mf.Refined.IsStatic)
                     Error(mf, "Refined methods cannot be static");
                 } else {
                   Error(member, "Refined class has a non-method member with the same name: {0}", member.Name);
-                }            
+                }
               }
             } else {
               Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);
             }
           }
-        
-        } else if (member is CouplingInvariant) {        
+
+        } else if (member is CouplingInvariant) {
           CouplingInvariant inv = (CouplingInvariant)member;
           if (inv.Refined != null) {
             inv.Formals = new List<Formal>();
@@ -460,7 +460,7 @@ namespace Microsoft.Dafny {
             }
             ResolveExpression(inv.Expr, false);
             scope.PopMarker();
-          }                
+          }
         } else {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member type
         }
@@ -476,13 +476,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(dt != null);
       Contract.Requires(cce.NonNullElements(dependencies));
       foreach (DatatypeCtor ctor in dt.Ctors) {
-        
+
         ctor.EnclosingDatatype = dt;
 
         allTypeParameters.PushMarker();
         ResolveCtorSignature(ctor);
         allTypeParameters.PopMarker();
-        
+
         foreach (Formal p in ctor.Formals) {
           DatatypeDecl dependee = p.Type.AsDatatype;
           if (dependee != null) {
@@ -497,7 +497,7 @@ namespace Microsoft.Dafny {
     /// datatype has some value that can be constructed from datatypes in lower stratospheres only.
     /// The algorithm used here is quadratic in the number of datatypes in the SCC.  Since that number is
     /// deemed to be rather small, this seems okay.
-    /// </summary>    
+    /// </summary>
     void SccStratosphereCheck(DatatypeDecl startingPoint, Graph<DatatypeDecl/*!*/>/*!*/ dependencies)
     {
       Contract.Requires(startingPoint != null);
@@ -573,7 +573,7 @@ namespace Microsoft.Dafny {
         ResolveAttributeArgs(attrs.Args, twoState);
       }
     }
-        
+
     void ResolveAttributeArgs(List<Attributes.Argument/*!*/>/*!*/ args, bool twoState) {
       Contract.Requires(args != null);
       foreach (Attributes.Argument aa in args) {
@@ -583,7 +583,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-        
+
     void ResolveTriggers(Triggers trigs, bool twoState) {
       // order does not matter for resolution, so resolve them in reverse order
       for (; trigs != null; trigs = trigs.Prev) {
@@ -592,9 +592,9 @@ namespace Microsoft.Dafny {
         }
       }
     }
-        
+
     void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) {
-      
+
       Contract.Requires(tparams != null);
       Contract.Requires(parent != null);
       // push type arguments of the refined class
@@ -603,7 +603,7 @@ namespace Microsoft.Dafny {
         if (refined != null)
           ResolveTypeParameters(refined.TypeArgs, false, refined);
       }
-    
+
       // push non-duplicated type parameter names
       foreach (TypeParameter tp in tparams) {
         Contract.Assert(tp != null);
@@ -616,7 +616,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     /// <summary>
     /// Assumes type parameters have already been pushed
     /// </summary>
@@ -683,7 +683,7 @@ namespace Microsoft.Dafny {
       currentFunction = null;
       scope.PopMarker();
     }
-    
+
     void ResolveFrameExpression(FrameExpression fe, string kind) {
       Contract.Requires(fe != null);
       Contract.Requires(kind != null);
@@ -717,7 +717,7 @@ namespace Microsoft.Dafny {
         Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type);
       }
     }
-    
+
     /// <summary>
     /// Assumes type parameters have already been pushed
     /// </summary>
@@ -740,7 +740,7 @@ namespace Microsoft.Dafny {
       }
       scope.PopMarker();
     }
-    
+
     /// <summary>
     /// Assumes type parameters have already been pushed
     /// </summary>
@@ -754,7 +754,7 @@ namespace Microsoft.Dafny {
       foreach (Formal p in m.Ins) {
         scope.Push(p.Name, p);
       }
-      
+
       // Start resolving specification...
       foreach (MaybeFreeExpression e in m.Req) {
         ResolveExpression(e.E, false);
@@ -770,7 +770,7 @@ namespace Microsoft.Dafny {
         ResolveExpression(e, false);
         // any type is fine
       }
-      
+
       // Add out-parameters to a new scope that will also include the outermost-level locals of the body
       // Don't care about any duplication errors among the out-parameters, since they have already been reported
       scope.PushMarker();
@@ -786,16 +786,16 @@ namespace Microsoft.Dafny {
           Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
         }
       }
-      
+
       // Resolve body
       if (m.Body != null) {
         ResolveBlockStatement(m.Body, m.IsGhost, m);
       }
-      
+
       scope.PopMarker();  // for the out-parameters and outermost-level locals
       scope.PopMarker();  // for the in-parameters
     }
-    
+
     void ResolveCtorSignature(DatatypeCtor ctor) {
       Contract.Requires(ctor != null);
       foreach (Formal p in ctor.Formals) {
@@ -839,18 +839,18 @@ namespace Microsoft.Dafny {
             Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);
           }
         }
-      
+
       } else if (type is TypeProxy) {
         TypeProxy t = (TypeProxy)type;
         if (t.T != null) {
           ResolveType(tok, t.T);
         }
-        
+
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type
       }
     }
-    
+
     public bool UnifyTypes(Type a, Type b) {
       Contract.Requires(a != null);
       Contract.Requires(b != null);
@@ -866,7 +866,7 @@ namespace Microsoft.Dafny {
           a = proxy.T;
         }
       }
-      
+
       while (b is TypeProxy) {
         TypeProxy proxy = (TypeProxy)b;
         if (proxy.T == null) {
@@ -876,7 +876,7 @@ namespace Microsoft.Dafny {
           b = proxy.T;
         }
       }
-      
+
 #if !NO_CHEAP_OBJECT_WORKAROUND
       if (a is ObjectType || b is ObjectType) {  // TODO: remove this temporary hack
         var other = a is ObjectType ? b : a;
@@ -888,7 +888,7 @@ namespace Microsoft.Dafny {
       }
 #endif
       // Now, a and b are non-proxies and stand for the same things as the original a and b, respectively.
-      
+
       if (a is BoolType) {
         return b is BoolType;
       } else if (a is IntType) {
@@ -923,12 +923,12 @@ namespace Microsoft.Dafny {
           // something is wrong; either aa or bb wasn't properly resolved, or they don't unify
           return false;
         }
-        
+
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type
       }
     }
-    
+
     bool AssignProxy(TypeProxy proxy, Type t){
       Contract.Requires(proxy != null);
       Contract.Requires(t != null);
@@ -939,15 +939,15 @@ namespace Microsoft.Dafny {
       if (proxy == t) {
         // they are already in the same equivalence class
         return true;
-      
+
       } else if (proxy is UnrestrictedTypeProxy) {
         // it's fine to redirect proxy to t (done below)
-        
+
       } else if (t is UnrestrictedTypeProxy) {
           // merge proxy and t by redirecting t to proxy, rather than the other way around
           ((TypeProxy)t).T = proxy;
           return true;
-      
+
       } else if (t is RestrictedTypeProxy) {
         // Both proxy and t are restricted type proxies.  To simplify unification, order proxy and t
         // according to their types.
@@ -958,7 +958,7 @@ namespace Microsoft.Dafny {
         } else {
           return AssignRestrictedProxies(r1, r0);
         }
-      
+
       // In the remaining cases, proxy is a restricted proxy and t is a non-proxy
       } else if (proxy is DatatypeProxy) {
         if (t.IsDatatype) {
@@ -966,14 +966,14 @@ namespace Microsoft.Dafny {
         } else {
           return false;
         }
-      
+
       } else if (proxy is ObjectTypeProxy) {
         if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {
           // all is fine, proxy can be redirected to t
         } else {
           return false;
         }
-      
+
       } else if (proxy is ObjectsTypeProxy) {
         if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {
           // all is good
@@ -981,7 +981,7 @@ namespace Microsoft.Dafny {
           proxy.T = new CollectionTypeProxy(new ObjectTypeProxy());
           return UnifyTypes(proxy.T, t);
         }
-        
+
       } else if (proxy is CollectionTypeProxy) {
         CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy;
         if (t is CollectionType) {
@@ -991,7 +991,7 @@ namespace Microsoft.Dafny {
         } else {
           return false;
         }
-      
+
       } else if (proxy is OperationTypeProxy) {
         OperationTypeProxy opProxy = (OperationTypeProxy)proxy;
         if (t is IntType || t is SetType || (opProxy.AllowSeq && t is SeqType)) {
@@ -1014,11 +1014,11 @@ namespace Microsoft.Dafny {
         } else {
           return false;
         }
-                
+
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected proxy type
       }
-      
+
       // do the merge, but never infer a subrange type
       if (t is NatType) {
         proxy.T = Type.Int;
@@ -1027,7 +1027,7 @@ namespace Microsoft.Dafny {
       }
       return true;
     }
-    
+
     bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b)
     { Contract.Requires(a != null);
       Contract.Requires(b != null);
@@ -1036,7 +1036,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(a.OrderID <= b.OrderID);
       //modifies a.T, b.T;
       Contract.Ensures(Contract.Result<bool>() || a.T != null || b.T != null);
-    
+
       if (a is DatatypeProxy) {
         if (b is DatatypeProxy) {
           // all is fine
@@ -1062,7 +1062,7 @@ namespace Microsoft.Dafny {
         } else {
           return false;
         }
-        
+
       } else if (a is ObjectsTypeProxy) {
         if (b is ObjectsTypeProxy) {
           // fine
@@ -1093,7 +1093,7 @@ namespace Microsoft.Dafny {
         } else {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected restricted-proxy type
         }
-          
+
       } else if (a is CollectionTypeProxy) {
         if (b is CollectionTypeProxy) {
           a.T = b;
@@ -1117,7 +1117,7 @@ namespace Microsoft.Dafny {
         } else {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected restricted-proxy type
         }
-        
+
       } else if (a is OperationTypeProxy) {
         OperationTypeProxy pa = (OperationTypeProxy)a;
         if (b is OperationTypeProxy) {
@@ -1138,12 +1138,12 @@ namespace Microsoft.Dafny {
             return false;
           }
         }
-        
+
       } else if (a is IndexableTypeProxy) {
         Contract.Assert(b is IndexableTypeProxy);  // else we have unexpected restricted-proxy type
         a.T = b;
         return UnifyTypes(((IndexableTypeProxy)a).Arg, ((IndexableTypeProxy)b).Arg);
-        
+
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected restricted-proxy type
       }
@@ -1164,14 +1164,14 @@ namespace Microsoft.Dafny {
         if (!UnifyTypes(s.Expr.Type, Type.Bool)) {
           Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);
         }
-      
+
       } else if (stmt is PrintStmt) {
         PrintStmt s = (PrintStmt)stmt;
         ResolveAttributeArgs(s.Args, false);
         if (specContextOnly) {
           Error(stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
         }
-          
+
       } else if (stmt is BreakStmt) {
         var s = (BreakStmt)stmt;
         if (s.TargetLabel != null) {
@@ -1322,7 +1322,7 @@ namespace Microsoft.Dafny {
         } else {
           Error(stmt, "LHS of assignment must denote a mutable variable or field");
         }
-        
+
         s.IsGhost = lvalueIsGhost;
         Type lhsType = s.Lhs.Type;
         if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {
@@ -1362,7 +1362,7 @@ namespace Microsoft.Dafny {
         } else {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS
         }
-        
+
       } else if (stmt is VarDecl) {
         VarDecl s = (VarDecl)stmt;
         if (s.OptionalType != null) {
@@ -1377,16 +1377,16 @@ namespace Microsoft.Dafny {
           // a local variable in a specification-only context might as well be ghost
           s.IsGhost = true;
         }
-      
+
       } else if (stmt is CallStmt) {
         CallStmt s = (CallStmt)stmt;
         ResolveCallStmt(s, specContextOnly, method, null);
-        
+
       } else if (stmt is BlockStmt) {
         scope.PushMarker();
         ResolveBlockStatement((BlockStmt)stmt, specContextOnly, method);
         scope.PopMarker();
-      
+
       } else if (stmt is IfStmt) {
         IfStmt s = (IfStmt)stmt;
         bool branchesAreSpecOnly = specContextOnly;
@@ -1480,20 +1480,20 @@ namespace Microsoft.Dafny {
         if (!UnifyTypes(s.Collection.Type, new CollectionTypeProxy(s.BoundVar.Type))) {
           Error(s.Collection, "The type is expected to be a collection of {0} (instead got {1})", s.BoundVar.Type, s.Collection.Type);
         }
-        
+
         scope.PushMarker();
         bool b = scope.Push(s.BoundVar.Name, s.BoundVar);
         Contract.Assert(b);  // since we just pushed a marker, we expect the Push to succeed
         ResolveType(s.BoundVar.tok, s.BoundVar.Type);
         int prevErrorCount = ErrorCount;
-        
+
         ResolveExpression(s.Range, true);
         Contract.Assert(s.Range.Type != null);  // follows from postcondition of ResolveExpression
         if (!UnifyTypes(s.Range.Type, Type.Bool)) {
           Error(s.Range, "range condition is expected to be of type {0}, but is {1}", Type.Bool, s.Range.Type);
         }
         bool successfullyResolvedCollectionAndRange = ErrorCount == prevErrorCount;
-        
+
         foreach (PredicateStmt ss in s.BodyPrefix) {
           ResolveStatement(ss, specContextOnly, method);
         }
@@ -1527,7 +1527,7 @@ namespace Microsoft.Dafny {
         }
 
         scope.PopMarker();
-      
+
       } else if (stmt is MatchStmt) {
         MatchStmt s = (MatchStmt)stmt;
         bool bodyIsSpecOnly = specContextOnly;
@@ -1553,14 +1553,14 @@ namespace Microsoft.Dafny {
           Contract.Assert(sourceType != null);  // dtd and sourceType are set together above
           ctors = datatypeCtors[dtd];
           Contract.Assert(ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage
-          
+
           // build the type-parameter substitution map for this use of the datatype
           for (int i = 0; i < dtd.TypeArgs.Count; i++) {
             subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
           }
         }
         s.IsGhost = bodyIsSpecOnly;
-        
+
         Dictionary<string,object> memberNamesUsed = new Dictionary<string,object>();  // this is really a set
         foreach (MatchCaseStmt mc in s.Cases) {
           DatatypeCtor ctor = null;
@@ -1615,8 +1615,8 @@ namespace Microsoft.Dafny {
           }
           Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);
         }
-        
-        
+
+
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();
       }
@@ -2183,7 +2183,7 @@ namespace Microsoft.Dafny {
     }
 
     /// <summary>
-    /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression; 
+    /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression;
     /// if null, no "match" expression will be allowed.
     /// </summary>
     void ResolveExpression(Expression expr, bool twoState, List<IVariable> matchVarContext) {
@@ -2194,7 +2194,7 @@ namespace Microsoft.Dafny {
         // expression has already been resovled
         return;
       }
-      
+
       // The following cases will resolve the subexpressions and will attempt to assign a type of expr.  However, if errors occur
       // and it cannot be determined what the type of expr is, then it is fine to leave expr.Type as null.  In that case, the end
       // of this method will assign proxy type to the expression, which reduces the number of error messages that are produced
@@ -2227,13 +2227,13 @@ namespace Microsoft.Dafny {
         } else {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected literal type
         }
-        
+
       } else if (expr is ThisExpr) {
         if (!scope.AllowInstance) {
           Error(expr, "'this' is not allowed in a 'static' context");
         }
         expr.Type = GetThisType(expr.tok, currentClass);  // do this regardless of scope.AllowInstance, for better error reporting
-        
+
       } else if (expr is IdentifierExpr) {
         IdentifierExpr e = (IdentifierExpr)expr;
         e.Var = scope.Find(e.Name);
@@ -2242,7 +2242,7 @@ namespace Microsoft.Dafny {
         } else {
           expr.Type = e.Var.Type;
         }
-      
+
       } else if (expr is DatatypeValue) {
         DatatypeValue dtv = (DatatypeValue)expr;
         TopLevelDecl d;
@@ -2263,7 +2263,7 @@ namespace Microsoft.Dafny {
           }
           expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt);
           ResolveType(expr.tok, expr.Type);
-          
+
           DatatypeCtor ctor;
           if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {
             Error(expr.tok, "undeclared constructor {0} in datatype {1}", dtv.MemberName, dtv.DatatypeName);
@@ -2288,7 +2288,7 @@ namespace Microsoft.Dafny {
             j++;
           }
         }
-        
+
       } else if (expr is DisplayExpression) {
         DisplayExpression e = (DisplayExpression)expr;
         Type elementType = new InferredTypeProxy();
@@ -2304,7 +2304,7 @@ namespace Microsoft.Dafny {
         } else {
           expr.Type = new SeqType(elementType);
         }
-        
+
       } else if (expr is FieldSelectExpr) {
         var e = (FieldSelectExpr)expr;
         ResolveExpression(e.Obj, twoState);
@@ -2331,7 +2331,7 @@ namespace Microsoft.Dafny {
           }
           e.Type = SubstType(e.Field.Type, subst);
         }
-      
+
       } else if (expr is SeqSelectExpr) {
         SeqSelectExpr e = (SeqSelectExpr)expr;
         ResolveSeqSelectExpr(e, twoState, false);
@@ -2380,11 +2380,11 @@ namespace Microsoft.Dafny {
         if (!seqErr) {
           expr.Type = e.Seq.Type;
         }
-        
+
       } else if (expr is FunctionCallExpr) {
         FunctionCallExpr e = (FunctionCallExpr)expr;
         ResolveFunctionCallExpr(e, twoState, false);
-        
+
       } else if (expr is OldExpr) {
         OldExpr e = (OldExpr)expr;
         if (!twoState) {
@@ -2392,7 +2392,7 @@ namespace Microsoft.Dafny {
         }
         ResolveExpression(e.E, twoState);
         expr.Type = e.E.Type;
-        
+
       } else if (expr is FreshExpr) {
         FreshExpr e = (FreshExpr)expr;
         if (!twoState) {
@@ -2447,7 +2447,7 @@ namespace Microsoft.Dafny {
           default:
             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected unary operator
         }
-        
+
       } else if (expr is BinaryExpr) {
         BinaryExpr e = (BinaryExpr)expr;
         ResolveExpression(e.E0, twoState);
@@ -2467,7 +2467,7 @@ namespace Microsoft.Dafny {
             }
             expr.Type = Type.Bool;
             break;
-          
+
           case BinaryExpr.Opcode.Eq:
           case BinaryExpr.Opcode.Neq:
             if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
@@ -2475,7 +2475,7 @@ namespace Microsoft.Dafny {
             }
             expr.Type = Type.Bool;
             break;
-          
+
           case BinaryExpr.Opcode.Disjoint:
             if (!UnifyTypes(e.E0.Type, new SetType(new InferredTypeProxy()))) {
               Error(expr, "arguments must be of a set type (got {0})", e.E0.Type);
@@ -2485,7 +2485,7 @@ namespace Microsoft.Dafny {
             }
             expr.Type = Type.Bool;
             break;
-          
+
           case BinaryExpr.Opcode.Lt:
           case BinaryExpr.Opcode.Le:
           case BinaryExpr.Opcode.Add:
@@ -2513,7 +2513,7 @@ namespace Microsoft.Dafny {
               }
             }
             break;
-          
+
           case BinaryExpr.Opcode.Sub:
           case BinaryExpr.Opcode.Mul:
           case BinaryExpr.Opcode.Gt:
@@ -2550,7 +2550,7 @@ namespace Microsoft.Dafny {
             }
             expr.Type = Type.Bool;
             break;
-            
+
           case BinaryExpr.Opcode.Div:
           case BinaryExpr.Opcode.Mod:
             if (!UnifyTypes(e.E0.Type, Type.Int)) {
@@ -2561,12 +2561,12 @@ namespace Microsoft.Dafny {
             }
             expr.Type = Type.Int;
             break;
-          
+
           default:
             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected operator
         }
         e.ResolvedOp = ResolveOp(e.Op, e.E1.Type);
-        
+
       } else if (expr is QuantifierExpr) {
         QuantifierExpr e = (QuantifierExpr)expr;
         int prevErrorCount = ErrorCount;
@@ -2639,7 +2639,7 @@ namespace Microsoft.Dafny {
 
       } else if (expr is WildcardExpr) {
         expr.Type = new SetType(new ObjectType());
-        
+
       } else if (expr is ITEExpr) {
         ITEExpr e = (ITEExpr)expr;
         ResolveExpression(e.Test, twoState);
@@ -2656,7 +2656,7 @@ namespace Microsoft.Dafny {
         } else {
           Error(expr, "the two branches of an if-then-else expression must have the same type (got {0} and {1})", e.Thn.Type, e.Els.Type);
         }
-      
+
       } else if (expr is MatchExpr) {
         MatchExpr me = (MatchExpr)expr;
         Contract.Assert(!twoState);  // currently, match expressions are allowed only at the outermost level of function bodies
@@ -2682,7 +2682,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(sourceType != null);  // dtd and sourceType are set together above
           ctors = datatypeCtors[dtd];
           Contract.Assert(ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage
-          
+
           IdentifierExpr ie = me.Source.Resolved as IdentifierExpr;
           if (ie == null || !(ie.Var is Formal || ie.Var is BoundVar)) {
             Error(me.Source.tok, "match source expression must be a formal parameter of the enclosing function or an enclosing match expression");
@@ -2691,13 +2691,13 @@ namespace Microsoft.Dafny {
           } else {
             goodMatchVariable = ie.Var;
           }
-          
+
           // build the type-parameter substitution map for this use of the datatype
           for (int i = 0; i < dtd.TypeArgs.Count; i++) {
             subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
           }
         }
-        
+
         Dictionary<string,object> memberNamesUsed = new Dictionary<string,object>();  // this is really a set
         expr.Type = new InferredTypeProxy();
         foreach (MatchCaseExpr mc in me.Cases) {
@@ -2760,7 +2760,7 @@ namespace Microsoft.Dafny {
           }
           Contract.Assert(memberNamesUsed.Count + me.MissingCases.Count == dtd.Ctors.Count);
         }
-        
+
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression
       }
@@ -3479,13 +3479,13 @@ namespace Microsoft.Dafny {
         return s == null ? new HashSet<IVariable>() : s;
       }
     }
-    
+
     void ResolveReceiver(Expression expr, bool twoState)
     {
       Contract.Requires(expr != null);
       Contract.Requires(currentClass != null);
       Contract.Ensures(expr.Type != null);
-    
+
       if (expr is ThisExpr) {
         // Allow 'this' here, regardless of scope.AllowInstance.  The caller is responsible for
         // making sure 'this' does not really get used when it's not available.
@@ -3494,7 +3494,7 @@ namespace Microsoft.Dafny {
         ResolveExpression(expr, twoState);
       }
     }
-    
+
     void ResolveSeqSelectExpr(SeqSelectExpr e, bool twoState, bool allowNonUnitArraySelection) {
       Contract.Requires(e != null);
       if (e.Type != null) {
@@ -3538,7 +3538,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     /// <summary>
     /// Note: this method is allowed to be called even if "type" does not make sense for "op", as might be the case if
     /// resolution of the binary expression failed.  If so, an arbitrary resolved opcode is returned.
@@ -3647,7 +3647,7 @@ namespace Microsoft.Dafny {
     {
       Contract.Requires(expr != null);
       Contract.Requires(currentClass != null);
-    
+
       if (expr is LiteralExpr) {
         return false;
       } else if (expr is ThisExpr) {
@@ -3723,7 +3723,7 @@ namespace Microsoft.Dafny {
     [Rep] readonly List<string> names = new List<string>();  // a null means a marker
     [Rep] readonly List<Thing> things = new List<Thing>();
     [ContractInvariantMethod]
-    void ObjectInvariant() 
+    void ObjectInvariant()
     {
       Contract.Invariant(names != null);
       Contract.Invariant(things != null);
@@ -3732,7 +3732,7 @@ namespace Microsoft.Dafny {
     }
 
     int scopeSizeWhereInstancesWereDisallowed = -1;
-    
+
     public bool AllowInstance {
       get { return scopeSizeWhereInstancesWereDisallowed == -1; }
       set
@@ -3745,7 +3745,7 @@ namespace Microsoft.Dafny {
       names.Add(null);
       things.Add(null);
     }
-    
+
     public void PopMarker() {
       int n = names.Count;
       while (true) {
@@ -3760,7 +3760,7 @@ namespace Microsoft.Dafny {
         scopeSizeWhereInstancesWereDisallowed = -1;
       }
     }
-    
+
     // Pushes name-->thing association and returns "true", if name has not already been pushed since the last marker.
     // If name already has been pushed since the last marker, does nothing and returns "false".
     public bool Push(string name, Thing thing) {
@@ -3774,7 +3774,7 @@ namespace Microsoft.Dafny {
         return true;
       }
     }
-    
+
     Thing Find(string name, bool topScopeOnly) {
       Contract.Requires(name != null);
       for (int n = names.Count; 0 <= --n; ) {
@@ -3790,7 +3790,7 @@ namespace Microsoft.Dafny {
       }
       return null;  // not present
     }
-    
+
     public Thing Find(string name) {
       Contract.Requires(name != null);
       return Find(name, false);
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 19157a32..37c08ddc 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
 	//    a) whole stream in buffer
 	//    b) part of stream in buffer
 	// 2) non seekable stream (network, console)
-  
+
 	public const int EOF = 65535 + 1; // char.MaxValue + 1;
 	const int MIN_BUFFER_LENGTH = 1024; // 1KB
 	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,15 +31,17 @@ public class Buffer {
 	Stream/*!*/ stream;      // input stream (seekable)
 	bool isUserStream;  // was the stream opened by the user?
 
-[ContractInvariantMethod]
-void ObjectInvariant(){
-  Contract.Invariant(buf != null);
-  Contract.Invariant(stream != null);}
-    [NotDelayed]
-	public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
+	[ContractInvariantMethod]
+	void ObjectInvariant(){
+		Contract.Invariant(buf != null);
+		Contract.Invariant(stream != null);
+	}
+
+//  [NotDelayed]
+	public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
 	  Contract.Requires(s != null);
 		stream = s; this.isUserStream = isUserStream;
-		
+
 		int fl, bl;
 		if (s.CanSeek) {
 			fl = (int) s.Length;
@@ -51,12 +53,12 @@ void ObjectInvariant(){
 
 		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
 		fileLen = fl;  bufLen = bl;
-		
+
 		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
 		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
 		if (bufLen == fileLen && s.CanSeek) Close();
 	}
-	
+
 	protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
 	  Contract.Requires(b != null);
 		buf = b.buf;
@@ -73,14 +75,14 @@ void ObjectInvariant(){
 	}
 
 	~Buffer() { Close(); }
-	
+
 	protected void Close() {
 		if (!isUserStream && stream != null) {
 			stream.Close();
 			//stream = null;
 		}
 	}
-	
+
 	public virtual int Read () {
 		if (bufPos < bufLen) {
 			return buf[bufPos++];
@@ -100,7 +102,7 @@ void ObjectInvariant(){
 		Pos = curPos;
 		return ch;
 	}
-	
+
 	public string/*!*/ GetString (int beg, int end) {
 	  Contract.Ensures(Contract.Result<string>() != null);
 		int len = 0;
@@ -139,7 +141,7 @@ void ObjectInvariant(){
 			}
 		}
 	}
-	
+
 	// Read the next chunk of bytes from the stream, increases the buffer
 	// if needed and updates the fields fileLen and bufLen.
 	// Returns the number of bytes read.
@@ -213,22 +215,24 @@ public class Scanner {
 	const int noSym = 104;
 
 
-[ContractInvariantMethod]
-void objectInvariant(){
-  Contract.Invariant(buffer!=null);
-  Contract.Invariant(t != null);
-  Contract.Invariant(start != null);
-  Contract.Invariant(tokens != null);
-  Contract.Invariant(pt != null);
-  Contract.Invariant(tval != null);
-  Contract.Invariant(Filename != null);
-  Contract.Invariant(errorHandler != null);
-}
+	[ContractInvariantMethod]
+	void objectInvariant(){
+		Contract.Invariant(buffer!=null);
+		Contract.Invariant(t != null);
+		Contract.Invariant(start != null);
+		Contract.Invariant(tokens != null);
+		Contract.Invariant(pt != null);
+		Contract.Invariant(tval != null);
+		Contract.Invariant(Filename != null);
+		Contract.Invariant(errorHandler != null);
+	}
+
 	public Buffer/*!*/ buffer; // scanner buffer
-	
+
 	Token/*!*/ t;          // current token
 	int ch;           // current input character
 	int pos;          // byte position of current character
+	int charPos;
 	int col;          // column number of current character
 	int line;         // line number of current character
 	int oldEols;      // EOLs that appeared in a comment;
@@ -236,13 +240,13 @@ void objectInvariant(){
 
 	Token/*!*/ tokens;     // list of tokens already peeked (first token is a dummy)
 	Token/*!*/ pt;         // current peek token
-	
+
 	char[]/*!*/ tval = new char[128]; // text of current token
 	int tlen;         // length of current token
-	
+
 	private string/*!*/ Filename;
 	private Errors/*!*/ errorHandler;
-	
+
 	static Scanner() {
 		start = new Hashtable(128);
 		for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -290,9 +294,9 @@ void objectInvariant(){
 		start[Buffer.EOF] = -1;
 
 	}
-	
-	[NotDelayed]
-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
+
+//	[NotDelayed]
+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
 	  Contract.Requires(fileName != null);
 	  Contract.Requires(errorHandler != null);
 		this.errorHandler = errorHandler;
@@ -302,15 +306,14 @@ void objectInvariant(){
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
 			buffer = new Buffer(stream, false);
 			Filename = fileName;
-			
 			Init();
 		} catch (IOException) {
 			throw new FatalError("Cannot open file " + fileName);
 		}
 	}
-	
-	[NotDelayed]
-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
+
+//	[NotDelayed]
+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
 	  Contract.Requires(s != null);
 	  Contract.Requires(errorHandler != null);
 	  Contract.Requires(fileName != null);
@@ -319,10 +322,9 @@ void objectInvariant(){
 		buffer = new Buffer(s, true);
 		this.errorHandler = errorHandler;
 		this.Filename = fileName;
-		
 		Init();
 	}
-	
+
 	void Init() {
 		pos = -1; line = 1; col = 0;
 		oldEols = 0;
@@ -343,11 +345,11 @@ void objectInvariant(){
 	Contract.Ensures(Contract.Result<string>() != null);
 	  int p = buffer.Pos;
 	  int ch = buffer.Read();
-      // replace isolated '\r' by '\n' in order to make
+	  // replace isolated '\r' by '\n' in order to make
 	  // eol handling uniform across Windows, Unix and Mac
 	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
 	  while (ch != EOL && ch != Buffer.EOF){
-	    ch = buffer.Read();
+		ch = buffer.Read();
 		// replace isolated '\r' by '\n' in order to make
 		// eol handling uniform across Windows, Unix and Mac
 		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -358,7 +360,7 @@ void objectInvariant(){
 	}
 
 	void NextCh() {
-		if (oldEols > 0) { ch = EOL; oldEols--; } 
+		if (oldEols > 0) { ch = EOL; oldEols--; }
 		else {
 //			pos = buffer.Pos;
 //			ch = buffer.Read(); col++;
@@ -366,9 +368,9 @@ void objectInvariant(){
 //			// eol handling uniform across Windows, Unix and Mac
 //			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
 //			if (ch == EOL) { line++; col = 0; }
-			
+
 			while (true) {
-			    pos = buffer.Pos;
+				pos = buffer.Pos;
 				ch = buffer.Read(); col++;
 				// replace isolated '\r' by '\n' in order to make
 				// eol handling uniform across Windows, Unix and Mac
@@ -418,7 +420,7 @@ void objectInvariant(){
 				return;
 			  }
 
-			
+
 		}
 
 	}
@@ -438,7 +440,7 @@ void objectInvariant(){
 
 
 	bool Comment0() {
-		int level = 1, pos0 = pos, line0 = line, col0 = col;
+		int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos;
 		NextCh();
 		if (ch == '/') {
 			NextCh();
@@ -451,13 +453,13 @@ void objectInvariant(){
 				else NextCh();
 			}
 		} else {
-			buffer.Pos = pos0; NextCh(); line = line0; col = col0;
+			buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0;
 		}
 		return false;
 	}
 
 	bool Comment1() {
-		int level = 1, pos0 = pos, line0 = line, col0 = col;
+		int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos;
 		NextCh();
 		if (ch == '*') {
 			NextCh();
@@ -478,7 +480,7 @@ void objectInvariant(){
 				else NextCh();
 			}
 		} else {
-			buffer.Pos = pos0; NextCh(); line = line0; col = col0;
+			buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0;
 		}
 		return false;
 	}
@@ -555,10 +557,13 @@ void objectInvariant(){
 		t.pos = pos; t.col = col; t.line = line;
 		t.filename = this.Filename;
 		int state;
-		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
+		if (start.ContainsKey(ch)) {
+			Contract.Assert(start[ch] != null);
+			state = (int) start[ch];
+		}
 		else { state = 0; }
 		tlen = 0; AddCh();
-		
+
 		switch (state) {
 			case -1: { t.kind = eofSym; break; } // NextCh already done
 			case 0: {
@@ -764,14 +769,14 @@ void objectInvariant(){
 		t.val = new String(tval, 0, tlen);
 		return t;
 	}
-	
+
 	private void SetScannerBehindT() {
 		buffer.Pos = t.pos;
 		NextCh();
 		line = t.line; col = t.col;
 		for (int i = 0; i < tlen; i++) NextCh();
 	}
-	
+
 	// get the next token (possibly a token already seen during peeking)
 	public Token/*!*/ Scan () {
 	 Contract.Ensures(Contract.Result<Token>() != null);
@@ -792,7 +797,7 @@ void objectInvariant(){
 			}
 			pt = pt.next;
 		} while (pt.kind > maxT); // skip pragmas
-	
+
 		return pt;
 	}
 
diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs
index 9f4b22c5..4ae1c185 100644
--- a/Source/Dafny/SccGraph.cs
+++ b/Source/Dafny/SccGraph.cs
@@ -12,14 +12,14 @@ namespace Microsoft.Dafny {
       public readonly List<Vertex/*!*/>/*!*/ Successors = new List<Vertex/*!*/>();
       public List<Vertex/*!*/> SccMembers;  // non-null only for the representative of the SCC
       [ContractInvariantMethod]
-      void ObjectInvariant() 
+      void ObjectInvariant()
       {
         Contract.Invariant(cce.NonNullElements(Successors));
         Contract.Invariant(SccMembers==null || cce.NonNullElements(SccMembers));
       }
 
       public Vertex SccRepresentative;  // null if not computed
-      
+
       public int SccId;  // valid only for SCC representatives; indicates position of this representative vertex in the graph's topological sort
       // the following field is used during the computation of SCCs and of reachability
       public VisitedStatus Visited;
@@ -28,7 +28,7 @@ namespace Microsoft.Dafny {
       public int LowLink;
       // the following field is used during a Reaches computation
       public int Gen;  // generation <= Gen means this vertex has been visited in the current generation
-      
+
       public Vertex(Node n) {
         N = n;
       }
@@ -40,7 +40,7 @@ namespace Microsoft.Dafny {
 
 
     [ContractInvariantMethod]
-    void ObjectInvariant() 
+    void ObjectInvariant()
     {
       Contract.Invariant(vertices!=null);
       Contract.Invariant(cce.NonNullElements(vertices.Values));
@@ -51,7 +51,7 @@ namespace Microsoft.Dafny {
     Dictionary<Node, Vertex/*!*/>/*!*/ vertices = new Dictionary<Node, Vertex/*!*/>();
     bool sccComputed = false;
     List<Vertex/*!*/> topologicallySortedRepresentatives;  // computed by the SCC computation
-    
+
     public int SccCount {
       get {
         ComputeSCCs();
@@ -60,11 +60,11 @@ namespace Microsoft.Dafny {
       }
     }
     int generation = 0;
-    
+
     public Graph()
     {
     }
-    
+
     /// <summary>
     /// Idempotently adds a vertex 'n' to the graph.
     /// </summary>
@@ -74,7 +74,7 @@ namespace Microsoft.Dafny {
 
     /// <summary>
     /// Idempotently adds a vertex 'n' to the graph and then returns the Vertex for it.
-    /// </summary>    
+    /// </summary>
     Vertex GetVertex(Node n) {
       Contract.Ensures(Contract.Result<Vertex>() != null);
 
@@ -93,7 +93,7 @@ namespace Microsoft.Dafny {
       }
       return v;
     }
-    
+
     /// <summary>
     /// Returns the vertex for 'n' if 'n' is in the graph.  Otherwise, returns null.
     /// </summary>
@@ -117,7 +117,7 @@ namespace Microsoft.Dafny {
       v0.AddSuccessor(v1);
       sccComputed = false;  // the addition of an edge may invalidate any previous computation of the graph's SCCs
     }
-    
+
     /// <summary>
     /// Idempotently adds 'n' as a vertex and then returns a Node that is the representative element of the
     /// strongly connected component containing 'n'.
@@ -125,7 +125,7 @@ namespace Microsoft.Dafny {
     public Node GetSCCRepresentative(Node n) {
       return GetSCCRepr(n).N;
     }
-    
+
     /// <summary>
     /// Idempotently adds 'n' as a vertex.  Then, returns the number of SCCs before the SCC of 'n' in the
     /// topologically sorting of SCCs.
@@ -133,7 +133,7 @@ namespace Microsoft.Dafny {
     public int GetSCCRepresentativeId(Node n) {
       return GetSCCRepr(n).SccId;
     }
-    
+
     Vertex GetSCCRepr(Node n) {
       Contract.Ensures(Contract.Result<Vertex>() != null);
 
@@ -142,7 +142,7 @@ namespace Microsoft.Dafny {
       Contract.Assert(v.SccRepresentative != null);  // follows from what ComputeSCCs does
       return v.SccRepresentative;
     }
-    
+
     /// <summary>
     /// Returns a list of the topologically sorted SCCs, each represented in the list by its representative node.
     /// </summary>
@@ -172,21 +172,21 @@ namespace Microsoft.Dafny {
       }
       return nn;
     }
-    
+
     /// <summary>
     /// Idempotently adds 'n' as a vertex and then returns the size of the set of Node's in the strongly connected component
     /// that contains 'n'.
     /// </summary>
     public int GetSCCSize(Node n){
       Contract.Ensures(1 <= Contract.Result<int>());
-    
+
       Vertex v = GetVertex(n);
       ComputeSCCs();
       Vertex repr = v.SccRepresentative;
       Contract.Assert(repr != null && repr.SccMembers != null);  // follows from postcondition of ComputeSCCs
       return repr.SccMembers.Count;
     }
-    
+
     /// <summary>
     /// This method sets the SccRepresentative fields of the graph's vertices so that two
     /// vertices have the same representative iff they are in the same strongly connected
@@ -197,7 +197,7 @@ namespace Microsoft.Dafny {
     void ComputeSCCs()
     {
       Contract.Ensures(sccComputed);
-    
+
       if (sccComputed) { return; }  // check if already computed
 
       // reset all SCC information
@@ -217,7 +217,7 @@ namespace Microsoft.Dafny {
 
       sccComputed = true;
     }
-    
+
     /// <summary>
     /// This is the 'SearchC' procedure from the Aho, Hopcroft, and Ullman book 'The Design and Analysis of Computer Algorithms'.
     /// </summary>
@@ -227,13 +227,13 @@ namespace Microsoft.Dafny {
      Contract.Requires(v.Visited == VisitedStatus.Unvisited);
      Contract.Requires(topologicallySortedRepresentatives != null);
       Contract.Ensures(v.Visited != VisitedStatus.Unvisited);
-    
+
       v.DfNumber = cnt;
       cnt++;
       v.LowLink = v.DfNumber;
       stack.Push(v);
       v.Visited = VisitedStatus.OnStack;
-      
+
       foreach (Vertex w in v.Successors) {
         if (w.Visited == VisitedStatus.Unvisited) {
           SearchC(w, stack, ref cnt);
@@ -243,7 +243,7 @@ namespace Microsoft.Dafny {
           v.LowLink = Math.Min(v.LowLink, w.DfNumber);
         }
       }
-      
+
       if (v.LowLink == v.DfNumber) {
         // The SCC containing 'v' has now been computed.
         v.SccId = topologicallySortedRepresentatives.Count;
@@ -258,7 +258,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     /// <summary>
     /// Returns null if the graph has no cycles.  If the graph does contain some cycle, returns the list of
     /// vertices on one such cycle.
@@ -268,7 +268,7 @@ namespace Microsoft.Dafny {
       foreach (Vertex v in vertices.Values) {
         v.Visited = VisitedStatus.Unvisited;
       }
-      
+
       foreach (Vertex v in vertices.Values) {
         Contract.Assert(v.Visited != VisitedStatus.OnStack);
         if (v.Visited == VisitedStatus.Unvisited) {
@@ -284,7 +284,7 @@ namespace Microsoft.Dafny {
       }
       return null;  // there are no cycles
     }
-    
+
     /// <summary>
     /// A return of null means there are no cycles involving any vertex in the subtree rooted at v.
     /// A non-null return means a cycle has been found.  Then:
@@ -300,7 +300,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(v.Visited != VisitedStatus.Unvisited);
       Contract.Ensures(Contract.Result<List<Vertex>>() != null || v.Visited == VisitedStatus.Visited);
       Contract.Ensures(Contract.Result<List<Vertex>>() == null || Contract.Result<List<Vertex>>().Count != 0);
-    
+
       v.Visited = VisitedStatus.OnStack;
       foreach (Vertex succ in v.Successors) {
         // todo:  I would use a 'switch' statement, but there seems to be a bug in the Spec# compiler's type checking.
@@ -337,7 +337,7 @@ namespace Microsoft.Dafny {
       v.Visited = VisitedStatus.Visited;  // there are no cycles from here on
       return null;
     }
-    
+
     /// <summary>
     /// Returns whether or not 'source' reaches 'sink' in the graph.
     /// 'source' and 'sink' need not be in the graph; if neither is, the return value
@@ -352,7 +352,7 @@ namespace Microsoft.Dafny {
       generation++;
       return ReachSearch(a, b);
     }
-    
+
     bool ReachSearch(Vertex source, Vertex sink) {
       Contract.Requires(source != null);
       Contract.Requires(sink != null);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index d1c77122..74d33479 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -21,14 +21,14 @@ namespace Microsoft.Dafny {
         predef = FindPredefinedDecls(boogieProgram);
       }
     }
-    
+
     // translation state
     readonly Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>/*!*/ classes = new Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>();
     readonly Dictionary<Field/*!*/,Bpl.Constant/*!*/>/*!*/ fields = new Dictionary<Field/*!*/,Bpl.Constant/*!*/>();
     readonly Dictionary<Field/*!*/, Bpl.Function/*!*/>/*!*/ fieldFunctions = new Dictionary<Field/*!*/, Bpl.Function/*!*/>();
 
     [ContractInvariantMethod]
-    void ObjectInvariant() 
+    void ObjectInvariant()
     {
       Contract.Invariant(cce.NonNullDictionaryAndValues(classes));
       Contract.Invariant(cce.NonNullDictionaryAndValues(fields));
@@ -77,14 +77,14 @@ namespace Microsoft.Dafny {
 
         return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));
       }
-      
+
       public Bpl.Type SeqType(IToken tok, Bpl.Type ty) {
         Contract.Requires(tok != null);
         Contract.Requires(ty != null);
         Contract.Ensures(Contract.Result<Bpl.Type>() != null);
         return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));
       }
-      
+
       public Bpl.Type FieldName(IToken tok, Bpl.Type ty) {
         Contract.Requires(tok != null);
         Contract.Requires(ty != null);
@@ -92,7 +92,7 @@ namespace Microsoft.Dafny {
 
         return new Bpl.CtorType(tok, fieldName, new Bpl.TypeSeq(ty));
       }
-      
+
       public Bpl.IdentifierExpr Alloc(IToken tok) {
         Contract.Requires(tok != null);
         Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>() != null);
@@ -135,14 +135,14 @@ namespace Microsoft.Dafny {
         this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
       }
     }
-    
+
     static PredefinedDecls FindPredefinedDecls(Bpl.Program prog) {
       Contract.Requires(prog != null);
       if (prog.Resolve() != 0) {
         Console.WriteLine("Error: resolution errors encountered in Dafny prelude");
         return null;
       }
-      
+
       Bpl.TypeCtorDecl refType = null;
       Bpl.TypeSynonymDecl setTypeCtor = null;
       Bpl.TypeCtorDecl seqTypeCtor = null;
@@ -220,7 +220,7 @@ namespace Microsoft.Dafny {
       }
       return null;
     }
-    
+
     static Bpl.Program ReadPrelude() {
       string preludePath = Bpl.CommandLineOptions.Clo.DafnyPrelude;
       if (preludePath == null)
@@ -229,7 +229,7 @@ namespace Microsoft.Dafny {
           string codebase = cce.NonNull(System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
           preludePath = System.IO.Path.Combine(codebase, "DafnyPrelude.bpl");
       }
-      
+
       Bpl.Program prelude;
       int errorCount = Bpl.Parser.Parse(preludePath, null, out prelude);
       if (prelude == null || errorCount > 0) {
@@ -237,7 +237,7 @@ namespace Microsoft.Dafny {
       } else {
         return prelude;
       }
-/*      
+/*
       List<string!> defines = new List<string!>();
       using (System.IO.Stream stream = new System.IO.FileStream(preludePath, System.IO.FileMode.Open, System.IO.FileAccess.Read))
       {
@@ -251,9 +251,9 @@ namespace Microsoft.Dafny {
           return prelude;
         }
       }
-*/      
+*/
     }
-    
+
     public Bpl.Program Translate(Program program) {
       Contract.Requires(program != null);
       Contract.Ensures(Contract.Result<Bpl.Program>() != null);
@@ -282,13 +282,13 @@ namespace Microsoft.Dafny {
       }
       return sink;
     }
-    
+
     void AddDatatype(DatatypeDecl dt)
     {
       Contract.Requires(dt != null);
       Contract.Requires(sink != null && predef != null);
       sink.TopLevelDeclarations.Add(GetClass(dt));
-    
+
       foreach (DatatypeCtor ctor in dt.Ctors) {
         // Add:  function #dt.ctor(paramTypes) returns (DatatypeType);
         Bpl.VariableSeq argTypes = new Bpl.VariableSeq();
@@ -348,7 +348,7 @@ namespace Microsoft.Dafny {
         fn.Body = Bpl.Expr.Eq(lhs, new Bpl.IdentifierExpr(ctor.tok, cid));  // this uses the "cid" defined for the previous axiom
         sink.TopLevelDeclarations.Add(fn);
 
-        // Add:  axiom (forall params, h: HeapType :: 
+        // Add:  axiom (forall params, h: HeapType ::
         //                 { DtAlloc(#dt.ctor(params), h) }
         //                 $IsGoodHeap(h) ==>
         //                     (DtAlloc(#dt.ctor(params), h) <==> ...each param has its expected type...));
@@ -440,7 +440,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     void CreateBoundVariables(List<Formal/*!*/>/*!*/ formals, out Bpl.VariableSeq/*!*/ bvs, out List<Bpl.Expr/*!*/>/*!*/ args)
     {
       Contract.Requires(formals != null);
@@ -459,13 +459,13 @@ namespace Microsoft.Dafny {
         args.Add(new Bpl.IdentifierExpr(arg.tok, bv));
       }
     }
-    
+
     void AddClassMembers(ClassDecl c)
     {
       Contract.Requires(sink != null && predef != null);
       Contract.Requires(c != null);
       sink.TopLevelDeclarations.Add(GetClass(c));
-      
+
       foreach (MemberDecl member in c.Members) {
         if (member is Field) {
           Field f = (Field)member;
@@ -478,7 +478,7 @@ namespace Microsoft.Dafny {
           }
 
           AddAllocationAxiom(f);
-          
+
         } else if (member is Function) {
           Function f = (Function)member;
           AddFunction(f);
@@ -500,7 +500,7 @@ namespace Microsoft.Dafny {
           }
           AddFrameAxiom(f);
           AddWellformednessCheck(f);
-          
+
         } else if (member is Method) {
           Method m = (Method)member;
           // wellformedness check for method specification
@@ -514,14 +514,14 @@ namespace Microsoft.Dafny {
             // ...and its implementation
             AddMethodImpl(m, proc, false);
           }
-          
+
           // refinement condition
           if (member is MethodRefinement) {
             AddMethodRefinement((MethodRefinement)member);
           }
-        
+
         } else if (member is CouplingInvariant) {
-          // TODO: define a well-foundedness condition to check          
+          // TODO: define a well-foundedness condition to check
 
         } else {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member
@@ -616,9 +616,9 @@ namespace Microsoft.Dafny {
       Contract.Requires(layerOffset == 0 || (layerOffset == 1 && f.IsRecursive && !f.IsUnlimited));
       Contract.Requires(predef != null);
       Contract.Requires(f.EnclosingClass != null);
- 
+
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
-      
+
       // axiom
       //   mh < ModuleContextHeight ||
       //   (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext))
@@ -659,7 +659,7 @@ namespace Microsoft.Dafny {
       args.Add(new Bpl.IdentifierExpr(f.tok, bv));
       // ante:  $IsHeap($Heap) && this != null && formals-have-the-expected-types &&
       Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
-      
+
       Bpl.BoundVariable bvThis;
       Bpl.Expr bvThisIdExpr;
       if (f.IsStatic) {
@@ -711,7 +711,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr.Or(
             Bpl.Expr.Le(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()),
             etran.InMethodContext())));
-      
+
       var substMap = new Dictionary<IVariable, Expression>();
       if (specialization != null) {
         substMap = specialization.SubstMap;
@@ -770,7 +770,7 @@ namespace Microsoft.Dafny {
       }
       return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);
     }
-    
+
     void AddLimitedAxioms(Function f, int fromLayer) {
       Contract.Requires(f != null);
       Contract.Requires(f.IsRecursive && !f.IsUnlimited);
@@ -807,7 +807,7 @@ namespace Microsoft.Dafny {
       Bpl.Expr origFuncAppl = new Bpl.NAryExpr(f.tok, origFuncID, args);
       Bpl.FunctionCall limitedFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, fromLayer-1), TrType(f.ResultType)));
       Bpl.Expr limitedFuncAppl = new Bpl.NAryExpr(f.tok, limitedFuncID, args);
-      
+
       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
 
       Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(origFuncAppl));
@@ -833,7 +833,7 @@ namespace Microsoft.Dafny {
       }
       return name;
     }
-    
+
     /// <summary>
     /// Generate:
     ///   axiom (forall h: [ref, Field x]x, o: ref ::
@@ -844,13 +844,13 @@ namespace Microsoft.Dafny {
     {
       Contract.Requires(f != null);
       Contract.Requires(sink != null && predef != null);
-    
+
       Bpl.BoundVariable hVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h", predef.HeapType));
       Bpl.Expr h = new Bpl.IdentifierExpr(f.tok, hVar);
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, h);
       Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));
       Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);
-      
+
       // h[o,f]
       Bpl.Expr oDotF;
       if (f.IsMutable) {
@@ -894,7 +894,7 @@ namespace Microsoft.Dafny {
       }
       return Bpl.Expr.And(lower, upper);
     }
-    
+
     Method currentMethod = null;  // the method whose implementation is currently being translated
     int loopHeapVarCount = 0;
     int otherTmpVarCount = 0;
@@ -927,7 +927,7 @@ namespace Microsoft.Dafny {
 
       return GetTmpVar_IdExpr(tok, "$prevHeap", predef.HeapType, locals);
     }
-    
+
     Bpl.IdentifierExpr GetNewVar_IdExpr(IToken tok, Bpl.VariableSeq locals)  // local variable that's shared between statements that need it
     {
       Contract.Requires(tok != null);
@@ -970,7 +970,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(wellformednessProc || m.Body != null);
       Contract.Requires(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
       Contract.Ensures(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
-    
+
       currentMethod = m;
 
       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
@@ -1032,7 +1032,7 @@ namespace Microsoft.Dafny {
         typeParams, inParams, outParams,
         localVariables, stmts);
       sink.TopLevelDeclarations.Add(impl);
-      
+
       currentMethod = null;
       loopHeapVarCount = 0;
       otherTmpVarCount = 0;
@@ -1047,7 +1047,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);
       Contract.Requires(localVariables != null);
       Contract.Requires(predef != null);
-    
+
       // set up the information used to verify the method's modifies clause
       DefineFrame(m.tok, m.Mod, builder, localVariables, null);
     }
@@ -1064,14 +1064,14 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);
       return CaptureState(tok, null);
     }
-    
+
     void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables, string name){
       Contract.Requires(tok != null);
       Contract.Requires(cce.NonNullElements(frameClause));
       Contract.Requires(builder != null);
       Contract.Requires(cce.NonNullElements(localVariables));
       Contract.Requires(predef != null);
-    
+
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);
       // Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool
       Bpl.IdentifierExpr theFrame = etran.TheFrame(tok);  // this is a throw-away expression, used only to extract the type of the $_Frame variable
@@ -1088,7 +1088,7 @@ namespace Microsoft.Dafny {
       Bpl.Expr consequent = InRWClause(tok, o, f, frameClause, etran, null, null);
       Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null,
                                            Bpl.Expr.Imp(ante, consequent));
-    
+
       builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));
     }
 
@@ -1119,7 +1119,7 @@ namespace Microsoft.Dafny {
                                       Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), inEnclosingFrame));
       builder.Add(Assert(tok, q, errorMessage, kv));
     }
-    
+
     /// <summary>
     /// Generates:
     ///   axiom (forall h0: HeapType, h1: HeapType, formals... ::
@@ -1141,18 +1141,18 @@ namespace Microsoft.Dafny {
     {
       Contract.Requires(f != null);
       Contract.Requires(sink != null && predef != null);
-    
+
       Bpl.BoundVariable h0Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h0", predef.HeapType));
       Bpl.BoundVariable h1Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h1", predef.HeapType));
       Bpl.Expr h0 = new Bpl.IdentifierExpr(f.tok, h0Var);
       Bpl.Expr h1 = new Bpl.IdentifierExpr(f.tok, h1Var);
       ExpressionTranslator etran0 = new ExpressionTranslator(this, predef, h0);
       ExpressionTranslator etran1 = new ExpressionTranslator(this, predef, h1);
-      
+
       Bpl.Expr wellFormed = Bpl.Expr.And(
         FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr),
         FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran1.HeapExpr));
-      
+
       Bpl.TypeVariable alpha = new Bpl.TypeVariable(f.tok, "alpha");
       Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));
       Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);
@@ -1161,12 +1161,12 @@ namespace Microsoft.Dafny {
       Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
       Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o)));
       Bpl.Expr unchanged = Bpl.Expr.Eq(ExpressionTranslator.ReadHeap(f.tok, h0, o, field), ExpressionTranslator.ReadHeap(f.tok, h1, o, field));
-      
+
       Bpl.Expr heapSucc = FunctionCall(f.tok, BuiltinFunction.HeapSucc, null, h0, h1);
       Bpl.Expr r0 = InRWClause(f.tok, o, field, f.Reads, etran0, null, null);
       Bpl.Expr q0 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),
         Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r0), unchanged));
-      
+
       // bvars:  h0, h1, formals
       // f0args:  h0, formals
       // f1args:  h1, formals
@@ -1200,7 +1200,7 @@ namespace Microsoft.Dafny {
         wh = GetWhereClause(p.tok, formal, p.Type, etran1);
         if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }
       }
-      
+
       string axiomComment = "frame axiom for " + f.FullName;
       Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
       while (fn != null) {
@@ -1208,7 +1208,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);
         Bpl.Expr eq = Bpl.Expr.Eq(F0, F1);
         Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(heapSucc, F1));
-        
+
         Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
         Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,
           Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, heapSucc),
@@ -1222,7 +1222,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     Bpl.Expr/*!*/ InRWClause(IToken/*!*/ tok, Bpl.Expr/*!*/ o, Bpl.Expr/*!*/ f, List<FrameExpression/*!*/>/*!*/ rw, ExpressionTranslator/*!*/ etran,
                              Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/> substMap) {
       Contract.Requires(tok != null);
@@ -1237,7 +1237,7 @@ namespace Microsoft.Dafny {
 
       // requires o to denote an expression of type RefType
       // "rw" is is allowed to contain a WildcardExpr
-    
+
       Bpl.Expr disjunction = null;
       foreach (FrameExpression rwComponent in rw) {
         Expression e = rwComponent.E;
@@ -1280,12 +1280,12 @@ namespace Microsoft.Dafny {
         return disjunction;
       }
     }
-    
+
     void AddWellformednessCheck(Function f) {
       Contract.Requires(f != null);
       Contract.Requires(sink != null && predef != null);
       Contract.Requires(f.EnclosingClass != null);
-    
+
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
       // parameters of the procedure
       Bpl.VariableSeq inParams = new Bpl.VariableSeq();
@@ -1317,7 +1317,7 @@ namespace Microsoft.Dafny {
       VariableSeq implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);
       Bpl.VariableSeq locals = new Bpl.VariableSeq();
       Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
-      
+
       // check well-formedness of the preconditions (including termination, but no reads checks), and then
       // assume each one of them
       foreach (Expression p in f.Req) {
@@ -1423,7 +1423,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);Contract.Requires(etran != null);
       Contract.Requires(predef != null);
       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
-    
+
       if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {
         return Bpl.Expr.True;
       } else if (expr is DisplayExpression) {
@@ -1586,7 +1586,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression
       }
     }
-    
+
     Bpl.Expr/*!*/ IsTotal(List<Expression/*!*/>/*!*/ exprs, ExpressionTranslator/*!*/ etran) {
       Contract.Requires(etran != null);
       Contract.Requires(exprs != null);
@@ -1746,7 +1746,7 @@ namespace Microsoft.Dafny {
         return Bpl.Expr.And(a, b);
       }
     }
-    
+
     Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) {
       Contract.Requires(a != null);
       Contract.Requires(b != null);
@@ -1758,14 +1758,14 @@ namespace Microsoft.Dafny {
         return Bpl.Expr.Imp(a, b);
       }
     }
-    
+
     void CheckNonNull(IToken tok, Expression e, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Bpl.QKeyValue kv) {
       Contract.Requires(tok != null);
       Contract.Requires(e != null);
       Contract.Requires(builder != null);
       Contract.Requires(etran != null);
       Contract.Requires(predef != null);
-    
+
       if (e is ThisExpr) {
         // already known to be non-null
       } else {
@@ -1840,7 +1840,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);
       Contract.Requires(etran != null);
       Contract.Requires(predef != null);
-    
+
       if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {
         // always allowed
       } else if (expr is DisplayExpression) {
@@ -2084,7 +2084,7 @@ namespace Microsoft.Dafny {
         CheckWellformed(e.Thn, options, locals, bThen, etran);
         CheckWellformed(e.Els, options, locals, bElse, etran);
         builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.Test), bThen.Collect(expr.tok), null, bElse.Collect(expr.tok)));
-      
+
       } else if (expr is MatchExpr) {
         MatchExpr me = (MatchExpr)expr;
         CheckWellformed(me.Source, options, locals, builder, etran);
@@ -2308,7 +2308,7 @@ namespace Microsoft.Dafny {
         return s;
       }
     }
-    
+
     Bpl.Constant GetClass(TopLevelDecl cl)
     {
       Contract.Requires(cl != null);
@@ -2324,7 +2324,7 @@ namespace Microsoft.Dafny {
       }
       return cc;
     }
-    
+
     Bpl.Expr GetTypeExpr(IToken tok, Type type)
     {
       Contract.Requires(tok != null);
@@ -2373,13 +2373,13 @@ namespace Microsoft.Dafny {
         return t;
       }
     }
-    
+
     Bpl.Constant GetField(Field f)
     {
       Contract.Requires(f != null && f.IsMutable);
       Contract.Requires(sink != null && predef != null);
       Contract.Ensures(Contract.Result<Bpl.Constant>() != null);
-     
+
       Bpl.Constant fc;
       if (fields.TryGetValue(f, out fc)) {
         Contract.Assert(fc != null);
@@ -2434,13 +2434,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(fse != null);
       Contract.Requires(fse.Field != null && fse.Field.IsMutable);
       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
-     
+
       return new Bpl.IdentifierExpr(fse.tok, GetField(fse.Field));
     }
 
     /// <summary>
     /// This method is expected to be called just once for each function in the program.
-    /// </summary>    
+    /// </summary>
     void AddFunction(Function f)
     {
       Contract.Requires(f != null);
@@ -2457,7 +2457,7 @@ namespace Microsoft.Dafny {
       Bpl.Formal res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, TrType(f.ResultType)), false);
       Bpl.Function func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res);
       sink.TopLevelDeclarations.Add(func);
-      
+
       if (f.IsRecursive && !f.IsUnlimited) {
         sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 0), args, res));
         sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 2), args, res));
@@ -2467,12 +2467,12 @@ namespace Microsoft.Dafny {
       Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullName + "#canCall", args, res);
       sink.TopLevelDeclarations.Add(canCallF);
     }
-    
+
     /// <summary>
     /// This method is expected to be called just twice for each procedure in the program (once with
     /// wellformednessProc set to true, once with wellformednessProc set to false).
     /// In addition, it is used once to generate refinement conditions.
-    /// </summary>    
+    /// </summary>
     Bpl.Procedure AddMethod(Method m, bool wellformednessProc, bool skipEnsures)
     {
       Contract.Requires(m != null);
@@ -2482,7 +2482,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<Bpl.Procedure>() != null);
 
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
-      
+
       Bpl.VariableSeq inParams = new Bpl.VariableSeq();
       Bpl.VariableSeq outParams = new Bpl.VariableSeq();
       if (!m.IsStatic) {
@@ -2502,7 +2502,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
         outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false));
       }
-      
+
       Bpl.RequiresSeq req = new Bpl.RequiresSeq();
       Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();
       Bpl.EnsuresSeq ens = new Bpl.EnsuresSeq();
@@ -2513,7 +2513,7 @@ namespace Microsoft.Dafny {
       req.Add(Requires(m.tok, true, context, null, null));
       mod.Add(etran.HeapExpr);
       mod.Add(etran.Tick());
-      
+
       if (!wellformednessProc) {
         string comment = "user-defined preconditions";
         foreach (MaybeFreeExpression p in m.Req) {
@@ -2551,54 +2551,54 @@ namespace Microsoft.Dafny {
       return proc;
     }
 
-    #region Refinement extension    
-    
-    void AddMethodRefinement(MethodRefinement m) 
+    #region Refinement extension
+
+    void AddMethodRefinement(MethodRefinement m)
      {
       Contract.Requires(m != null);
       Contract.Requires(sink != null && predef != null);
-      // r is abstract, m is concrete 
+      // r is abstract, m is concrete
       Method r = m.Refined;
       Contract.Assert(r != null);
       Contract.Assert(m.EnclosingClass != null);
       string name = "Refinement$$" + m.FullName;
       string that = "that";
-      
+
       Bpl.IdentifierExpr heap = new Bpl.IdentifierExpr(m.tok, predef.HeapVarName, predef.HeapType);
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, heap, that);
-      
+
       // TODO: this straight inlining does not handle recursive calls
-      // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure, or check refinement of frames      
-            
+      // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure, or check refinement of frames
+
       // generate procedure declaration with pre-condition wp(r, true)
       Bpl.Procedure proc = AddMethod(r, false, true);
       proc.Name = name;
-      
+
       // create "that" for m
       Bpl.Expr wh = Bpl.Expr.And(
         Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, that, predef.RefType), predef.Null),
         etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, that, predef.RefType), Resolver.GetReceiverType(m.tok, m)));
       Bpl.Formal thatVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, that, predef.RefType, wh), true);
       proc.InParams.Add(thatVar);
-      
-      // add outs of m to the outs of the refinement procedure   
+
+      // add outs of m to the outs of the refinement procedure
       foreach (Formal p in m.Outs) {
         Bpl.Type varType = TrType(p.Type);
         Bpl.Expr w = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
         proc.OutParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, w), false));
       }
       sink.TopLevelDeclarations.Add(proc);
-           
-      // generate procedure implementation:      
+
+      // generate procedure implementation:
       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
       Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
       Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);
       Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
       Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
-      
+
       Contract.Assert(m.Body != null);
       Contract.Assert(r.Body != null);
-      
+
       // declare a frame variable that allows anything to be changed (not checking modifies clauses)
       Bpl.IdentifierExpr theFrame = etran.TheFrame(m.tok);
       Contract.Assert(theFrame.Type != null);
@@ -2610,12 +2610,12 @@ namespace Microsoft.Dafny {
       Bpl.BoundVariable fVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$f", predef.FieldName(m.tok, alpha)));
       Bpl.Expr lambda = new Bpl.LambdaExpr(m.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, Bpl.Expr.True);
       builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, frame), lambda));
-      
-      // assume I($Heap, $Heap)              
+
+      // assume I($Heap, $Heap)
       builder.Add(new Bpl.AssumeCmd(m.tok, TrCouplingInvariant(m, heap, "this", heap, that)));
-      
+
       // assign input formals of m (except "this")
-      for (int i = 0; i < m.Ins.Count; i++) {        
+      for (int i = 0; i < m.Ins.Count; i++) {
         Bpl.LocalVariable arg = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, m.Ins[i].UniqueName, TrType(m.Ins[i].Type)));
         localVariables.Add(arg);
         Bpl.Variable var = inParams[i+1];
@@ -2628,7 +2628,7 @@ namespace Microsoft.Dafny {
       loopHeapVarCount = 0;
       otherTmpVarCount = 0;
       _tmpIEs.Clear();
-            
+
       //  call inlined m;
       TrStmt(m.Body, builder, localVariables, etran);
 
@@ -2636,10 +2636,10 @@ namespace Microsoft.Dafny {
       Bpl.LocalVariable heap2 = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, heap.Name+"2", predef.HeapType));
       localVariables.Add(heap2);
       builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, heap2), etran.HeapExpr));
-      
+
       //  $Heap := old($Heap);
       builder.Add(Bpl.Cmd.SimpleAssign(m.tok, heap, new Bpl.OldExpr(m.tok, heap)));
-                                
+
       //  call inlined r;
       currentMethod = r;
       etran = new ExpressionTranslator(this, predef, heap);
@@ -2650,7 +2650,7 @@ namespace Microsoft.Dafny {
       loopHeapVarCount = 0;
       otherTmpVarCount = 0;
       _tmpIEs.Clear();
-      
+
       // assert output variables of r and m are pairwise equal
       Contract.Assert(outParams.Length % 2 == 0);
       int k = outParams.Length / 2;
@@ -2658,21 +2658,21 @@ namespace Microsoft.Dafny {
         Bpl.Variable rOut = outParams[i];
         Bpl.Variable mOut = outParams[i+k];
         Contract.Assert(rOut != null && mOut != null);
-        builder.Add(Assert(m.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(m.tok, mOut), new Bpl.IdentifierExpr(m.tok, rOut)), 
+        builder.Add(Assert(m.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(m.tok, mOut), new Bpl.IdentifierExpr(m.tok, rOut)),
           "Refinement method may not produce the same value for output variable " + m.Outs[i].Name));
       }
-            
-      // assert I($Heap1, $Heap)      
+
+      // assert I($Heap1, $Heap)
       builder.Add(Assert(m.tok, TrCouplingInvariant(m, heap, "this", new Bpl.IdentifierExpr(m.tok, heap2), that),
         "Refinement method may not preserve the coupling invariant"));
-                                                
+
       Bpl.StmtList stmts = builder.Collect(m.tok);
       Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
         typeParams, inParams, outParams,
         localVariables, stmts);
       sink.TopLevelDeclarations.Add(impl);
     }
-    
+
     private sealed class NominalSubstituter : Duplicator
     {
       private readonly Dictionary<string,Bpl.Expr> subst;
@@ -2686,7 +2686,7 @@ namespace Microsoft.Dafny {
         Contract.Invariant(cce.NonNullDictionaryAndValues(subst));
       }
 
-          
+
       public override Expr VisitIdentifierExpr(Bpl.IdentifierExpr node)
       {
         Contract.Requires(node != null);
@@ -2694,7 +2694,7 @@ namespace Microsoft.Dafny {
 
         if (subst.ContainsKey(node.Name))
           return subst[node.Name];
-        else 
+        else
           return base.VisitIdentifierExpr(node);
       }
     }
@@ -2711,32 +2711,32 @@ namespace Microsoft.Dafny {
       ClassRefinementDecl c = m.EnclosingClass as ClassRefinementDecl;
       Contract.Assert(c != null);
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, conHeap, conThis);
-            
-      foreach (MemberDecl d in c.Members) 
+
+      foreach (MemberDecl d in c.Members)
         if (d is CouplingInvariant) {
           CouplingInvariant inv = (CouplingInvariant)d;
 
           Contract.Assert(inv.Refined != null);
           Contract.Assert(inv.Formals != null);
-          
-          // replace formals with field dereferences                    
+
+          // replace formals with field dereferences
           Dictionary<string,Bpl.Expr> map = new Dictionary<string,Bpl.Expr>();
           Bpl.Expr absVar = new Bpl.IdentifierExpr(d.tok, absThis, predef.RefType);
-          for (int i = 0; i < inv.Refined.Count; i++) {     
+          for (int i = 0; i < inv.Refined.Count; i++) {
             // TODO: boxing/unboxing?
             Bpl.Expr result = ExpressionTranslator.ReadHeap(inv.Toks[i], absHeap, absVar, new Bpl.IdentifierExpr(inv.Toks[i], GetField(cce.NonNull(inv.Refined[i]))));
             map.Add(inv.Formals[i].UniqueName, result);
           }
-                              
+
           Bpl.Expr e = new NominalSubstituter(map).VisitExpr(etran.TrExpr(inv.Expr));
           cond = Bpl.Expr.And(cond, e);
         }
-            
+
       return cond;
     }
-    
+
     #endregion
-    
+
     class BoilerplateTriple {  // a triple that is now a quintuple
       [ContractInvariantMethod]
       void ObjectInvariant() {
@@ -2764,7 +2764,7 @@ namespace Microsoft.Dafny {
         Comment = comment;
       }
     }
-    
+
     /// <summary>
     /// There are 3 states of interest when generating two-state boilerplate:
     ///  S0. the beginning of the method or loop, which is where the modifies clause is interpreted
@@ -2781,17 +2781,17 @@ namespace Microsoft.Dafny {
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<BoilerplateTriple>>()));
 
       List<BoilerplateTriple> boilerplate = new List<BoilerplateTriple>();
-      
+
       // the frame condition, which is free since it is checked with every heap update and call
       boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, etranPre, etran, etranMod), null, "frame condition"));
 
       // HeapSucc(S1, S2)
       Bpl.Expr heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);
       boilerplate.Add(new BoilerplateTriple(tok, true, heapSucc, null, "boilerplate"));
-      
+
       return boilerplate;
     }
-    
+
     /// <summary>
     /// There are 3 states of interest when generating a frame condition:
     ///  S0. the beginning of the method/loop, which is where the modifies clause is interpreted
@@ -2823,9 +2823,9 @@ namespace Microsoft.Dafny {
       Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);
       Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranMod.IsAlloced(tok, o));
       Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);
-      
+
       consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etranMod, null, null));
-      
+
       Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
       return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
     }
@@ -2857,15 +2857,15 @@ namespace Microsoft.Dafny {
 
       Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
       return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
-    }    
+    }
     // ----- Type ---------------------------------------------------------------------------------
-    
+
     Bpl.Type TrType(Type type)
      {
       Contract.Requires(type != null);
       Contract.Requires(predef != null);
       Contract.Ensures(Contract.Result<Bpl.Type>() != null);
-     
+
       while (true) {
         TypeProxy tp = type as TypeProxy;
         if (tp == null) {
@@ -2877,7 +2877,7 @@ namespace Microsoft.Dafny {
           type = tp.T;
         }
       }
-      
+
       if (type is BoolType) {
         return Bpl.Type.Bool;
       } else if (type is IntType) {
@@ -2897,7 +2897,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type
       }
     }
-    
+
     Bpl.TypeVariableSeq TrTypeParamDecls(List<TypeParameter/*!*/>/*!*/ tps)
     {
       Contract.Requires(cce.NonNullElements(tps));
@@ -2908,7 +2908,7 @@ namespace Microsoft.Dafny {
     }
 
     // ----- Statement ----------------------------------------------------------------------------
-    
+
     Bpl.AssertCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage)
     {
       Contract.Requires(tok != null);
@@ -2978,10 +2978,10 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);
       Contract.Requires(currentMethod != null && predef != null);
       Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);
-     
+
       return TrStmt2StmtList(new Bpl.StmtListBuilder(), block, locals, etran);
     }
-    
+
     Bpl.StmtList TrStmt2StmtList(Bpl.StmtListBuilder builder, Statement block, Bpl.VariableSeq locals, ExpressionTranslator etran)
      {
       Contract.Requires(builder != null);
@@ -2990,11 +2990,11 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);
       Contract.Requires(currentMethod != null && predef != null);
       Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);
-      
+
       TrStmt(block, builder, locals, etran);
       return builder.Collect(block.Tok);  // TODO: would be nice to have an end-curly location for "block"
     }
-    
+
     void TrStmt(Statement stmt, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran)
     {
       Contract.Requires(stmt != null);
@@ -3035,7 +3035,7 @@ namespace Microsoft.Dafny {
             TrStmt_CheckWellformed(arg.E, builder, locals, etran, false);
           }
         }
-         
+
       } else if (stmt is BreakStmt) {
         AddComment(builder, stmt, "break statement");
         var s = (BreakStmt)stmt;
@@ -3254,7 +3254,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr qqq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), bbb);
           builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined"));  // totality check
         }
-        
+
         // Here comes:  assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);
         Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o, GetField((FieldSelectExpr)s.BodyAssign.Lhs)));
         Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
@@ -3288,14 +3288,14 @@ namespace Microsoft.Dafny {
           qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
           builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
         }
-        
+
         builder.Add(CaptureState(stmt.Tok));
-        
+
       } else if (stmt is MatchStmt) {
         var s = (MatchStmt)stmt;
         TrStmt_CheckWellformed(s.Source, builder, locals, etran, true);
         Bpl.Expr source = etran.TrExpr(s.Source);
-        
+
         var b = new Bpl.StmtListBuilder();
         b.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False));
         Bpl.StmtList els = b.Collect(stmt.Tok);
@@ -3450,7 +3450,7 @@ namespace Microsoft.Dafny {
       }
       // add a free invariant which says that the heap hasn't changed outside of the modifies clause.
       invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));
-      
+
       // include a free invariant that says that all completed iterations so far have only decreased the termination metric
       if (initDecr != null) {
         List<IToken> toks = new List<IToken>();
@@ -3607,7 +3607,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);
       Contract.Requires(locals != null);
       Contract.Requires(etran != null);
-      
+
       Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver);
       Bpl.ExprSeq ins = new Bpl.ExprSeq();
       if (!method.IsStatic) {
@@ -3692,7 +3692,7 @@ namespace Microsoft.Dafny {
         }
       }
     }
-    
+
     static Expression CreateIntLiteral(IToken tok, int n)
     {
       Contract.Requires(tok != null);
@@ -3706,13 +3706,13 @@ namespace Microsoft.Dafny {
         return CreateIntSub(tok, CreateIntLiteral(tok, 0), CreateIntLiteral(tok, -n));
       }
     }
-    
+
     static Expression CreateIntSub(IToken tok, Expression e0, Expression e1)
      {
       Contract.Requires(tok != null);
       Contract.Requires(e0 != null);
       Contract.Requires(e1 != null);
-      
+
 
       Contract.Requires(e0.Type is IntType && e1.Type is IntType);
       Contract.Ensures(Contract.Result<Expression>() != null);
@@ -3721,7 +3721,7 @@ namespace Microsoft.Dafny {
       s.Type = Type.Int;  // resolve here
       return s;
     }
-    
+
     static Expression CreateIntITE(IToken tok, Expression test, Expression e0, Expression e1)
      {
       Contract.Requires(tok != null);
@@ -3735,7 +3735,7 @@ namespace Microsoft.Dafny {
       ite.Type = Type.Int;  // resolve here
       return ite;
     }
-    
+
     public IEnumerable<Expression> Conjuncts(Expression expr)
      {
       Contract.Requires(expr != null);
@@ -3773,7 +3773,7 @@ namespace Microsoft.Dafny {
         // record value of each decreases expression at beginning of the loop iteration
         Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(e.tok, bf, etran.TrExpr(e));
         builder.Add(cmd);
-        
+
         c++;
       }
       return oldBfs;
@@ -3825,7 +3825,7 @@ namespace Microsoft.Dafny {
       }
       builder.Add(Assert(tok, decrExpr, inferredDecreases ? "cannot prove termination; try supplying a decreases clause" : "failure to decrease termination measure"));
     }
-    
+
     /// <summary>
     /// Returns the expression that says whether or not the decreases function has gone down (if !allowNoChange)
     /// or has gone down or stayed the same (if allowNoChange).
@@ -3846,7 +3846,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
 
       int N = types.Count;
-      
+
       // compute eq and less for each component of the lexicographic pair
       List<Bpl.Expr> Eq = new List<Bpl.Expr>(N);
       List<Bpl.Expr> Less = new List<Bpl.Expr>(N);
@@ -3913,7 +3913,7 @@ namespace Microsoft.Dafny {
         return false;  // don't consider any type parameters to be the same (since we have no comparison function for them anyway)
       }
     }
-    
+
     void ComputeLessEq(IToken/*!*/ tok, Type/*!*/ ty, Bpl.Expr/*!*/ e0, Bpl.Expr/*!*/ e1, out Bpl.Expr/*!*/ less, out Bpl.Expr/*!*/ atmost, out Bpl.Expr/*!*/ eq,
                        ExpressionTranslator/*!*/ etran, bool includeLowerBound)
      {
@@ -3926,7 +3926,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.ValueAtReturn(out less)!=null);
       Contract.Ensures(Contract.ValueAtReturn(out atmost)!=null);
       Contract.Ensures(Contract.ValueAtReturn(out eq)!=null);
-     
+
       if (ty is BoolType) {
         eq = Bpl.Expr.Iff(e0, e1);
         less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);
@@ -3955,7 +3955,7 @@ namespace Microsoft.Dafny {
         eq = Bpl.Expr.Eq(b0, b1);
         less = Bpl.Expr.Lt(b0, b1);
         atmost = Bpl.Expr.Le(b0, b1);
-        
+
       } else {
         // reference type
         Bpl.Expr b0 = Bpl.Expr.Neq(e0, predef.Null);
@@ -3965,14 +3965,14 @@ namespace Microsoft.Dafny {
         atmost = Bpl.Expr.Imp(b0, b1);
       }
     }
-    
+
     void AddComment(Bpl.StmtListBuilder builder, Statement stmt, string comment) {
       Contract.Requires(builder != null);
       Contract.Requires(stmt != null);
       Contract.Requires(comment != null);
       builder.Add(new Bpl.CommentCmd(string.Format("----- {0} ----- {1}({2},{3})", comment, stmt.Tok.filename, stmt.Tok.line, stmt.Tok.col)));
-    }    
-    
+    }
+
     Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran)
     {
       Contract.Requires(tok != null);
@@ -4001,7 +4001,7 @@ namespace Microsoft.Dafny {
 
       } else  if (type is BoolType || type is IntType) {
         // nothing todo
-      
+
       } else if (type is SetType) {
         SetType st = (SetType)type;
         // (forall t: BoxType :: { x[t] } x[t] ==> Unbox(t)-has-the-expected-type)
@@ -4016,7 +4016,7 @@ namespace Microsoft.Dafny {
           Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));
           return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));
         }
-        
+
       } else if (type is SeqType) {
         SeqType st = (SeqType)type;
         // (forall i: int :: { Seq#Index(x,i) }
@@ -4053,7 +4053,7 @@ namespace Microsoft.Dafny {
 
       } else if (type.IsTypeParameter) {
         return FunctionCall(tok, BuiltinFunction.GenericAlloc, null, x, etran.HeapExpr);
-        
+
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type
       }
@@ -4244,7 +4244,7 @@ namespace Microsoft.Dafny {
 
           var obj = SaveInTemp(etran.TrExpr(mse.Array), rhsCanAffectPreviouslyKnownExpressions,
             "$obj" + i, predef.RefType, builder, locals);
-          var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhsCanAffectPreviouslyKnownExpressions, 
+          var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhsCanAffectPreviouslyKnownExpressions,
             "$index" + i, predef.FieldName(mse.tok, predef.BoxType), builder, locals);
           prevObj[i] = obj;
           prevIndex[i] = fieldName;
@@ -4434,7 +4434,7 @@ namespace Microsoft.Dafny {
       readonly int layerOffset = 0;
       public int Statistics_FunctionCount = 0;
       [ContractInvariantMethod]
-      void ObjectInvariant() 
+      void ObjectInvariant()
       {
         Contract.Invariant(HeapExpr != null);
         Contract.Invariant(predef != null);
@@ -4453,7 +4453,7 @@ namespace Microsoft.Dafny {
         this.HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);
         this.This = "this";
       }
-      
+
       public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap) {
         Contract.Requires(translator != null);
         Contract.Requires(predef != null);
@@ -4463,7 +4463,7 @@ namespace Microsoft.Dafny {
         this.HeapExpr = heap;
         this.This = "this";
       }
-      
+
       public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar) {
         Contract.Requires(translator != null);
         Contract.Requires(predef != null);
@@ -4521,7 +4521,7 @@ namespace Microsoft.Dafny {
           return HeapExpr is Bpl.OldExpr;
         }
       }
-      
+
       public ExpressionTranslator LimitedFunctions(Function applyLimited_CurrentFunction) {
         Contract.Requires(applyLimited_CurrentFunction != null);
         Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
@@ -4596,10 +4596,10 @@ namespace Microsoft.Dafny {
           } else {
             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected literal
           }
-          
+
         } else if (expr is ThisExpr) {
           return new Bpl.IdentifierExpr(expr.tok, This, predef.RefType);
-        
+
         } else if (expr is IdentifierExpr) {
           IdentifierExpr e = (IdentifierExpr)expr;
           return TrVar(expr.tok, cce.NonNull(e.Var));
@@ -4607,7 +4607,7 @@ namespace Microsoft.Dafny {
         } else if (expr is BoogieWrapper) {
           var e = (BoogieWrapper)expr;
           return e.Expr;
-        
+
         } else if (expr is SetDisplayExpr) {
           SetDisplayExpr e = (SetDisplayExpr)expr;
           Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);
@@ -4616,7 +4616,7 @@ namespace Microsoft.Dafny {
             s = translator.FunctionCall(expr.tok, BuiltinFunction.SetUnionOne, predef.BoxType, s, ss);
           }
           return s;
-          
+
         } else if (expr is SeqDisplayExpr) {
           SeqDisplayExpr e = (SeqDisplayExpr)expr;
           Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);
@@ -4627,7 +4627,7 @@ namespace Microsoft.Dafny {
             i++;
           }
           return s;
-        
+
         } else if (expr is FieldSelectExpr) {
           FieldSelectExpr e = (FieldSelectExpr)expr;
           Contract.Assert(e.Field != null);
@@ -4639,7 +4639,7 @@ namespace Microsoft.Dafny {
             result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(translator.GetReadonlyField(e.Field)), new Bpl.ExprSeq(obj));
           }
           return CondApplyUnbox(expr.tok, result, e.Field.Type, cce.NonNull(expr.Type));
-          
+
         } else if (expr is SeqSelectExpr) {
           SeqSelectExpr e = (SeqSelectExpr)expr;
           Bpl.Expr seq = TrExpr(e.Seq);
@@ -4676,7 +4676,7 @@ namespace Microsoft.Dafny {
             }
             return seq;
           }
-        
+
         } else if (expr is SeqUpdateExpr) {
           SeqUpdateExpr e = (SeqUpdateExpr)expr;
           Bpl.Expr seq = TrExpr(e.Seq);
@@ -4714,7 +4714,7 @@ namespace Microsoft.Dafny {
           Bpl.ExprSeq args = FunctionInvocationArguments(e);
           Bpl.Expr result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(id), args);
           return CondApplyUnbox(expr.tok, result, e.Function.ResultType, expr.Type);
-        
+
         } else if (expr is DatatypeValue) {
           DatatypeValue dtv = (DatatypeValue)expr;
           Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved
@@ -4727,11 +4727,11 @@ namespace Microsoft.Dafny {
           }
           Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(dtv.tok, dtv.Ctor.FullName, predef.DatatypeType);
           return new Bpl.NAryExpr(dtv.tok, new Bpl.FunctionCall(id), args);
-            
+
         } else if (expr is OldExpr) {
           OldExpr e = (OldExpr)expr;
           return new Bpl.OldExpr(expr.tok, TrExpr(e.E));
-        
+
         } else if (expr is FreshExpr) {
           FreshExpr e = (FreshExpr)expr;
           Bpl.Expr oldHeap = new Bpl.OldExpr(expr.tok, HeapExpr);
@@ -4789,7 +4789,7 @@ namespace Microsoft.Dafny {
             default:
               Contract.Assert(false); throw new cce.UnreachableException();  // unexpected unary expression
           }
-        
+
         } else if (expr is BinaryExpr) {
           BinaryExpr e = (BinaryExpr)expr;
           Bpl.Expr e0 = TrExpr(e.E0);
@@ -4810,12 +4810,12 @@ namespace Microsoft.Dafny {
               bOpcode = BinaryOperator.Opcode.And; break;
             case BinaryExpr.ResolvedOpcode.Or:
               bOpcode = BinaryOperator.Opcode.Or; break;
-              
+
             case BinaryExpr.ResolvedOpcode.EqCommon:
               bOpcode = BinaryOperator.Opcode.Eq; break;
             case BinaryExpr.ResolvedOpcode.NeqCommon:
               bOpcode = BinaryOperator.Opcode.Neq; break;
-              
+
             case BinaryExpr.ResolvedOpcode.Lt:
               bOpcode = BinaryOperator.Opcode.Lt; break;
             case BinaryExpr.ResolvedOpcode.Le:
@@ -4892,12 +4892,12 @@ namespace Microsoft.Dafny {
               return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.Gt,
                 translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e0),
                 translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e1));
-              
+
             default:
               Contract.Assert(false); throw new cce.UnreachableException();  // unexpected binary expression
           }
           return Bpl.Expr.Binary(expr.tok, bOpcode, e0, e1);
-        
+
         } else if (expr is QuantifierExpr) {
           QuantifierExpr e = (QuantifierExpr)expr;
           Bpl.VariableSeq bvars = new Bpl.VariableSeq();
@@ -4916,7 +4916,7 @@ namespace Microsoft.Dafny {
             antecedent = Bpl.Expr.And(antecedent, TrExpr(e.Range));
           }
           Bpl.Expr body = TrExpr(e.Term);
-          
+
           if (e is ForallExpr) {
             return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.Imp(antecedent, body));
           } else {
@@ -4955,11 +4955,11 @@ namespace Microsoft.Dafny {
         } else if (expr is BoxingCastExpr) {
           BoxingCastExpr e = (BoxingCastExpr)expr;
           return CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType);
-          
+
         } else if (expr is UnboxingCastExpr) {
           UnboxingCastExpr e = (UnboxingCastExpr)expr;
           return CondApplyUnbox(e.tok, TrExpr(e.E), e.FromType, e.ToType);
-          
+
         } else {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression
         }
@@ -4968,7 +4968,7 @@ namespace Microsoft.Dafny {
       public Bpl.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, Bpl.VariableSeq bvars) {
         Contract.Requires(boundVars != null);
         Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
-        
+
         Bpl.Expr typeAntecedent = Bpl.Expr.True;
         foreach (BoundVar bv in boundVars) {
           Bpl.Variable bvar = new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, translator.TrType(bv.Type)));
@@ -5047,7 +5047,7 @@ namespace Microsoft.Dafny {
           return e;
         }
       }
-      
+
       public Bpl.Expr BoxIfNecessary(IToken tok, Bpl.Expr e, Type fromType) {
         Contract.Requires(tok != null);
         Contract.Requires(e != null);
@@ -5056,7 +5056,7 @@ namespace Microsoft.Dafny {
 
         return CondApplyBox(tok, e, fromType, null);
       }
-      
+
       public Bpl.Expr CondApplyUnbox(IToken tok, Bpl.Expr e, Type fromType, Type toType) {
         Contract.Requires(tok != null);
         Contract.Requires(e != null);
@@ -5070,7 +5070,7 @@ namespace Microsoft.Dafny {
           return e;
         }
       }
-      
+
       public static bool ModeledAsBoxType(Type t) {
         Contract.Requires(t != null);
         while (true) {
@@ -5173,7 +5173,7 @@ namespace Microsoft.Dafny {
         }
         return Bpl.Expr.SelectTok(tok, TrExpr(s), BoxIfNecessary(tok, elmt, elmtType));
       }
-      
+
       Bpl.QKeyValue TrAttributes(Attributes attrs) {
         Bpl.QKeyValue kv = null;
         while (attrs != null) {
@@ -5190,7 +5190,7 @@ namespace Microsoft.Dafny {
         }
         return kv;
       }
-      
+
       // --------------- help routines ---------------
 
       public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e) {
@@ -5200,7 +5200,7 @@ namespace Microsoft.Dafny {
 
         return IsAlloced(tok, e, HeapExpr);
       }
-          
+
       Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e, Bpl.Expr heap) {
         Contract.Requires(tok != null);
         Contract.Requires(e != null);
@@ -5209,7 +5209,7 @@ namespace Microsoft.Dafny {
 
         return ReadHeap(tok, heap, e, predef.Alloc(tok));
       }
-      
+
       public Bpl.Expr GoodRef(IToken tok, Bpl.Expr e, Type type) {
         Contract.Requires(tok != null);
         Contract.Requires(e != null);
@@ -5224,7 +5224,7 @@ namespace Microsoft.Dafny {
           return IsAlloced(tok, e);
         }
       }
-      
+
       public Bpl.Expr GoodRef_Class(IToken tok, Bpl.Expr e, UserDefinedType type, bool isNew)
        {
         Contract.Requires(tok != null);
@@ -5246,12 +5246,12 @@ namespace Microsoft.Dafny {
         if (isNew) {
           r = Bpl.Expr.Not(r);  // use the conjunct:  !Heap[e, alloc]
         }
-        
+
         // dtype(e) == C
         Bpl.Expr dtypeFunc = translator.FunctionCall(tok, BuiltinFunction.DynamicType, null, e);
         Bpl.Expr dtype = Bpl.Expr.Eq(dtypeFunc, type);
         r = r == null ? dtype : Bpl.Expr.And(r, dtype);
-        
+
         // TypeParams(e, #) == T
         int n = 0;
         foreach (Type arg in typeArgs) {
@@ -5262,7 +5262,7 @@ namespace Microsoft.Dafny {
           }
           n++;
         }
-        
+
         return r;
       }
 
@@ -5290,7 +5290,7 @@ namespace Microsoft.Dafny {
         return r;
       }
     }
-    
+
     enum BuiltinFunction {
       SetEmpty,
       SetUnionOne,
@@ -5301,7 +5301,7 @@ namespace Microsoft.Dafny {
       SetSubset,
       SetDisjoint,
       SetChoose,
-      
+
       SeqLength,
       SeqEmpty,
       SeqBuild,
@@ -5313,17 +5313,17 @@ namespace Microsoft.Dafny {
       SeqTake,
       SeqEqual,
       SeqSameUntil,
-      
+
       IndexField,
       MultiIndexField,
-      
+
       Box,
       Unbox,
       IsCanonicalBoolBox,
-      
+
       IsGoodHeap,
       HeapSucc,
-      
+
       DynamicType,  // allocated type (of object reference)
       DtType,       // type of datatype value
       TypeParams,   // type parameters of allocated type
@@ -5338,7 +5338,7 @@ namespace Microsoft.Dafny {
 
       GenericAlloc,
     }
-    
+
     // The "typeInstantiation" argument is passed in to help construct the result type of the function.
     Bpl.NAryExpr FunctionCall(IToken tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[] args)
     {
@@ -5433,7 +5433,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 3);
           Contract.Assert(typeInstantiation == null);
           return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args);
-          
+
         case BuiltinFunction.IndexField:
           Contract.Assert(args.Length == 1);
           Contract.Assert(typeInstantiation == null);
@@ -5516,7 +5516,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected built-in function
       }
     }
-    
+
     Bpl.NAryExpr FunctionCall(IToken tok, string function, Bpl.Type returnType, params Bpl.Expr[] args)
     {
       Contract.Requires(tok != null);
@@ -5984,7 +5984,7 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < dt.TypeArgs.Count; i++) {
           subst.Add(dt.TypeArgs[i], instantiatedType.TypeArgs[i]);
         }
-        
+
         foreach (DatatypeCtor ctor in dt.Ctors) {
           Bpl.VariableSeq bvs;
           List<Bpl.Expr> args;
@@ -6037,7 +6037,7 @@ namespace Microsoft.Dafny {
             newExpr = new SeqDisplayExpr(expr.tok, newElements);
           }
         }
-        
+
       } else if (expr is FieldSelectExpr) {
         FieldSelectExpr fse = (FieldSelectExpr)expr;
         Expression substE = Substitute(fse.Obj, receiverReplacement, substMap);
@@ -6046,7 +6046,7 @@ namespace Microsoft.Dafny {
           fseNew.Field = fse.Field;  // resolve on the fly (and fseExpr.Type is set at end of method)
           newExpr = fseNew;
         }
-        
+
       } else if (expr is SeqSelectExpr) {
         SeqSelectExpr sse = (SeqSelectExpr)expr;
         Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);
@@ -6055,7 +6055,7 @@ namespace Microsoft.Dafny {
         if (seq != sse.Seq || e0 != sse.E0 || e1 != sse.E1) {
           newExpr = new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);
         }
-        
+
       } else if (expr is SeqUpdateExpr) {
         SeqUpdateExpr sse = (SeqUpdateExpr)expr;
         Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);
@@ -6082,7 +6082,7 @@ namespace Microsoft.Dafny {
           newFce.Function = e.Function;  // resolve on the fly (and set newFce.Type below, at end)
           newExpr = newFce;
         }
-      
+
       } else if (expr is DatatypeValue) {
         DatatypeValue dtv = (DatatypeValue)expr;
         List<Expression> newArgs = SubstituteExprList(dtv.Arguments, receiverReplacement, substMap);
@@ -6125,7 +6125,7 @@ namespace Microsoft.Dafny {
           newBin.ResolvedOp = e.ResolvedOp;  // part of what needs to be done to resolve on the fly (newBin.Type is set below, at end)
           newExpr = newBin;
         }
-        
+
       } else if (expr is ComprehensionExpr) {
         var e = (ComprehensionExpr)expr;
         Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);
@@ -6148,7 +6148,7 @@ namespace Microsoft.Dafny {
         } else {
           Contract.Assume(false);  // unexpected ComprehensionExpr
         }
-        
+
       } else if (expr is ITEExpr) {
         ITEExpr e = (ITEExpr)expr;
         Expression test = Substitute(e.Test, receiverReplacement, substMap);
@@ -6162,7 +6162,7 @@ namespace Microsoft.Dafny {
         var e = (ConcreteSyntaxExpression)expr;
         return Substitute(e.ResolvedExpression, receiverReplacement, substMap);
       }
-      
+
       if (newExpr == null) {
         return expr;
       } else {
@@ -6170,18 +6170,18 @@ namespace Microsoft.Dafny {
         return newExpr;
       }
     }
-    
+
     static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,
                                                  Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
       Contract.Requires(cce.NonNullElements(elist));
       Contract.Requires((receiverReplacement == null) == (substMap == null));
       Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));
-      
+
       List<Expression> newElist = null;  // initialized lazily
       for (int i = 0; i < elist.Count; i++)
       {cce.LoopInvariant(  newElist == null || newElist.Count == i);
-      
+
         Expression substE = Substitute(elist[i], receiverReplacement, substMap);
         if (substE != elist[i] && newElist == null) {
           newElist = new List<Expression>();
@@ -6199,7 +6199,7 @@ namespace Microsoft.Dafny {
         return newElist;
       }
     }
-    
+
     static Triggers SubstTriggers(Triggers trigs, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
       Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
       if (trigs != null) {
@@ -6231,7 +6231,7 @@ namespace Microsoft.Dafny {
         if (!anyArgSubst) {
           newArgs = attrs.Args;
         }
-        
+
         Attributes prev = SubstAttributes(attrs.Prev, receiverReplacement, substMap);
         if (newArgs != attrs.Args || prev != attrs.Prev) {
           return new Attributes(attrs.Name, newArgs, prev);
@@ -6239,6 +6239,6 @@ namespace Microsoft.Dafny {
       }
       return attrs;
     }
-        
+
   }
-}
\ No newline at end of file
+}
-- 
cgit v1.2.3