17 files changed, 943 insertions, 1065 deletions

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 6b8bb178..b1fbd609 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -45,7 +45,7 @@ Contract.Requires(cce.NonNullElements(defines,true));
   return ret;

 }

 

-  

+

 public static int Parse (Stream stream, string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

 Contract.Requires(stream != null);

 Contract.Requires(filename != null);

@@ -341,7 +341,7 @@ Types<TypeSeq/*!*/ ts>
 

 

 /*------------------------------------------------------------------------*/

-Consts<out VariableSeq/*!*/ ds> 

+Consts<out VariableSeq/*!*/ ds>

 = (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; TypedIdentSeq/*!*/ xs;

      ds = new VariableSeq();

      bool u = false; QKeyValue kv = null;

@@ -415,16 +415,16 @@ ds = new DeclarationSeq(); IToken/*!*/ z;
      Expr definition = null;

      Expr/*!*/ tmp;

   .)

-  "function" { Attribute<ref kv> } Ident<out z> 

+  "function" { Attribute<ref kv> } Ident<out z>

   [ TypeParams<out typeParamTok, out typeParams> ]

   "("

   [ VarOrType<out tyd>      (. arguments.Add(new Formal(tyd.tok, tyd, true)); .)

   { "," VarOrType<out tyd>  (. arguments.Add(new Formal(tyd.tok, tyd, true)); .)

   } ] ")"

-  ( 

+  (

     "returns" "(" VarOrType<out tyd> ")" (. retTyd = tyd; .)

-    | 

-    ":" Type<out retTy>   (. retTyd = new TypedIdent(retTy.tok, "", retTy); .) 

+    |

+    ":" Type<out retTy>   (. retTyd = new TypedIdent(retTy.tok, "", retTy); .)

   )

   ( "{" Expression<out tmp> (. definition = tmp; .) "}" | ";" )

   (.

@@ -587,7 +587,7 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>
     (.

       // here we attach kv only to the Procedure, not its implementation

       impl = new Implementation(x, x.val, typeParams,

-                                Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors); 

+                                Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);

     .)

   )

   (. proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); .)

@@ -1047,12 +1047,12 @@ ImpliesExpression<bool noExplies, out Expr/*!*/ e0>
     ExpliesOp      (. if (noExplies)

                         this.SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");

                       x = t; .)

-    LogicalExpression<out e1> 

+    LogicalExpression<out e1>

                    (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .)

     /* loop because explies is left-associative */

     {

       ExpliesOp    (. x = t; .)

-      LogicalExpression<out e1> 

+      LogicalExpression<out e1>

                    (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .)

     }

   ]

@@ -1211,19 +1211,19 @@ ArrayExpression<out Expr/*!*/ e>
                   allArgs.Add(e);

                   store = false; bvExtract = false; .)

       [

-        Expression<out index0> 

+        Expression<out index0>

                (. if (index0 is BvBounds)

                     bvExtract = true;

                   else

                     allArgs.Add(index0);

                .)

-        { "," Expression<out e1> 

+        { "," Expression<out e1>

                (. if (bvExtract || e1 is BvBounds)

                     this.SemErr("bitvectors only have one dimension");

                   allArgs.Add(e1);

                .)

         }

-        [ ":=" Expression<out e1> 

+        [ ":=" Expression<out e1>

                (. if (bvExtract || e1 is BvBounds)

                     this.SemErr("assignment to bitvectors is not possible");

                   allArgs.Add(e1); store = true;

@@ -1239,7 +1239,7 @@ ArrayExpression<out Expr/*!*/ e>
                                ((BvBounds)index0).Upper.ToIntSafe,

                                ((BvBounds)index0).Lower.ToIntSafe);

        else

-         e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs); 

+         e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);

     .)

   }

   .

@@ -1282,11 +1282,11 @@ AtomExpression<out Expr/*!*/ e>
                                             (. if (typeParams.Length + ds.Length > 0)

                                                  e = new ForallExpr(x, typeParams, ds, kv, trig, e); .)

         | Exists                            (. x = t; .)

-          QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e> 

+          QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e>

                                             (. if (typeParams.Length + ds.Length > 0)

                                                  e = new ExistsExpr(x, typeParams, ds, kv, trig, e); .)

         | Lambda                            (. x = t; .)

-          QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e> 

+          QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e>

                                             (. if (trig != null)

                                                  SemErr("triggers not allowed in lambda expressions");

                                                if (typeParams.Length + ds.Length > 0)

@@ -1404,7 +1404,7 @@ AttributeParameter<out object/*!*/ o>
 IfThenElseExpression<out Expr/*!*/ e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

      IToken/*!*/ tok;

-     Expr/*!*/ e0, e1, e2; 

+     Expr/*!*/ e0, e1, e2;

      e = dummyExpr; .)

   "if" (. tok = t; .) Expression<out e0> "then" Expression<out e1> "else" Expression<out e2>

   (. e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); .)

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4a9c531b..56116601 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -72,12 +72,12 @@ namespace Microsoft.Boogie {
       }

     }

 

-    private static CommandLineOptions clo = new CommandLineOptions(); 

+    private static CommandLineOptions clo = new CommandLineOptions();

     public static CommandLineOptions/*!*/ Clo

     {

       get { return clo; }

     }

-    

+

     public string/*!*/ Environment = "";

     public string/*!*/ FileName = "unknown";

 

@@ -450,7 +450,7 @@ namespace Microsoft.Boogie {
 

     [Verify(false)]

     private CommandLineOptions() {

-      // this is just to suppress verification. 

+      // this is just to suppress verification.

     }

 

     [Verify(false)]

@@ -1170,7 +1170,7 @@ namespace Microsoft.Boogie {
             }

             break;

           case "-recursionBound":

-          case "/recursionBound": 

+          case "/recursionBound":

             if(ps.ConfirmArgumentCount(1)){

               RecursionBound = Int32.Parse(cce.NonNull(args[ps.i]));

             }

@@ -1918,7 +1918,7 @@ namespace Microsoft.Boogie {
   ---- On axioms -------------------------------------------------------------

 

     {:inline true}

-      Works on axiom of the form: 

+      Works on axiom of the form:

         (forall VARS :: f(VARS) = expr(VARS))

       Makes Boogie replace f(VARS) with expr(VARS) everywhere just before

       doing VC generation.

@@ -1934,36 +1934,36 @@ namespace Microsoft.Boogie {
   ---- On implementations and procedures -------------------------------------

 

      {:inline N}

-       Inline given procedure (can be also used on implementation). 

-       N should be a non-negative number and represents the inlining depth. 

+       Inline given procedure (can be also used on implementation).

+       N should be a non-negative number and represents the inlining depth.

        With /inline:assume call is replaced with ""assume false"" once inlining depth is reached.

        With /inline:assert call is replaced with ""assert false"" once inlining depth is reached.

        With /inline:spec call is left as is once inlining depth is reached.

        With the above three options, methods with the attribute {:inline N} are not verified.

-       With /inline:none the entire attribute is ignored. 

-       

+       With /inline:none the entire attribute is ignored.

+

      {:verify false}

        Skip verification of an implementation.

-       

+

      {:forceBvZ3Native true}

        Verify the given implementation with the native Z3 bitvector

        handling. Only works if /bv:i (or /bv:z, but then it does not do

        anything) is given on the command line.

-       

+

      {:forceBvInt true}

        Use int translation for the given implementation. Only work with

        /bv:z (or /bv:i).

-       

+

      {:vcs_max_cost N}

      {:vcs_max_splits N}

      {:vcs_max_keep_going_splits N}

-       Per-implementation versions of 

+       Per-implementation versions of

        /vcsMaxCost, /vcsMaxSplits and /vcsMaxKeepGoingSplits.

 

      {:selective_checking true}

        Turn all asserts into assumes except for the ones reachable from

        assumptions marked with the attribute {:start_checking_here}.

-       Thus, ""assume {:start_checking_here} something;"" becomes an inverse 

+       Thus, ""assume {:start_checking_here} something;"" becomes an inverse

        of ""assume false;"": the first one disables all verification before

        it, and the second one disables all verification after.

 

@@ -1971,7 +1971,7 @@ namespace Microsoft.Boogie {
 

      {:bvbuiltin ""spec""}

        Z3 specific, used only with /bv:z.

-       

+

      {:bvint ""fn""}

        With /bv:i rewrite the function to function symbol 'fn', except if

        the 'fn' is 'id', in which case just strip the function altogether.

@@ -1996,7 +1996,7 @@ namespace Microsoft.Boogie {
 

      {:subsumption n}

        Overrides the /subsumption command-line setting for this assertion.

-       

+

   ---- The end ---------------------------------------------------------------

 ");

     }

@@ -2099,7 +2099,7 @@ namespace Microsoft.Boogie {
                               t = trivial (implied by /methodology:vs)

   /printModel:<n> : 0 (default) - do not print Z3's error model

                     1 - print Z3's error model

-                    2 - print Z3's error model plus reverse mappings         

+                    2 - print Z3's error model plus reverse mappings

                     4 - print Z3's error model in a more human readable way

   /printModelToFile:<file> : print model to <file> instead of console

   /mv:<file>        Specify file where to save the model in BVD format

@@ -2107,7 +2107,7 @@ namespace Microsoft.Boogie {
                                1 - Z3 error model enhanced error messages

 

   ---- Dafny options ---------------------------------------------------------

-  

+

   Multiple .dfy files supplied on the command line are concatenated into one

   Dafny program.

 

@@ -2137,7 +2137,7 @@ namespace Microsoft.Boogie {
                    identifies variables

   /printUnstructured : with /print option, desugars all structured statements

   /printDesugared : with /print option, desugars calls

-  

+

   /overlookTypeErrors : skip any implementation with resolution or type

                         checking errors

 

@@ -2152,7 +2152,7 @@ namespace Microsoft.Boogie {
                                           + @"

                    <flags> are as follows (missing <flags> means all)

                    i = intervals

-                   c = constant propagation        

+                   c = constant propagation

                    d = dynamic type

                    n = nullness

                    p = polyhedra for linear inequalities

@@ -2186,8 +2186,8 @@ namespace Microsoft.Boogie {
   /break[:method] : break into debugger

 

   ---- Verification-condition generation options -----------------------------

-  

-  /liveVariableAnalysis:<c> : 0 = do not perform live variable analysis 

+

+  /liveVariableAnalysis:<c> : 0 = do not perform live variable analysis

                               1 = perform live variable analysis (default)

                               2 = perform interprocedural live variable analysis

   /noVerify      : skip VC generation and invocation of the theorem prover

@@ -2211,25 +2211,25 @@ namespace Microsoft.Boogie {
                    n = none

                    z = native Z3 bitvectors (default)

                    i = unsoundly translate bitvectors to integers

-  /inline:<i>    : use inlining strategy <i> for procedures with the :inline 

+  /inline:<i>    : use inlining strategy <i> for procedures with the :inline

                    attribute, see /attrHelp for details:

                    none

                    assume (default)

                    assert

                    spec

-  /printInlined  : print the implementation after inlining calls to 

+  /printInlined  : print the implementation after inlining calls to

                    procedures with the :inline attribute (works with /inline)

   /lazyInline:1  : Use the lazy inlining algorithm

   /stratifiedInline:1 : Use the stratified inlining algorithm

-  /recursionBound:<n> : Set the recursion bound for stratified inlining to 

+  /recursionBound:<n> : Set the recursion bound for stratified inlining to

                         be n (default 500)

   /inferLeastForUnsat:<str> : Infer the least number of constants (whose names

-                              are prefixed by <str>) that need to be set to 

+                              are prefixed by <str>) that need to be set to

                               true for the program to be correct. This turns

                               on stratified inlining.

-  /smoke         : Soundness Smoke Test: try to stick assert false; in some 

+  /smoke         : Soundness Smoke Test: try to stick assert false; in some

                    places in the BPL and see if we can still prove it

-  /smokeTimeout:<n> : Timeout, in seconds, for a single theorem prover 

+  /smokeTimeout:<n> : Timeout, in seconds, for a single theorem prover

                    invocation during smoke test, defaults to 10.

   /causalImplies : Translate Boogie's A ==> B into prover's A ==> A && B.

   /typeEncoding:<m> : how to encode types when sending VC to theorem prover

@@ -2247,38 +2247,38 @@ namespace Microsoft.Boogie {
   /vcsMaxCost:<f>   : VC will not be split unless the cost of a VC exceeds this

                       number, defaults to 2000.0. This does NOT apply in the

                       keep-going mode after first round of splitting.

-  /vcsMaxSplits:<n> : Maximal number of VC generated per method. In keep 

+  /vcsMaxSplits:<n> : Maximal number of VC generated per method. In keep

                       going mode only applies to the first round.

                       Defaults to 1.

-  /vcsMaxKeepGoingSplits:<n> : If set to more than 1, activates the keep 

+  /vcsMaxKeepGoingSplits:<n> : If set to more than 1, activates the keep

                       going mode, where after the first round of splitting,

                       VCs that timed out are split into <n> pieces and retried

-                      until we succeed proving them, or there is only one 

+                      until we succeed proving them, or there is only one

                       assertion on a single path and it timeouts (in which

-                      case error is reported for that assertion). 

+                      case error is reported for that assertion).

                       Defaults to 1.

   /vcsKeepGoingTimeout:<n> : Timeout in seconds for a single theorem prover

                       invocation in keep going mode, except for the final

                       single-assertion case. Defaults to 1s.

-  /vcsFinalAssertTimeout:<n> : Timeout in seconds for the single last 

+  /vcsFinalAssertTimeout:<n> : Timeout in seconds for the single last

                       assertion in the keep going mode. Defaults to 30s.

   /vcsPathJoinMult:<f> : If more than one path join at a block, by how much

                       multiply the number of paths in that block, to accomodate

                       for the fact that the prover will learn something on one

                       paths, before proceeding to another. Defaults to 0.8.

   /vcsPathCostMult:<f1>

-  /vcsAssumeMult:<f2> : The cost of a block is 

+  /vcsAssumeMult:<f2> : The cost of a block is

          (<assert-cost> + <f2>*<assume-cost>)*(1.0 + <f1>*<entering-paths>)

                       <f1> defaults to 1.0, <f2> defaults to 0.01.

-                      The cost of a single assertion or assumption is 

+                      The cost of a single assertion or assumption is

                       currently always 1.0.

-  /vcsPathSplitMult:<f> : If the best path split of a VC of cost A is into 

+  /vcsPathSplitMult:<f> : If the best path split of a VC of cost A is into

                       VCs of cost B and C, then the split is applied if

-                      A >= <f>*(B+C), otherwise assertion splitting will be 

-                      applied. Defaults to 0.5 (always do path splitting if 

+                      A >= <f>*(B+C), otherwise assertion splitting will be

+                      applied. Defaults to 0.5 (always do path splitting if

                       possible), set to more to do less path splitting

                       and more assertion splitting.

-  /vcsDumpSplits      For split #n dump split.n.dot and split.n.bpl. 

+  /vcsDumpSplits      For split #n dump split.n.dot and split.n.bpl.

                       Warning: Affects error reporting.

   /vcsCores:<n>     : Try to verify <n> VCs at once. Defaults to 1.

 

@@ -2292,10 +2292,10 @@ namespace Microsoft.Boogie {
                     1 (default) - include useful Trace labels in error output,

                     2 - include all Trace labels in the error output

   /vcBrackets:<b> : bracket odd-charactered identifier names with |'s.  <b> is:

-                   0 - no (default with /prover:Z3), 

+                   0 - no (default with /prover:Z3),

                    1 - yes (default with /prover:Simplify)

   /prover:<tp>   : use theorem prover <tp>, where <tp> is either the name of

-                   a DLL containing the prover interface located in the 

+                   a DLL containing the prover interface located in the

                    Boogie directory, or a full path to a DLL containing such

                    an interface. The standard interfaces shipped include:

                    Z3 (default)

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index cab72087..9c208b86 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -64,7 +64,7 @@ Contract.Requires(cce.NonNullElements(defines,true));
   return ret;

 }

 

-  

+

 public static int Parse (Stream stream, string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

 Contract.Requires(stream != null);

 Contract.Requires(filename != null);

@@ -283,41 +283,41 @@ private class BvBounds : Expr {
 		}

 		bool makeClone = false;

 		foreach(TypedIdent/*!*/ x in xs){

-		  Contract.Assert(x != null);

+		 Contract.Assert(x != null);

+		

+		 // ensure that no sharing is introduced

+		 List<ConstantParent/*!*/> ParentsClone;

+		 if (makeClone && Parents != null) {

+		   ParentsClone = new List<ConstantParent/*!*/> ();

+		   foreach (ConstantParent/*!*/ p in Parents){

+		     Contract.Assert(p != null);

+		     ParentsClone.Add(new ConstantParent (

+		                      new IdentifierExpr (p.Parent.tok, p.Parent.Name),

+		                      p.Unique));}

+		 } else {

+		   ParentsClone = Parents;

+		 }

+		 makeClone = true;

 		

-		       // ensure that no sharing is introduced

-		       List<ConstantParent/*!*/> ParentsClone;

-		       if (makeClone && Parents != null) {

-		         ParentsClone = new List<ConstantParent/*!*/> ();

-		         foreach (ConstantParent/*!*/ p in Parents){

-		           Contract.Assert(p != null);

-		           ParentsClone.Add(new ConstantParent (

-		                            new IdentifierExpr (p.Parent.tok, p.Parent.Name),

-		                            p.Unique));}

-		       } else {

-		         ParentsClone = Parents;

-		       }

-		       makeClone = true;

+		 ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));

+		}

 		

-		       ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));

-		     }

-		  

 		Expect(7);

 	}

 

 	void Function(out DeclarationSeq/*!*/ ds) {

 		Contract.Ensures(Contract.ValueAtReturn(out ds) != null);

 		ds = new DeclarationSeq(); IToken/*!*/ z;

-		     IToken/*!*/ typeParamTok;

-		     TypeVariableSeq/*!*/ typeParams = new TypeVariableSeq();

-		     VariableSeq arguments = new VariableSeq();

-		     TypedIdent/*!*/ tyd;

-		     TypedIdent retTyd = null;

-		     Type/*!*/ retTy;

-		     QKeyValue kv = null;

-		     Expr definition = null;

-		     Expr/*!*/ tmp;

-		  

+		IToken/*!*/ typeParamTok;

+		TypeVariableSeq/*!*/ typeParams = new TypeVariableSeq();

+		VariableSeq arguments = new VariableSeq();

+		TypedIdent/*!*/ tyd;

+		TypedIdent retTyd = null;

+		Type/*!*/ retTy;

+		QKeyValue kv = null;

+		Expr definition = null;

+		Expr/*!*/ tmp;

+		

 		Expect(23);

 		while (la.kind == 25) {

 			Attribute(ref kv);

@@ -360,78 +360,78 @@ private class BvBounds : Expr {
 		 // construct a dummy type for the case of syntax error

 		 tyd = new TypedIdent(t, "", new BasicType(t, SimpleType.Int));

 		} else {

-		  tyd = retTyd;

+		 tyd = retTyd;

 		}

 		Function/*!*/ func = new Function(z, z.val, typeParams, arguments,

-		                       new Formal(tyd.tok, tyd, false), null, kv);

+		                      new Formal(tyd.tok, tyd, false), null, kv);

 		Contract.Assert(func != null);

 		ds.Add(func);

 		bool allUnnamed = true;

 		foreach(Formal/*!*/ f in arguments){

-		  Contract.Assert(f != null);

-		  if (f.TypedIdent.Name != "") {

-		    allUnnamed = false;

+		 Contract.Assert(f != null);

+		 if (f.TypedIdent.Name != "") {

+		   allUnnamed = false;

 		break;

-		     }

-		   }

-		   if (!allUnnamed) {

-		     Type prevType = null;

-		     for (int i = arguments.Length - 1; i >= 0; i--) {

-		       TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;

-		       if (curr.Name == "") {

-		  if (prevType == null) {

-		    this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");

-		    break;

-		  }

-		  Type ty = curr.Type;

-		         if (ty is UnresolvedTypeIdentifier &&

-		             cce.NonNull(ty as UnresolvedTypeIdentifier).Arguments.Length == 0) {

-		    curr.Name = cce.NonNull(ty as UnresolvedTypeIdentifier).Name;

-		    curr.Type = prevType;

-		  } else {

-		    this.errors.SemErr(curr.tok, "expecting an identifier as parameter name");

-		  }

+		 }

+		}

+		if (!allUnnamed) {

+		 Type prevType = null;

+		 for (int i = arguments.Length - 1; i >= 0; i--) {

+		   TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;

+		   if (curr.Name == "") {

+		if (prevType == null) {

+		this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");

+		break;

+		}

+		Type ty = curr.Type;

+		     if (ty is UnresolvedTypeIdentifier &&

+		         cce.NonNull(ty as UnresolvedTypeIdentifier).Arguments.Length == 0) {

+		curr.Name = cce.NonNull(ty as UnresolvedTypeIdentifier).Name;

+		curr.Type = prevType;

 		} else {

-		  prevType = curr.Type;

+		this.errors.SemErr(curr.tok, "expecting an identifier as parameter name");

 		}

-		     }

+		} else {

+		prevType = curr.Type;

+		}

+		 }

+		}

+		if (definition != null) {

+		 // generate either an axiom or a function body

+		 if (QKeyValue.FindBoolAttribute(kv, "inline")) {

+		   func.Body = definition;

+		 } else {

+		   VariableSeq dummies = new VariableSeq();

+		   ExprSeq callArgs = new ExprSeq();

+		   int i = 0;

+		   foreach(Formal/*!*/ f in arguments){

+		     Contract.Assert(f != null);

+		     string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;

+		     dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));

+		     callArgs.Add(new IdentifierExpr(f.tok, nm));

+		     i++;

+		   }

+		   TypeVariableSeq/*!*/ quantifiedTypeVars = new TypeVariableSeq ();

+		   foreach(TypeVariable/*!*/ t in typeParams){

+		     Contract.Assert(t != null);

+		     quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));

 		   }

-		   if (definition != null) {

-		     // generate either an axiom or a function body

-		     if (QKeyValue.FindBoolAttribute(kv, "inline")) {

-		       func.Body = definition;

-		     } else {

-		       VariableSeq dummies = new VariableSeq();

-		       ExprSeq callArgs = new ExprSeq();

-		       int i = 0;

-		       foreach(Formal/*!*/ f in arguments){

-		         Contract.Assert(f != null);

-		         string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;

-		         dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));

-		         callArgs.Add(new IdentifierExpr(f.tok, nm));

-		         i++;

-		       }

-		       TypeVariableSeq/*!*/ quantifiedTypeVars = new TypeVariableSeq ();

-		       foreach(TypeVariable/*!*/ t in typeParams){

-		         Contract.Assert(t != null);

-		         quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));

-		       }

 		

-		        Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);

-		        // specify the type of the function, because it might be that

-		        // type parameters only occur in the output type

-		        call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone());

-		        Expr def = Expr.Eq(call, definition);

-		        if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

-		          def = new ForallExpr(z, quantifiedTypeVars, dummies,

-		                               kv,

-		                               new Trigger(z, true, new ExprSeq(call), null),

-		                               def);

-		        }

-		        ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));

-		      }

-		    }

-		  

+		   Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);

+		   // specify the type of the function, because it might be that

+		   // type parameters only occur in the output type

+		   call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone());

+		   Expr def = Expr.Eq(call, definition);

+		   if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

+		     def = new ForallExpr(z, quantifiedTypeVars, dummies,

+		                          kv,

+		                          new Trigger(z, true, new ExprSeq(call), null),

+		                          def);

+		   }

+		   ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));

+		 }

+		}

+		

 	}

 

 	void Axiom(out Axiom/*!*/ m) {

@@ -485,11 +485,11 @@ private class BvBounds : Expr {
 		IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();

 		EnsuresSeq/*!*/ post = new EnsuresSeq();

 		

-		     VariableSeq/*!*/ locals = new VariableSeq();

-		     StmtList/*!*/ stmtList;

-		     QKeyValue kv = null;

-		     impl = null;

-		  

+		VariableSeq/*!*/ locals = new VariableSeq();

+		StmtList/*!*/ stmtList;

+		QKeyValue kv = null;

+		impl = null;

+		

 		Expect(30);

 		ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);

 		if (la.kind == 7) {

@@ -503,7 +503,7 @@ private class BvBounds : Expr {
 			}

 			ImplBody(out locals, out stmtList);

 			impl = new Implementation(x, x.val, typeParams,

-			                         Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors); 

+			                         Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);

 			

 		} else SynErr(91);

 		proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); 

@@ -584,8 +584,8 @@ private class BvBounds : Expr {
 		Type(out ty);

 		tyds = new TypedIdentSeq();

 		foreach(Token/*!*/ id in ids){

-		  Contract.Assert(id != null);

-		  tyds.Add(new TypedIdent(id, id.val, ty, null));

+		 Contract.Assert(id != null);

+		 tyds.Add(new TypedIdent(id, id.val, ty, null));

 		}

 		

 	}

@@ -628,7 +628,7 @@ private class BvBounds : Expr {
 			if (allowWhereClauses) {

 			 wh = nne;

 			} else {

-			  this.SemErr("where clause not allowed here");

+			 this.SemErr("where clause not allowed here");

 			}

 			

 		}

@@ -670,7 +670,7 @@ private class BvBounds : Expr {
 		Expect(1);

 		x = t;

 		if (x.val.StartsWith("\\"))

-		  x.val = x.val.Substring(1);

+		 x.val = x.val.Substring(1);

 		

 	}

 

@@ -725,8 +725,8 @@ private class BvBounds : Expr {
 		Expect(18);

 		typeParams = new TypeVariableSeq ();

 		foreach(Token/*!*/ id in typeParamToks){

-		  Contract.Assert(id != null);

-		  typeParams.Add(new TypeVariable(id, id.val));}

+		 Contract.Assert(id != null);

+		 typeParams.Add(new TypeVariable(id, id.val));}

 		

 	}

 

@@ -785,7 +785,7 @@ private class BvBounds : Expr {
 			   cce.NonNull(ty as UnresolvedTypeIdentifier).Arguments.Length == 0) {

 			 varName = cce.NonNull(ty as UnresolvedTypeIdentifier).Name;

 			} else {

-			  this.SemErr("expected identifier before ':'");

+			 this.SemErr("expected identifier before ':'");

 			}

 			

 			Type(out ty);

@@ -817,7 +817,7 @@ private class BvBounds : Expr {
 		   typeParams.Add(new TypeVariable(t, t.val));}

 		 decl = new TypeSynonymDecl(id, id.val, typeParams, body, kv);

 		} else {

-		  decl = new TypeCtorDecl(id, id.val, paramTokens.Length, kv);

+		 decl = new TypeCtorDecl(id, id.val, paramTokens.Length, kv);

 		}

 		

 	}

@@ -924,18 +924,18 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				 Contract.Assert(cs != null);

 				 cs.Add(c);

 				} else {

-				  // LabelOrCmd read a label

-				  Contract.Assert(label != null);

-				  if (startToken != null) {

-				    Contract.Assert(cs != null);

-				    // dump the built-up state into a BigBlock

-				    b = new BigBlock(startToken, currentLabel, cs, null, null);

-				    bigblocks.Add(b);

-				    cs = null;

-				  }

-				  startToken = label;

-				  currentLabel = label.val;

-				  cs = new CmdSeq();

+				 // LabelOrCmd read a label

+				 Contract.Assert(label != null);

+				 if (startToken != null) {

+				   Contract.Assert(cs != null);

+				   // dump the built-up state into a BigBlock

+				   b = new BigBlock(startToken, currentLabel, cs, null, null);

+				   bigblocks.Add(b);

+				   cs = null;

+				 }

+				 startToken = label;

+				 currentLabel = label.val;

+				 cs = new CmdSeq();

 				}

 				

 			} else if (la.kind == 38 || la.kind == 40 || la.kind == 43) {

@@ -961,16 +961,16 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		Expect(26);

 		IToken/*!*/ endCurly = t;

 		if (startToken == null && bigblocks.Count == 0) {

-		  startToken = t;  cs = new CmdSeq();

+		 startToken = t;  cs = new CmdSeq();

 		}

 		if (startToken != null) {

-		  Contract.Assert(cs != null);

-		  b = new BigBlock(startToken, currentLabel, cs, null, null);

-		  bigblocks.Add(b);

+		 Contract.Assert(cs != null);

+		 b = new BigBlock(startToken, currentLabel, cs, null, null);

+		 bigblocks.Add(b);

 		}

 		

-		     stmtList = new StmtList(bigblocks, endCurly);

-		  

+		stmtList = new StmtList(bigblocks, endCurly);

+		

 	}

 

 	void LabelOrCmd(out Cmd c, out IToken label) {

@@ -1008,8 +1008,8 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 			Expect(7);

 			ids = new IdentifierExprSeq();

 			foreach(IToken/*!*/ y in xs){

-			  Contract.Assert(y != null);

-			  ids.Add(new IdentifierExpr(y, y.val));

+			 Contract.Assert(y != null);

+			 ids.Add(new IdentifierExpr(y, y.val));

 			}

 			c = new HavocCmd(x,ids);

 			

@@ -1104,7 +1104,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 			if (isFree) {

 			 invariants.Add(new AssumeCmd(z, e));

 			} else {

-			  invariants.Add(new AssertCmd(z, e));

+			 invariants.Add(new AssertCmd(z, e));

 			}

 			

 			Expect(7);

@@ -1223,7 +1223,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 					if (p==null) {

 					  ids.Add(null);

 					} else {

-					   ids.Add(new IdentifierExpr(p, p.val));

+					  ids.Add(new IdentifierExpr(p, p.val));

 					}

 					

 					while (la.kind == 11) {

@@ -1232,7 +1232,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 						if (p==null) {

 						  ids.Add(null);

 						} else {

-						   ids.Add(new IdentifierExpr(p, p.val));

+						  ids.Add(new IdentifierExpr(p, p.val));

 						}

 						

 					}

@@ -1277,7 +1277,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				if (p==null) {

 				  ids.Add(null);

 				} else {

-				   ids.Add(new IdentifierExpr(p, p.val));

+				  ids.Add(new IdentifierExpr(p, p.val));

 				}

 				

 				while (la.kind == 11) {

@@ -1286,7 +1286,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 					if (p==null) {

 					  ids.Add(null);

 					} else {

-					   ids.Add(new IdentifierExpr(p, p.val));

+					  ids.Add(new IdentifierExpr(p, p.val));

 					}

 					

 				}

@@ -1625,7 +1625,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				 this.SemErr("arguments of extract need to be integer literals");

 				 e = new BvBounds(x, bn, BigNum.ZERO);

 				} else {

-				  e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);

+				 e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);

 				}

 				

 			} else SynErr(117);

@@ -1650,7 +1650,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 					if (index0 is BvBounds)

 					 bvExtract = true;

 					else

-					  allArgs.Add(index0);

+					 allArgs.Add(index0);

 					

 					while (la.kind == 11) {

 						Get();

@@ -1678,11 +1678,11 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 			if (store)

 			 e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs);

 			else if (bvExtract)

-			  e = new BvExtractExpr(x, e,

-			                        ((BvBounds)index0).Upper.ToIntSafe,

-			                        ((BvBounds)index0).Lower.ToIntSafe);

+			 e = new BvExtractExpr(x, e,

+			                       ((BvBounds)index0).Upper.ToIntSafe,

+			                       ((BvBounds)index0).Lower.ToIntSafe);

 			else

-			  e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs); 

+			 e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);

 			

 		}

 	}

@@ -1692,8 +1692,8 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		try {

 		 n = BigNum.FromString(t.val);

 		} catch (FormatException) {

-		  this.SemErr("incorrectly formatted number");

-		  n = BigNum.ZERO;

+		 this.SemErr("incorrectly formatted number");

+		 n = BigNum.ZERO;

 		}

 		

 	}

@@ -1779,7 +1779,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				if (trig != null)

 				 SemErr("triggers not allowed in lambda expressions");

 				if (typeParams.Length + ds.Length > 0)

-				  e = new LambdaExpr(x, typeParams, ds, kv, e); 

+				 e = new LambdaExpr(x, typeParams, ds, kv, e); 

 			} else SynErr(119);

 			Expect(9);

 			break;

@@ -1803,12 +1803,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		string a = t.val.Substring(0, pos);

 		string b = t.val.Substring(pos + 2);

 		try {

-		  n = BigNum.FromString(a);

-		  m = Convert.ToInt32(b);

+		 n = BigNum.FromString(a);

+		 m = Convert.ToInt32(b);

 		} catch (FormatException) {

-		  this.SemErr("incorrectly formatted bitvector");

-		  n = BigNum.ZERO;

-		  m = 0;

+		 this.SemErr("incorrectly formatted bitvector");

+		 n = BigNum.ZERO;

+		 m = 0;

 		}

 		

 	}

@@ -1825,10 +1825,10 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {

 		Contract.Requires(q != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ds) != null); Contract.Ensures(Contract.ValueAtReturn(out body) != null);

 		trig = null; typeParams = new TypeVariableSeq ();

-		     IToken/*!*/ tok;

-		     kv = null;

-		     ds = new VariableSeq ();

-		  

+		IToken/*!*/ tok;

+		kv = null;

+		ds = new VariableSeq ();

+		

 		if (la.kind == 17) {

 			TypeParams(out tok, out typeParams);

 			if (la.kind == 1) {

@@ -1863,7 +1863,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 	void IfThenElseExpression(out Expr/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null);

 		IToken/*!*/ tok;

-		Expr/*!*/ e0, e1, e2; 

+		Expr/*!*/ e0, e1, e2;

 		e = dummyExpr; 

 		Expect(38);

 		tok = t; 

@@ -1909,8 +1909,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 			 Contract.Assert(label == null);

 			 cs.Add(c);

 			} else {

-			  Contract.Assert(label != null);

-			  SemErr("SpecBlock's can only have one label");

+			 Contract.Assert(label != null);

+			 SemErr("SpecBlock's can only have one label");

 			}

 			

 		}

@@ -1963,11 +1963,11 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 			   this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter");

 			 }

 			} else {

-			  if (kv==null) {

-			    kv = new QKeyValue(tok, key, parameters, null);

-			  } else {

-			    kv.AddLast(new QKeyValue(tok, key, parameters, null));

-			  }

+			 if (kv==null) {

+			   kv = new QKeyValue(tok, key, parameters, null);

+			 } else {

+			   kv.AddLast(new QKeyValue(tok, key, parameters, null));

+			 }

 			}

 			

 		} else if (StartOf(7)) {

@@ -1981,7 +1981,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 			if (trig==null) {

 			 trig = new Trigger(tok, true, es, null);

 			} else {

-			  trig.AddLast(new Trigger(tok, true, es, null));

+			 trig.AddLast(new Trigger(tok, true, es, null));

 			}

 			

 		} else SynErr(126);

@@ -2017,6 +2017,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		la.val = "";

 		Get();

 		BoogiePL();

+		Expect(0);

 

 		Expect(0);

 	}

@@ -2219,4 +2220,5 @@ public class FatalError: Exception {
 	public FatalError(string m): base(m) {}

 }

 

+

 }
\ No newline at end of file
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index 7c3522ca..e3d131e0 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -232,6 +232,7 @@ public class Scanner {
 	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;

@@ -440,7 +441,7 @@ public class Scanner {
 

 

 	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();

@@ -453,13 +454,13 @@ public class Scanner {
 				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();

@@ -480,7 +481,7 @@ public class Scanner {
 				else NextCh();

 			}

 		} else {

-			buffer.Pos = pos0; NextCh(); line = line0; col = col0;

+			buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0;

 		}

 		return false;

 	}

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index d61d653d..0653fe2e 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -19,13 +19,13 @@ namespace Microsoft.Dafny {
     }

 

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(wr!=null);

     }

 

     TextWriter wr;

-    

+

     public int ErrorCount;

     void Error(string msg, params object[] args) {Contract.Requires(msg != null);

       string s = string.Format("Compilation error: " + msg, args);

@@ -33,7 +33,7 @@ namespace Microsoft.Dafny {
       wr.WriteLine("/* {0} */", s);

       ErrorCount++;

     }

-    

+

     void ReadRuntimeSystem() {

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

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

@@ -226,7 +226,7 @@ namespace Microsoft.Dafny {
         Indent(indent);  wr.WriteLine("}");

       }

     }

-    

+

     void CompileDatatypeStruct(DatatypeDecl dt, int indent) {

       Contract.Requires(dt != null);

 

@@ -254,23 +254,23 @@ namespace Microsoft.Dafny {
       if (dt.TypeArgs.Count != 0) {

         DtT += "<" + TypeParameters(dt.TypeArgs) + ">";

       }

-      

+

       Indent(indent);

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

       int ind = indent + IndentAmount;

-      

+

       Indent(ind);

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

-      

+

       Indent(ind);

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

       Indent(ind + IndentAmount);

       wr.WriteLine("get { if (d == null) { d = Default; } return d; }");

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

-      

+

       Indent(ind);

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

-      

+

       Indent(ind);

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

       Indent(ind + IndentAmount);

@@ -320,7 +320,7 @@ namespace Microsoft.Dafny {
       Indent(indent);

       wr.WriteLine("}");

     }

-    

+

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

     {

       Contract.Requires(sep != null);

@@ -336,20 +336,20 @@ namespace Microsoft.Dafny {
       }

       return i;  // the number of formals written

     }

-    

+

     string FormalName(Formal formal, int i) {

       Contract.Requires(formal != null);

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

 

       return formal.HasName ? formal.Name : "_a" + i;

     }

-    

+

     string DtCtorName(DatatypeCtor ctor) {

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

 

       return cce.NonNull(ctor.EnclosingDatatype).Name + "_" + ctor.Name;

     }

-        

+

     void CompileClassMembers(ClassDecl c, int indent)

     {

       Contract.Requires(c != null);

@@ -360,7 +360,7 @@ namespace Microsoft.Dafny {
             Indent(indent);

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

           }

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           if (f.IsGhost) {

@@ -379,7 +379,7 @@ namespace Microsoft.Dafny {
             CompileReturnBody(f.Body, indent);

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

           }

-          

+

         } else if (member is Method) {

           Method m = (Method)member;

           if (!m.IsGhost) {

@@ -483,10 +483,10 @@ namespace Microsoft.Dafny {
     }

 

     // ----- Type ---------------------------------------------------------------------------------

-    

+

     readonly string DafnySetClass = "Dafny.Set";

     readonly string DafnySeqClass = "Dafny.Sequence";

-    

+

     string TypeName(Type type)

     {

       Contract.Requires(type != null);

@@ -503,7 +503,7 @@ namespace Microsoft.Dafny {
           type = tp.T;

         }

       }

-      

+

       if (type is BoolType) {

         return "bool";

       } else if (type is IntType) {

@@ -558,7 +558,7 @@ namespace Microsoft.Dafny {
       }

       return s;

     }

-    

+

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

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

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

@@ -571,7 +571,7 @@ namespace Microsoft.Dafny {
       }

       return s;

     }

-    

+

     string DefaultValue(Type type)

     {

       Contract.Requires(type != null);

@@ -588,7 +588,7 @@ namespace Microsoft.Dafny {
           type = tp.T;

         }

       }

-      

+

       if (type is BoolType) {

         return "false";

       } else if (type is IntType) {

@@ -613,16 +613,16 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

     }

-    

+

     // ----- Stmt ---------------------------------------------------------------------------------

-    

+

     void TrStmt(Statement stmt, int indent)

     {

       Contract.Requires(stmt != null);

       if (stmt.IsGhost) {

         return;

       }

-      

+

       if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

         foreach (Attributes.Argument arg in s.Args) {

@@ -723,19 +723,19 @@ namespace Microsoft.Dafny {
         } else {

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

         }

-        

+

       } else if (stmt is VarDecl) {

         TrVarDecl((VarDecl)stmt, true, indent);

-        

+

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

         TrCallStmt(s, null, indent);

-        

+

       } else if (stmt is BlockStmt) {

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

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

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

-        

+

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

         Indent(indent);

@@ -746,7 +746,7 @@ namespace Microsoft.Dafny {
           TrExpr(s.Guard);

           wr.WriteLine(")");

         }

-        

+

         TrStmt(s.Thn, indent);

         if (s.Els != null && s.Guard != null) {

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

@@ -816,20 +816,20 @@ namespace Microsoft.Dafny {
         tmpVarCount++;

         string TType = TypeName(s.BoundVar.Type);

         string RhsType = TypeName(cce.NonNull(s.BodyAssign.Lhs.Type));

-        

+

         Indent(indent);

         wr.WriteLine("List<Pair<{0},{1}>> {2} = new List<Pair<{0},{1}>>();", TType, RhsType, pu);

-        

+

         Indent(indent);

         wr.Write("foreach ({0} @{1} in (", TType, s.BoundVar.Name);

         TrExpr(s.Collection);

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

-        

+

         Indent(indent + IndentAmount);

         wr.Write("if (");

         TrExpr(s.Range);

         wr.WriteLine(") {");

-        

+

         foreach (PredicateStmt p in s.BodyPrefix) {

           TrStmt(p, indent + 2*IndentAmount);

         }

@@ -842,7 +842,7 @@ namespace Microsoft.Dafny {
           wr.Write(DefaultValue(s.BodyAssign.Lhs.Type));

         }

         wr.WriteLine("))");

-        

+

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

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

 

@@ -851,7 +851,7 @@ namespace Microsoft.Dafny {
         FieldSelectExpr fse = (FieldSelectExpr)s.BodyAssign.Lhs;

         wr.WriteLine("{0}.Car.{1} = {0}.Cdr;", pr, fse.FieldName);

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

-        

+

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         // Type source = e;

@@ -1035,16 +1035,16 @@ namespace Microsoft.Dafny {
       }

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

     }

-    

+

     int tmpVarCount = 0;

-    

+

     void TrAssignmentRhs(AssignmentRhs rhs) {

       Contract.Requires(rhs != null);

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

       if (rhs is ExprRhs) {

         ExprRhs e = (ExprRhs)rhs;

         TrExpr(e.Expr);

-        

+

       } else {

         TypeRhs tp = (TypeRhs)rhs;

         if (tp.ArrayDimensions == null) {

@@ -1074,7 +1074,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

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

       foreach (Statement ss in stmts) {

         TrStmt(ss, indent + IndentAmount);

@@ -1131,7 +1131,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-        

+

     // ----- Expression ---------------------------------------------------------------------------

 

     void TrParenExpr(string prefix, Expression expr) {

@@ -1147,7 +1147,7 @@ namespace Microsoft.Dafny {
       TrExpr(expr);

       wr.Write(")");

     }

-    

+

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

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

       wr.Write("(");

@@ -1179,26 +1179,26 @@ namespace Microsoft.Dafny {
         } else {

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

         }

-        

+

       } else if (expr is ThisExpr) {

         wr.Write("this");

-        

+

       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

         wr.Write("@" + e.Var.Name);

-      

+

       } else if (expr is SetDisplayExpr) {

         SetDisplayExpr e = (SetDisplayExpr)expr;

         Type elType = cce.NonNull((SetType)e.Type).Arg;

         wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType));

         TrExprList(e.Elements);

-        

+

       } else if (expr is SeqDisplayExpr) {

         SeqDisplayExpr e = (SeqDisplayExpr)expr;

         Type elType = cce.NonNull((SeqType)e.Type).Arg;

         wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));

         TrExprList(e.Elements);

-      

+

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr e = (FieldSelectExpr)expr;

         SpecialField sf = e.Field as SpecialField;

@@ -1211,7 +1211,7 @@ namespace Microsoft.Dafny {
           TrParenExpr(e.Obj);

           wr.Write(".@{0}", e.Field.Name);

         }

-        

+

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         TrParenExpr(e.Seq);

@@ -1233,7 +1233,7 @@ namespace Microsoft.Dafny {
             TrParenExpr(".Drop", e.E0);

           }

         }

-      

+

       } else if (expr is MultiSelectExpr) {

         MultiSelectExpr e = (MultiSelectExpr)expr;

         TrParenExpr(e.Array);

@@ -1253,7 +1253,7 @@ namespace Microsoft.Dafny {
         wr.Write(", ");

         TrExpr(e.Value);

         wr.Write(")");

-      

+

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         Function f = cce.NonNull(e.Function);

@@ -1273,7 +1273,7 @@ namespace Microsoft.Dafny {
           }

         }

         wr.Write(")");

-      

+

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved

@@ -1292,13 +1292,13 @@ namespace Microsoft.Dafny {
           }

         }

         wr.Write("))");

-          

+

       } else if (expr is OldExpr) {

         Contract.Assert(false); throw new cce.UnreachableException();  // 'old' is always a ghost (right?)

-      

+

       } else if (expr is FreshExpr) {

         Contract.Assert(false); throw new cce.UnreachableException();  // 'fresh' is always a ghost

-      

+

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         switch (e.Op) {

@@ -1323,13 +1323,13 @@ namespace Microsoft.Dafny {
           default:

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

         }

-      

+

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

         string opString = null;

         string preOpString = "";

         string callString = null;

-        

+

         switch (e.ResolvedOp) {

           case BinaryExpr.ResolvedOpcode.Iff:

             opString = "==";  break;

@@ -1339,7 +1339,7 @@ namespace Microsoft.Dafny {
             opString = "||";  break;

           case BinaryExpr.ResolvedOpcode.And:

             opString = "&&";  break;

-            

+

           case BinaryExpr.ResolvedOpcode.EqCommon: {

             Type t = cce.NonNull(e.E0.Type);

             if (t.IsDatatype || t.IsTypeParameter) {

@@ -1359,7 +1359,7 @@ namespace Microsoft.Dafny {
             }

             break;

           }

-            

+

           case BinaryExpr.ResolvedOpcode.Lt:

             opString = "<";  break;

           case BinaryExpr.ResolvedOpcode.Le:

@@ -1460,7 +1460,7 @@ namespace Microsoft.Dafny {
           TrExpr(e.E1);

           wr.Write(")");

         }

-      

+

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

         Contract.Assert(e.Bounds != null);  // for non-ghost quantifiers, the resolver would have insisted on finding bounds

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 15d39460..c0aae345 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -3,39 +3,29 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------*/

-

 /*---------------------------------------------------------------------------

 // Dafny

 // Rustan Leino, first created 25 January 2008

 //--------------------------------------------------------------------------*/

-

 using System.Collections.Generic;

 using System.Numerics;

 using Microsoft.Boogie;

 using System.IO;

 using System.Text;

-

-

 COMPILER Dafny

-

 /*--------------------------------------------------------------------------*/

-

 static List<ModuleDecl/*!*/> theModules;

 static BuiltIns theBuiltIns;

-

-

 static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);

 static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);

 static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);

 static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");

 static int anonymousIds = 0;

-

 struct MemberModifiers {

   public bool IsGhost;

   public bool IsStatic;

   public bool IsUnlimited;

 }

-

 // helper routine for parsing call statements

 private static Expression/*!*/ ConvertToLocal(Expression/*!*/ e)

 {

@@ -47,7 +37,6 @@ Contract.Ensures(Contract.Result<Expression>() != null);
   }

   return e;  // cannot convert to IdentifierExpr (or is already an IdentifierExpr)

 }

-

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members) from "filename"

 /// and appends them in appropriate form to "modules".

@@ -68,7 +57,6 @@ public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ module
     }

   }

 }

-

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members)

 /// and appends them in appropriate form to "modules".

@@ -82,7 +70,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   Errors errors = new Errors();

   return Parse(s, filename, modules, builtIns, errors);

 }

-

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members)

 /// and appends them in appropriate form to "modules".

@@ -108,7 +95,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   theBuiltIns = oldBuiltIns;

   return parser.errors.count;

 }

-

 /*--------------------------------------------------------------------------*/

 CHARACTERS

   letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".

@@ -116,25 +102,20 @@ CHARACTERS
   posDigit = "123456789".

   special = "'_?\\".

   glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".

-

   cr        = '\r'.

   lf        = '\n'.

   tab       = '\t'.

-

   space = ' '.

   quote = '"'.

-

   nondigit = letter + special.

   idchar = nondigit + digit.

   nonquote = letter + digit + space + glyph.

-

   /* exclude the characters in 'array' */

   nondigitMinusA = nondigit - 'a'.

   idcharMinusA = idchar - 'a'.

   idcharMinusR = idchar - 'r'.

   idcharMinusY = idchar - 'y'.

   idcharMinusPosDigit = idchar - posDigit.

-

 /*------------------------------------------------------------------------*/

 TOKENS

   ident =  nondigitMinusA {idchar}            /* if char 0 is not an 'a', then anything else is fine */

@@ -147,23 +128,16 @@ TOKENS
   digits = digit {digit}.

   arrayToken = 'a' 'r' 'r' 'a' 'y' [posDigit {digit}].

   string = quote {nonquote} quote.

-

 COMMENTS FROM "/*" TO "*/" NESTED

 COMMENTS FROM "//" TO lf

-

 IGNORE cr + lf + tab

-

-

 /*------------------------------------------------------------------------*/

 PRODUCTIONS

-

 Dafny

 = (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;

      Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;

-

      List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();

      ModuleDecl module;

-     

      // to support multiple files, create a default module only if theModules doesn't already contain one

      DefaultModuleDecl defaultModule = null;

      foreach (ModuleDecl mdecl in theModules) {

@@ -206,7 +180,6 @@ Dafny
   .)

   EOF

   .

-

 ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>

 = (. Contract.Requires(module != null);

      Contract.Ensures(Contract.ValueAtReturn(out c) != null);

@@ -227,16 +200,15 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
   "{"                                            (. bodyStart = t; .)

   { ClassMemberDecl<members, true>

   }

-  "}"                                      

-  (. if (optionalId == null)        

+  "}"

+  (. if (optionalId == null)

        c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);

-     else 

+     else

        c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

      c.BodyStartTok = bodyStart;

      c.BodyEndTok = t;

   .)

   .

-

 ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>

 = (. Contract.Requires(cce.NonNullElements(mm));

      Method/*!*/ m;

@@ -247,13 +219,12 @@ ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
   | "static"                               (. mmod.IsStatic = true; .)

   | "unlimited"                            (. mmod.IsUnlimited = true; .)

   }

-  ( FieldDecl<mmod, mm>  

+  ( FieldDecl<mmod, mm>

   | FunctionDecl<mmod, out f>                   (. mm.Add(f); .)

   | MethodDecl<mmod, allowConstructors, out m>  (. mm.Add(m); .)

-  | CouplingInvDecl<mmod, mm> 

+  | CouplingInvDecl<mmod, mm>

   )

   .

-

 DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>

 = (. Contract.Requires(module != null);

      Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);

@@ -276,7 +247,6 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
      dt.BodyEndTok = t;

   .)

   .

-

 DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>

 = (. Contract.Requires(cce.NonNullElements(ctors));

      Attributes attrs = null;

@@ -288,7 +258,6 @@ DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
   [ FormalsOptionalIds<formals> ]

   (. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .)

   .

-

 FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>

 = (. Contract.Requires(cce.NonNullElements(mm));

      Attributes attrs = null;

@@ -304,7 +273,6 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
   }

   ";"

   .

-

 CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>

 = (. Contract.Requires(cce.NonNullElements(mm));

      Attributes attrs = null;

@@ -317,17 +285,15 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
      if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }

      if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }

   .)

-  { Attribute<ref attrs> }  

+  { Attribute<ref attrs> }

   Ident<out id>                                     (. ids.Add(id); .)

   { "," Ident<out id>                               (. ids.Add(id); .)

   }

-  "by"    

+  "by"

   Expression<out e>

   ";"

-  (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)  

+  (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)

   .

-

-

 GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>

 /* isGhost always returns as false if allowGhostKeyword is false */

 = (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

@@ -337,14 +303,12 @@ GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out boo
   ]

   IdentType<out id, out ty>

   .

-

 IdentType<out IToken/*!*/ id, out Type/*!*/ ty>

 = (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)

   Ident<out id>

   ":"

   Type<out ty>

   .

-

 LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>

 = (. IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;

   .)

@@ -353,7 +317,6 @@ LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
   ]

   (. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)

   .

-

 IdentTypeOptional<out BoundVar/*!*/ var>

 = (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;

   .)

@@ -362,7 +325,6 @@ IdentTypeOptional<out BoundVar/*!*/ var>
   ]

   (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)

   .

-

 TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ ty, out bool isGhost>

 = (.Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

      Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);

@@ -389,9 +351,7 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t
      }

   .)

   .

-

 /*------------------------------------------------------------------------*/

-

 GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>

 = (. Contract.Requires(cce.NonNullElements(typeArgs));

      IToken/*!*/ id; .)

@@ -401,9 +361,7 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
   }

   ">"

   .

-

 /*------------------------------------------------------------------------*/

-

 MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>

 = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);

      IToken/*!*/ id;

@@ -447,11 +405,9 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   [ "returns"                                 (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)

     Formals<false, !mmod.IsGhost, outs>

   ]

-

   { MethodSpec<req, mod, ens, dec> }

   [ BlockStmt<out bb, out bodyStart, out bodyEnd>    (. body = (BlockStmt)bb; .)

   ]

-  

   (. if (isRefinement)

        m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

      else if (isConstructor)

@@ -462,7 +418,6 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
      m.BodyEndTok = bodyEnd;

  .)

   .

-

 MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,

            List<Expression/*!*/>/*!*/ decreases.>

 = (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));

@@ -480,8 +435,7 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
   | "decreases" DecreasesList<decreases, false> ";"

   )

   .

-

-Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.> 

+Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>

 = (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; .)

   "("

   [

@@ -491,8 +445,7 @@ Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
   ]

   ")"

   .

-

-FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.> 

+FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>

 = (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; .)

   "("

   [

@@ -502,14 +455,11 @@ FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
   ]

   ")"

   .

-

 /*------------------------------------------------------------------------*/

-

 Type<out Type/*!*/ ty>

 = (. Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; .)

   TypeAndToken<out tok, out ty>

   .

-

 TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>

 = (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

      List<Type/*!*/>/*!*/ gt;

@@ -523,7 +473,6 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
                                        }

                                        ty = new SetType(gt[0]);

                                     .)

-    

   | "seq"                           (. tok = t;  gt = new List<Type/*!*/>(); .)

     GenericInstantiation<gt>        (. if (gt.Count != 1) {

                                          SemErr("seq type expects exactly one type argument");

@@ -533,7 +482,6 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
   | ReferenceType<out tok, out ty>

   )

   .

-

 ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>

 = (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);

      tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

@@ -554,7 +502,6 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
     [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt); .)

   )

   .

-

 GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>

 = (. Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; .)

   "<"

@@ -563,9 +510,7 @@ GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
     }

   ">"

   .

-

 /*------------------------------------------------------------------------*/

-

 FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>

 = (. Contract.Ensures(Contract.ValueAtReturn(out f)!=null);

      Attributes attrs = null;

@@ -588,7 +533,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }

   .)

   { Attribute<ref attrs> }

-  Ident<out id> 

+  Ident<out id>

   [ GenericParameters<typeArgs> ]

   Formals<true, isFunctionMethod, formals>

   ":"

@@ -601,7 +546,6 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
      f.BodyEndTok = bodyEnd;

   .)

   .

-

 FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases.>

 = (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));

      Expression/*!*/ e;  FrameExpression/*!*/ fe; .)

@@ -614,7 +558,6 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r
   | "decreases" DecreasesList<decreases, false> ";"

   )

   .

-

 PossiblyWildExpression<out Expression/*!*/ e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e)!=null);

      e = dummyExpr; .)

@@ -625,7 +568,6 @@ PossiblyWildExpression<out Expression/*!*/ e>
   | Expression<out e>

   )

   .

-

 PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>

 = (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; .)

   /* A reads clause can list a wildcard, which allows the enclosing function to

@@ -638,7 +580,6 @@ PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>
   | FrameExpression<out fe>

   )

   .

-

 FrameExpression<out FrameExpression/*!*/ fe>

 = (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e;  IToken/*!*/ id;  string fieldName = null; .)

   Expression<out e>

@@ -646,16 +587,13 @@ FrameExpression<out FrameExpression/*!*/ fe>
   ]

   (. fe = new FrameExpression(e, fieldName); .)

   .

-

 FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)

   "{"                         (. bodyStart = t; .)

   Expression<out e>

   "}"                         (. bodyEnd = t; .)

   .

-  

 /*------------------------------------------------------------------------*/

-

 BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>

 = (. Contract.Ensures(Contract.ValueAtReturn(out block) != null);

      List<Statement/*!*/> body = new List<Statement/*!*/>();

@@ -666,13 +604,11 @@ BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
   "}"                                  (. bodyEnd = t;

                                           block = new BlockStmt(bodyStart, body); .)

   .

-

 Stmt<.List<Statement/*!*/>/*!*/ ss.>

 = (. Statement/*!*/ s;

   .)

   OneStmt<out s>                                (. ss.Add(s); .)

   .

-

 OneStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  IToken/*!*/ id;  string label = null;

      s = dummyStmt;  /* to please the compiler */

@@ -702,7 +638,6 @@ OneStmt<out Statement/*!*/ s>
   | ReturnStmt<out s>

   )

   .

-

 ReturnStmt<out Statement/*!*/ s>

 = (.

    IToken returnTok = null;

@@ -738,7 +673,6 @@ UpdateStmt<out Statement/*!*/ s>
   )

   (. s = new UpdateStmt(x, lhss, rhss); .)

   .

-

 Rhs<out AssignmentRhs r, Expression receiverForInitCall>

 = (. IToken/*!*/ x, newToken;  Expression/*!*/ e;

      List<Expression> ee = null;

@@ -766,17 +700,13 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
          r = new TypeRhs(newToken, ty, initCall);

        }

     .)

-    

   /* One day, the choose expression should be treated just as a special case of a method call. */

   | "choose"                           (. x = t; .)

     Expression<out e>                  (. r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); .)

-

   | "*"                                (. r = new HavocRhs(t); .)

-

   | Expression<out e>                  (. r = new ExprRhs(e); .)

   )

   .

-

 VarDeclStatement<.out Statement/*!*/ s.>

 = (. IToken x = null, assignTok = null;  bool isGhost = false;

      VarDecl/*!*/ d;

@@ -810,7 +740,6 @@ VarDeclStatement<.out Statement/*!*/ s.>
      s = new VarDeclStmt(x, lhss, update);

   .)

   .

-

 IfStmt<out Statement/*!*/ ifStmt>

 = (. Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x;

      Expression guard;

@@ -836,7 +765,6 @@ IfStmt<out Statement/*!*/ ifStmt>
     (. ifStmt = new AlternativeStmt(x, alternatives); .)

   )

   .

-

 AlternativeBlock<.out List<GuardedAlternative> alternatives.>

 = (. alternatives = new List<GuardedAlternative>();

      IToken x;

@@ -853,7 +781,6 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives.>
   }

   "}"

   .

-

 WhileStmt<out Statement/*!*/ stmt>

 = (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;

      Expression guard;

@@ -877,7 +804,6 @@ WhileStmt<out Statement/*!*/ stmt>
     (. stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); .)

   )

   .

-

 LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>

 = (. bool isFree;  Expression/*!*/ e; FrameExpression/*!*/ fe;

      invariants = new List<MaybeFreeExpression/*!*/>();

@@ -898,7 +824,6 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
                ] ";"

   }

   .

-

 DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>

 = (. Expression/*!*/ e; .)

   PossiblyWildExpression<out e>          (. if (!allowWildcard && e is WildcardExpr) {

@@ -915,7 +840,6 @@ DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
                                          .)

   }

   .

-

 Guard<out Expression e>   /* null represents demonic-choice */

 = (. Expression/*!*/ ee;  e = null; .)

   "("

@@ -924,7 +848,6 @@ Guard<out Expression e>   /* null represents demonic-choice */
   )

   ")"

   .

-

 MatchStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);

      Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;

@@ -937,7 +860,6 @@ MatchStmt<out Statement/*!*/ s>
   "}"

   (. s = new MatchStmt(x, e, cases); .)

   .

-

 CaseStatement<out MatchCaseStmt/*!*/ c>

 = (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);

      IToken/*!*/ x, id, arg;

@@ -955,9 +877,7 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
     { Stmt<body> }

   (. c = new MatchCaseStmt(x, id.val, arguments, body); .)

   .

-

 /*------------------------------------------------------------------------*/

-

 ForeachStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);

      IToken/*!*/ x, boundVar;

@@ -988,19 +908,16 @@ ForeachStmt<out Statement/*!*/ s>
                                                   }

                                                .)

   .

-

 AssertStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; .)

   "assert"                                     (. x = t; .)

   Expression<out e> ";"                        (. s = new AssertStmt(x, e); .)

   .

-

 AssumeStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; .)

   "assume"                                     (. x = t; .)

   Expression<out e> ";"                        (. s = new AssumeStmt(x, e); .)

   .

-

 PrintStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

      List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

@@ -1011,13 +928,11 @@ PrintStmt<out Statement/*!*/ s>
   }

   ";"                                          (. s = new PrintStmt(x, args); .)

   .

-

 /*------------------------------------------------------------------------*/

 Expression<out Expression/*!*/ e>

 =

   EquivExpression<out e>

   .

-

 /*------------------------------------------------------------------------*/

 EquivExpression<out Expression/*!*/ e0>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)

@@ -1026,9 +941,7 @@ EquivExpression<out Expression/*!*/ e0>
     ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)

   }

   .

-

 EquivOp = "<==>" | '\u21d4'.

-

 /*------------------------------------------------------------------------*/

 ImpliesExpression<out Expression/*!*/ e0>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)

@@ -1037,9 +950,7 @@ ImpliesExpression<out Expression/*!*/ e0>
     ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)

   ]

   .

-

 ImpliesOp = "==>" | '\u21d2'.

-

 /*------------------------------------------------------------------------*/

 LogicalExpression<out Expression/*!*/ e0>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)

@@ -1056,10 +967,8 @@ LogicalExpression<out Expression/*!*/ e0>
     }

   ]

   .

-

 AndOp = "&&" | '\u2227'.

 OrOp = "||" | '\u2228'.

-

 /*------------------------------------------------------------------------*/

 RelationalExpression<out Expression/*!*/ e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

@@ -1143,7 +1052,6 @@ RelationalExpression<out Expression/*!*/ e>
      }

   .)

   .

-

 RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>

 = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; .)

   ( "=="           (. x = t;  op = BinaryExpr.Opcode.Eq; .)

@@ -1160,7 +1068,6 @@ RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
   | '\u2265'       (. x = t;  op = BinaryExpr.Opcode.Ge; .)

   )

   .

-

 /*------------------------------------------------------------------------*/

 Term<out Expression/*!*/ e0>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; .)

@@ -1169,14 +1076,12 @@ Term<out Expression/*!*/ e0>
     Factor<out e1>                             (. e0 = new BinaryExpr(x, op, e0, e1); .)

   }

   .

-

 AddOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>

 =          (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; .)

   ( "+"            (. x = t;  op = BinaryExpr.Opcode.Add; .)

   | "-"            (. x = t;  op = BinaryExpr.Opcode.Sub; .)

   )

   .

-

 /*------------------------------------------------------------------------*/

 Factor<out Expression/*!*/ e0>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; .)

@@ -1185,7 +1090,6 @@ Factor<out Expression/*!*/ e0>
     UnaryExpression<out e1>                    (. e0 = new BinaryExpr(x, op, e0, e1); .)

   }

   .

-

 MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>

 = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; .)

   ( "*"            (. x = t;  op = BinaryExpr.Opcode.Mul; .)

@@ -1193,7 +1097,6 @@ MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
   | "%"            (. x = t;  op = BinaryExpr.Opcode.Mod; .)

   )

   .

-

 /*------------------------------------------------------------------------*/

 UnaryExpression<out Expression/*!*/ e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; .)

@@ -1209,7 +1112,6 @@ UnaryExpression<out Expression/*!*/ e>
     { Suffix<ref e> }

   )

   .

-

 Lhs<out Expression e>

 = (. e = null;  // to please the compiler

   .)

@@ -1220,9 +1122,7 @@ Lhs<out Expression e>
     { Suffix<ref e> }

   )

   .

-

 NegOp = "!" | '\u00ac'.

-

 /* A ConstAtomExpression is never an l-value.  Also, a ConstAtomExpression is never followed by

  * an open paren (but could very well have a suffix that starts with a period or a square bracket).

  * (The "Also..." part may change if expressions in Dafny could yield functions.)

@@ -1251,7 +1151,6 @@ ConstAtomExpression<out Expression/*!*/ e>
     ")"

   )

   .

-

 DisplayExpr<out Expression e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

      IToken/*!*/ x;  List<Expression/*!*/>/*!*/ elements;

@@ -1265,7 +1164,6 @@ DisplayExpr<out Expression e>
     "]"

   )

   .

-

 EndlessExpression<out Expression e>

 = (. IToken/*!*/ x;

      Expression e0, e1;

@@ -1280,7 +1178,6 @@ EndlessExpression<out Expression e>
   | ComprehensionExpr<out e>

   )

   .

-

 MatchExpression<out Expression/*!*/ e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

      List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();

@@ -1294,7 +1191,6 @@ MatchExpression<out Expression/*!*/ e>
   }

   (. e = new MatchExpr(x, e, cases); .)

   .

-

 CaseExpression<out MatchCaseExpr/*!*/ c>

 = (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;

      List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();

@@ -1310,9 +1206,7 @@ CaseExpression<out MatchCaseExpr/*!*/ c>
   "=>"

   Expression<out body>       (. c = new MatchCaseExpr(x, id.val, arguments, body); .)

   .

-

 /*------------------------------------------------------------------------*/

-

 DottedIdentifiersAndFunction<out Expression e>

 = (. IToken id;  IToken openParen = null;

      List<Expression> args = null;

@@ -1328,7 +1222,6 @@ DottedIdentifiersAndFunction<out Expression e>
   ]

   (. e = new IdentifierSequence(idents, openParen, args); .)

   .

-

 Suffix<ref Expression/*!*/ e>

 = (. Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x;  List<Expression/*!*/>/*!*/ args;

      Expression e0 = null;  Expression e1 = null;  Expression/*!*/ ee;  bool anyDots = false;

@@ -1341,7 +1234,6 @@ Suffix<ref Expression/*!*/ e>
         [ Expressions<args> ]

       ")"                                      (. e = new FunctionCallExpr(id, id.val, e, args); .)

     ]                                          (. if (!func) { e = new FieldSelectExpr(id, e, id.val); } .)

-    

   | "["                                        (. x = t; .)

       ( Expression<out ee>                     (. e0 = ee; .)

         ( ".."                                 (. anyDots = true; .)

@@ -1384,9 +1276,7 @@ Suffix<ref Expression/*!*/ e>
     "]"

   )

   .

-

 /*------------------------------------------------------------------------*/

-

 QuantifierGuts<out Expression/*!*/ q>

 = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;

      bool univ = false;

@@ -1417,11 +1307,9 @@ QuantifierGuts<out Expression/*!*/ q>
      }

   .)

   .

-

 Forall = "forall" | '\u2200'.

 Exists = "exists" | '\u2203'.

 QSep = "::" | '\u2022'.

-

 ComprehensionExpr<out Expression/*!*/ q>

 = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);

      IToken/*!*/ x = Token.NoToken;

@@ -1444,22 +1332,18 @@ ComprehensionExpr<out Expression/*!*/ q>
      q = new SetComprehension(x, bvars, range, body);

   .)

   .

-

 Expressions<.List<Expression/*!*/>/*!*/ args.>

 = (. Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; .)

   Expression<out e>                            (. args.Add(e); .)

   { "," Expression<out e>                      (. args.Add(e); .)

   }

   .

-

 /*------------------------------------------------------------------------*/

-

 Attribute<ref Attributes attrs>

 = "{"

     AttributeBody<ref attrs>

   "}"

   .

-

 AttributeBody<ref Attributes attrs>

 = (. string aName;

      List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();

@@ -1471,14 +1355,12 @@ AttributeBody<ref Attributes attrs>
     }

   ]                                    (. attrs = new Attributes(aName, aArgs, attrs); .)

   .

-

 AttributeArg<out Attributes.Argument/*!*/ arg>

 = (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e;  arg = dummyAttrArg; .)

   ( string                             (. arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); .)

   | Expression<out e>                  (. arg = new Attributes.Argument(e); .)

   )

   .

-

 AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>

 = (. List<Expression/*!*/> es = new List<Expression/*!*/>();

   .)

@@ -1489,21 +1371,17 @@ AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>
     )

   "}"

   .

-

 /*------------------------------------------------------------------------*/

-

 Idents<.List<string/*!*/>/*!*/ ids.>

 = (. IToken/*!*/ id; .)

   Ident<out id>                            (. ids.Add(id.val); .)

   { "," Ident<out id>                      (. ids.Add(id.val); .)

   }

   .

-

 Ident<out IToken/*!*/ x>

 = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)

   ident            (. x = t; .)

   .

-

 Nat<out BigInteger n>

 =

   digits

@@ -1513,7 +1391,6 @@ Nat<out BigInteger n>
        SemErr("incorrectly formatted number");

        n = BigInteger.Zero;

      }

-  .) 

+  .)

   .

-

-END Dafny.
\ No newline at end of file
+END Dafny.

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 4868be10..8bb381ea 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -400,13 +400,13 @@ namespace Microsoft.Dafny {
 

   /// <summary>

   /// This proxy stands for any type.

-  /// </summary>  

+  /// </summary>

   public class InferredTypeProxy : UnrestrictedTypeProxy {

   }

 

   /// <summary>

   /// This proxy stands for any type, but it originates from an instantiated type parameter.

-  /// </summary>  

+  /// </summary>

   public class ParamTypeProxy : UnrestrictedTypeProxy {

     TypeParameter orig;

     [ContractInvariantMethod]

@@ -432,7 +432,7 @@ namespace Microsoft.Dafny {
 

   /// <summary>

   /// This proxy stands for any datatype.

-  /// </summary>  

+  /// </summary>

   public class DatatypeProxy : RestrictedTypeProxy {

     public override int OrderID {

       get {

@@ -443,7 +443,7 @@ namespace Microsoft.Dafny {
 

   /// <summary>

   /// This proxy stands for object or any class/array type.

-  /// </summary>  

+  /// </summary>

   public class ObjectTypeProxy : RestrictedTypeProxy {

     public override int OrderID {

       get {

@@ -491,7 +491,7 @@ namespace Microsoft.Dafny {
   /// if AllowSeq, or:

   ///     int or set

   /// if !AllowSeq.

-  /// </summary>  

+  /// </summary>

   public class OperationTypeProxy : RestrictedTypeProxy {

     public readonly bool AllowSeq;

     public OperationTypeProxy(bool allowSeq) {

@@ -675,7 +675,7 @@ namespace Microsoft.Dafny {
 

   public class ClassRefinementDecl : ClassDecl {

     public readonly IToken/*!*/ RefinedClass;

-    public ClassDecl Refined; // filled in during resolution 

+    public ClassDecl Refined; // filled in during resolution

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(RefinedClass != null);

@@ -720,7 +720,7 @@ namespace Microsoft.Dafny {
       Dims = dims;

     }

   }

-  

+

   public class DatatypeDecl : TopLevelDecl {

     public readonly List<DatatypeCtor/*!*/>/*!*/ Ctors;

     [ContractInvariantMethod]

@@ -1685,7 +1685,7 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Mod == null || cce.NonNullElements(Mod));

     }

     public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod)

-    : base(tok) 

+    : base(tok)

     {

       Contract.Requires(tok != null);

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

@@ -2511,7 +2511,7 @@ namespace Microsoft.Dafny {
 

     public List<BoundedPool> Bounds;  // initialized and filled in by resolver

     // invariant Bounds == null || Bounds.Count == BoundVars.Count;

-    public List<BoundVar> MissingBounds;  // filled in during resolution; remains "null" if bounds can be found 

+    public List<BoundVar> MissingBounds;  // filled in during resolution; remains "null" if bounds can be found

     // invariant Bounds == null || MissingBounds == null;

 

     public ComprehensionExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression/*!*/ term, Attributes attrs)

@@ -2529,7 +2529,7 @@ namespace Microsoft.Dafny {
     public override IEnumerable<Expression> SubExpressions {

       get {

         if (Range != null) { yield return Range; }

-        yield return Term; 

+        yield return Term;

       }

     }

   }

diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index a18ea938..3f0b6e97 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -27,21 +27,21 @@ namespace Microsoft.Dafny {
         if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {

           Bpl.CommandLineOptions.Clo.XmlSink.WriteFileFragment(dafnyFileName);

         }

-        if (Bpl.CommandLineOptions.Clo.Trace) 

+        if (Bpl.CommandLineOptions.Clo.Trace)

         {

           Console.WriteLine("Parsing " + dafnyFileName);

         }

 

         int errorCount;

-        try 

+        try

         {

           errorCount = Dafny.Parser.Parse(dafnyFileName, modules, builtIns);

-          if (errorCount != 0) 

+          if (errorCount != 0)

           {

             return string.Format("{0} parse errors detected in {1}", errorCount, dafnyFileName);

           }

-        } 

-        catch (IOException e) 

+        }

+        catch (IOException e)

         {

           return string.Format("Error opening file \"{0}\": {1}", dafnyFileName, e.Message);

         }

@@ -61,7 +61,7 @@ namespace Microsoft.Dafny {
           }

         }

       }

-      

+

       if (Bpl.CommandLineOptions.Clo.NoResolve || Bpl.CommandLineOptions.Clo.NoTypecheck) { return null; }

 

       Dafny.Resolver r = new Dafny.Resolver(program);

@@ -73,4 +73,4 @@ namespace Microsoft.Dafny {
       return null;  // success

     }

   }

-}
\ No newline at end of file
+}

diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index 7f063c2c..6a15b1f7 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

@@ -147,11 +147,11 @@
     </BootstrapperPackage>

   </ItemGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it.

        Other similar extension points exist, see Microsoft.Common.targets.

   <Target Name="BeforeBuild">

   </Target>

   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>
\ No newline at end of file
+</Project>

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 42014762..8fcb6bb0 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -5,8 +5,6 @@ using System.IO;
 using System.Text;

 

 

-

-

 using System;

 using System.Diagnostics.Contracts;

 

@@ -25,7 +23,7 @@ public class Parser {
 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

-	

+

 	public Scanner/*!*/ scanner;

 	public Errors/*!*/  errors;

 

@@ -35,20 +33,16 @@ public class Parser {
 

 static List<ModuleDecl/*!*/> theModules;

 static BuiltIns theBuiltIns;

-

-

 static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);

 static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);

 static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);

 static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");

 static int anonymousIds = 0;

-

 struct MemberModifiers {

   public bool IsGhost;

   public bool IsStatic;

   public bool IsUnlimited;

 }

-

 // helper routine for parsing call statements

 private static Expression/*!*/ ConvertToLocal(Expression/*!*/ e)

 {

@@ -60,7 +54,6 @@ Contract.Ensures(Contract.Result<Expression>() != null);
   }

   return e;  // cannot convert to IdentifierExpr (or is already an IdentifierExpr)

 }

-

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members) from "filename"

 /// and appends them in appropriate form to "modules".

@@ -81,7 +74,6 @@ public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ module
     }

   }

 }

-

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members)

 /// and appends them in appropriate form to "modules".

@@ -95,7 +87,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   Errors errors = new Errors();

   return Parse(s, filename, modules, builtIns, errors);

 }

-

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members)

 /// and appends them in appropriate form to "modules".

@@ -121,7 +112,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   theBuiltIns = oldBuiltIns;

   return parser.errors.count;

 }

-

 /*--------------------------------------------------------------------------*/

 

 

@@ -144,10 +134,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (errDist >= minErrDist) errors.SemErr(t, msg);

 		errDist = 0;

 	}

-	

-    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

-      Contract.Requires(tok != null);

-      Contract.Requires(msg != null);

+

+	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

+	  Contract.Requires(tok != null);

+	  Contract.Requires(msg != null);

 	  errors.SemErr(tok, msg);

 	}

 

@@ -160,15 +150,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			la = t;

 		}

 	}

-	

+

 	void Expect (int n) {

 		if (la.kind==n) Get(); else { SynErr(n); }

 	}

-	

+

 	bool StartOf (int s) {

 		return set[s, la.kind];

 	}

-	

+

 	void ExpectWeak (int n, int follow) {

 		if (la.kind == n) Get();

 		else {

@@ -192,26 +182,24 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}

 	}

 

-	

+

 	void Dafny() {

 		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;

 		Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;

+		List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();

+		ModuleDecl module;

+		// to support multiple files, create a default module only if theModules doesn't already contain one

+		DefaultModuleDecl defaultModule = null;

+		foreach (ModuleDecl mdecl in theModules) {

+		 defaultModule = mdecl as DefaultModuleDecl;

+		 if (defaultModule != null) { break; }

+		}

+		bool defaultModuleCreatedHere = false;

+		if (defaultModule == null) {

+		 defaultModuleCreatedHere = true;

+		 defaultModule = new DefaultModuleDecl();

+		}

 		

-		     List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();

-		     ModuleDecl module;

-		     

-		     // to support multiple files, create a default module only if theModules doesn't already contain one

-		     DefaultModuleDecl defaultModule = null;

-		     foreach (ModuleDecl mdecl in theModules) {

-		       defaultModule = mdecl as DefaultModuleDecl;

-		       if (defaultModule != null) { break; }

-		     }

-		     bool defaultModuleCreatedHere = false;

-		     if (defaultModule == null) {

-		       defaultModuleCreatedHere = true;

-		       defaultModule = new DefaultModuleDecl();

-		     }

-		  

 		while (StartOf(1)) {

 			if (la.kind == 5) {

 				Get();

@@ -253,14 +241,14 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		 defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));

 		 theModules.Add(defaultModule);

 		} else {

-		  // find the default class in the default module, then append membersDefaultClass to its member list

-		  foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

-		    DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

-		    if (defaultClass != null) {

-		      defaultClass.Members.AddRange(membersDefaultClass);

-		      break;

-		    }

-		  }

+		 // find the default class in the default module, then append membersDefaultClass to its member list

+		 foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

+		   DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

+		   if (defaultClass != null) {

+		     defaultClass.Members.AddRange(membersDefaultClass);

+		     break;

+		   }

+		 }

 		}

 		

 		Expect(0);

@@ -319,10 +307,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			ClassMemberDecl(members, true);

 		}

 		Expect(8);

-		if (optionalId == null)        

+		if (optionalId == null)

 		 c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);

-		else 

-		  c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

+		else

+		 c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

 		c.BodyStartTok = bodyStart;

 		c.BodyEndTok = t;

 		

@@ -496,7 +484,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			if (allowConstructor) {

 			 isConstructor = true;

 			} else {

-			  SemErr(t, "constructors are only allowed in classes");

+			 SemErr(t, "constructors are only allowed in classes");

 			}

 			

 		} else if (la.kind == 10) {

@@ -505,12 +493,12 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		} else SynErr(106);

 		if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }

 		if (isConstructor) {

-		  if (mmod.IsGhost) {

-		    SemErr(t, "constructors cannot be declared 'ghost'");

-		  }

-		  if (mmod.IsStatic) {

-		    SemErr(t, "constructors cannot be declared 'static'");

-		  }

+		 if (mmod.IsGhost) {

+		   SemErr(t, "constructors cannot be declared 'ghost'");

+		 }

+		 if (mmod.IsStatic) {

+		   SemErr(t, "constructors cannot be declared 'static'");

+		 }

 		}

 		

 		while (la.kind == 7) {

@@ -536,9 +524,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (isRefinement)

 		 m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

 		else if (isConstructor)

-		  m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);

+		 m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);

 		else

-		  m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

+		 m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

 		m.BodyStartTok = bodyStart;

 		m.BodyEndTok = bodyEnd;

 		

@@ -668,9 +656,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Get();

 			UserDefinedType udt = ty as UserDefinedType;

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

-			  name = udt.Name;

+			 name = udt.Name;

 			} else {

-			  SemErr(id, "invalid formal-parameter name in datatype constructor");

+			 SemErr(id, "invalid formal-parameter name in datatype constructor");

 			}

 			

 			Type(out ty);

@@ -678,7 +666,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (name != null) {

 		 identName = name;

 		} else {

-		  identName = "#" + anonymousIds++;

+		 identName = "#" + anonymousIds++;

 		}

 		

 	}

@@ -819,7 +807,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (!allowWildcard && e is WildcardExpr) {

 		 SemErr(e.tok, "'decreases *' is only allowed on loops");

 		} else {

-		  decreases.Add(e);

+		 decreases.Add(e);

 		}

 		

 		while (la.kind == 19) {

@@ -828,7 +816,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (!allowWildcard && e is WildcardExpr) {

 			 SemErr(e.tok, "'decreases *' is only allowed on loops");

 			} else {

-			  decreases.Add(e);

+			 decreases.Add(e);

 			}

 			

 		}

@@ -864,7 +852,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}

 			int dims = 1;

 			if (tok.val.Length != 5) {

-			  dims = int.Parse(tok.val.Substring(5));

+			 dims = int.Parse(tok.val.Substring(5));

 			}

 			ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);

 			

@@ -1132,13 +1120,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(17);

 		UpdateStmt update;

 		if (rhss.Count == 0) {

-		  update = null;

+		 update = null;

 		} else {

-		  var ies = new List<Expression>();

-		  foreach (var lhs in lhss) {

-		    ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

-		  }

-		  update = new UpdateStmt(assignTok, ies, rhss);

+		 var ies = new List<Expression>();

+		 foreach (var lhs in lhss) {

+		   ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

+		 }

+		 update = new UpdateStmt(assignTok, ies, rhss);

 		}

 		s = new VarDeclStmt(x, lhss, update);

 		

@@ -1261,7 +1249,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (bodyAssign != null) {

 		 s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);

 		} else {

-		  s = dummyStmt;  // some error occurred in parsing the bodyAssign

+		 s = dummyStmt;  // some error occurred in parsing the bodyAssign

 		}

 		

 	}

@@ -1322,7 +1310,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (ee != null) {

 			 r = new TypeRhs(newToken, ty, ee);

 			} else {

-			  r = new TypeRhs(newToken, ty, initCall);

+			 r = new TypeRhs(newToken, ty, initCall);

 			}

 			

 		} else if (la.kind == 53) {

@@ -1551,10 +1539,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Expression> chain = null;

 		List<BinaryExpr.Opcode> ops = null;

 		int kind = 0;  // 0 ("uncommitted") indicates chain of ==, possibly with one !=

-		               // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=

-		               // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=

-		               // 3 ("illegal")     indicates illegal chain

-		               // 4 ("disjoint")    indicates chain of disjoint set operators

+		              // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=

+		              // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=

+		              // 3 ("illegal")     indicates illegal chain

+		              // 4 ("disjoint")    indicates chain of disjoint set operators

 		bool hasSeenNeq = false;

 		

 		Term(out e0);

@@ -1565,7 +1553,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Term(out e1);

 			e = new BinaryExpr(x, op, e0, e1);

 			if (op == BinaryExpr.Opcode.Disjoint)

-			  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

+			 acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

 			

 			while (StartOf(14)) {

 				if (chain == null) {

@@ -1621,11 +1609,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Term(out e1);

 				ops.Add(op); chain.Add(e1);

 				if (op == BinaryExpr.Opcode.Disjoint) {

-				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));

-				  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

+				 e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));

+				 acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

 				}

 				else

-				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

+				 e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

 				

 			}

 		}

@@ -1918,21 +1906,21 @@ List<Expression/*!*/>/*!*/ decreases) {
 			 // make sure an array class with this dimensionality exists

 			 UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true);

 			} else {

-			  if (!anyDots && e0 == null) {

-			    /* a parsing error occurred */

-			    e0 = dummyExpr;

-			  }

-			  Contract.Assert(anyDots || e0 != null);

-			  if (anyDots) {

-			    Contract.Assert(e0 != null || e1 != null);

-			    e = new SeqSelectExpr(x, false, e, e0, e1);

-			  } else if (e1 == null) {

-			    Contract.Assert(e0 != null);

-			    e = new SeqSelectExpr(x, true, e, e0, null);

-			  } else {

-			    Contract.Assert(e0 != null);

-			    e = new SeqUpdateExpr(x, e, e0, e1);

-			  }

+			 if (!anyDots && e0 == null) {

+			   /* a parsing error occurred */

+			   e0 = dummyExpr;

+			 }

+			 Contract.Assert(anyDots || e0 != null);

+			 if (anyDots) {

+			   Contract.Assert(e0 != null || e1 != null);

+			   e = new SeqSelectExpr(x, false, e, e0, e1);

+			 } else if (e1 == null) {

+			   Contract.Assert(e0 != null);

+			   e = new SeqSelectExpr(x, true, e, e0, null);

+			 } else {

+			   Contract.Assert(e0 != null);

+			   e = new SeqUpdateExpr(x, e, e0, e1);

+			 }

 			}

 			

 			Expect(51);

@@ -2046,8 +2034,8 @@ List<Expression/*!*/>/*!*/ decreases) {
 		try {

 		 n = BigInteger.Parse(t.val);

 		} catch (System.FormatException) {

-		  SemErr("incorrectly formatted number");

-		  n = BigInteger.Zero;

+		 SemErr("incorrectly formatted number");

+		 n = BigInteger.Zero;

 		}

 		

 	}

@@ -2102,7 +2090,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (univ) {

 		 q = new ForallExpr(x, bvars, range, body, trigs, attrs);

 		} else {

-		  q = new ExistsExpr(x, bvars, range, body, trigs, attrs);

+		 q = new ExistsExpr(x, bvars, range, body, trigs, attrs);

 		}

 		

 	}

@@ -2221,13 +2209,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	public void Parse() {

 		la = new Token();

-		la.val = "";		

+		la.val = "";

 		Get();

 		Dafny();

+		Expect(0);

 

-    Expect(0);

+		Expect(0);

 	}

-	

+

 	static readonly bool[,]/*!*/ set = {

 		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

@@ -2254,18 +2243,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 public class Errors {

 	public int count = 0;                                    // number of errors detected

 	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream

-  public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

-  public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

-  

+	public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

+	public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

+

 	public void SynErr(string filename, int line, int col, int n) {

-    SynErr(filename, line, col, GetSyntaxErrorString(n));

-  }

-	public virtual void SynErr(string filename, int line, int col, string msg) {

-	  Contract.Requires(msg != null);

+		SynErr(filename, line, col, GetSyntaxErrorString(n));

+	}

+

+	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {

+		Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

-  }

-  string GetSyntaxErrorString(int n) {

+	}

+

+	string GetSyntaxErrorString(int n) {

 		string s;

 		switch (n) {

 			case 0: s = "EOF expected"; break;

@@ -2415,7 +2406,7 @@ public class Errors {
 

 			default: s = "error " + n; break;

 		}

-    return s;

+		return s;

 	}

 

 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

@@ -2423,8 +2414,9 @@ public class Errors {
 		Contract.Requires(msg != null);

 		SemErr(tok.filename, tok.line, tok.col, msg);

 	}

+

 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

-	  Contract.Requires(msg != null);

+		Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

 	}

@@ -2440,4 +2432,5 @@ public class FatalError: Exception {
 	public FatalError(string m): base(m) {}

 }

 

+

 }
\ No newline at end of file
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index b9c8601e..ba9963c7 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -14,7 +14,7 @@ namespace Microsoft.Dafny {
   class Printer {

     TextWriter wr;

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(wr!=null);

     }

@@ -23,7 +23,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(wr != null);

       this.wr = wr;

     }

-    

+

     public void PrintProgram(Program prog) {

       Contract.Requires(prog != null);

       if (Bpl.CommandLineOptions.Clo.ShowEnv != Bpl.CommandLineOptions.ShowEnvironment.Never) {

@@ -56,7 +56,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     public void PrintTopLevelDecls(List<TopLevelDecl> classes, int indent) {

       Contract.Requires(classes!= null);

       int i = 0;

@@ -79,7 +79,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     public void PrintClass(ClassDecl c, int indent) {

       Contract.Requires(c != null);

       Indent(indent);

@@ -97,12 +97,12 @@ namespace Microsoft.Dafny {
         wr.WriteLine("}");

       }

     }

-    

+

     public void PrintClass_Members(ClassDecl c, int indent)

     {

       Contract.Requires(c != null);

       Contract.Requires( c.Members.Count != 0);

-    

+

       int state = 0;  // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field

       foreach (MemberDecl m in c.Members) {

         if (m is Method) {

@@ -126,7 +126,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     void PrintClassMethodHelper(string kind, Attributes attrs, string name, List<TypeParameter> typeArgs) {

       Contract.Requires(kind != null);

       Contract.Requires(name != null);

@@ -147,7 +147,7 @@ namespace Microsoft.Dafny {
         wr.Write(">");

       }

     }

-    

+

     public void PrintDatatype(DatatypeDecl dt, int indent) {

       Contract.Requires(dt != null);

       Indent(indent);

@@ -164,17 +164,17 @@ namespace Microsoft.Dafny {
       }

       wr.WriteLine(";");

     }

-    

+

     public void PrintAttributes(Attributes a) {

       if (a != null) {

         PrintAttributes(a.Prev);

-        

+

         wr.Write("{{:{0}", a.Name);

         PrintAttributeArgs(a.Args);

         wr.Write("} ");

       }

     }

-    

+

     public void PrintAttributeArgs(List<Attributes.Argument> args) {

       Contract.Requires(args != null);

       string prefix = " ";

@@ -190,7 +190,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     public void PrintField(Field field, int indent) {

       Contract.Requires(field != null);

       Indent(indent);

@@ -203,7 +203,7 @@ namespace Microsoft.Dafny {
       PrintType(field.Type);

       wr.WriteLine(";");

     }

-    

+

     public void PrintCouplingInvariant(CouplingInvariant inv, int indent) {

       Contract.Requires(inv != null);

       Indent(indent);

@@ -218,7 +218,7 @@ namespace Microsoft.Dafny {
       PrintExpression(inv.Expr);

       wr.WriteLine(";");

     }

-    

+

     public void PrintFunction(Function f, int indent) {

       Contract.Requires(f != null);

       Indent(indent);

@@ -245,20 +245,20 @@ namespace Microsoft.Dafny {
         wr.WriteLine("}");

       }

     }

-    

+

     // ----------------------------- PrintMethod -----------------------------

 

     const int IndentAmount = 2;

     const string BunchaSpaces = "                                ";

     void Indent(int amount)

     {  Contract.Requires( 0 <= amount);

-    

+

       while (0 < amount) {

         wr.Write(BunchaSpaces.Substring(0, amount));

         amount -= BunchaSpaces.Length;

       }

     }

-    

+

     public void PrintMethod(Method method, int indent) {

       Contract.Requires(method != null);

       Indent(indent);

@@ -284,14 +284,14 @@ namespace Microsoft.Dafny {
       PrintFrameSpecLine("modifies", method.Mod, ind);

       PrintSpec("ensures", method.Ens, ind);

       PrintSpecLine("decreases", method.Decreases, ind);

-      

+

       if (method.Body != null) {

         Indent(indent);

         PrintStatement(method.Body, indent);

         wr.WriteLine();

       }

     }

-    

+

     void PrintFormals(List<Formal> ff) {

       Contract.Requires(ff!=null);

       wr.Write("(");

@@ -304,7 +304,7 @@ namespace Microsoft.Dafny {
       }

       wr.Write(")");

     }

-    

+

     void PrintFormal(Formal f) {

       Contract.Requires(f != null);

       if (f.IsGhost) {

@@ -315,7 +315,7 @@ namespace Microsoft.Dafny {
       }

       PrintType(f.Type);

     }

-    

+

     void PrintSpec(string kind, List<Expression> ee, int indent) {

       Contract.Requires(kind != null);

       Contract.Requires(ee != null);

@@ -363,7 +363,7 @@ namespace Microsoft.Dafny {
     }

 

     // ----------------------------- PrintType -----------------------------

-    

+

     public void PrintType(Type ty) {

       Contract.Requires(ty != null);

       wr.Write(ty.ToString());

@@ -379,7 +379,7 @@ namespace Microsoft.Dafny {
     }

 

     // ----------------------------- PrintStatement -----------------------------

-    

+

     /// <summary>

     /// Prints from the current position of the current line.

     /// If the statement requires several lines, subsequent lines are indented at "indent".

@@ -393,23 +393,23 @@ namespace Microsoft.Dafny {
           Indent(indent);

         }

       }

-        

+

       if (stmt is AssertStmt) {

         wr.Write("assert ");

         PrintExpression(((AssertStmt)stmt).Expr);

         wr.Write(";");

-        

+

       } else if (stmt is AssumeStmt) {

         wr.Write("assume ");

         PrintExpression(((AssumeStmt)stmt).Expr);

         wr.Write(";");

-        

+

       } else if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

         wr.Write("print");

         PrintAttributeArgs(s.Args);

         wr.Write(";");

-        

+

       } else if (stmt is BreakStmt) {

         BreakStmt s = (BreakStmt)stmt;

         if (s.TargetLabel != null) {

@@ -422,7 +422,7 @@ namespace Microsoft.Dafny {
           }

           wr.Write(";");

         }

-        

+

       } else if (stmt is ReturnStmt) {

         var s = (ReturnStmt) stmt;

         wr.Write("return");

@@ -435,14 +435,14 @@ namespace Microsoft.Dafny {
           }

         }

           wr.Write(";");

-        

+

       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

         PrintExpression(s.Lhs);

         wr.Write(" := ");

         PrintRhs(s.Rhs);

         wr.Write(";");

-        

+

       } else if (stmt is VarDecl) {

         VarDecl s = (VarDecl)stmt;

         if (s.IsGhost) {

@@ -451,7 +451,7 @@ namespace Microsoft.Dafny {
         wr.Write("var {0}", s.Name);

         PrintType(": ", s.OptionalType);

         wr.Write(";");

-      

+

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

         wr.Write("call ");

@@ -471,7 +471,7 @@ namespace Microsoft.Dafny {
         wr.Write("{0}(", s.MethodName);

         PrintExpressionList(s.Args);

         wr.Write(");");

-        

+

       } else if (stmt is BlockStmt) {

         wr.WriteLine("{");

         int ind = indent + IndentAmount;

@@ -482,7 +482,7 @@ namespace Microsoft.Dafny {
         }

         Indent(indent);

         wr.Write("}");

-        

+

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

         while (true) {

@@ -508,7 +508,7 @@ namespace Microsoft.Dafny {
         PrintAlternatives(indent, s.Alternatives);

         Indent(indent);

         wr.Write("}");

-      

+

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

         wr.Write("while (");

@@ -556,7 +556,7 @@ namespace Microsoft.Dafny {
         wr.WriteLine();

         Indent(indent);

         wr.Write("}");

-        

+

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         wr.Write("match ");

@@ -644,7 +644,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     void PrintRhs(AssignmentRhs rhs) {

       Contract.Requires(rhs != null);

       if (rhs is ExprRhs) {

@@ -673,7 +673,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS

       }

     }

-    

+

     void PrintGuard(Expression guard) {

       if (guard == null) {

         wr.Write("*");

@@ -681,7 +681,7 @@ namespace Microsoft.Dafny {
         PrintExpression(guard);

       }

     }

-    

+

     // ----------------------------- PrintExpression -----------------------------

 

     public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen) {

@@ -739,12 +739,12 @@ namespace Microsoft.Dafny {
         wr.WriteLine(endWithCloseParen ? ")" : "");

       }

     }

-    

+

     public void PrintExpression(Expression expr) {

       Contract.Requires(expr != null);

       PrintExpr(expr, 0, false, true, -1);

     }

-    

+

     /// <summary>

     /// An indent of -1 means print the entire expression on one line.

     /// </summary>

@@ -752,7 +752,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);

       PrintExpr(expr, 0, false, true, indent);

     }

-    

+

     /// <summary>

     /// An indent of -1 means print the entire expression on one line.

     /// </summary>

@@ -770,13 +770,13 @@ namespace Microsoft.Dafny {
         } else {

           wr.Write((BigInteger)e.Value);

         }

-      

+

       } else if (expr is ThisExpr) {

         wr.Write("this");

-  

+

       } else if (expr is IdentifierExpr) {

         wr.Write(((IdentifierExpr)expr).Name);

-      

+

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName);

@@ -785,13 +785,13 @@ namespace Microsoft.Dafny {
           PrintExpressionList(dtv.Arguments);

           wr.Write(")");

         }

-        

+

       } else if (expr is DisplayExpression) {

         DisplayExpression e = (DisplayExpression)expr;

         wr.Write(e is SetDisplayExpr ? "{" : "[");

         PrintExpressionList(e.Elements);

         wr.Write(e is SetDisplayExpr ? "}" : "]");

-        

+

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr e = (FieldSelectExpr)expr;

         // determine if parens are needed

@@ -799,7 +799,7 @@ namespace Microsoft.Dafny {
         bool parensNeeded = !(e.Obj is ImplicitThisExpr) &&

           opBindingStrength < contextBindingStrength ||

           (fragileContext && opBindingStrength == contextBindingStrength);

-        

+

         if (parensNeeded) { wr.Write("("); }

         if (!(e.Obj is ImplicitThisExpr)) {

           PrintExpr(e.Obj, opBindingStrength, false, false, -1);

@@ -814,7 +814,7 @@ namespace Microsoft.Dafny {
         int opBindingStrength = 0x70;

         bool parensNeeded = opBindingStrength < contextBindingStrength ||

           (fragileContext && opBindingStrength == contextBindingStrength);

-        

+

         if (parensNeeded) { wr.Write("("); }

         PrintExpr(e.Seq, 0x00, false, false, indent);  // BOGUS: fix me

         wr.Write("[");

@@ -858,7 +858,7 @@ namespace Microsoft.Dafny {
         int opBindingStrength = 0x70;

         bool parensNeeded = opBindingStrength < contextBindingStrength ||

           (fragileContext && opBindingStrength == contextBindingStrength);

-        

+

         if (parensNeeded) { wr.Write("("); }

         PrintExpr(e.Seq, 00, false, false, indent);  // BOGUS: fix me

         wr.Write("[");

@@ -867,7 +867,7 @@ namespace Microsoft.Dafny {
         PrintExpression(e.Value);

         wr.Write("]");

         if (parensNeeded) { wr.Write(")"); }

-      

+

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         // determine if parens are needed

@@ -875,7 +875,7 @@ namespace Microsoft.Dafny {
         bool parensNeeded = !(e.Receiver is ImplicitThisExpr) &&

           opBindingStrength < contextBindingStrength ||

           (fragileContext && opBindingStrength == contextBindingStrength);

-        

+

         if (parensNeeded) { wr.Write("("); }

         if (!(e.Receiver is ImplicitThisExpr)) {

           PrintExpr(e.Receiver, opBindingStrength, false, false, -1);

@@ -886,12 +886,12 @@ namespace Microsoft.Dafny {
         PrintExpressionList(e.Args);

         wr.Write(")");

         if (parensNeeded) { wr.Write(")"); }

-      

+

       } else if (expr is OldExpr) {

         wr.Write("old(");

         PrintExpression(((OldExpr)expr).E);

         wr.Write(")");

-      

+

       } else if (expr is FreshExpr) {

         wr.Write("fresh(");

         PrintExpression(((FreshExpr)expr).E);

@@ -929,14 +929,14 @@ namespace Microsoft.Dafny {
           PrintExpr(e.E, opBindingStrength, false, parensNeeded || isRightmost, -1);

           if (parensNeeded) { wr.Write(")"); }

         }

-      

+

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

         // determine if parens are needed

         int opBindingStrength;

         bool fragileLeftContext = false;  // false means "allow same binding power on left without parens"

         bool fragileRightContext = false;  // false means "allow same binding power on right without parens"

-        switch (e.Op) 

+        switch (e.Op)

         {

           case BinaryExpr.Opcode.Add:

             opBindingStrength = 0x40; break;

@@ -1064,7 +1064,7 @@ namespace Microsoft.Dafny {
 

       } else if (expr is WildcardExpr) {

         wr.Write("*");

-        

+

       } else if (expr is ITEExpr) {

         ITEExpr ite = (ITEExpr)expr;

         bool parensNeeded = !isRightmost;

@@ -1076,7 +1076,7 @@ namespace Microsoft.Dafny {
         wr.Write(" else ");

         PrintExpression(ite.Els);

         if (parensNeeded) { wr.Write(")"); }

-        

+

       } else if (expr is ParensExpression) {

         var e = (ParensExpression)expr;

         // printing of parentheses is done optimally, not according to the parentheses in the given program

@@ -1094,24 +1094,24 @@ namespace Microsoft.Dafny {
           PrintExpressionList(e.Arguments);

           wr.Write(")");

         }

-        

+

       } else if (expr is MatchExpr) {

         Contract.Assert(false); throw new cce.UnreachableException();  // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr

       } else {

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

       }

     }

-    

+

     void PrintTriggers(Triggers trigs) {

       if (trigs != null) {

         PrintTriggers(trigs.Prev);

-        

+

         wr.Write("{ ");

         PrintExpressionList(trigs.Terms);

         wr.Write(" } ");

       }

     }

-    

+

     void PrintExpressionList(List<Expression> exprs) {

       Contract.Requires(exprs != null);

       string sep = "";

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 197a603e..8ec5d4c1 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -67,7 +67,7 @@ namespace Microsoft.Dafny {
     }

 

     bool checkRefinements = true; // used to indicate a cycle in refinements

-      

+

     public void ResolveProgram(Program prog) {

       Contract.Requires(prog != null);

       // register modules

@@ -119,15 +119,15 @@ namespace Microsoft.Dafny {
         }

       }

 

-      // resolve top-level declarations of refinements      

-      foreach (ModuleDecl m in prog.Modules) 

-        foreach (TopLevelDecl decl in m.TopLevelDecls) 

+      // resolve top-level declarations of refinements

+      foreach (ModuleDecl m in prog.Modules)

+        foreach (TopLevelDecl decl in m.TopLevelDecls)

           if (decl is ClassRefinementDecl) {

             ClassRefinementDecl rdecl = (ClassRefinementDecl) decl;

             ResolveTopLevelRefinement(rdecl);

             if (rdecl.Refined != null) refines.AddEdge(rdecl, rdecl.Refined);

           }

-      

+

       // attempt finding refinement cycles

       List<TopLevelDecl> refinesCycle = refines.TryFindCycle();

       if (refinesCycle != null) {

@@ -139,8 +139,8 @@ namespace Microsoft.Dafny {
         }

         Error(refinesCycle[0], "Detected a cyclic refinement declaration: {0}", cy);

         checkRefinements = false;

-      } 

-      

+      }

+

       // resolve top-level declarations

       Graph<DatatypeDecl> datatypeDependencies = new Graph<DatatypeDecl>();

       foreach (ModuleDecl m in prog.Modules) {

@@ -168,7 +168,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     public void RegisterTopLevelDecls(List<TopLevelDecl> declarations) {

       Contract.Requires(declarations != null);

       foreach (TopLevelDecl d in declarations) {

@@ -209,7 +209,7 @@ namespace Microsoft.Dafny {
           // ... and of the other members

           Dictionary<string, MemberDecl> members = new Dictionary<string, MemberDecl>();

           datatypeMembers.Add(dt, members);

-        

+

           foreach (DatatypeCtor ctor in dt.Ctors) {

             if (ctor.Name.EndsWith("?")) {

               Error(ctor, "a datatype constructor name is not allowed to end with '?'");

@@ -224,7 +224,7 @@ namespace Microsoft.Dafny {
               query.EnclosingClass = dt;  // resolve here

               members.Add(queryName, query);

               ctor.QueryField = query;

-                

+

               // also register the constructor name globally

               Tuple<DatatypeCtor, bool> pair;

               if (allDatatypeCtors.TryGetValue(ctor.Name, out pair)) {

@@ -268,9 +268,9 @@ namespace Microsoft.Dafny {
         }

         decl.Refined = cce.NonNull((ClassDecl) a);

         // TODO: copy over remaining members of a

-      }        

-    }  

-      

+      }

+    }

+

     public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {

       Contract.Requires(declarations != null);

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

@@ -286,7 +286,7 @@ namespace Microsoft.Dafny {
         allTypeParameters.PopMarker();

       }

     }

-    

+

     public void ResolveTopLevelDecls_Meat(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {

       Contract.Requires(declarations != null);

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

@@ -306,7 +306,7 @@ namespace Microsoft.Dafny {
         allTypeParameters.PopMarker();

       }

     }

-    

+

     ClassDecl currentClass;

     Function currentFunction;

     readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();

@@ -314,7 +314,7 @@ namespace Microsoft.Dafny {
     readonly Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();

     readonly List<Statement> loopStack = new List<Statement>();  // the enclosing loops (from which it is possible to break out)

     readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>();  // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -323,13 +323,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(cl != null);

       Contract.Requires(currentClass == null);

       Contract.Ensures(currentClass == null);

-    

+

       currentClass = cl;

       foreach (MemberDecl member in cl.Members) {

         member.EnclosingClass = cl;

         if (member is Field) {

           ResolveType(member.tok, ((Field)member).Type);

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           allTypeParameters.PushMarker();

@@ -343,15 +343,15 @@ namespace Microsoft.Dafny {
           ResolveTypeParameters(m.TypeArgs, true, m);

           ResolveMethodSignature(m);

           allTypeParameters.PopMarker();

-          

+

         } else if (member is CouplingInvariant) {

           CouplingInvariant inv = (CouplingInvariant)member;

-          if (currentClass is ClassRefinementDecl) {      

+          if (currentClass is ClassRefinementDecl) {

             ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

             if (refined != null) {

               Contract.Assert(classMembers.ContainsKey(refined));

               Dictionary<string,MemberDecl> members = classMembers[refined];

-            

+

               // resolve abstracted fields in the refined class

               List<Field> fields = new List<Field>();

               foreach (IToken tok in inv.Toks) {

@@ -359,29 +359,29 @@ namespace Microsoft.Dafny {
                   Error(tok, "Refined class does not declare a field: {0}", tok.val);

                 else {

                   MemberDecl field = members[tok.val];

-                  if (!(field is Field)) 

+                  if (!(field is Field))

                     Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);

                   else if (fields.Contains(cce.NonNull((Field)field)))

                     Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);

                   else

                     fields.Add(cce.NonNull((Field)field));

-                }                  

-              }            

+                }

+              }

               inv.Refined = fields;

             }

-            

+

           } else {

             Error(member, "Coupling invariants can only be declared in refinement classes");

           }

         } else {

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

         }

-        

-        if (currentClass is ClassRefinementDecl) {          

+

+        if (currentClass is ClassRefinementDecl) {

           ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

           if (refined != null) {

             Contract.Assert(classMembers.ContainsKey(refined));

-          

+

             // there is a member with the same name in refined class if and only if the member is a refined method

             if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))

               Error(member, "Refined class has a member with the same name as in the refinement class: {0}", member.Name);

@@ -399,14 +399,14 @@ namespace Microsoft.Dafny {
       Contract.Requires(cl != null);

       Contract.Requires(currentClass == null);

       Contract.Ensures(currentClass == null);

-    

+

       ResolveAttributes(cl.Attributes, false);

       currentClass = cl;

       foreach (MemberDecl member in cl.Members) {

         ResolveAttributes(member.Attributes, false);

         if (member is Field) {

           // nothing more to do

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           allTypeParameters.PushMarker();

@@ -420,13 +420,13 @@ namespace Microsoft.Dafny {
           ResolveTypeParameters(m.TypeArgs, false, m);

           ResolveMethod(m);

           allTypeParameters.PopMarker();

-          

+

           // check if signature of the refined method matches the refinement method

           if (member is MethodRefinement) {

             MethodRefinement mf = (MethodRefinement)member;

             if (currentClass is ClassRefinementDecl) {

               // should have already been resolved

-              if (((ClassRefinementDecl)currentClass).Refined != null) { 

+              if (((ClassRefinementDecl)currentClass).Refined != null) {

                 MemberDecl d = classMembers[((ClassRefinementDecl)currentClass).Refined][mf.Name];

                 if (d is Method) {

                   mf.Refined = (Method)d;

@@ -434,18 +434,18 @@ namespace Microsoft.Dafny {
                     Error(mf, "Different number of input variables");

                   if (mf.Outs.Count != mf.Refined.Outs.Count)

                     Error(mf, "Different number of output variables");

-                  if (mf.IsStatic || mf.Refined.IsStatic) 

+                  if (mf.IsStatic || mf.Refined.IsStatic)

                     Error(mf, "Refined methods cannot be static");

                 } else {

                   Error(member, "Refined class has a non-method member with the same name: {0}", member.Name);

-                }            

+                }

               }

             } else {

               Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);

             }

           }

-        

-        } else if (member is CouplingInvariant) {        

+

+        } else if (member is CouplingInvariant) {

           CouplingInvariant inv = (CouplingInvariant)member;

           if (inv.Refined != null) {

             inv.Formals = new List<Formal>();

@@ -460,7 +460,7 @@ namespace Microsoft.Dafny {
             }

             ResolveExpression(inv.Expr, false);

             scope.PopMarker();

-          }                

+          }

         } else {

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

         }

@@ -476,13 +476,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(dt != null);

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

       foreach (DatatypeCtor ctor in dt.Ctors) {

-        

+

         ctor.EnclosingDatatype = dt;

 

         allTypeParameters.PushMarker();

         ResolveCtorSignature(ctor);

         allTypeParameters.PopMarker();

-        

+

         foreach (Formal p in ctor.Formals) {

           DatatypeDecl dependee = p.Type.AsDatatype;

           if (dependee != null) {

@@ -497,7 +497,7 @@ namespace Microsoft.Dafny {
     /// datatype has some value that can be constructed from datatypes in lower stratospheres only.

     /// The algorithm used here is quadratic in the number of datatypes in the SCC.  Since that number is

     /// deemed to be rather small, this seems okay.

-    /// </summary>    

+    /// </summary>

     void SccStratosphereCheck(DatatypeDecl startingPoint, Graph<DatatypeDecl/*!*/>/*!*/ dependencies)

     {

       Contract.Requires(startingPoint != null);

@@ -573,7 +573,7 @@ namespace Microsoft.Dafny {
         ResolveAttributeArgs(attrs.Args, twoState);

       }

     }

-        

+

     void ResolveAttributeArgs(List<Attributes.Argument/*!*/>/*!*/ args, bool twoState) {

       Contract.Requires(args != null);

       foreach (Attributes.Argument aa in args) {

@@ -583,7 +583,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-        

+

     void ResolveTriggers(Triggers trigs, bool twoState) {

       // order does not matter for resolution, so resolve them in reverse order

       for (; trigs != null; trigs = trigs.Prev) {

@@ -592,9 +592,9 @@ namespace Microsoft.Dafny {
         }

       }

     }

-        

+

     void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) {

-      

+

       Contract.Requires(tparams != null);

       Contract.Requires(parent != null);

       // push type arguments of the refined class

@@ -603,7 +603,7 @@ namespace Microsoft.Dafny {
         if (refined != null)

           ResolveTypeParameters(refined.TypeArgs, false, refined);

       }

-    

+

       // push non-duplicated type parameter names

       foreach (TypeParameter tp in tparams) {

         Contract.Assert(tp != null);

@@ -616,7 +616,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -683,7 +683,7 @@ namespace Microsoft.Dafny {
       currentFunction = null;

       scope.PopMarker();

     }

-    

+

     void ResolveFrameExpression(FrameExpression fe, string kind) {

       Contract.Requires(fe != null);

       Contract.Requires(kind != null);

@@ -717,7 +717,7 @@ namespace Microsoft.Dafny {
         Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type);

       }

     }

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -740,7 +740,7 @@ namespace Microsoft.Dafny {
       }

       scope.PopMarker();

     }

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -754,7 +754,7 @@ namespace Microsoft.Dafny {
       foreach (Formal p in m.Ins) {

         scope.Push(p.Name, p);

       }

-      

+

       // Start resolving specification...

       foreach (MaybeFreeExpression e in m.Req) {

         ResolveExpression(e.E, false);

@@ -770,7 +770,7 @@ namespace Microsoft.Dafny {
         ResolveExpression(e, false);

         // any type is fine

       }

-      

+

       // Add out-parameters to a new scope that will also include the outermost-level locals of the body

       // Don't care about any duplication errors among the out-parameters, since they have already been reported

       scope.PushMarker();

@@ -786,16 +786,16 @@ namespace Microsoft.Dafny {
           Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);

         }

       }

-      

+

       // Resolve body

       if (m.Body != null) {

         ResolveBlockStatement(m.Body, m.IsGhost, m);

       }

-      

+

       scope.PopMarker();  // for the out-parameters and outermost-level locals

       scope.PopMarker();  // for the in-parameters

     }

-    

+

     void ResolveCtorSignature(DatatypeCtor ctor) {

       Contract.Requires(ctor != null);

       foreach (Formal p in ctor.Formals) {

@@ -839,18 +839,18 @@ namespace Microsoft.Dafny {
             Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);

           }

         }

-      

+

       } else if (type is TypeProxy) {

         TypeProxy t = (TypeProxy)type;

         if (t.T != null) {

           ResolveType(tok, t.T);

         }

-        

+

       } else {

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

       }

     }

-    

+

     public bool UnifyTypes(Type a, Type b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -866,7 +866,7 @@ namespace Microsoft.Dafny {
           a = proxy.T;

         }

       }

-      

+

       while (b is TypeProxy) {

         TypeProxy proxy = (TypeProxy)b;

         if (proxy.T == null) {

@@ -876,7 +876,7 @@ namespace Microsoft.Dafny {
           b = proxy.T;

         }

       }

-      

+

 #if !NO_CHEAP_OBJECT_WORKAROUND

       if (a is ObjectType || b is ObjectType) {  // TODO: remove this temporary hack

         var other = a is ObjectType ? b : a;

@@ -888,7 +888,7 @@ namespace Microsoft.Dafny {
       }

 #endif

       // Now, a and b are non-proxies and stand for the same things as the original a and b, respectively.

-      

+

       if (a is BoolType) {

         return b is BoolType;

       } else if (a is IntType) {

@@ -923,12 +923,12 @@ namespace Microsoft.Dafny {
           // something is wrong; either aa or bb wasn't properly resolved, or they don't unify

           return false;

         }

-        

+

       } else {

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

       }

     }

-    

+

     bool AssignProxy(TypeProxy proxy, Type t){

       Contract.Requires(proxy != null);

       Contract.Requires(t != null);

@@ -939,15 +939,15 @@ namespace Microsoft.Dafny {
       if (proxy == t) {

         // they are already in the same equivalence class

         return true;

-      

+

       } else if (proxy is UnrestrictedTypeProxy) {

         // it's fine to redirect proxy to t (done below)

-        

+

       } else if (t is UnrestrictedTypeProxy) {

           // merge proxy and t by redirecting t to proxy, rather than the other way around

           ((TypeProxy)t).T = proxy;

           return true;

-      

+

       } else if (t is RestrictedTypeProxy) {

         // Both proxy and t are restricted type proxies.  To simplify unification, order proxy and t

         // according to their types.

@@ -958,7 +958,7 @@ namespace Microsoft.Dafny {
         } else {

           return AssignRestrictedProxies(r1, r0);

         }

-      

+

       // In the remaining cases, proxy is a restricted proxy and t is a non-proxy

       } else if (proxy is DatatypeProxy) {

         if (t.IsDatatype) {

@@ -966,14 +966,14 @@ namespace Microsoft.Dafny {
         } else {

           return false;

         }

-      

+

       } else if (proxy is ObjectTypeProxy) {

         if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {

           // all is fine, proxy can be redirected to t

         } else {

           return false;

         }

-      

+

       } else if (proxy is ObjectsTypeProxy) {

         if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {

           // all is good

@@ -981,7 +981,7 @@ namespace Microsoft.Dafny {
           proxy.T = new CollectionTypeProxy(new ObjectTypeProxy());

           return UnifyTypes(proxy.T, t);

         }

-        

+

       } else if (proxy is CollectionTypeProxy) {

         CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy;

         if (t is CollectionType) {

@@ -991,7 +991,7 @@ namespace Microsoft.Dafny {
         } else {

           return false;

         }

-      

+

       } else if (proxy is OperationTypeProxy) {

         OperationTypeProxy opProxy = (OperationTypeProxy)proxy;

         if (t is IntType || t is SetType || (opProxy.AllowSeq && t is SeqType)) {

@@ -1014,11 +1014,11 @@ namespace Microsoft.Dafny {
         } else {

           return false;

         }

-                

+

       } else {

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

       }

-      

+

       // do the merge, but never infer a subrange type

       if (t is NatType) {

         proxy.T = Type.Int;

@@ -1027,7 +1027,7 @@ namespace Microsoft.Dafny {
       }

       return true;

     }

-    

+

     bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b)

     { Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -1036,7 +1036,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(a.OrderID <= b.OrderID);

       //modifies a.T, b.T;

       Contract.Ensures(Contract.Result<bool>() || a.T != null || b.T != null);

-    

+

       if (a is DatatypeProxy) {

         if (b is DatatypeProxy) {

           // all is fine

@@ -1062,7 +1062,7 @@ namespace Microsoft.Dafny {
         } else {

           return false;

         }

-        

+

       } else if (a is ObjectsTypeProxy) {

         if (b is ObjectsTypeProxy) {

           // fine

@@ -1093,7 +1093,7 @@ namespace Microsoft.Dafny {
         } else {

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

         }

-          

+

       } else if (a is CollectionTypeProxy) {

         if (b is CollectionTypeProxy) {

           a.T = b;

@@ -1117,7 +1117,7 @@ namespace Microsoft.Dafny {
         } else {

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

         }

-        

+

       } else if (a is OperationTypeProxy) {

         OperationTypeProxy pa = (OperationTypeProxy)a;

         if (b is OperationTypeProxy) {

@@ -1138,12 +1138,12 @@ namespace Microsoft.Dafny {
             return false;

           }

         }

-        

+

       } else if (a is IndexableTypeProxy) {

         Contract.Assert(b is IndexableTypeProxy);  // else we have unexpected restricted-proxy type

         a.T = b;

         return UnifyTypes(((IndexableTypeProxy)a).Arg, ((IndexableTypeProxy)b).Arg);

-        

+

       } else {

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

       }

@@ -1164,14 +1164,14 @@ namespace Microsoft.Dafny {
         if (!UnifyTypes(s.Expr.Type, Type.Bool)) {

           Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);

         }

-      

+

       } else if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

         ResolveAttributeArgs(s.Args, false);

         if (specContextOnly) {

           Error(stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

         }

-          

+

       } else if (stmt is BreakStmt) {

         var s = (BreakStmt)stmt;

         if (s.TargetLabel != null) {

@@ -1322,7 +1322,7 @@ namespace Microsoft.Dafny {
         } else {

           Error(stmt, "LHS of assignment must denote a mutable variable or field");

         }

-        

+

         s.IsGhost = lvalueIsGhost;

         Type lhsType = s.Lhs.Type;

         if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {

@@ -1362,7 +1362,7 @@ namespace Microsoft.Dafny {
         } else {

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

         }

-        

+

       } else if (stmt is VarDecl) {

         VarDecl s = (VarDecl)stmt;

         if (s.OptionalType != null) {

@@ -1377,16 +1377,16 @@ namespace Microsoft.Dafny {
           // a local variable in a specification-only context might as well be ghost

           s.IsGhost = true;

         }

-      

+

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

         ResolveCallStmt(s, specContextOnly, method, null);

-        

+

       } else if (stmt is BlockStmt) {

         scope.PushMarker();

         ResolveBlockStatement((BlockStmt)stmt, specContextOnly, method);

         scope.PopMarker();

-      

+

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

         bool branchesAreSpecOnly = specContextOnly;

@@ -1480,20 +1480,20 @@ namespace Microsoft.Dafny {
         if (!UnifyTypes(s.Collection.Type, new CollectionTypeProxy(s.BoundVar.Type))) {

           Error(s.Collection, "The type is expected to be a collection of {0} (instead got {1})", s.BoundVar.Type, s.Collection.Type);

         }

-        

+

         scope.PushMarker();

         bool b = scope.Push(s.BoundVar.Name, s.BoundVar);

         Contract.Assert(b);  // since we just pushed a marker, we expect the Push to succeed

         ResolveType(s.BoundVar.tok, s.BoundVar.Type);

         int prevErrorCount = ErrorCount;

-        

+

         ResolveExpression(s.Range, true);

         Contract.Assert(s.Range.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(s.Range.Type, Type.Bool)) {

           Error(s.Range, "range condition is expected to be of type {0}, but is {1}", Type.Bool, s.Range.Type);

         }

         bool successfullyResolvedCollectionAndRange = ErrorCount == prevErrorCount;

-        

+

         foreach (PredicateStmt ss in s.BodyPrefix) {

           ResolveStatement(ss, specContextOnly, method);

         }

@@ -1527,7 +1527,7 @@ namespace Microsoft.Dafny {
         }

 

         scope.PopMarker();

-      

+

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         bool bodyIsSpecOnly = specContextOnly;

@@ -1553,14 +1553,14 @@ namespace Microsoft.Dafny {
           Contract.Assert(sourceType != null);  // dtd and sourceType are set together above

           ctors = datatypeCtors[dtd];

           Contract.Assert(ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage

-          

+

           // build the type-parameter substitution map for this use of the datatype

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

             subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);

           }

         }

         s.IsGhost = bodyIsSpecOnly;

-        

+

         Dictionary<string,object> memberNamesUsed = new Dictionary<string,object>();  // this is really a set

         foreach (MatchCaseStmt mc in s.Cases) {

           DatatypeCtor ctor = null;

@@ -1615,8 +1615,8 @@ namespace Microsoft.Dafny {
           }

           Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);

         }

-        

-        

+

+

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();

       }

@@ -2183,7 +2183,7 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression; 

+    /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression;

     /// if null, no "match" expression will be allowed.

     /// </summary>

     void ResolveExpression(Expression expr, bool twoState, List<IVariable> matchVarContext) {

@@ -2194,7 +2194,7 @@ namespace Microsoft.Dafny {
         // expression has already been resovled

         return;

       }

-      

+

       // The following cases will resolve the subexpressions and will attempt to assign a type of expr.  However, if errors occur

       // and it cannot be determined what the type of expr is, then it is fine to leave expr.Type as null.  In that case, the end

       // of this method will assign proxy type to the expression, which reduces the number of error messages that are produced

@@ -2227,13 +2227,13 @@ namespace Microsoft.Dafny {
         } else {

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

         }

-        

+

       } else if (expr is ThisExpr) {

         if (!scope.AllowInstance) {

           Error(expr, "'this' is not allowed in a 'static' context");

         }

         expr.Type = GetThisType(expr.tok, currentClass);  // do this regardless of scope.AllowInstance, for better error reporting

-        

+

       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

         e.Var = scope.Find(e.Name);

@@ -2242,7 +2242,7 @@ namespace Microsoft.Dafny {
         } else {

           expr.Type = e.Var.Type;

         }

-      

+

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         TopLevelDecl d;

@@ -2263,7 +2263,7 @@ namespace Microsoft.Dafny {
           }

           expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt);

           ResolveType(expr.tok, expr.Type);

-          

+

           DatatypeCtor ctor;

           if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {

             Error(expr.tok, "undeclared constructor {0} in datatype {1}", dtv.MemberName, dtv.DatatypeName);

@@ -2288,7 +2288,7 @@ namespace Microsoft.Dafny {
             j++;

           }

         }

-        

+

       } else if (expr is DisplayExpression) {

         DisplayExpression e = (DisplayExpression)expr;

         Type elementType = new InferredTypeProxy();

@@ -2304,7 +2304,7 @@ namespace Microsoft.Dafny {
         } else {

           expr.Type = new SeqType(elementType);

         }

-        

+

       } else if (expr is FieldSelectExpr) {

         var e = (FieldSelectExpr)expr;

         ResolveExpression(e.Obj, twoState);

@@ -2331,7 +2331,7 @@ namespace Microsoft.Dafny {
           }

           e.Type = SubstType(e.Field.Type, subst);

         }

-      

+

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         ResolveSeqSelectExpr(e, twoState, false);

@@ -2380,11 +2380,11 @@ namespace Microsoft.Dafny {
         if (!seqErr) {

           expr.Type = e.Seq.Type;

         }

-        

+

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         ResolveFunctionCallExpr(e, twoState, false);

-        

+

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

         if (!twoState) {

@@ -2392,7 +2392,7 @@ namespace Microsoft.Dafny {
         }

         ResolveExpression(e.E, twoState);

         expr.Type = e.E.Type;

-        

+

       } else if (expr is FreshExpr) {

         FreshExpr e = (FreshExpr)expr;

         if (!twoState) {

@@ -2447,7 +2447,7 @@ namespace Microsoft.Dafny {
           default:

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

         }

-        

+

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

         ResolveExpression(e.E0, twoState);

@@ -2467,7 +2467,7 @@ namespace Microsoft.Dafny {
             }

             expr.Type = Type.Bool;

             break;

-          

+

           case BinaryExpr.Opcode.Eq:

           case BinaryExpr.Opcode.Neq:

             if (!UnifyTypes(e.E0.Type, e.E1.Type)) {

@@ -2475,7 +2475,7 @@ namespace Microsoft.Dafny {
             }

             expr.Type = Type.Bool;

             break;

-          

+

           case BinaryExpr.Opcode.Disjoint:

             if (!UnifyTypes(e.E0.Type, new SetType(new InferredTypeProxy()))) {

               Error(expr, "arguments must be of a set type (got {0})", e.E0.Type);

@@ -2485,7 +2485,7 @@ namespace Microsoft.Dafny {
             }

             expr.Type = Type.Bool;

             break;

-          

+

           case BinaryExpr.Opcode.Lt:

           case BinaryExpr.Opcode.Le:

           case BinaryExpr.Opcode.Add:

@@ -2513,7 +2513,7 @@ namespace Microsoft.Dafny {
               }

             }

             break;

-          

+

           case BinaryExpr.Opcode.Sub:

           case BinaryExpr.Opcode.Mul:

           case BinaryExpr.Opcode.Gt:

@@ -2550,7 +2550,7 @@ namespace Microsoft.Dafny {
             }

             expr.Type = Type.Bool;

             break;

-            

+

           case BinaryExpr.Opcode.Div:

           case BinaryExpr.Opcode.Mod:

             if (!UnifyTypes(e.E0.Type, Type.Int)) {

@@ -2561,12 +2561,12 @@ namespace Microsoft.Dafny {
             }

             expr.Type = Type.Int;

             break;

-          

+

           default:

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

         }

         e.ResolvedOp = ResolveOp(e.Op, e.E1.Type);

-        

+

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

         int prevErrorCount = ErrorCount;

@@ -2639,7 +2639,7 @@ namespace Microsoft.Dafny {
 

       } else if (expr is WildcardExpr) {

         expr.Type = new SetType(new ObjectType());

-        

+

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         ResolveExpression(e.Test, twoState);

@@ -2656,7 +2656,7 @@ namespace Microsoft.Dafny {
         } else {

           Error(expr, "the two branches of an if-then-else expression must have the same type (got {0} and {1})", e.Thn.Type, e.Els.Type);

         }

-      

+

       } else if (expr is MatchExpr) {

         MatchExpr me = (MatchExpr)expr;

         Contract.Assert(!twoState);  // currently, match expressions are allowed only at the outermost level of function bodies

@@ -2682,7 +2682,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(sourceType != null);  // dtd and sourceType are set together above

           ctors = datatypeCtors[dtd];

           Contract.Assert(ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage

-          

+

           IdentifierExpr ie = me.Source.Resolved as IdentifierExpr;

           if (ie == null || !(ie.Var is Formal || ie.Var is BoundVar)) {

             Error(me.Source.tok, "match source expression must be a formal parameter of the enclosing function or an enclosing match expression");

@@ -2691,13 +2691,13 @@ namespace Microsoft.Dafny {
           } else {

             goodMatchVariable = ie.Var;

           }

-          

+

           // build the type-parameter substitution map for this use of the datatype

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

             subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);

           }

         }

-        

+

         Dictionary<string,object> memberNamesUsed = new Dictionary<string,object>();  // this is really a set

         expr.Type = new InferredTypeProxy();

         foreach (MatchCaseExpr mc in me.Cases) {

@@ -2760,7 +2760,7 @@ namespace Microsoft.Dafny {
           }

           Contract.Assert(memberNamesUsed.Count + me.MissingCases.Count == dtd.Ctors.Count);

         }

-        

+

       } else {

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

       }

@@ -3479,13 +3479,13 @@ namespace Microsoft.Dafny {
         return s == null ? new HashSet<IVariable>() : s;

       }

     }

-    

+

     void ResolveReceiver(Expression expr, bool twoState)

     {

       Contract.Requires(expr != null);

       Contract.Requires(currentClass != null);

       Contract.Ensures(expr.Type != null);

-    

+

       if (expr is ThisExpr) {

         // Allow 'this' here, regardless of scope.AllowInstance.  The caller is responsible for

         // making sure 'this' does not really get used when it's not available.

@@ -3494,7 +3494,7 @@ namespace Microsoft.Dafny {
         ResolveExpression(expr, twoState);

       }

     }

-    

+

     void ResolveSeqSelectExpr(SeqSelectExpr e, bool twoState, bool allowNonUnitArraySelection) {

       Contract.Requires(e != null);

       if (e.Type != null) {

@@ -3538,7 +3538,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     /// <summary>

     /// Note: this method is allowed to be called even if "type" does not make sense for "op", as might be the case if

     /// resolution of the binary expression failed.  If so, an arbitrary resolved opcode is returned.

@@ -3647,7 +3647,7 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(expr != null);

       Contract.Requires(currentClass != null);

-    

+

       if (expr is LiteralExpr) {

         return false;

       } else if (expr is ThisExpr) {

@@ -3723,7 +3723,7 @@ namespace Microsoft.Dafny {
     [Rep] readonly List<string> names = new List<string>();  // a null means a marker

     [Rep] readonly List<Thing> things = new List<Thing>();

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(names != null);

       Contract.Invariant(things != null);

@@ -3732,7 +3732,7 @@ namespace Microsoft.Dafny {
     }

 

     int scopeSizeWhereInstancesWereDisallowed = -1;

-    

+

     public bool AllowInstance {

       get { return scopeSizeWhereInstancesWereDisallowed == -1; }

       set

@@ -3745,7 +3745,7 @@ namespace Microsoft.Dafny {
       names.Add(null);

       things.Add(null);

     }

-    

+

     public void PopMarker() {

       int n = names.Count;

       while (true) {

@@ -3760,7 +3760,7 @@ namespace Microsoft.Dafny {
         scopeSizeWhereInstancesWereDisallowed = -1;

       }

     }

-    

+

     // Pushes name-->thing association and returns "true", if name has not already been pushed since the last marker.

     // If name already has been pushed since the last marker, does nothing and returns "false".

     public bool Push(string name, Thing thing) {

@@ -3774,7 +3774,7 @@ namespace Microsoft.Dafny {
         return true;

       }

     }

-    

+

     Thing Find(string name, bool topScopeOnly) {

       Contract.Requires(name != null);

       for (int n = names.Count; 0 <= --n; ) {

@@ -3790,7 +3790,7 @@ namespace Microsoft.Dafny {
       }

       return null;  // not present

     }

-    

+

     public Thing Find(string name) {

       Contract.Requires(name != null);

       return Find(name, false);

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 19157a32..37c08ddc 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
 	//    a) whole stream in buffer

 	//    b) part of stream in buffer

 	// 2) non seekable stream (network, console)

-  

+

 	public const int EOF = 65535 + 1; // char.MaxValue + 1;

 	const int MIN_BUFFER_LENGTH = 1024; // 1KB

 	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB

@@ -31,15 +31,17 @@ public class Buffer {
 	Stream/*!*/ stream;      // input stream (seekable)

 	bool isUserStream;  // was the stream opened by the user?

 

-[ContractInvariantMethod]

-void ObjectInvariant(){

-  Contract.Invariant(buf != null);

-  Contract.Invariant(stream != null);}

-    [NotDelayed]

-	public Buffer (Stream/*!*/ s, bool isUserStream) :base() {

+	[ContractInvariantMethod]

+	void ObjectInvariant(){

+		Contract.Invariant(buf != null);

+		Contract.Invariant(stream != null);

+	}

+

+//  [NotDelayed]

+	public Buffer (Stream/*!*/ s, bool isUserStream) : base() {

 	  Contract.Requires(s != null);

 		stream = s; this.isUserStream = isUserStream;

-		

+

 		int fl, bl;

 		if (s.CanSeek) {

 			fl = (int) s.Length;

@@ -51,12 +53,12 @@ void ObjectInvariant(){
 

 		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];

 		fileLen = fl;  bufLen = bl;

-		

+

 		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)

 		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid

 		if (bufLen == fileLen && s.CanSeek) Close();

 	}

-	

+

 	protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor

 	  Contract.Requires(b != null);

 		buf = b.buf;

@@ -73,14 +75,14 @@ void ObjectInvariant(){
 	}

 

 	~Buffer() { Close(); }

-	

+

 	protected void Close() {

 		if (!isUserStream && stream != null) {

 			stream.Close();

 			//stream = null;

 		}

 	}

-	

+

 	public virtual int Read () {

 		if (bufPos < bufLen) {

 			return buf[bufPos++];

@@ -100,7 +102,7 @@ void ObjectInvariant(){
 		Pos = curPos;

 		return ch;

 	}

-	

+

 	public string/*!*/ GetString (int beg, int end) {

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

 		int len = 0;

@@ -139,7 +141,7 @@ void ObjectInvariant(){
 			}

 		}

 	}

-	

+

 	// Read the next chunk of bytes from the stream, increases the buffer

 	// if needed and updates the fields fileLen and bufLen.

 	// Returns the number of bytes read.

@@ -213,22 +215,24 @@ public class Scanner {
 	const int noSym = 104;

 

 

-[ContractInvariantMethod]

-void objectInvariant(){

-  Contract.Invariant(buffer!=null);

-  Contract.Invariant(t != null);

-  Contract.Invariant(start != null);

-  Contract.Invariant(tokens != null);

-  Contract.Invariant(pt != null);

-  Contract.Invariant(tval != null);

-  Contract.Invariant(Filename != null);

-  Contract.Invariant(errorHandler != null);

-}

+	[ContractInvariantMethod]

+	void objectInvariant(){

+		Contract.Invariant(buffer!=null);

+		Contract.Invariant(t != null);

+		Contract.Invariant(start != null);

+		Contract.Invariant(tokens != null);

+		Contract.Invariant(pt != null);

+		Contract.Invariant(tval != null);

+		Contract.Invariant(Filename != null);

+		Contract.Invariant(errorHandler != null);

+	}

+

 	public Buffer/*!*/ buffer; // scanner buffer

-	

+

 	Token/*!*/ t;          // current token

 	int ch;           // current input character

 	int pos;          // byte position of current character

+	int charPos;

 	int col;          // column number of current character

 	int line;         // line number of current character

 	int oldEols;      // EOLs that appeared in a comment;

@@ -236,13 +240,13 @@ void objectInvariant(){
 

 	Token/*!*/ tokens;     // list of tokens already peeked (first token is a dummy)

 	Token/*!*/ pt;         // current peek token

-	

+

 	char[]/*!*/ tval = new char[128]; // text of current token

 	int tlen;         // length of current token

-	

+

 	private string/*!*/ Filename;

 	private Errors/*!*/ errorHandler;

-	

+

 	static Scanner() {

 		start = new Hashtable(128);

 		for (int i = 39; i <= 39; ++i) start[i] = 1;

@@ -290,9 +294,9 @@ void objectInvariant(){
 		start[Buffer.EOF] = -1;

 

 	}

-	

-	[NotDelayed]

-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){

+

+//	[NotDelayed]

+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -302,15 +306,14 @@ void objectInvariant(){
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

 			buffer = new Buffer(stream, false);

 			Filename = fileName;

-			

 			Init();

 		} catch (IOException) {

 			throw new FatalError("Cannot open file " + fileName);

 		}

 	}

-	

-	[NotDelayed]

-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){

+

+//	[NotDelayed]

+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

@@ -319,10 +322,9 @@ void objectInvariant(){
 		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = fileName;

-		

 		Init();

 	}

-	

+

 	void Init() {

 		pos = -1; line = 1; col = 0;

 		oldEols = 0;

@@ -343,11 +345,11 @@ void objectInvariant(){
 	Contract.Ensures(Contract.Result<string>() != null);

 	  int p = buffer.Pos;

 	  int ch = buffer.Read();

-      // replace isolated '\r' by '\n' in order to make

+	  // replace isolated '\r' by '\n' in order to make

 	  // eol handling uniform across Windows, Unix and Mac

 	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 	  while (ch != EOL && ch != Buffer.EOF){

-	    ch = buffer.Read();

+		ch = buffer.Read();

 		// replace isolated '\r' by '\n' in order to make

 		// eol handling uniform across Windows, Unix and Mac

 		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

@@ -358,7 +360,7 @@ void objectInvariant(){
 	}

 

 	void NextCh() {

-		if (oldEols > 0) { ch = EOL; oldEols--; } 

+		if (oldEols > 0) { ch = EOL; oldEols--; }

 		else {

 //			pos = buffer.Pos;

 //			ch = buffer.Read(); col++;

@@ -366,9 +368,9 @@ void objectInvariant(){
 //			// eol handling uniform across Windows, Unix and Mac

 //			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 //			if (ch == EOL) { line++; col = 0; }

-			

+

 			while (true) {

-			    pos = buffer.Pos;

+				pos = buffer.Pos;

 				ch = buffer.Read(); col++;

 				// replace isolated '\r' by '\n' in order to make

 				// eol handling uniform across Windows, Unix and Mac

@@ -418,7 +420,7 @@ void objectInvariant(){
 				return;

 			  }

 

-			

+

 		}

 

 	}

@@ -438,7 +440,7 @@ void objectInvariant(){
 

 

 	bool Comment0() {

-		int level = 1, pos0 = pos, line0 = line, col0 = col;

+		int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos;

 		NextCh();

 		if (ch == '/') {

 			NextCh();

@@ -451,13 +453,13 @@ void objectInvariant(){
 				else NextCh();

 			}

 		} else {

-			buffer.Pos = pos0; NextCh(); line = line0; col = col0;

+			buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0;

 		}

 		return false;

 	}

 

 	bool Comment1() {

-		int level = 1, pos0 = pos, line0 = line, col0 = col;

+		int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos;

 		NextCh();

 		if (ch == '*') {

 			NextCh();

@@ -478,7 +480,7 @@ void objectInvariant(){
 				else NextCh();

 			}

 		} else {

-			buffer.Pos = pos0; NextCh(); line = line0; col = col0;

+			buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0;

 		}

 		return false;

 	}

@@ -555,10 +557,13 @@ void objectInvariant(){
 		t.pos = pos; t.col = col; t.line = line;

 		t.filename = this.Filename;

 		int state;

-		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }

+		if (start.ContainsKey(ch)) {

+			Contract.Assert(start[ch] != null);

+			state = (int) start[ch];

+		}

 		else { state = 0; }

 		tlen = 0; AddCh();

-		

+

 		switch (state) {

 			case -1: { t.kind = eofSym; break; } // NextCh already done

 			case 0: {

@@ -764,14 +769,14 @@ void objectInvariant(){
 		t.val = new String(tval, 0, tlen);

 		return t;

 	}

-	

+

 	private void SetScannerBehindT() {

 		buffer.Pos = t.pos;

 		NextCh();

 		line = t.line; col = t.col;

 		for (int i = 0; i < tlen; i++) NextCh();

 	}

-	

+

 	// get the next token (possibly a token already seen during peeking)

 	public Token/*!*/ Scan () {

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

@@ -792,7 +797,7 @@ void objectInvariant(){
 			}

 			pt = pt.next;

 		} while (pt.kind > maxT); // skip pragmas

-	

+

 		return pt;

 	}

 

diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs
index 9f4b22c5..4ae1c185 100644
--- a/Source/Dafny/SccGraph.cs
+++ b/Source/Dafny/SccGraph.cs
@@ -12,14 +12,14 @@ namespace Microsoft.Dafny {
       public readonly List<Vertex/*!*/>/*!*/ Successors = new List<Vertex/*!*/>();

       public List<Vertex/*!*/> SccMembers;  // non-null only for the representative of the SCC

       [ContractInvariantMethod]

-      void ObjectInvariant() 

+      void ObjectInvariant()

       {

         Contract.Invariant(cce.NonNullElements(Successors));

         Contract.Invariant(SccMembers==null || cce.NonNullElements(SccMembers));

       }

 

       public Vertex SccRepresentative;  // null if not computed

-      

+

       public int SccId;  // valid only for SCC representatives; indicates position of this representative vertex in the graph's topological sort

       // the following field is used during the computation of SCCs and of reachability

       public VisitedStatus Visited;

@@ -28,7 +28,7 @@ namespace Microsoft.Dafny {
       public int LowLink;

       // the following field is used during a Reaches computation

       public int Gen;  // generation <= Gen means this vertex has been visited in the current generation

-      

+

       public Vertex(Node n) {

         N = n;

       }

@@ -40,7 +40,7 @@ namespace Microsoft.Dafny {
 

 

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(vertices!=null);

       Contract.Invariant(cce.NonNullElements(vertices.Values));

@@ -51,7 +51,7 @@ namespace Microsoft.Dafny {
     Dictionary<Node, Vertex/*!*/>/*!*/ vertices = new Dictionary<Node, Vertex/*!*/>();

     bool sccComputed = false;

     List<Vertex/*!*/> topologicallySortedRepresentatives;  // computed by the SCC computation

-    

+

     public int SccCount {

       get {

         ComputeSCCs();

@@ -60,11 +60,11 @@ namespace Microsoft.Dafny {
       }

     }

     int generation = 0;

-    

+

     public Graph()

     {

     }

-    

+

     /// <summary>

     /// Idempotently adds a vertex 'n' to the graph.

     /// </summary>

@@ -74,7 +74,7 @@ namespace Microsoft.Dafny {
 

     /// <summary>

     /// Idempotently adds a vertex 'n' to the graph and then returns the Vertex for it.

-    /// </summary>    

+    /// </summary>

     Vertex GetVertex(Node n) {

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

 

@@ -93,7 +93,7 @@ namespace Microsoft.Dafny {
       }

       return v;

     }

-    

+

     /// <summary>

     /// Returns the vertex for 'n' if 'n' is in the graph.  Otherwise, returns null.

     /// </summary>

@@ -117,7 +117,7 @@ namespace Microsoft.Dafny {
       v0.AddSuccessor(v1);

       sccComputed = false;  // the addition of an edge may invalidate any previous computation of the graph's SCCs

     }

-    

+

     /// <summary>

     /// Idempotently adds 'n' as a vertex and then returns a Node that is the representative element of the

     /// strongly connected component containing 'n'.

@@ -125,7 +125,7 @@ namespace Microsoft.Dafny {
     public Node GetSCCRepresentative(Node n) {

       return GetSCCRepr(n).N;

     }

-    

+

     /// <summary>

     /// Idempotently adds 'n' as a vertex.  Then, returns the number of SCCs before the SCC of 'n' in the

     /// topologically sorting of SCCs.

@@ -133,7 +133,7 @@ namespace Microsoft.Dafny {
     public int GetSCCRepresentativeId(Node n) {

       return GetSCCRepr(n).SccId;

     }

-    

+

     Vertex GetSCCRepr(Node n) {

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

 

@@ -142,7 +142,7 @@ namespace Microsoft.Dafny {
       Contract.Assert(v.SccRepresentative != null);  // follows from what ComputeSCCs does

       return v.SccRepresentative;

     }

-    

+

     /// <summary>

     /// Returns a list of the topologically sorted SCCs, each represented in the list by its representative node.

     /// </summary>

@@ -172,21 +172,21 @@ namespace Microsoft.Dafny {
       }

       return nn;

     }

-    

+

     /// <summary>

     /// Idempotently adds 'n' as a vertex and then returns the size of the set of Node's in the strongly connected component

     /// that contains 'n'.

     /// </summary>

     public int GetSCCSize(Node n){

       Contract.Ensures(1 <= Contract.Result<int>());

-    

+

       Vertex v = GetVertex(n);

       ComputeSCCs();

       Vertex repr = v.SccRepresentative;

       Contract.Assert(repr != null && repr.SccMembers != null);  // follows from postcondition of ComputeSCCs

       return repr.SccMembers.Count;

     }

-    

+

     /// <summary>

     /// This method sets the SccRepresentative fields of the graph's vertices so that two

     /// vertices have the same representative iff they are in the same strongly connected

@@ -197,7 +197,7 @@ namespace Microsoft.Dafny {
     void ComputeSCCs()

     {

       Contract.Ensures(sccComputed);

-    

+

       if (sccComputed) { return; }  // check if already computed

 

       // reset all SCC information

@@ -217,7 +217,7 @@ namespace Microsoft.Dafny {
 

       sccComputed = true;

     }

-    

+

     /// <summary>

     /// This is the 'SearchC' procedure from the Aho, Hopcroft, and Ullman book 'The Design and Analysis of Computer Algorithms'.

     /// </summary>

@@ -227,13 +227,13 @@ namespace Microsoft.Dafny {
      Contract.Requires(v.Visited == VisitedStatus.Unvisited);

      Contract.Requires(topologicallySortedRepresentatives != null);

       Contract.Ensures(v.Visited != VisitedStatus.Unvisited);

-    

+

       v.DfNumber = cnt;

       cnt++;

       v.LowLink = v.DfNumber;

       stack.Push(v);

       v.Visited = VisitedStatus.OnStack;

-      

+

       foreach (Vertex w in v.Successors) {

         if (w.Visited == VisitedStatus.Unvisited) {

           SearchC(w, stack, ref cnt);

@@ -243,7 +243,7 @@ namespace Microsoft.Dafny {
           v.LowLink = Math.Min(v.LowLink, w.DfNumber);

         }

       }

-      

+

       if (v.LowLink == v.DfNumber) {

         // The SCC containing 'v' has now been computed.

         v.SccId = topologicallySortedRepresentatives.Count;

@@ -258,7 +258,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     /// <summary>

     /// Returns null if the graph has no cycles.  If the graph does contain some cycle, returns the list of

     /// vertices on one such cycle.

@@ -268,7 +268,7 @@ namespace Microsoft.Dafny {
       foreach (Vertex v in vertices.Values) {

         v.Visited = VisitedStatus.Unvisited;

       }

-      

+

       foreach (Vertex v in vertices.Values) {

         Contract.Assert(v.Visited != VisitedStatus.OnStack);

         if (v.Visited == VisitedStatus.Unvisited) {

@@ -284,7 +284,7 @@ namespace Microsoft.Dafny {
       }

       return null;  // there are no cycles

     }

-    

+

     /// <summary>

     /// A return of null means there are no cycles involving any vertex in the subtree rooted at v.

     /// A non-null return means a cycle has been found.  Then:

@@ -300,7 +300,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(v.Visited != VisitedStatus.Unvisited);

       Contract.Ensures(Contract.Result<List<Vertex>>() != null || v.Visited == VisitedStatus.Visited);

       Contract.Ensures(Contract.Result<List<Vertex>>() == null || Contract.Result<List<Vertex>>().Count != 0);

-    

+

       v.Visited = VisitedStatus.OnStack;

       foreach (Vertex succ in v.Successors) {

         // todo:  I would use a 'switch' statement, but there seems to be a bug in the Spec# compiler's type checking.

@@ -337,7 +337,7 @@ namespace Microsoft.Dafny {
       v.Visited = VisitedStatus.Visited;  // there are no cycles from here on

       return null;

     }

-    

+

     /// <summary>

     /// Returns whether or not 'source' reaches 'sink' in the graph.

     /// 'source' and 'sink' need not be in the graph; if neither is, the return value

@@ -352,7 +352,7 @@ namespace Microsoft.Dafny {
       generation++;

       return ReachSearch(a, b);

     }

-    

+

     bool ReachSearch(Vertex source, Vertex sink) {

       Contract.Requires(source != null);

       Contract.Requires(sink != null);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index d1c77122..74d33479 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -21,14 +21,14 @@ namespace Microsoft.Dafny {
         predef = FindPredefinedDecls(boogieProgram);

       }

     }

-    

+

     // translation state

     readonly Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>/*!*/ classes = new Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>();

     readonly Dictionary<Field/*!*/,Bpl.Constant/*!*/>/*!*/ fields = new Dictionary<Field/*!*/,Bpl.Constant/*!*/>();

     readonly Dictionary<Field/*!*/, Bpl.Function/*!*/>/*!*/ fieldFunctions = new Dictionary<Field/*!*/, Bpl.Function/*!*/>();

 

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(cce.NonNullDictionaryAndValues(classes));

       Contract.Invariant(cce.NonNullDictionaryAndValues(fields));

@@ -77,14 +77,14 @@ namespace Microsoft.Dafny {
 

         return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));

       }

-      

+

       public Bpl.Type SeqType(IToken tok, Bpl.Type ty) {

         Contract.Requires(tok != null);

         Contract.Requires(ty != null);

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

         return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));

       }

-      

+

       public Bpl.Type FieldName(IToken tok, Bpl.Type ty) {

         Contract.Requires(tok != null);

         Contract.Requires(ty != null);

@@ -92,7 +92,7 @@ namespace Microsoft.Dafny {
 

         return new Bpl.CtorType(tok, fieldName, new Bpl.TypeSeq(ty));

       }

-      

+

       public Bpl.IdentifierExpr Alloc(IToken tok) {

         Contract.Requires(tok != null);

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

@@ -135,14 +135,14 @@ namespace Microsoft.Dafny {
         this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);

       }

     }

-    

+

     static PredefinedDecls FindPredefinedDecls(Bpl.Program prog) {

       Contract.Requires(prog != null);

       if (prog.Resolve() != 0) {

         Console.WriteLine("Error: resolution errors encountered in Dafny prelude");

         return null;

       }

-      

+

       Bpl.TypeCtorDecl refType = null;

       Bpl.TypeSynonymDecl setTypeCtor = null;

       Bpl.TypeCtorDecl seqTypeCtor = null;

@@ -220,7 +220,7 @@ namespace Microsoft.Dafny {
       }

       return null;

     }

-    

+

     static Bpl.Program ReadPrelude() {

       string preludePath = Bpl.CommandLineOptions.Clo.DafnyPrelude;

       if (preludePath == null)

@@ -229,7 +229,7 @@ namespace Microsoft.Dafny {
           string codebase = cce.NonNull(System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));

           preludePath = System.IO.Path.Combine(codebase, "DafnyPrelude.bpl");

       }

-      

+

       Bpl.Program prelude;

       int errorCount = Bpl.Parser.Parse(preludePath, null, out prelude);

       if (prelude == null || errorCount > 0) {

@@ -237,7 +237,7 @@ namespace Microsoft.Dafny {
       } else {

         return prelude;

       }

-/*      

+/*

       List<string!> defines = new List<string!>();

       using (System.IO.Stream stream = new System.IO.FileStream(preludePath, System.IO.FileMode.Open, System.IO.FileAccess.Read))

       {

@@ -251,9 +251,9 @@ namespace Microsoft.Dafny {
           return prelude;

         }

       }

-*/      

+*/

     }

-    

+

     public Bpl.Program Translate(Program program) {

       Contract.Requires(program != null);

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

@@ -282,13 +282,13 @@ namespace Microsoft.Dafny {
       }

       return sink;

     }

-    

+

     void AddDatatype(DatatypeDecl dt)

     {

       Contract.Requires(dt != null);

       Contract.Requires(sink != null && predef != null);

       sink.TopLevelDeclarations.Add(GetClass(dt));

-    

+

       foreach (DatatypeCtor ctor in dt.Ctors) {

         // Add:  function #dt.ctor(paramTypes) returns (DatatypeType);

         Bpl.VariableSeq argTypes = new Bpl.VariableSeq();

@@ -348,7 +348,7 @@ namespace Microsoft.Dafny {
         fn.Body = Bpl.Expr.Eq(lhs, new Bpl.IdentifierExpr(ctor.tok, cid));  // this uses the "cid" defined for the previous axiom

         sink.TopLevelDeclarations.Add(fn);

 

-        // Add:  axiom (forall params, h: HeapType :: 

+        // Add:  axiom (forall params, h: HeapType ::

         //                 { DtAlloc(#dt.ctor(params), h) }

         //                 $IsGoodHeap(h) ==>

         //                     (DtAlloc(#dt.ctor(params), h) <==> ...each param has its expected type...));

@@ -440,7 +440,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     void CreateBoundVariables(List<Formal/*!*/>/*!*/ formals, out Bpl.VariableSeq/*!*/ bvs, out List<Bpl.Expr/*!*/>/*!*/ args)

     {

       Contract.Requires(formals != null);

@@ -459,13 +459,13 @@ namespace Microsoft.Dafny {
         args.Add(new Bpl.IdentifierExpr(arg.tok, bv));

       }

     }

-    

+

     void AddClassMembers(ClassDecl c)

     {

       Contract.Requires(sink != null && predef != null);

       Contract.Requires(c != null);

       sink.TopLevelDeclarations.Add(GetClass(c));

-      

+

       foreach (MemberDecl member in c.Members) {

         if (member is Field) {

           Field f = (Field)member;

@@ -478,7 +478,7 @@ namespace Microsoft.Dafny {
           }

 

           AddAllocationAxiom(f);

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           AddFunction(f);

@@ -500,7 +500,7 @@ namespace Microsoft.Dafny {
           }

           AddFrameAxiom(f);

           AddWellformednessCheck(f);

-          

+

         } else if (member is Method) {

           Method m = (Method)member;

           // wellformedness check for method specification

@@ -514,14 +514,14 @@ namespace Microsoft.Dafny {
             // ...and its implementation

             AddMethodImpl(m, proc, false);

           }

-          

+

           // refinement condition

           if (member is MethodRefinement) {

             AddMethodRefinement((MethodRefinement)member);

           }

-        

+

         } else if (member is CouplingInvariant) {

-          // TODO: define a well-foundedness condition to check          

+          // TODO: define a well-foundedness condition to check

 

         } else {

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

@@ -616,9 +616,9 @@ namespace Microsoft.Dafny {
       Contract.Requires(layerOffset == 0 || (layerOffset == 1 && f.IsRecursive && !f.IsUnlimited));

       Contract.Requires(predef != null);

       Contract.Requires(f.EnclosingClass != null);

- 

+

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

-      

+

       // axiom

       //   mh < ModuleContextHeight ||

       //   (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext))

@@ -659,7 +659,7 @@ namespace Microsoft.Dafny {
       args.Add(new Bpl.IdentifierExpr(f.tok, bv));

       // ante:  $IsHeap($Heap) && this != null && formals-have-the-expected-types &&

       Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);

-      

+

       Bpl.BoundVariable bvThis;

       Bpl.Expr bvThisIdExpr;

       if (f.IsStatic) {

@@ -711,7 +711,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr.Or(

             Bpl.Expr.Le(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()),

             etran.InMethodContext())));

-      

+

       var substMap = new Dictionary<IVariable, Expression>();

       if (specialization != null) {

         substMap = specialization.SubstMap;

@@ -770,7 +770,7 @@ namespace Microsoft.Dafny {
       }

       return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);

     }

-    

+

     void AddLimitedAxioms(Function f, int fromLayer) {

       Contract.Requires(f != null);

       Contract.Requires(f.IsRecursive && !f.IsUnlimited);

@@ -807,7 +807,7 @@ namespace Microsoft.Dafny {
       Bpl.Expr origFuncAppl = new Bpl.NAryExpr(f.tok, origFuncID, args);

       Bpl.FunctionCall limitedFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, fromLayer-1), TrType(f.ResultType)));

       Bpl.Expr limitedFuncAppl = new Bpl.NAryExpr(f.tok, limitedFuncID, args);

-      

+

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

 

       Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(origFuncAppl));

@@ -833,7 +833,7 @@ namespace Microsoft.Dafny {
       }

       return name;

     }

-    

+

     /// <summary>

     /// Generate:

     ///   axiom (forall h: [ref, Field x]x, o: ref ::

@@ -844,13 +844,13 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(f != null);

       Contract.Requires(sink != null && predef != null);

-    

+

       Bpl.BoundVariable hVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h", predef.HeapType));

       Bpl.Expr h = new Bpl.IdentifierExpr(f.tok, hVar);

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, h);

       Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));

       Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);

-      

+

       // h[o,f]

       Bpl.Expr oDotF;

       if (f.IsMutable) {

@@ -894,7 +894,7 @@ namespace Microsoft.Dafny {
       }

       return Bpl.Expr.And(lower, upper);

     }

-    

+

     Method currentMethod = null;  // the method whose implementation is currently being translated

     int loopHeapVarCount = 0;

     int otherTmpVarCount = 0;

@@ -927,7 +927,7 @@ namespace Microsoft.Dafny {
 

       return GetTmpVar_IdExpr(tok, "$prevHeap", predef.HeapType, locals);

     }

-    

+

     Bpl.IdentifierExpr GetNewVar_IdExpr(IToken tok, Bpl.VariableSeq locals)  // local variable that's shared between statements that need it

     {

       Contract.Requires(tok != null);

@@ -970,7 +970,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(wellformednessProc || m.Body != null);

       Contract.Requires(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);

       Contract.Ensures(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);

-    

+

       currentMethod = m;

 

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);

@@ -1032,7 +1032,7 @@ namespace Microsoft.Dafny {
         typeParams, inParams, outParams,

         localVariables, stmts);

       sink.TopLevelDeclarations.Add(impl);

-      

+

       currentMethod = null;

       loopHeapVarCount = 0;

       otherTmpVarCount = 0;

@@ -1047,7 +1047,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);

       Contract.Requires(localVariables != null);

       Contract.Requires(predef != null);

-    

+

       // set up the information used to verify the method's modifies clause

       DefineFrame(m.tok, m.Mod, builder, localVariables, null);

     }

@@ -1064,14 +1064,14 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);

       return CaptureState(tok, null);

     }

-    

+

     void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables, string name){

       Contract.Requires(tok != null);

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

       Contract.Requires(builder != null);

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

       Contract.Requires(predef != null);

-    

+

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);

       // Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool

       Bpl.IdentifierExpr theFrame = etran.TheFrame(tok);  // this is a throw-away expression, used only to extract the type of the $_Frame variable

@@ -1088,7 +1088,7 @@ namespace Microsoft.Dafny {
       Bpl.Expr consequent = InRWClause(tok, o, f, frameClause, etran, null, null);

       Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null,

                                            Bpl.Expr.Imp(ante, consequent));

-    

+

       builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));

     }

 

@@ -1119,7 +1119,7 @@ namespace Microsoft.Dafny {
                                       Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), inEnclosingFrame));

       builder.Add(Assert(tok, q, errorMessage, kv));

     }

-    

+

     /// <summary>

     /// Generates:

     ///   axiom (forall h0: HeapType, h1: HeapType, formals... ::

@@ -1141,18 +1141,18 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(f != null);

       Contract.Requires(sink != null && predef != null);

-    

+

       Bpl.BoundVariable h0Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h0", predef.HeapType));

       Bpl.BoundVariable h1Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h1", predef.HeapType));

       Bpl.Expr h0 = new Bpl.IdentifierExpr(f.tok, h0Var);

       Bpl.Expr h1 = new Bpl.IdentifierExpr(f.tok, h1Var);

       ExpressionTranslator etran0 = new ExpressionTranslator(this, predef, h0);

       ExpressionTranslator etran1 = new ExpressionTranslator(this, predef, h1);

-      

+

       Bpl.Expr wellFormed = Bpl.Expr.And(

         FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr),

         FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran1.HeapExpr));

-      

+

       Bpl.TypeVariable alpha = new Bpl.TypeVariable(f.tok, "alpha");

       Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));

       Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);

@@ -1161,12 +1161,12 @@ namespace Microsoft.Dafny {
       Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);

       Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o)));

       Bpl.Expr unchanged = Bpl.Expr.Eq(ExpressionTranslator.ReadHeap(f.tok, h0, o, field), ExpressionTranslator.ReadHeap(f.tok, h1, o, field));

-      

+

       Bpl.Expr heapSucc = FunctionCall(f.tok, BuiltinFunction.HeapSucc, null, h0, h1);

       Bpl.Expr r0 = InRWClause(f.tok, o, field, f.Reads, etran0, null, null);

       Bpl.Expr q0 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),

         Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r0), unchanged));

-      

+

       // bvars:  h0, h1, formals

       // f0args:  h0, formals

       // f1args:  h1, formals

@@ -1200,7 +1200,7 @@ namespace Microsoft.Dafny {
         wh = GetWhereClause(p.tok, formal, p.Type, etran1);

         if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }

       }

-      

+

       string axiomComment = "frame axiom for " + f.FullName;

       Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));

       while (fn != null) {

@@ -1208,7 +1208,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);

         Bpl.Expr eq = Bpl.Expr.Eq(F0, F1);

         Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(heapSucc, F1));

-        

+

         Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

         Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,

           Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, heapSucc),

@@ -1222,7 +1222,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     Bpl.Expr/*!*/ InRWClause(IToken/*!*/ tok, Bpl.Expr/*!*/ o, Bpl.Expr/*!*/ f, List<FrameExpression/*!*/>/*!*/ rw, ExpressionTranslator/*!*/ etran,

                              Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/> substMap) {

       Contract.Requires(tok != null);

@@ -1237,7 +1237,7 @@ namespace Microsoft.Dafny {
 

       // requires o to denote an expression of type RefType

       // "rw" is is allowed to contain a WildcardExpr

-    

+

       Bpl.Expr disjunction = null;

       foreach (FrameExpression rwComponent in rw) {

         Expression e = rwComponent.E;

@@ -1280,12 +1280,12 @@ namespace Microsoft.Dafny {
         return disjunction;

       }

     }

-    

+

     void AddWellformednessCheck(Function f) {

       Contract.Requires(f != null);

       Contract.Requires(sink != null && predef != null);

       Contract.Requires(f.EnclosingClass != null);

-    

+

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

       // parameters of the procedure

       Bpl.VariableSeq inParams = new Bpl.VariableSeq();

@@ -1317,7 +1317,7 @@ namespace Microsoft.Dafny {
       VariableSeq implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);

       Bpl.VariableSeq locals = new Bpl.VariableSeq();

       Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

-      

+

       // check well-formedness of the preconditions (including termination, but no reads checks), and then

       // assume each one of them

       foreach (Expression p in f.Req) {

@@ -1423,7 +1423,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);Contract.Requires(etran != null);

       Contract.Requires(predef != null);

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

-    

+

       if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {

         return Bpl.Expr.True;

       } else if (expr is DisplayExpression) {

@@ -1586,7 +1586,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

       }

     }

-    

+

     Bpl.Expr/*!*/ IsTotal(List<Expression/*!*/>/*!*/ exprs, ExpressionTranslator/*!*/ etran) {

       Contract.Requires(etran != null);

       Contract.Requires(exprs != null);

@@ -1746,7 +1746,7 @@ namespace Microsoft.Dafny {
         return Bpl.Expr.And(a, b);

       }

     }

-    

+

     Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -1758,14 +1758,14 @@ namespace Microsoft.Dafny {
         return Bpl.Expr.Imp(a, b);

       }

     }

-    

+

     void CheckNonNull(IToken tok, Expression e, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Bpl.QKeyValue kv) {

       Contract.Requires(tok != null);

       Contract.Requires(e != null);

       Contract.Requires(builder != null);

       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

-    

+

       if (e is ThisExpr) {

         // already known to be non-null

       } else {

@@ -1840,7 +1840,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);

       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

-    

+

       if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {

         // always allowed

       } else if (expr is DisplayExpression) {

@@ -2084,7 +2084,7 @@ namespace Microsoft.Dafny {
         CheckWellformed(e.Thn, options, locals, bThen, etran);

         CheckWellformed(e.Els, options, locals, bElse, etran);

         builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.Test), bThen.Collect(expr.tok), null, bElse.Collect(expr.tok)));

-      

+

       } else if (expr is MatchExpr) {

         MatchExpr me = (MatchExpr)expr;

         CheckWellformed(me.Source, options, locals, builder, etran);

@@ -2308,7 +2308,7 @@ namespace Microsoft.Dafny {
         return s;

       }

     }

-    

+

     Bpl.Constant GetClass(TopLevelDecl cl)

     {

       Contract.Requires(cl != null);

@@ -2324,7 +2324,7 @@ namespace Microsoft.Dafny {
       }

       return cc;

     }

-    

+

     Bpl.Expr GetTypeExpr(IToken tok, Type type)

     {

       Contract.Requires(tok != null);

@@ -2373,13 +2373,13 @@ namespace Microsoft.Dafny {
         return t;

       }

     }

-    

+

     Bpl.Constant GetField(Field f)

     {

       Contract.Requires(f != null && f.IsMutable);

       Contract.Requires(sink != null && predef != null);

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

-     

+

       Bpl.Constant fc;

       if (fields.TryGetValue(f, out fc)) {

         Contract.Assert(fc != null);

@@ -2434,13 +2434,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(fse != null);

       Contract.Requires(fse.Field != null && fse.Field.IsMutable);

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

-     

+

       return new Bpl.IdentifierExpr(fse.tok, GetField(fse.Field));

     }

 

     /// <summary>

     /// This method is expected to be called just once for each function in the program.

-    /// </summary>    

+    /// </summary>

     void AddFunction(Function f)

     {

       Contract.Requires(f != null);

@@ -2457,7 +2457,7 @@ namespace Microsoft.Dafny {
       Bpl.Formal res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, TrType(f.ResultType)), false);

       Bpl.Function func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res);

       sink.TopLevelDeclarations.Add(func);

-      

+

       if (f.IsRecursive && !f.IsUnlimited) {

         sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 0), args, res));

         sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 2), args, res));

@@ -2467,12 +2467,12 @@ namespace Microsoft.Dafny {
       Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullName + "#canCall", args, res);

       sink.TopLevelDeclarations.Add(canCallF);

     }

-    

+

     /// <summary>

     /// This method is expected to be called just twice for each procedure in the program (once with

     /// wellformednessProc set to true, once with wellformednessProc set to false).

     /// In addition, it is used once to generate refinement conditions.

-    /// </summary>    

+    /// </summary>

     Bpl.Procedure AddMethod(Method m, bool wellformednessProc, bool skipEnsures)

     {

       Contract.Requires(m != null);

@@ -2482,7 +2482,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<Bpl.Procedure>() != null);

 

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);

-      

+

       Bpl.VariableSeq inParams = new Bpl.VariableSeq();

       Bpl.VariableSeq outParams = new Bpl.VariableSeq();

       if (!m.IsStatic) {

@@ -2502,7 +2502,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

         outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false));

       }

-      

+

       Bpl.RequiresSeq req = new Bpl.RequiresSeq();

       Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();

       Bpl.EnsuresSeq ens = new Bpl.EnsuresSeq();

@@ -2513,7 +2513,7 @@ namespace Microsoft.Dafny {
       req.Add(Requires(m.tok, true, context, null, null));

       mod.Add(etran.HeapExpr);

       mod.Add(etran.Tick());

-      

+

       if (!wellformednessProc) {

         string comment = "user-defined preconditions";

         foreach (MaybeFreeExpression p in m.Req) {

@@ -2551,54 +2551,54 @@ namespace Microsoft.Dafny {
       return proc;

     }

 

-    #region Refinement extension    

-    

-    void AddMethodRefinement(MethodRefinement m) 

+    #region Refinement extension

+

+    void AddMethodRefinement(MethodRefinement m)

      {

       Contract.Requires(m != null);

       Contract.Requires(sink != null && predef != null);

-      // r is abstract, m is concrete 

+      // r is abstract, m is concrete

       Method r = m.Refined;

       Contract.Assert(r != null);

       Contract.Assert(m.EnclosingClass != null);

       string name = "Refinement$$" + m.FullName;

       string that = "that";

-      

+

       Bpl.IdentifierExpr heap = new Bpl.IdentifierExpr(m.tok, predef.HeapVarName, predef.HeapType);

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, heap, that);

-      

+

       // TODO: this straight inlining does not handle recursive calls

-      // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure, or check refinement of frames      

-            

+      // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure, or check refinement of frames

+

       // generate procedure declaration with pre-condition wp(r, true)

       Bpl.Procedure proc = AddMethod(r, false, true);

       proc.Name = name;

-      

+

       // create "that" for m

       Bpl.Expr wh = Bpl.Expr.And(

         Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, that, predef.RefType), predef.Null),

         etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, that, predef.RefType), Resolver.GetReceiverType(m.tok, m)));

       Bpl.Formal thatVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, that, predef.RefType, wh), true);

       proc.InParams.Add(thatVar);

-      

-      // add outs of m to the outs of the refinement procedure   

+

+      // add outs of m to the outs of the refinement procedure

       foreach (Formal p in m.Outs) {

         Bpl.Type varType = TrType(p.Type);

         Bpl.Expr w = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

         proc.OutParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, w), false));

       }

       sink.TopLevelDeclarations.Add(proc);

-           

-      // generate procedure implementation:      

+

+      // generate procedure implementation:

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);

       Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);

       Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);

       Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

       Bpl.VariableSeq localVariables = new Bpl.VariableSeq();

-      

+

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

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

-      

+

       // declare a frame variable that allows anything to be changed (not checking modifies clauses)

       Bpl.IdentifierExpr theFrame = etran.TheFrame(m.tok);

       Contract.Assert(theFrame.Type != null);

@@ -2610,12 +2610,12 @@ namespace Microsoft.Dafny {
       Bpl.BoundVariable fVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$f", predef.FieldName(m.tok, alpha)));

       Bpl.Expr lambda = new Bpl.LambdaExpr(m.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, Bpl.Expr.True);

       builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, frame), lambda));

-      

-      // assume I($Heap, $Heap)              

+

+      // assume I($Heap, $Heap)

       builder.Add(new Bpl.AssumeCmd(m.tok, TrCouplingInvariant(m, heap, "this", heap, that)));

-      

+

       // assign input formals of m (except "this")

-      for (int i = 0; i < m.Ins.Count; i++) {        

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

         Bpl.LocalVariable arg = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, m.Ins[i].UniqueName, TrType(m.Ins[i].Type)));

         localVariables.Add(arg);

         Bpl.Variable var = inParams[i+1];

@@ -2628,7 +2628,7 @@ namespace Microsoft.Dafny {
       loopHeapVarCount = 0;

       otherTmpVarCount = 0;

       _tmpIEs.Clear();

-            

+

       //  call inlined m;

       TrStmt(m.Body, builder, localVariables, etran);

 

@@ -2636,10 +2636,10 @@ namespace Microsoft.Dafny {
       Bpl.LocalVariable heap2 = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, heap.Name+"2", predef.HeapType));

       localVariables.Add(heap2);

       builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, heap2), etran.HeapExpr));

-      

+

       //  $Heap := old($Heap);

       builder.Add(Bpl.Cmd.SimpleAssign(m.tok, heap, new Bpl.OldExpr(m.tok, heap)));

-                                

+

       //  call inlined r;

       currentMethod = r;

       etran = new ExpressionTranslator(this, predef, heap);

@@ -2650,7 +2650,7 @@ namespace Microsoft.Dafny {
       loopHeapVarCount = 0;

       otherTmpVarCount = 0;

       _tmpIEs.Clear();

-      

+

       // assert output variables of r and m are pairwise equal

       Contract.Assert(outParams.Length % 2 == 0);

       int k = outParams.Length / 2;

@@ -2658,21 +2658,21 @@ namespace Microsoft.Dafny {
         Bpl.Variable rOut = outParams[i];

         Bpl.Variable mOut = outParams[i+k];

         Contract.Assert(rOut != null && mOut != null);

-        builder.Add(Assert(m.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(m.tok, mOut), new Bpl.IdentifierExpr(m.tok, rOut)), 

+        builder.Add(Assert(m.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(m.tok, mOut), new Bpl.IdentifierExpr(m.tok, rOut)),

           "Refinement method may not produce the same value for output variable " + m.Outs[i].Name));

       }

-            

-      // assert I($Heap1, $Heap)      

+

+      // assert I($Heap1, $Heap)

       builder.Add(Assert(m.tok, TrCouplingInvariant(m, heap, "this", new Bpl.IdentifierExpr(m.tok, heap2), that),

         "Refinement method may not preserve the coupling invariant"));

-                                                

+

       Bpl.StmtList stmts = builder.Collect(m.tok);

       Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,

         typeParams, inParams, outParams,

         localVariables, stmts);

       sink.TopLevelDeclarations.Add(impl);

     }

-    

+

     private sealed class NominalSubstituter : Duplicator

     {

       private readonly Dictionary<string,Bpl.Expr> subst;

@@ -2686,7 +2686,7 @@ namespace Microsoft.Dafny {
         Contract.Invariant(cce.NonNullDictionaryAndValues(subst));

       }

 

-          

+

       public override Expr VisitIdentifierExpr(Bpl.IdentifierExpr node)

       {

         Contract.Requires(node != null);

@@ -2694,7 +2694,7 @@ namespace Microsoft.Dafny {
 

         if (subst.ContainsKey(node.Name))

           return subst[node.Name];

-        else 

+        else

           return base.VisitIdentifierExpr(node);

       }

     }

@@ -2711,32 +2711,32 @@ namespace Microsoft.Dafny {
       ClassRefinementDecl c = m.EnclosingClass as ClassRefinementDecl;

       Contract.Assert(c != null);

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, conHeap, conThis);

-            

-      foreach (MemberDecl d in c.Members) 

+

+      foreach (MemberDecl d in c.Members)

         if (d is CouplingInvariant) {

           CouplingInvariant inv = (CouplingInvariant)d;

 

           Contract.Assert(inv.Refined != null);

           Contract.Assert(inv.Formals != null);

-          

-          // replace formals with field dereferences                    

+

+          // replace formals with field dereferences

           Dictionary<string,Bpl.Expr> map = new Dictionary<string,Bpl.Expr>();

           Bpl.Expr absVar = new Bpl.IdentifierExpr(d.tok, absThis, predef.RefType);

-          for (int i = 0; i < inv.Refined.Count; i++) {     

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

             // TODO: boxing/unboxing?

             Bpl.Expr result = ExpressionTranslator.ReadHeap(inv.Toks[i], absHeap, absVar, new Bpl.IdentifierExpr(inv.Toks[i], GetField(cce.NonNull(inv.Refined[i]))));

             map.Add(inv.Formals[i].UniqueName, result);

           }

-                              

+

           Bpl.Expr e = new NominalSubstituter(map).VisitExpr(etran.TrExpr(inv.Expr));

           cond = Bpl.Expr.And(cond, e);

         }

-            

+

       return cond;

     }

-    

+

     #endregion

-    

+

     class BoilerplateTriple {  // a triple that is now a quintuple

       [ContractInvariantMethod]

       void ObjectInvariant() {

@@ -2764,7 +2764,7 @@ namespace Microsoft.Dafny {
         Comment = comment;

       }

     }

-    

+

     /// <summary>

     /// There are 3 states of interest when generating two-state boilerplate:

     ///  S0. the beginning of the method or loop, which is where the modifies clause is interpreted

@@ -2781,17 +2781,17 @@ namespace Microsoft.Dafny {
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<BoilerplateTriple>>()));

 

       List<BoilerplateTriple> boilerplate = new List<BoilerplateTriple>();

-      

+

       // the frame condition, which is free since it is checked with every heap update and call

       boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, etranPre, etran, etranMod), null, "frame condition"));

 

       // HeapSucc(S1, S2)

       Bpl.Expr heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);

       boilerplate.Add(new BoilerplateTriple(tok, true, heapSucc, null, "boilerplate"));

-      

+

       return boilerplate;

     }

-    

+

     /// <summary>

     /// There are 3 states of interest when generating a frame condition:

     ///  S0. the beginning of the method/loop, which is where the modifies clause is interpreted

@@ -2823,9 +2823,9 @@ namespace Microsoft.Dafny {
       Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);

       Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranMod.IsAlloced(tok, o));

       Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);

-      

+

       consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etranMod, null, null));

-      

+

       Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));

       return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));

     }

@@ -2857,15 +2857,15 @@ namespace Microsoft.Dafny {
 

       Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));

       return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));

-    }    

+    }

     // ----- Type ---------------------------------------------------------------------------------

-    

+

     Bpl.Type TrType(Type type)

      {

       Contract.Requires(type != null);

       Contract.Requires(predef != null);

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

-     

+

       while (true) {

         TypeProxy tp = type as TypeProxy;

         if (tp == null) {

@@ -2877,7 +2877,7 @@ namespace Microsoft.Dafny {
           type = tp.T;

         }

       }

-      

+

       if (type is BoolType) {

         return Bpl.Type.Bool;

       } else if (type is IntType) {

@@ -2897,7 +2897,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

     }

-    

+

     Bpl.TypeVariableSeq TrTypeParamDecls(List<TypeParameter/*!*/>/*!*/ tps)

     {

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

@@ -2908,7 +2908,7 @@ namespace Microsoft.Dafny {
     }

 

     // ----- Statement ----------------------------------------------------------------------------

-    

+

     Bpl.AssertCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage)

     {

       Contract.Requires(tok != null);

@@ -2978,10 +2978,10 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(currentMethod != null && predef != null);

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

-     

+

       return TrStmt2StmtList(new Bpl.StmtListBuilder(), block, locals, etran);

     }

-    

+

     Bpl.StmtList TrStmt2StmtList(Bpl.StmtListBuilder builder, Statement block, Bpl.VariableSeq locals, ExpressionTranslator etran)

      {

       Contract.Requires(builder != null);

@@ -2990,11 +2990,11 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(currentMethod != null && predef != null);

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

-      

+

       TrStmt(block, builder, locals, etran);

       return builder.Collect(block.Tok);  // TODO: would be nice to have an end-curly location for "block"

     }

-    

+

     void TrStmt(Statement stmt, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran)

     {

       Contract.Requires(stmt != null);

@@ -3035,7 +3035,7 @@ namespace Microsoft.Dafny {
             TrStmt_CheckWellformed(arg.E, builder, locals, etran, false);

           }

         }

-         

+

       } else if (stmt is BreakStmt) {

         AddComment(builder, stmt, "break statement");

         var s = (BreakStmt)stmt;

@@ -3254,7 +3254,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr qqq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), bbb);

           builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined"));  // totality check

         }

-        

+

         // Here comes:  assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);

         Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o, GetField((FieldSelectExpr)s.BodyAssign.Lhs)));

         Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);

@@ -3288,14 +3288,14 @@ namespace Microsoft.Dafny {
           qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);

           builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));

         }

-        

+

         builder.Add(CaptureState(stmt.Tok));

-        

+

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

         TrStmt_CheckWellformed(s.Source, builder, locals, etran, true);

         Bpl.Expr source = etran.TrExpr(s.Source);

-        

+

         var b = new Bpl.StmtListBuilder();

         b.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False));

         Bpl.StmtList els = b.Collect(stmt.Tok);

@@ -3450,7 +3450,7 @@ namespace Microsoft.Dafny {
       }

       // add a free invariant which says that the heap hasn't changed outside of the modifies clause.

       invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));

-      

+

       // include a free invariant that says that all completed iterations so far have only decreased the termination metric

       if (initDecr != null) {

         List<IToken> toks = new List<IToken>();

@@ -3607,7 +3607,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);

       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

-      

+

       Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver);

       Bpl.ExprSeq ins = new Bpl.ExprSeq();

       if (!method.IsStatic) {

@@ -3692,7 +3692,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     static Expression CreateIntLiteral(IToken tok, int n)

     {

       Contract.Requires(tok != null);

@@ -3706,13 +3706,13 @@ namespace Microsoft.Dafny {
         return CreateIntSub(tok, CreateIntLiteral(tok, 0), CreateIntLiteral(tok, -n));

       }

     }

-    

+

     static Expression CreateIntSub(IToken tok, Expression e0, Expression e1)

      {

       Contract.Requires(tok != null);

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      

+

 

       Contract.Requires(e0.Type is IntType && e1.Type is IntType);

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

@@ -3721,7 +3721,7 @@ namespace Microsoft.Dafny {
       s.Type = Type.Int;  // resolve here

       return s;

     }

-    

+

     static Expression CreateIntITE(IToken tok, Expression test, Expression e0, Expression e1)

      {

       Contract.Requires(tok != null);

@@ -3735,7 +3735,7 @@ namespace Microsoft.Dafny {
       ite.Type = Type.Int;  // resolve here

       return ite;

     }

-    

+

     public IEnumerable<Expression> Conjuncts(Expression expr)

      {

       Contract.Requires(expr != null);

@@ -3773,7 +3773,7 @@ namespace Microsoft.Dafny {
         // record value of each decreases expression at beginning of the loop iteration

         Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(e.tok, bf, etran.TrExpr(e));

         builder.Add(cmd);

-        

+

         c++;

       }

       return oldBfs;

@@ -3825,7 +3825,7 @@ namespace Microsoft.Dafny {
       }

       builder.Add(Assert(tok, decrExpr, inferredDecreases ? "cannot prove termination; try supplying a decreases clause" : "failure to decrease termination measure"));

     }

-    

+

     /// <summary>

     /// Returns the expression that says whether or not the decreases function has gone down (if !allowNoChange)

     /// or has gone down or stayed the same (if allowNoChange).

@@ -3846,7 +3846,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

 

       int N = types.Count;

-      

+

       // compute eq and less for each component of the lexicographic pair

       List<Bpl.Expr> Eq = new List<Bpl.Expr>(N);

       List<Bpl.Expr> Less = new List<Bpl.Expr>(N);

@@ -3913,7 +3913,7 @@ namespace Microsoft.Dafny {
         return false;  // don't consider any type parameters to be the same (since we have no comparison function for them anyway)

       }

     }

-    

+

     void ComputeLessEq(IToken/*!*/ tok, Type/*!*/ ty, Bpl.Expr/*!*/ e0, Bpl.Expr/*!*/ e1, out Bpl.Expr/*!*/ less, out Bpl.Expr/*!*/ atmost, out Bpl.Expr/*!*/ eq,

                        ExpressionTranslator/*!*/ etran, bool includeLowerBound)

      {

@@ -3926,7 +3926,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.ValueAtReturn(out less)!=null);

       Contract.Ensures(Contract.ValueAtReturn(out atmost)!=null);

       Contract.Ensures(Contract.ValueAtReturn(out eq)!=null);

-     

+

       if (ty is BoolType) {

         eq = Bpl.Expr.Iff(e0, e1);

         less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);

@@ -3955,7 +3955,7 @@ namespace Microsoft.Dafny {
         eq = Bpl.Expr.Eq(b0, b1);

         less = Bpl.Expr.Lt(b0, b1);

         atmost = Bpl.Expr.Le(b0, b1);

-        

+

       } else {

         // reference type

         Bpl.Expr b0 = Bpl.Expr.Neq(e0, predef.Null);

@@ -3965,14 +3965,14 @@ namespace Microsoft.Dafny {
         atmost = Bpl.Expr.Imp(b0, b1);

       }

     }

-    

+

     void AddComment(Bpl.StmtListBuilder builder, Statement stmt, string comment) {

       Contract.Requires(builder != null);

       Contract.Requires(stmt != null);

       Contract.Requires(comment != null);

       builder.Add(new Bpl.CommentCmd(string.Format("----- {0} ----- {1}({2},{3})", comment, stmt.Tok.filename, stmt.Tok.line, stmt.Tok.col)));

-    }    

-    

+    }

+

     Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran)

     {

       Contract.Requires(tok != null);

@@ -4001,7 +4001,7 @@ namespace Microsoft.Dafny {
 

       } else  if (type is BoolType || type is IntType) {

         // nothing todo

-      

+

       } else if (type is SetType) {

         SetType st = (SetType)type;

         // (forall t: BoxType :: { x[t] } x[t] ==> Unbox(t)-has-the-expected-type)

@@ -4016,7 +4016,7 @@ namespace Microsoft.Dafny {
           Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));

           return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));

         }

-        

+

       } else if (type is SeqType) {

         SeqType st = (SeqType)type;

         // (forall i: int :: { Seq#Index(x,i) }

@@ -4053,7 +4053,7 @@ namespace Microsoft.Dafny {
 

       } else if (type.IsTypeParameter) {

         return FunctionCall(tok, BuiltinFunction.GenericAlloc, null, x, etran.HeapExpr);

-        

+

       } else {

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

       }

@@ -4244,7 +4244,7 @@ namespace Microsoft.Dafny {
 

           var obj = SaveInTemp(etran.TrExpr(mse.Array), rhsCanAffectPreviouslyKnownExpressions,

             "$obj" + i, predef.RefType, builder, locals);

-          var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhsCanAffectPreviouslyKnownExpressions, 

+          var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhsCanAffectPreviouslyKnownExpressions,

             "$index" + i, predef.FieldName(mse.tok, predef.BoxType), builder, locals);

           prevObj[i] = obj;

           prevIndex[i] = fieldName;

@@ -4434,7 +4434,7 @@ namespace Microsoft.Dafny {
       readonly int layerOffset = 0;

       public int Statistics_FunctionCount = 0;

       [ContractInvariantMethod]

-      void ObjectInvariant() 

+      void ObjectInvariant()

       {

         Contract.Invariant(HeapExpr != null);

         Contract.Invariant(predef != null);

@@ -4453,7 +4453,7 @@ namespace Microsoft.Dafny {
         this.HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);

         this.This = "this";

       }

-      

+

       public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap) {

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

@@ -4463,7 +4463,7 @@ namespace Microsoft.Dafny {
         this.HeapExpr = heap;

         this.This = "this";

       }

-      

+

       public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar) {

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

@@ -4521,7 +4521,7 @@ namespace Microsoft.Dafny {
           return HeapExpr is Bpl.OldExpr;

         }

       }

-      

+

       public ExpressionTranslator LimitedFunctions(Function applyLimited_CurrentFunction) {

         Contract.Requires(applyLimited_CurrentFunction != null);

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

@@ -4596,10 +4596,10 @@ namespace Microsoft.Dafny {
           } else {

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

           }

-          

+

         } else if (expr is ThisExpr) {

           return new Bpl.IdentifierExpr(expr.tok, This, predef.RefType);

-        

+

         } else if (expr is IdentifierExpr) {

           IdentifierExpr e = (IdentifierExpr)expr;

           return TrVar(expr.tok, cce.NonNull(e.Var));

@@ -4607,7 +4607,7 @@ namespace Microsoft.Dafny {
         } else if (expr is BoogieWrapper) {

           var e = (BoogieWrapper)expr;

           return e.Expr;

-        

+

         } else if (expr is SetDisplayExpr) {

           SetDisplayExpr e = (SetDisplayExpr)expr;

           Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);

@@ -4616,7 +4616,7 @@ namespace Microsoft.Dafny {
             s = translator.FunctionCall(expr.tok, BuiltinFunction.SetUnionOne, predef.BoxType, s, ss);

           }

           return s;

-          

+

         } else if (expr is SeqDisplayExpr) {

           SeqDisplayExpr e = (SeqDisplayExpr)expr;

           Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);

@@ -4627,7 +4627,7 @@ namespace Microsoft.Dafny {
             i++;

           }

           return s;

-        

+

         } else if (expr is FieldSelectExpr) {

           FieldSelectExpr e = (FieldSelectExpr)expr;

           Contract.Assert(e.Field != null);

@@ -4639,7 +4639,7 @@ namespace Microsoft.Dafny {
             result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(translator.GetReadonlyField(e.Field)), new Bpl.ExprSeq(obj));

           }

           return CondApplyUnbox(expr.tok, result, e.Field.Type, cce.NonNull(expr.Type));

-          

+

         } else if (expr is SeqSelectExpr) {

           SeqSelectExpr e = (SeqSelectExpr)expr;

           Bpl.Expr seq = TrExpr(e.Seq);

@@ -4676,7 +4676,7 @@ namespace Microsoft.Dafny {
             }

             return seq;

           }

-        

+

         } else if (expr is SeqUpdateExpr) {

           SeqUpdateExpr e = (SeqUpdateExpr)expr;

           Bpl.Expr seq = TrExpr(e.Seq);

@@ -4714,7 +4714,7 @@ namespace Microsoft.Dafny {
           Bpl.ExprSeq args = FunctionInvocationArguments(e);

           Bpl.Expr result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(id), args);

           return CondApplyUnbox(expr.tok, result, e.Function.ResultType, expr.Type);

-        

+

         } else if (expr is DatatypeValue) {

           DatatypeValue dtv = (DatatypeValue)expr;

           Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved

@@ -4727,11 +4727,11 @@ namespace Microsoft.Dafny {
           }

           Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(dtv.tok, dtv.Ctor.FullName, predef.DatatypeType);

           return new Bpl.NAryExpr(dtv.tok, new Bpl.FunctionCall(id), args);

-            

+

         } else if (expr is OldExpr) {

           OldExpr e = (OldExpr)expr;

           return new Bpl.OldExpr(expr.tok, TrExpr(e.E));

-        

+

         } else if (expr is FreshExpr) {

           FreshExpr e = (FreshExpr)expr;

           Bpl.Expr oldHeap = new Bpl.OldExpr(expr.tok, HeapExpr);

@@ -4789,7 +4789,7 @@ namespace Microsoft.Dafny {
             default:

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

           }

-        

+

         } else if (expr is BinaryExpr) {

           BinaryExpr e = (BinaryExpr)expr;

           Bpl.Expr e0 = TrExpr(e.E0);

@@ -4810,12 +4810,12 @@ namespace Microsoft.Dafny {
               bOpcode = BinaryOperator.Opcode.And; break;

             case BinaryExpr.ResolvedOpcode.Or:

               bOpcode = BinaryOperator.Opcode.Or; break;

-              

+

             case BinaryExpr.ResolvedOpcode.EqCommon:

               bOpcode = BinaryOperator.Opcode.Eq; break;

             case BinaryExpr.ResolvedOpcode.NeqCommon:

               bOpcode = BinaryOperator.Opcode.Neq; break;

-              

+

             case BinaryExpr.ResolvedOpcode.Lt:

               bOpcode = BinaryOperator.Opcode.Lt; break;

             case BinaryExpr.ResolvedOpcode.Le:

@@ -4892,12 +4892,12 @@ namespace Microsoft.Dafny {
               return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.Gt,

                 translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e0),

                 translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e1));

-              

+

             default:

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

           }

           return Bpl.Expr.Binary(expr.tok, bOpcode, e0, e1);

-        

+

         } else if (expr is QuantifierExpr) {

           QuantifierExpr e = (QuantifierExpr)expr;

           Bpl.VariableSeq bvars = new Bpl.VariableSeq();

@@ -4916,7 +4916,7 @@ namespace Microsoft.Dafny {
             antecedent = Bpl.Expr.And(antecedent, TrExpr(e.Range));

           }

           Bpl.Expr body = TrExpr(e.Term);

-          

+

           if (e is ForallExpr) {

             return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.Imp(antecedent, body));

           } else {

@@ -4955,11 +4955,11 @@ namespace Microsoft.Dafny {
         } else if (expr is BoxingCastExpr) {

           BoxingCastExpr e = (BoxingCastExpr)expr;

           return CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType);

-          

+

         } else if (expr is UnboxingCastExpr) {

           UnboxingCastExpr e = (UnboxingCastExpr)expr;

           return CondApplyUnbox(e.tok, TrExpr(e.E), e.FromType, e.ToType);

-          

+

         } else {

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

         }

@@ -4968,7 +4968,7 @@ namespace Microsoft.Dafny {
       public Bpl.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, Bpl.VariableSeq bvars) {

         Contract.Requires(boundVars != null);

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

-        

+

         Bpl.Expr typeAntecedent = Bpl.Expr.True;

         foreach (BoundVar bv in boundVars) {

           Bpl.Variable bvar = new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, translator.TrType(bv.Type)));

@@ -5047,7 +5047,7 @@ namespace Microsoft.Dafny {
           return e;

         }

       }

-      

+

       public Bpl.Expr BoxIfNecessary(IToken tok, Bpl.Expr e, Type fromType) {

         Contract.Requires(tok != null);

         Contract.Requires(e != null);

@@ -5056,7 +5056,7 @@ namespace Microsoft.Dafny {
 

         return CondApplyBox(tok, e, fromType, null);

       }

-      

+

       public Bpl.Expr CondApplyUnbox(IToken tok, Bpl.Expr e, Type fromType, Type toType) {

         Contract.Requires(tok != null);

         Contract.Requires(e != null);

@@ -5070,7 +5070,7 @@ namespace Microsoft.Dafny {
           return e;

         }

       }

-      

+

       public static bool ModeledAsBoxType(Type t) {

         Contract.Requires(t != null);

         while (true) {

@@ -5173,7 +5173,7 @@ namespace Microsoft.Dafny {
         }

         return Bpl.Expr.SelectTok(tok, TrExpr(s), BoxIfNecessary(tok, elmt, elmtType));

       }

-      

+

       Bpl.QKeyValue TrAttributes(Attributes attrs) {

         Bpl.QKeyValue kv = null;

         while (attrs != null) {

@@ -5190,7 +5190,7 @@ namespace Microsoft.Dafny {
         }

         return kv;

       }

-      

+

       // --------------- help routines ---------------

 

       public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e) {

@@ -5200,7 +5200,7 @@ namespace Microsoft.Dafny {
 

         return IsAlloced(tok, e, HeapExpr);

       }

-          

+

       Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e, Bpl.Expr heap) {

         Contract.Requires(tok != null);

         Contract.Requires(e != null);

@@ -5209,7 +5209,7 @@ namespace Microsoft.Dafny {
 

         return ReadHeap(tok, heap, e, predef.Alloc(tok));

       }

-      

+

       public Bpl.Expr GoodRef(IToken tok, Bpl.Expr e, Type type) {

         Contract.Requires(tok != null);

         Contract.Requires(e != null);

@@ -5224,7 +5224,7 @@ namespace Microsoft.Dafny {
           return IsAlloced(tok, e);

         }

       }

-      

+

       public Bpl.Expr GoodRef_Class(IToken tok, Bpl.Expr e, UserDefinedType type, bool isNew)

        {

         Contract.Requires(tok != null);

@@ -5246,12 +5246,12 @@ namespace Microsoft.Dafny {
         if (isNew) {

           r = Bpl.Expr.Not(r);  // use the conjunct:  !Heap[e, alloc]

         }

-        

+

         // dtype(e) == C

         Bpl.Expr dtypeFunc = translator.FunctionCall(tok, BuiltinFunction.DynamicType, null, e);

         Bpl.Expr dtype = Bpl.Expr.Eq(dtypeFunc, type);

         r = r == null ? dtype : Bpl.Expr.And(r, dtype);

-        

+

         // TypeParams(e, #) == T

         int n = 0;

         foreach (Type arg in typeArgs) {

@@ -5262,7 +5262,7 @@ namespace Microsoft.Dafny {
           }

           n++;

         }

-        

+

         return r;

       }

 

@@ -5290,7 +5290,7 @@ namespace Microsoft.Dafny {
         return r;

       }

     }

-    

+

     enum BuiltinFunction {

       SetEmpty,

       SetUnionOne,

@@ -5301,7 +5301,7 @@ namespace Microsoft.Dafny {
       SetSubset,

       SetDisjoint,

       SetChoose,

-      

+

       SeqLength,

       SeqEmpty,

       SeqBuild,

@@ -5313,17 +5313,17 @@ namespace Microsoft.Dafny {
       SeqTake,

       SeqEqual,

       SeqSameUntil,

-      

+

       IndexField,

       MultiIndexField,

-      

+

       Box,

       Unbox,

       IsCanonicalBoolBox,

-      

+

       IsGoodHeap,

       HeapSucc,

-      

+

       DynamicType,  // allocated type (of object reference)

       DtType,       // type of datatype value

       TypeParams,   // type parameters of allocated type

@@ -5338,7 +5338,7 @@ namespace Microsoft.Dafny {
 

       GenericAlloc,

     }

-    

+

     // The "typeInstantiation" argument is passed in to help construct the result type of the function.

     Bpl.NAryExpr FunctionCall(IToken tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[] args)

     {

@@ -5433,7 +5433,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 3);

           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args);

-          

+

         case BuiltinFunction.IndexField:

           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);

@@ -5516,7 +5516,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected built-in function

       }

     }

-    

+

     Bpl.NAryExpr FunctionCall(IToken tok, string function, Bpl.Type returnType, params Bpl.Expr[] args)

     {

       Contract.Requires(tok != null);

@@ -5984,7 +5984,7 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < dt.TypeArgs.Count; i++) {

           subst.Add(dt.TypeArgs[i], instantiatedType.TypeArgs[i]);

         }

-        

+

         foreach (DatatypeCtor ctor in dt.Ctors) {

           Bpl.VariableSeq bvs;

           List<Bpl.Expr> args;

@@ -6037,7 +6037,7 @@ namespace Microsoft.Dafny {
             newExpr = new SeqDisplayExpr(expr.tok, newElements);

           }

         }

-        

+

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr fse = (FieldSelectExpr)expr;

         Expression substE = Substitute(fse.Obj, receiverReplacement, substMap);

@@ -6046,7 +6046,7 @@ namespace Microsoft.Dafny {
           fseNew.Field = fse.Field;  // resolve on the fly (and fseExpr.Type is set at end of method)

           newExpr = fseNew;

         }

-        

+

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr sse = (SeqSelectExpr)expr;

         Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);

@@ -6055,7 +6055,7 @@ namespace Microsoft.Dafny {
         if (seq != sse.Seq || e0 != sse.E0 || e1 != sse.E1) {

           newExpr = new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);

         }

-        

+

       } else if (expr is SeqUpdateExpr) {

         SeqUpdateExpr sse = (SeqUpdateExpr)expr;

         Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);

@@ -6082,7 +6082,7 @@ namespace Microsoft.Dafny {
           newFce.Function = e.Function;  // resolve on the fly (and set newFce.Type below, at end)

           newExpr = newFce;

         }

-      

+

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         List<Expression> newArgs = SubstituteExprList(dtv.Arguments, receiverReplacement, substMap);

@@ -6125,7 +6125,7 @@ namespace Microsoft.Dafny {
           newBin.ResolvedOp = e.ResolvedOp;  // part of what needs to be done to resolve on the fly (newBin.Type is set below, at end)

           newExpr = newBin;

         }

-        

+

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);

@@ -6148,7 +6148,7 @@ namespace Microsoft.Dafny {
         } else {

           Contract.Assume(false);  // unexpected ComprehensionExpr

         }

-        

+

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         Expression test = Substitute(e.Test, receiverReplacement, substMap);

@@ -6162,7 +6162,7 @@ namespace Microsoft.Dafny {
         var e = (ConcreteSyntaxExpression)expr;

         return Substitute(e.ResolvedExpression, receiverReplacement, substMap);

       }

-      

+

       if (newExpr == null) {

         return expr;

       } else {

@@ -6170,18 +6170,18 @@ namespace Microsoft.Dafny {
         return newExpr;

       }

     }

-    

+

     static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,

                                                  Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

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

       Contract.Requires((receiverReplacement == null) == (substMap == null));

       Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));

-      

+

       List<Expression> newElist = null;  // initialized lazily

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

       {cce.LoopInvariant(  newElist == null || newElist.Count == i);

-      

+

         Expression substE = Substitute(elist[i], receiverReplacement, substMap);

         if (substE != elist[i] && newElist == null) {

           newElist = new List<Expression>();

@@ -6199,7 +6199,7 @@ namespace Microsoft.Dafny {
         return newElist;

       }

     }

-    

+

     static Triggers SubstTriggers(Triggers trigs, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

       Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

       if (trigs != null) {

@@ -6231,7 +6231,7 @@ namespace Microsoft.Dafny {
         if (!anyArgSubst) {

           newArgs = attrs.Args;

         }

-        

+

         Attributes prev = SubstAttributes(attrs.Prev, receiverReplacement, substMap);

         if (newArgs != attrs.Args || prev != attrs.Prev) {

           return new Attributes(attrs.Name, newArgs, prev);

@@ -6239,6 +6239,6 @@ namespace Microsoft.Dafny {
       }

       return attrs;

     }

-        

+

   }

-}
\ No newline at end of file
+}

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