39 files changed, 1763 insertions, 1278 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 742fd4e4..fef8fe1f 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -558,6 +558,11 @@ axiom (forall x: int, h: HeapType ::
 axiom (forall r: ref, h: HeapType ::

   { GenericAlloc($Box(r), h) }

   $IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h));

+// boxes in the heap

+axiom (forall r: ref, f: Field BoxType, h: HeapType ::

+  { GenericAlloc(read(h, r, f), h) }

+  $IsGoodHeap(h) && r != null && read(h, r, alloc) ==>

+  GenericAlloc(read(h, r, f), h));

 

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

 // -- Arrays -----------------------------------------------------

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index afab0c1f..fa8ea6da 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -74,18 +74,18 @@ namespace Microsoft.Dafny {
         }

         int indent = 0;

         if (!m.IsDefaultModule) {

-          wr.WriteLine("namespace @{0} {{", m.Name);

+          wr.WriteLine("namespace @{0} {{", m.CompileName);

           indent += IndentAmount;

         }

         foreach (TopLevelDecl d in m.TopLevelDecls) {

           wr.WriteLine();

           if (d is ArbitraryTypeDecl) {

             var at = (ArbitraryTypeDecl)d;

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

+            Error("Arbitrary type ('{0}') cannot be compiled", at.CompileName);

           } else if (d is DatatypeDecl) {

             var dt = (DatatypeDecl)d;

             Indent(indent);

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

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

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

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

             }

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

             ClassDecl cl = (ClassDecl)d;

             Indent(indent);

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

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

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

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

             }

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

         }

         if (!m.IsDefaultModule) {

-          wr.WriteLine("}} // end of namespace {0}", m.Name);

+          wr.WriteLine("}} // end of namespace {0}", m.CompileName);

         }

       }

     }

@@ -200,18 +200,18 @@ namespace Microsoft.Dafny {
         //   public Base_Dt<T> Get() { return c(); }

         // }

         Indent(indent);

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

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

         int ind = indent + IndentAmount;

         Indent(ind);

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

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

         Indent(ind);

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

         Indent(ind);

         wr.WriteLine("Computer c;");

         Indent(ind);

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

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

         Indent(ind);

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

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

         Indent(indent);

         wr.WriteLine("}");

       }

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

         Indent(indent);

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

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

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

         int ind = indent + IndentAmount;

 

         int i = 0;

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

         if (dt is IndDatatypeDecl) {

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

-          string nm = (dt.Module.IsDefaultModule ? "" : dt.Module.Name + ".") + dt.Name + "." + ctor.Name;

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

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

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

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

@@ -345,13 +345,13 @@ namespace Microsoft.Dafny {
       //   public override int GetHashCode() { return _D.GetHashCode(); }

       //   public override string ToString() { return _D.ToString(); }  // only for inductive datatypes

       //

-      //   public bool _Ctor0 { get { return _D is Dt_Ctor0; } }

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

       //   ...

       //

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

       //   ...

       // }

-      string DtT = dt.Name;

+      string DtT = dt.CompileName;

       string DtT_TypeArgs = "";

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

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

@@ -376,9 +376,9 @@ namespace Microsoft.Dafny {
       if (dt is CoDatatypeDecl) {

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

         Indent(ind + 2 * IndentAmount);

-        wr.WriteLine("}} else if (d is {0}__Lazy{1}) {{", dt.Name, typeParams);

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

         Indent(ind + 3 * IndentAmount);

-        wr.WriteLine("d = (({0}__Lazy{1})d).Get();", dt.Name, typeParams);

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

       }

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

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

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

 

       Indent(ind);

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

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

 

       Indent(ind);

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

@@ -440,9 +440,9 @@ namespace Microsoft.Dafny {
 

       // query properties

       foreach (var ctor in dt.Ctors) {

-        //   public bool _Ctor0 { get { return _D is Dt_Ctor0; } }

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

         Indent(ind);

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

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

       }

 

       // destructors

@@ -451,7 +451,7 @@ namespace Microsoft.Dafny {
           if (!arg.IsGhost && arg.HasName) {

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

             Indent(ind);

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

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

           }

         }

       }

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

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

 

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

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

     }

 

     string DtCtorName(DatatypeCtor ctor) {

       Contract.Requires(ctor != null);

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

 

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

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

     }

 

     string DtCtorName(DatatypeCtor ctor, List<TypeParameter> typeParams) {

@@ -539,7 +539,7 @@ namespace Microsoft.Dafny {
           Field f = (Field)member;

           if (!f.IsGhost) {

             Indent(indent);

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

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

           }

 

         } else if (member is Function) {

@@ -550,7 +550,7 @@ namespace Microsoft.Dafny {
             Error("Function {0} has no body", f.FullName);

           } else {

             Indent(indent);

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

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

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

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

             }

@@ -565,7 +565,7 @@ namespace Microsoft.Dafny {
           Method m = (Method)member;

           if (!m.IsGhost) {

             Indent(indent);

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

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

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

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

             }

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

               if (!p.IsGhost) {

                 Indent(indent + IndentAmount);

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

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

               }

             }

             if (m.Body == null) {

@@ -595,7 +595,7 @@ namespace Microsoft.Dafny {
               wr.WriteLine("public static void Main(string[] args) {");

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

               Indent(indent + IndentAmount);

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

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

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

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

                 wr.Write("<");

@@ -623,7 +623,7 @@ namespace Microsoft.Dafny {
       if (body is MatchExpr) {

         MatchExpr me = (MatchExpr)body;

         // Type source = e;

-        // if (source._Ctor0) {

+        // if (source.is_Ctor0) {

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

         //   ...

         //   return Body0;

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

         foreach (var v in e.Vars) {

           Indent(indent);

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

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

         }

       }

       foreach (var ee in expr.SubExpressions) {

@@ -724,7 +724,7 @@ namespace Microsoft.Dafny {
         return name + "]";

       } else if (type is UserDefinedType) {

         UserDefinedType udt = (UserDefinedType)type;

-        string s = "@" + udt.FullName;

+        string s = "@" + udt.FullCompileName;

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

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

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

@@ -782,7 +782,7 @@ namespace Microsoft.Dafny {
       string s = "";

       string sep = "";

       foreach (TypeParameter tp in targs) {

-        s += sep + "@" + tp.Name;

+        s += sep + "@" + tp.CompileName;

         sep = ",";

       }

       return s;

@@ -813,14 +813,14 @@ namespace Microsoft.Dafny {
         return string.Format("({0})null", TypeName(type));

       } else if (type.IsDatatype) {

         UserDefinedType udt = (UserDefinedType)type;

-        string s = "@" + udt.Name;

+        string s = "@" + udt.FullCompileName;

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

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

         }

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

       } else if (type.IsTypeParameter) {

         UserDefinedType udt = (UserDefinedType)type;

-        return "default(@" + udt.Name + ")";

+        return "default(@" + udt.FullCompileName + ")";

       } else if (type is SetType) {

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

       } else if (type is MultiSetType) {

@@ -841,7 +841,10 @@ namespace Microsoft.Dafny {
       if (stmt is AssumeStmt) {

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

       } else if (stmt is AssignSuchThatStmt) {

-        Error("an assign-such-that statement cannot be compiled (line {0})", stmt.Tok.line);

+        var s = (AssignSuchThatStmt)stmt;

+        if (s.AssumeToken != null) {

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

+        }

       } else {

         foreach (var ss in stmt.SubStatements) {

           CheckHasNoAssumes(ss);

@@ -882,7 +885,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is BreakStmt) {

         var s = (BreakStmt)stmt;

         Indent(indent);

-        wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.UniqueId);

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

       } else if (stmt is ReturnStmt) {

         var s = (ReturnStmt)stmt;

         if (s.hiddenUpdate != null)

@@ -925,6 +928,16 @@ namespace Microsoft.Dafny {
         Contract.Assert(!(s.Lhs is SeqSelectExpr) || ((SeqSelectExpr)s.Lhs).SelectOne);  // multi-element array assignments are not allowed

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

 

+      } else if (stmt is AssignSuchThatStmt) {

+        var s = (AssignSuchThatStmt)stmt;

+        foreach (var lhs in s.Lhss) {

+          // assigning to a local ghost variable or to a ghost field is okay

+          if (!AssignStmt.LhsIsToGhost(lhs)) {

+            Error("compiling an assign-such-that statement with a non-ghost left-hand side is currently not supported (line {0})", stmt.Tok.line);

+            break;  // no need to say more

+          }

+        }

+

       } else if (stmt is VarDecl) {

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

 

@@ -1099,7 +1112,7 @@ namespace Microsoft.Dafny {
 

         // declare and construct "ingredients"

         Indent(indent);

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

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

 

         var n = s.BoundVars.Count;

         Contract.Assert(s.Bounds.Count == n);

@@ -1109,29 +1122,29 @@ namespace Microsoft.Dafny {
           var bv = s.BoundVars[i];

           if (bound is QuantifierExpr.BoolBoundedPool) {

             Indent(ind);

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

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

           } else if (bound is QuantifierExpr.IntBoundedPool) {

             var b = (QuantifierExpr.IntBoundedPool)bound;

             SpillLetVariableDecls(b.LowerBound, ind);

             SpillLetVariableDecls(b.UpperBound, ind);

             Indent(ind);

-            wr.Write("for (var @{0} = ", bv.Name);

+            wr.Write("for (var @{0} = ", bv.CompileName);

             TrExpr(b.LowerBound);

-            wr.Write("; @{0} < ", bv.Name);

+            wr.Write("; @{0} < ", bv.CompileName);

             TrExpr(b.UpperBound);

-            wr.Write("; @{0}++) {{ ", bv.Name);

+            wr.Write("; @{0}++) {{ ", bv.CompileName);

           } else if (bound is QuantifierExpr.SetBoundedPool) {

             var b = (QuantifierExpr.SetBoundedPool)bound;

             SpillLetVariableDecls(b.Set, ind);

             Indent(ind);

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

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

             TrExpr(b.Set);

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

           } else if (bound is QuantifierExpr.SeqBoundedPool) {

             var b = (QuantifierExpr.SeqBoundedPool)bound;

             SpillLetVariableDecls(b.Seq, ind);

             Indent(ind);

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

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

             TrExpr(b.Seq);

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

           } else {

@@ -1213,7 +1226,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         // Type source = e;

-        // if (source._Ctor0) {

+        // if (source.is_Ctor0) {

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

         //   ...

         //   Body0;

@@ -1258,7 +1271,7 @@ namespace Microsoft.Dafny {
       SpillLetVariableDecls(lhs, indent);

       if (lhs is IdentifierExpr) {

         var ll = (IdentifierExpr)lhs;

-        return "@" + ll.Var.Name;

+        return "@" + ll.Var.CompileName;

       } else if (lhs is FieldSelectExpr) {

         var ll = (FieldSelectExpr)lhs;

         string obj = "_obj" + tmpVarCount;

@@ -1267,7 +1280,7 @@ namespace Microsoft.Dafny {
         wr.Write("var {0} = ", obj);

         TrExpr(ll.Obj);

         wr.WriteLine(";");

-        return string.Format("{0}.@{1}", obj, ll.Field.Name);

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

       } else if (lhs is SeqSelectExpr) {

         var ll = (SeqSelectExpr)lhs;

         string arr = "_arr" + tmpVarCount;

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

         TrParenExpr(s.Receiver);

       }

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

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

 

       string sep = "";

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

@@ -1462,7 +1475,7 @@ namespace Microsoft.Dafny {
         TrStmt(ss, indent + IndentAmount);

         if (ss.Labels != null) {

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

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

+          wr.WriteLine("after_{0}: ;", ss.Labels.Data.UniqueId);

         }

       }

     }

@@ -1475,7 +1488,7 @@ namespace Microsoft.Dafny {
       }

 

       Indent(indent);

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

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

       if (alwaysInitialize) {

         // produce a default value

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

@@ -1489,7 +1502,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(sourceType != null);

       Contract.Requires(ctor != null);

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

-      // if (source._Ctor0) {

+      // if (source.is_Ctor0) {

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

       //   ...

       Indent(indent);

@@ -1497,7 +1510,7 @@ namespace Microsoft.Dafny {
       if (caseIndex == caseCount - 1) {

         wr.Write("true");

       } else {

-        wr.Write("{0}._{1}", source, ctor.Name);

+        wr.Write("{0}.is_{1}", source, ctor.CompileName);

       }

       wr.WriteLine(") {");

 

@@ -1509,7 +1522,7 @@ namespace Microsoft.Dafny {
           // FormalType f0 = ((Dt_Ctor0)source._D).a0;

           Indent(indent + IndentAmount);

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

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

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

           k++;

         }

       }

@@ -1599,7 +1612,7 @@ namespace Microsoft.Dafny {
 

       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

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

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

 

       } else if (expr is SetDisplayExpr) {

         SetDisplayExpr e = (SetDisplayExpr)expr;

@@ -1634,7 +1647,7 @@ namespace Microsoft.Dafny {
           wr.Write(sf.PostString);

         } else {

           TrParenExpr(e.Obj);

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

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

         }

 

       } else if (expr is SeqSelectExpr) {

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

             } else {

               TrParenExpr(e.E);

-              wr.Write(".Length");


+              wr.Write(".Length");

             }

             break;

           default:

@@ -1827,6 +1840,11 @@ namespace Microsoft.Dafny {
             Type t = cce.NonNull(e.E0.Type);

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

               callString = "Equals";

+            } else if (t.IsRefType) {

+              // Dafny's type rules are slightly different C#, so we may need a cast here.

+              // For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some

+              // type parameter.

+              opString = "== (object)";

             } else {

               opString = "==";

             }

@@ -1837,6 +1855,11 @@ namespace Microsoft.Dafny {
             if (t.IsDatatype || t.IsTypeParameter) {

               preOpString = "!";

               callString = "Equals";

+            } else if (t.IsRefType) {

+              // Dafny's type rules are slightly different C#, so we may need a cast here.

+              // For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some

+              // type parameter.

+              opString = "!= (object)";

             } else {

               opString = "!=";

             }

@@ -1969,7 +1992,7 @@ namespace Microsoft.Dafny {
         // preceded by the declaration of x.

         Contract.Assert(e.Vars.Count == e.RHSs.Count);  // checked by resolution

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

-          wr.Write("Dafny.Helpers.ExpressionSequence(@{0} = ", e.Vars[i].Name);

+          wr.Write("Dafny.Helpers.ExpressionSequence(@{0} = ", e.Vars[i].CompileName);

           TrExpr(e.RHSs[i]);

           wr.Write(", ");

         }

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

           }

           wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");

-          wr.Write("@{0} => ", bv.Name);

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

         }

         TrExpr(e.LogicalBody());

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

@@ -2050,27 +2073,27 @@ namespace Microsoft.Dafny {
           var bound = e.Bounds[i];

           var bv = e.BoundVars[i];

           if (bound is QuantifierExpr.BoolBoundedPool) {

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

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

           } else if (bound is QuantifierExpr.IntBoundedPool) {

             var b = (QuantifierExpr.IntBoundedPool)bound;

-            wr.Write("for (var @{0} = ", bv.Name);

+            wr.Write("for (var @{0} = ", bv.CompileName);

             TrExpr(b.LowerBound);

-            wr.Write("; @{0} < ", bv.Name);

+            wr.Write("; @{0} < ", bv.CompileName);

             TrExpr(b.UpperBound);

-            wr.Write("; @{0}++) {{ ", bv.Name);

+            wr.Write("; @{0}++) {{ ", bv.CompileName);

           } else if (bound is QuantifierExpr.SetBoundedPool) {

             var b = (QuantifierExpr.SetBoundedPool)bound;

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

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

             TrExpr(b.Set);

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

           } else if (bound is QuantifierExpr.MapBoundedPool) {

             var b = (QuantifierExpr.MapBoundedPool)bound;

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

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

             TrExpr(b.Map);

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

           } else if (bound is QuantifierExpr.SeqBoundedPool) {

             var b = (QuantifierExpr.SeqBoundedPool)bound;

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

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

             TrExpr(b.Seq);

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

           } else {

@@ -2116,27 +2139,27 @@ namespace Microsoft.Dafny {
         var bound = e.Bounds[0];

         var bv = e.BoundVars[0];

         if (bound is QuantifierExpr.BoolBoundedPool) {

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

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

         } else if (bound is QuantifierExpr.IntBoundedPool) {

           var b = (QuantifierExpr.IntBoundedPool)bound;

-          wr.Write("for (var @{0} = ", bv.Name);

+          wr.Write("for (var @{0} = ", bv.CompileName);

           TrExpr(b.LowerBound);

-          wr.Write("; @{0} < ", bv.Name);

+          wr.Write("; @{0} < ", bv.CompileName);

           TrExpr(b.UpperBound);

-          wr.Write("; @{0}++) {{ ", bv.Name);

+          wr.Write("; @{0}++) {{ ", bv.CompileName);

         } else if (bound is QuantifierExpr.SetBoundedPool) {

           var b = (QuantifierExpr.SetBoundedPool)bound;

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

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

           TrExpr(b.Set);

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

         } else if (bound is QuantifierExpr.MapBoundedPool) {

           var b = (QuantifierExpr.MapBoundedPool)bound;

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

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

           TrExpr(b.Map);

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

         } else if (bound is QuantifierExpr.SeqBoundedPool) {

           var b = (QuantifierExpr.SeqBoundedPool)bound;

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

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

           TrExpr(b.Seq);

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

         } else {

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

         TrExpr(e.Range);

         wr.Write(") { ");

-        wr.Write("_coll.Add(new Dafny.Pair<{0},{1}>(@{2},", domtypeName, rantypeName, bv.Name);

+        wr.Write("_coll.Add(new Dafny.Pair<{0},{1}>(@{2},", domtypeName, rantypeName, bv.CompileName);

         TrExpr(e.Term);

         wr.Write(")); }");

         wr.Write("}");

@@ -2186,7 +2209,7 @@ namespace Microsoft.Dafny {
         tr(e.Receiver);

         twr.Write(")");

       }

-      twr.Write(".@{0}", f.Name);

+      twr.Write(".@{0}", f.CompileName);

       twr.Write("(");

       string sep = "";

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

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 97da97e3..13f6c245 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -24,7 +24,6 @@ static int anonymousIds = 0;
 struct MemberModifiers {

   public bool IsGhost;

   public bool IsStatic;

-  public bool IsUnlimited;

 }

 // helper routine for parsing call statements

 ///<summary>

@@ -226,7 +225,6 @@ ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool isAlreadyGhost, bool allowC
   .)

   { "ghost"                                (. mmod.IsGhost = true; .)

   | "static"                               (. mmod.IsStatic = true; .)

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

   }

   ( FieldDecl<mmod, mm>

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

@@ -281,8 +279,7 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
   .)

   SYNC

   "var"

-  (. if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }

-     if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }

+  (. if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }

   .)

   { Attribute<ref attrs> }

   IdentType<out id, out ty>                         (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)

@@ -396,8 +393,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
                                        }

                                     .)

   )

-  (. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }

-     if (isConstructor) {

+  (. if (isConstructor) {

        if (mmod.IsGhost) {

          SemErr(t, "constructors cannot be declared 'ghost'");

        }

@@ -503,7 +499,7 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
     GenericInstantiation<gt>        (. if (gt.Count != 2) {

                                          SemErr("map type expects exactly two type arguments");

                                        }

-                                       ty = new MapType(gt[0], gt[1]);

+                                       else { ty = new MapType(gt[0], gt[1]); }

                                     .)

   | ReferenceType<out tok, out ty>

   )

@@ -511,6 +507,7 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ 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*/

+     IToken moduleName = null;

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

   .)

   ( "object"                        (. tok = t;  ty = new ObjectType(); .)

@@ -525,7 +522,10 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
                                        ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);

                                     .)

   | Ident<out tok>                  (. gt = new List<Type/*!*/>(); .)

-    [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt); .)

+    [                               (. moduleName = tok; .)

+      "." Ident<out tok>

+    ]

+    [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt, moduleName); .)

   )

   .

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

@@ -596,10 +596,10 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   [ FunctionBody<out body, out bodyStart, out bodyEnd>

   ]

   (. if (isPredicate) {

-        f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals,

+        f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

                           reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs, signatureOmitted);

      } else {

-        f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals, returnType,

+        f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,

                          reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureOmitted);

      }

      f.BodyStartTok = bodyStart;

@@ -691,7 +691,7 @@ OneStmt<out Statement/*!*/ s>
   | ParallelStmt<out s>

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

     Ident<out id> ":"

-    OneStmt<out s>                     (. s.Labels = new LabelNode(x, id.val, s.Labels); .)

+    OneStmt<out s>                     (. s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); .)

   | "break"                            (. x = t; breakCount = 1; label = null; .)

     ( Ident<out id>                    (. label = id.val; .)

     | { "break"                        (. breakCount++; .)

@@ -725,6 +725,7 @@ UpdateStmt<out Statement/*!*/ s>
      Expression lhs0;

      IToken x;

      Attributes attrs = null;

+     IToken suchThatAssume = null;

      Expression suchThat = null;

   .)

   Lhs<out e>                       (. x = e.tok; .)

@@ -738,13 +739,15 @@ UpdateStmt<out Statement/*!*/ s>
       { "," Rhs<out r, lhs0>       (. rhss.Add(r); .)

       }

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

+      [ "assume"                   (. suchThatAssume = t; .)

+      ]

       Expression<out suchThat>

     )

     ";"

   | ":"                            (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)

   )

   (. if (suchThat != null) {

-       s = new AssignSuchThatStmt(x, lhss, suchThat);

+       s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);

      } else {

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

      }

@@ -769,8 +772,23 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
     | "." Ident<out x>

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

         [ Expressions<args> ]

-      ")"                              (. initCall = new CallStmt(x, new List<Expression>(),

-                                                                  receiverForInitCall, x.val, args); .)

+      ")"                              (. initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args); .)

+    | "("                              (. var udf = ty as UserDefinedType;

+                                          if (udf != null && udf.ModuleName != null && udf.TypeArgs.Count == 0) {

+                                            // The parsed name had the form "A.B", so treat "A" as the name of the type and "B" as

+                                            // the name of the constructor that's being invoked.

+                                            x = udf.tok;

+                                            ty = new UserDefinedType(udf.ModuleName, udf.ModuleName.val, new List<Type>(), null);

+                                          } else {

+                                            SemErr(t, "expected '.'");

+                                            x = null;

+                                          }

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

+        [ Expressions<args> ]

+      ")"                              (. if (x != null) {

+                                            initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);

+                                          }

+                                       .)

     ]

     (. if (ee != null) {

          r = new TypeRhs(newToken, ty, ee);

@@ -784,7 +802,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
   | "*"                                (. r = new HavocRhs(t); .)

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

   )

-  { Attribute<ref attrs> }             (. r.Attributes = attrs; .)

+  { Attribute<ref attrs> }             (. if (r != null) r.Attributes = attrs; .)

   .

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

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

@@ -792,6 +810,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
      AssignmentRhs r;  IdentifierExpr lhs0;

      List<VarDecl> lhss = new List<VarDecl>();

      List<AssignmentRhs> rhss = new List<AssignmentRhs>();

+     IToken suchThatAssume = null;

      Expression suchThat = null;

   .)

   [ "ghost"                                 (. isGhost = true;  x = t; .)

@@ -809,6 +828,8 @@ VarDeclStatement<.out Statement/*!*/ s.>
     { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)

     }

   | ":|"                           (. assignTok = t; .)

+    [ "assume"                     (. suchThatAssume = t; .)

+    ]

     Expression<out suchThat>

   ]

   ";"

@@ -818,7 +839,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
        foreach (var lhs in lhss) {

          ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));

        }

-       update = new AssignSuchThatStmt(assignTok, ies, suchThat);

+       update = new AssignSuchThatStmt(assignTok, ies, suchThat, suchThatAssume);

      } else if (rhss.Count == 0) {

        update = null;

      } else {

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 5fd34e65..a57ef79d 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -54,7 +54,7 @@ namespace Microsoft.Dafny {
 

       List<Type/*!*/> typeArgs = new List<Type/*!*/>();

       typeArgs.Add(arg);

-      UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs);

+      UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null);

       if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {

         ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);

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

@@ -393,7 +393,8 @@ namespace Microsoft.Dafny {
       Contract.Invariant(cce.NonNullElements(TypeArgs));

     }

 

-    public readonly IToken tok;

+    public readonly IToken ModuleName;  // may be null

+    public readonly IToken tok;  // token of the Name

     public readonly string Name;

     [Rep]

     public readonly List<Type/*!*/>/*!*/ TypeArgs;

@@ -408,13 +409,33 @@ namespace Microsoft.Dafny {
       }

     }

 

+    string compileName;

+    public string CompileName {

+      get {

+        if (compileName == null) {

+          compileName = NonglobalVariable.CompilerizeName(Name);

+        }

+        return compileName;

+      }

+    }

+    public string FullCompileName {

+      get {

+        if (ResolvedClass != null && !ResolvedClass.Module.IsDefaultModule) {

+          return ResolvedClass.Module.CompileName + "." + CompileName;

+        } else {

+          return CompileName;

+        }

+      }

+    }

+

     public TopLevelDecl ResolvedClass;  // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype

     public TypeParameter ResolvedParam;  // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list

 

-    public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs) {

+    public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs, IToken moduleName) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

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

+      this.ModuleName = moduleName;

       this.tok = tok;

       this.Name = name;

       this.TypeArgs = typeArgs;

@@ -480,6 +501,9 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<string>() != null);

 

       string s = Name;

+      if (ModuleName != null) {

+        s = ModuleName.val + "." + s;

+      }

       if (TypeArgs.Count != 0) {

         string sep = "<";

         foreach (Type t in TypeArgs) {

@@ -652,6 +676,15 @@ namespace Microsoft.Dafny {
     public IToken BodyStartTok = Token.NoToken;

     public IToken BodyEndTok = Token.NoToken;

     public readonly string/*!*/ Name;

+    string compileName;

+    public string CompileName {

+      get {

+        if (compileName == null) {

+          compileName = NonglobalVariable.CompilerizeName(Name);

+        }

+        return compileName;

+      }

+    }

     public readonly Attributes Attributes;

 

     public Declaration(IToken tok, string name, Attributes attributes) {

@@ -770,6 +803,11 @@ namespace Microsoft.Dafny {
         return Module.Name + "." + Name;

       }

     }

+    public string FullCompileName {

+      get {

+        return Module.CompileName + "." + CompileName;

+      }

+    }

   }

 

   public class ClassDecl : TopLevelDecl {

@@ -934,6 +972,14 @@ namespace Microsoft.Dafny {
         return EnclosingClass.FullName + "." + Name;

       }

     }

+    public string FullCompileName {

+      get {

+        Contract.Requires(EnclosingClass != null);

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

+

+        return EnclosingClass.FullCompileName + "." + CompileName;

+      }

+    }

   }

 

   public class Field : MemberDecl {

@@ -1019,6 +1065,9 @@ namespace Microsoft.Dafny {
     string/*!*/ UniqueName {

       get;

     }

+    string/*!*/ CompileName {

+      get;

+    }

     Type/*!*/ Type {

       get;

     }

@@ -1043,6 +1092,12 @@ namespace Microsoft.Dafny {
         throw new NotImplementedException();

       }

     }

+    public string CompileName {

+      get {

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

+        throw new NotImplementedException();

+      }

+    }

     public Type Type {

       get {

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

@@ -1085,6 +1140,46 @@ namespace Microsoft.Dafny {
         return name + "#" + varId;

       }

     }

+    static char[] specialChars = new char[] { '\'', '_', '?', '\\' };

+    public static string CompilerizeName(string nm) {

+      string name = null;

+      int i = 0;

+      while (true) {

+        int j = nm.IndexOfAny(specialChars, i);

+        if (j == -1) {

+          if (i == 0) {

+            return nm;  // this is the common case

+          } else {

+            return name + nm.Substring(i);

+          }

+        } else {

+          string nxt = nm.Substring(i, j);

+          name = name == null ? nxt : name + nxt;

+          switch (nm[j]) {

+            case '\'': name += "_k"; break;

+            case '_': name += "__"; break;

+            case '?': name += "_q"; break;

+            case '\\': name += "_b"; break;

+            default:

+              Contract.Assume(false);  // unexpected character

+              break;

+          }

+          i = j + 1;

+          if (i == nm.Length) {

+            return name;

+          }

+        }

+      }

+    }

+    protected string compileName;

+    public virtual string CompileName {

+      get {

+        if (compileName == null) {

+          compileName = string.Format("_{0}_{1}", varId, CompilerizeName(name));

+        }

+        return compileName;

+      }

+    }

     Type type;

     //[Pure(false)]  // TODO: if Type gets the status of [Frozen], then this attribute is not needed

     public Type/*!*/ Type {

@@ -1140,6 +1235,14 @@ namespace Microsoft.Dafny {
         return !Name.StartsWith("#");

       }

     }

+    public override string CompileName {

+      get {

+        if (compileName == null) {

+          compileName = CompilerizeName(Name);

+        }

+        return compileName;

+      }

+    }

   }

 

   /// <summary>

@@ -1172,7 +1275,6 @@ namespace Microsoft.Dafny {
 

   public class Function : MemberDecl, TypeParameter.ParentType {

     public readonly bool IsGhost;  // functions are "ghost" by default; a non-ghost function is called a "function method"

-    public readonly bool IsUnlimited;

     public bool IsRecursive;  // filled in during resolution

     public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;

     public readonly IToken OpenParen;  // can be null (for predicates), if there are no formals

@@ -1195,7 +1297,7 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Decreases != null);

     }

 

-    public Function(IToken tok, string name, bool isStatic, bool isGhost, bool isUnlimited,

+    public Function(IToken tok, string name, bool isStatic, bool isGhost,

                     List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals, Type resultType,

                     List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,

                     Expression body, Attributes attributes, bool signatureOmitted)

@@ -1211,7 +1313,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(ens));

       Contract.Requires(decreases != null);

       this.IsGhost = isGhost;

-      this.IsUnlimited = isUnlimited;

       this.TypeArgs = typeArgs;

       this.OpenParen = openParen;

       this.Formals = formals;

@@ -1228,11 +1329,11 @@ namespace Microsoft.Dafny {
   public class Predicate : Function

   {

     public readonly bool BodyIsExtended;  // says that this predicate definition is a refinement extension of a predicate definition is a refining module

-    public Predicate(IToken tok, string name, bool isStatic, bool isGhost, bool isUnlimited,

+    public Predicate(IToken tok, string name, bool isStatic, bool isGhost,

                      List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals,

                      List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,

                      Expression body, bool bodyIsExtended, Attributes attributes, bool signatureOmitted)

-      : base(tok, name, isStatic, isGhost, isUnlimited, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureOmitted) {

+      : base(tok, name, isStatic, isGhost, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureOmitted) {

       Contract.Requires(!bodyIsExtended || body != null);

       BodyIsExtended = bodyIsExtended;

     }

@@ -1320,7 +1421,7 @@ namespace Microsoft.Dafny {
 

   public abstract class Statement {

     public readonly IToken Tok;

-    public LabelNode Labels;  // mutable during resolution

+    public LList<Label> Labels;  // mutable during resolution

 

     private Attributes attributes;

     public Attributes Attributes {

@@ -1363,19 +1464,43 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class LabelNode

+  public class LList<T>

+  {

+    public readonly T Data;

+    public readonly LList<T> Next;

+    const LList<T> Empty = null;

+

+    public LList(T d, LList<T> next) {

+      Data = d;

+      Next = next;

+    }

+

+    public static LList<T> Append(LList<T> a, LList<T> b) {

+      if (a == null) return b;

+      return new LList<T>(a.Data, Append(a.Next, b));

+      // pretend this is ML

+    }

+    public static int Count(LList<T> n) {

+      int count = 0;

+      while (n != null) {

+        count++;

+        n = n.Next;

+      }

+      return count;

+    }

+  }

+

+  public class Label

   {

     public readonly IToken Tok;

-    public readonly string Label;

+    public readonly string Name;

     public readonly int UniqueId;

-    public readonly LabelNode Next;

     static int nodes = 0;

 

-    public LabelNode(IToken tok, string label, LabelNode next) {

+    public Label(IToken tok, string label) {

       Contract.Requires(tok != null);

       Tok = tok;

-      Label = label;

-      Next = next;

+      Name = label;

       UniqueId = nodes++;

     }

   }

@@ -1676,14 +1801,22 @@ namespace Microsoft.Dafny {
 

   public class AssignSuchThatStmt : ConcreteUpdateStatement

   {

-    public readonly AssumeStmt Assume;

-    public AssignSuchThatStmt(IToken tok, List<Expression> lhss, Expression expr)

+    public readonly Expression Expr;

+    public readonly IToken AssumeToken;

+    /// <summary>

+    /// "assumeToken" is allowed to be "null", in which case the verifier will check that a RHS value exists.

+    /// If "assumeToken" is non-null, then it should denote the "assume" keyword used in the statement.

+    /// </summary>

+    public AssignSuchThatStmt(IToken tok, List<Expression> lhss, Expression expr, IToken assumeToken)

       : base(tok, lhss) {

       Contract.Requires(tok != null);

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

       Contract.Requires(lhss.Count != 0);

       Contract.Requires(expr != null);

-      Assume = new AssumeStmt(tok, expr);

+      Expr = expr;

+      if (assumeToken != null) {

+        AssumeToken = assumeToken;

+      }

     }

   }

 

@@ -1744,6 +1877,24 @@ namespace Microsoft.Dafny {
         }

       }

     }

+

+    /// <summary>

+    /// This method assumes "lhs" has been successfully resolved.

+    /// </summary>

+    public static bool LhsIsToGhost(Expression lhs) {

+      Contract.Requires(lhs != null);

+      lhs = lhs.Resolved;

+      if (lhs is IdentifierExpr) {

+        var x = (IdentifierExpr)lhs;

+        return x.Var.IsGhost;

+      } else if (lhs is FieldSelectExpr) {

+        var x = (FieldSelectExpr)lhs;

+        return x.Field.IsGhost;

+      } else {

+        // LHS denotes an array element, which is always non-ghost

+        return false;

+      }

+    }

   }

 

   public class VarDecl : Statement, IVariable {

@@ -1778,6 +1929,15 @@ namespace Microsoft.Dafny {
         return name + "#" + varId;

       }

     }

+    string compileName;

+    public string CompileName {

+      get {

+        if (compileName == null) {

+          compileName = string.Format("_{0}_{1}", varId, NonglobalVariable.CompilerizeName(name));

+        }

+        return compileName;

+      }

+    }

     public readonly Type OptionalType;  // this is the type mentioned in the declaration, if any

     internal Type type;  // this is the declared or inferred type of the variable; it is non-null after resolution (even if resolution fails)

     //[Pure(false)]

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index fe4d58a9..9a439914 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -21,7 +21,7 @@ public class Parser {
 	public const int _colon = 5;

 	public const int _lbrace = 6;

 	public const int _rbrace = 7;

-	public const int maxT = 108;

+	public const int maxT = 107;

 

 	const bool T = true;

 	const bool x = false;

@@ -44,7 +44,6 @@ static int anonymousIds = 0;
 struct MemberModifiers {

   public bool IsGhost;

   public bool IsStatic;

-  public bool IsUnlimited;

 }

 // helper routine for parsing call statements

 ///<summary>

@@ -231,10 +230,10 @@ bool IsAttribute() {
 					if (la.kind == 12) {

 						ClassDecl(module, out c);

 						module.TopLevelDecls.Add(c); 

-					} else if (la.kind == 15 || la.kind == 16) {

+					} else if (la.kind == 14 || la.kind == 15) {

 						DatatypeDecl(module, out dt);

 						module.TopLevelDecls.Add(dt); 

-					} else if (la.kind == 22) {

+					} else if (la.kind == 21) {

 						ArbitraryTypeDecl(module, out at);

 						module.TopLevelDecls.Add(at); 

 					} else {

@@ -249,17 +248,17 @@ bool IsAttribute() {
 				if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } 

 				ClassDecl(defaultModule, out c);

 				defaultModule.TopLevelDecls.Add(c); 

-			} else if (la.kind == 15 || la.kind == 16) {

+			} else if (la.kind == 14 || la.kind == 15) {

 				if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } 

 				DatatypeDecl(defaultModule, out dt);

 				defaultModule.TopLevelDecls.Add(dt); 

-			} else if (la.kind == 22) {

+			} else if (la.kind == 21) {

 				if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } 

 				ArbitraryTypeDecl(defaultModule, out at);

 				defaultModule.TopLevelDecls.Add(at); 

 			} else if (StartOf(3)) {

 				ClassMemberDecl(membersDefaultClass, isGhost, false);

-			} else SynErr(109);

+			} else SynErr(108);

 		}

 		if (defaultModuleCreatedHere) {

 		 defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));

@@ -294,7 +293,7 @@ bool IsAttribute() {
 		IToken/*!*/ id; 

 		Ident(out id);

 		ids.Add(id.val); 

-		while (la.kind == 21) {

+		while (la.kind == 20) {

 			Get();

 			Ident(out id);

 			ids.Add(id.val); 

@@ -310,13 +309,13 @@ bool IsAttribute() {
 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

 		IToken bodyStart;

 		

-		while (!(la.kind == 0 || la.kind == 12)) {SynErr(110); Get();}

+		while (!(la.kind == 0 || la.kind == 12)) {SynErr(109); Get();}

 		Expect(12);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 23) {

+		if (la.kind == 22) {

 			GenericParameters(typeArgs);

 		}

 		Expect(6);

@@ -341,29 +340,29 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;  // dummy assignment

 		bool co = false;

 		

-		while (!(la.kind == 0 || la.kind == 15 || la.kind == 16)) {SynErr(111); Get();}

-		if (la.kind == 15) {

+		while (!(la.kind == 0 || la.kind == 14 || la.kind == 15)) {SynErr(110); Get();}

+		if (la.kind == 14) {

 			Get();

-		} else if (la.kind == 16) {

+		} else if (la.kind == 15) {

 			Get();

 			co = true; 

-		} else SynErr(112);

+		} else SynErr(111);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 23) {

+		if (la.kind == 22) {

 			GenericParameters(typeArgs);

 		}

-		Expect(17);

+		Expect(16);

 		bodyStart = t; 

 		DatatypeMemberDecl(ctors);

-		while (la.kind == 18) {

+		while (la.kind == 17) {

 			Get();

 			DatatypeMemberDecl(ctors);

 		}

-		while (!(la.kind == 0 || la.kind == 19)) {SynErr(113); Get();}

-		Expect(19);

+		while (!(la.kind == 0 || la.kind == 18)) {SynErr(112); Get();}

+		Expect(18);

 		if (co) {

 		 dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);

 		} else {

@@ -378,14 +377,14 @@ bool IsAttribute() {
 		IToken/*!*/ id;

 		Attributes attrs = null;

 		

-		Expect(22);

+		Expect(21);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

 		at = new ArbitraryTypeDecl(id, id.val, module, attrs); 

-		while (!(la.kind == 0 || la.kind == 19)) {SynErr(114); Get();}

-		Expect(19);

+		while (!(la.kind == 0 || la.kind == 18)) {SynErr(113); Get();}

+		Expect(18);

 	}

 

 	void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm, bool isAlreadyGhost, bool allowConstructors) {

@@ -395,41 +394,38 @@ bool IsAttribute() {
 		MemberModifiers mmod = new MemberModifiers();

 		mmod.IsGhost = isAlreadyGhost;

 		

-		while (la.kind == 8 || la.kind == 13 || la.kind == 14) {

+		while (la.kind == 8 || la.kind == 13) {

 			if (la.kind == 8) {

 				Get();

 				mmod.IsGhost = true; 

-			} else if (la.kind == 13) {

-				Get();

-				mmod.IsStatic = true; 

 			} else {

 				Get();

-				mmod.IsUnlimited = true; 

+				mmod.IsStatic = true; 

 			}

 		}

-		if (la.kind == 20) {

+		if (la.kind == 19) {

 			FieldDecl(mmod, mm);

 		} else if (la.kind == 44 || la.kind == 45) {

 			FunctionDecl(mmod, out f);

 			mm.Add(f); 

-		} else if (la.kind == 25 || la.kind == 26) {

+		} else if (la.kind == 24 || la.kind == 25) {

 			MethodDecl(mmod, allowConstructors, out m);

 			mm.Add(m); 

-		} else SynErr(115);

+		} else SynErr(114);

 	}

 

 	void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {

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

 		IToken/*!*/ id; 

-		Expect(23);

+		Expect(22);

 		Ident(out id);

 		typeArgs.Add(new TypeParameter(id, id.val)); 

-		while (la.kind == 21) {

+		while (la.kind == 20) {

 			Get();

 			Ident(out id);

 			typeArgs.Add(new TypeParameter(id, id.val)); 

 		}

-		Expect(24);

+		Expect(23);

 	}

 

 	void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {

@@ -437,9 +433,8 @@ bool IsAttribute() {
 		Attributes attrs = null;

 		IToken/*!*/ id;  Type/*!*/ ty;

 		

-		while (!(la.kind == 0 || la.kind == 20)) {SynErr(116); Get();}

-		Expect(20);

-		if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }

+		while (!(la.kind == 0 || la.kind == 19)) {SynErr(115); Get();}

+		Expect(19);

 		if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }

 		

 		while (la.kind == 6) {

@@ -447,13 +442,13 @@ bool IsAttribute() {
 		}

 		IdentType(out id, out ty);

 		mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 

-		while (la.kind == 21) {

+		while (la.kind == 20) {

 			Get();

 			IdentType(out id, out ty);

 			mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 

 		}

-		while (!(la.kind == 0 || la.kind == 19)) {SynErr(117); Get();}

-		Expect(19);

+		while (!(la.kind == 0 || la.kind == 18)) {SynErr(116); Get();}

+		Expect(18);

 	}

 

 	void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) {

@@ -477,7 +472,7 @@ bool IsAttribute() {
 		

 		if (la.kind == 44) {

 			Get();

-			if (la.kind == 25) {

+			if (la.kind == 24) {

 				Get();

 				isFunctionMethod = true; 

 			}

@@ -487,22 +482,22 @@ bool IsAttribute() {
 				Attribute(ref attrs);

 			}

 			Ident(out id);

-			if (la.kind == 23 || la.kind == 34) {

-				if (la.kind == 23) {

+			if (la.kind == 22 || la.kind == 33) {

+				if (la.kind == 22) {

 					GenericParameters(typeArgs);

 				}

 				Formals(true, isFunctionMethod, formals, out openParen);

 				Expect(5);

 				Type(out returnType);

-			} else if (la.kind == 28) {

+			} else if (la.kind == 27) {

 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(118);

+			} else SynErr(117);

 		} else if (la.kind == 45) {

 			Get();

 			isPredicate = true; 

-			if (la.kind == 25) {

+			if (la.kind == 24) {

 				Get();

 				isFunctionMethod = true; 

 			}

@@ -513,22 +508,22 @@ bool IsAttribute() {
 			}

 			Ident(out id);

 			if (StartOf(4)) {

-				if (la.kind == 23) {

+				if (la.kind == 22) {

 					GenericParameters(typeArgs);

 				}

-				if (la.kind == 34) {

+				if (la.kind == 33) {

 					Formals(true, isFunctionMethod, formals, out openParen);

 					if (la.kind == 5) {

 						Get();

 						SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); 

 					}

 				}

-			} else if (la.kind == 28) {

+			} else if (la.kind == 27) {

 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(119);

-		} else SynErr(120);

+			} else SynErr(118);

+		} else SynErr(119);

 		while (StartOf(5)) {

 			FunctionSpec(reqs, reads, ens, decreases);

 		}

@@ -536,10 +531,10 @@ bool IsAttribute() {
 			FunctionBody(out body, out bodyStart, out bodyEnd);

 		}

 		if (isPredicate) {

-		  f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals,

+		  f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

 		                    reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs, signatureOmitted);

 		} else {

-		  f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals, returnType,

+		  f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,

 		                   reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureOmitted);

 		}

 		f.BodyStartTok = bodyStart;

@@ -567,10 +562,10 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

-		while (!(la.kind == 0 || la.kind == 25 || la.kind == 26)) {SynErr(121); Get();}

-		if (la.kind == 25) {

+		while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(120); Get();}

+		if (la.kind == 24) {

 			Get();

-		} else if (la.kind == 26) {

+		} else if (la.kind == 25) {

 			Get();

 			if (allowConstructor) {

 			 isConstructor = true;

@@ -578,8 +573,7 @@ bool IsAttribute() {
 			 SemErr(t, "constructors are only allowed in classes");

 			}

 			

-		} else SynErr(122);

-		if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }

+		} else SynErr(121);

 		if (isConstructor) {

 		 if (mmod.IsGhost) {

 		   SemErr(t, "constructors cannot be declared 'ghost'");

@@ -593,20 +587,20 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 23 || la.kind == 34) {

-			if (la.kind == 23) {

+		if (la.kind == 22 || la.kind == 33) {

+			if (la.kind == 22) {

 				GenericParameters(typeArgs);

 			}

 			Formals(true, !mmod.IsGhost, ins, out openParen);

-			if (la.kind == 27) {

+			if (la.kind == 26) {

 				Get();

 				if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } 

 				Formals(false, !mmod.IsGhost, outs, out openParen);

 			}

-		} else if (la.kind == 28) {

+		} else if (la.kind == 27) {

 			Get();

 			signatureOmitted = true; openParen = Token.NoToken; 

-		} else SynErr(123);

+		} else SynErr(122);

 		while (StartOf(6)) {

 			MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);

 		}

@@ -635,7 +629,7 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 34) {

+		if (la.kind == 33) {

 			FormalsOptionalIds(formals);

 		}

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

@@ -643,17 +637,17 @@ bool IsAttribute() {
 

 	void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {

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

-		Expect(34);

+		Expect(33);

 		if (StartOf(7)) {

 			TypeIdentOptional(out id, out name, out ty, out isGhost);

 			formals.Add(new Formal(id, name, ty, true, isGhost)); 

-			while (la.kind == 21) {

+			while (la.kind == 20) {

 				Get();

 				TypeIdentOptional(out id, out name, out ty, out isGhost);

 				formals.Add(new Formal(id, name, ty, true, isGhost)); 

 			}

 		}

-		Expect(35);

+		Expect(34);

 	}

 

 	void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {

@@ -737,22 +731,22 @@ bool IsAttribute() {
 		List<Type/*!*/>/*!*/ gt;

 		

 		switch (la.kind) {

-		case 36: {

+		case 35: {

 			Get();

 			tok = t; 

 			break;

 		}

-		case 37: {

+		case 36: {

 			Get();

 			tok = t;  ty = new NatType(); 

 			break;

 		}

-		case 38: {

+		case 37: {

 			Get();

 			tok = t;  ty = new IntType(); 

 			break;

 		}

-		case 39: {

+		case 38: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -763,7 +757,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 40: {

+		case 39: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -774,7 +768,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 41: {

+		case 40: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -785,39 +779,39 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 42: {

+		case 41: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

 			if (gt.Count != 2) {

 			 SemErr("map type expects exactly two type arguments");

 			}

-			ty = new MapType(gt[0], gt[1]);

+			else { ty = new MapType(gt[0], gt[1]); }

 			

 			break;

 		}

-		case 1: case 3: case 43: {

+		case 1: case 3: case 42: {

 			ReferenceType(out tok, out ty);

 			break;

 		}

-		default: SynErr(124); break;

+		default: SynErr(123); break;

 		}

 	}

 

 	void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen) {

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

-		Expect(34);

+		Expect(33);

 		openParen = t; 

 		if (la.kind == 1 || la.kind == 8) {

 			GIdentType(allowGhostKeyword, out id, out ty, out isGhost);

 			formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 

-			while (la.kind == 21) {

+			while (la.kind == 20) {

 				Get();

 				GIdentType(allowGhostKeyword, out id, out ty, out isGhost);

 				formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 

 			}

 		}

-		Expect(35);

+		Expect(34);

 	}

 

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

@@ -825,8 +819,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false; Attributes ensAttrs = null;

 		

-		while (!(StartOf(8))) {SynErr(125); Get();}

-		if (la.kind == 29) {

+		while (!(StartOf(8))) {SynErr(124); Get();}

+		if (la.kind == 28) {

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref modAttrs);

@@ -834,44 +828,44 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (StartOf(9)) {

 				FrameExpression(out fe);

 				mod.Add(fe); 

-				while (la.kind == 21) {

+				while (la.kind == 20) {

 					Get();

 					FrameExpression(out fe);

 					mod.Add(fe); 

 				}

 			}

-			while (!(la.kind == 0 || la.kind == 19)) {SynErr(126); Get();}

-			Expect(19);

-		} else if (la.kind == 30 || la.kind == 31 || la.kind == 32) {

-			if (la.kind == 30) {

+			while (!(la.kind == 0 || la.kind == 18)) {SynErr(125); Get();}

+			Expect(18);

+		} else if (la.kind == 29 || la.kind == 30 || la.kind == 31) {

+			if (la.kind == 29) {

 				Get();

 				isFree = true; 

 			}

-			if (la.kind == 31) {

+			if (la.kind == 30) {

 				Get();

 				Expression(out e);

-				while (!(la.kind == 0 || la.kind == 19)) {SynErr(127); Get();}

-				Expect(19);

+				while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();}

+				Expect(18);

 				req.Add(new MaybeFreeExpression(e, isFree)); 

-			} else if (la.kind == 32) {

+			} else if (la.kind == 31) {

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref ensAttrs);

 				}

 				Expression(out e);

-				while (!(la.kind == 0 || la.kind == 19)) {SynErr(128); Get();}

-				Expect(19);

+				while (!(la.kind == 0 || la.kind == 18)) {SynErr(127); Get();}

+				Expect(18);

 				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 

-			} else SynErr(129);

-		} else if (la.kind == 33) {

+			} else SynErr(128);

+		} else if (la.kind == 32) {

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref decAttrs);

 			}

 			DecreasesList(decreases, false);

-			while (!(la.kind == 0 || la.kind == 19)) {SynErr(130); Get();}

-			Expect(19);

-		} else SynErr(131);

+			while (!(la.kind == 0 || la.kind == 18)) {SynErr(129); Get();}

+			Expect(18);

+		} else SynErr(130);

 	}

 

 	void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {

@@ -912,7 +906,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		 decreases.Add(e);

 		}

 		

-		while (la.kind == 21) {

+		while (la.kind == 20) {

 			Get();

 			PossiblyWildExpression(out e);

 			if (!allowWildcard && e is WildcardExpr) {

@@ -926,23 +920,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {

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

-		Expect(23);

+		Expect(22);

 		Type(out ty);

 		gt.Add(ty); 

-		while (la.kind == 21) {

+		while (la.kind == 20) {

 			Get();

 			Type(out ty);

 			gt.Add(ty); 

 		}

-		Expect(24);

+		Expect(23);

 	}

 

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

+		IToken moduleName = null;

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

 		

-		if (la.kind == 43) {

+		if (la.kind == 42) {

 			Get();

 			tok = t;  ty = new ObjectType(); 

 		} else if (la.kind == 3) {

@@ -961,48 +956,53 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 1) {

 			Ident(out tok);

 			gt = new List<Type/*!*/>(); 

-			if (la.kind == 23) {

+			if (la.kind == 43) {

+				moduleName = tok; 

+				Get();

+				Ident(out tok);

+			}

+			if (la.kind == 22) {

 				GenericInstantiation(gt);

 			}

-			ty = new UserDefinedType(tok, tok.val, gt); 

-		} else SynErr(132);

+			ty = new UserDefinedType(tok, tok.val, gt, moduleName); 

+		} else SynErr(131);

 	}

 

 	void 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; 

-		if (la.kind == 31) {

-			while (!(la.kind == 0 || la.kind == 31)) {SynErr(133); Get();}

+		if (la.kind == 30) {

+			while (!(la.kind == 0 || la.kind == 30)) {SynErr(132); Get();}

 			Get();

 			Expression(out e);

-			while (!(la.kind == 0 || la.kind == 19)) {SynErr(134); Get();}

-			Expect(19);

+			while (!(la.kind == 0 || la.kind == 18)) {SynErr(133); Get();}

+			Expect(18);

 			reqs.Add(e); 

 		} else if (la.kind == 46) {

 			Get();

 			if (StartOf(11)) {

 				PossiblyWildFrameExpression(out fe);

 				reads.Add(fe); 

-				while (la.kind == 21) {

+				while (la.kind == 20) {

 					Get();

 					PossiblyWildFrameExpression(out fe);

 					reads.Add(fe); 

 				}

 			}

-			while (!(la.kind == 0 || la.kind == 19)) {SynErr(135); Get();}

-			Expect(19);

-		} else if (la.kind == 32) {

+			while (!(la.kind == 0 || la.kind == 18)) {SynErr(134); Get();}

+			Expect(18);

+		} else if (la.kind == 31) {

 			Get();

 			Expression(out e);

-			while (!(la.kind == 0 || la.kind == 19)) {SynErr(136); Get();}

-			Expect(19);

+			while (!(la.kind == 0 || la.kind == 18)) {SynErr(135); Get();}

+			Expect(18);

 			ens.Add(e); 

-		} else if (la.kind == 33) {

+		} else if (la.kind == 32) {

 			Get();

 			DecreasesList(decreases, false);

-			while (!(la.kind == 0 || la.kind == 19)) {SynErr(137); Get();}

-			Expect(19);

-		} else SynErr(138);

+			while (!(la.kind == 0 || la.kind == 18)) {SynErr(136); Get();}

+			Expect(18);

+		} else SynErr(137);

 	}

 

 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {

@@ -1021,7 +1021,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			fe = new FrameExpression(new WildcardExpr(t), null); 

 		} else if (StartOf(9)) {

 			FrameExpression(out fe);

-		} else SynErr(139);

+		} else SynErr(138);

 	}

 

 	void PossiblyWildExpression(out Expression/*!*/ e) {

@@ -1032,7 +1032,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new WildcardExpr(t); 

 		} else if (StartOf(9)) {

 			Expression(out e);

-		} else SynErr(140);

+		} else SynErr(139);

 	}

 

 	void Stmt(List<Statement/*!*/>/*!*/ ss) {

@@ -1049,7 +1049,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken bodyStart, bodyEnd;

 		int breakCount;

 		

-		while (!(StartOf(12))) {SynErr(141); Get();}

+		while (!(StartOf(12))) {SynErr(140); Get();}

 		switch (la.kind) {

 		case 6: {

 			BlockStmt(out bs, out bodyStart, out bodyEnd);

@@ -1060,19 +1060,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			AssertStmt(out s);

 			break;

 		}

-		case 67: {

+		case 54: {

 			AssumeStmt(out s);

 			break;

 		}

-		case 68: {

+		case 67: {

 			PrintStmt(out s);

 			break;

 		}

-		case 1: case 2: case 18: case 34: case 93: case 94: case 95: case 96: case 97: case 98: case 99: {

+		case 1: case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

 			UpdateStmt(out s);

 			break;

 		}

-		case 8: case 20: {

+		case 8: case 19: {

 			VarDeclStatement(out s);

 			break;

 		}

@@ -1088,7 +1088,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			MatchStmt(out s);

 			break;

 		}

-		case 69: {

+		case 68: {

 			ParallelStmt(out s);

 			break;

 		}

@@ -1098,7 +1098,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Ident(out id);

 			Expect(5);

 			OneStmt(out s);

-			s.Labels = new LabelNode(x, id.val, s.Labels); 

+			s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); 

 			break;

 		}

 		case 50: {

@@ -1107,14 +1107,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (la.kind == 1) {

 				Ident(out id);

 				label = id.val; 

-			} else if (la.kind == 19 || la.kind == 50) {

+			} else if (la.kind == 18 || la.kind == 50) {

 				while (la.kind == 50) {

 					Get();

 					breakCount++; 

 				}

-			} else SynErr(142);

-			while (!(la.kind == 0 || la.kind == 19)) {SynErr(143); Get();}

-			Expect(19);

+			} else SynErr(141);

+			while (!(la.kind == 0 || la.kind == 18)) {SynErr(142); Get();}

+			Expect(18);

 			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 

 			break;

 		}

@@ -1122,13 +1122,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			ReturnStmt(out s);

 			break;

 		}

-		case 28: {

+		case 27: {

 			Get();

 			s = new SkeletonStatement(t); 

-			Expect(19);

+			Expect(18);

 			break;

 		}

-		default: SynErr(144); break;

+		default: SynErr(143); break;

 		}

 	}

 

@@ -1143,10 +1143,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		if (StartOf(9)) {

 			Expression(out e);

-		} else if (la.kind == 28) {

+		} else if (la.kind == 27) {

 			Get();

-		} else SynErr(145);

-		Expect(19);

+		} else SynErr(144);

+		Expect(18);

 		if (e == null) {

 		 s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);

 		} else {

@@ -1157,10 +1157,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void AssumeStmt(out Statement/*!*/ s) {

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

-		Expect(67);

+		Expect(54);

 		x = t; 

 		Expression(out e);

-		Expect(19);

+		Expect(18);

 		s = new AssumeStmt(x, e); 

 	}

 

@@ -1168,16 +1168,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

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

 		

-		Expect(68);

+		Expect(67);

 		x = t; 

 		AttributeArg(out arg);

 		args.Add(arg); 

-		while (la.kind == 21) {

+		while (la.kind == 20) {

 			Get();

 			AttributeArg(out arg);

 			args.Add(arg); 

 		}

-		Expect(19);

+		Expect(18);

 		s = new PrintStmt(x, args); 

 	}

 

@@ -1188,19 +1188,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression lhs0;

 		IToken x;

 		Attributes attrs = null;

+		IToken suchThatAssume = null;

 		Expression suchThat = null;

 		

 		Lhs(out e);

 		x = e.tok; 

-		if (la.kind == 6 || la.kind == 19) {

+		if (la.kind == 6 || la.kind == 18) {

 			while (la.kind == 6) {

 				Attribute(ref attrs);

 			}

-			Expect(19);

+			Expect(18);

 			rhss.Add(new ExprRhs(e, attrs)); 

-		} else if (la.kind == 21 || la.kind == 52 || la.kind == 53) {

+		} else if (la.kind == 20 || la.kind == 52 || la.kind == 53) {

 			lhss.Add(e);  lhs0 = e; 

-			while (la.kind == 21) {

+			while (la.kind == 20) {

 				Get();

 				Lhs(out e);

 				lhss.Add(e); 

@@ -1210,7 +1211,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				x = t; 

 				Rhs(out r, lhs0);

 				rhss.Add(r); 

-				while (la.kind == 21) {

+				while (la.kind == 20) {

 					Get();

 					Rhs(out r, lhs0);

 					rhss.Add(r); 

@@ -1218,15 +1219,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else if (la.kind == 53) {

 				Get();

 				x = t; 

+				if (la.kind == 54) {

+					Get();

+					suchThatAssume = t; 

+				}

 				Expression(out suchThat);

-			} else SynErr(146);

-			Expect(19);

+			} else SynErr(145);

+			Expect(18);

 		} else if (la.kind == 5) {

 			Get();

 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

-		} else SynErr(147);

+		} else SynErr(146);

 		if (suchThat != null) {

-		 s = new AssignSuchThatStmt(x, lhss, suchThat);

+		 s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);

 		} else {

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

 		}

@@ -1239,17 +1244,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		AssignmentRhs r;  IdentifierExpr lhs0;

 		List<VarDecl> lhss = new List<VarDecl>();

 		List<AssignmentRhs> rhss = new List<AssignmentRhs>();

+		IToken suchThatAssume = null;

 		Expression suchThat = null;

 		

 		if (la.kind == 8) {

 			Get();

 			isGhost = true;  x = t; 

 		}

-		Expect(20);

+		Expect(19);

 		if (!isGhost) { x = t; } 

 		LocalIdentTypeOptional(out d, isGhost);

 		lhss.Add(d); 

-		while (la.kind == 21) {

+		while (la.kind == 20) {

 			Get();

 			LocalIdentTypeOptional(out d, isGhost);

 			lhss.Add(d); 

@@ -1263,7 +1269,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				

 				Rhs(out r, lhs0);

 				rhss.Add(r); 

-				while (la.kind == 21) {

+				while (la.kind == 20) {

 					Get();

 					Rhs(out r, lhs0);

 					rhss.Add(r); 

@@ -1271,17 +1277,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else {

 				Get();

 				assignTok = t; 

+				if (la.kind == 54) {

+					Get();

+					suchThatAssume = t; 

+				}

 				Expression(out suchThat);

 			}

 		}

-		Expect(19);

+		Expect(18);

 		ConcreteUpdateStatement update;

 		if (suchThat != null) {

 		 var ies = new List<Expression>();

 		 foreach (var lhs in lhss) {

 		   ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));

 		 }

-		 update = new AssignSuchThatStmt(assignTok, ies, suchThat);

+		 update = new AssignSuchThatStmt(assignTok, ies, suchThat, suchThatAssume);

 		} else if (rhss.Count == 0) {

 		 update = null;

 		} else {

@@ -1308,8 +1318,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Expect(59);

 		x = t; 

-		if (la.kind == 28 || la.kind == 34) {

-			if (la.kind == 34) {

+		if (la.kind == 27 || la.kind == 33) {

+			if (la.kind == 33) {

 				Guard(out guard);

 			} else {

 				Get();

@@ -1324,7 +1334,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				} else if (la.kind == 6) {

 					BlockStmt(out bs, out bodyStart, out bodyEnd);

 					els = bs; 

-				} else SynErr(148);

+				} else SynErr(147);

 			}

 			if (guardOmitted) {

 			 ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);

@@ -1335,7 +1345,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 6) {

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(149);

+		} else SynErr(148);

 	}

 

 	void WhileStmt(out Statement/*!*/ stmt) {

@@ -1353,8 +1363,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Expect(63);

 		x = t; 

-		if (la.kind == 28 || la.kind == 34) {

-			if (la.kind == 34) {

+		if (la.kind == 27 || la.kind == 33) {

+			if (la.kind == 33) {

 				Guard(out guard);

 				Contract.Assume(guard == null || cce.Owner.None(guard)); 

 			} else {

@@ -1364,10 +1374,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

 			if (la.kind == 6) {

 				BlockStmt(out body, out bodyStart, out bodyEnd);

-			} else if (la.kind == 28) {

+			} else if (la.kind == 27) {

 				Get();

 				bodyOmitted = true; 

-			} else SynErr(150);

+			} else SynErr(149);

 			if (guardOmitted || bodyOmitted) {

 			 if (decreases.Count != 0) {

 			   SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops");

@@ -1388,7 +1398,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

 			AlternativeBlock(out alternatives);

 			stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); 

-		} else SynErr(151);

+		} else SynErr(150);

 	}

 

 	void MatchStmt(out Statement/*!*/ s) {

@@ -1419,9 +1429,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BlockStmt/*!*/ block;

 		IToken bodyStart, bodyEnd;

 		

-		Expect(69);

+		Expect(68);

 		x = t; 

-		Expect(34);

+		Expect(33);

 		if (la.kind == 1) {

 			List<BoundVar/*!*/> bvarsX;  Attributes attrsX;  Expression rangeX; 

 			QuantifierDomain(out bvarsX, out attrsX, out rangeX);

@@ -1431,16 +1441,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (bvars == null) { bvars = new List<BoundVar>(); }

 		if (range == null) { range = new LiteralExpr(x, true); }

 		

-		Expect(35);

-		while (la.kind == 30 || la.kind == 32) {

+		Expect(34);

+		while (la.kind == 29 || la.kind == 31) {

 			isFree = false; 

-			if (la.kind == 30) {

+			if (la.kind == 29) {

 				Get();

 				isFree = true; 

 			}

-			Expect(32);

+			Expect(31);

 			Expression(out e);

-			Expect(19);

+			Expect(18);

 			ens.Add(new MaybeFreeExpression(e, isFree)); 

 		}

 		BlockStmt(out block, out bodyStart, out bodyEnd);

@@ -1457,13 +1467,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (StartOf(14)) {

 			Rhs(out r, null);

 			rhss = new List<AssignmentRhs>(); rhss.Add(r); 

-			while (la.kind == 21) {

+			while (la.kind == 20) {

 				Get();

 				Rhs(out r, null);

 				rhss.Add(r); 

 			}

 		}

-		Expect(19);

+		Expect(18);

 		s = new ReturnStmt(returnTok, rhss); 

 	}

 

@@ -1476,29 +1486,49 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		r = null;  // to please compiler

 		Attributes attrs = null;

 		

-		if (la.kind == 54) {

+		if (la.kind == 55) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

-			if (la.kind == 55 || la.kind == 57) {

-				if (la.kind == 55) {

+			if (la.kind == 33 || la.kind == 43 || la.kind == 56) {

+				if (la.kind == 56) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(56);

+					Expect(57);

 					UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);

 					

-				} else {

+				} else if (la.kind == 43) {

 					Get();

 					Ident(out x);

+					Expect(33);

+					args = new List<Expression/*!*/>(); 

+					if (StartOf(9)) {

+						Expressions(args);

+					}

 					Expect(34);

+					initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args); 

+				} else {

+					Get();

+					var udf = ty as UserDefinedType;

+					if (udf != null && udf.ModuleName != null && udf.TypeArgs.Count == 0) {

+					 // The parsed name had the form "A.B", so treat "A" as the name of the type and "B" as

+					 // the name of the constructor that's being invoked.

+					 x = udf.tok;

+					 ty = new UserDefinedType(udf.ModuleName, udf.ModuleName.val, new List<Type>(), null);

+					} else {

+					 SemErr(t, "expected '.'");

+					 x = null;

+					}

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

 					if (StartOf(9)) {

 						Expressions(args);

 					}

-					Expect(35);

-					initCall = new CallStmt(x, new List<Expression>(),

-					                       receiverForInitCall, x.val, args); 

+					Expect(34);

+					if (x != null) {

+					 initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);

+					}

+					

 				}

 			}

 			if (ee != null) {

@@ -1518,11 +1548,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(9)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(152);

+		} else SynErr(151);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

-		r.Attributes = attrs; 

+		if (r != null) r.Attributes = attrs; 

 	}

 

 	void Lhs(out Expression e) {

@@ -1530,23 +1560,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 55 || la.kind == 57) {

+			while (la.kind == 43 || la.kind == 56) {

 				Suffix(ref e);

 			}

 		} else if (StartOf(15)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

-			while (la.kind == 55 || la.kind == 57) {

+			while (la.kind == 43 || la.kind == 56) {

 				Suffix(ref e);

 			}

-		} else SynErr(153);

+		} else SynErr(152);

 	}

 

 	void Expressions(List<Expression/*!*/>/*!*/ args) {

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

 		Expression(out e);

 		args.Add(e); 

-		while (la.kind == 21) {

+		while (la.kind == 20) {

 			Get();

 			Expression(out e);

 			args.Add(e); 

@@ -1555,15 +1585,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Guard(out Expression e) {

 		Expression/*!*/ ee;  e = null; 

-		Expect(34);

+		Expect(33);

 		if (la.kind == 47) {

 			Get();

 			e = null; 

 		} else if (StartOf(9)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(154);

-		Expect(35);

+		} else SynErr(153);

+		Expect(34);

 	}

 

 	void AlternativeBlock(out List<GuardedAlternative> alternatives) {

@@ -1595,22 +1625,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		mod = null;

 		

 		while (StartOf(16)) {

-			if (la.kind == 30 || la.kind == 64) {

+			if (la.kind == 29 || la.kind == 64) {

 				Invariant(out invariant);

-				while (!(la.kind == 0 || la.kind == 19)) {SynErr(155); Get();}

-				Expect(19);

+				while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();}

+				Expect(18);

 				invariants.Add(invariant); 

-			} else if (la.kind == 33) {

-				while (!(la.kind == 0 || la.kind == 33)) {SynErr(156); Get();}

+			} else if (la.kind == 32) {

+				while (!(la.kind == 0 || la.kind == 32)) {SynErr(155); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

-				while (!(la.kind == 0 || la.kind == 19)) {SynErr(157); Get();}

-				Expect(19);

+				while (!(la.kind == 0 || la.kind == 18)) {SynErr(156); Get();}

+				Expect(18);

 			} else {

-				while (!(la.kind == 0 || la.kind == 29)) {SynErr(158); Get();}

+				while (!(la.kind == 0 || la.kind == 28)) {SynErr(157); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

@@ -1619,22 +1649,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				if (StartOf(9)) {

 					FrameExpression(out fe);

 					mod.Add(fe); 

-					while (la.kind == 21) {

+					while (la.kind == 20) {

 						Get();

 						FrameExpression(out fe);

 						mod.Add(fe); 

 					}

 				}

-				while (!(la.kind == 0 || la.kind == 19)) {SynErr(159); Get();}

-				Expect(19);

+				while (!(la.kind == 0 || la.kind == 18)) {SynErr(158); Get();}

+				Expect(18);

 			}

 		}

 	}

 

 	void Invariant(out MaybeFreeExpression/*!*/ invariant) {

 		bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; 

-		while (!(la.kind == 0 || la.kind == 30 || la.kind == 64)) {SynErr(160); Get();}

-		if (la.kind == 30) {

+		while (!(la.kind == 0 || la.kind == 29 || la.kind == 64)) {SynErr(159); Get();}

+		if (la.kind == 29) {

 			Get();

 			isFree = true; 

 		}

@@ -1656,16 +1686,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(61);

 		x = t; 

 		Ident(out id);

-		if (la.kind == 34) {

+		if (la.kind == 33) {

 			Get();

 			IdentTypeOptional(out bv);

 			arguments.Add(bv); 

-			while (la.kind == 21) {

+			while (la.kind == 20) {

 				Get();

 				IdentTypeOptional(out bv);

 				arguments.Add(bv); 

 			}

-			Expect(35);

+			Expect(34);

 		}

 		Expect(62);

 		while (StartOf(10)) {

@@ -1682,7 +1712,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(9)) {

 			Expression(out e);

 			arg = new Attributes.Argument(t, e); 

-		} else SynErr(161);

+		} else SynErr(160);

 	}

 

 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {

@@ -1693,7 +1723,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

-		while (la.kind == 21) {

+		while (la.kind == 20) {

 			Get();

 			IdentTypeOptional(out bv);

 			bvars.Add(bv); 

@@ -1701,7 +1731,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

-		if (la.kind == 18) {

+		if (la.kind == 17) {

 			Get();

 			Expression(out range);

 		}

@@ -1710,7 +1740,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void EquivExpression(out Expression/*!*/ e0) {

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

 		ImpliesExpression(out e0);

-		while (la.kind == 70 || la.kind == 71) {

+		while (la.kind == 69 || la.kind == 70) {

 			EquivOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1721,7 +1751,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ImpliesExpression(out Expression/*!*/ e0) {

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

 		LogicalExpression(out e0);

-		if (la.kind == 72 || la.kind == 73) {

+		if (la.kind == 71 || la.kind == 72) {

 			ImpliesOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1730,23 +1760,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void EquivOp() {

-		if (la.kind == 70) {

+		if (la.kind == 69) {

 			Get();

-		} else if (la.kind == 71) {

+		} else if (la.kind == 70) {

 			Get();

-		} else SynErr(162);

+		} else SynErr(161);

 	}

 

 	void LogicalExpression(out Expression/*!*/ e0) {

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

 		RelationalExpression(out e0);

 		if (StartOf(17)) {

-			if (la.kind == 74 || la.kind == 75) {

+			if (la.kind == 73 || la.kind == 74) {

 				AndOp();

 				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 

-				while (la.kind == 74 || la.kind == 75) {

+				while (la.kind == 73 || la.kind == 74) {

 					AndOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1757,7 +1787,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 

-				while (la.kind == 76 || la.kind == 77) {

+				while (la.kind == 75 || la.kind == 76) {

 					OrOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1768,11 +1798,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void ImpliesOp() {

-		if (la.kind == 72) {

+		if (la.kind == 71) {

 			Get();

-		} else if (la.kind == 73) {

+		} else if (la.kind == 72) {

 			Get();

-		} else SynErr(163);

+		} else SynErr(162);

 	}

 

 	void RelationalExpression(out Expression/*!*/ e) {

@@ -1866,25 +1896,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void AndOp() {

-		if (la.kind == 74) {

+		if (la.kind == 73) {

 			Get();

-		} else if (la.kind == 75) {

+		} else if (la.kind == 74) {

 			Get();

-		} else SynErr(164);

+		} else SynErr(163);

 	}

 

 	void OrOp() {

-		if (la.kind == 76) {

+		if (la.kind == 75) {

 			Get();

-		} else if (la.kind == 77) {

+		} else if (la.kind == 76) {

 			Get();

-		} else SynErr(165);

+		} else SynErr(164);

 	}

 

 	void Term(out Expression/*!*/ e0) {

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

 		Factor(out e0);

-		while (la.kind == 88 || la.kind == 89) {

+		while (la.kind == 87 || la.kind == 88) {

 			AddOp(out x, out op);

 			Factor(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -1897,50 +1927,50 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken y;

 		

 		switch (la.kind) {

-		case 78: {

+		case 77: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Eq; 

 			break;

 		}

-		case 23: {

+		case 22: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Lt; 

 			break;

 		}

-		case 24: {

+		case 23: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Gt; 

 			break;

 		}

-		case 79: {

+		case 78: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Le; 

 			break;

 		}

-		case 80: {

+		case 79: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		case 81: {

+		case 80: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Neq; 

 			break;

 		}

-		case 82: {

+		case 81: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Disjoint; 

 			break;

 		}

-		case 83: {

+		case 82: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.In; 

 			break;

 		}

-		case 84: {

+		case 83: {

 			Get();

 			x = t;  y = Token.NoToken; 

-			if (la.kind == 83) {

+			if (la.kind == 82) {

 				Get();

 				y = t; 

 			}

@@ -1955,29 +1985,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			

 			break;

 		}

-		case 85: {

+		case 84: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Neq; 

 			break;

 		}

-		case 86: {

+		case 85: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Le; 

 			break;

 		}

-		case 87: {

+		case 86: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(166); break;

+		default: SynErr(165); break;

 		}

 	}

 

 	void Factor(out Expression/*!*/ e0) {

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

 		UnaryExpression(out e0);

-		while (la.kind == 47 || la.kind == 90 || la.kind == 91) {

+		while (la.kind == 47 || la.kind == 89 || la.kind == 90) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -1986,63 +2016,63 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

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

-		if (la.kind == 88) {

+		if (la.kind == 87) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Add; 

-		} else if (la.kind == 89) {

+		} else if (la.kind == 88) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Sub; 

-		} else SynErr(167);

+		} else SynErr(166);

 	}

 

 	void UnaryExpression(out Expression/*!*/ e) {

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

 		switch (la.kind) {

-		case 89: {

+		case 88: {

 			Get();

 			x = t; 

 			UnaryExpression(out e);

 			e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); 

 			break;

 		}

-		case 84: case 92: {

+		case 83: case 91: {

 			NegOp();

 			x = t; 

 			UnaryExpression(out e);

 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

-		case 20: case 39: case 59: case 65: case 66: case 67: case 102: case 103: case 104: case 105: {

+		case 19: case 38: case 54: case 59: case 65: case 66: case 101: case 102: case 103: case 104: {

 			EndlessExpression(out e);

 			break;

 		}

 		case 1: {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 55 || la.kind == 57) {

+			while (la.kind == 43 || la.kind == 56) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 6: case 55: {

+		case 6: case 56: {

 			DisplayExpr(out e);

 			break;

 		}

-		case 40: {

+		case 39: {

 			MultiSetExpr(out e);

 			break;

 		}

-		case 42: {

+		case 41: {

 			MapExpr(out e);

 			break;

 		}

-		case 2: case 18: case 34: case 93: case 94: case 95: case 96: case 97: case 98: case 99: {

+		case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

 			ConstAtomExpression(out e);

-			while (la.kind == 55 || la.kind == 57) {

+			while (la.kind == 43 || la.kind == 56) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		default: SynErr(168); break;

+		default: SynErr(167); break;

 		}

 	}

 

@@ -2051,21 +2081,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 47) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mul; 

-		} else if (la.kind == 90) {

+		} else if (la.kind == 89) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Div; 

-		} else if (la.kind == 91) {

+		} else if (la.kind == 90) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mod; 

-		} else SynErr(169);

+		} else SynErr(168);

 	}

 

 	void NegOp() {

-		if (la.kind == 84) {

+		if (la.kind == 83) {

 			Get();

-		} else if (la.kind == 92) {

+		} else if (la.kind == 91) {

 			Get();

-		} else SynErr(170);

+		} else SynErr(169);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -2080,7 +2110,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(100);

+			Expect(99);

 			Expression(out e0);

 			Expect(60);

 			Expression(out e1);

@@ -2091,11 +2121,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			MatchExpression(out e);

 			break;

 		}

-		case 102: case 103: case 104: case 105: {

+		case 101: case 102: case 103: case 104: {

 			QuantifierGuts(out e);

 			break;

 		}

-		case 39: {

+		case 38: {

 			ComprehensionExpr(out e);

 			break;

 		}

@@ -2103,28 +2133,28 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			x = t; 

 			Expression(out e0);

-			Expect(19);

+			Expect(18);

 			Expression(out e1);

 			e = new AssertExpr(x, e0, e1); 

 			break;

 		}

-		case 67: {

+		case 54: {

 			Get();

 			x = t; 

 			Expression(out e0);

-			Expect(19);

+			Expect(18);

 			Expression(out e1);

 			e = new AssumeExpr(x, e0, e1); 

 			break;

 		}

-		case 20: {

+		case 19: {

 			Get();

 			x = t;

 			letVars = new List<BoundVar>();

 			letRHSs = new List<Expression>(); 

 			IdentTypeOptional(out d);

 			letVars.Add(d); 

-			while (la.kind == 21) {

+			while (la.kind == 20) {

 				Get();

 				IdentTypeOptional(out d);

 				letVars.Add(d); 

@@ -2132,17 +2162,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(52);

 			Expression(out e);

 			letRHSs.Add(e); 

-			while (la.kind == 21) {

+			while (la.kind == 20) {

 				Get();

 				Expression(out e);

 				letRHSs.Add(e); 

 			}

-			Expect(19);

+			Expect(18);

 			Expression(out e);

 			e = new LetExpr(x, letVars, letRHSs, e); 

 			break;

 		}

-		default: SynErr(171); break;

+		default: SynErr(170); break;

 		}

 	}

 

@@ -2153,18 +2183,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Ident(out id);

 		idents.Add(id); 

-		while (la.kind == 57) {

+		while (la.kind == 43) {

 			Get();

 			Ident(out id);

 			idents.Add(id); 

 		}

-		if (la.kind == 34) {

+		if (la.kind == 33) {

 			Get();

 			openParen = t;  args = new List<Expression>(); 

 			if (StartOf(9)) {

 				Expressions(args);

 			}

-			Expect(35);

+			Expect(34);

 		}

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

 	}

@@ -2175,26 +2205,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Expression> multipleIndices = null;

 		bool func = false;

 		

-		if (la.kind == 57) {

+		if (la.kind == 43) {

 			Get();

 			Ident(out id);

-			if (la.kind == 34) {

+			if (la.kind == 33) {

 				Get();

 				IToken openParen = t;  args = new List<Expression/*!*/>();  func = true; 

 				if (StartOf(9)) {

 					Expressions(args);

 				}

-				Expect(35);

+				Expect(34);

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

 			}

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

-		} else if (la.kind == 55) {

+		} else if (la.kind == 56) {

 			Get();

 			x = t; 

 			if (StartOf(9)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (la.kind == 101) {

+				if (la.kind == 100) {

 					Get();

 					anyDots = true; 

 					if (StartOf(9)) {

@@ -2205,8 +2235,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Get();

 					Expression(out ee);

 					e1 = ee; 

-				} else if (la.kind == 21 || la.kind == 56) {

-					while (la.kind == 21) {

+				} else if (la.kind == 20 || la.kind == 57) {

+					while (la.kind == 20) {

 						Get();

 						Expression(out ee);

 						if (multipleIndices == null) {

@@ -2216,15 +2246,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(172);

-			} else if (la.kind == 101) {

+				} else SynErr(171);

+			} else if (la.kind == 100) {

 				Get();

 				anyDots = true; 

 				if (StartOf(9)) {

 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(173);

+			} else SynErr(172);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

@@ -2247,8 +2277,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			

-			Expect(56);

-		} else SynErr(174);

+			Expect(57);

+		} else SynErr(173);

 	}

 

 	void DisplayExpr(out Expression e) {

@@ -2264,15 +2294,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new SetDisplayExpr(x, elements);

 			Expect(7);

-		} else if (la.kind == 55) {

+		} else if (la.kind == 56) {

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

 			if (StartOf(9)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(56);

-		} else SynErr(175);

+			Expect(57);

+		} else SynErr(174);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2280,7 +2310,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

-		Expect(40);

+		Expect(39);

 		x = t; 

 		if (la.kind == 6) {

 			Get();

@@ -2290,15 +2320,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new MultiSetDisplayExpr(x, elements);

 			Expect(7);

-		} else if (la.kind == 34) {

+		} else if (la.kind == 33) {

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

 			Expression(out e);

 			e = new MultiSetFormingExpr(x, e); 

-			Expect(35);

+			Expect(34);

 		} else if (StartOf(19)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

-		} else SynErr(176);

+		} else SynErr(175);

 	}

 

 	void MapExpr(out Expression e) {

@@ -2307,16 +2337,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<ExpressionPair/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

-		Expect(42);

+		Expect(41);

 		x = t; 

-		if (la.kind == 55) {

+		if (la.kind == 56) {

 			Get();

 			elements = new List<ExpressionPair/*!*/>(); 

 			if (StartOf(9)) {

 				MapLiteralExpressions(out elements);

 			}

 			e = new MapDisplayExpr(x, elements);

-			Expect(56);

+			Expect(57);

 		} else if (la.kind == 1) {

 			BoundVar/*!*/ bv;

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

@@ -2325,14 +2355,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			

 			IdentTypeOptional(out bv);

 			bvars.Add(bv); 

-			Expect(18);

+			Expect(17);

 			Expression(out range);

 			QSep();

 			Expression(out body);

 			e = new MapComprehension(x, bvars, range, body); 

 		} else if (StartOf(19)) {

 			SemErr("map must be followed by literal in brackets or comprehension."); 

-		} else SynErr(177);

+		} else SynErr(176);

 	}

 

 	void ConstAtomExpression(out Expression/*!*/ e) {

@@ -2341,17 +2371,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;

 		

 		switch (la.kind) {

-		case 93: {

+		case 92: {

 			Get();

 			e = new LiteralExpr(t, false); 

 			break;

 		}

-		case 94: {

+		case 93: {

 			Get();

 			e = new LiteralExpr(t, true); 

 			break;

 		}

-		case 95: {

+		case 94: {

 			Get();

 			e = new LiteralExpr(t); 

 			break;

@@ -2361,55 +2391,55 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LiteralExpr(t, n); 

 			break;

 		}

-		case 96: {

+		case 95: {

 			Get();

 			e = new ThisExpr(t); 

 			break;

 		}

-		case 97: {

+		case 96: {

 			Get();

 			x = t; 

-			Expect(34);

+			Expect(33);

 			Expression(out e);

-			Expect(35);

+			Expect(34);

 			e = new FreshExpr(x, e); 

 			break;

 		}

-		case 98: {

+		case 97: {

 			Get();

 			x = t; 

-			Expect(34);

+			Expect(33);

 			Expression(out e);

-			Expect(35);

+			Expect(34);

 			e = new AllocatedExpr(x, e); 

 			break;

 		}

-		case 99: {

+		case 98: {

 			Get();

 			x = t; 

-			Expect(34);

+			Expect(33);

 			Expression(out e);

-			Expect(35);

+			Expect(34);

 			e = new OldExpr(x, e); 

 			break;

 		}

-		case 18: {

+		case 17: {

 			Get();

 			x = t; 

 			Expression(out e);

 			e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); 

-			Expect(18);

+			Expect(17);

 			break;

 		}

-		case 34: {

+		case 33: {

 			Get();

 			x = t; 

 			Expression(out e);

 			e = new ParensExpression(x, e); 

-			Expect(35);

+			Expect(34);

 			break;

 		}

-		default: SynErr(178); break;

+		default: SynErr(177); break;

 		}

 	}

 

@@ -2431,7 +2461,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(52);

 		Expression(out r);

 		elements.Add(new ExpressionPair(d,r)); 

-		while (la.kind == 21) {

+		while (la.kind == 20) {

 			Get();

 			Expression(out d);

 			Expect(52);

@@ -2441,11 +2471,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void QSep() {

-		if (la.kind == 106) {

+		if (la.kind == 105) {

 			Get();

-		} else if (la.kind == 107) {

+		} else if (la.kind == 106) {

 			Get();

-		} else SynErr(179);

+		} else SynErr(178);

 	}

 

 	void MatchExpression(out Expression/*!*/ e) {

@@ -2470,13 +2500,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression range;

 		Expression/*!*/ body;

 		

-		if (la.kind == 102 || la.kind == 103) {

+		if (la.kind == 101 || la.kind == 102) {

 			Forall();

 			x = t;  univ = true; 

-		} else if (la.kind == 104 || la.kind == 105) {

+		} else if (la.kind == 103 || la.kind == 104) {

 			Exists();

 			x = t; 

-		} else SynErr(180);

+		} else SynErr(179);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body);

@@ -2496,18 +2526,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ range;

 		Expression body = null;

 		

-		Expect(39);

+		Expect(38);

 		x = t; 

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

-		while (la.kind == 21) {

+		while (la.kind == 20) {

 			Get();

 			IdentTypeOptional(out bv);

 			bvars.Add(bv); 

 		}

-		Expect(18);

+		Expect(17);

 		Expression(out range);

-		if (la.kind == 106 || la.kind == 107) {

+		if (la.kind == 105 || la.kind == 106) {

 			QSep();

 			Expression(out body);

 		}

@@ -2525,16 +2555,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(61);

 		x = t; 

 		Ident(out id);

-		if (la.kind == 34) {

+		if (la.kind == 33) {

 			Get();

 			IdentTypeOptional(out bv);

 			arguments.Add(bv); 

-			while (la.kind == 21) {

+			while (la.kind == 20) {

 				Get();

 				IdentTypeOptional(out bv);

 				arguments.Add(bv); 

 			}

-			Expect(35);

+			Expect(34);

 		}

 		Expect(62);

 		Expression(out body);

@@ -2542,19 +2572,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void Forall() {

-		if (la.kind == 102) {

+		if (la.kind == 101) {

 			Get();

-		} else if (la.kind == 103) {

+		} else if (la.kind == 102) {

 			Get();

-		} else SynErr(181);

+		} else SynErr(180);

 	}

 

 	void Exists() {

-		if (la.kind == 104) {

+		if (la.kind == 103) {

 			Get();

-		} else if (la.kind == 105) {

+		} else if (la.kind == 104) {

 			Get();

-		} else SynErr(182);

+		} else SynErr(181);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2568,7 +2598,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (StartOf(20)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

-			while (la.kind == 21) {

+			while (la.kind == 20) {

 				Get();

 				AttributeArg(out aArg);

 				aArgs.Add(aArg); 

@@ -2590,27 +2620,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	static readonly bool[,]/*!*/ set = {

-		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, T,x,T,T, T,x,x,x, x,T,T,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,T, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

-		{x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, T,x,x,x, T,x,T,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, T,x,x,x, T,x,T,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,x, x,x,x,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, T,x,x,x, T,x,T,T, x,T,T,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

-		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,T,x, T,x,x,x, x,x,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

-		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,T,x, T,x,x,x, x,x,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

-		{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

-		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, T,x,x,x, T,T,T,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},

-		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}

+		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, T,T,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

+		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

+		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

+		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},

+		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}

 

 	};

 } // end Parser

@@ -2649,36 +2679,36 @@ public class Errors {
 			case 11: s = "\"imports\" expected"; break;

 			case 12: s = "\"class\" expected"; break;

 			case 13: s = "\"static\" expected"; break;

-			case 14: s = "\"unlimited\" expected"; break;

-			case 15: s = "\"datatype\" expected"; break;

-			case 16: s = "\"codatatype\" expected"; break;

-			case 17: s = "\"=\" expected"; break;

-			case 18: s = "\"|\" expected"; break;

-			case 19: s = "\";\" expected"; break;

-			case 20: s = "\"var\" expected"; break;

-			case 21: s = "\",\" expected"; break;

-			case 22: s = "\"type\" expected"; break;

-			case 23: s = "\"<\" expected"; break;

-			case 24: s = "\">\" expected"; break;

-			case 25: s = "\"method\" expected"; break;

-			case 26: s = "\"constructor\" expected"; break;

-			case 27: s = "\"returns\" expected"; break;

-			case 28: s = "\"...\" expected"; break;

-			case 29: s = "\"modifies\" expected"; break;

-			case 30: s = "\"free\" expected"; break;

-			case 31: s = "\"requires\" expected"; break;

-			case 32: s = "\"ensures\" expected"; break;

-			case 33: s = "\"decreases\" expected"; break;

-			case 34: s = "\"(\" expected"; break;

-			case 35: s = "\")\" expected"; break;

-			case 36: s = "\"bool\" expected"; break;

-			case 37: s = "\"nat\" expected"; break;

-			case 38: s = "\"int\" expected"; break;

-			case 39: s = "\"set\" expected"; break;

-			case 40: s = "\"multiset\" expected"; break;

-			case 41: s = "\"seq\" expected"; break;

-			case 42: s = "\"map\" expected"; break;

-			case 43: s = "\"object\" expected"; break;

+			case 14: s = "\"datatype\" expected"; break;

+			case 15: s = "\"codatatype\" expected"; break;

+			case 16: s = "\"=\" expected"; break;

+			case 17: s = "\"|\" expected"; break;

+			case 18: s = "\";\" expected"; break;

+			case 19: s = "\"var\" expected"; break;

+			case 20: s = "\",\" expected"; break;

+			case 21: s = "\"type\" expected"; break;

+			case 22: s = "\"<\" expected"; break;

+			case 23: s = "\">\" expected"; break;

+			case 24: s = "\"method\" expected"; break;

+			case 25: s = "\"constructor\" expected"; break;

+			case 26: s = "\"returns\" expected"; break;

+			case 27: s = "\"...\" expected"; break;

+			case 28: s = "\"modifies\" expected"; break;

+			case 29: s = "\"free\" expected"; break;

+			case 30: s = "\"requires\" expected"; break;

+			case 31: s = "\"ensures\" expected"; break;

+			case 32: s = "\"decreases\" expected"; break;

+			case 33: s = "\"(\" expected"; break;

+			case 34: s = "\")\" expected"; break;

+			case 35: s = "\"bool\" expected"; break;

+			case 36: s = "\"nat\" expected"; break;

+			case 37: s = "\"int\" expected"; break;

+			case 38: s = "\"set\" expected"; break;

+			case 39: s = "\"multiset\" expected"; break;

+			case 40: s = "\"seq\" expected"; break;

+			case 41: s = "\"map\" expected"; break;

+			case 42: s = "\"object\" expected"; break;

+			case 43: s = "\".\" expected"; break;

 			case 44: s = "\"function\" expected"; break;

 			case 45: s = "\"predicate\" expected"; break;

 			case 46: s = "\"reads\" expected"; break;

@@ -2689,10 +2719,10 @@ public class Errors {
 			case 51: s = "\"return\" expected"; break;

 			case 52: s = "\":=\" expected"; break;

 			case 53: s = "\":|\" expected"; break;

-			case 54: s = "\"new\" expected"; break;

-			case 55: s = "\"[\" expected"; break;

-			case 56: s = "\"]\" expected"; break;

-			case 57: s = "\".\" expected"; break;

+			case 54: s = "\"assume\" expected"; break;

+			case 55: s = "\"new\" expected"; break;

+			case 56: s = "\"[\" expected"; break;

+			case 57: s = "\"]\" expected"; break;

 			case 58: s = "\"choose\" expected"; break;

 			case 59: s = "\"if\" expected"; break;

 			case 60: s = "\"else\" expected"; break;

@@ -2702,122 +2732,121 @@ public class Errors {
 			case 64: s = "\"invariant\" expected"; break;

 			case 65: s = "\"match\" expected"; break;

 			case 66: s = "\"assert\" expected"; break;

-			case 67: s = "\"assume\" expected"; break;

-			case 68: s = "\"print\" expected"; break;

-			case 69: s = "\"parallel\" expected"; break;

-			case 70: s = "\"<==>\" expected"; break;

-			case 71: s = "\"\\u21d4\" expected"; break;

-			case 72: s = "\"==>\" expected"; break;

-			case 73: s = "\"\\u21d2\" expected"; break;

-			case 74: s = "\"&&\" expected"; break;

-			case 75: s = "\"\\u2227\" expected"; break;

-			case 76: s = "\"||\" expected"; break;

-			case 77: s = "\"\\u2228\" expected"; break;

-			case 78: s = "\"==\" expected"; break;

-			case 79: s = "\"<=\" expected"; break;

-			case 80: s = "\">=\" expected"; break;

-			case 81: s = "\"!=\" expected"; break;

-			case 82: s = "\"!!\" expected"; break;

-			case 83: s = "\"in\" expected"; break;

-			case 84: s = "\"!\" expected"; break;

-			case 85: s = "\"\\u2260\" expected"; break;

-			case 86: s = "\"\\u2264\" expected"; break;

-			case 87: s = "\"\\u2265\" expected"; break;

-			case 88: s = "\"+\" expected"; break;

-			case 89: s = "\"-\" expected"; break;

-			case 90: s = "\"/\" expected"; break;

-			case 91: s = "\"%\" expected"; break;

-			case 92: s = "\"\\u00ac\" expected"; break;

-			case 93: s = "\"false\" expected"; break;

-			case 94: s = "\"true\" expected"; break;

-			case 95: s = "\"null\" expected"; break;

-			case 96: s = "\"this\" expected"; break;

-			case 97: s = "\"fresh\" expected"; break;

-			case 98: s = "\"allocated\" expected"; break;

-			case 99: s = "\"old\" expected"; break;

-			case 100: s = "\"then\" expected"; break;

-			case 101: s = "\"..\" expected"; break;

-			case 102: s = "\"forall\" expected"; break;

-			case 103: s = "\"\\u2200\" expected"; break;

-			case 104: s = "\"exists\" expected"; break;

-			case 105: s = "\"\\u2203\" expected"; break;

-			case 106: s = "\"::\" expected"; break;

-			case 107: s = "\"\\u2022\" expected"; break;

-			case 108: s = "??? expected"; break;

-			case 109: s = "invalid Dafny"; break;

-			case 110: s = "this symbol not expected in ClassDecl"; break;

-			case 111: s = "this symbol not expected in DatatypeDecl"; break;

-			case 112: s = "invalid DatatypeDecl"; break;

-			case 113: s = "this symbol not expected in DatatypeDecl"; break;

-			case 114: s = "this symbol not expected in ArbitraryTypeDecl"; break;

-			case 115: s = "invalid ClassMemberDecl"; break;

+			case 67: s = "\"print\" expected"; break;

+			case 68: s = "\"parallel\" expected"; break;

+			case 69: s = "\"<==>\" expected"; break;

+			case 70: s = "\"\\u21d4\" expected"; break;

+			case 71: s = "\"==>\" expected"; break;

+			case 72: s = "\"\\u21d2\" expected"; break;

+			case 73: s = "\"&&\" expected"; break;

+			case 74: s = "\"\\u2227\" expected"; break;

+			case 75: s = "\"||\" expected"; break;

+			case 76: s = "\"\\u2228\" expected"; break;

+			case 77: s = "\"==\" expected"; break;

+			case 78: s = "\"<=\" expected"; break;

+			case 79: s = "\">=\" expected"; break;

+			case 80: s = "\"!=\" expected"; break;

+			case 81: s = "\"!!\" expected"; break;

+			case 82: s = "\"in\" expected"; break;

+			case 83: s = "\"!\" expected"; break;

+			case 84: s = "\"\\u2260\" expected"; break;

+			case 85: s = "\"\\u2264\" expected"; break;

+			case 86: s = "\"\\u2265\" expected"; break;

+			case 87: s = "\"+\" expected"; break;

+			case 88: s = "\"-\" expected"; break;

+			case 89: s = "\"/\" expected"; break;

+			case 90: s = "\"%\" expected"; break;

+			case 91: s = "\"\\u00ac\" expected"; break;

+			case 92: s = "\"false\" expected"; break;

+			case 93: s = "\"true\" expected"; break;

+			case 94: s = "\"null\" expected"; break;

+			case 95: s = "\"this\" expected"; break;

+			case 96: s = "\"fresh\" expected"; break;

+			case 97: s = "\"allocated\" expected"; break;

+			case 98: s = "\"old\" expected"; break;

+			case 99: s = "\"then\" expected"; break;

+			case 100: s = "\"..\" expected"; break;

+			case 101: s = "\"forall\" expected"; break;

+			case 102: s = "\"\\u2200\" expected"; break;

+			case 103: s = "\"exists\" expected"; break;

+			case 104: s = "\"\\u2203\" expected"; break;

+			case 105: s = "\"::\" expected"; break;

+			case 106: s = "\"\\u2022\" expected"; break;

+			case 107: s = "??? expected"; break;

+			case 108: s = "invalid Dafny"; break;

+			case 109: s = "this symbol not expected in ClassDecl"; break;

+			case 110: s = "this symbol not expected in DatatypeDecl"; break;

+			case 111: s = "invalid DatatypeDecl"; break;

+			case 112: s = "this symbol not expected in DatatypeDecl"; break;

+			case 113: s = "this symbol not expected in ArbitraryTypeDecl"; break;

+			case 114: s = "invalid ClassMemberDecl"; break;

+			case 115: s = "this symbol not expected in FieldDecl"; break;

 			case 116: s = "this symbol not expected in FieldDecl"; break;

-			case 117: s = "this symbol not expected in FieldDecl"; break;

+			case 117: s = "invalid FunctionDecl"; break;

 			case 118: s = "invalid FunctionDecl"; break;

 			case 119: s = "invalid FunctionDecl"; break;

-			case 120: s = "invalid FunctionDecl"; break;

-			case 121: s = "this symbol not expected in MethodDecl"; break;

+			case 120: s = "this symbol not expected in MethodDecl"; break;

+			case 121: s = "invalid MethodDecl"; break;

 			case 122: s = "invalid MethodDecl"; break;

-			case 123: s = "invalid MethodDecl"; break;

-			case 124: s = "invalid TypeAndToken"; break;

+			case 123: s = "invalid TypeAndToken"; break;

+			case 124: s = "this symbol not expected in MethodSpec"; break;

 			case 125: s = "this symbol not expected in MethodSpec"; break;

 			case 126: s = "this symbol not expected in MethodSpec"; break;

 			case 127: s = "this symbol not expected in MethodSpec"; break;

-			case 128: s = "this symbol not expected in MethodSpec"; break;

-			case 129: s = "invalid MethodSpec"; break;

-			case 130: s = "this symbol not expected in MethodSpec"; break;

-			case 131: s = "invalid MethodSpec"; break;

-			case 132: s = "invalid ReferenceType"; break;

+			case 128: s = "invalid MethodSpec"; break;

+			case 129: s = "this symbol not expected in MethodSpec"; break;

+			case 130: s = "invalid MethodSpec"; break;

+			case 131: s = "invalid ReferenceType"; break;

+			case 132: s = "this symbol not expected in FunctionSpec"; break;

 			case 133: s = "this symbol not expected in FunctionSpec"; break;

 			case 134: s = "this symbol not expected in FunctionSpec"; break;

 			case 135: s = "this symbol not expected in FunctionSpec"; break;

 			case 136: s = "this symbol not expected in FunctionSpec"; break;

-			case 137: s = "this symbol not expected in FunctionSpec"; break;

-			case 138: s = "invalid FunctionSpec"; break;

-			case 139: s = "invalid PossiblyWildFrameExpression"; break;

-			case 140: s = "invalid PossiblyWildExpression"; break;

-			case 141: s = "this symbol not expected in OneStmt"; break;

-			case 142: s = "invalid OneStmt"; break;

-			case 143: s = "this symbol not expected in OneStmt"; break;

-			case 144: s = "invalid OneStmt"; break;

-			case 145: s = "invalid AssertStmt"; break;

+			case 137: s = "invalid FunctionSpec"; break;

+			case 138: s = "invalid PossiblyWildFrameExpression"; break;

+			case 139: s = "invalid PossiblyWildExpression"; break;

+			case 140: s = "this symbol not expected in OneStmt"; break;

+			case 141: s = "invalid OneStmt"; break;

+			case 142: s = "this symbol not expected in OneStmt"; break;

+			case 143: s = "invalid OneStmt"; break;

+			case 144: s = "invalid AssertStmt"; break;

+			case 145: s = "invalid UpdateStmt"; break;

 			case 146: s = "invalid UpdateStmt"; break;

-			case 147: s = "invalid UpdateStmt"; break;

+			case 147: s = "invalid IfStmt"; break;

 			case 148: s = "invalid IfStmt"; break;

-			case 149: s = "invalid IfStmt"; break;

+			case 149: s = "invalid WhileStmt"; break;

 			case 150: s = "invalid WhileStmt"; break;

-			case 151: s = "invalid WhileStmt"; break;

-			case 152: s = "invalid Rhs"; break;

-			case 153: s = "invalid Lhs"; break;

-			case 154: s = "invalid Guard"; break;

+			case 151: s = "invalid Rhs"; break;

+			case 152: s = "invalid Lhs"; break;

+			case 153: s = "invalid Guard"; break;

+			case 154: s = "this symbol not expected in LoopSpec"; break;

 			case 155: s = "this symbol not expected in LoopSpec"; break;

 			case 156: s = "this symbol not expected in LoopSpec"; break;

 			case 157: s = "this symbol not expected in LoopSpec"; break;

 			case 158: s = "this symbol not expected in LoopSpec"; break;

-			case 159: s = "this symbol not expected in LoopSpec"; break;

-			case 160: s = "this symbol not expected in Invariant"; break;

-			case 161: s = "invalid AttributeArg"; break;

-			case 162: s = "invalid EquivOp"; break;

-			case 163: s = "invalid ImpliesOp"; break;

-			case 164: s = "invalid AndOp"; break;

-			case 165: s = "invalid OrOp"; break;

-			case 166: s = "invalid RelOp"; break;

-			case 167: s = "invalid AddOp"; break;

-			case 168: s = "invalid UnaryExpression"; break;

-			case 169: s = "invalid MulOp"; break;

-			case 170: s = "invalid NegOp"; break;

-			case 171: s = "invalid EndlessExpression"; break;

+			case 159: s = "this symbol not expected in Invariant"; break;

+			case 160: s = "invalid AttributeArg"; break;

+			case 161: s = "invalid EquivOp"; break;

+			case 162: s = "invalid ImpliesOp"; break;

+			case 163: s = "invalid AndOp"; break;

+			case 164: s = "invalid OrOp"; break;

+			case 165: s = "invalid RelOp"; break;

+			case 166: s = "invalid AddOp"; break;

+			case 167: s = "invalid UnaryExpression"; break;

+			case 168: s = "invalid MulOp"; break;

+			case 169: s = "invalid NegOp"; break;

+			case 170: s = "invalid EndlessExpression"; break;

+			case 171: s = "invalid Suffix"; break;

 			case 172: s = "invalid Suffix"; break;

 			case 173: s = "invalid Suffix"; break;

-			case 174: s = "invalid Suffix"; break;

-			case 175: s = "invalid DisplayExpr"; break;

-			case 176: s = "invalid MultiSetExpr"; break;

-			case 177: s = "invalid MapExpr"; break;

-			case 178: s = "invalid ConstAtomExpression"; break;

-			case 179: s = "invalid QSep"; break;

-			case 180: s = "invalid QuantifierGuts"; break;

-			case 181: s = "invalid Forall"; break;

-			case 182: s = "invalid Exists"; break;

+			case 174: s = "invalid DisplayExpr"; break;

+			case 175: s = "invalid MultiSetExpr"; break;

+			case 176: s = "invalid MapExpr"; break;

+			case 177: s = "invalid ConstAtomExpression"; break;

+			case 178: s = "invalid QSep"; break;

+			case 179: s = "invalid QuantifierGuts"; break;

+			case 180: s = "invalid Forall"; break;

+			case 181: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 6cf71fa1..fb46ba4b 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -222,7 +222,6 @@ namespace Microsoft.Dafny {
       var isPredicate = f is Predicate;

       Indent(indent);

       string k = isPredicate ? "predicate" : "function";

-      if (f.IsUnlimited) { k = "unlimited " + k; }

       if (f.IsStatic) { k = "static " + k; }

       if (!f.IsGhost) { k += " method"; }

       PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs);

@@ -421,9 +420,9 @@ namespace Microsoft.Dafny {
     /// </summary>

     public void PrintStatement(Statement stmt, int indent) {

       Contract.Requires(stmt != null);

-      for (LabelNode label = stmt.Labels; label != null; label = label.Next) {

-        if (label.Label != null) {

-          wr.WriteLine("label {0}:", label.Label);

+      for (LList<Label> label = stmt.Labels; label != null; label = label.Next) {

+        if (label.Data.Name != null) {

+          wr.WriteLine("label {0}:", label.Data.Name);

           Indent(indent);

         }

       }

@@ -662,7 +661,10 @@ namespace Microsoft.Dafny {
       } else if (s is AssignSuchThatStmt) {

         var update = (AssignSuchThatStmt)s;

         wr.Write(" :| ");

-        PrintExpression(update.Assume.Expr);

+        if (update.AssumeToken != null) {

+          wr.Write("assume ");

+        }

+        PrintExpression(update.Expr);

       } else {

         Contract.Assert(s == null);  // otherwise, unknown type

       }

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index d966a76f..51b22443 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -186,19 +186,19 @@ namespace Microsoft.Dafny {
         return t;

       } else if (t is SetType) {

         var tt = (SetType)t;

-        return new SetType(tt.Arg);

+        return new SetType(CloneType(tt.Arg));

       } else if (t is SeqType) {

         var tt = (SeqType)t;

-        return new SeqType(tt.Arg);

+        return new SeqType(CloneType(tt.Arg));

       } else if (t is MultiSetType) {

         var tt = (MultiSetType)t;

-        return new MultiSetType(tt.Arg);

+        return new MultiSetType(CloneType(tt.Arg));

       } else if (t is MapType) {

         var tt = (MapType)t;

-        return new MapType(tt.Domain, tt.Range);

+        return new MapType(CloneType(tt.Domain), CloneType(tt.Range));

       } else if (t is UserDefinedType) {

         var tt = (UserDefinedType)t;

-        return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType));

+        return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.ModuleName == null ? null : Tok(tt.ModuleName));

       } else if (t is InferredTypeProxy) {

         return new InferredTypeProxy();

       } else {

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

       } else if (stmt is AssignSuchThatStmt) {

         var s = (AssignSuchThatStmt)stmt;

-        r = new AssignSuchThatStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Assume.Expr));

+        r = new AssignSuchThatStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Expr), s.AssumeToken == null ? null : Tok(s.AssumeToken));

 

       } else if (stmt is UpdateStmt) {

         var s = (UpdateStmt)stmt;

@@ -513,13 +513,13 @@ namespace Microsoft.Dafny {
       return r;

     }

 

-    void AddStmtLabels(Statement s, LabelNode node) {

+    void AddStmtLabels(Statement s, LList<Label> node) {

       if (node != null) {

         AddStmtLabels(s, node.Next);

-        if (node.Label == null) {

+        if (node.Data.Name == null) {

           // this indicates an implicit-target break statement that has been resolved; don't add it

         } else {

-          s.Labels = new LabelNode(Tok(node.Tok), node.Label, s.Labels);

+          s.Labels = new LList<Label>(new Label(Tok(node.Data.Tok), node.Data.Name), s.Labels);

         }

       }

     }

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

 

       if (f is Predicate) {

-        return new Predicate(tok, f.Name, f.IsStatic, isGhost, f.IsUnlimited, tps, f.OpenParen, formals,

+        return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,

           req, reads, ens, decreases, body, moreBody != null, null, false);

       } else {

-        return new Function(tok, f.Name, f.IsStatic, isGhost, f.IsUnlimited, tps, f.OpenParen, formals, CloneType(f.ResultType),

+        return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),

           req, reads, ens, decreases, body, null, false);

       }

     }

@@ -638,9 +638,6 @@ namespace Microsoft.Dafny {
               if (prevFunction.IsStatic != f.IsStatic) {

                 reporter.Error(f, "a function in a refining module cannot be changed from static to non-static or vice versa: {0}", f.Name);

               }

-              if (prevFunction.IsUnlimited != f.IsUnlimited) {

-                reporter.Error(f, "a function in a refining module cannot be changed from unlimited to limited or vice versa: {0}", f.Name);

-              }

               if (!prevFunction.IsGhost && f.IsGhost) {

                 reporter.Error(f, "a function method cannot be changed into a (ghost) function in a refining module: {0}", f.Name);

               } else if (prevFunction.IsGhost && !f.IsGhost && prevFunction.Body != null) {

@@ -917,7 +914,7 @@ namespace Microsoft.Dafny {
                   doMerge = true;

                 } else if (cOld.Update is AssignSuchThatStmt) {

                   doMerge = true;

-                  addedAssert = CloneExpr(((AssignSuchThatStmt)cOld.Update).Assume.Expr);

+                  addedAssert = CloneExpr(((AssignSuchThatStmt)cOld.Update).Expr);

                 } else {

                   var updateOld = (UpdateStmt)cOld.Update;  // if cast fails, there are more ConcreteUpdateStatement subclasses than expected

                   if (updateOld.Rhss.Count == 1 && updateOld.Rhss[0] is HavocRhs) {

@@ -1090,8 +1087,8 @@ namespace Microsoft.Dafny {
       Contract.Requires(labels != null);

       Contract.Requires(0 <= loopLevels);

 

-      for (LabelNode n = s.Labels; n != null; n = n.Next) {

-        labels.Push(n.Label);

+      for (LList<Label> n = s.Labels; n != null; n = n.Next) {

+        labels.Push(n.Data.Name);

       }

 

       if (s is SkeletonStatement) {

@@ -1116,7 +1113,7 @@ namespace Microsoft.Dafny {
         }

       }

 

-      for (LabelNode n = s.Labels; n != null; n = n.Next) {

+      for (LList<Label> n = s.Labels; n != null; n = n.Next) {

         labels.Pop();

       }

     }

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 7be3fca2..f0990aa0 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -322,7 +322,7 @@ namespace Microsoft.Dafny {
 

               // create and add the query "method" (field, really)

               string queryName = ctor.Name + "?";

-              var query = new SpecialField(ctor.tok, queryName, "_" + ctor.Name, "", "", false, false, Type.Bool, null);

+              var query = new SpecialField(ctor.tok, queryName, "is_" + ctor.CompileName, "", "", false, false, Type.Bool, null);

               query.EnclosingClass = dt;  // resolve here

               members.Add(queryName, query);

               ctor.QueryField = query;

@@ -937,7 +937,7 @@ namespace Microsoft.Dafny {
             Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");

           }

         }

-        TypeParameter tp = allTypeParameters.Find(t.Name);

+        TypeParameter tp = t.ModuleName == null ? allTypeParameters.Find(t.Name) : null;

         if (tp != null) {

           if (t.TypeArgs.Count == 0) {

             t.ResolvedParam = tp;

@@ -945,11 +945,32 @@ namespace Microsoft.Dafny {
             Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name);

           }

         } else if (t.ResolvedClass == null) {  // this test is because 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string')

-          TopLevelDecl d;

-          if (!classes.TryGetValue(t.Name, out d)) {

+          TopLevelDecl d = null;

+          if (t.ModuleName != null) {

+            foreach (var imp in currentClass.Module.Imports) {

+              if (imp.Name == t.ModuleName.val) {

+                // now search among the types declared in module "imp"

+                foreach (var tld in imp.TopLevelDecls) {  // this search is slow, but oh well

+                  if (tld.Name == t.Name) {

+                    // found the class

+                    d = tld;

+                    goto DONE_WITH_QUALIFIED_NAME;

+                  }

+                }

+                Error(t.tok, "Undeclared class name {0} in module {1}", t.Name, t.ModuleName.val);

+                goto DONE_WITH_QUALIFIED_NAME;

+              }

+            }

+            Error(t.ModuleName, "Undeclared module name: {0} (did you forget a module import?)", t.ModuleName.val);

+          DONE_WITH_QUALIFIED_NAME: ;

+          } else if (!classes.TryGetValue(t.Name, out d)) {

             Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget a module import?)", t.Name);

+          }

+

+          if (d == null) {

+            // error has been reported above

           } else if (d is AmbiguousTopLevelDecl) {

-            Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames());

+            Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames());

           } else if (d is ArbitraryTypeDecl) {

             t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType;  // resolve like a type parameter

           } else {

@@ -973,7 +994,7 @@ namespace Microsoft.Dafny {
                   Contract.Assert(d.TypeArgs.Count <= defaultTypeArguments.Count);

                   // automatically supply a prefix of the arguments from defaultTypeArguments

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

-                    var typeArg = new UserDefinedType(t.tok, defaultTypeArguments[i].Name, new List<Type>());

+                    var typeArg = new UserDefinedType(t.tok, defaultTypeArguments[i].Name, new List<Type>(), null);

                     typeArg.ResolvedParam = defaultTypeArguments[i];  // resolve "typeArg" here

                     t.TypeArgs.Add(typeArg);

                   }

@@ -1355,7 +1376,7 @@ namespace Microsoft.Dafny {
             Statement target = loopStack[loopStack.Count - s.BreakCount];

             if (target.Labels == null) {

               // make sure there is a label, because the compiler and translator will want to see a unique ID

-              target.Labels = new LabelNode(target.Tok, null, null);

+              target.Labels = new LList<Label>(new Label(target.Tok, null), null);

             }

             s.TargetStmt = target;

             if (specContextOnly && !target.IsGhost && !inSpecOnlyContext[target]) {

@@ -1818,13 +1839,15 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();

       }

     }

-

     private void ResolveUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, Method method)

     {

       int prevErrorCount = ErrorCount;

       // First, resolve all LHS's and expression-looking RHS's.

       SeqSelectExpr arrayRangeLhs = null;

+      var update = s as UpdateStmt;

+

       foreach (var lhs in s.Lhss) {

+        var ec = ErrorCount;

         if (lhs is SeqSelectExpr) {

           var sse = (SeqSelectExpr)lhs;

           ResolveSeqSelectExpr(sse, true, true);

@@ -1834,14 +1857,34 @@ namespace Microsoft.Dafny {
         } else {

           ResolveExpression(lhs, true);

         }

+        if (update == null && ec == ErrorCount && specContextOnly && !AssignStmt.LhsIsToGhost(lhs)) {

+          Error(lhs, "cannot assign to non-ghost variable in a ghost context");

+        }

       }

       IToken firstEffectfulRhs = null;

       CallRhs callRhs = null;

-      var update = s as UpdateStmt;

       // Resolve RHSs

       if (update == null) {

         var suchThat = (AssignSuchThatStmt)s;  // this is the other possible subclass

-        s.ResolvedStatements.Add(suchThat.Assume);

+        ResolveExpression(suchThat.Expr, true);

+        if (suchThat.AssumeToken == null) {

+          // to ease in the verification, only allow local variables as LHSs

+          var lhsNames = new Dictionary<string, object>();

+          foreach (var lhs in s.Lhss) {

+            if (!(lhs.Resolved is IdentifierExpr)) {

+              Error(lhs, "the assign-such-that statement currently only supports local-variable LHSs");

+            }

+            else {

+              var ie = (IdentifierExpr)lhs.Resolved;

+              if (lhsNames.ContainsKey(ie.Name)) {

+                 // disallow same LHS.

+                Error(s, "duplicate variable in left-hand side of assign-such-that statement: {0}", ie.Name);

+              } else {

+                lhsNames.Add(ie.Name, null);

+              }

+            }

+          }

+        }

       } else {

         foreach (var rhs in update.Rhss) {

           bool isEffectful;

@@ -1877,13 +1920,14 @@ namespace Microsoft.Dafny {
         var ie = lhs.Resolved as IdentifierExpr;

         if (ie != null) {

           if (lhsNameSet.ContainsKey(ie.Name)) {

-            Error(s, "Duplicate variable in left-hand side of {1} statement: {0}", ie.Name, callRhs != null ? "call" : "assignment");

+            if (callRhs != null)

+              // only allow same LHS in a multiassignment, not a call statement

+              Error(s, "duplicate variable in left-hand side of call statement: {0}", ie.Name);

           } else {

             lhsNameSet.Add(ie.Name, null);

           }

         }

       }

-

       if (update != null) {

         // figure out what kind of UpdateStmt this is

         if (firstEffectfulRhs == null) {

@@ -2158,17 +2202,18 @@ namespace Microsoft.Dafny {
       foreach (Statement ss in blockStmt.Body) {

         labeledStatements.PushMarker();

         // push labels

-        for (var lnode = ss.Labels; lnode != null; lnode = lnode.Next) {

-          Contract.Assert(lnode.Label != null);  // LabelNode's with .Label==null are added only during resolution of the break statements with 'stmt' as their target, which hasn't happened yet

-          var prev = labeledStatements.Find(lnode.Label);

+        for (var l = ss.Labels; l != null; l = l.Next) {

+          var lnode = l.Data;

+          Contract.Assert(lnode.Name != null);  // LabelNode's with .Label==null are added only during resolution of the break statements with 'stmt' as their target, which hasn't happened yet

+          var prev = labeledStatements.Find(lnode.Name);

           if (prev == ss) {

             Error(lnode.Tok, "duplicate label");

           } else if (prev != null) {

             Error(lnode.Tok, "label shadows an enclosing label");

           } else {

-            bool b = labeledStatements.Push(lnode.Label, ss);

+            bool b = labeledStatements.Push(lnode.Name, ss);

             Contract.Assert(b);  // since we just checked for duplicates, we expect the Push to succeed

-            if (lnode == ss.Labels) {  // add it only once

+            if (l == ss.Labels) {  // add it only once

               inSpecOnlyContext.Add(ss, specContextOnly);

             }

           }

@@ -2338,7 +2383,7 @@ namespace Microsoft.Dafny {
             }

             if (!callsConstructor && rr.EType is UserDefinedType) {

               var udt = (UserDefinedType)rr.EType;

-              var cl = (ClassDecl)udt.ResolvedClass;  // cast is guarantted by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test

+              var cl = (ClassDecl)udt.ResolvedClass;  // cast is guaranteed by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test

               if (cl.HasConstructor) {

                 Error(stmt, "when allocating an object of type '{0}', one of its constructor methods must be called", cl.Name);

               }

@@ -2594,7 +2639,7 @@ namespace Microsoft.Dafny {
             dtv.InferredTypeArgs.Add(t);

             subst.Add(dt.TypeArgs[i], t);

           }

-          expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt);

+          expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt, null);

           ResolveType(expr.tok, expr.Type, null, true);

 

           DatatypeCtor ctor;

@@ -2855,8 +2900,10 @@ namespace Microsoft.Dafny {
 

           case BinaryExpr.Opcode.Eq:

           case BinaryExpr.Opcode.Neq:

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

-              Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);

+            if (!CouldPossiblyBeSameType(e.E0.Type, e.E1.Type)) {

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

+                Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);

+              }

             }

             expr.Type = Type.Bool;

             break;

@@ -3248,6 +3295,35 @@ namespace Microsoft.Dafny {
       }

     }

 

+    private bool CouldPossiblyBeSameType(Type A, Type B) {

+      if (A.IsTypeParameter || B.IsTypeParameter) {

+        return true;

+      }

+      if (A.IsArrayType && B.IsArrayType) {

+        Type a = UserDefinedType.ArrayElementType(A);

+        Type b = UserDefinedType.ArrayElementType(B);

+        return CouldPossiblyBeSameType(a, b);

+      }

+      if (A is UserDefinedType && B is UserDefinedType) {

+        UserDefinedType a = (UserDefinedType)A;

+        UserDefinedType b = (UserDefinedType)B;

+        if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass == b.ResolvedClass) {

+          if (a.TypeArgs.Count != b.TypeArgs.Count) {

+            return false; // this probably doesn't happen if the classes are the same.

+          }

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

+            if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i]))

+              return false;

+          }

+          // all parameters could be the same

+          return true;

+        }

+        // either we don't know what class it is yet, or the classes mismatch

+        return false;

+      }

+      return false;

+    }

+

     /// <summary>

     /// Generate an error for every non-ghost feature used in "expr".

     /// Requires "expr" to have been successfully resolved.

diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 0c91c68c..d35fc22f 100644
--- a/Dafny/Scanner.cs
+++ b/Dafny/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
 public class Scanner {

 	const char EOL = '\n';

 	const int eofSym = 0; /* pdt */

-	const int maxT = 108;

-	const int noSym = 108;

+	const int maxT = 107;

+	const int noSym = 107;

 

 

 	[ContractInvariantMethod]

@@ -494,34 +494,34 @@ public class Scanner {
 			case "imports": t.kind = 11; break;

 			case "class": t.kind = 12; break;

 			case "static": t.kind = 13; break;

-			case "unlimited": t.kind = 14; break;

-			case "datatype": t.kind = 15; break;

-			case "codatatype": t.kind = 16; break;

-			case "var": t.kind = 20; break;

-			case "type": t.kind = 22; break;

-			case "method": t.kind = 25; break;

-			case "constructor": t.kind = 26; break;

-			case "returns": t.kind = 27; break;

-			case "modifies": t.kind = 29; break;

-			case "free": t.kind = 30; break;

-			case "requires": t.kind = 31; break;

-			case "ensures": t.kind = 32; break;

-			case "decreases": t.kind = 33; break;

-			case "bool": t.kind = 36; break;

-			case "nat": t.kind = 37; break;

-			case "int": t.kind = 38; break;

-			case "set": t.kind = 39; break;

-			case "multiset": t.kind = 40; break;

-			case "seq": t.kind = 41; break;

-			case "map": t.kind = 42; break;

-			case "object": t.kind = 43; break;

+			case "datatype": t.kind = 14; break;

+			case "codatatype": t.kind = 15; break;

+			case "var": t.kind = 19; break;

+			case "type": t.kind = 21; break;

+			case "method": t.kind = 24; break;

+			case "constructor": t.kind = 25; break;

+			case "returns": t.kind = 26; break;

+			case "modifies": t.kind = 28; break;

+			case "free": t.kind = 29; break;

+			case "requires": t.kind = 30; break;

+			case "ensures": t.kind = 31; break;

+			case "decreases": t.kind = 32; break;

+			case "bool": t.kind = 35; break;

+			case "nat": t.kind = 36; break;

+			case "int": t.kind = 37; break;

+			case "set": t.kind = 38; break;

+			case "multiset": t.kind = 39; break;

+			case "seq": t.kind = 40; break;

+			case "map": t.kind = 41; break;

+			case "object": t.kind = 42; break;

 			case "function": t.kind = 44; break;

 			case "predicate": t.kind = 45; break;

 			case "reads": t.kind = 46; break;

 			case "label": t.kind = 49; break;

 			case "break": t.kind = 50; break;

 			case "return": t.kind = 51; break;

-			case "new": t.kind = 54; break;

+			case "assume": t.kind = 54; break;

+			case "new": t.kind = 55; break;

 			case "choose": t.kind = 58; break;

 			case "if": t.kind = 59; break;

 			case "else": t.kind = 60; break;

@@ -530,20 +530,19 @@ public class Scanner {
 			case "invariant": t.kind = 64; break;

 			case "match": t.kind = 65; break;

 			case "assert": t.kind = 66; break;

-			case "assume": t.kind = 67; break;

-			case "print": t.kind = 68; break;

-			case "parallel": t.kind = 69; break;

-			case "in": t.kind = 83; break;

-			case "false": t.kind = 93; break;

-			case "true": t.kind = 94; break;

-			case "null": t.kind = 95; break;

-			case "this": t.kind = 96; break;

-			case "fresh": t.kind = 97; break;

-			case "allocated": t.kind = 98; break;

-			case "old": t.kind = 99; break;

-			case "then": t.kind = 100; break;

-			case "forall": t.kind = 102; break;

-			case "exists": t.kind = 104; break;

+			case "print": t.kind = 67; break;

+			case "parallel": t.kind = 68; break;

+			case "in": t.kind = 82; break;

+			case "false": t.kind = 92; break;

+			case "true": t.kind = 93; break;

+			case "null": t.kind = 94; break;

+			case "this": t.kind = 95; break;

+			case "fresh": t.kind = 96; break;

+			case "allocated": t.kind = 97; break;

+			case "old": t.kind = 98; break;

+			case "then": t.kind = 99; break;

+			case "forall": t.kind = 101; break;

+			case "exists": t.kind = 103; break;

 			default: break;

 		}

 	}

@@ -649,15 +648,15 @@ public class Scanner {
 				else if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}

 				else {t.kind = 3; break;}

 			case 19:

-				{t.kind = 19; break;}

+				{t.kind = 18; break;}

 			case 20:

-				{t.kind = 21; break;}

+				{t.kind = 20; break;}

 			case 21:

-				{t.kind = 28; break;}

+				{t.kind = 27; break;}

 			case 22:

-				{t.kind = 34; break;}

+				{t.kind = 33; break;}

 			case 23:

-				{t.kind = 35; break;}

+				{t.kind = 34; break;}

 			case 24:

 				{t.kind = 47; break;}

 			case 25:

@@ -667,63 +666,63 @@ public class Scanner {
 			case 27:

 				{t.kind = 53; break;}

 			case 28:

-				{t.kind = 55; break;}

-			case 29:

 				{t.kind = 56; break;}

+			case 29:

+				{t.kind = 57; break;}

 			case 30:

 				{t.kind = 62; break;}

 			case 31:

 				if (ch == '>') {AddCh(); goto case 32;}

 				else {goto case 0;}

 			case 32:

-				{t.kind = 70; break;}

+				{t.kind = 69; break;}

 			case 33:

-				{t.kind = 71; break;}

+				{t.kind = 70; break;}

 			case 34:

-				{t.kind = 72; break;}

+				{t.kind = 71; break;}

 			case 35:

-				{t.kind = 73; break;}

+				{t.kind = 72; break;}

 			case 36:

 				if (ch == '&') {AddCh(); goto case 37;}

 				else {goto case 0;}

 			case 37:

-				{t.kind = 74; break;}

+				{t.kind = 73; break;}

 			case 38:

-				{t.kind = 75; break;}

+				{t.kind = 74; break;}

 			case 39:

-				{t.kind = 76; break;}

+				{t.kind = 75; break;}

 			case 40:

-				{t.kind = 77; break;}

+				{t.kind = 76; break;}

 			case 41:

-				{t.kind = 80; break;}

+				{t.kind = 79; break;}

 			case 42:

-				{t.kind = 81; break;}

+				{t.kind = 80; break;}

 			case 43:

-				{t.kind = 82; break;}

+				{t.kind = 81; break;}

 			case 44:

-				{t.kind = 85; break;}

+				{t.kind = 84; break;}

 			case 45:

-				{t.kind = 86; break;}

+				{t.kind = 85; break;}

 			case 46:

-				{t.kind = 87; break;}

+				{t.kind = 86; break;}

 			case 47:

-				{t.kind = 88; break;}

+				{t.kind = 87; break;}

 			case 48:

-				{t.kind = 89; break;}

+				{t.kind = 88; break;}

 			case 49:

-				{t.kind = 90; break;}

+				{t.kind = 89; break;}

 			case 50:

-				{t.kind = 91; break;}

+				{t.kind = 90; break;}

 			case 51:

-				{t.kind = 92; break;}

+				{t.kind = 91; break;}

 			case 52:

-				{t.kind = 103; break;}

+				{t.kind = 102; break;}

 			case 53:

-				{t.kind = 105; break;}

+				{t.kind = 104; break;}

 			case 54:

-				{t.kind = 106; break;}

+				{t.kind = 105; break;}

 			case 55:

-				{t.kind = 107; break;}

+				{t.kind = 106; break;}

 			case 56:

 				recEnd = pos; recKind = 5;

 				if (ch == '=') {AddCh(); goto case 26;}

@@ -731,43 +730,43 @@ public class Scanner {
 				else if (ch == ':') {AddCh(); goto case 54;}

 				else {t.kind = 5; break;}

 			case 57:

-				recEnd = pos; recKind = 17;

+				recEnd = pos; recKind = 16;

 				if (ch == '>') {AddCh(); goto case 30;}

 				else if (ch == '=') {AddCh(); goto case 63;}

-				else {t.kind = 17; break;}

+				else {t.kind = 16; break;}

 			case 58:

-				recEnd = pos; recKind = 18;

+				recEnd = pos; recKind = 17;

 				if (ch == '|') {AddCh(); goto case 39;}

-				else {t.kind = 18; break;}

+				else {t.kind = 17; break;}

 			case 59:

-				recEnd = pos; recKind = 23;

+				recEnd = pos; recKind = 22;

 				if (ch == '=') {AddCh(); goto case 64;}

-				else {t.kind = 23; break;}

+				else {t.kind = 22; break;}

 			case 60:

-				recEnd = pos; recKind = 24;

+				recEnd = pos; recKind = 23;

 				if (ch == '=') {AddCh(); goto case 41;}

-				else {t.kind = 24; break;}

+				else {t.kind = 23; break;}

 			case 61:

-				recEnd = pos; recKind = 57;

+				recEnd = pos; recKind = 43;

 				if (ch == '.') {AddCh(); goto case 65;}

-				else {t.kind = 57; break;}

+				else {t.kind = 43; break;}

 			case 62:

-				recEnd = pos; recKind = 84;

+				recEnd = pos; recKind = 83;

 				if (ch == '=') {AddCh(); goto case 42;}

 				else if (ch == '!') {AddCh(); goto case 43;}

-				else {t.kind = 84; break;}

+				else {t.kind = 83; break;}

 			case 63:

-				recEnd = pos; recKind = 78;

+				recEnd = pos; recKind = 77;

 				if (ch == '>') {AddCh(); goto case 34;}

-				else {t.kind = 78; break;}

+				else {t.kind = 77; break;}

 			case 64:

-				recEnd = pos; recKind = 79;

+				recEnd = pos; recKind = 78;

 				if (ch == '=') {AddCh(); goto case 31;}

-				else {t.kind = 79; break;}

+				else {t.kind = 78; break;}

 			case 65:

-				recEnd = pos; recKind = 101;

+				recEnd = pos; recKind = 100;

 				if (ch == '.') {AddCh(); goto case 21;}

-				else {t.kind = 101; break;}

+				else {t.kind = 100; break;}

 

 		}

 		t.val = new String(tval, 0, tlen);

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 0189c11b..c05d9a38 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -574,7 +574,7 @@ namespace Microsoft.Dafny {
         } else if (member is Function) {

           Function f = (Function)member;

           AddFunction(f);

-          if (f.IsRecursive && !f.IsUnlimited) {

+          if (f.IsRecursive) {

             AddLimitedAxioms(f, 2);

             AddLimitedAxioms(f, 1);

           }

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

               AddFunctionAxiom(f, body, f.Ens, null, layerOffset);

             }

-            if (!f.IsRecursive || f.IsUnlimited) { break; }

+            if (!f.IsRecursive) { break; }

           }

           AddFrameAxiom(f);

           AddWellformednessCheck(f);

@@ -666,7 +666,7 @@ namespace Microsoft.Dafny {
         // create and resolve datatype value

         var r = new DatatypeValue(mc.tok, mc.Ctor.EnclosingDatatype.Name, mc.Ctor.Name, rArgs);

         r.Ctor = mc.Ctor;

-        r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/);

+        r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/, null);

 

         Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();

         substMap.Add(formal, r);

@@ -716,7 +716,7 @@ namespace Microsoft.Dafny {
     Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, FunctionAxiomVisibility visibility, Expression body, List<Expression/*!*/>/*!*/ ens, Specialization specialization, int layerOffset) {

       Contract.Requires(f != null);

       Contract.Requires(ens != null);

-      Contract.Requires(layerOffset == 0 || (layerOffset == 1 && f.IsRecursive && !f.IsUnlimited));

+      Contract.Requires(layerOffset == 0 || (layerOffset == 1 && f.IsRecursive));

       Contract.Requires(predef != null);

       Contract.Requires(f.EnclosingClass != null);

 

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

     void AddLimitedAxioms(Function f, int fromLayer) {

       Contract.Requires(f != null);

-      Contract.Requires(f.IsRecursive && !f.IsUnlimited);

+      Contract.Requires(f.IsRecursive);

       Contract.Requires(fromLayer == 1 || fromLayer == 2);

       Contract.Requires(sink != null && predef != null);

       // With fromLayer==1, generate:

@@ -1380,7 +1380,7 @@ namespace Microsoft.Dafny {
     ///        F(h0,formals) == F(h1,formals)

     ///      );

     ///

-    /// If the function is a recursive, non-unlimited function, then the same axiom is also produced for "F#limited" instead of "F".

+    /// If the function is a recursive function, then the same axiom is also produced for "F#limited" instead of "F".

     /// </summary>

     void AddFrameAxiom(Function f)

     {

@@ -1459,7 +1459,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, heapSucc),

           Bpl.Expr.Imp(q0, eq)));

         sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, axiomComment));

-        if (axiomComment != null && f.IsRecursive && !f.IsUnlimited) {

+        if (axiomComment != null && f.IsRecursive) {

           fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, 0), TrType(f.ResultType)));

           axiomComment = null;  // the comment goes only with the first frame axiom

         } else {

@@ -2933,7 +2933,7 @@ namespace Microsoft.Dafny {
       Bpl.Function func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res);

       sink.TopLevelDeclarations.Add(func);

 

-      if (f.IsRecursive && !f.IsUnlimited) {

+      if (f.IsRecursive) {

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

       }

@@ -3403,7 +3403,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is BreakStmt) {

         AddComment(builder, stmt, "break statement");

         var s = (BreakStmt)stmt;

-        builder.Add(new GotoCmd(s.Tok, new StringSeq("after_" + s.TargetStmt.Labels.UniqueId)));

+        builder.Add(new GotoCmd(s.Tok, new StringSeq("after_" + s.TargetStmt.Labels.Data.UniqueId)));

       } else if (stmt is ReturnStmt) {

         var s = (ReturnStmt)stmt;

         AddComment(builder, stmt, "return statement");

@@ -3414,7 +3414,11 @@ namespace Microsoft.Dafny {
       } else if (stmt is AssignSuchThatStmt) {

         var s = (AssignSuchThatStmt)stmt;

         AddComment(builder, s, "assign-such-that statement");

-        // treat like a parallel havoc, followed by an assume

+        // Essentially, treat like an assert, a parallel havoc, and an assume.  However, we also need to check

+        // the well-formedness of the expression, which is easiest to do after the havoc.  So, we do the havoc

+        // first, then the well-formedness check, then the assert (unless the whole statement is an assume), and

+        // finally the assume.

+

         // Here comes the havoc part

         var lhss = new List<Expression>();

         var havocRhss = new List<AssignmentRhs>();

@@ -3424,10 +3428,40 @@ namespace Microsoft.Dafny {
         }

         List<AssignToLhs> lhsBuilder;

         List<Bpl.IdentifierExpr> bLhss;

-        ProcessLhss(lhss, false, builder, locals, etran, out lhsBuilder, out bLhss);

+        Bpl.Expr[] ignore1, ignore2;

+        string[] ignore3;

+        ProcessLhss(lhss, false, true, builder, locals, etran, out lhsBuilder, out bLhss, out ignore1, out ignore2, out ignore3);

         ProcessRhss(lhsBuilder, bLhss, lhss, havocRhss, builder, locals, etran);

+        // Here comes the well-formedness check

+        TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);

+        // Here comes the assert part

+        if (s.AssumeToken == null) {

+          var substMap = new Dictionary<IVariable, Expression>();

+          var bvars = new List<BoundVar>();

+          foreach (var lhs in s.Lhss) {

+            var l = lhs.Resolved;

+            if (l is IdentifierExpr) {

+              var x = (IdentifierExpr)l;

+              BoundVar bv;

+              IdentifierExpr ie;

+              CloneVariableAsBoundVar(x.tok, x.Var, "$as#" + x.Name, out bv, out ie);

+              bvars.Add(bv);

+              substMap.Add(x.Var, ie);

+            } else {

+              // other forms of LHSs have been ruled out by the resolver (it would be possible to

+              // handle them, but it would involve heap-update expressions--the translation would take

+              // effort, and it's not certain that the existential would be successful in verification).

+              Contract.Assume(false);  // unexpected case

+            }

+          }

+          var bvs = new VariableSeq();

+          var typeAntecedent = etran.TrBoundVariables(bvars, bvs);

+          var substE = etran.TrExpr(Substitute(s.Expr, null, substMap));

+          var ex = new Bpl.ExistsExpr(s.Tok, bvs, BplAnd(typeAntecedent, substE));

+          builder.Add(Assert(s.Tok, ex, "cannot establish the existence of LHS values that satisfy the such-that predicate"));

+        }

         // End by doing the assume

-        TrStmt(s.Assume, builder, locals, etran);

+        builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Expr)));

         builder.Add(CaptureState(s.Tok));  // just do one capture state--here, at the very end (that is, don't do one before the assume)

 

       } else if (stmt is UpdateStmt) {

@@ -3443,11 +3477,28 @@ namespace Microsoft.Dafny {
           foreach (var lhs in s.Lhss) {

             lhss.Add(lhs.Resolved);

           }

-          bool rhssCanAffectPreviouslyKnownExpressions = s.Rhss.Exists(rhs => rhs.CanAffectPreviouslyKnownExpressions);

           List<AssignToLhs> lhsBuilder;

           List<Bpl.IdentifierExpr> bLhss;

-          ProcessLhss(lhss, rhssCanAffectPreviouslyKnownExpressions, builder, locals, etran, out lhsBuilder, out bLhss);

-          ProcessRhss(lhsBuilder, bLhss, lhss, s.Rhss, builder, locals, etran);

+          // note: because we have more than one expression, we always must assign to Boogie locals in a two

+          // phase operation. Thus rhssCanAffectPreviouslyKnownExpressions is just true.

+          Contract.Assert(1 < lhss.Count);

+

+          Bpl.Expr[] lhsObjs, lhsFields;

+          string[] lhsNames;

+          ProcessLhss(lhss, true, false, builder, locals, etran, out lhsBuilder, out bLhss, out lhsObjs, out lhsFields, out lhsNames);

+          // We know that, because the translation saves to a local variable, that the RHS always need to

+          // generate a new local, i.e. bLhss is just all nulls.

+          Contract.Assert(Contract.ForAll(bLhss, lhs => lhs == null));

+          // This generates the assignments, and gives them to us as finalRhss.

+          var finalRhss = ProcessUpdateAssignRhss(lhss, s.Rhss, builder, locals, etran);

+          // ProcessLhss has laid down framing conditions and the ProcessUpdateAssignRhss will check subranges (nats),

+          // but we need to generate the distinctness condition (two LHS are equal only when the RHS is also

+          // equal). We need both the LHS and the RHS to do this, which is why we need to do it here.

+          CheckLhssDistinctness(finalRhss, lhss, builder, etran, lhsObjs, lhsFields, lhsNames);

+          // Now actually perform the assignments to the LHS.

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

+            lhsBuilder[i](finalRhss[i], builder, etran);

+          }

           builder.Add(CaptureState(s.Tok));

         }

 

@@ -3471,7 +3522,7 @@ namespace Microsoft.Dafny {
         foreach (Statement ss in ((BlockStmt)stmt).Body) {

           TrStmt(ss, builder, locals, etran);

           if (ss.Labels != null) {

-            builder.AddLabelCmd("after_" + ss.Labels.UniqueId);

+            builder.AddLabelCmd("after_" + ss.Labels.Data.UniqueId);

           }

         }

       } else if (stmt is IfStmt) {

@@ -4235,7 +4286,9 @@ namespace Microsoft.Dafny {
     void TrCallStmt(CallStmt s, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran, Bpl.Expr actualReceiver) {

       List<AssignToLhs> lhsBuilders;

       List<Bpl.IdentifierExpr> bLhss;

-      ProcessLhss(s.Lhs, true, builder, locals, etran, out lhsBuilders, out bLhss);

+      Bpl.Expr[] ignore1, ignore2;

+      string[] ignore3;

+      ProcessLhss(s.Lhs, true, true, builder, locals, etran, out lhsBuilders, out bLhss, out ignore1, out ignore2, out ignore3);

       Contract.Assert(s.Lhs.Count == lhsBuilders.Count);

       Contract.Assert(s.Lhs.Count == bLhss.Count);

       var lhsTypes = new List<Type>();

@@ -4869,8 +4922,10 @@ namespace Microsoft.Dafny {
       List<AssignToLhs> lhsBuilder;

       List<Bpl.IdentifierExpr> bLhss;

       var lhss = new List<Expression>() { lhs };

-      ProcessLhss(lhss, rhs.CanAffectPreviouslyKnownExpressions, builder, locals, etran,

-        out lhsBuilder, out bLhss);

+      Bpl.Expr[] ignore1, ignore2;

+      string[] ignore3;

+      ProcessLhss(lhss, rhs.CanAffectPreviouslyKnownExpressions, true, builder, locals, etran,

+        out lhsBuilder, out bLhss, out ignore1, out ignore2, out ignore3);

       Contract.Assert(lhsBuilder.Count == 1 && bLhss.Count == 1);  // guaranteed by postcondition of ProcessLhss

 

       var rhss = new List<AssignmentRhs>() { rhs };

@@ -4919,16 +4974,104 @@ namespace Microsoft.Dafny {
       }

     }

 

+    List<Bpl.IdentifierExpr> ProcessUpdateAssignRhss(List<Expression> lhss, List<AssignmentRhs> rhss,

+      Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {

+      Contract.Requires(cce.NonNullElements(lhss));

+      Contract.Requires(cce.NonNullElements(rhss));

+      Contract.Requires(builder != null);

+      Contract.Requires(cce.NonNullElements(locals));

+      Contract.Requires(etran != null);

+      Contract.Requires(predef != null);

+      Contract.Ensures(Contract.ForAll(Contract.Result<List<Bpl.IdentifierExpr>>(), i => i != null));

+

+      var finalRhss = new List<Bpl.IdentifierExpr>();

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

+        var lhs = lhss[i];

+        // the following assumes are part of the precondition, really

+        Contract.Assume(!(lhs is ConcreteSyntaxExpression));

+        Contract.Assume(!(lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne));  // array-range assignments are not allowed

+

+        Type lhsType = null;

+        if (lhs is IdentifierExpr) {

+          lhsType = lhs.Type;

+        } else if (lhs is FieldSelectExpr) {

+          var fse = (FieldSelectExpr)lhs;

+          lhsType = fse.Field.Type;

+        }

+        var bRhs = TrAssignmentRhs(rhss[i].Tok, null, lhsType, rhss[i], lhs.Type, builder, locals, etran);

+        finalRhss.Add(bRhs);

+      }

+      return finalRhss;

+    }

+

+

+    private void CheckLhssDistinctness(List<Bpl.IdentifierExpr> rhs, List<Expression> lhss, StmtListBuilder builder, ExpressionTranslator etran,

+      Bpl.Expr[] objs, Bpl.Expr[] fields, string[] names) {

+      Contract.Requires(cce.NonNullElements(lhss));

+      Contract.Requires(builder != null);

+      Contract.Requires(etran != null);

+      Contract.Requires(predef != null);

+      

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

+        var lhs = lhss[i];

+        Contract.Assume(!(lhs is ConcreteSyntaxExpression));

+        IToken tok = lhs.tok;

+

+        if (lhs is IdentifierExpr) {

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

+            var prev = lhss[j] as IdentifierExpr;

+            if (prev != null && names[i] == names[j]) {

+              builder.Add(Assert(tok, Bpl.Expr.Imp(Bpl.Expr.True, Bpl.Expr.Eq(rhs[i],rhs[j])), string.Format("when left-hand sides {0} and {1} refer to the same location, they must have the same value", j, i)));

+            }

+          }

+        } else if (lhs is FieldSelectExpr) {

+          var fse = (FieldSelectExpr)lhs;

+          // check that this LHS is not the same as any previous LHSs

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

+            var prev = lhss[j] as FieldSelectExpr;

+            if (prev != null && prev.Field == fse.Field) {

+              builder.Add(Assert(tok, Bpl.Expr.Imp(Bpl.Expr.Eq(objs[j], objs[i]), Bpl.Expr.Eq(rhs[i], rhs[j])), string.Format("when left-hand sides {0} and {1} refer to the same location, they must have the same value", j, i)));

+            }

+          }

+        } else if (lhs is SeqSelectExpr) {

+          SeqSelectExpr sel = (SeqSelectExpr)lhs;

+          // check that this LHS is not the same as any previous LHSs

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

+            var prev = lhss[j] as SeqSelectExpr;

+            if (prev != null) {

+              builder.Add(Assert(tok,

+                Bpl.Expr.Imp(Bpl.Expr.And(Bpl.Expr.Eq(objs[j], objs[i]), Bpl.Expr.Eq(fields[j], fields[i])), Bpl.Expr.Eq(rhs[i], rhs[j])),

+                string.Format("when left-hand sides {0} and {1} may refer to the same location, they must have the same value", j, i)));

+            }

+          }

+        } else {

+          MultiSelectExpr mse = (MultiSelectExpr)lhs;

+          // check that this LHS is not the same as any previous LHSs

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

+            var prev = lhss[j] as MultiSelectExpr;

+            if (prev != null) {

+              builder.Add(Assert(tok,

+                Bpl.Expr.Imp(Bpl.Expr.And(Bpl.Expr.Eq(objs[j], objs[i]), Bpl.Expr.Eq(fields[j], fields[i])), Bpl.Expr.Eq(rhs[i], rhs[j])),

+                string.Format("when left-hand sides {0} and {1} refer to the same location, they must have the same value", j, i)));

+            }

+          }

+          

+        }

+      }

+    }

+

     delegate void AssignToLhs(Bpl.Expr rhs, Bpl.StmtListBuilder builder, ExpressionTranslator etran);

 

     /// <summary>

     /// Creates a list of protected Boogie LHSs for the given Dafny LHSs.  Along the way,

-    /// builds code that checks that the LHSs are well-defined, denote different locations,

+    /// builds code that checks that the LHSs are well-defined,

     /// and are allowed by the enclosing modifies clause.

+    /// Checks that they denote different locations iff checkDistinctness is true.

     /// </summary>

-    void ProcessLhss(List<Expression> lhss, bool rhsCanAffectPreviouslyKnownExpressions,

+    void ProcessLhss(List<Expression> lhss, bool rhsCanAffectPreviouslyKnownExpressions, bool checkDistinctness,

       Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran,

-      out List<AssignToLhs> lhsBuilders, out List<Bpl.IdentifierExpr/*may be null*/> bLhss) {

+      out List<AssignToLhs> lhsBuilders, out List<Bpl.IdentifierExpr/*may be null*/> bLhss,

+      out Bpl.Expr[] prevObj, out Bpl.Expr[] prevIndex, out string[] prevNames) {

 

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

       Contract.Requires(builder != null);

@@ -4943,17 +5086,31 @@ namespace Microsoft.Dafny {
       // for each Dafny LHS, build a protected Boogie LHS for the eventual assignment

       lhsBuilders = new List<AssignToLhs>();

       bLhss = new List<Bpl.IdentifierExpr>();

-      var prevObj = new Bpl.Expr[lhss.Count];

-      var prevIndex = new Bpl.Expr[lhss.Count];

+      prevObj = new Bpl.Expr[lhss.Count];

+      prevIndex = new Bpl.Expr[lhss.Count];

+      prevNames = new string[lhss.Count];

       int i = 0;

+

+      var lhsNameSet = new Dictionary<string, object>();

+      

       foreach (var lhs in lhss) {

         Contract.Assume(!(lhs is ConcreteSyntaxExpression));

         IToken tok = lhs.tok;

         TrStmt_CheckWellformed(lhs, builder, locals, etran, true);

 

         if (lhs is IdentifierExpr) {

+          var ie = (IdentifierExpr)lhs;

+          // Note, the resolver does not check for duplicate IdentifierExpr's in LHSs, so do it here.

+          if (checkDistinctness) {

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

+              var prev = lhss[j] as IdentifierExpr;

+              if (prev != null && ie.Name == prev.Name) {

+                builder.Add(Assert(tok, Bpl.Expr.False, string.Format("left-hand sides {0} and {1} refer to the same location", j, i)));

+              }

+            }

+          }

+          prevNames[i] = ie.Name;

           var bLhs = (Bpl.IdentifierExpr)etran.TrExpr(lhs);  // TODO: is this cast always justified?

-          // Note, the resolver checks for duplicate IdentifierExpr's in LHSs

           bLhss.Add(rhsCanAffectPreviouslyKnownExpressions ? null : bLhs);

           lhsBuilders.Add(delegate(Bpl.Expr rhs, Bpl.StmtListBuilder bldr, ExpressionTranslator et) {

             builder.Add(Bpl.Cmd.SimpleAssign(tok, bLhs, rhs));

@@ -4968,11 +5125,13 @@ namespace Microsoft.Dafny {
           // check that the enclosing modifies clause allows this object to be written:  assert $_Frame[obj]);

           builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing context's modifies clause"));

 

-          // check that this LHS is not the same as any previous LHSs

-          for (int j = 0; j < i; j++) {

-            var prev = lhss[j] as FieldSelectExpr;

-            if (prev != null && prev.Field == fse.Field) {

-              builder.Add(Assert(tok, Bpl.Expr.Neq(prevObj[j], obj), string.Format("left-hand sides {0} and {1} may refer to the same location", j, i)));

+          if (checkDistinctness) {

+            // check that this LHS is not the same as any previous LHSs

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

+              var prev = lhss[j] as FieldSelectExpr;

+              if (prev != null && prev.Field == fse.Field) {

+                builder.Add(Assert(tok, Bpl.Expr.Neq(prevObj[j], obj), string.Format("left-hand sides {0} and {1} may refer to the same location", j, i)));

+              }

             }

           }

 

@@ -4999,16 +5158,17 @@ namespace Microsoft.Dafny {
           // check that the enclosing modifies clause allows this object to be written:  assert $_Frame[obj,index]);

           builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause"));

 

-          // check that this LHS is not the same as any previous LHSs

-          for (int j = 0; j < i; j++) {

-            var prev = lhss[j] as SeqSelectExpr;

-            if (prev != null) {

-              builder.Add(Assert(tok,

-                Bpl.Expr.Or(Bpl.Expr.Neq(prevObj[j], obj), Bpl.Expr.Neq(prevIndex[j], fieldName)),

-                string.Format("left-hand sides {0} and {1} may refer to the same location", j, i)));

+          if (checkDistinctness) {

+            // check that this LHS is not the same as any previous LHSs

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

+              var prev = lhss[j] as SeqSelectExpr;

+              if (prev != null) {

+                builder.Add(Assert(tok,

+                  Bpl.Expr.Or(Bpl.Expr.Neq(prevObj[j], obj), Bpl.Expr.Neq(prevIndex[j], fieldName)),

+                  string.Format("left-hand sides {0} and {1} may refer to the same location", j, i)));

+              }

             }

           }

-

           bLhss.Add(null);

           lhsBuilders.Add(delegate(Bpl.Expr rhs, Bpl.StmtListBuilder bldr, ExpressionTranslator et) {

             var h = (Bpl.IdentifierExpr)et.HeapExpr;  // TODO: is this cast always justified?

@@ -5030,16 +5190,17 @@ namespace Microsoft.Dafny {
           prevIndex[i] = fieldName;

           builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause"));

 

-          // check that this LHS is not the same as any previous LHSs

-          for (int j = 0; j < i; j++) {

-            var prev = lhss[j] as MultiSelectExpr;

-            if (prev != null) {

-              builder.Add(Assert(tok,

-                Bpl.Expr.Or(Bpl.Expr.Neq(prevObj[j], obj), Bpl.Expr.Neq(prevIndex[j], fieldName)),

-                string.Format("left-hand sides {0} and {1} may refer to the same location", j, i)));

+          if (checkDistinctness) {

+            // check that this LHS is not the same as any previous LHSs

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

+              var prev = lhss[j] as MultiSelectExpr;

+              if (prev != null) {

+                builder.Add(Assert(tok,

+                  Bpl.Expr.Or(Bpl.Expr.Neq(prevObj[j], obj), Bpl.Expr.Neq(prevIndex[j], fieldName)),

+                  string.Format("left-hand sides {0} and {1} may refer to the same location", j, i)));

+              }

             }

           }

-

           bLhss.Add(null);

           lhsBuilders.Add(delegate(Bpl.Expr rhs, Bpl.StmtListBuilder bldr, ExpressionTranslator et) {

             var h = (Bpl.IdentifierExpr)et.HeapExpr;  // TODO: is this cast always justified?

@@ -5097,7 +5258,10 @@ namespace Microsoft.Dafny {
 

       } else if (rhs is HavocRhs) {

         builder.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(bLhs)));

-

+        var isNat = CheckSubrange_Expr(tok, bLhs, checkSubrangeType);

+        if (isNat != null) {

+          builder.Add(new Bpl.AssumeCmd(tok, isNat));

+        }

       } else {

         Contract.Assert(rhs is TypeRhs);  // otherwise, an unexpected AssignmentRhs

         TypeRhs tRhs = (TypeRhs)rhs;

@@ -5535,12 +5699,12 @@ namespace Microsoft.Dafny {
 

         } else if (expr is FunctionCallExpr) {

           FunctionCallExpr e = (FunctionCallExpr)expr;

-          int offsetToUse = e.Function.IsRecursive && !e.Function.IsUnlimited ? this.layerOffset : 0;

-          if (e.Function.IsRecursive && !e.Function.IsUnlimited) {

+          int offsetToUse = e.Function.IsRecursive ? this.layerOffset : 0;

+          if (e.Function.IsRecursive) {

             Statistics_CustomLayerFunctionCount++;

           }

           string nm = FunctionName(e.Function, 1 + offsetToUse);

-          if (this.applyLimited_CurrentFunction != null && e.Function.IsRecursive && !e.Function.IsUnlimited) {

+          if (this.applyLimited_CurrentFunction != null && e.Function.IsRecursive) {

             ModuleDecl module = cce.NonNull(e.Function.EnclosingClass).Module;

             if (module == cce.NonNull(applyLimited_CurrentFunction.EnclosingClass).Module) {

               if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(applyLimited_CurrentFunction)) {

diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat
index 9535d677..63f5df23 100644
--- a/Test/VSComp2010/runtest.bat
+++ b/Test/VSComp2010/runtest.bat
@@ -3,8 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy

             Problem3-FindZero.dfy Problem4-Queens.dfy

diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index 611f9251..f5b9d1b9 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -3,8 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (

   echo.

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c451cc62..5f80df86 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -91,8 +91,10 @@ TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the
 TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type

 TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type

 TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+TypeTests.dfy(116,4): Error: cannot assign to non-ghost variable in a ghost context

+TypeTests.dfy(117,7): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-34 resolution/type errors detected in TypeTests.dfy

+36 resolution/type errors detected in TypeTests.dfy

 

 -------------------- NatTypes.dfy --------------------

 NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative

@@ -280,7 +282,7 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(584,18): Error: target object may be null

+SmallTests.dfy(584,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

 SmallTests.dfy(597,10): Error: assertion violation

@@ -712,13 +714,13 @@ Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA
 Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB

 Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB

 Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M

+Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

+Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

+Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

+Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

+Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

 Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)

-Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M

+Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

 Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)

 Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)

 Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)

@@ -730,13 +732,20 @@ Modules0.dfy(250,15): Error: unresolved identifier: X
 Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X

 Modules0.dfy(294,16): Error: member R does not exist in class B

 Modules0.dfy(294,6): Error: expected method call, found expression

+Modules0.dfy(317,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)

+Modules0.dfy(321,13): Error: arguments must have the same type (got Q_Imp.Node and Node)

+Modules0.dfy(322,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)

+Modules0.dfy(323,11): Error: Undeclared module name: Wazzup (did you forget a module import?)

+Modules0.dfy(324,17): Error: Undeclared class name Edon in module Q_Imp

+Modules0.dfy(326,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)

+Modules0.dfy(327,30): Error: member Create does not exist in class Klassy

 Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts

 Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts

 Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts

 Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts

 Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context

 Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context

-30 resolution/type errors detected in Modules0.dfy

+37 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

 Modules1.dfy(74,16): Error: assertion violation

@@ -758,7 +767,7 @@ Modules1.dfy(58,3): Error: failure to decrease termination measure
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 19 verified, 5 errors

+Dafny program verifier finished with 22 verified, 5 errors

 

 -------------------- BadFunction.dfy --------------------

 BadFunction.dfy(6,3): Error: failure to decrease termination measure

@@ -801,14 +810,7 @@ Basics.dfy(100,16): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

-Basics.dfy(113,12): Error: left-hand sides 0 and 1 may refer to the same location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3

-    (0,0): anon11_Else

-    (0,0): anon6

-    (0,0): anon12_Then

-Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location

+Basics.dfy(119,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have the same value

 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

@@ -817,7 +819,7 @@ Execution trace:
     (0,0): anon6

     (0,0): anon12_Then

     (0,0): anon9

-Basics.dfy(133,10): Error: left-hand sides 0 and 1 may refer to the same location

+Basics.dfy(133,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value

 Execution trace:

     (0,0): anon0

 Basics.dfy(145,19): Error: assertion violation

@@ -848,8 +850,11 @@ Execution trace:
     (0,0): anon13_Then

     (0,0): anon8

     (0,0): anon14_Then

+Basics.dfy(226,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 19 verified, 11 errors

+Dafny program verifier finished with 32 verified, 11 errors

 

 -------------------- ControlStructures.dfy --------------------

 ControlStructures.dfy(5,3): Error: missing case in case statement: Blue

@@ -1567,6 +1572,11 @@ Execution trace:
 

 Dafny program verifier finished with 30 verified, 2 errors

 

+-------------------- LiberalEquality.dfy --------------------

+LiberalEquality.dfy(37,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)

+LiberalEquality.dfy(52,14): Error: arguments must have the same type (got array<int> and array<bool>)

+2 resolution/type errors detected in LiberalEquality.dfy

+

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

 Execution trace:

@@ -1708,7 +1718,7 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(584,18): Error: target object may be null

+SmallTests.dfy(584,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

 SmallTests.dfy(597,10): Error: assertion violation

@@ -1856,7 +1866,7 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-out.tmp.dfy(530,18): Error: target object may be null

+out.tmp.dfy(530,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

 out.tmp.dfy(543,10): Error: assertion violation

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index 6aa1e34d..7fca7199 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -110,7 +110,7 @@ method TestMulti(m: Multi, p: Multi)
   assert p.x == 300;

   if (*) {

     p.x, m.y := 10, 10;

-    p.x, m.x := 8, 8;  // error: duplicate assignment (since m and p may be the same)

+    p.x, m.x := 8, 8;

   }

 

   var a, b := new int[20], new int[30];

@@ -184,4 +184,59 @@ method EuclideanTest(a: int, b: int)
    assert 0 <= r < abs(b);

    assert a == b * q + r;

    assert (a/b) * b + a % b == a;

-}
\ No newline at end of file
+}

+

+method havocInMultiassignment()

+{

+   var i: nat, j: nat;

+   i, j := *, 3;

+   assert 0 <= i;

+}

+

+method m()

+{

+  var i: int, j: int;

+  i, j := 3, 6;

+  i, i := 3, 3;

+}

+

+method swap(a: array<int>, i: nat, j: nat)

+  requires a != null && 0 <= i < a.Length && 0 <= j < a.Length;

+  modifies a;

+{

+  a[i], a[j] := a[j], a[i];

+}

+

+class CC {

+  var x : int;

+  var y : int;

+}

+

+method notQuiteSwap(c: CC, d: CC)

+  requires c != null && d != null;

+  modifies c,d;

+{

+  c.x, d.x := c.x, c.x;

+}

+

+method notQuiteSwap2(c: CC, d: CC)

+  requires c != null && d != null;

+  modifies c,d;

+{

+  c.x, d.x := d.x, c.y; // BAD: c and d could be the same.

+}

+

+method OKNowIt'sSwapAgain(c: CC, d: CC)

+  requires c != null && d != null;

+  modifies c,d;

+{

+  c.x, d.x := d.x, c.x;

+}

+

+method notQuiteSwap3(c: CC, d: CC)

+  requires c != null && d != null && c != d;

+  modifies c,d;

+{

+  c.x, d.x := 4, c.y;

+  c.x, c.y := 3, c.y;

+}

diff --git a/Test/dafny0/LiberalEquality.dfy b/Test/dafny0/LiberalEquality.dfy
new file mode 100644
index 00000000..3dc52c80
--- /dev/null
+++ b/Test/dafny0/LiberalEquality.dfy
@@ -0,0 +1,55 @@
+

+class Array<T>

+{

+   var Length: nat;

+}

+

+class Test<T> {

+  var a: Array<int>;

+  var b: Array<T>;

+  predicate valid()

+      reads this, a, b;

+  {

+      a != null && b != null && a != b && a.Length == b.Length

+  }

+}

+

+method m1<T, U>(t: T, u: U)

+   requires t != u;

+{

+   

+}

+

+method m2<T>(t: array<T>, a: array<int>)

+   requires t != null && a != null && t != a && t.Length == a.Length;

+{

+

+}

+

+

+class Weird<T, U, V>

+{

+

+}

+

+

+method m3<T, V>(a: Weird<T, int, V>, b: Weird<T, bool, V>)

+   requires a == b; // Bad: second parameter can't be both bool and int.

+{

+

+}

+

+

+method m4<T, U, V>(a: Weird<T, U, V>, b: Weird<T, bool, V>)

+  requires a == b;

+{

+

+}

+

+

+// Just to make sure nothing went wrong.

+method m5(a: array<int>, b: array<bool>)

+   requires a == b; // Bad: never equal

+{

+

+}

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index b171a9c9..cc66c3c1 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -301,3 +301,31 @@ module Local imports NonLocalA, NonLocalB {
     method Q() { }

   }

 }

+

+// ------ qualified type names ----------------------------------

+

+module Q_Imp {

+  class Node { }

+  datatype List<T> = Nil | Cons(T, List);

+  class Klassy {

+    method Init()

+  }

+}

+

+module Q_M imports Q_Imp {

+  method MyMethod(root: Q_Imp.Node, S: set<Node>)

+    requires root in S;  // error: the element type of S does not agree with the type of root

+  {

+    var i := new Q_Imp.Node;

+    var j := new Node;

+    assert i != j;  // error: i and j have different types

+    var k: LongLostModule.Node;  // error: undeclared module

+    var l: Wazzup.WazzupA;  // error: undeclared module (it has not been imported)

+    var m: Q_Imp.Edon;  // error: undeclared class in module Q_Imp

+    var n: Q_Imp.List;

+    var o := new Q_Imp.List;  // error: not a class declared in module Q_Imp

+    var p := new Q_Imp.Klassy.Create();  // error: Create is not a method

+    var q := new Q_Imp.Klassy.Init();

+  }

+  class Node { }

+}

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 5e2d0fff..e8a88749 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -89,3 +89,23 @@ module B_Visibility imports A_Visibility {
     }

   }

 }

+

+// ------ qualified type names ----------------------------------

+

+module Q_Imp {

+  class Node { }

+  class Klassy {

+    method Init()

+  }

+}

+

+module Q_M imports Q_Imp {

+  method MyMethod(root: Q_Imp.Node, S: set<Q_Imp.Node>)

+    requires root in S;

+  {

+    var i := new Q_Imp.Node;

+    var j := new Node;

+    assert i != j;  // fine

+    var q := new Q_Imp.Klassy.Init();

+  }

+}

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index ab711d02..f260edb5 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -103,6 +103,6 @@ method M1() {
 method M2() {

   var a := new int[100];

   parallel (x | 0 <= x < 100) {

-    a[x] :| a[x] > 0;  // error: not allowed to update heap location in a parallel statement with a(n implicit) assume

+    a[x] :| assume a[x] > 0;  // error: not allowed to update heap location in a parallel statement with an assume

   }

 }

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index f8569b3a..146129b5 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -79,7 +79,7 @@ module Tight refines Loose {
 }

 

 module UnawareClient imports Loose {

-  method Main() {

+  method Main0() {

     var n := new MyNumber.Init();

     assert n.N == 0;  // error: this is not known

     n.Inc();

@@ -90,7 +90,7 @@ module UnawareClient imports Loose {
 }

 

 module AwareClient imports Tight {

-  method Main() {

+  method Main1() {

     var n := new MyNumber.Init();

     assert n.N == 0;

     n.Inc();

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 4d219cd3..e8b618d7 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -542,21 +542,21 @@ method AssignSuchThat0(a: int, b: int) returns (x: int, y: int)
   ensures x == a && y == b;

 {

   if (*) {

-    x, y :| a <= x < a + 1 && b + a <= y + a && y <= b;

+    x, y :| assume a <= x < a + 1 && b + a <= y + a && y <= b;

   } else {

-    var xx, yy :| a <= xx < a + 1 && b + a <= yy + a && yy <= b;

+    var xx, yy :| assume a <= xx < a + 1 && b + a <= yy + a && yy <= b;

     x, y := xx, yy;

   }

 }

 

 method AssignSuchThat1(a: int, b: int) returns (x: int, y: int)

 {

-  var k :| 0 <= k < a - b;  // this acts like an 'assume 0 < a - b;'

+  var k :| assume 0 <= k < a - b;  // this acts like an 'assume 0 < a - b;'

   assert b < a;

-  k :| k == old(2*k);  // note, the 'old' has no effect on local variables like k

+  k :| assume k == old(2*k);  // note, the 'old' has no effect on local variables like k

   assert k == 0;

   var S := {2, 4, 7};

-  var T :| T <= S;

+  var T :| assume T <= S;

   assert 3 !in T;

   assert T == {};  // error: T may be larger

 }

@@ -568,38 +568,38 @@ method AssignSuchThat2(i: int, j: int, ghost S: set<Node>)
   var a := new int[25];

   var t;

   if (0 <= i < j < 25) {

-    a[i], t, a[j], n.next, n :| true;

+    a[i], t, a[j], n.next, n :| assume true;

   }

   if (n != null && n.next != null) {

     assume n in S && n.next in S;

-    n.next.next, n.next :| n != null && n.next != null && n.next.next == n.next;  // error: n.next may equal n (thus aliasing n.next.next and n.next)

+    n.next.next, n.next :| assume n != null && n.next != null && n.next.next == n.next;  // error: n.next may equal n (thus aliasing n.next.next and n.next)

   } else if (0 <= i < 25 && 0 <= j < 25) {

-    t, a[i], a[j] :| t < a[i] < a[j];  // error: i may equal j (thus aliasing a[i] and a[j])

+    t, a[i], a[j] :| assume t < a[i] < a[j];  // error: i may equal j (thus aliasing a[i] and a[j])

   }

 }

 

 method AssignSuchThat3()

 {

   var n := new Node;

-  n, n.next :| n.next == n;  // error: RHS is not well defined (RHS is evaluated after the havocking of the LHS)

+  n, n.next :| assume n.next == n;  // error: RHS is not well defined (RHS is evaluated after the havocking of the LHS)

 }

 

 method AssignSuchThat4()

 {

   var n := new Node;

-  n, n.next :| n != null && n.next == n;  // that's the ticket

+  n, n.next :| assume n != null && n.next == n;  // that's the ticket

 }

 

 method AssignSuchThat5()

 {

   var n := new Node;

-  n :| fresh(n);  // fine

+  n :| assume fresh(n);  // fine

   assert false;  // error

 }

 

 method AssignSuchThat6()

 {

   var n: Node;

-  n :| n != null && fresh(n);  // there is no non-null fresh object, so this amounts to 'assume false;'

+  n :| assume n != null && fresh(n);  // there is no non-null fresh object, so this amounts to 'assume false;'

   assert false;  // no problemo

 }

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 29274381..8434f06c 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -92,3 +92,28 @@ method K(s: set<nat>) {  // error: not allowed to instantiate 'set' with 'nat'
   var b := new nat[100,200];  // error: not allowed the type array2<nat>

 }

 

+// --------------------- more ghost tests, for assign-such-that statements

+

+method M()

+{

+  ghost var b: bool;

+  ghost var k: int, l: int;

+  var m: int;

+

+  // These three statements are allowed by the resolver, but the compiler will complain

+  // if it ever gets them.

+  k :| k < 10;

+  k, m :| 0 <= k < m;

+  m :| m < 10;

+

+  // Because of the ghost guard, these 'if' statements are ghost contexts, so only

+  // assignments to ghosts are allowed.

+  if (b) {

+    k :| k < 10;  // should be allowed

+    k, l :| 0 <= k < l;  // ditto

+  }

+  if (b) {

+    m :| m < 10;  // error: not allowed in ghost context

+    k, m :| 0 <= k < m;  // error: not allowed in ghost context

+  }

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index e4c134f6..ac7c8aed 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -3,7 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

 

 for %%f in (Simple.dfy) do (

   echo.

@@ -22,7 +21,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy

-            Predicates.dfy Skeletons.dfy Maps.dfy) do (

+            Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 9ed6d75a..7c7719ee 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -1,8 +1,4 @@
 

--------------------- BQueue.bpl --------------------

-

-Boogie program verifier finished with 8 verified, 0 errors

-

 -------------------- Queue.dfy --------------------

 

 Dafny program verifier finished with 22 verified, 0 errors

diff --git a/Test/dafny1/BQueue.bpl b/Test/dafny1/BQueue.bpl
deleted file mode 100644
index 77f1efb3..00000000
--- a/Test/dafny1/BQueue.bpl
+++ /dev/null
@@ -1,430 +0,0 @@
-// BQueue.bpl

-// A queue program specified in the style of dynamic frames.

-// Rustan Leino, Michal Moskal, and Wolfram Schulte, 2007.

-

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

-

-type ref;

-const null: ref;

-

-type Field x;

-

-// this variable represents the heap; read its type as \forall \alpha. ref * Field \alpha --> \alpha

-type HeapType = <x>[ref, Field x]x;

-var H: HeapType;

-

-// every object has an 'alloc' field, which says whether or not the object has been allocated

-const unique alloc: Field bool;

-

-// for simplicity, we say that every object has one field representing its abstract value and one

-// field representing its footprint (aka frame aka data group).

-

-const unique abstractValue: Field Seq;

-const unique footprint: Field [ref]bool;

-

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

-

-type T;  // the type of the elements of the queue

-const NullT: T;  // some value of type T

-

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

-

-// Queue:

-const unique head: Field ref;

-const unique tail: Field ref;

-const unique mynodes: Field [ref]bool;

-// Node:

-const unique data: Field T;

-const unique next: Field ref;

-

-function ValidQueue(HeapType, ref) returns (bool);

-axiom (forall h: HeapType, q: ref ::

-  { ValidQueue(h, q) }

-  q != null && h[q,alloc] ==>

-  (ValidQueue(h, q) <==>

-     h[q,head] != null && h[h[q,head],alloc] &&

-     h[q,tail] != null && h[h[q,tail],alloc] &&

-     h[h[q,tail], next] == null &&

-     // The following line can be suppressed now that we have a ValidFootprint invariant

-     (forall o: ref :: { h[q,footprint][o] } o != null && h[q,footprint][o] ==> h[o,alloc]) &&

-     h[q,footprint][q] &&

-     h[q,mynodes][h[q,head]] && h[q,mynodes][h[q,tail]] &&

-     (forall n: ref :: { h[q,mynodes][n] }

-       h[q,mynodes][n] ==>

-           n != null && h[n,alloc] && ValidNode(h, n) &&

-           SubSet(h[n,footprint], h[q,footprint]) &&

-           !h[n,footprint][q] &&

-           (h[n,next] == null ==> n == h[q,tail])

-     ) &&

-     (forall n: ref :: { h[n,next] }

-       h[q,mynodes][n] ==>

-           (h[n,next] != null ==> h[q,mynodes][h[n,next]])

-     ) &&

-     h[q,abstractValue] == h[h[q,head],abstractValue]

-  ));

-

-// frame axiom for ValidQueue

-axiom (forall h0: HeapType, h1: HeapType, n: ref ::

-  { ValidQueue(h0,n), ValidQueue(h1,n) }

-  (forall<alpha> o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o]

-      ==> h0[o,f] == h1[o,f])

-  &&

-  (forall<alpha> o: ref, f: Field alpha :: o != null && h1[o,alloc] && h1[n,footprint][o]

-      ==> h0[o,f] == h1[o,f])

-  ==>

-  ValidQueue(h0,n) == ValidQueue(h1,n));

-

-function ValidNode(HeapType, ref) returns (bool);

-axiom (forall h: HeapType, n: ref ::

-  { ValidNode(h, n) }

-  n != null && h[n,alloc] ==>

-  (ValidNode(h, n) <==>

-     // The following line can be suppressed now that we have a ValidFootprint invariant

-     (forall o: ref :: { h[n,footprint][o] } o != null && h[n,footprint][o] ==> h[o,alloc]) &&

-     h[n,footprint][n] &&

-     (h[n,next] != null ==>

-         h[h[n,next],alloc] &&

-         SubSet(h[h[n,next], footprint], h[n,footprint]) &&

-         !h[h[n,next], footprint][n]) &&

-     (h[n,next] == null ==> EqualSeq(h[n,abstractValue], EmptySeq)) &&

-     (h[n,next] != null ==> EqualSeq(h[n,abstractValue],

-                            Append(Singleton(h[h[n,next],data]), h[h[n,next],abstractValue])))

-  ));

-

-// frame axiom for ValidNode

-axiom (forall h0: HeapType, h1: HeapType, n: ref ::

-  { ValidNode(h0,n), ValidNode(h1,n) }

-  (forall<alpha> o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o]

-      ==> h0[o,f] == h1[o,f])

-  &&

-  (forall<alpha> o: ref, f: Field alpha :: o != null && h1[o,alloc] && h1[n,footprint][o]

-      ==> h0[o,f] == h1[o,f])

-  ==>

-  ValidNode(h0,n) == ValidNode(h1,n));

-

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

-

-procedure MakeQueue() returns (q: ref)

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, EmptySet);

-  ensures q != null && H[q,alloc];

-  ensures AllNewSet(old(H), H[q,footprint]);

-  ensures ValidQueue(H, q);

-  ensures Length(H[q,abstractValue]) == 0;

-{

-  var n: ref;

-

-  assume Fresh(H,q);

-  H[q,alloc] := true;

-

-  call n := MakeNode(NullT);

-  H[q,head] := n;

-  H[q,tail] := n;

-  H[q,mynodes] := SingletonSet(n);

-  H[q,footprint] := UnionSet(SingletonSet(q), H[n,footprint]);

-  H[q,abstractValue] := H[n,abstractValue];

-}

-

-procedure IsEmpty(q: ref) returns (isEmpty: bool)

-  requires ValidFootprints(H);

-  requires q != null && H[q,alloc] && ValidQueue(H, q);

-  ensures isEmpty <==> Length(H[q,abstractValue]) == 0;

-{

-  isEmpty := H[q,head] == H[q,tail];

-}

-

-procedure Enqueue(q: ref, t: T)

-  requires ValidFootprints(H);

-  requires q != null && H[q,alloc] && ValidQueue(H, q);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, old(H)[q,footprint]);

-  ensures DifferenceIsNew(old(H), old(H)[q,footprint], H[q,footprint]);

-  ensures ValidQueue(H, q);

-  ensures EqualSeq(H[q,abstractValue], Append(old(H)[q,abstractValue], Singleton(t)));

-{

-  var n: ref;

-

-  call n := MakeNode(t);

-

-  // foreach m in q.mynodes { m.footprint := m.footprint U n.footprint }

-  call BulkUpdateFootprint(H[q,mynodes], H[n,footprint]);

-  H[q,footprint] := UnionSet(H[q,footprint], H[n,footprint]);

-

-  // foreach m in q.mynodes { m.abstractValue := Append(m.abstractValue, Singleton(t)) }

-  call BulkUpdateAbstractValue(H[q,mynodes], t);

-  H[q,abstractValue] := H[H[q,head],abstractValue];

-

-  H[q,mynodes] := UnionSet(H[q,mynodes], SingletonSet(n));

-

-  H[H[q,tail], next] := n;

-  H[q,tail] := n;

-}

-

-procedure BulkUpdateFootprint(targetSet: [ref]bool, delta: [ref]bool);

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySetField(old(H), H, targetSet, footprint);

-  ensures (forall o: ref ::

-    o != null && old(H)[o,alloc] && targetSet[o]

-    ==> H[o,footprint] == UnionSet(old(H)[o,footprint], delta));

-

-procedure BulkUpdateAbstractValue(targetSet: [ref]bool, t: T);

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySetField(old(H), H, targetSet, abstractValue);

-  ensures (forall o: ref ::

-    o != null && old(H)[o,alloc] && targetSet[o]

-    ==> EqualSeq(H[o,abstractValue], Append(old(H)[o,abstractValue], Singleton(t))));

-

-procedure Front(q: ref) returns (t: T)

-  requires ValidFootprints(H);

-  requires q != null && H[q,alloc] && ValidQueue(H, q);

-  requires 0 < Length(H[q,abstractValue]);

-  ensures t == Index(H[q,abstractValue], 0);

-{

-  t := H[H[H[q,head], next], data];

-}

-

-procedure Dequeue(q: ref)

-  requires ValidFootprints(H);

-  requires q != null && H[q,alloc] && ValidQueue(H, q);

-  requires 0 < Length(H[q,abstractValue]);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, old(H)[q,footprint]);

-  ensures DifferenceIsNew(old(H), old(H)[q,footprint], H[q,footprint]);

-  ensures ValidQueue(H, q);

-  ensures EqualSeq(H[q,abstractValue], Drop(old(H)[q,abstractValue], 1));

-{

-  var n: ref;

-

-  n := H[H[q,head], next];

-  H[q,head] := n;

-  // we could also remove old(H)[q,head] from H[q,mynodes], and similar for the footprints

-  H[q,abstractValue] := H[n,abstractValue];

-}

-

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

-

-procedure MakeNode(t: T) returns (n: ref)

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, EmptySet);

-  ensures n != null && H[n,alloc];

-  ensures AllNewSet(old(H), H[n,footprint]);

-  ensures ValidNode(H, n);

-  ensures H[n,data] == t && H[n,next] == null;

-{

-  assume Fresh(H,n);

-  H[n,alloc] := true;

-

-  H[n,next] := null;

-  H[n,data] := t;

-  H[n,footprint] := SingletonSet(n);

-  H[n,abstractValue] := EmptySeq;

-}

-

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

-

-procedure Main(t: T, u: T, v: T)

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, EmptySet);

-{

-  var q0, q1: ref;

-  var w: T;

-

-  call q0 := MakeQueue();

-  call q1 := MakeQueue();

-

-  call Enqueue(q0, t);

-  call Enqueue(q0, u);

-

-  call Enqueue(q1, v);

-

-  assert Length(H[q0,abstractValue]) == 2;

-

-  call w := Front(q0);

-  assert w == t;

-  call Dequeue(q0);

-

-  call w := Front(q0);

-  assert w == u;

-

-  assert Length(H[q0,abstractValue]) == 1;

-  assert Length(H[q1,abstractValue]) == 1;

-}

-

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

-

-procedure Main2(t: T, u: T, v: T, q0: ref, q1: ref)

-  requires q0 != null && H[q0,alloc] && ValidQueue(H, q0);

-  requires q1 != null && H[q1,alloc] && ValidQueue(H, q1);

-  requires DisjointSet(H[q0,footprint], H[q1,footprint]);

-  requires Length(H[q0,abstractValue]) == 0;

-

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, UnionSet(old(H)[q0,footprint], old(H)[q1,footprint]));

-{

-  var w: T;

-

-  call Enqueue(q0, t);

-  call Enqueue(q0, u);

-

-  call Enqueue(q1, v);

-

-  assert Length(H[q0,abstractValue]) == 2;

-

-  call w := Front(q0);

-  assert w == t;

-  call Dequeue(q0);

-

-  call w := Front(q0);

-  assert w == u;

-

-  assert Length(H[q0,abstractValue]) == 1;

-  assert Length(H[q1,abstractValue]) == old(Length(H[q1,abstractValue])) + 1;

-}

-

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

-

-// Helpful predicates used in specs

-

-function ModifiesOnlySet(oldHeap: HeapType, newHeap: HeapType, set: [ref]bool) returns (bool);

-axiom (forall oldHeap: HeapType, newHeap: HeapType, set: [ref]bool ::

-  { ModifiesOnlySet(oldHeap, newHeap, set) }

-  ModifiesOnlySet(oldHeap, newHeap, set) <==>

-    NoDeallocs(oldHeap, newHeap) &&

-    (forall<alpha> o: ref, f: Field alpha :: { newHeap[o,f] }

-      o != null && oldHeap[o,alloc] ==>

-      oldHeap[o,f] == newHeap[o,f] || set[o]));

-

-function ModifiesOnlySetField<alpha>(oldHeap: HeapType, newHeap: HeapType,

-                                     set: [ref]bool, field: Field alpha) returns (bool);

-axiom (forall<alpha> oldHeap: HeapType, newHeap: HeapType, set: [ref]bool, field: Field alpha ::

-  { ModifiesOnlySetField(oldHeap, newHeap, set, field) }

-  ModifiesOnlySetField(oldHeap, newHeap, set, field) <==>

-    NoDeallocs(oldHeap, newHeap) &&

-    (forall<beta> o: ref, f: Field beta :: { newHeap[o,f] }

-      o != null && oldHeap[o,alloc] ==>

-      oldHeap[o,f] == newHeap[o,f] || (set[o] && f == field)));

-

-function NoDeallocs(oldHeap: HeapType, newHeap: HeapType) returns (bool);

-axiom (forall oldHeap: HeapType, newHeap: HeapType ::

-  { NoDeallocs(oldHeap, newHeap) }

-  NoDeallocs(oldHeap, newHeap) <==>

-    (forall o: ref :: { newHeap[o,alloc] }

-      o != null && oldHeap[o,alloc] ==> newHeap[o,alloc]));

-

-function AllNewSet(oldHeap: HeapType, set: [ref]bool) returns (bool);

-axiom (forall oldHeap: HeapType, set: [ref]bool ::

-  { AllNewSet(oldHeap, set) }

-  AllNewSet(oldHeap, set) <==>

-    (forall o: ref :: { oldHeap[o,alloc] }

-      o != null && set[o] ==> !oldHeap[o,alloc]));

-

-function DifferenceIsNew(oldHeap: HeapType, oldSet: [ref]bool, newSet: [ref]bool) returns (bool);

-axiom (forall oldHeap: HeapType, oldSet: [ref]bool, newSet: [ref]bool ::

-  { DifferenceIsNew(oldHeap, oldSet, newSet) }

-  DifferenceIsNew(oldHeap, oldSet, newSet) <==>

-    (forall o: ref :: { oldHeap[o,alloc] }

-      o != null && !oldSet[o] && newSet[o] ==> !oldHeap[o,alloc]));

-

-function ValidFootprints(h: HeapType) returns (bool);

-axiom (forall h: HeapType ::

-  { ValidFootprints(h) }

-  ValidFootprints(h) <==>

-    (forall o: ref, r: ref :: { h[o,footprint][r] }

-      o != null && h[o,alloc] && r != null && h[o,footprint][r] ==> h[r,alloc]));

-

-function Fresh(h: HeapType, o: ref) returns (bool);

-axiom (forall h: HeapType, o: ref ::

-  { Fresh(h,o) }

-  Fresh(h,o) <==>

-    o != null && !h[o,alloc] && h[o,footprint] == SingletonSet(o));

-

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

-

-const EmptySet: [ref]bool;

-axiom (forall o: ref :: { EmptySet[o] } !EmptySet[o]);

-

-function SingletonSet(ref) returns ([ref]bool);

-axiom (forall r: ref :: { SingletonSet(r) } SingletonSet(r)[r]);

-axiom (forall r: ref, o: ref :: { SingletonSet(r)[o] } SingletonSet(r)[o] <==> r == o);

-

-function UnionSet([ref]bool, [ref]bool) returns ([ref]bool);

-axiom (forall a: [ref]bool, b: [ref]bool, o: ref :: { UnionSet(a,b)[o] }

-  UnionSet(a,b)[o] <==> a[o] || b[o]);

-

-function SubSet([ref]bool, [ref]bool) returns (bool);

-axiom(forall a: [ref]bool, b: [ref]bool :: { SubSet(a,b) }

-  SubSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} a[o] ==> b[o]));

-

-function EqualSet([ref]bool, [ref]bool) returns (bool);

-axiom(forall a: [ref]bool, b: [ref]bool :: { EqualSet(a,b) }

-  EqualSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} a[o] <==> b[o]));

-

-function DisjointSet([ref]bool, [ref]bool) returns (bool);

-axiom (forall a: [ref]bool, b: [ref]bool :: { DisjointSet(a,b) }

-  DisjointSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} !a[o] || !b[o]));

-

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

-

-// Sequence of T

-type Seq;

-

-function Length(Seq) returns (int);

-axiom (forall s: Seq :: { Length(s) } 0 <= Length(s));

-

-const EmptySeq: Seq;

-axiom Length(EmptySeq) == 0;

-axiom (forall s: Seq :: { Length(s) } Length(s) == 0 ==> s == EmptySeq);

-

-function Singleton(T) returns (Seq);

-axiom (forall t: T :: { Length(Singleton(t)) } Length(Singleton(t)) == 1);

-

-function Append(Seq, Seq) returns (Seq);

-axiom (forall s0: Seq, s1: Seq :: { Length(Append(s0,s1)) }

-  Length(Append(s0,s1)) == Length(s0) + Length(s1));

-

-function Index(Seq, int) returns (T);

-axiom (forall t: T :: { Index(Singleton(t), 0) } Index(Singleton(t), 0) == t);

-axiom (forall s0: Seq, s1: Seq, n: int :: { Index(Append(s0,s1), n) }

-  (n < Length(s0) ==> Index(Append(s0,s1), n) == Index(s0, n)) &&

-  (Length(s0) <= n ==> Index(Append(s0,s1), n) == Index(s1, n - Length(s0))));

-

-function EqualSeq(Seq, Seq) returns (bool);

-axiom (forall s0: Seq, s1: Seq :: { EqualSeq(s0,s1) }

-  EqualSeq(s0,s1) <==>

-    Length(s0) == Length(s1) &&

-    (forall j: int :: { Index(s0,j) } { Index(s1,j) }

-        0 <= j && j < Length(s0) ==> Index(s0,j) == Index(s1,j)));

-

-function Take(s: Seq, howMany: int) returns (Seq);

-axiom (forall s: Seq, n: int :: { Length(Take(s,n)) }

-  0 <= n ==>

-    (n <= Length(s) ==> Length(Take(s,n)) == n) &&

-    (Length(s) < n ==> Length(Take(s,n)) == Length(s)));

-axiom (forall s: Seq, n: int, j: int :: { Index(Take(s,n), j) }

-  0 <= j && j < n && j < Length(s) ==>

-    Index(Take(s,n), j) == Index(s, j));

-

-function Drop(s: Seq, howMany: int) returns (Seq);

-axiom (forall s: Seq, n: int :: { Length(Drop(s,n)) }

-  0 <= n ==>

-    (n <= Length(s) ==> Length(Drop(s,n)) == Length(s) - n) &&

-    (Length(s) < n ==> Length(Drop(s,n)) == 0));

-axiom (forall s: Seq, n: int, j: int :: { Index(Drop(s,n), j) }

-  0 <= n && 0 <= j && j < Length(s)-n ==>

-    Index(Drop(s,n), j) == Index(s, j+n));

-

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

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 1f5d78df..d098d753 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -3,14 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

-

-for %%f in (BQueue.bpl) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %BPLEXE% %* %%f

-)

 

 for %%f in (Queue.dfy PriorityQueue.dfy

             ExtensibleArray.dfy ExtensibleArrayAuto.dfy

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index 381b9cb1..9c37549e 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -31,6 +31,22 @@ Dafny program verifier finished with 23 verified, 0 errors
 

 Dafny program verifier finished with 5 verified, 0 errors

 

+-------------------- TreeFill.dfy --------------------

+

+Dafny program verifier finished with 3 verified, 0 errors

+

+-------------------- TuringFactorial.dfy --------------------

+

+Dafny program verifier finished with 3 verified, 0 errors

+

 -------------------- StoreAndRetrieve.dfy --------------------

 

 Dafny program verifier finished with 22 verified, 0 errors

+

+-------------------- MajorityVote.dfy --------------------

+

+Dafny program verifier finished with 11 verified, 0 errors

+

+-------------------- SegmentSum.dfy --------------------

+

+Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
new file mode 100644
index 00000000..a7512486
--- /dev/null
+++ b/Test/dafny2/MajorityVote.dfy
@@ -0,0 +1,171 @@
+// Rustan Leino, June 2012.

+// This file verifies an algorithm, due to Boyer and Moore, that finds the majority choice

+// among a sequence of votes, see http://www.cs.utexas.edu/~moore/best-ideas/mjrty/.

+// Actually, this algorithm is a slight variation on theirs, but the general idea for why

+// it is correct is the same.  In the Boyer and Moore algorithm, the loop counter is advanced

+// by exactly 1 each iteration, which means that there may or may not be a "current leader".

+// In my program below, I had instead written the loop invariant to say there is always a

+// "current leader", which requires the loop index sometimes to skip a value.

+//

+// This file has two versions of the algorithm.  In the first version, the given sequence

+// of votes is assumed to have a (strict) majority choice, meaning that strictly more than

+// 50% of the votes are for one candidate.  It is convenient to have a name for the majority

+// choice, in order to talk about it in specifications.  The easiest way to do this in

+// Dafny is probably to introduce a ghost parameter with the given properties.  That's what

+// the algorithm does, see parameter K.  The postcondition is thus to output the value of

+// K, which is done in the non-ghost out-parameter k.

+// The proof of the algorithm requires two lemmas.  These lemmas are proved automatically

+// by Dafny's induction tactic.

+//

+// In the second version of the program, the main method does not assume there is a majority

+// choice.  Rather, it eseentially uses the first algorithm and then checks if what it

+// returns really is a majority choice.  To do this, the specification of the first algorithm

+// needs to be changed slightly to accommodate the possibility that there is no majority

+// choice.  That change in specification is also reflected in the loop invariant.  Moreover,

+// the algorithm itself now needs to extra 'if' statements to see if the entire sequence

+// has been searched through.  (This extra 'if' is essentially already handled by Boyer and

+// Moore's algorithm, because it increments the loop index by 1 each iteration and therefore

+// already has a special case for the case of running out of sequence elements without a

+// current leader.)

+// The calling harness, DetermineElection, somewhat existentially comes up with the majority

+// choice, if there is such a choice, and then passes in that choice as the ghost parameter K

+// to the main algorithm.  Neat, huh?

+

+// Advanced remark:

+// There is a subtle situation in the verification of DetermineElection.  Suppose the type

+// parameter Candidate denotes some type whose instances depend on which object are

+// allocated.  For example, if Candidate is some class type, then more candidates can come

+// into being by object allocations (using "new").  What does the quantification of

+// candidates "c" in the postcondition of DetermineElection now mean--all candidates that

+// existed in the pre-state or (the possibly larger set of) all candidates that exist in the

+// post-state?  (It means the latter.)  And if there does not exist a candidate in majority

+// in the pre-state, could there be a (newly created) candidate in majority in the post-state?

+// This will require some proof.  The simplest argument seems to be that even if more candidates

+// are created during the course of DetermineElection, such candidates cannot possibly

+// be in majority in the sequence "a", since "a" can only contain candidates that were already

+// created in the pre-state.  This property is easily specified by adding a postcondition

+// to the Count function.  Alternatively, one could have added the antecedent "c in a" or

+// "old(allocated(c))" to the "forall c" quantification in the postcondition of DetermineElection.

+

+function method Count<T>(a: seq<T>, s: int, t: int, x: T): int

+  requires 0 <= s <= t <= |a|;

+  ensures Count(a, s, t, x) == 0 || x in a;

+{

+  if s == t then 0 else

+  Count(a, s, t-1, x) + if a[t-1] == x then 1 else 0

+}

+

+// Here is the first version of the algorithm, the one that assumes there is a majority choice.

+

+method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)

+  requires 2 * Count(a, 0, |a|, K) > |a|;  // K has a (strict) majority of the votes

+  ensures k == K;  // find K

+{

+  k := a[0];

+  var n, c, s := 1, 1, 0;

+  while (n < |a|)

+    invariant 0 <= s <= n <= |a|;

+    invariant 2 * Count(a, s, |a|, K) > |a| - s;  // K has majority among a[s..]

+    invariant 2 * Count(a, s, n, k) > n - s;  // k has majority among a[s..n]

+    invariant c == Count(a, s, n, k);

+  {

+    if (a[n] == k) {

+      n, c := n + 1, c + 1;

+    } else if (2 * c > n + 1 - s) {

+      n := n + 1;

+    } else {

+      n := n + 1;

+      // We have 2*Count(a, s, n, k) == n-s, and thus the following lemma

+      // lets us conclude 2*Count(a, s, n, K) <= n-s.

+      Lemma_Unique(a, s, n, K, k);

+      // We also have 2*Count(a, s, |a|, K) > |a|-s, and the following lemma

+      // tells us Count(a, s, |a|, K) == Count(a, s, n, K) + Count(a, n, |a|, K),

+      // and thus we can conclude 2*Count(a, n, |a|, K) > |a|-n.

+      Lemma_Split(a, s, n, |a|, K);

+      k, n, c, s := a[n], n + 1, 1, n;

+    }

+  }

+  Lemma_Unique(a, s, |a|, K, k);  // both k and K have a majority, so K == k

+}

+

+// ------------------------------------------------------------------------------

+

+// Here is the second version of the program, the one that also computes whether or not

+// there is a majority choice.

+

+method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)

+  ensures hasWinner ==> 2 * Count(a, 0, |a|, cand) > |a|;

+  ensures !hasWinner ==> forall c :: 2 * Count(a, 0, |a|, c) <= |a|;

+{

+  ghost var b := exists c :: 2 * Count(a, 0, |a|, c) > |a|;

+  ghost var w :| b ==> 2 * Count(a, 0, |a|, w) > |a|;

+  cand := SearchForWinner(a, b, w);

+  return 2 * Count(a, 0, |a|, cand) > |a|, cand;

+}

+

+// The difference between SearchForWinner for FindWinner above are the occurrences of the

+// antecedent "hasWinner ==>" and the two checks for no-more-votes that may result in a "return"

+// statement.

+

+method SearchForWinner<Candidate>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)

+  requires hasWinner ==> 2 * Count(a, 0, |a|, K) > |a|;  // K has a (strict) majority of the votes

+  ensures hasWinner ==> k == K;  // find K

+{

+  if (|a| == 0) { return; }

+  k := a[0];

+  var n, c, s := 1, 1, 0;

+  while (n < |a|)

+    invariant 0 <= s <= n <= |a|;

+    invariant hasWinner ==> 2 * Count(a, s, |a|, K) > |a| - s;  // K has majority among a[s..]

+    invariant 2 * Count(a, s, n, k) > n - s;  // k has majority among a[s..n]

+    invariant c == Count(a, s, n, k);

+  {

+    if (a[n] == k) {

+      n, c := n + 1, c + 1;

+    } else if (2 * c > n + 1 - s) {

+      n := n + 1;

+    } else {

+      n := n + 1;

+      // We have 2*Count(a, s, n, k) == n-s, and thus the following lemma

+      // lets us conclude 2*Count(a, s, n, K) <= n-s.

+      Lemma_Unique(a, s, n, K, k);

+      // We also have 2*Count(a, s, |a|, K) > |a|-s, and the following lemma

+      // tells us Count(a, s, |a|, K) == Count(a, s, n, K) + Count(a, n, |a|, K),

+      // and thus we can conclude 2*Count(a, n, |a|, K) > |a|-n.

+      Lemma_Split(a, s, n, |a|, K);

+      if (|a| == n) { return; }

+      k, n, c, s := a[n], n + 1, 1, n;

+    }

+  }

+  Lemma_Unique(a, s, |a|, K, k);  // both k and K have a majority, so K == k

+}

+

+// ------------------------------------------------------------------------------

+

+// Here are two lemmas about Count that are used in the methods above.

+

+ghost method Lemma_Split<T>(a: seq<T>, s: int, t: int, u: int, x: T)

+  requires 0 <= s <= t <= u <= |a|;

+  ensures Count(a, s, t, x) + Count(a, t, u, x) == Count(a, s, u, x);

+{

+  /* The postcondition of this method is proved automatically via Dafny's

+     induction tactic.  But if a manual proof had to be provided, it would

+     look like this:

+  if (s != t) {

+    Lemma_Split(a, s, t-1, u, x);

+  }

+  */

+}

+

+ghost method Lemma_Unique<T>(a: seq<T>, s: int, t: int, x: T, y: T)

+  requires 0 <= s <= t <= |a|;

+  ensures x != y ==> Count(a, s, t, x) + Count(a, s, t, y) <= t - s;

+{

+  /* The postcondition of this method is proved automatically via Dafny's

+     induction tactic.  But if a manual proof had to be provided, it would

+     look like this:

+  if (s != t) {

+    Lemma_Unique(a, s, t-1, x, y);

+  }

+  */

+}

diff --git a/Test/dafny2/SegmentSum.dfy b/Test/dafny2/SegmentSum.dfy
new file mode 100644
index 00000000..dc67162b
--- /dev/null
+++ b/Test/dafny2/SegmentSum.dfy
@@ -0,0 +1,29 @@
+function Sum(a: seq<int>, s: int, t: int): int

+  requires 0 <= s <= t <= |a|;

+{

+  if s == t then 0 else Sum(a, s, t-1) + a[t-1]

+}

+

+method MaxSegSum(a: seq<int>) returns (k: int, m: int)

+  ensures 0 <= k <= m <= |a|;

+  ensures forall p,q :: 0 <= p <= q <= |a| ==> Sum(a, p, q) <= Sum(a, k, m);

+{

+  k, m := 0, 0;

+  var s := 0;  // invariant s == Sum(a, k, m)

+  var n := 0;

+  var c, t := 0, 0;  // invariant t == Sum(a, c, n)

+  while (n < |a|)

+    invariant n <= |a|;

+    invariant 0 <= c <= n && t == Sum(a, c, n);

+    invariant forall b :: 0 <= b <= n ==> Sum(a, b, n) <= Sum(a, c, n);

+    invariant 0 <= k <= m <= n && s == Sum(a, k, m);

+    invariant forall p,q :: 0 <= p <= q <= n ==> Sum(a, p, q) <= Sum(a, k, m);

+  {

+    t, n := t + a[n], n + 1;

+    if (t < 0) {

+      c, t := n, 0;

+    } else if (s < t) {

+      k, m, s := c, n, t;

+    }

+  }

+}

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index ea26a234..15c82d65 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -1,4 +1,4 @@
-module A imports Library {

+ghost module A imports Library {

   class {:autocontracts} StoreAndRetrieve<Thing> {

     ghost var Contents: set<Thing>;

     predicate Valid

diff --git a/Test/dafny2/TreeFill.dfy b/Test/dafny2/TreeFill.dfy
new file mode 100644
index 00000000..f7e2cc89
--- /dev/null
+++ b/Test/dafny2/TreeFill.dfy
@@ -0,0 +1,27 @@
+datatype Tree<T> = Null | Node(Tree, T, Tree);

+

+function Contains<T>(t: Tree, v: T): bool

+{

+  match t

+  case Null => false

+  case Node(left, x, right) => x == v || Contains(left, v) || Contains(right, v)

+}

+

+method Fill<T>(t: Tree, a: array<T>, start: int) returns (end: int)

+  requires a != null && 0 <= start <= a.Length;

+  modifies a;

+  ensures start <= end <= a.Length;

+  ensures forall i :: 0 <= i < start ==> a[i] == old(a[i]);

+  ensures forall i :: start <= i < end ==> Contains(t, a[i]);

+{

+  match (t) {

+    case Null =>

+      end := start;

+    case Node(left, x, right) =>

+      end := Fill(left, a, start);

+      if (end < a.Length) {

+        a[end] := x;

+        end := Fill(right, a, end + 1);

+      }

+  }

+}

diff --git a/Test/dafny2/TuringFactorial.dfy b/Test/dafny2/TuringFactorial.dfy
new file mode 100644
index 00000000..585c998e
--- /dev/null
+++ b/Test/dafny2/TuringFactorial.dfy
@@ -0,0 +1,26 @@
+function Factorial(n: nat): nat

+{

+  if n == 0 then 1 else n * Factorial(n-1)

+}

+

+method ComputeFactorial(n: int) returns (u: int)

+  requires 1 <= n;

+  ensures u == Factorial(n);

+{

+  var r := 1;

+  u := 1;

+  while (r < n)  

+    invariant r <= n;

+    invariant u == Factorial(r);

+  { 

+    var v, s := u, 1;

+    while (s < r + 1)

+      invariant s <= r + 1;

+      invariant v == Factorial(r) && u == s * Factorial(r);

+    {

+      u := u + v;

+      s := s + 1;

+    }

+    r := r + 1;

+  }

+}

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index a4796939..b68ba251 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -3,7 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 REM soon again:    SnapshotableTrees.dfy 

 for %%f in (

@@ -14,8 +13,8 @@ for %%f in (
     COST-verif-comp-2011-2-MaxTree-datatype.dfy

     COST-verif-comp-2011-3-TwoDuplicates.dfy

     COST-verif-comp-2011-4-FloydCycleDetect.dfy

-    Intervals.dfy

-    StoreAndRetrieve.dfy

+    Intervals.dfy TreeFill.dfy TuringFactorial.dfy

+    StoreAndRetrieve.dfy MajorityVote.dfy SegmentSum.dfy

   ) do (

   echo.

   echo -------------------- %%f --------------------

diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy
index e56a8317..3e5a95ef 100644
--- a/Test/vacid0/LazyInitArray.dfy
+++ b/Test/vacid0/LazyInitArray.dfy
@@ -11,10 +11,10 @@ class LazyInitArray<T> {
     reads this, a, b, c;

   {

     a != null && b != null && c != null &&

-    a.Length == |Contents| + 1 &&  // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'

+    a.Length == |Contents| &&

     b.Length == |Contents| &&

     c.Length == |Contents| &&

-    b != c &&

+    b != c && a != b && a != c &&

     0 <= n && n <= c.Length &&

     (forall i :: 0 <= i && i < |Contents| ==>

        Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&

@@ -41,7 +41,7 @@ class LazyInitArray<T> {
     ensures |Contents| == N && Zero == zero;

     ensures (forall x :: x in Contents ==> x == zero);

   {

-    a := new T[N+1];

+    a := new T[N];

     b := new int[N];

     c := new int[N];

     n := 0;

diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat
index efe7b3d5..cd047d39 100644
--- a/Test/vacid0/runtest.bat
+++ b/Test/vacid0/runtest.bat
@@ -3,8 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (

   echo.

diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index 770f41dc..7f7c9b9f 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -3,7 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 for %%f in (

     Two-Way-Sort.dfy

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index f16b09b5..05f06b41 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -30,7 +30,7 @@
 ]\\)*" . font-lock-comment-face)

 

    `(,(dafny-regexp-opt '(

-        "class" "datatype" "codatatype" "type" "function" "predicate" "ghost" "var" "method" "constructor" "unlimited"

+        "class" "datatype" "codatatype" "type" "function" "predicate" "ghost" "var" "method" "constructor"

         "module" "imports" "static" "refines"

         "returns" "requires" "ensures" "modifies" "reads" "free"

         "invariant" "decreases"

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 635115fb..4244e817 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -19,7 +19,7 @@ namespace Demo
         this.MarkReservedWords(  // NOTE: these keywords must also appear once more below

           "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", "type",

           "assert", "assume", "new", "this", "object", "refines",

-          "unlimited", "module", "imports",

+          "module", "imports",

           "if", "then", "else", "while", "invariant",

           "break", "label", "return", "parallel", "havoc", "print",

           "returns", "requires", "ensures", "modifies", "reads", "decreases",

@@ -275,7 +275,6 @@ namespace Demo
           | "this"

           | "object"

           | "refines"

-          | "unlimited"

           | "module"

           | "imports"

           | "if"

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 48faa5ec..d621b1a9 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -288,7 +288,6 @@ namespace DafnyLanguage
                 case "this":

                 case "true":

                 case "type":

-                case "unlimited":

                 case "var":

                 case "while":

                 #endregion

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 4126d2f2..051d60f4 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -6,7 +6,7 @@
 

 \lstdefinelanguage{dafny}{

   morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,%

-      function,predicate,unlimited,

+      function,predicate,

       ghost,var,static,refines,

       method,constructor,returns,module,imports,in,

       requires,modifies,ensures,reads,decreases,free,