13 files changed, 724 insertions, 849 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index d61d653d..0653fe2e 100644
--- a/Dafny/Compiler.cs
+++ b/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/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 15d39460..c0aae345 100644
--- a/Dafny/Dafny.atg
+++ b/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/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 4868be10..8bb381ea 100644
--- a/Dafny/DafnyAst.cs
+++ b/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/Dafny/DafnyMain.cs b/Dafny/DafnyMain.cs
index a18ea938..3f0b6e97 100644
--- a/Dafny/DafnyMain.cs
+++ b/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/Dafny/DafnyPipeline.csproj b/Dafny/DafnyPipeline.csproj
index 7f063c2c..6a15b1f7 100644
--- a/Dafny/DafnyPipeline.csproj
+++ b/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/Dafny/Parser.cs b/Dafny/Parser.cs
index 42014762..8fcb6bb0 100644
--- a/Dafny/Parser.cs
+++ b/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/Dafny/Printer.cs b/Dafny/Printer.cs
index b9c8601e..ba9963c7 100644
--- a/Dafny/Printer.cs
+++ b/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/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 197a603e..8ec5d4c1 100644
--- a/Dafny/Resolver.cs
+++ b/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/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 19157a32..37c08ddc 100644
--- a/Dafny/Scanner.cs
+++ b/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/Dafny/SccGraph.cs b/Dafny/SccGraph.cs
index 9f4b22c5..4ae1c185 100644
--- a/Dafny/SccGraph.cs
+++ b/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/Dafny/Translator.cs b/Dafny/Translator.cs
index d1c77122..74d33479 100644
--- a/Dafny/Translator.cs
+++ b/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
+}

diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs
index afd36aa8..d8d0e0e0 100644
--- a/DafnyDriver/DafnyDriver.cs
+++ b/DafnyDriver/DafnyDriver.cs
@@ -8,7 +8,7 @@
 //       - main program for taking a Dafny program and verifying it

 //---------------------------------------------------------------------------------------------

 

-namespace Microsoft.Boogie 

+namespace Microsoft.Boogie

 {

   using System;

   using System.IO;

@@ -22,7 +22,7 @@ namespace Microsoft.Boogie
   using VC;

   using AI = Microsoft.AbstractInterpretationFramework;

 

-/* 

+/*

   The following assemblies are referenced because they are needed at runtime, not at compile time:

     BaseTypes

     Provers.Z3

@@ -33,8 +33,8 @@ namespace Microsoft.Boogie
   {

     // ------------------------------------------------------------------------

     // Main

-    

-    public static int Main (string[] args) 

+

+    public static int Main (string[] args)

     {Contract.Requires(cce.NonNullElements(args));

       //assert forall{int i in (0:args.Length); args[i] != null};

       ExitValue exitValue = ExitValue.VERIFIED;

@@ -47,14 +47,14 @@ namespace Microsoft.Boogie
       if (CommandLineOptions.Clo.Files.Count == 0)

       {

         ErrorWriteLine("*** Error: No input files were specified.");

-        exitValue = ExitValue.PREPROCESSING_ERROR; 

+        exitValue = ExitValue.PREPROCESSING_ERROR;

         goto END;

       }

       if (CommandLineOptions.Clo.XmlSink != null) {

         string errMsg = CommandLineOptions.Clo.XmlSink.Open();

         if (errMsg != null) {

           ErrorWriteLine("*** Error: " + errMsg);

-          exitValue = ExitValue.PREPROCESSING_ERROR; 

+          exitValue = ExitValue.PREPROCESSING_ERROR;

           goto END;

         }

       }

@@ -62,17 +62,17 @@ namespace Microsoft.Boogie
       {

         Console.WriteLine(CommandLineOptions.Clo.Version);

       }

-      if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always) 

+      if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always)

       {

         Console.WriteLine("---Command arguments");

-        foreach (string arg in args) 

+        foreach (string arg in args)

         {Contract.Assert(arg != null);

           Console.WriteLine(arg);

         }

         Console.WriteLine("--------------------");

       }

 

-      foreach (string file in CommandLineOptions.Clo.Files) 

+      foreach (string file in CommandLineOptions.Clo.Files)

       {Contract.Assert(file != null);

         string extension = Path.GetExtension(file);

         if (extension != null) { extension = extension.ToLower(); }

@@ -91,12 +91,12 @@ namespace Microsoft.Boogie
         if (CommandLineOptions.Clo.XmlSink != null) {

           CommandLineOptions.Clo.XmlSink.Close();

         }

-        if (CommandLineOptions.Clo.Wait) 

+        if (CommandLineOptions.Clo.Wait)

         {

           Console.WriteLine("Press Enter to exit.");

           Console.ReadLine();

         }

-        return (int)exitValue;        

+        return (int)exitValue;

     }

 

     public static void ErrorWriteLine(string s) {Contract.Requires(s != null);

@@ -104,7 +104,7 @@ namespace Microsoft.Boogie
         Console.WriteLine(s);

         return;

       }

-      

+

       // split the string up into its first line and the remaining lines

       string remaining = null;

       int i = s.IndexOf('\r');

@@ -115,12 +115,12 @@ namespace Microsoft.Boogie
         }

         s = s.Substring(0, i);

       }

-      

+

       ConsoleColor col = Console.ForegroundColor;

       Console.ForegroundColor = ConsoleColor.Red;

       Console.WriteLine(s);

       Console.ForegroundColor = col;

-      

+

       if (remaining != null) {

         Console.WriteLine(remaining);

       }

@@ -156,7 +156,7 @@ namespace Microsoft.Boogie
         } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {

           Dafny.Translator translator = new Dafny.Translator();

           Program boogieProgram = translator.Translate(dafnyProgram);

-          if (CommandLineOptions.Clo.PrintFile != null) 

+          if (CommandLineOptions.Clo.PrintFile != null)

           {

             PrintBplFile(CommandLineOptions.Clo.PrintFile, boogieProgram, false);

           }

@@ -208,7 +208,7 @@ namespace Microsoft.Boogie
         }

       }

     }

-    

+

     static void PrintBplFile (string filename, Program program, bool allowPrintDesugaring)

     {

       Contract.Requires(filename != null);

@@ -228,17 +228,17 @@ namespace Microsoft.Boogie
         }

         CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaring;

     }

-    

-    

+

+

     static bool ProgramHasDebugInfo (Program program)

     {

       Contract.Requires(program != null);

         // We inspect the last declaration because the first comes from the prelude and therefore always has source context.

-        return program.TopLevelDeclarations.Count > 0 && 

+        return program.TopLevelDeclarations.Count > 0 &&

             cce.NonNull(program.TopLevelDeclarations[program.TopLevelDeclarations.Count - 1]).tok.IsValid;

     }

-    

-    

+

+

     /// <summary>

     /// Inform the user about something and proceed with translation normally.

     /// Print newline after the message.

@@ -265,7 +265,7 @@ namespace Microsoft.Boogie
       Console.Out.Flush();

     }

 

-    

+

 

     static void ReportBplError(IToken tok, string message, bool error)

     {

@@ -335,7 +335,7 @@ namespace Microsoft.Boogie
         return program;

       }

     }

-    

+

         /// <summary>

     /// Resolve, type check, infer invariants for, and verify the given Boogie program.

     /// The intention is that this Boogie program has been produced by translation from something

@@ -349,14 +349,14 @@ namespace Microsoft.Boogie
     {Contract.Requires(program != null);

     Contract.Requires(bplFileName != null);

       Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

-    

-      

+

+

       errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;

       PipelineOutcome oc = ResolveAndTypecheck(program, bplFileName);

       switch (oc) {

         case PipelineOutcome.Done:

           return oc;

-          

+

         case PipelineOutcome.ResolutionError:

         case PipelineOutcome.TypeCheckingError:

           {

@@ -376,7 +376,7 @@ namespace Microsoft.Boogie
 

         case PipelineOutcome.ResolvedAndTypeChecked:

           return InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

-          

+

         default:

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

       }

@@ -409,16 +409,16 @@ namespace Microsoft.Boogie
       }

 

       // ---------- Type check ------------------------------------------------------------

-      

+

       if (CommandLineOptions.Clo.NoTypecheck) { return PipelineOutcome.Done; }

-      

+

       errorCount = program.Typecheck();

       if (errorCount != 0) {

         Console.WriteLine("{0} type checking errors detected in {1}", errorCount, bplFileName);

         return PipelineOutcome.TypeCheckingError;

       }

-    

-      if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings) 

+

+      if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings)

       {

         // if PrintDesugaring option is engaged, print the file here, after resolution and type checking

         PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true);

@@ -426,7 +426,7 @@ namespace Microsoft.Boogie
 

       return PipelineOutcome.ResolvedAndTypeChecked;

     }

-    

+

     /// <summary>

     /// Given a resolved and type checked Boogie program, infers invariants for the program

     /// and then attempts to verify it.  Returns:

@@ -439,14 +439,14 @@ namespace Microsoft.Boogie
                                            out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)

     {Contract.Requires(program != null);

       Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

-    

+

       errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;

-  

+

       // ---------- Infer invariants --------------------------------------------------------

-      

+

       // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)

       Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

-       

+

       if (CommandLineOptions.Clo.LoopUnrollCount != -1) {

         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

       }

@@ -463,9 +463,9 @@ namespace Microsoft.Boogie
       // ---------- Verify ------------------------------------------------------------

 

       if (!CommandLineOptions.Clo.Verify) { return PipelineOutcome.Done; }

-            

+

       #region Verify each implementation

-      

+

 #if ROB_DEBUG

       string now = DateTime.Now.ToString().Replace(' ','-').Replace('/','-').Replace(':','-');

       System.IO.StreamWriter w = new System.IO.StreamWriter(@"\temp\batch_"+now+".bpl");

@@ -482,7 +482,7 @@ namespace Microsoft.Boogie
         } else

         {

           vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        }         

+        }

       }

       catch (ProverException e)

       {

@@ -648,7 +648,7 @@ namespace Microsoft.Boogie
                                 else

                                 {

                                     // for ErrorTrace == 1 restrict the output;

-                                    // do not print tokens with -17:-4 as their location because they have been 

+                                    // do not print tokens with -17:-4 as their location because they have been

                                     // introduced in the translation and do not give any useful feedback to the user

                                     if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4))

                                     {

@@ -682,9 +682,9 @@ namespace Microsoft.Boogie
       cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();

 

       #endregion

-      

+

       return PipelineOutcome.VerificationCompleted;

     }

-   

+

   }

 }

diff --git a/DafnyDriver/DafnyDriver.csproj b/DafnyDriver/DafnyDriver.csproj
index fb68eefd..cf88eed4 100644
--- a/DafnyDriver/DafnyDriver.csproj
+++ b/DafnyDriver/DafnyDriver.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>

@@ -140,11 +140,11 @@
     <None Include="app.config" />

   </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>