Merge

26 files changed, 1176 insertions, 1070 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 6fa9440a..6a448172 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -19,13 +19,13 @@ namespace Microsoft.Dafny {
     }

 

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(wr!=null);

     }

 

     TextWriter wr;

-    

+

     public int ErrorCount;

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

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

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

       ErrorCount++;

     }

-    

+

     void ReadRuntimeSystem() {

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

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

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

       }

     }

-    

+

     void CompileDatatypeStruct(DatatypeDecl dt, int indent) {

       Contract.Requires(dt != null);

 

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

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

       }

-      

+

       Indent(indent);

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

       int ind = indent + IndentAmount;

-      

+

       Indent(ind);

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

-      

+

       Indent(ind);

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

       Indent(ind + IndentAmount);

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

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

-      

+

       Indent(ind);

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

-      

+

       Indent(ind);

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

       Indent(ind + IndentAmount);

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

       wr.WriteLine("}");

     }

-    

+

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

     {

       Contract.Requires(sep != null);

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

       return i;  // the number of formals written

     }

-    

+

     string FormalName(Formal formal, int i) {

       Contract.Requires(formal != null);

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

 

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

     }

-    

+

     string DtCtorName(DatatypeCtor ctor) {

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

 

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

     }

-        

+

     void CompileClassMembers(ClassDecl c, int indent)

     {

       Contract.Requires(c != null);

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

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

           }

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           if (f.IsGhost) {

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

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

           }

-          

+

         } else if (member is Method) {

           Method m = (Method)member;

           if (!m.IsGhost) {

@@ -487,7 +487,7 @@ namespace Microsoft.Dafny {
     readonly string DafnySetClass = "Dafny.Set";

     readonly string DafnyMultiSetClass = "Dafny.MultiSet";

     readonly string DafnySeqClass = "Dafny.Sequence";

-    

+

     string TypeName(Type type)

     {

       Contract.Requires(type != null);

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

         }

       }

-      

+

       if (type is BoolType) {

         return "bool";

       } else if (type is IntType) {

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

       return s;

     }

-    

+

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

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

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

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

       return s;

     }

-    

+

     string DefaultValue(Type type)

     {

       Contract.Requires(type != null);

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

         }

       }

-      

+

       if (type is BoolType) {

         return "false";

       } else if (type is IntType) {

@@ -622,16 +622,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) {

@@ -732,19 +732,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);

@@ -755,7 +755,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");

@@ -825,20 +825,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);

         }

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

         }

         wr.WriteLine("))");

-        

+

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

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

 

@@ -860,7 +860,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;

@@ -1044,16 +1044,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) {

@@ -1083,7 +1083,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);

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

       }

     }

-        

+

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

 

     void TrParenExpr(string prefix, Expression expr) {

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

       wr.Write(")");

     }

-    

+

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

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

       wr.Write("(");

@@ -1188,10 +1188,10 @@ 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);

@@ -1213,7 +1213,7 @@ namespace Microsoft.Dafny {
         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;

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

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

         }

-        

+

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         Contract.Assert(e.Seq.Type != null);

@@ -1288,7 +1288,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);

@@ -1308,7 +1308,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

@@ -1327,13 +1327,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) {

@@ -1358,13 +1358,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;

@@ -1374,7 +1374,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) {

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

             break;

           }

-            

+

           case BinaryExpr.ResolvedOpcode.Lt:

             opString = "<";  break;

           case BinaryExpr.ResolvedOpcode.Le:

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

           wr.Write(")");

         }

-      

+

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

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

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 665cf33f..028d6826 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -3,39 +3,29 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

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

-

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

 // Dafny

 // Rustan Leino, first created 25 January 2008

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

-

 using System.Collections.Generic;

 using System.Numerics;

 using Microsoft.Boogie;

 using System.IO;

 using System.Text;

-

-

 COMPILER Dafny

-

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

-

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

 static BuiltIns theBuiltIns;

-

-

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

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

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

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

 static int anonymousIds = 0;

-

 struct MemberModifiers {

   public bool IsGhost;

   public bool IsStatic;

   public bool IsUnlimited;

 }

-

 // helper routine for parsing call statements

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

 {

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

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

 }

-

 ///<summary>

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

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

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

   }

 }

-

 ///<summary>

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

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

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

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

 }

-

 ///<summary>

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

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

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

   return parser.errors.count;

 }

-

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

 CHARACTERS

   letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".

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

   special = "'_?\\".

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

-

   cr        = '\r'.

   lf        = '\n'.

   tab       = '\t'.

-

   space = ' '.

   quote = '"'.

-

   nondigit = letter + special.

   idchar = nondigit + digit.

   nonquote = letter + digit + space + glyph.

-

   /* exclude the characters in 'array' */

   nondigitMinusA = nondigit - 'a'.

   idcharMinusA = idchar - 'a'.

   idcharMinusR = idchar - 'r'.

   idcharMinusY = idchar - 'y'.

   idcharMinusPosDigit = idchar - posDigit.

-

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

 TOKENS

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

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

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

   string = quote {nonquote} quote.

-

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

 COMMENTS FROM "//" TO lf

-

 IGNORE cr + lf + tab

-

-

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

 PRODUCTIONS

-

 Dafny

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

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

-

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

      ModuleDecl module;

-     

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

      DefaultModuleDecl defaultModule = null;

      foreach (ModuleDecl mdecl in theModules) {

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

   EOF

   .

-

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

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

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

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

   { ClassMemberDecl<members, true>

   }

-  "}"                                      

-  (. if (optionalId == null)        

+  "}"

+  (. if (optionalId == null)

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

-     else 

+     else

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

      c.BodyStartTok = bodyStart;

      c.BodyEndTok = t;

   .)

   .

-

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

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

      Method/*!*/ m;

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

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

   }

-  ( FieldDecl<mmod, mm>  

+  ( FieldDecl<mmod, mm>

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

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

-  | CouplingInvDecl<mmod, mm> 

+  | CouplingInvDecl<mmod, mm>

   )

   .

-

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

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

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

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

   .)

   .

-

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

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

      Attributes attrs = null;

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

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

   .

-

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

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

      Attributes attrs = null;

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

   ";"

   .

-

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

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

      Attributes attrs = null;

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

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

   .)

-  { Attribute<ref attrs> }  

+  { Attribute<ref attrs> }

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

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

   }

-  "by"    

+  "by"

   Expression<out e>

   ";"

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

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

   .

-

-

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

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

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

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

   IdentType<out id, out ty>

   .

-

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

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

   Ident<out id>

   ":"

   Type<out ty>

   .

-

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

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

   .)

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

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

   .

-

 IdentTypeOptional<out BoundVar/*!*/ var>

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

   .)

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

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

   .

-

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

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

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

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

   .)

   .

-

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

-

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

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

      IToken/*!*/ id; .)

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

   ">"

   .

-

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

-

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

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

      IToken/*!*/ id;

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

     Formals<false, !mmod.IsGhost, outs>

   ]

-

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

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

   ]

-  

   (. if (isRefinement)

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

      else if (isConstructor)

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

  .)

   .

-

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

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

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

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

   )

   .

-

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

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

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

   "("

   [

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

   ")"

   .

-

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

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

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

   "("

   [

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

   ")"

   .

-

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

-

 Type<out Type/*!*/ ty>

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

   TypeAndToken<out tok, out ty>

   .

-

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

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

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

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

                                        ty = new MultiSetType(gt[0]);

                                     .)

-    

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

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

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

@@ -539,7 +488,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*/

@@ -560,7 +508,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; .)

   "<"

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

   ">"

   .

-

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

-

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

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

      Attributes attrs = null;

@@ -594,7 +539,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>

   ":"

@@ -607,7 +552,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; .)

@@ -620,7 +564,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; .)

@@ -631,7 +574,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

@@ -644,7 +586,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>

@@ -652,16 +593,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/*!*/>();

@@ -672,13 +610,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 */

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

   )

   .

-

 ReturnStmt<out Statement/*!*/ s>

 = (.

    IToken returnTok = null;

@@ -744,7 +679,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;

@@ -772,17 +706,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;

@@ -816,7 +746,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;

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

   )

   .

-

 AlternativeBlock<.out List<GuardedAlternative> alternatives.>

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

      IToken x;

@@ -859,7 +787,6 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives.>
   }

   "}"

   .

-

 WhileStmt<out Statement/*!*/ stmt>

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

      Expression guard;

@@ -883,7 +810,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/*!*/>();

@@ -904,7 +830,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) {

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

   }

   .

-

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

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

   "("

@@ -930,7 +854,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;

@@ -943,7 +866,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;

@@ -961,9 +883,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;

@@ -994,19 +914,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/*!*/>();

@@ -1017,13 +934,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; .)

@@ -1032,9 +947,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; .)

@@ -1043,9 +956,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; .)

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

   ]

   .

-

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

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

-

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

 RelationalExpression<out Expression/*!*/ e>

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

@@ -1149,7 +1058,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; .)

@@ -1166,7 +1074,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; .)

@@ -1175,14 +1082,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; .)

@@ -1191,7 +1096,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; .)

@@ -1199,7 +1103,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; .)

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

   )

   .

-

 Lhs<out Expression e>

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

   .)

@@ -1227,9 +1129,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.)

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

   )

   .

-

 DisplayExpr<out Expression e>

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

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

@@ -1287,7 +1186,6 @@ MultiSetExpr<out Expression e>
   | (. SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); .)

   )

   .

-

 EndlessExpression<out Expression e>

 = (. IToken/*!*/ x;

      Expression e0, e1;

@@ -1302,7 +1200,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/*!*/>();

@@ -1316,7 +1213,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/*!*/>();

@@ -1332,9 +1228,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;

@@ -1350,7 +1244,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;

@@ -1363,7 +1256,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; .)

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

   )

   .

-

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

-

 QuantifierGuts<out Expression/*!*/ q>

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

      bool univ = false;

@@ -1441,11 +1331,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;

@@ -1468,22 +1356,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/*!*/>();

@@ -1495,14 +1379,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/*!*/>();

   .)

@@ -1513,21 +1395,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

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

        n = BigInteger.Zero;

      }

-  .) 

+  .)

   .

-

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

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 871a8b34..218f95e5 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -413,13 +413,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]

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

   /// <summary>

   /// This proxy stands for any datatype.

-  /// </summary>  

+  /// </summary>

   public class DatatypeProxy : RestrictedTypeProxy {

     public override int OrderID {

       get {

@@ -456,7 +456,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 {

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

   ///     int or set or multiset

   /// if !AllowSeq.

-  /// </summary>  

+  /// </summary>

   public class OperationTypeProxy : RestrictedTypeProxy {

     public readonly bool AllowSeq;

     public OperationTypeProxy(bool allowSeq) {

@@ -688,7 +688,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);

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

     }

   }

-  

+

   public class DatatypeDecl : TopLevelDecl {

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

     [ContractInvariantMethod]

@@ -1698,7 +1698,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));

@@ -2564,7 +2564,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)

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

       get {

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

-        yield return Term; 

+        yield return Term;

       }

     }

   }

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

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

         }

-        if (Bpl.CommandLineOptions.Clo.Trace) 

+        if (Bpl.CommandLineOptions.Clo.Trace)

         {

           Console.WriteLine("Parsing " + dafnyFileName);

         }

 

         int errorCount;

-        try 

+        try

         {

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

-          if (errorCount != 0) 

+          if (errorCount != 0)

           {

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

           }

-        } 

-        catch (IOException e) 

+        }

+        catch (IOException e)

         {

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

         }

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

         }

       }

-      

+

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

 

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

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

     }

   }

-}
\ No newline at end of file
+}

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

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

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

   <PropertyGroup>

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

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

   </ItemGroup>

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

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

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

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

   <Target Name="BeforeBuild">

   </Target>

   <Target Name="AfterBuild">

   </Target>

   -->

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

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 15a3f65d..63b5f926 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -14,7 +14,7 @@ namespace Microsoft.Dafny {
   class Printer {

     TextWriter wr;

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(wr!=null);

     }

@@ -23,7 +23,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(wr != null);

       this.wr = wr;

     }

-    

+

     public void PrintProgram(Program prog) {

       Contract.Requires(prog != null);

       if (Bpl.CommandLineOptions.Clo.ShowEnv != Bpl.CommandLineOptions.ShowEnvironment.Never) {

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

       }

     }

-    

+

     public void PrintTopLevelDecls(List<TopLevelDecl> classes, int indent) {

       Contract.Requires(classes!= null);

       int i = 0;

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

       }

     }

-    

+

     public void PrintClass(ClassDecl c, int indent) {

       Contract.Requires(c != null);

       Indent(indent);

@@ -97,12 +97,12 @@ namespace Microsoft.Dafny {
         wr.WriteLine("}");

       }

     }

-    

+

     public void PrintClass_Members(ClassDecl c, int indent)

     {

       Contract.Requires(c != null);

       Contract.Requires( c.Members.Count != 0);

-    

+

       int state = 0;  // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field

       foreach (MemberDecl m in c.Members) {

         if (m is Method) {

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

       }

     }

-    

+

     void PrintClassMethodHelper(string kind, Attributes attrs, string name, List<TypeParameter> typeArgs) {

       Contract.Requires(kind != null);

       Contract.Requires(name != null);

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

       }

     }

-    

+

     public void PrintDatatype(DatatypeDecl dt, int indent) {

       Contract.Requires(dt != null);

       Indent(indent);

@@ -164,17 +164,17 @@ namespace Microsoft.Dafny {
       }

       wr.WriteLine(";");

     }

-    

+

     public void PrintAttributes(Attributes a) {

       if (a != null) {

         PrintAttributes(a.Prev);

-        

+

         wr.Write("{{:{0}", a.Name);

         PrintAttributeArgs(a.Args);

         wr.Write("} ");

       }

     }

-    

+

     public void PrintAttributeArgs(List<Attributes.Argument> args) {

       Contract.Requires(args != null);

       string prefix = " ";

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

       }

     }

-    

+

     public void PrintField(Field field, int indent) {

       Contract.Requires(field != null);

       Indent(indent);

@@ -203,7 +203,7 @@ namespace Microsoft.Dafny {
       PrintType(field.Type);

       wr.WriteLine(";");

     }

-    

+

     public void PrintCouplingInvariant(CouplingInvariant inv, int indent) {

       Contract.Requires(inv != null);

       Indent(indent);

@@ -218,7 +218,7 @@ namespace Microsoft.Dafny {
       PrintExpression(inv.Expr);

       wr.WriteLine(";");

     }

-    

+

     public void PrintFunction(Function f, int indent) {

       Contract.Requires(f != null);

       Indent(indent);

@@ -245,20 +245,20 @@ namespace Microsoft.Dafny {
         wr.WriteLine("}");

       }

     }

-    

+

     // ----------------------------- PrintMethod -----------------------------

 

     const int IndentAmount = 2;

     const string BunchaSpaces = "                                ";

     void Indent(int amount)

     {  Contract.Requires( 0 <= amount);

-    

+

       while (0 < amount) {

         wr.Write(BunchaSpaces.Substring(0, amount));

         amount -= BunchaSpaces.Length;

       }

     }

-    

+

     public void PrintMethod(Method method, int indent) {

       Contract.Requires(method != null);

       Indent(indent);

@@ -284,14 +284,14 @@ namespace Microsoft.Dafny {
       PrintFrameSpecLine("modifies", method.Mod, ind);

       PrintSpec("ensures", method.Ens, ind);

       PrintSpecLine("decreases", method.Decreases, ind);

-      

+

       if (method.Body != null) {

         Indent(indent);

         PrintStatement(method.Body, indent);

         wr.WriteLine();

       }

     }

-    

+

     void PrintFormals(List<Formal> ff) {

       Contract.Requires(ff!=null);

       wr.Write("(");

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

       wr.Write(")");

     }

-    

+

     void PrintFormal(Formal f) {

       Contract.Requires(f != null);

       if (f.IsGhost) {

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

       PrintType(f.Type);

     }

-    

+

     void PrintSpec(string kind, List<Expression> ee, int indent) {

       Contract.Requires(kind != null);

       Contract.Requires(ee != null);

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

 

     // ----------------------------- PrintType -----------------------------

-    

+

     public void PrintType(Type ty) {

       Contract.Requires(ty != null);

       wr.Write(ty.ToString());

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

 

     // ----------------------------- PrintStatement -----------------------------

-    

+

     /// <summary>

     /// Prints from the current position of the current line.

     /// If the statement requires several lines, subsequent lines are indented at "indent".

@@ -393,23 +393,23 @@ namespace Microsoft.Dafny {
           Indent(indent);

         }

       }

-        

+

       if (stmt is AssertStmt) {

         wr.Write("assert ");

         PrintExpression(((AssertStmt)stmt).Expr);

         wr.Write(";");

-        

+

       } else if (stmt is AssumeStmt) {

         wr.Write("assume ");

         PrintExpression(((AssumeStmt)stmt).Expr);

         wr.Write(";");

-        

+

       } else if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

         wr.Write("print");

         PrintAttributeArgs(s.Args);

         wr.Write(";");

-        

+

       } else if (stmt is BreakStmt) {

         BreakStmt s = (BreakStmt)stmt;

         if (s.TargetLabel != null) {

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

           wr.Write(";");

         }

-        

+

       } else if (stmt is ReturnStmt) {

         var s = (ReturnStmt) stmt;

         wr.Write("return");

@@ -435,14 +435,14 @@ namespace Microsoft.Dafny {
           }

         }

           wr.Write(";");

-        

+

       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

         PrintExpression(s.Lhs);

         wr.Write(" := ");

         PrintRhs(s.Rhs);

         wr.Write(";");

-        

+

       } else if (stmt is VarDecl) {

         VarDecl s = (VarDecl)stmt;

         if (s.IsGhost) {

@@ -451,7 +451,7 @@ namespace Microsoft.Dafny {
         wr.Write("var {0}", s.Name);

         PrintType(": ", s.OptionalType);

         wr.Write(";");

-      

+

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

         wr.Write("call ");

@@ -471,7 +471,7 @@ namespace Microsoft.Dafny {
         wr.Write("{0}(", s.MethodName);

         PrintExpressionList(s.Args);

         wr.Write(");");

-        

+

       } else if (stmt is BlockStmt) {

         wr.WriteLine("{");

         int ind = indent + IndentAmount;

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

         Indent(indent);

         wr.Write("}");

-        

+

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

         while (true) {

@@ -508,7 +508,7 @@ namespace Microsoft.Dafny {
         PrintAlternatives(indent, s.Alternatives);

         Indent(indent);

         wr.Write("}");

-      

+

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

         wr.Write("while (");

@@ -556,7 +556,7 @@ namespace Microsoft.Dafny {
         wr.WriteLine();

         Indent(indent);

         wr.Write("}");

-        

+

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         wr.Write("match ");

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

       }

     }

-    

+

     void PrintRhs(AssignmentRhs rhs) {

       Contract.Requires(rhs != null);

       if (rhs is ExprRhs) {

@@ -673,7 +673,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS

       }

     }

-    

+

     void PrintGuard(Expression guard) {

       if (guard == null) {

         wr.Write("*");

@@ -681,7 +681,7 @@ namespace Microsoft.Dafny {
         PrintExpression(guard);

       }

     }

-    

+

     // ----------------------------- PrintExpression -----------------------------

 

     public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen) {

@@ -739,12 +739,12 @@ namespace Microsoft.Dafny {
         wr.WriteLine(endWithCloseParen ? ")" : "");

       }

     }

-    

+

     public void PrintExpression(Expression expr) {

       Contract.Requires(expr != null);

       PrintExpr(expr, 0, false, true, -1);

     }

-    

+

     /// <summary>

     /// An indent of -1 means print the entire expression on one line.

     /// </summary>

@@ -752,7 +752,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);

       PrintExpr(expr, 0, false, true, indent);

     }

-    

+

     /// <summary>

     /// An indent of -1 means print the entire expression on one line.

     /// </summary>

@@ -770,13 +770,13 @@ namespace Microsoft.Dafny {
         } else {

           wr.Write((BigInteger)e.Value);

         }

-      

+

       } else if (expr is ThisExpr) {

         wr.Write("this");

-  

+

       } else if (expr is IdentifierExpr) {

         wr.Write(((IdentifierExpr)expr).Name);

-      

+

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName);

@@ -785,14 +785,14 @@ namespace Microsoft.Dafny {
           PrintExpressionList(dtv.Arguments);

           wr.Write(")");

         }

-        

+

       } else if (expr is DisplayExpression) {

         DisplayExpression e = (DisplayExpression)expr;

         if (e is MultiSetDisplayExpr) wr.Write("multiset");

         wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "{" : "[");

         PrintExpressionList(e.Elements);

         wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "}" : "]");

-        

+

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr e = (FieldSelectExpr)expr;

         // determine if parens are needed

@@ -800,7 +800,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);

@@ -815,7 +815,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("[");

@@ -859,7 +859,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("[");

@@ -868,7 +868,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

@@ -876,7 +876,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);

@@ -935,14 +935,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;

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

       } else if (expr is WildcardExpr) {

         wr.Write("*");

-        

+

       } else if (expr is ITEExpr) {

         ITEExpr ite = (ITEExpr)expr;

         bool parensNeeded = !isRightmost;

@@ -1082,7 +1082,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

@@ -1100,24 +1100,24 @@ namespace Microsoft.Dafny {
           PrintExpressionList(e.Arguments);

           wr.Write(")");

         }

-        

+

       } else if (expr is MatchExpr) {

         Contract.Assert(false); throw new cce.UnreachableException();  // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr

       } else {

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

       }

     }

-    

+

     void PrintTriggers(Triggers trigs) {

       if (trigs != null) {

         PrintTriggers(trigs.Prev);

-        

+

         wr.Write("{ ");

         PrintExpressionList(trigs.Terms);

         wr.Write(" } ");

       }

     }

-    

+

     void PrintExpressionList(List<Expression> exprs) {

       Contract.Requires(exprs != null);

       string sep = "";

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 1321a987..098dbad2 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -67,7 +67,7 @@ namespace Microsoft.Dafny {
     }

 

     bool checkRefinements = true; // used to indicate a cycle in refinements

-      

+

     public void ResolveProgram(Program prog) {

       Contract.Requires(prog != null);

       // register modules

@@ -119,15 +119,15 @@ namespace Microsoft.Dafny {
         }

       }

 

-      // resolve top-level declarations of refinements      

-      foreach (ModuleDecl m in prog.Modules) 

-        foreach (TopLevelDecl decl in m.TopLevelDecls) 

+      // resolve top-level declarations of refinements

+      foreach (ModuleDecl m in prog.Modules)

+        foreach (TopLevelDecl decl in m.TopLevelDecls)

           if (decl is ClassRefinementDecl) {

             ClassRefinementDecl rdecl = (ClassRefinementDecl) decl;

             ResolveTopLevelRefinement(rdecl);

             if (rdecl.Refined != null) refines.AddEdge(rdecl, rdecl.Refined);

           }

-      

+

       // attempt finding refinement cycles

       List<TopLevelDecl> refinesCycle = refines.TryFindCycle();

       if (refinesCycle != null) {

@@ -139,8 +139,8 @@ namespace Microsoft.Dafny {
         }

         Error(refinesCycle[0], "Detected a cyclic refinement declaration: {0}", cy);

         checkRefinements = false;

-      } 

-      

+      }

+

       // resolve top-level declarations

       Graph<DatatypeDecl> datatypeDependencies = new Graph<DatatypeDecl>();

       foreach (ModuleDecl m in prog.Modules) {

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

       }

     }

-    

+

     public void RegisterTopLevelDecls(List<TopLevelDecl> declarations) {

       Contract.Requires(declarations != null);

       foreach (TopLevelDecl d in declarations) {

@@ -209,7 +209,7 @@ namespace Microsoft.Dafny {
           // ... and of the other members

           Dictionary<string, MemberDecl> members = new Dictionary<string, MemberDecl>();

           datatypeMembers.Add(dt, members);

-        

+

           foreach (DatatypeCtor ctor in dt.Ctors) {

             if (ctor.Name.EndsWith("?")) {

               Error(ctor, "a datatype constructor name is not allowed to end with '?'");

@@ -224,7 +224,7 @@ namespace Microsoft.Dafny {
               query.EnclosingClass = dt;  // resolve here

               members.Add(queryName, query);

               ctor.QueryField = query;

-                

+

               // also register the constructor name globally

               Tuple<DatatypeCtor, bool> pair;

               if (allDatatypeCtors.TryGetValue(ctor.Name, out pair)) {

@@ -268,9 +268,9 @@ namespace Microsoft.Dafny {
         }

         decl.Refined = cce.NonNull((ClassDecl) a);

         // TODO: copy over remaining members of a

-      }        

-    }  

-      

+      }

+    }

+

     public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {

       Contract.Requires(declarations != null);

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

@@ -286,7 +286,7 @@ namespace Microsoft.Dafny {
         allTypeParameters.PopMarker();

       }

     }

-    

+

     public void ResolveTopLevelDecls_Meat(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {

       Contract.Requires(declarations != null);

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

@@ -306,7 +306,7 @@ namespace Microsoft.Dafny {
         allTypeParameters.PopMarker();

       }

     }

-    

+

     ClassDecl currentClass;

     Function currentFunction;

     readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();

@@ -314,7 +314,7 @@ namespace Microsoft.Dafny {
     readonly Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();

     readonly List<Statement> loopStack = new List<Statement>();  // the enclosing loops (from which it is possible to break out)

     readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>();  // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -323,13 +323,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(cl != null);

       Contract.Requires(currentClass == null);

       Contract.Ensures(currentClass == null);

-    

+

       currentClass = cl;

       foreach (MemberDecl member in cl.Members) {

         member.EnclosingClass = cl;

         if (member is Field) {

           ResolveType(member.tok, ((Field)member).Type);

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           allTypeParameters.PushMarker();

@@ -343,15 +343,15 @@ namespace Microsoft.Dafny {
           ResolveTypeParameters(m.TypeArgs, true, m);

           ResolveMethodSignature(m);

           allTypeParameters.PopMarker();

-          

+

         } else if (member is CouplingInvariant) {

           CouplingInvariant inv = (CouplingInvariant)member;

-          if (currentClass is ClassRefinementDecl) {      

+          if (currentClass is ClassRefinementDecl) {

             ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

             if (refined != null) {

               Contract.Assert(classMembers.ContainsKey(refined));

               Dictionary<string,MemberDecl> members = classMembers[refined];

-            

+

               // resolve abstracted fields in the refined class

               List<Field> fields = new List<Field>();

               foreach (IToken tok in inv.Toks) {

@@ -359,29 +359,29 @@ namespace Microsoft.Dafny {
                   Error(tok, "Refined class does not declare a field: {0}", tok.val);

                 else {

                   MemberDecl field = members[tok.val];

-                  if (!(field is Field)) 

+                  if (!(field is Field))

                     Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);

                   else if (fields.Contains(cce.NonNull((Field)field)))

                     Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);

                   else

                     fields.Add(cce.NonNull((Field)field));

-                }                  

-              }            

+                }

+              }

               inv.Refined = fields;

             }

-            

+

           } else {

             Error(member, "Coupling invariants can only be declared in refinement classes");

           }

         } else {

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

         }

-        

-        if (currentClass is ClassRefinementDecl) {          

+

+        if (currentClass is ClassRefinementDecl) {

           ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

           if (refined != null) {

             Contract.Assert(classMembers.ContainsKey(refined));

-          

+

             // there is a member with the same name in refined class if and only if the member is a refined method

             if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))

               Error(member, "Refined class has a member with the same name as in the refinement class: {0}", member.Name);

@@ -399,14 +399,14 @@ namespace Microsoft.Dafny {
       Contract.Requires(cl != null);

       Contract.Requires(currentClass == null);

       Contract.Ensures(currentClass == null);

-    

+

       ResolveAttributes(cl.Attributes, false);

       currentClass = cl;

       foreach (MemberDecl member in cl.Members) {

         ResolveAttributes(member.Attributes, false);

         if (member is Field) {

           // nothing more to do

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           allTypeParameters.PushMarker();

@@ -420,13 +420,13 @@ namespace Microsoft.Dafny {
           ResolveTypeParameters(m.TypeArgs, false, m);

           ResolveMethod(m);

           allTypeParameters.PopMarker();

-          

+

           // check if signature of the refined method matches the refinement method

           if (member is MethodRefinement) {

             MethodRefinement mf = (MethodRefinement)member;

             if (currentClass is ClassRefinementDecl) {

               // should have already been resolved

-              if (((ClassRefinementDecl)currentClass).Refined != null) { 

+              if (((ClassRefinementDecl)currentClass).Refined != null) {

                 MemberDecl d = classMembers[((ClassRefinementDecl)currentClass).Refined][mf.Name];

                 if (d is Method) {

                   mf.Refined = (Method)d;

@@ -434,18 +434,18 @@ namespace Microsoft.Dafny {
                     Error(mf, "Different number of input variables");

                   if (mf.Outs.Count != mf.Refined.Outs.Count)

                     Error(mf, "Different number of output variables");

-                  if (mf.IsStatic || mf.Refined.IsStatic) 

+                  if (mf.IsStatic || mf.Refined.IsStatic)

                     Error(mf, "Refined methods cannot be static");

                 } else {

                   Error(member, "Refined class has a non-method member with the same name: {0}", member.Name);

-                }            

+                }

               }

             } else {

               Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);

             }

           }

-        

-        } else if (member is CouplingInvariant) {        

+

+        } else if (member is CouplingInvariant) {

           CouplingInvariant inv = (CouplingInvariant)member;

           if (inv.Refined != null) {

             inv.Formals = new List<Formal>();

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

             ResolveExpression(inv.Expr, false);

             scope.PopMarker();

-          }                

+          }

         } else {

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

         }

@@ -476,13 +476,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(dt != null);

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

       foreach (DatatypeCtor ctor in dt.Ctors) {

-        

+

         ctor.EnclosingDatatype = dt;

 

         allTypeParameters.PushMarker();

         ResolveCtorSignature(ctor);

         allTypeParameters.PopMarker();

-        

+

         foreach (Formal p in ctor.Formals) {

           DatatypeDecl dependee = p.Type.AsDatatype;

           if (dependee != null) {

@@ -497,7 +497,7 @@ namespace Microsoft.Dafny {
     /// datatype has some value that can be constructed from datatypes in lower stratospheres only.

     /// The algorithm used here is quadratic in the number of datatypes in the SCC.  Since that number is

     /// deemed to be rather small, this seems okay.

-    /// </summary>    

+    /// </summary>

     void SccStratosphereCheck(DatatypeDecl startingPoint, Graph<DatatypeDecl/*!*/>/*!*/ dependencies)

     {

       Contract.Requires(startingPoint != null);

@@ -573,7 +573,7 @@ namespace Microsoft.Dafny {
         ResolveAttributeArgs(attrs.Args, twoState);

       }

     }

-        

+

     void ResolveAttributeArgs(List<Attributes.Argument/*!*/>/*!*/ args, bool twoState) {

       Contract.Requires(args != null);

       foreach (Attributes.Argument aa in args) {

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

       }

     }

-        

+

     void ResolveTriggers(Triggers trigs, bool twoState) {

       // order does not matter for resolution, so resolve them in reverse order

       for (; trigs != null; trigs = trigs.Prev) {

@@ -592,9 +592,9 @@ namespace Microsoft.Dafny {
         }

       }

     }

-        

+

     void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) {

-      

+

       Contract.Requires(tparams != null);

       Contract.Requires(parent != null);

       // push type arguments of the refined class

@@ -603,7 +603,7 @@ namespace Microsoft.Dafny {
         if (refined != null)

           ResolveTypeParameters(refined.TypeArgs, false, refined);

       }

-    

+

       // push non-duplicated type parameter names

       foreach (TypeParameter tp in tparams) {

         Contract.Assert(tp != null);

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

       }

     }

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -683,7 +683,7 @@ namespace Microsoft.Dafny {
       currentFunction = null;

       scope.PopMarker();

     }

-    

+

     void ResolveFrameExpression(FrameExpression fe, string kind) {

       Contract.Requires(fe != null);

       Contract.Requires(kind != null);

@@ -717,7 +717,7 @@ namespace Microsoft.Dafny {
         Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type);

       }

     }

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

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

       scope.PopMarker();

     }

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -754,7 +754,7 @@ namespace Microsoft.Dafny {
       foreach (Formal p in m.Ins) {

         scope.Push(p.Name, p);

       }

-      

+

       // Start resolving specification...

       foreach (MaybeFreeExpression e in m.Req) {

         ResolveExpression(e.E, false);

@@ -770,7 +770,7 @@ namespace Microsoft.Dafny {
         ResolveExpression(e, false);

         // any type is fine

       }

-      

+

       // Add out-parameters to a new scope that will also include the outermost-level locals of the body

       // Don't care about any duplication errors among the out-parameters, since they have already been reported

       scope.PushMarker();

@@ -786,16 +786,16 @@ namespace Microsoft.Dafny {
           Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);

         }

       }

-      

+

       // Resolve body

       if (m.Body != null) {

         ResolveBlockStatement(m.Body, m.IsGhost, m);

       }

-      

+

       scope.PopMarker();  // for the out-parameters and outermost-level locals

       scope.PopMarker();  // for the in-parameters

     }

-    

+

     void ResolveCtorSignature(DatatypeCtor ctor) {

       Contract.Requires(ctor != null);

       foreach (Formal p in ctor.Formals) {

@@ -839,18 +839,18 @@ namespace Microsoft.Dafny {
             Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);

           }

         }

-      

+

       } else if (type is TypeProxy) {

         TypeProxy t = (TypeProxy)type;

         if (t.T != null) {

           ResolveType(tok, t.T);

         }

-        

+

       } else {

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

       }

     }

-    

+

     public bool UnifyTypes(Type a, Type b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -866,7 +866,7 @@ namespace Microsoft.Dafny {
           a = proxy.T;

         }

       }

-      

+

       while (b is TypeProxy) {

         TypeProxy proxy = (TypeProxy)b;

         if (proxy.T == null) {

@@ -876,7 +876,7 @@ namespace Microsoft.Dafny {
           b = proxy.T;

         }

       }

-      

+

 #if !NO_CHEAP_OBJECT_WORKAROUND

       if (a is ObjectType || b is ObjectType) {  // TODO: remove this temporary hack

         var other = a is ObjectType ? b : a;

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

 #endif

       // Now, a and b are non-proxies and stand for the same things as the original a and b, respectively.

-      

+

       if (a is BoolType) {

         return b is BoolType;

       } else if (a is IntType) {

@@ -925,12 +925,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);

@@ -941,15 +941,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.

@@ -960,7 +960,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) {

@@ -968,14 +968,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

@@ -983,7 +983,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) {

@@ -993,7 +993,7 @@ namespace Microsoft.Dafny {
         } else {

           return false;

         }

-      

+

       } else if (proxy is OperationTypeProxy) {

         OperationTypeProxy opProxy = (OperationTypeProxy)proxy;

         if (t is IntType || t is SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) {

@@ -1016,11 +1016,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;

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

       return true;

     }

-    

+

     bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b)

     { Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -1038,7 +1038,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

@@ -1064,7 +1064,7 @@ namespace Microsoft.Dafny {
         } else {

           return false;

         }

-        

+

       } else if (a is ObjectsTypeProxy) {

         if (b is ObjectsTypeProxy) {

           // fine

@@ -1095,7 +1095,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;

@@ -1119,7 +1119,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) {

@@ -1140,12 +1140,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

       }

@@ -1166,14 +1166,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) {

@@ -1323,7 +1323,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) {

@@ -1378,16 +1378,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;

@@ -1481,20 +1481,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);

         }

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

 

         scope.PopMarker();

-      

+

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         bool bodyIsSpecOnly = specContextOnly;

@@ -1554,14 +1554,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;

@@ -1616,8 +1616,8 @@ namespace Microsoft.Dafny {
           }

           Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);

         }

-        

-        

+

+

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();

       }

@@ -2186,7 +2186,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) {

@@ -2197,7 +2197,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

@@ -2230,13 +2230,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);

@@ -2245,7 +2245,7 @@ namespace Microsoft.Dafny {
         } else {

           expr.Type = e.Var.Type;

         }

-      

+

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         TopLevelDecl d;

@@ -2266,7 +2266,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);

@@ -2291,7 +2291,7 @@ namespace Microsoft.Dafny {
             j++;

           }

         }

-        

+

       } else if (expr is DisplayExpression) {

         DisplayExpression e = (DisplayExpression)expr;

         Type elementType = new InferredTypeProxy();

@@ -2309,7 +2309,7 @@ namespace Microsoft.Dafny {
         } else {

           expr.Type = new SeqType(elementType);

         }

-        

+

       } else if (expr is FieldSelectExpr) {

         var e = (FieldSelectExpr)expr;

         ResolveExpression(e.Obj, twoState);

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

           e.Type = SubstType(e.Field.Type, subst);

         }

-      

+

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         ResolveSeqSelectExpr(e, twoState, true);

@@ -2385,7 +2385,7 @@ namespace Microsoft.Dafny {
         if (!seqErr) {

           expr.Type = e.Seq.Type;

         }

-        

+

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         ResolveFunctionCallExpr(e, twoState, false);

@@ -2459,7 +2459,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);

@@ -2479,7 +2479,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)) {

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

             expr.Type = Type.Bool;

             break;

-          

+

           case BinaryExpr.Opcode.Disjoint:

             // TODO: the error messages are backwards from what (ideally) they should be. this is necessary because UnifyTypes can't backtrack.

             if (!UnifyTypes(e.E0.Type, e.E1.Type)) {

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

             expr.Type = Type.Bool;

             break;

-          

+

           case BinaryExpr.Opcode.Lt:

           case BinaryExpr.Opcode.Le:

           case BinaryExpr.Opcode.Add:

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

             }

             break;

-          

+

           case BinaryExpr.Opcode.Sub:

           case BinaryExpr.Opcode.Mul:

           case BinaryExpr.Opcode.Gt:

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

             expr.Type = Type.Bool;

             break;

-            

+

           case BinaryExpr.Opcode.Div:

           case BinaryExpr.Opcode.Mod:

             if (!UnifyTypes(e.E0.Type, Type.Int)) {

@@ -2574,12 +2574,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;

@@ -2652,7 +2652,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);

@@ -2669,7 +2669,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

@@ -2695,7 +2695,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");

@@ -2704,13 +2704,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) {

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

           Contract.Assert(memberNamesUsed.Count + me.MissingCases.Count == dtd.Ctors.Count);

         }

-        

+

       } else {

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

       }

@@ -3498,13 +3498,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.

@@ -3513,7 +3513,7 @@ namespace Microsoft.Dafny {
         ResolveExpression(expr, twoState);

       }

     }

-    

+

     void ResolveSeqSelectExpr(SeqSelectExpr e, bool twoState, bool allowNonUnitArraySelection) {

       Contract.Requires(e != null);

       if (e.Type != null) {

@@ -3557,7 +3557,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.

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

       Contract.Requires(expr != null);

       Contract.Requires(currentClass != null);

-    

+

       if (expr is LiteralExpr) {

         return false;

       } else if (expr is ThisExpr) {

@@ -3769,7 +3769,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);

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

 

     int scopeSizeWhereInstancesWereDisallowed = -1;

-    

+

     public bool AllowInstance {

       get { return scopeSizeWhereInstancesWereDisallowed == -1; }

       set

@@ -3791,7 +3791,7 @@ namespace Microsoft.Dafny {
       names.Add(null);

       things.Add(null);

     }

-    

+

     public void PopMarker() {

       int n = names.Count;

       while (true) {

@@ -3806,7 +3806,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) {

@@ -3820,7 +3820,7 @@ namespace Microsoft.Dafny {
         return true;

       }

     }

-    

+

     Thing Find(string name, bool topScopeOnly) {

       Contract.Requires(name != null);

       for (int n = names.Count; 0 <= --n; ) {

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

       return null;  // not present

     }

-    

+

     public Thing Find(string name) {

       Contract.Requires(name != null);

       return Find(name, false);

diff --git a/Dafny/SccGraph.cs b/Dafny/SccGraph.cs
index 9f4b22c5..4ae1c185 100644
--- a/Dafny/SccGraph.cs
+++ b/Dafny/SccGraph.cs
@@ -12,14 +12,14 @@ namespace Microsoft.Dafny {
       public readonly List<Vertex/*!*/>/*!*/ Successors = new List<Vertex/*!*/>();

       public List<Vertex/*!*/> SccMembers;  // non-null only for the representative of the SCC

       [ContractInvariantMethod]

-      void ObjectInvariant() 

+      void ObjectInvariant()

       {

         Contract.Invariant(cce.NonNullElements(Successors));

         Contract.Invariant(SccMembers==null || cce.NonNullElements(SccMembers));

       }

 

       public Vertex SccRepresentative;  // null if not computed

-      

+

       public int SccId;  // valid only for SCC representatives; indicates position of this representative vertex in the graph's topological sort

       // the following field is used during the computation of SCCs and of reachability

       public VisitedStatus Visited;

@@ -28,7 +28,7 @@ namespace Microsoft.Dafny {
       public int LowLink;

       // the following field is used during a Reaches computation

       public int Gen;  // generation <= Gen means this vertex has been visited in the current generation

-      

+

       public Vertex(Node n) {

         N = n;

       }

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

 

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(vertices!=null);

       Contract.Invariant(cce.NonNullElements(vertices.Values));

@@ -51,7 +51,7 @@ namespace Microsoft.Dafny {
     Dictionary<Node, Vertex/*!*/>/*!*/ vertices = new Dictionary<Node, Vertex/*!*/>();

     bool sccComputed = false;

     List<Vertex/*!*/> topologicallySortedRepresentatives;  // computed by the SCC computation

-    

+

     public int SccCount {

       get {

         ComputeSCCs();

@@ -60,11 +60,11 @@ namespace Microsoft.Dafny {
       }

     }

     int generation = 0;

-    

+

     public Graph()

     {

     }

-    

+

     /// <summary>

     /// Idempotently adds a vertex 'n' to the graph.

     /// </summary>

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

     /// <summary>

     /// Idempotently adds a vertex 'n' to the graph and then returns the Vertex for it.

-    /// </summary>    

+    /// </summary>

     Vertex GetVertex(Node n) {

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

 

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

       return v;

     }

-    

+

     /// <summary>

     /// Returns the vertex for 'n' if 'n' is in the graph.  Otherwise, returns null.

     /// </summary>

@@ -117,7 +117,7 @@ namespace Microsoft.Dafny {
       v0.AddSuccessor(v1);

       sccComputed = false;  // the addition of an edge may invalidate any previous computation of the graph's SCCs

     }

-    

+

     /// <summary>

     /// Idempotently adds 'n' as a vertex and then returns a Node that is the representative element of the

     /// strongly connected component containing 'n'.

@@ -125,7 +125,7 @@ namespace Microsoft.Dafny {
     public Node GetSCCRepresentative(Node n) {

       return GetSCCRepr(n).N;

     }

-    

+

     /// <summary>

     /// Idempotently adds 'n' as a vertex.  Then, returns the number of SCCs before the SCC of 'n' in the

     /// topologically sorting of SCCs.

@@ -133,7 +133,7 @@ namespace Microsoft.Dafny {
     public int GetSCCRepresentativeId(Node n) {

       return GetSCCRepr(n).SccId;

     }

-    

+

     Vertex GetSCCRepr(Node n) {

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

 

@@ -142,7 +142,7 @@ namespace Microsoft.Dafny {
       Contract.Assert(v.SccRepresentative != null);  // follows from what ComputeSCCs does

       return v.SccRepresentative;

     }

-    

+

     /// <summary>

     /// Returns a list of the topologically sorted SCCs, each represented in the list by its representative node.

     /// </summary>

@@ -172,21 +172,21 @@ namespace Microsoft.Dafny {
       }

       return nn;

     }

-    

+

     /// <summary>

     /// Idempotently adds 'n' as a vertex and then returns the size of the set of Node's in the strongly connected component

     /// that contains 'n'.

     /// </summary>

     public int GetSCCSize(Node n){

       Contract.Ensures(1 <= Contract.Result<int>());

-    

+

       Vertex v = GetVertex(n);

       ComputeSCCs();

       Vertex repr = v.SccRepresentative;

       Contract.Assert(repr != null && repr.SccMembers != null);  // follows from postcondition of ComputeSCCs

       return repr.SccMembers.Count;

     }

-    

+

     /// <summary>

     /// This method sets the SccRepresentative fields of the graph's vertices so that two

     /// vertices have the same representative iff they are in the same strongly connected

@@ -197,7 +197,7 @@ namespace Microsoft.Dafny {
     void ComputeSCCs()

     {

       Contract.Ensures(sccComputed);

-    

+

       if (sccComputed) { return; }  // check if already computed

 

       // reset all SCC information

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

       sccComputed = true;

     }

-    

+

     /// <summary>

     /// This is the 'SearchC' procedure from the Aho, Hopcroft, and Ullman book 'The Design and Analysis of Computer Algorithms'.

     /// </summary>

@@ -227,13 +227,13 @@ namespace Microsoft.Dafny {
      Contract.Requires(v.Visited == VisitedStatus.Unvisited);

      Contract.Requires(topologicallySortedRepresentatives != null);

       Contract.Ensures(v.Visited != VisitedStatus.Unvisited);

-    

+

       v.DfNumber = cnt;

       cnt++;

       v.LowLink = v.DfNumber;

       stack.Push(v);

       v.Visited = VisitedStatus.OnStack;

-      

+

       foreach (Vertex w in v.Successors) {

         if (w.Visited == VisitedStatus.Unvisited) {

           SearchC(w, stack, ref cnt);

@@ -243,7 +243,7 @@ namespace Microsoft.Dafny {
           v.LowLink = Math.Min(v.LowLink, w.DfNumber);

         }

       }

-      

+

       if (v.LowLink == v.DfNumber) {

         // The SCC containing 'v' has now been computed.

         v.SccId = topologicallySortedRepresentatives.Count;

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

       }

     }

-    

+

     /// <summary>

     /// Returns null if the graph has no cycles.  If the graph does contain some cycle, returns the list of

     /// vertices on one such cycle.

@@ -268,7 +268,7 @@ namespace Microsoft.Dafny {
       foreach (Vertex v in vertices.Values) {

         v.Visited = VisitedStatus.Unvisited;

       }

-      

+

       foreach (Vertex v in vertices.Values) {

         Contract.Assert(v.Visited != VisitedStatus.OnStack);

         if (v.Visited == VisitedStatus.Unvisited) {

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

       return null;  // there are no cycles

     }

-    

+

     /// <summary>

     /// A return of null means there are no cycles involving any vertex in the subtree rooted at v.

     /// A non-null return means a cycle has been found.  Then:

@@ -300,7 +300,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(v.Visited != VisitedStatus.Unvisited);

       Contract.Ensures(Contract.Result<List<Vertex>>() != null || v.Visited == VisitedStatus.Visited);

       Contract.Ensures(Contract.Result<List<Vertex>>() == null || Contract.Result<List<Vertex>>().Count != 0);

-    

+

       v.Visited = VisitedStatus.OnStack;

       foreach (Vertex succ in v.Successors) {

         // todo:  I would use a 'switch' statement, but there seems to be a bug in the Spec# compiler's type checking.

@@ -337,7 +337,7 @@ namespace Microsoft.Dafny {
       v.Visited = VisitedStatus.Visited;  // there are no cycles from here on

       return null;

     }

-    

+

     /// <summary>

     /// Returns whether or not 'source' reaches 'sink' in the graph.

     /// 'source' and 'sink' need not be in the graph; if neither is, the return value

@@ -352,7 +352,7 @@ namespace Microsoft.Dafny {
       generation++;

       return ReachSearch(a, b);

     }

-    

+

     bool ReachSearch(Vertex source, Vertex sink) {

       Contract.Requires(source != null);

       Contract.Requires(sink != null);

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 4d84a5f5..cc97fb40 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -21,14 +21,14 @@ namespace Microsoft.Dafny {
         predef = FindPredefinedDecls(boogieProgram);

       }

     }

-    

+

     // translation state

     readonly Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>/*!*/ classes = new Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>();

     readonly Dictionary<Field/*!*/,Bpl.Constant/*!*/>/*!*/ fields = new Dictionary<Field/*!*/,Bpl.Constant/*!*/>();

     readonly Dictionary<Field/*!*/, Bpl.Function/*!*/>/*!*/ fieldFunctions = new Dictionary<Field/*!*/, Bpl.Function/*!*/>();

 

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(cce.NonNullDictionaryAndValues(classes));

       Contract.Invariant(cce.NonNullDictionaryAndValues(fields));

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

         return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));

       }

-      

+

       public Bpl.Type MultiSetType(IToken tok, Bpl.Type ty) {

         Contract.Requires(tok != null);

         Contract.Requires(ty != null);

@@ -96,7 +96,7 @@ namespace Microsoft.Dafny {
         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);

@@ -104,7 +104,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);

@@ -150,7 +150,7 @@ 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) {

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

       return null;

     }

-    

+

     static Bpl.Program ReadPrelude() {

       string preludePath = Bpl.CommandLineOptions.Clo.DafnyPrelude;

       if (preludePath == null)

@@ -257,7 +257,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) {

@@ -265,7 +265,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))

       {

@@ -279,9 +279,9 @@ namespace Microsoft.Dafny {
           return prelude;

         }

       }

-*/      

+*/

     }

-    

+

     public Bpl.Program Translate(Program program) {

       Contract.Requires(program != null);

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

@@ -310,13 +310,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();

@@ -376,7 +376,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...));

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

       }

     }

-    

+

     void CreateBoundVariables(List<Formal/*!*/>/*!*/ formals, out Bpl.VariableSeq/*!*/ bvs, out List<Bpl.Expr/*!*/>/*!*/ args)

     {

       Contract.Requires(formals != null);

@@ -501,13 +501,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;

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

 

           AddAllocationAxiom(f);

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           AddFunction(f);

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

           AddFrameAxiom(f);

           AddWellformednessCheck(f);

-          

+

         } else if (member is Method) {

           Method m = (Method)member;

           // wellformedness check for method specification

@@ -557,14 +557,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

@@ -659,9 +659,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))

@@ -702,7 +702,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) {

@@ -754,7 +754,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;

@@ -813,7 +813,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);

@@ -850,7 +850,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));

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

       return name;

     }

-    

+

     /// <summary>

     /// Generate:

     ///   axiom (forall h: [ref, Field x]x, o: ref ::

@@ -887,13 +887,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) {

@@ -937,7 +937,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;

@@ -970,7 +970,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);

@@ -1013,7 +1013,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);

@@ -1075,7 +1075,7 @@ namespace Microsoft.Dafny {
         typeParams, inParams, outParams,

         localVariables, stmts);

       sink.TopLevelDeclarations.Add(impl);

-      

+

       currentMethod = null;

       loopHeapVarCount = 0;

       otherTmpVarCount = 0;

@@ -1090,7 +1090,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);

     }

@@ -1107,14 +1107,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

@@ -1131,7 +1131,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));

     }

 

@@ -1162,7 +1162,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... ::

@@ -1184,18 +1184,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);

@@ -1204,12 +1204,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

@@ -1243,7 +1243,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) {

@@ -1251,7 +1251,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),

@@ -1265,7 +1265,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);

@@ -1280,7 +1280,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;

@@ -1323,12 +1323,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();

@@ -1360,7 +1360,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) {

@@ -1466,7 +1466,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) {

@@ -1632,7 +1632,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);

@@ -1795,7 +1795,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);

@@ -1807,14 +1807,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 {

@@ -1889,7 +1889,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) {

@@ -2136,7 +2136,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);

@@ -2360,7 +2360,7 @@ namespace Microsoft.Dafny {
         return s;

       }

     }

-    

+

     Bpl.Constant GetClass(TopLevelDecl cl)

     {

       Contract.Requires(cl != null);

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

       return cc;

     }

-    

+

     Bpl.Expr GetTypeExpr(IToken tok, Type type)

     {

       Contract.Requires(tok != null);

@@ -2425,13 +2425,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);

@@ -2490,13 +2490,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);

@@ -2513,7 +2513,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));

@@ -2523,12 +2523,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);

@@ -2538,7 +2538,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) {

@@ -2558,7 +2558,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();

@@ -2569,7 +2569,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) {

@@ -2607,54 +2607,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);

@@ -2666,12 +2666,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];

@@ -2684,7 +2684,7 @@ namespace Microsoft.Dafny {
       loopHeapVarCount = 0;

       otherTmpVarCount = 0;

       _tmpIEs.Clear();

-            

+

       //  call inlined m;

       TrStmt(m.Body, builder, localVariables, etran);

 

@@ -2692,10 +2692,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);

@@ -2706,7 +2706,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;

@@ -2714,21 +2714,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;

@@ -2742,7 +2742,7 @@ namespace Microsoft.Dafny {
         Contract.Invariant(cce.NonNullDictionaryAndValues(subst));

       }

 

-          

+

       public override Expr VisitIdentifierExpr(Bpl.IdentifierExpr node)

       {

         Contract.Requires(node != null);

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

         if (subst.ContainsKey(node.Name))

           return subst[node.Name];

-        else 

+        else

           return base.VisitIdentifierExpr(node);

       }

     }

@@ -2767,32 +2767,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() {

@@ -2820,7 +2820,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

@@ -2837,17 +2837,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

@@ -2879,9 +2879,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));

     }

@@ -2913,15 +2913,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) {

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

         }

       }

-      

+

       if (type is BoolType) {

         return Bpl.Type.Bool;

       } else if (type is IntType) {

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

       }

     }

-    

+

     Bpl.TypeVariableSeq TrTypeParamDecls(List<TypeParameter/*!*/>/*!*/ tps)

     {

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

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

 

     // ----- Statement ----------------------------------------------------------------------------

-    

+

     Bpl.AssertCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage)

     {

       Contract.Requires(tok != null);

@@ -3036,10 +3036,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);

@@ -3048,11 +3048,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);

@@ -3093,7 +3093,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;

@@ -3316,7 +3316,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);

@@ -3350,14 +3350,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);

@@ -3512,7 +3512,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>();

@@ -3669,7 +3669,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) {

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

       }

     }

-    

+

     static Expression CreateIntLiteral(IToken tok, int n)

     {

       Contract.Requires(tok != null);

@@ -3768,13 +3768,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);

@@ -3783,7 +3783,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);

@@ -3797,7 +3797,7 @@ namespace Microsoft.Dafny {
       ite.Type = Type.Int;  // resolve here

       return ite;

     }

-    

+

     public IEnumerable<Expression> Conjuncts(Expression expr)

      {

       Contract.Requires(expr != null);

@@ -3835,7 +3835,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;

@@ -3887,7 +3887,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).

@@ -3908,7 +3908,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);

@@ -3975,7 +3975,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)

      {

@@ -3988,7 +3988,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);

@@ -4017,7 +4017,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);

@@ -4027,14 +4027,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);

@@ -4063,7 +4063,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)

@@ -4131,7 +4131,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

       }

@@ -4322,7 +4322,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;

@@ -4512,7 +4512,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);

@@ -4531,7 +4531,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);

@@ -4541,7 +4541,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);

@@ -4599,7 +4599,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);

@@ -4674,10 +4674,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));

@@ -4714,7 +4714,7 @@ namespace Microsoft.Dafny {
             i++;

           }

           return s;

-        

+

         } else if (expr is FieldSelectExpr) {

           FieldSelectExpr e = (FieldSelectExpr)expr;

           Contract.Assert(e.Field != null);

@@ -4766,7 +4766,7 @@ namespace Microsoft.Dafny {
             // if e0 == null && e1 == null, then we have the identity operation seq[..] == seq;

             return seq;

           }

-        

+

         } else if (expr is SeqUpdateExpr) {

           SeqUpdateExpr e = (SeqUpdateExpr)expr;

           Bpl.Expr seq = TrExpr(e.Seq);

@@ -4804,7 +4804,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

@@ -4890,7 +4890,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);

@@ -4916,12 +4916,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:

@@ -5031,12 +5031,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();

@@ -5055,7 +5055,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 {

@@ -5094,11 +5094,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

         }

@@ -5107,7 +5107,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)));

@@ -5186,7 +5186,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);

@@ -5195,7 +5195,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);

@@ -5209,7 +5209,7 @@ namespace Microsoft.Dafny {
           return e;

         }

       }

-      

+

       public static bool ModeledAsBoxType(Type t) {

         Contract.Requires(t != null);

         while (true) {

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

         return kv;

       }

-      

+

       // --------------- help routines ---------------

 

       public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e) {

@@ -5381,7 +5381,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);

@@ -5390,7 +5390,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);

@@ -5405,7 +5405,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);

@@ -5427,12 +5427,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) {

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

           n++;

         }

-        

+

         return r;

       }

 

@@ -5471,7 +5471,7 @@ namespace Microsoft.Dafny {
         return r;

       }

     }

-    

+

     enum BuiltinFunction {

       SetEmpty,

       SetUnionOne,

@@ -5507,17 +5507,17 @@ namespace Microsoft.Dafny {
       SeqEqual,

       SeqSameUntil,

       SeqFromArray,

-      

+

       IndexField,

       MultiIndexField,

-      

+

       Box,

       Unbox,

       IsCanonicalBoolBox,

 

       IsGoodHeap,

       HeapSucc,

-      

+

       DynamicType,  // allocated type (of object reference)

       DtType,       // type of datatype value

       TypeParams,   // type parameters of allocated type

@@ -5532,7 +5532,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)

     {

@@ -5684,7 +5684,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 2);

           Contract.Assert(typeInstantiation != null);

           return FunctionCall(tok, "Seq#FromArray", typeInstantiation, args);

-          

+

         case BuiltinFunction.IndexField:

           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);

@@ -5767,7 +5767,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);

@@ -6238,7 +6238,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;

@@ -6293,7 +6293,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);

@@ -6302,7 +6302,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);

@@ -6311,7 +6311,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);

@@ -6338,7 +6338,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);

@@ -6381,7 +6381,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);

@@ -6404,7 +6404,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);

@@ -6418,7 +6418,7 @@ namespace Microsoft.Dafny {
         var e = (ConcreteSyntaxExpression)expr;

         return Substitute(e.ResolvedExpression, receiverReplacement, substMap);

       }

-      

+

       if (newExpr == null) {

         return expr;

       } else {

@@ -6426,18 +6426,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>();

@@ -6455,7 +6455,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) {

@@ -6487,7 +6487,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);

@@ -6495,6 +6495,6 @@ namespace Microsoft.Dafny {
       }

       return attrs;

     }

-        

+

   }

-}
\ No newline at end of file
+}

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

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

 

-namespace Microsoft.Boogie 

+namespace Microsoft.Boogie

 {

   using System;

   using System.IO;

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

   using AI = Microsoft.AbstractInterpretationFramework;

 

-/* 

+/*

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

     BaseTypes

     Provers.Z3

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

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

     // Main

-    

-    public static int Main (string[] args) 

+

+    public static int Main (string[] args)

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

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

       ExitValue exitValue = ExitValue.VERIFIED;

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

       {

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

-        exitValue = ExitValue.PREPROCESSING_ERROR; 

+        exitValue = ExitValue.PREPROCESSING_ERROR;

         goto END;

       }

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

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

         if (errMsg != null) {

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

-          exitValue = ExitValue.PREPROCESSING_ERROR; 

+          exitValue = ExitValue.PREPROCESSING_ERROR;

           goto END;

         }

       }

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

         Console.WriteLine(CommandLineOptions.Clo.Version);

       }

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

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

       {

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

-        foreach (string arg in args) 

+        foreach (string arg in args)

         {Contract.Assert(arg != null);

           Console.WriteLine(arg);

         }

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

       }

 

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

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

       {Contract.Assert(file != null);

         string extension = Path.GetExtension(file);

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

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

           CommandLineOptions.Clo.XmlSink.Close();

         }

-        if (CommandLineOptions.Clo.Wait) 

+        if (CommandLineOptions.Clo.Wait)

         {

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

           Console.ReadLine();

         }

-        return (int)exitValue;        

+        return (int)exitValue;

     }

 

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

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

         return;

       }

-      

+

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

       string remaining = null;

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

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

         s = s.Substring(0, i);

       }

-      

+

       ConsoleColor col = Console.ForegroundColor;

       Console.ForegroundColor = ConsoleColor.Red;

       Console.WriteLine(s);

       Console.ForegroundColor = col;

-      

+

       if (remaining != null) {

         Console.WriteLine(remaining);

       }

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

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

           Program boogieProgram = translator.Translate(dafnyProgram);

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

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

           {

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

           }

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

       }

     }

-    

+

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

     {

       Contract.Requires(filename != null);

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

         CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaring;

     }

-    

-    

+

+

     static bool ProgramHasDebugInfo (Program program)

     {

       Contract.Requires(program != null);

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

-        return program.TopLevelDeclarations.Count > 0 && 

+        return program.TopLevelDeclarations.Count > 0 &&

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

     }

-    

-    

+

+

     /// <summary>

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

     /// Print newline after the message.

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

     }

 

-    

+

 

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

     {

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

       }

     }

-    

+

         /// <summary>

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

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

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

     Contract.Requires(bplFileName != null);

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

-    

-      

+

+

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

       PipelineOutcome oc = ResolveAndTypecheck(program, bplFileName);

       switch (oc) {

         case PipelineOutcome.Done:

           return oc;

-          

+

         case PipelineOutcome.ResolutionError:

         case PipelineOutcome.TypeCheckingError:

           {

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

         case PipelineOutcome.ResolvedAndTypeChecked:

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

-          

+

         default:

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

       }

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

 

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

-      

+

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

-      

+

       errorCount = program.Typecheck();

       if (errorCount != 0) {

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

         return PipelineOutcome.TypeCheckingError;

       }

-    

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

+

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

       {

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

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

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

       return PipelineOutcome.ResolvedAndTypeChecked;

     }

-    

+

     /// <summary>

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

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

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

     {Contract.Requires(program != null);

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

-    

+

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

-  

+

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

-      

+

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

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

-       

+

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

         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

       }

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

 

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

-            

+

       #region Verify each implementation

-      

+

 #if ROB_DEBUG

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

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

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

         {

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

-        }         

+        }

       }

       catch (ProverException e)

       {

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

                                 {

                                     // for ErrorTrace == 1 restrict the output;

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

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

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

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

                                     {

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

 

       #endregion

-      

+

       return PipelineOutcome.VerificationCompleted;

     }

-   

+

   }

 }

diff --git a/DafnyDriver/DafnyDriver.csproj b/DafnyDriver/DafnyDriver.csproj
index fb68eefd..cf88eed4 100644
--- a/DafnyDriver/DafnyDriver.csproj
+++ b/DafnyDriver/DafnyDriver.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

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

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

   <PropertyGroup>

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

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

   </ItemGroup>

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

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

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

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

   <Target Name="BeforeBuild">

   </Target>

   <Target Name="AfterBuild">

   </Target>

   -->

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

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index 47313465..9603dd6e 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -12,11 +12,14 @@ open DafnyPrinter
 open Utils

 

 open Microsoft.Boogie

-                    

-let VarsAreDifferent aa bb =

-  printf "false"

-  List.iter2 (fun (_,Var(a,_)) (_,Var(b,_)) -> printf " || %s != %s" a b) aa bb

 

+type MethodSolution = {

+   pathCond: Expr; 

+   heap : Map<Const * VarDecl, Const>; 

+   env  : Map<Const, Const>; 

+   ctx  : Set<Set<Const>>;

+}

+                    

 let Rename suffix vars =

   vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp))

 

@@ -75,6 +78,7 @@ let rec IsArgsOnly args expr =
   | IntLiteral(_)                        -> true

   | BoolLiteral(_)                       -> true

   | Star                                 -> true

+  | ObjLiteral(id)                       -> true

   | VarLiteral(id)

   | IdLiteral(id)                        -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false)

   | UnaryExpr(_,e)                       -> IsArgsOnly args e

@@ -87,7 +91,9 @@ let rec IsArgsOnly args expr =
   | SeqLength(e)                         -> IsArgsOnly args e

   | ForallExpr(vars,e)                   -> IsArgsOnly (List.concat [args; vars]) e

 

-let GetUnifications expr args (heap,env,ctx) =

+//TODO: unifications should probably by "Expr <--> Expr" instead of "Expr <--> Const"

+let GetUnifications indent expr args (heap,env,ctx) =

+  let idt = Indent indent

   // - first looks if the give expression talks only about method arguments (args)

   // - then checks if it doesn't already exist in the unification map

   // - then it tries to evaluate it to a constant

@@ -98,7 +104,7 @@ let GetUnifications expr args (heap,env,ctx) =
       let! argsOnly = IsArgsOnly args e |> Utils.BoolToOption

       let! notAlreadyAdded = Map.tryFind e unifMap |> Utils.IsNoneOption |> Utils.BoolToOption

       let! v = try Some(Eval (heap,env,ctx) true e |> Expr2Const) with ex -> None

-      Logger.DebugLine ("      - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v));

+      Logger.DebugLine (idt + "    - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v));

       return Map.add e v unifMap

     }

   // just recurses on all expressions

@@ -108,6 +114,7 @@ let GetUnifications expr args (heap,env,ctx) =
     | IntLiteral(_)

     | BoolLiteral(_)

     | VarLiteral(_)

+    | ObjLiteral(_)

     | IdLiteral(_)

     | Star                   -> unifs

     | Dot(e, _)

@@ -127,14 +134,15 @@ let GetUnifications expr args (heap,env,ctx) =
 /// Returns a map (Expr |--> Const) containing unifications

 /// found for the given method and heap/env/ctx

 //  =======================================================

-let GetUnificationsForMethod comp m (heap,env,ctx) =

+let GetUnificationsForMethod indent comp m (heap,env,ctx) =

+  let idt = Indent indent

   let rec GetArgValueUnifications args env = 

     match args with

     | Var(name,_) :: rest -> 

         match Map.tryFind (Unresolved(name)) env with

         | Some(c) ->

-            Logger.DebugLine ("      - adding unification " + (PrintConst c) + " <--> " + name);

-            Map.ofList [IdLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest env)

+            Logger.DebugLine (idt + "    - adding unification " + (PrintConst c) + " <--> " + name);

+            Map.ofList [VarLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest env)

         | None -> failwith ("couldn't find value for argument " + name)

     | [] -> Map.empty

   (* --- function body starts here --- *)

@@ -143,7 +151,7 @@ let GetUnificationsForMethod comp m (heap,env,ctx) =
       let args = List.concat [ins; outs]

       match args with 

       | [] -> Map.empty

-      | _  -> GetUnifications (BinaryAnd pre post) args (heap,env,ctx)

+      | _  -> GetUnifications indent (BinaryAnd pre post) args (heap,env,ctx)

               |> Utils.MapAddAll (GetArgValueUnifications args env)

   | _ -> failwith ("not a method: " + m.ToString())

 

@@ -164,7 +172,7 @@ let GetObjRefExpr o (heap,env,ctx) =
       let newVisited = Set.add o visited

       let refName = PrintObjRefName o (env,ctx)

       match refName with

-      | "this" -> Some(IdLiteral(refName))

+      | "this" -> Some(ObjLiteral("this"))

       | _ -> 

           let rec __fff lst = 

             match lst with

@@ -179,11 +187,11 @@ let GetObjRefExpr o (heap,env,ctx) =
   if objRef2ExprCache.ContainsKey(o) then

     Some(objRef2ExprCache.[o])

   else

-      let res = __GetObjRefExpr o (heap,env,ctx) (Set.empty)

-      match res with 

-      | Some(e) -> objRef2ExprCache.Add(o, e)

-      | None -> ()

-      res

+    let res = __GetObjRefExpr o (heap,env,ctx) (Set.empty)

+    match res with 

+    | Some(e) -> objRef2ExprCache.Add(o, e)

+    | None -> ()

+    res

 

 //  =======================================================

 /// Applies given unifications onto the given heap/env/ctx

@@ -191,7 +199,8 @@ let GetObjRefExpr o (heap,env,ctx) =
 /// If "conservative" is true, applies only those that 

 /// can be verified to hold, otherwise applies all of them

 //  =======================================================

-let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative = 

+let rec ApplyUnifications indent prog comp mthd unifs (heap,env,ctx) conservative = 

+  let idt = Indent indent

   let __CheckUnif o f e idx =

     if not conservative || not Options.CONFIG.checkUnifications then 

       true 

@@ -205,7 +214,7 @@ let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative =
                           | _                                            -> BinaryEq lhs e 

       // check if the assertion follows and if so update the env

       let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr)

-      Logger.Debug ("      - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ")

+      Logger.Debug (idt + "    - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ")

       let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd))

       if ok then

         Logger.DebugLine " HOLDS"

@@ -215,13 +224,13 @@ let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative =
   (* --- function body starts here --- *)

   match unifs with

   | (e,c) :: rest -> 

-      let restHeap,env,ctx = ApplyUnifications prog comp mthd rest (heap,env,ctx) conservative

+      let restHeap,env,ctx = ApplyUnifications indent prog comp mthd rest (heap,env,ctx) conservative

       let newHeap = restHeap |> Map.fold (fun acc (o,f) l ->

                                             let value = TryResolve (env,ctx) l

                                             if value = c then

                                               if __CheckUnif o f e -1 then                                                

                                                 // change the value to expression

-                                                Logger.TraceLine (sprintf "      - applied: %s.%s --> %s" (PrintConst o) (GetVarName f) (PrintExpr 0 e) )

+                                                //Logger.TraceLine (sprintf "%s    - applied: %s.%s --> %s" idt (PrintConst o) (GetVarName f) (PrintExpr 0 e) )

                                                 acc |> Map.add (o,f) (ExprConst(e))

                                               else

                                                 // don't change the value unless "conservative = false"

@@ -231,7 +240,7 @@ let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative =
                                                     match lst with

                                                     | lstElem :: rest when lstElem = c ->

                                                         if __CheckUnif o f e cnt then

-                                                          Logger.TraceLine (sprintf "      - applied: %s.%s[%d] --> %s" (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) )

+                                                          //Logger.TraceLine (sprintf "%s    - applied: %s.%s[%d] --> %s" idt (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) )

                                                           ExprConst(e) :: __UnifyOverLst rest (cnt+1)

                                                         else  

                                                           lstElem :: __UnifyOverLst rest (cnt+1)

@@ -255,53 +264,33 @@ let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative =
 //  ====================================================================================

 /// Returns whether the code synthesized for the given method can be verified with Dafny

 //  ====================================================================================

-let VerifySolution prog comp mthd (heap,env,ctx) =

+let VerifySolution prog comp mthd sol =

   // print the solution to file and try to verify it with Dafny

-  let solution = Map.empty |> Map.add (comp,mthd) (heap,env,ctx)

-  let code = PrintImplCode prog solution (fun p -> [comp,mthd])

+  let solutions = Map.empty |> Map.add (comp,mthd) sol

+  let code = PrintImplCode prog solutions (fun p -> [comp,mthd])

   CheckDafnyProgram code dafnyVerifySuffix

 

-let TryInferConditionals prog comp m unifs (heap,env,ctx) = 

-  let heap2,env2,ctx2 = ApplyUnifications prog comp m unifs (heap,env,ctx) false

-  // get expressions to evaluate:

-  //   - add pre and post conditions

-  //   - go through all objects on the heap and assert its invariant  

-  let pre,post = GetMethodPrePost m

-  let prepostExpr = post //TODO: do we need the "pre" here as well?

-  let heapObjs = heap |> Map.fold (fun acc (o,_) _ -> acc |> Set.add o) Set.empty

-  let expr = heapObjs |> Set.fold (fun acc o -> 

-                                     let receiverOpt = GetObjRefExpr o (heap,env,ctx) 

-                                     let receiver = Utils.ExtractOption receiverOpt

-                                     match Resolve (env,ctx) o with

-                                     | NewObj(_,tOpt) | ThisConst(_,tOpt) ->

-                                         let t = Utils.ExtractOptionMsg "Type missing for heap object" tOpt

-                                         let objComp = FindComponent prog (GetTypeShortName t) |> Utils.ExtractOption

-                                         let objInvs = GetInvariantsAsList objComp

-                                         let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)

-                                         objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

-                                     | _ -> failwith "not supposed to happen"

-                                  ) prepostExpr

-  expr |> SplitIntoConjunts |> List.iter (fun e -> printfn "%s" (PrintExpr 0 e); printfn "")

-  // now evaluate and see what's left

-  let c = Eval (heap2,env2,ctx2) false expr

-  Some(heap2,env2,ctx2)

-   

 //  ============================================================================

 /// Attempts to synthesize the initialization code for the given constructor "m"

 ///

 /// Returns a (heap,env,ctx) tuple

 //  ============================================================================                           

-let AnalyzeConstructor prog comp m =

+let rec AnalyzeConstructor indent prog comp m =

+  let idt = Indent indent

   let methodName = GetMethodName m

+  let pre,post = GetMethodPrePost m

   // generate Dafny code for analysis first

   let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m) FalseLiteral)

-  Logger.InfoLine ("  [*] analyzing constructor " + methodName + (PrintSig (GetMethodSig m)))

-  Logger.Info      "      - searching for an instance      ..."

+  Logger.InfoLine (idt + "[*] Analyzing constructor")

+  Logger.InfoLine (idt + "------------------------------------------")

+  Logger.InfoLine (PrintMethodSignFull (indent + 4) m)

+  Logger.InfoLine (idt + "------------------------------------------")

+  Logger.Info     (idt + "    - searching for an instance      ...")

   let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m))  

   if models.Count = 0 then

     // no models means that the "assert false" was verified, which means that the spec is inconsistent

-    Logger.WarnLine " !!! SPEC IS INCONSISTENT !!!"

-    None

+    Logger.WarnLine (idt + " !!! SPEC IS INCONSISTENT !!!")

+    []

   else 

     if models.Count > 1 then 

       Logger.WarnLine " FAILED "

@@ -309,21 +298,65 @@ let AnalyzeConstructor prog comp m =
     Logger.InfoLine " OK "

     let model = models.[0]

     let heap,env,ctx = ReadFieldValuesFromModel model prog comp m

-    let unifs = GetUnificationsForMethod comp m (heap,env,ctx) |> Map.toList

-    let heap,env,ctx = ApplyUnifications prog comp m unifs (heap,env,ctx) true

+    let unifs = GetUnificationsForMethod indent comp m (heap,env,ctx) |> Map.toList

+    let heap,env,ctx = ApplyUnifications indent prog comp m unifs (heap,env,ctx) true

     if Options.CONFIG.verifySolutions then

-      Logger.InfoLine "      - verifying synthesized solution ... "

-      let verified = VerifySolution prog comp m (heap,env,ctx)

-      Logger.Info "      "      

+      Logger.InfoLine (idt + "    - verifying synthesized solution ... ")

+      let sol = [TrueLiteral, (heap,env,ctx)]

+      let verified = VerifySolution prog comp m sol

+      Logger.Info (idt + "    ")

       if verified then

         Logger.InfoLine "~~~ VERIFIED ~~~"

-        Some(heap,env,ctx)

+        sol

       else 

         Logger.InfoLine "!!! NOT VERIFIED !!!"

-        Logger.InfoLine "Trying to infer conditionals"

-        TryInferConditionals prog comp m unifs (heap,env,ctx)

+        Logger.InfoLine (idt + "    Strengthening the pre-condition")

+        TryInferConditionals (indent + 4) prog comp m unifs (heap,env,ctx)

     else

-      Some(heap,env,ctx)

+      [TrueLiteral, (heap,env,ctx)]

+and TryInferConditionals indent prog comp m unifs (heap,env,ctx) = 

+  let idt = Indent indent

+  let heap2,env2,ctx2 = ApplyUnifications indent prog comp m unifs (heap,env,ctx) false

+  // get expressions to evaluate:

+  //   - add pre and post conditions                                     

+  //   - go through all objects on the heap and assert its invariant  

+  let pre,post = GetMethodPrePost m

+  let prepostExpr = post //TODO: do we need the "pre" here as well?

+  let heapObjs = heap |> Map.fold (fun acc (o,_) _ -> acc |> Set.add o) Set.empty

+  let expr = heapObjs |> Set.fold (fun acc o -> 

+                                     let receiverOpt = GetObjRefExpr o (heap,env,ctx) 

+                                     let receiver = Utils.ExtractOption receiverOpt

+                                     match Resolve (env,ctx) o with

+                                     | NewObj(_,tOpt) | ThisConst(_,tOpt) ->

+                                         let t = Utils.ExtractOptionMsg "Type missing for heap object" tOpt

+                                         let objComp = FindComponent prog (GetTypeShortName t) |> Utils.ExtractOption

+                                         let objInvs = GetInvariantsAsList objComp

+                                         let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)

+                                         objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

+                                     | _ -> failwith "not supposed to happen"

+                                  ) prepostExpr

+  //expr |> SplitIntoConjunts |> List.iter (fun e -> printfn "%s" (PrintExpr 0 e); printfn "")

+  // now evaluate and see what's left

+  let newCond = Eval (heap2,env2,ctx2) false expr

+  try

+    if newCond = TrueLiteral then

+      Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

+      []

+    else

+      Logger.InfoLine (sprintf "%s    - candidate pre-condition: %s" idt (PrintExpr 0 newCond))

+      let p2,c2,m2 = AddPrecondition prog comp m newCond

+      Logger.Info (idt + "    - verifying partial solution ... ")

+      let sol = [newCond, (heap2,env2,ctx2)]

+      let verified = VerifySolution p2 c2 m2 sol

+      if verified then

+        Logger.InfoLine "VERIFIED"

+        let p3,c3,m3 = AddPrecondition prog comp m (UnaryNot(newCond))

+        sol.[0] :: AnalyzeConstructor (indent + 2) p3 c3 m3

+      else 

+        Logger.InfoLine "NOT VERIFIED"

+        []                     

+  with

+    ex -> raise ex

 

 let GetMethodsToAnalyze prog =

   let mOpt = Options.CONFIG.methodToSynth;

@@ -365,11 +398,9 @@ let rec AnalyzeMethods prog members =
   | (comp,m) :: rest -> 

       match m with

       | Method(_,_,_,_,true) -> 

-          let solOpt = AnalyzeConstructor prog comp m

+          let solOpt = AnalyzeConstructor 2 prog comp m

           Logger.InfoLine ""

-          match solOpt with

-          | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx)

-          | None -> AnalyzeMethods prog rest

+          AnalyzeMethods prog rest |> Map.add (comp,m) solOpt

       | _ -> AnalyzeMethods prog rest

   | [] -> Map.empty

 

diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs
index 7af1b6f6..1ddf1f31 100644
--- a/Jennisys/Ast.fs
+++ b/Jennisys/Ast.fs
@@ -24,12 +24,16 @@ type VarDecl =
 (* 

    the difference between IdLiteral and VarLiteral is that the VarLiteral is more specific, 

    it always referes to a local variable (either method parameter or quantification variable)  

+

+   ObjLiteral is a concrete object, so if two ObjLiterals have different names, 

+   they are different objects (as opposed to IdLiterals and VarLiterals, which can alias).

  *)

 type Expr =

   | IntLiteral of int

   | BoolLiteral of bool

   | VarLiteral of string  

-  | IdLiteral of string  

+  | IdLiteral of string 

+  | ObjLiteral of string 

   | Star

   | Dot of Expr * string

   | UnaryExpr of string * Expr

@@ -42,6 +46,19 @@ type Expr =
   | SetExpr of Expr list //TODO: maybe this should really be a set instead of a list

   | ForallExpr of VarDecl list * Expr

 

+type Const = 

+  | IntConst   of int

+  | BoolConst  of bool

+  | SetConst   of Set<Const>

+  | SeqConst   of Const list

+  | NullConst

+  | NoneConst

+  | ThisConst  of (* loc id *) string * Type option

+  | VarConst   of string

+  | NewObj     of (* loc id *) string * Type option

+  | ExprConst  of Expr

+  | Unresolved of (* loc id *) string 

+

 type Stmt =

   | Block of Stmt list

   | Assign of Expr * Expr

@@ -67,15 +84,3 @@ type Component =
 

 type Program =

   | Program of Component list

-

-type Const = 

-  | IntConst   of int

-  | BoolConst  of bool

-  | SetConst   of Set<Const>

-  | SeqConst   of Const list

-  | NullConst

-  | NoneConst

-  | ThisConst  of (* loc id *) string * Type option

-  | NewObj     of (* loc id *) string * Type option

-  | ExprConst  of Expr

-  | Unresolved of (* loc id *) string 
\ No newline at end of file
diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index 72bd189e..25d2a129 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -9,258 +9,89 @@ module AstUtils
 open Ast

 open Utils

 

-// ------------------------------- Visitor Stuff -------------------------------------------

-

-let rec VisitExpr visitorFunc expr acc =

-  match expr with

-  | IntLiteral(_)

-  | BoolLiteral(_)

-  | VarLiteral(_)

-  | IdLiteral(_)  

-  | Star                             -> acc |> visitorFunc expr

-  | Dot(e, _)

-  | ForallExpr(_,e)                  

-  | UnaryExpr(_,e)                   

-  | SeqLength(e)                     -> acc |> visitorFunc expr |> VisitExpr visitorFunc e

-  | SelectExpr(e1, e2)               

-  | BinaryExpr(_,_,e1,e2)            -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2

-  | IteExpr(e1,e2,e3)                 

-  | UpdateExpr(e1,e2,e3)             -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 |> VisitExpr visitorFunc e3

-  | SequenceExpr(exs) | SetExpr(exs) -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc)

-  

-

-// ------------------------------- End Visitor Stuff -------------------------------------------

-

-exception EvalFailed 

-

-let DefaultResolver e = e

-

-let DefaultFallbackResolver resolverFunc e = 

-  match resolverFunc e with

-  | Some(e') -> e'

-  | None -> e

-

-let EvalSym resolverFunc expr = 

-  let rec __EvalSym ctx expr = 

-    match expr with

-    | IntLiteral(_)  -> expr

-    | BoolLiteral(_) -> expr

-    | Star           -> expr //TODO: can we do better?

-    | VarLiteral(_)  -> resolverFunc expr

-    | IdLiteral(_)   -> resolverFunc expr

-    | Dot(_)         -> resolverFunc expr

-    | SeqLength(e)   -> 

-        let e' = __EvalSym ctx e

-        match e' with

-        | SequenceExpr(elist) -> IntLiteral(List.length elist)

-        | _ -> SeqLength(e')

-    | SequenceExpr(elist) -> 

-        let elist' = elist |> List.fold (fun acc e -> __EvalSym ctx e :: acc) [] |> List.rev

-        SequenceExpr(elist')

-    | SetExpr(elist) -> 

-        let eset' = elist |> List.fold (fun acc e -> Set.add (__EvalSym ctx e) acc) Set.empty

-        SetExpr(Set.toList eset')

-    | SelectExpr(lst, idx) ->

-        let lst', idx' = __EvalSym ctx lst, __EvalSym ctx idx 

-        match lst', idx' with

-        | SequenceExpr(elist), IntLiteral(n) -> elist.[n] 

-        | _ -> SelectExpr(lst', idx')

-    | UpdateExpr(lst,idx,v) ->

-        let lst', idx', v' = __EvalSym ctx lst, __EvalSym ctx idx, __EvalSym ctx v

-        match lst', idx', v' with

-        | SequenceExpr(elist), IntLiteral(n), _ -> SequenceExpr(Utils.ListSet n v' elist)

-        | _ -> UpdateExpr(lst', idx', v')

-    | IteExpr(c, e1, e2) ->

-       let c', e1', e2' = __EvalSym ctx c, __EvalSym ctx e1, __EvalSym ctx e2

-       match c' with

-       | BoolLiteral(b) -> if b then e1' else e2'

-       | _ -> IteExpr(c', e1', e2')

-    | BinaryExpr(p,op,e1,e2) ->

-        let e1' = __EvalSym ctx e1

-        let e2' = __EvalSym ctx e2 

-        let recomposed = BinaryExpr(p,op,e1',e2')

-        match op with

-        | "=" ->

-            match e1', e2' with

-            | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2)

-            | IntLiteral(n1), IntLiteral(n2)   -> BoolLiteral(n1 = n2)

-            | _ when e1' = e2' -> BoolLiteral(true)

-            | _ -> recomposed

-        | "!=" -> 

-            match e1', e2' with

-            | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(not (b1 = b2))

-            | IntLiteral(n1), IntLiteral(n2)   -> BoolLiteral(not (n1 = n2))

-            | _ when e1' = e2' -> BoolLiteral(false)

-            | _ -> resolverFunc expr

-        | "<" -> 

-            match e1', e2' with

-            | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 < n2)

-            | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) < (List.length s2))

-            | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2))

-            | _ -> recomposed

-        | "<=" -> 

-            match e1', e2' with

-            | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 <= n2)

-            | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) <= (List.length s2))

-            | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2))

-            | _ -> recomposed

-        | ">" -> 

-            match e1', e2' with

-            | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 > n2)

-            | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) > (List.length s2))

-            | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2))

-            | _ -> recomposed

-        | ">=" -> 

-            match e1', e2' with

-            | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 >= n2)

-            | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) >= (List.length s2))

-            | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2))

-            | _ -> recomposed

-        | "in" -> 

-            match e1', e2' with

-            | _, SetExpr(s)       

-            | _, SequenceExpr(s)  -> BoolLiteral(Utils.ListContains e1' s)

-            | _ -> recomposed

-        | "!in" -> 

-            match e1', e2' with

-            | _, SetExpr(s)       

-            | _, SequenceExpr(s)  -> BoolLiteral(not (Utils.ListContains e1' s))

-            | _ -> recomposed

-        | "+" -> 

-            match e1', e2' with

-            | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 + n2)

-            | SequenceExpr(l1), SequenceExpr(l2) -> SequenceExpr(List.append l1 l2)

-            | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.union (Set.ofList s1) (Set.ofList s2) |> Set.toList)

-            | _ -> recomposed

-        | "-" -> 

-            match e1', e2' with

-            | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 - n2)

-            | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.difference (Set.ofList s1) (Set.ofList s2) |> Set.toList)

-            | _ -> recomposed

-        | "*" -> 

-            match e1', e2' with

-            | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 * n2)

-            | _ -> recomposed

-        | "div" -> 

-            match e1', e2' with

-            | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 / n2)

-            | _ -> recomposed

-        | "mod" -> 

-            match e1', e2' with

-            | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 % n2)

-            | _ -> recomposed

-        | "&&" -> 

-           match e1', e2' with

-            | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 && b2)

-            | _ -> recomposed

-        | "||" -> 

-           match e1', e2' with

-            | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 || b2)

-            | _ -> recomposed

-        | "==>" -> 

-           match e1', e2' with

-            | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral((not b1) || b2)

-            | _ -> recomposed

-        | "<==>" -> 

-           match e1', e2' with

-            | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2)

-            | _ -> recomposed

-        | _ -> recomposed

-    | UnaryExpr(op, e) ->

-        let e' = __EvalSym ctx e

-        let recomposed = UnaryExpr(op, e')

-        match op with

-        | "!" -> 

-            match e' with

-            | BoolLiteral(b) -> BoolLiteral(not b)

-            | _ -> recomposed

-        | "-" -> 

-            match e' with

-            | IntLiteral(n) -> IntLiteral(-n)

-            | _ -> recomposed

-        | _ -> recomposed

-    | ForallExpr(vars, e) -> 

-        let rec PrintSep sep f list =

-          match list with

-          | [] -> ""

-          | [a] -> f a

-          | a :: more -> (f a) + sep + (PrintSep sep f more)

-        let rec PrintType ty =

-          match ty with

-          | IntType                   -> "int"

-          | BoolType                  -> "bool"

-          | NamedType(id, args)       -> if List.isEmpty args then id else (PrintSep ", " (fun s -> s) args)

-          | SeqType(t)                -> sprintf "seq[%s]" (PrintType t)

-          | SetType(t)                -> sprintf "set[%s]" (PrintType t)

-          | InstantiatedType(id,args) -> sprintf "%s[%s]" id (PrintSep ", " (fun a -> PrintType a) args)

-        let PrintVarDecl vd =

-          match vd with

-          | Var(id,None) -> id

-          | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)

-        vars |> List.iter (fun v -> printfn "%s" (PrintVarDecl v))

-        resolverFunc expr //TODO

-  __EvalSym [] expr 

+//  =====================

+/// Returns TRUE literal

+//  =====================

+let TrueLiteral = BoolLiteral(true)

 

-//  =======================================

-/// Converts a given constant to expression

-//  =======================================

-let rec Const2Expr c =

-  match c with

-  | IntConst(n) -> IntLiteral(n)

-  | BoolConst(b) -> BoolLiteral(b)

-  | SeqConst(clist) -> 

-      let expList = clist |> List.fold (fun acc c -> Const2Expr c :: acc) [] |> List.rev

-      SequenceExpr(expList)

-  | ThisConst(_) -> IdLiteral("this")

-  | Unresolved(name) -> IdLiteral(name)

-  | NullConst -> IdLiteral("null")

-  | ExprConst(e) -> e

-  | _ -> failwithf "not implemented or not supported: %O" c

+//  =====================

+/// Returns FALSE literal

+//  =====================

+let FalseLiteral = BoolLiteral(false)

 

-let rec Expr2Const e =

-  match e with

-  | IntLiteral(n) -> IntConst(n)

-  | BoolLiteral(b) -> BoolConst(b)

-  | IdLiteral("this") -> ThisConst("this",None)

-  | IdLiteral("null") -> NullConst

-  | IdLiteral(id) -> Unresolved(id)

-  | VarLiteral(id) -> Unresolved(id)

-  | SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2Const)

-  | SetExpr(elist) -> SetConst(elist |> List.map Expr2Const |> Set.ofList)

-  | _ -> failwithf "Not a constant: %O" e

+let UnaryNeg sub =

+  match sub with

+  | UnaryExpr("-", s) -> s

+  | _ -> UnaryExpr("-", sub)

 

-let TryExpr2Const e =

-  try 

-    Some(Expr2Const e)

-  with

-    | ex -> None

+let UnaryNot sub =

+  match sub with

+  | UnaryExpr("!", s) -> s

+  | _ -> UnaryExpr("!", sub)

 

 //  =======================================================================

 /// Returns a binary AND of the two given expressions with short-circuiting

 //  =======================================================================

 let BinaryAnd (lhs: Expr) (rhs: Expr) = 

-    match lhs, rhs with

-    | IdLiteral("true"), _  -> rhs

-    | IdLiteral("false"), _ -> IdLiteral("false")

-    | _, IdLiteral("true")  -> lhs

-    | _, IdLiteral("false") -> IdLiteral("false")

-    | _, _                  -> BinaryExpr(30, "&&", lhs, rhs)

+  match lhs, rhs with

+  | BoolLiteral(true), _  -> rhs

+  | BoolLiteral(false), _ -> FalseLiteral

+  | _, BoolLiteral(true)  -> lhs

+  | _, BoolLiteral(false) -> FalseLiteral

+  | _, _                  -> BinaryExpr(30, "&&", lhs, rhs)

 

 //  =======================================================================

 /// Returns a binary OR of the two given expressions with short-circuiting

 //  =======================================================================

 let BinaryOr (lhs: Expr) (rhs: Expr) = 

-    match lhs, rhs with

-    | IdLiteral("true"), _  -> IdLiteral("true")

-    | IdLiteral("false"), _ -> rhs

-    | _, IdLiteral("true")  -> IdLiteral("true")

-    | _, IdLiteral("false") -> lhs

-    | _, _                  -> BinaryExpr(30, "||", lhs, rhs)

+  match lhs, rhs with

+  | BoolLiteral(true), _  -> TrueLiteral

+  | BoolLiteral(false), _ -> rhs

+  | _, BoolLiteral(true)  -> TrueLiteral

+  | _, BoolLiteral(false) -> lhs

+  | _, _                  -> BinaryExpr(30, "||", lhs, rhs)

 

 //  ===================================================================================

-/// Returns a binary IMPLIES of the two given expressions (TODO: with short-circuiting)

+/// Returns a binary IMPLIES of the two given expressions 

 //  ===================================================================================

-let BinaryImplies lhs rhs = BinaryExpr(20, "==>", lhs, rhs)

+let BinaryImplies lhs rhs = 

+  match lhs, rhs with

+  | BoolLiteral(false), _ -> FalseLiteral

+  | BoolLiteral(true), _  -> rhs

+  | _, BoolLiteral(true)  -> lhs

+  | _, BoolLiteral(false) -> UnaryNot(lhs)

+  | _ -> BinaryExpr(20, "==>", lhs, rhs)

+

+

+//let TrueLiteral = IdLiteral("true")

+//let FalseLiteral = IdLiteral("false")

+//

+////  =======================================================================

+///// Returns a binary AND of the two given expressions with short-circuiting

+////  =======================================================================

+//let BinaryAnd (lhs: Expr) (rhs: Expr) = 

+//    match lhs, rhs with

+//    | IdLiteral("true"), _  -> rhs

+//    | IdLiteral("false"), _ -> IdLiteral("false")

+//    | _, IdLiteral("true")  -> lhs

+//    | _, IdLiteral("false") -> IdLiteral("false")

+//    | _, _                  -> BinaryExpr(30, "&&", lhs, rhs)

+//

+////  =======================================================================

+///// Returns a binary OR of the two given expressions with short-circuiting

+////  =======================================================================

+//let BinaryOr (lhs: Expr) (rhs: Expr) = 

+//    match lhs, rhs with

+//    | IdLiteral("true"), _  -> IdLiteral("true")

+//    | IdLiteral("false"), _ -> rhs

+//    | _, IdLiteral("true")  -> IdLiteral("true")

+//    | _, IdLiteral("false") -> lhs

+//    | _, _                  -> BinaryExpr(30, "||", lhs, rhs)

+//

+////  ===================================================================================

+///// Returns a binary IMPLIES of the two given expressions (TODO: with short-circuiting)

+////  ===================================================================================

+//let BinaryImplies lhs rhs = BinaryExpr(20, "==>", lhs, rhs)

 

 //  =======================================================

 /// Constructors for binary EQ/NEQ of two given expressions

@@ -273,23 +104,13 @@ let BinaryEq lhs rhs = BinaryExpr(40, "=", lhs, rhs)
 //  =======================================================

 let BinaryIn lhs rhs = BinaryExpr(40, "in", lhs, rhs)

 let BinaryNotIn lhs rhs = BinaryExpr(40, "!in", lhs, rhs)

-

-//  =====================

-/// Returns TRUE literal

-//  =====================

-let TrueLiteral = IdLiteral("true")

-

-//  =====================

-/// Returns FALSE literal

-//  =====================

-let FalseLiteral = IdLiteral("false")

-

+  

 //  ==========================================

 /// Splits "expr" into a list of its conjuncts

 //  ==========================================

 let rec SplitIntoConjunts expr = 

   match expr with

-  | IdLiteral("true") -> []

+  | BoolLiteral(true) -> []

   | BinaryExpr(_,"&&",e0,e1) -> List.concat [SplitIntoConjunts e0 ; SplitIntoConjunts e1]

   | _ -> [expr]

 

@@ -299,6 +120,46 @@ let rec SplitIntoConjunts expr =
 let rec ForeachConjunct f expr =

   SplitIntoConjunts expr |> List.fold (fun acc e -> acc + (f e)) ""

 

+//  =======================================

+/// Converts a given constant to expression

+//  =======================================

+let rec Const2Expr c =

+  match c with

+  | IntConst(n) -> IntLiteral(n)

+  | BoolConst(b) -> BoolLiteral(b)

+  | SeqConst(clist) -> 

+      let expList = clist |> List.fold (fun acc c -> Const2Expr c :: acc) [] |> List.rev

+      SequenceExpr(expList)

+  | SetConst(cset) -> 

+      let expSet = cset |> Set.fold (fun acc c -> Set.add (Const2Expr c) acc) Set.empty

+      SetExpr(Set.toList expSet)

+  | VarConst(id) -> VarLiteral(id)

+  | ThisConst(name,_) 

+  | NewObj(name,_)   -> ObjLiteral(name)

+  | NullConst -> ObjLiteral("null")

+  | ExprConst(e) -> e

+  | Unresolved(name) -> printf "What about unresolved stuff??"; failwith "don't want to convert unresolved to expr"

+  | _ -> failwithf "not implemented or not supported: %O" c

+

+let rec Expr2Const e =

+  match e with

+  | IntLiteral(n) -> IntConst(n)

+  | BoolLiteral(b) -> BoolConst(b)

+  | ObjLiteral("this") -> ThisConst("this",None)

+  | ObjLiteral("null") -> NullConst

+  | ObjLiteral(name) -> NewObj(name, None) //TODO: or Unresolved?

+  | IdLiteral(id) -> Unresolved(id)

+  | VarLiteral(id) -> VarConst(id)

+  | SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2Const)

+  | SetExpr(elist) -> SetConst(elist |> List.map Expr2Const |> Set.ofList)

+  | _ -> failwithf "Not a constant: %O" e

+

+let TryExpr2Const e =

+  try 

+    Some(Expr2Const e)

+  with

+    | ex -> None

+

 // --- search functions ---

                      

 //  =========================================================

@@ -460,6 +321,247 @@ let FindVar (prog: Program) clsName fldName =
       GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)

                         |> Utils.ListToOption

   | None -> None

+

+let AddPrecondition prog comp m e =

+  match prog, comp, m with

+  | Program(clist), Component(Class(cname, ctypeParams, members), model, code), Method(mn, sgn, pre, post, cstr) ->

+      let newMthd = Method(mn, sgn, BinaryAnd pre e, post, cstr)

+      let newCls = Class(cname, ctypeParams, Utils.ListReplace m newMthd members)

+      let newComp = Component(newCls, model, code)

+      let newProg = Program(Utils.ListReplace comp newComp clist)

+      newProg, newComp, newMthd

+  | _ -> failwithf "Not a method: %O" m

+

+////////////////////

+

+exception EvalFailed of string

+

+let DefaultResolver e = e

+

+let DefaultFallbackResolver resolverFunc e = 

+  match resolverFunc e with

+  | Some(e') -> e'

+  | None -> e

+

+let __CheckEqual e1 e2 =

+  match e1, e2 with

+  | BoolLiteral(b1), BoolLiteral(b2) -> Some(b1 = b2)

+  | IntLiteral(n1), IntLiteral(n2)   -> Some(n1 = n2)

+  | ObjLiteral(o1), ObjLiteral(o2)   -> Some(o1 = o2)

+  | SetExpr(elist1), SetExpr(elist2) -> Some(Set.ofList elist1 = Set.ofList elist2)

+  | SequenceExpr(elist1), SequenceExpr(elist2) -> Some(elist1 = elist2)

+  | UnaryExpr("-", sub1), sub2

+  | sub1, UnaryExpr("-", sub2)                 when sub1 = sub2 -> Some(false)

+  | UnaryExpr("-", sub1), UnaryExpr("-", sub2) when sub1 = sub2 -> Some(true)

+  | UnaryExpr("!", sub1), sub2

+  | sub1, UnaryExpr("!", sub2)                 when sub1 = sub2 -> Some(false)

+  | UnaryExpr("!", sub1), UnaryExpr("-", sub2) when sub1 = sub2 -> Some(true)

+  | _ when e1 = e2 -> Some(true)

+  | _ -> None

+

+let rec __EvalSym resolverFunc ctx expr = 

+  match expr with

+  | IntLiteral(_)  -> expr

+  | BoolLiteral(_) -> expr

+  | ObjLiteral(_)  -> expr

+  | Star           -> expr //TODO: can we do better?

+  | VarLiteral(id) -> 

+      try 

+        let _,e = ctx |> List.find (fun (v,e) -> GetVarName v = id)

+        e

+      with 

+      | ex -> resolverFunc expr

+  | IdLiteral(_)   -> resolverFunc expr

+  | Dot(_)         -> resolverFunc expr

+  | SeqLength(e)   -> 

+      let e' = __EvalSym resolverFunc ctx e

+      match e' with

+      | SequenceExpr(elist) -> IntLiteral(List.length elist)

+      | _ -> SeqLength(e')

+  | SequenceExpr(elist) -> 

+      let elist' = elist |> List.fold (fun acc e -> __EvalSym resolverFunc ctx e :: acc) [] |> List.rev

+      SequenceExpr(elist')

+  | SetExpr(elist) -> 

+      let eset' = elist |> List.fold (fun acc e -> Set.add (__EvalSym resolverFunc ctx e) acc) Set.empty

+      SetExpr(Set.toList eset')

+  | SelectExpr(lst, idx) ->

+      let lst', idx' = __EvalSym resolverFunc ctx lst, __EvalSym resolverFunc ctx idx 

+      match lst', idx' with

+      | SequenceExpr(elist), IntLiteral(n) -> elist.[n] 

+      | _ -> SelectExpr(lst', idx')

+  | UpdateExpr(lst,idx,v) ->

+      let lst', idx', v' = __EvalSym resolverFunc ctx lst, __EvalSym resolverFunc ctx idx, __EvalSym resolverFunc ctx v

+      match lst', idx', v' with

+      | SequenceExpr(elist), IntLiteral(n), _ -> SequenceExpr(Utils.ListSet n v' elist)

+      | _ -> UpdateExpr(lst', idx', v')

+  | IteExpr(c, e1, e2) ->

+      let c' = __EvalSym resolverFunc ctx c

+      match c' with

+      | BoolLiteral(b) -> if b then __EvalSym resolverFunc ctx e1 else __EvalSym resolverFunc ctx e2

+      | _ -> IteExpr(c', __EvalSym resolverFunc ctx e1, __EvalSym resolverFunc ctx e2)

+  | BinaryExpr(p,op,e1,e2) ->

+      let e1' = lazy (__EvalSym resolverFunc ctx e1)

+      let e2' = lazy (__EvalSym resolverFunc ctx e2)

+      let recomposed = lazy (BinaryExpr(p, op, e1'.Force(), e2'.Force()))

+      match op with

+      | "=" ->

+          let e1'' = e1'.Force()

+          let e2'' = e2'.Force()

+          let eq = __CheckEqual e1'' e2''

+          match eq with

+          | Some(b) -> BoolLiteral(b)

+          | None -> recomposed.Force()

+      | "!=" -> 

+          let e1'' = e1'.Force()

+          let e2'' = e2'.Force()

+          let eq = __CheckEqual e1'' e2''

+          match eq with

+          | Some(b) -> BoolLiteral(not b)

+          | None -> recomposed.Force()

+      | "<" -> 

+          match e1'.Force(), e2'.Force() with

+          | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 < n2)

+          | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) < (List.length s2))

+          | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2))

+          | _ -> recomposed.Force()

+      | "<=" -> 

+          let e1'' = e1'.Force()

+          let e2'' = e2'.Force()

+          let eq = __CheckEqual e1'' e2''

+          match eq with

+          | Some(true) -> TrueLiteral

+          | _ -> match e1'', e2'' with

+                 | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 <= n2)

+                 | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) <= (List.length s2))

+                 | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2))

+                 | _ -> recomposed.Force()

+      | ">" -> 

+          match e1'.Force(), e2'.Force() with

+          | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 > n2)

+          | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) > (List.length s2))

+          | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2))

+          | _ -> recomposed.Force()

+      | ">=" -> 

+          let e1'' = e1'.Force()

+          let e2'' = e2'.Force()

+          let eq = __CheckEqual e1'' e2''

+          match eq with

+          | Some(true) -> TrueLiteral

+          | _ -> match e1'', e2'' with

+                 | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 >= n2)

+                 | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) >= (List.length s2))

+                 | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2))

+                 | _ -> recomposed.Force()

+      | "in" -> 

+          match e1'.Force(), e2'.Force() with

+          | _, SetExpr(s)       

+          | _, SequenceExpr(s)  -> BoolLiteral(Utils.ListContains (e1'.Force()) s)

+          | _ -> recomposed.Force()

+      | "!in" -> 

+          match e1'.Force(), e2'.Force() with

+          | _, SetExpr(s)       

+          | _, SequenceExpr(s)  -> BoolLiteral(not (Utils.ListContains (e1'.Force()) s))

+          | _ -> recomposed.Force()

+      | "+" -> 

+          let e1'' = e1'.Force();

+          let e2'' = e2'.Force();

+          match e1'', e2'' with

+          | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 + n2)

+          | SequenceExpr(l1), SequenceExpr(l2) -> SequenceExpr(List.append l1 l2)

+          | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.union (Set.ofList s1) (Set.ofList s2) |> Set.toList)

+          | SetExpr(s), _ -> SetExpr(Set.add e2'' (Set.ofList s) |> Set.toList)

+          | _, SetExpr(s) -> SetExpr(Set.add e1'' (Set.ofList s) |> Set.toList)

+          | _ -> recomposed.Force()

+      | "-" -> 

+          match e1'.Force(), e2'.Force() with

+          | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 - n2)

+          | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.difference (Set.ofList s1) (Set.ofList s2) |> Set.toList)

+          | _ -> recomposed.Force()

+      | "*" -> 

+          match e1'.Force(), e2'.Force() with

+          | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 * n2)

+          | _ -> recomposed.Force()

+      | "div" -> 

+          match e1'.Force(), e2'.Force() with

+          | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 / n2)

+          | _ -> recomposed.Force()

+      | "mod" -> 

+          match e1'.Force(), e2'.Force() with

+          | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 % n2)

+          | _ -> recomposed.Force()

+      | "&&" -> 

+          // shortcircuit

+          match e1'.Force() with

+          | BoolLiteral(false) -> BoolLiteral(false)

+          | _ ->

+              match e1'.Force(), e2'.Force() with

+              | BoolLiteral(false), _            -> BoolLiteral(false)

+              | _, BoolLiteral(false)            -> BoolLiteral(false)

+              | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 && b2)

+              | _ -> BinaryAnd (e1'.Force()) (e2'.Force())

+      | "||" -> 

+          // shortcircuit

+          match e1'.Force() with

+          | BoolLiteral(true) -> BoolLiteral(true)

+          | _ ->

+              match e1'.Force(), e2'.Force() with

+              | BoolLiteral(true), _             -> BoolLiteral(true)

+              | _, BoolLiteral(true)             -> BoolLiteral(true)

+              | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 || b2)

+              | _ -> BinaryOr (e1'.Force()) (e2'.Force())

+      | "==>" -> 

+          // shortcircuit

+          match e1'.Force() with

+          | BoolLiteral(false) -> BoolLiteral(true)

+          | _ ->

+              match e1'.Force(), e2'.Force() with

+              | BoolLiteral(false), _            -> BoolLiteral(true)

+              | _, BoolLiteral(true)             -> BoolLiteral(true)

+              | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral((not b1) || b2)

+              | _ -> BinaryImplies (e1'.Force()) (e2'.Force())

+      | "<==>" -> 

+          match e1'.Force(), e2'.Force() with

+          | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2)

+          | x, BoolLiteral(b)

+          | BoolLiteral(b), x -> if b then x else UnaryNot(x)

+          | _ -> recomposed.Force()

+      | _ -> recomposed.Force()

+  | UnaryExpr(op, e) ->

+      let e' = __EvalSym resolverFunc ctx e

+      let recomposed = UnaryExpr(op, e')

+      match op with

+      | "!" -> 

+          match e' with

+          | BoolLiteral(b) -> BoolLiteral(not b)

+          | _ -> recomposed

+      | "-" -> 

+          match e' with

+          | IntLiteral(n) -> IntLiteral(-n)

+          | _ -> recomposed

+      | _ -> recomposed

+  | ForallExpr(vars, e) -> 

+      let rec __ExhaustVar v restV vDomain = 

+        match vDomain with

+        | vv :: restD -> 

+            let newCtx = (v,vv) :: ctx

+            let e = __EvalSym resolverFunc newCtx (ForallExpr(restV, e))

+            let erest = __ExhaustVar v restV restD

+            __EvalSym resolverFunc ctx (BinaryAnd e erest)

+        | [] -> BoolLiteral(true)

+      match vars with

+      | v :: restV -> 

+          let vDom = GetVarDomain resolverFunc v e

+          __ExhaustVar v restV vDom

+      | [] -> __EvalSym resolverFunc ctx e

+and GetVarDomain resolverFunc var expr = 

+  //TODO: don't hardcode this!!!

+  let elems = __EvalSym resolverFunc [] (Dot(ObjLiteral("this"), "elems"))

+  match elems with 

+  | SetExpr(elist) -> elist

+  | _ -> failwith "this is bogus"

+

+let EvalSym resolverFunc expr = 

+  __EvalSym resolverFunc [] expr 

   

 //  ==========================================================

 /// Desugars a given expression so that all list constructors 

@@ -471,6 +573,7 @@ let rec Desugar expr =
   | BoolLiteral(_)  

   | IdLiteral(_)   

   | VarLiteral(_)        

+  | ObjLiteral(_)

   | Star                   

   | Dot(_)                 

   | SelectExpr(_) 

@@ -504,7 +607,7 @@ let rec Desugar expr =
             | _ -> be

         | _ -> be

       with

-        | EvalFailed as ex -> (* printfn "%O" (ex.StackTrace);  *) be

+        | EvalFailed(_) as ex -> (* printfn "%O" (ex.StackTrace);  *) be

 

 let rec DesugarLst exprLst = 

   match exprLst with

@@ -517,10 +620,12 @@ let ChangeThisReceiver receiver expr =
     | IntLiteral(_)

     | BoolLiteral(_)                   

     | Star                             

-    | VarLiteral(_)

-    | IdLiteral("null")                -> expr

-    | IdLiteral("this")                -> receiver

-    | IdLiteral(id)                    -> if Set.contains id locals then VarLiteral(id) else __ChangeThis locals (Dot(IdLiteral("this"), id))

+    | VarLiteral(_)                    -> expr

+    | ObjLiteral("this")               -> receiver

+    | ObjLiteral(_)                    -> expr

+    | IdLiteral("null")                -> failwith "should never happen anymore"   //TODO

+    | IdLiteral("this")                -> failwith "should never happen anymore"

+    | IdLiteral(id)                    -> if Set.contains id locals then VarLiteral(id) else __ChangeThis locals (Dot(ObjLiteral("this"), id))

     | Dot(e, id)                       -> Dot(__ChangeThis locals e, id)

     | ForallExpr(vars,e)               -> let newLocals = vars |> List.map (function Var(name,_) -> name) |> Set.ofList |> Set.union locals

                                           ForallExpr(vars, __ChangeThis newLocals e)   

@@ -544,7 +649,8 @@ let rec Rewrite rewriterFunc expr =
   | IntLiteral(_)

   | BoolLiteral(_)                   

   | Star      

-  | VarLiteral(_)                       

+  | VarLiteral(_) 

+  | ObjLiteral(_)                      

   | IdLiteral(_)                     -> match rewriterFunc expr with

                                         | Some(e) -> e

                                         | None -> expr

diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index f0e59d3b..5d7f8611 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -120,9 +120,27 @@ let PrintVarAssignments (heap,env,ctx) indent =
                       acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline

                    ) ""

 

-let PrintHeapCreationCode (heap,env,ctx) indent = 

-  (PrintAllocNewObjects (heap,env,ctx) indent) +

-  (PrintVarAssignments (heap,env,ctx) indent)

+let rec PrintHeapCreationCode sol indent =    

+  let idt = Indent indent

+  match sol with

+  | (c, (heap,env,ctx)) :: rest ->

+      if c = TrueLiteral then

+        (PrintAllocNewObjects (heap,env,ctx) indent) +

+        (PrintVarAssignments (heap,env,ctx) indent) +

+        newline + 

+        (PrintHeapCreationCode rest indent) 

+      else

+        if List.length rest > 0 then

+          idt + "if (" + (PrintExpr 0 c) + ") {" + newline +

+          (PrintAllocNewObjects (heap,env,ctx) (indent+2)) +

+          (PrintVarAssignments (heap,env,ctx) (indent+2)) +

+          idt + "} else {" + newline + 

+          (PrintHeapCreationCode rest (indent+2)) +

+          idt + "}" + newline

+        else 

+          (PrintAllocNewObjects (heap,env,ctx) indent) +

+          (PrintVarAssignments (heap,env,ctx) indent)

+  | [] -> ""

 

 let GenConstructorCode mthd body =

   let validExpr = IdLiteral("Valid()");

@@ -146,7 +164,7 @@ let PrintImplCode prog solutions methodsToPrintFunc =
   PrintDafnyCodeSkeleton prog (fun comp mthd ->

                                  if Utils.ListContains (comp,mthd) methods  then

                                    let mthdBody = match Map.tryFind (comp,mthd) solutions with

-                                                  | Some(heap,env,ctx) -> PrintHeapCreationCode (heap,env,ctx) 4

+                                                  | Some(sol) -> PrintHeapCreationCode sol 4

                                                   | _ -> "    //unable to synthesize" + newline

                                    (GenConstructorCode mthd mthdBody) + newline

                                  else

diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs
index 05f333d1..d1dc73fc 100644
--- a/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/DafnyPrinter.fs
@@ -14,12 +14,14 @@ let rec PrintType ty =
 
 let rec PrintExpr ctx expr =
   match expr with
-  | IntLiteral(n) -> sprintf "%d" n
-  | BoolLiteral(b) -> sprintf "%b" b
+  | IntLiteral(d)     -> sprintf "%d" d
+  | BoolLiteral(b)    -> sprintf "%b" b
+  | ObjLiteral(id)
   | VarLiteral(id)
   | IdLiteral(id) -> id
   | Star -> assert false; "" // I hope this won't happen
   | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id
+  | UnaryExpr(op,UnaryExpr(op2, e2))   -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))
   | UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e)
   | BinaryExpr(strength,op,e0,e1) ->
       let op =
@@ -44,6 +46,20 @@ let rec PrintExpr ctx expr =
       let closeParen = if needParens then ")" else ""
       sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen
 
+let rec PrintConst cst = 
+  match cst with 
+  | IntConst(v)        -> sprintf "%d" v
+  | BoolConst(b)       -> sprintf "%b" b
+  | VarConst(v)        -> sprintf "%s" v
+  | SetConst(cset)     -> sprintf "{%s}" (PrintSep ", " (fun c -> PrintConst c) (Set.toList cset))
+  | SeqConst(cseq)     -> sprintf "[%s]" (PrintSep ", " (fun c -> PrintConst c) cseq)
+  | NullConst          -> "null"
+  | NoneConst          -> "<none>"
+  | ThisConst(_,_)     -> "this"
+  | ExprConst(e)       -> PrintExpr 0 e
+  | NewObj(name,_)     -> PrintGenSym name
+  | Unresolved(name)   -> sprintf "Unresolved(%s)" name
+
 let PrintTypeParams typeParams = 
   match typeParams with
   | [] -> ""
diff --git a/Jennisys/Jennisys.fs b/Jennisys/Jennisys.fs
index ca1ab1ad..d0a47fe1 100644
--- a/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys.fs
@@ -17,7 +17,6 @@ open TypeChecker
 open Analyzer
 
 let readAndProcess (filename: string) =
-  try
     printfn "// Jennisys, Copyright (c) 2011, Microsoft."
     // lex
     let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader
@@ -26,22 +25,18 @@ let readAndProcess (filename: string) =
                        pos_fname=if filename = null then "stdin" else filename; 
                        pos_cnum=0;
                        pos_lnum=1 }
-    try
+//    try
       // parse
-      let sprog = Parser.start Lexer.tokenize lexbuf
-      match TypeCheck sprog with
-      | None -> ()  // errors have already been reported
-      | Some(prog) ->
-          Analyze prog filename
-    with
-      | ex ->
-          let pos = lexbuf.EndPos
-          printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message
-          printfn "%s" (ex.StackTrace.ToString())
-  with
-    | ex ->
-        printfn "Unhandled Exception: %s" ex.Message
-        printfn "%s" (ex.StackTrace.ToString())
+    let sprog = Parser.start Lexer.tokenize lexbuf
+    match TypeCheck sprog with
+    | None -> ()  // errors have already been reported
+    | Some(prog) ->
+        Analyze prog filename
+//    with
+//      | ex ->
+//          let pos = lexbuf.EndPos
+//          printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message
+//          printfn "%O" ex.StackTrace
 
 try 
   let args = Environment.GetCommandLineArgs()
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index 832176fd..5e1bea61 100644
--- a/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

     <DocumentationFile>bin\Debug\Language.XML</DocumentationFile>

-    <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.Double /noCheckUnifs</StartArguments>

+    <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Number.jen /method:Number.Abs /checkUnifs</StartArguments>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">

     <DebugType>pdbonly</DebugType>

diff --git a/Jennisys/Logger.fs b/Jennisys/Logger.fs
index 2801354d..09b576fd 100644
--- a/Jennisys/Logger.fs
+++ b/Jennisys/Logger.fs
@@ -16,7 +16,7 @@ let _WARN = 40
 let _ERROR = 20

 let _NONE = 0

 

-let logLevel = _ALL

+let logLevel = _DEBUG

 

 let Log level msg =

   if logLevel >= level then

diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs
index 4a1487ce..a03f7213 100644
--- a/Jennisys/Options.fs
+++ b/Jennisys/Options.fs
@@ -20,7 +20,7 @@ let defaultConfig: Config = {
   inputFilename     = "";

   methodToSynth     = "*";

   verifySolutions   = true;

-  checkUnifications = true;

+  checkUnifications = false;

   timeout           = 0;

 }

 

diff --git a/Jennisys/Parser.fsy b/Jennisys/Parser.fsy
index 15b27ddb..c683e84c 100644
--- a/Jennisys/Parser.fsy
+++ b/Jennisys/Parser.fsy
@@ -69,11 +69,11 @@ Signature:
     | LPAREN VarDeclList RPAREN RETURNS LPAREN VarDeclList RPAREN  { Sig($2, $6) }

 

 Pre:

-    |                           { IdLiteral "true" }

+    |                           { TrueLiteral }

     | REQUIRES Expr Pre         { BinaryAnd $2 $3 }

 

 Post: 

-    |                           { IdLiteral "true" }

+  |                           { TrueLiteral }

 	| ENSURES Expr Post         { BinaryAnd $2 $3 }

 

 StmtList:

@@ -94,7 +94,7 @@ Member:
 	  | INVARIANT ExprList                     { Invariant($2) }

 

 FrameMembers:

-    |                                        { [], [], IdLiteral("true") }

+    |                                        { [], [], TrueLiteral }

     | VAR VarDecl FrameMembers               { match $3 with (vv,fr,inv) -> $2 :: vv, fr, inv }

     | FRAME FrameMembers                     { $2 }

     | FRAME FramePartitionList FrameMembers  { match $3 with (vv,fr,inv) -> vv, List.append $2 fr, inv }

@@ -180,7 +180,12 @@ Expr90:
 

 Expr100:

   | INTEGER                                  { IntLiteral($1) }

-  | ID                                       { IdLiteral($1) }

+  | ID                                       { if $1 = "this" then

+                                                 ObjLiteral("this")

+                                               elif $1 = "null" then

+                                                 ObjLiteral("null")

+                                               else

+                                                 IdLiteral($1) }

   | Expr100 DOT ID                           { Dot($1, $3) }

   | Expr100 LBRACKET StarExpr RBRACKET       { SelectExpr($1, $3) }

   | Expr100 LBRACKET Expr GETS Expr RBRACKET { UpdateExpr($1, $3, $5) }

diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs
index 54d0dc43..e051492f 100644
--- a/Jennisys/Printer.fs
+++ b/Jennisys/Printer.fs
@@ -34,12 +34,14 @@ let PrintVarName vd =
 
 let rec PrintExpr ctx expr =
   match expr with
-  | IntLiteral(n)     -> sprintf "%d" n
+  | IntLiteral(d)     -> sprintf "%d" d
   | BoolLiteral(b)    -> sprintf "%b" b
+  | ObjLiteral(id)
   | VarLiteral(id) 
   | IdLiteral(id)     -> id
   | Star              -> "*"
   | Dot(e,id)         -> sprintf "%s.%s" (PrintExpr 100 e) id
+  | UnaryExpr(op,UnaryExpr(op2, e2))   -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))
   | UnaryExpr(op,e)   -> sprintf "%s%s" op (PrintExpr 90 e)
   | BinaryExpr(strength,op,e0,e1) ->
       let needParens = strength <= ctx
@@ -58,6 +60,20 @@ let rec PrintExpr ctx expr =
       let closeParen = if needParens then ")" else ""
       sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen
 
+let rec PrintConst cst = 
+  match cst with 
+  | IntConst(v)        -> sprintf "%d" v
+  | BoolConst(b)       -> sprintf "%b" b
+  | VarConst(v)        -> sprintf "%s" v
+  | SetConst(cset)     -> sprintf "{%s}" (PrintSep " " (fun c -> PrintConst c) (Set.toList cset))
+  | SeqConst(cseq)     -> sprintf "[%s]" (PrintSep " " (fun c -> PrintConst c) cseq)
+  | NullConst          -> "null"
+  | NoneConst          -> "<none>"
+  | ThisConst(_,_)     -> "this"
+  | ExprConst(e)       -> PrintExpr 0 e
+  | NewObj(name,_)     -> PrintGenSym name
+  | Unresolved(name)   -> sprintf "Unresolved(%s)" name
+
 let PrintSig signature =
   match signature with
   | Sig(ins, outs) ->
@@ -115,24 +131,20 @@ let PrintDecl d =
   | Code(id,typeParams) ->
       (PrintTopLevelDeclHeader "code" id typeParams) + "}" + newline
 
+let PrintMethodSignFull indent m = 
+  let idt = Indent indent
+  let __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep newline (fun e -> pfix + (PrintExpr 0 e) + ";")

+  match m with

+  | Method(methodName, sgn, pre, post, isConstr) ->  

+      let mc = if isConstr then "constructor" else "method"

+      let preStr = (__PrintPrePost (idt + "  requires ") pre)

+      let postStr = (__PrintPrePost (idt + "  ensures ") post)

+      idt + mc + " " + methodName + (PrintSig sgn) + newline +

+      preStr + (if preStr = "" then "" else newline) +

+      postStr

+      
+  | _ -> failwithf "not a method: %O" m
+
 let Print prog =
   match prog with
   | SProgram(decls) -> List.fold (fun acc d -> acc + (PrintDecl d)) "" decls
-
-let rec PrintConst cst = 
-  match cst with 
-  | IntConst(v)        -> sprintf "%d" v
-  | BoolConst(b)       -> sprintf "%b" b
-  | SetConst(cset)     -> sprintf "{%s}" (PrintSep ", " (fun c -> PrintConst c) (Set.toList cset))
-  | SeqConst(cseq)     -> 
-      let seqCont = cseq |> List.fold (fun acc c ->
-                                         let sep = if acc = "" then "" else ", "
-                                         acc + sep + (PrintConst c)                                         
-                                      ) ""
-      sprintf "[%s]" seqCont
-  | NullConst          -> "null"
-  | NoneConst          -> "<none>"
-  | ThisConst(_,_)     -> "this"
-  | NewObj(name,_)     -> PrintGenSym name
-  | ExprConst(e)       -> PrintExpr 0 e
-  | Unresolved(name)   -> sprintf "Unresolved(%s)" name
\ No newline at end of file
diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs
index f87ce5bd..af49e51a 100644
--- a/Jennisys/Resolver.fs
+++ b/Jennisys/Resolver.fs
@@ -70,31 +70,22 @@ let Resolve (env,ctx) cst =
 let Eval (heap,env,ctx) resolveVars expr = 

   let rec __EvalResolver expr = 

     match expr with

-    | VarLiteral(id) when not resolveVars -> ExprConst(expr)

-    | IdLiteral("this") -> GetThisLoc env

+    | VarLiteral(id) when not resolveVars -> VarConst(id)

+    | ObjLiteral("this") -> GetThisLoc env

+    | ObjLiteral("null") -> NullConst

+    | IdLiteral("this") | IdLiteral("null") -> failwith "should never happen anymore" //TODO

     | VarLiteral(id)

     | IdLiteral(id) ->

         match TryResolve (env,ctx) (Unresolved(id)) with 

-        | Unresolved(_) -> __EvalResolver (Dot(IdLiteral("this"), id))

+        | Unresolved(_) -> __EvalResolver (Dot(ObjLiteral("this"), id))

         | _ as c -> c

     | Dot(e, str) -> 

         let discr = __EvalResolver e

         let h2 = Map.filter (fun (loc,Var(fldName,_)) v -> loc = discr && fldName = str) heap |> Map.toList

         match h2 with

         | ((_,_),x) :: [] -> x

-        | _ :: _ -> failwithf "can't evaluate expression deterministically: %s.%s resolves to multiple locations." (PrintConst discr) str

-        | [] -> failwithf "can't find value for %s.%s" (PrintConst discr) str

-    | _ -> failwith "NOT IMPLEMENTED YET"

-//  try 

+        | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" (PrintConst discr) str))

+        | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" (PrintConst discr) str))

+    | _ -> failwith ("NOT IMPLEMENTED YET: " + (PrintExpr 0 expr))

+  (* --- function body starts here --- *)

   EvalSym (fun e -> __EvalResolver e |> Resolve (env,ctx) |> Const2Expr) expr

-//                                     ccc |> Const2Expr

-//                                     match ccc with

-//                                     | ExprConst(eee) -> match Eval (heap,env,ctx) eee with

-//                                                         | Some(c) -> c

-//                                                         | None -> ccc

-//                                     | _ -> ccc

-//                                  ) expr

-    

-    //Some(TryResolve (env,ctx) unresolvedConst)

-//  with

-//    ex -> None
\ No newline at end of file
diff --git a/Jennisys/TypeChecker.fs b/Jennisys/TypeChecker.fs
index 377082d9..bf012a11 100644
--- a/Jennisys/TypeChecker.fs
+++ b/Jennisys/TypeChecker.fs
@@ -12,7 +12,7 @@ let GetClass name decls =
 let GetModel name decls =

   match decls |> List.tryFind (function Model(n,_,_,_,_) when n = name -> true | _ -> false) with

   | Some(m) -> m

-  | None -> Model(name,[],[],[],IdLiteral("true"))

+  | None -> Model(name,[],[],[],BoolLiteral(true))

 

 let GetCode name decls =

   match decls |> List.tryFind (function Code(n,_) when n = name -> true | _ -> false) with

diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs
index b7db5706..886d5868 100644
--- a/Jennisys/Utils.fs
+++ b/Jennisys/Utils.fs
@@ -119,6 +119,16 @@ let rec GenList n e =
   else

     e :: (GenList (n-1) e)

 

+//  =======================================

+/// ensures: forall i :: 0 <= i < |lst| ==> 

+///            if lst[i] = oldElem then

+///              ret[i] = newElem

+///            else

+///              ret[i] = lst[i]

+//  =======================================

+let ListReplace oldElem newElem lst = 

+  lst |> List.choose (fun e -> if e = oldElem then Some(newElem) else Some(e))

+

 //  ==========================

 /// ensures: ret = elem in lst

 //  ==========================

diff --git a/Jennisys/examples/Number.jen b/Jennisys/examples/Number.jen
new file mode 100644
index 00000000..75417168
--- /dev/null
+++ b/Jennisys/examples/Number.jen
@@ -0,0 +1,40 @@
+class Number { 
+  var num: int
+ 
+  constructor Init(p: int)
+    ensures num = p
+
+  constructor Double(p: int)
+    ensures num = 2*p
+
+  constructor Sum(a: int, b: int)
+    ensures num = a + b
+
+  constructor Min2(a: int, b: int)
+    ensures a < b ==> num = a
+    ensures a >= b ==> num = b
+
+  constructor Min22(a: int, b: int)
+    ensures num in {a b}
+    ensures num <= a && num <= b
+
+  constructor Min3(a: int, b: int, c: int)
+    ensures num in {a b c}
+    ensures num <= a && num <= b && num <= c
+
+ constructor MinSum(a: int, b: int, c: int)
+    ensures num in {a+b a+c b+c}
+    ensures num <= a+b && num <= b+c && num <= a+c
+
+ constructor Min4(a: int, b: int, c: int, d: int)
+    ensures num in {a b c d}
+    ensures num <= a && num <= b && num <= c && num <= d
+
+  constructor Abs(a: int) 
+    ensures a < 0 ==> num = -a
+    ensures a >= 0 ==> num = a
+}
+
+model Number {
+
+}
\ No newline at end of file