5 files changed, 459 insertions, 514 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 5623f091..b7b81d44 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -28,7 +28,6 @@ static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
 static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);

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

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

-static Scope<string>/*!*/ parseVarScope = new Scope<string>();

 static int anonymousIds = 0;

 

 struct MemberModifiers {

@@ -292,11 +291,8 @@ DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
   .)

   { Attribute<ref attrs> }

   Ident<out id>

-  (. parseVarScope.PushMarker(); .)

   [ FormalsOptionalIds<formals> ]

-  (. parseVarScope.PopMarker();

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

-  .)

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

   .

 

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

@@ -321,7 +317,6 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
      List<IToken/*!*/> ids = new List<IToken/*!*/>();;

      IToken/*!*/ id;

      Expression/*!*/ e;

-     parseVarScope.PushMarker();

   .)

   "replaces"

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

@@ -329,15 +324,13 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
      if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }

   .)

   { Attribute<ref attrs> }  

-  Ident<out id>                                     (. ids.Add(id); parseVarScope.Push(id.val, id.val); .)

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

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

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

   }

   "by"    

   Expression<out e>

   ";"

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

-     parseVarScope.PopMarker();

-  .)  

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

   .

 

 

@@ -441,7 +434,6 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
   { Attribute<ref attrs> }

   Ident<out id>

   [ GenericParameters<typeArgs> ]

-  (. parseVarScope.PushMarker(); .)

   Formals<true, true, ins>

   [ "returns"

     Formals<false, true, outs>

@@ -451,8 +443,7 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
   | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb, out bodyStart, out bodyEnd>    (. body = (BlockStmt)bb; .)

   )

   

-  (. parseVarScope.PopMarker();

-     if (isRefinement)

+  (. if (isRefinement)

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

      else 

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

@@ -483,8 +474,8 @@ Formals<.bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals.>
 = (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; .)

   "("

   [

-    GIdentType<allowGhosts, out id, out ty, out isGhost>         (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost));  parseVarScope.Push(id.val, id.val); .)

-    { "," GIdentType<allowGhosts, out id, out ty, out isGhost>   (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost));  parseVarScope.Push(id.val, id.val); .)

+    GIdentType<allowGhosts, out id, out ty, out isGhost>         (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

+    { "," GIdentType<allowGhosts, out id, out ty, out isGhost>   (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)

     }

   ]

   ")"

@@ -494,8 +485,8 @@ FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
 = (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; .)

   "("

   [

-    TypeIdentOptional<out id, out name, out ty, out isGhost>        (. formals.Add(new Formal(id, name, ty, true, isGhost));  parseVarScope.Push(name, name); .)

-    { "," TypeIdentOptional<out id, out name, out ty, out isGhost>  (. formals.Add(new Formal(id, name, ty, true, isGhost));  parseVarScope.Push(name, name); .)

+    TypeIdentOptional<out id, out name, out ty, out isGhost>        (. formals.Add(new Formal(id, name, ty, true, isGhost)); .)

+    { "," TypeIdentOptional<out id, out name, out ty, out isGhost>  (. formals.Add(new Formal(id, name, ty, true, isGhost)); .)

     }

   ]

   ")"

@@ -588,7 +579,6 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   { Attribute<ref attrs> }

   Ident<out id> 

   [ GenericParameters<typeArgs> ]

-  (. parseVarScope.PushMarker(); .)

   Formals<true, false, formals>

   ":"

   Type<out returnType>

@@ -597,8 +587,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   | { FunctionSpec<reqs, reads, ens, decreases> }

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

   )

-  (. parseVarScope.PopMarker();

-     f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);

+  (. f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);

      f.BodyStartTok = bodyStart;

      f.BodyEndTok = bodyEnd;

   .)

@@ -677,18 +666,15 @@ CaseExpression<out MatchCaseExpr/*!*/ c>
      List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();

      Expression/*!*/ body;

   .)

-  "case"                      (. x = t;  parseVarScope.PushMarker(); .)

+  "case"                      (. x = t; .)

   Ident<out id>

   [ "("

-    Ident<out arg>            (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

-                                 parseVarScope.Push(arg.val, arg.val); .)

-    { "," Ident<out arg>      (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

-                                 parseVarScope.Push(arg.val, arg.val); .)

+    Ident<out arg>            (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)

+    { "," Ident<out arg>      (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)

     }

   ")" ]

   "=>"

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

-                                 parseVarScope.PopMarker(); .)

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

   .

 

 /* Note, '(' is start of more than one alternative in MatchOrExpr, but the first intentionally hides

@@ -707,13 +693,11 @@ BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
 = (. Contract.Ensures(Contract.ValueAtReturn(out block) != null);

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

   .)

-  (. parseVarScope.PushMarker(); .)

   "{"                                  (. bodyStart = t; .)

   { Stmt<body>

   }

   "}"                                  (. bodyEnd = t;

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

-  (. parseVarScope.PopMarker(); .)

   .

 

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

@@ -733,8 +717,9 @@ OneStmt<out Statement/*!*/ s>
   | AssumeStmt<out s>

   | UseStmt<out s>

   | PrintStmt<out s>

+  | UpdateStmt<out s>

   | HavocStmt<out s>

-  | "call" UpdateStmt<out s>

+  | VarDeclStatement<out s>

   | IfStmt<out s>

   | WhileStmt<out s>

   | MatchStmt<out s>

@@ -746,8 +731,6 @@ OneStmt<out Statement/*!*/ s>
     ] ";"                              (. s = new BreakStmt(x, label); .)

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

     ";"                                (. s = new ReturnStmt(x); .)

-  | VarDeclStatement<out s>

-  | UpdateStmt<out s>

   )

   .

 

@@ -885,9 +868,7 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives.>
     Expression<out e>

     "=>"

     (. body = new List<Statement>(); .)

-    (. parseVarScope.PushMarker(); .)

     { Stmt<body> }

-    (. parseVarScope.PopMarker(); .)

     (. alternatives.Add(new GuardedAlternative(x, e, body)); .)

   }

   "}"

@@ -963,21 +944,16 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
      List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();

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

   .)

-  "case"                      (. x = t;  parseVarScope.PushMarker(); .)

+  "case"                      (. x = t; .)

   Ident<out id>

   [ "("

-    Ident<out arg>            (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

-                                 parseVarScope.Push(arg.val, arg.val); .)

-    { "," Ident<out arg>      (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

-                                 parseVarScope.Push(arg.val, arg.val); .)

+    Ident<out arg>            (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)

+    { "," Ident<out arg>      (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)

     }

   ")" ]

   "=>"

-    (. parseVarScope.PushMarker(); .)

     { Stmt<body> }

-    (. parseVarScope.PopMarker(); .)

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

-  (. parseVarScope.PopMarker(); .)

   .

 

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

@@ -991,7 +967,6 @@ ForeachStmt<out Statement/*!*/ s>
      List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();

      Statement bodyAssign = null;

   .)

-  (. parseVarScope.PushMarker(); .)

   "foreach"                                    (. x = t;

                                                   range = new LiteralExpr(x, true);

                                                   ty = new InferredTypeProxy();

@@ -999,7 +974,6 @@ ForeachStmt<out Statement/*!*/ s>
   "(" Ident<out boundVar>

       [ ":" Type<out ty> ]

       "in" Expression<out collection>

-                                               (. parseVarScope.Push(boundVar.val, boundVar.val); .)

       [ "|" Expression<out range> ]

   ")"

   "{"

@@ -1016,7 +990,6 @@ ForeachStmt<out Statement/*!*/ s>
                                                     s = dummyStmt;  // some error occurred in parsing the bodyAssign

                                                   }

                                                .)

-  (. parseVarScope.PopMarker(); .)

   .

 

 AssertStmt<out Statement/*!*/ s>

@@ -1322,10 +1295,9 @@ QuantifierGuts<out Expression/*!*/ q>
   ( Forall                                     (. x = t;  univ = true; .)

   | Exists                                     (. x = t; .)

   )

-  (. parseVarScope.PushMarker(); .)

-  IdentTypeOptional<out bv>                    (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)

+  IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)

   { ","

-    IdentTypeOptional<out bv>                  (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)

+    IdentTypeOptional<out bv>                  (. bvars.Add(bv); .)

   }

   { AttributeOrTrigger<ref attrs, ref trigs> }

   [ "|"

@@ -1338,7 +1310,6 @@ QuantifierGuts<out Expression/*!*/ q>
      } else {

        q = new ExistsExpr(x, bvars, range, body, trigs, attrs);

      }

-     parseVarScope.PopMarker();

   .)

   .

 

@@ -1355,10 +1326,9 @@ ComprehensionExpr<out Expression/*!*/ q>
      Expression body = null;

   .)

   "set"                                        (. x = t; .)

-  (. parseVarScope.PushMarker(); .)

-  IdentTypeOptional<out bv>                    (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)

+  IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)

   { ","

-    IdentTypeOptional<out bv>                  (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)

+    IdentTypeOptional<out bv>                  (. bvars.Add(bv); .)

   }

   "|" Expression<out range>

   [

@@ -1367,7 +1337,6 @@ ComprehensionExpr<out Expression/*!*/ q>
   ]

   (. if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }

      q = new SetComprehension(x, bvars, range, body);

-     parseVarScope.PopMarker();

   .)

   .

 

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 2586c67d..2fa88a69 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -20,7 +20,7 @@ public class Parser {
 	public const int _digits = 2;

 	public const int _arrayToken = 3;

 	public const int _string = 4;

-	public const int maxT = 106;

+	public const int maxT = 105;

 

 	const bool T = true;

 	const bool x = false;

@@ -41,7 +41,6 @@ static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
 static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);

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

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

-static Scope<string>/*!*/ parseVarScope = new Scope<string>();

 static int anonymousIds = 0;

 

 struct MemberModifiers {

@@ -363,7 +362,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 				DatatypeMemberDecl(ctors);

 			}

 			Expect(15);

-		} else SynErr(107);

+		} else SynErr(106);

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

 		dt.BodyStartTok = bodyStart;

 		dt.BodyEndTok = t;

@@ -398,7 +397,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			mm.Add(m); 

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

 			CouplingInvDecl(mmod, mm);

-		} else SynErr(108);

+		} else SynErr(107);

 	}

 

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

@@ -467,7 +466,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (la.kind == 23) {

 			GenericParameters(typeArgs);

 		}

-		parseVarScope.PushMarker(); 

 		Formals(true, false, formals);

 		Expect(22);

 		Type(out returnType);

@@ -482,8 +480,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			}

 			FunctionBody(out bb, out bodyStart, out bodyEnd);

 			body = bb; 

-		} else SynErr(109);

-		parseVarScope.PopMarker();

+		} else SynErr(108);

 		f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);

 		f.BodyStartTok = bodyStart;

 		f.BodyEndTok = bodyEnd;

@@ -511,7 +508,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		} else if (la.kind == 10) {

 			Get();

 			isRefinement = true; 

-		} else SynErr(110);

+		} else SynErr(109);

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

 		

 		while (la.kind == 7) {

@@ -521,7 +518,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (la.kind == 23) {

 			GenericParameters(typeArgs);

 		}

-		parseVarScope.PushMarker(); 

 		Formals(true, true, ins);

 		if (la.kind == 26) {

 			Get();

@@ -538,10 +534,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			}

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

 			body = (BlockStmt)bb; 

-		} else SynErr(111);

-		parseVarScope.PopMarker();

+		} else SynErr(110);

 		if (isRefinement)

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

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

 		else 

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

 		m.BodyStartTok = bodyStart;

@@ -555,7 +550,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		List<IToken/*!*/> ids = new List<IToken/*!*/>();;

 		IToken/*!*/ id;

 		Expression/*!*/ e;

-		parseVarScope.PushMarker();

 		

 		Expect(20);

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

@@ -566,18 +560,16 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		ids.Add(id); parseVarScope.Push(id.val, id.val); 

+		ids.Add(id); 

 		while (la.kind == 19) {

 			Get();

 			Ident(out id);

-			ids.Add(id); parseVarScope.Push(id.val, id.val); 

+			ids.Add(id); 

 		}

 		Expect(21);

 		Expression(out e);

 		Expect(15);

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

-		parseVarScope.PopMarker();

-		

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

 	}

 

 	void DatatypeMemberDecl(List<DatatypeCtor/*!*/>/*!*/ ctors) {

@@ -590,13 +582,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		parseVarScope.PushMarker(); 

 		if (la.kind == 32) {

 			FormalsOptionalIds(formals);

 		}

-		parseVarScope.PopMarker();

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

-		

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

 	}

 

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

@@ -604,11 +593,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Expect(32);

 		if (StartOf(7)) {

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

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

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

 			while (la.kind == 19) {

 				Get();

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

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

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

 			}

 		}

 		Expect(33);

@@ -740,7 +729,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			ReferenceType(out tok, out ty);

 			break;

 		}

-		default: SynErr(112); break;

+		default: SynErr(111); break;

 		}

 	}

 

@@ -749,11 +738,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Expect(32);

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

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

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

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

 			while (la.kind == 19) {

 				Get();

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

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

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

 			}

 		}

 		Expect(33);

@@ -791,19 +780,18 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Expression(out e);

 				Expect(15);

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

-			} else SynErr(113);

+			} else SynErr(112);

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

 			Get();

 			Expressions(decreases);

 			Expect(15);

-		} else SynErr(114);

+		} else SynErr(113);

 	}

 

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

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

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

 		

-		parseVarScope.PushMarker(); 

 		Expect(7);

 		bodyStart = t; 

 		while (StartOf(9)) {

@@ -812,7 +800,6 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(8);

 		bodyEnd = t;

 		block = new BlockStmt(bodyStart, body); 

-		parseVarScope.PopMarker(); 

 	}

 

 	void FrameExpression(out FrameExpression/*!*/ fe) {

@@ -878,7 +865,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				GenericInstantiation(gt);

 			}

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

-		} else SynErr(115);

+		} else SynErr(114);

 	}

 

 	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {

@@ -910,7 +897,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 			Expressions(decreases);

 			Expect(15);

-		} else SynErr(116);

+		} else SynErr(115);

 	}

 

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

@@ -921,7 +908,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			MatchExpression(out e);

 		} else if (StartOf(8)) {

 			Expression(out e);

-		} else SynErr(117);

+		} else SynErr(116);

 		Expect(8);

 		bodyEnd = t; 

 	}

@@ -933,7 +920,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			fe = new FrameExpression(new WildcardExpr(t), null); 

 		} else if (StartOf(8)) {

 			FrameExpression(out fe);

-		} else SynErr(118);

+		} else SynErr(117);

 	}

 

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

@@ -944,7 +931,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new WildcardExpr(t); 

 		} else if (StartOf(8)) {

 			Expression(out e);

-		} else SynErr(119);

+		} else SynErr(118);

 	}

 

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

@@ -967,25 +954,22 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expression/*!*/ body;

 		

 		Expect(45);

-		x = t;  parseVarScope.PushMarker(); 

+		x = t; 

 		Ident(out id);

 		if (la.kind == 32) {

 			Get();

 			Ident(out arg);

-			arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

-			parseVarScope.Push(arg.val, arg.val); 

+			arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); 

 			while (la.kind == 19) {

 				Get();

 				Ident(out arg);

-				arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

-				parseVarScope.Push(arg.val, arg.val); 

+				arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); 

 			}

 			Expect(33);

 		}

 		Expect(46);

 		MatchOrExpr(out body);

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

-		parseVarScope.PopMarker(); 

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

 	}

 

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

@@ -998,7 +982,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			MatchExpression(out e);

 		} else if (StartOf(8)) {

 			Expression(out e);

-		} else SynErr(120);

+		} else SynErr(119);

 	}

 

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

@@ -1015,34 +999,35 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		if (la.kind == 7) {

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

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

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

 			AssertStmt(out s);

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

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

 			AssumeStmt(out s);

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

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

 			UseStmt(out s);

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

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

 			PrintStmt(out s);

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

-			HavocStmt(out s);

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

-			Get();

+		} else if (StartOf(11)) {

 			UpdateStmt(out s);

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

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

+			HavocStmt(out s);

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

+			VarDeclStatement(out s);

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

 			IfStmt(out s);

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

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

 			WhileStmt(out s);

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

 			MatchStmt(out s);

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

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

 			ForeachStmt(out s);

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

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

 			Get();

 			x = t; 

 			Ident(out id);

 			Expect(22);

 			s = new LabelStmt(x, id.val); 

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

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

 			Get();

 			x = t; 

 			if (la.kind == 1) {

@@ -1051,21 +1036,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}

 			Expect(15);

 			s = new BreakStmt(x, label); 

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

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

 			Get();

 			x = t; 

 			Expect(15);

 			s = new ReturnStmt(x); 

-		} else if (la.kind == 11 || la.kind == 18) {

-			VarDeclStatement(out s);

-		} else if (StartOf(11)) {

-			UpdateStmt(out s);

-		} else SynErr(121);

+		} else SynErr(120);

 	}

 

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

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

-		Expect(64);

+		Expect(63);

 		x = t; 

 		Expression(out e);

 		Expect(15);

@@ -1074,7 +1055,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 

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

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

-		Expect(65);

+		Expect(64);

 		x = t; 

 		Expression(out e);

 		Expect(15);

@@ -1083,7 +1064,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 

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

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

-		Expect(66);

+		Expect(65);

 		x = t; 

 		Expression(out e);

 		Expect(15);

@@ -1094,7 +1075,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

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

 		

-		Expect(67);

+		Expect(66);

 		x = t; 

 		AttributeArg(out arg);

 		args.Add(arg); 

@@ -1107,15 +1088,6 @@ List<Expression/*!*/>/*!*/ decreases) {
 		s = new PrintStmt(x, args); 

 	}

 

-	void HavocStmt(out Statement/*!*/ s) {

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

-		Expect(57);

-		x = t; 

-		Lhs(out lhs);

-		Expect(15);

-		s = new AssignStmt(x, lhs); 

-	}

-

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

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

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

@@ -1128,14 +1100,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 15) {

 			Get();

 			rhss.Add(new ExprRhs(e)); 

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

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

 			lhss.Add(e);  lhs0 = e; 

 			while (la.kind == 19) {

 				Get();

 				Lhs(out e);

 				lhss.Add(e); 

 			}

-			Expect(51);

+			Expect(50);

 			x = t; 

 			Rhs(out r, lhs0);

 			rhss.Add(r); 

@@ -1145,10 +1117,65 @@ List<Expression/*!*/>/*!*/ decreases) {
 				rhss.Add(r); 

 			}

 			Expect(15);

-		} else SynErr(122);

+		} else SynErr(121);

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

 	}

 

+	void HavocStmt(out Statement/*!*/ s) {

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

+		Expect(56);

+		x = t; 

+		Lhs(out lhs);

+		Expect(15);

+		s = new AssignStmt(x, lhs); 

+	}

+

+	void VarDeclStatement(out Statement/*!*/ s) {

+		IToken x = null, assignTok = null;  bool isGhost = false;

+		VarDecl/*!*/ d;

+		DeterminedAssignmentRhs r;  Expression lhs0;

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

+		List<DeterminedAssignmentRhs> rhss = new List<DeterminedAssignmentRhs>();

+		

+		if (la.kind == 11) {

+			Get();

+			isGhost = true;  x = t; 

+		}

+		Expect(18);

+		if (!isGhost) { x = t; } 

+		LocalIdentTypeOptional(out d, isGhost);

+		lhss.Add(d); 

+		while (la.kind == 19) {

+			Get();

+			LocalIdentTypeOptional(out d, isGhost);

+			lhss.Add(d); 

+		}

+		if (la.kind == 50) {

+			Get();

+			assignTok = t;  lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); 

+			Rhs(out r, lhs0);

+			rhss.Add(r); 

+			while (la.kind == 19) {

+				Get();

+				Rhs(out r, lhs0);

+				rhss.Add(r); 

+			}

+		}

+		Expect(15);

+		UpdateStmt update;

+		if (rhss.Count == 0) {

+		  update = null;

+		} else {

+		  var ies = new List<Expression>();

+		  foreach (var lhs in lhss) {

+		    ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

+		  }

+		  update = new UpdateStmt(assignTok, ies, rhss);

+		}

+		s = new VarDeclStmt(x, lhss, update);

+		

+	}

+

 	void IfStmt(out Statement/*!*/ ifStmt) {

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

 		Expression guard;

@@ -1159,26 +1186,26 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<GuardedAlternative> alternatives;

 		ifStmt = dummyStmt;  // to please the compiler

 		

-		Expect(58);

+		Expect(57);

 		x = t; 

 		if (la.kind == 32) {

 			Guard(out guard);

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

-			if (la.kind == 59) {

+			if (la.kind == 58) {

 				Get();

-				if (la.kind == 58) {

+				if (la.kind == 57) {

 					IfStmt(out s);

 					els = s; 

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

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

 					els = s; 

-				} else SynErr(123);

+				} else SynErr(122);

 			}

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

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

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(124);

+		} else SynErr(123);

 	}

 

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

@@ -1191,7 +1218,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

 		

-		Expect(60);

+		Expect(59);

 		x = t; 

 		if (la.kind == 32) {

 			Guard(out guard);

@@ -1203,7 +1230,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			LoopSpec(out invariants, out decreases);

 			AlternativeBlock(out alternatives);

 			stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives); 

-		} else SynErr(125);

+		} else SynErr(124);

 	}

 

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

@@ -1231,8 +1258,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();

 		Statement bodyAssign = null;

 		

-		parseVarScope.PushMarker(); 

-		Expect(62);

+		Expect(61);

 		x = t;

 		range = new LiteralExpr(x, true);

 		ty = new InferredTypeProxy();

@@ -1243,20 +1269,19 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 			Type(out ty);

 		}

-		Expect(63);

+		Expect(62);

 		Expression(out collection);

-		parseVarScope.Push(boundVar.val, boundVar.val); 

 		if (la.kind == 17) {

 			Get();

 			Expression(out range);

 		}

 		Expect(33);

 		Expect(7);

-		while (la.kind == 64 || la.kind == 65 || la.kind == 66) {

-			if (la.kind == 64) {

+		while (la.kind == 63 || la.kind == 64 || la.kind == 65) {

+			if (la.kind == 63) {

 				AssertStmt(out s);

 				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 

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

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

 				AssumeStmt(out s);

 				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 

 			} else {

@@ -1267,10 +1292,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (StartOf(11)) {

 			UpdateStmt(out s);

 			bodyAssign = s; 

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

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

 			HavocStmt(out s);

 			bodyAssign = s; 

-		} else SynErr(126);

+		} else SynErr(125);

 		Expect(8);

 		if (bodyAssign != null) {

 		 s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);

@@ -1278,53 +1303,6 @@ List<Expression/*!*/>/*!*/ decreases) {
 		  s = dummyStmt;  // some error occurred in parsing the bodyAssign

 		}

 		

-		parseVarScope.PopMarker(); 

-	}

-

-	void VarDeclStatement(out Statement/*!*/ s) {

-		IToken x = null, assignTok = null;  bool isGhost = false;

-		VarDecl/*!*/ d;

-		DeterminedAssignmentRhs r;  Expression lhs0;

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

-		List<DeterminedAssignmentRhs> rhss = new List<DeterminedAssignmentRhs>();

-		

-		if (la.kind == 11) {

-			Get();

-			isGhost = true;  x = t; 

-		}

-		Expect(18);

-		if (!isGhost) { x = t; } 

-		LocalIdentTypeOptional(out d, isGhost);

-		lhss.Add(d); 

-		while (la.kind == 19) {

-			Get();

-			LocalIdentTypeOptional(out d, isGhost);

-			lhss.Add(d); 

-		}

-		if (la.kind == 51) {

-			Get();

-			assignTok = t;  lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); 

-			Rhs(out r, lhs0);

-			rhss.Add(r); 

-			while (la.kind == 19) {

-				Get();

-				Rhs(out r, lhs0);

-				rhss.Add(r); 

-			}

-		}

-		Expect(15);

-		UpdateStmt update;

-		if (rhss.Count == 0) {

-		  update = null;

-		} else {

-		  var ies = new List<Expression>();

-		  foreach (var lhs in lhss) {

-		    ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

-		  }

-		  update = new UpdateStmt(assignTok, ies, rhss);

-		}

-		s = new VarDeclStmt(x, lhss, update);

-		

 	}

 

 	void Lhs(out Expression e) {

@@ -1332,16 +1310,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e);

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

+			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

 		} else if (StartOf(13)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

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

+			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

-		} else SynErr(127);

+		} else SynErr(126);

 	}

 

 	void Rhs(out DeterminedAssignmentRhs r, Expression receiverForInitCall) {

@@ -1352,16 +1330,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Expression> args;

 		r = null;  // to please compiler

 		

-		if (la.kind == 52) {

+		if (la.kind == 51) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

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

-				if (la.kind == 53) {

+			if (la.kind == 52 || la.kind == 54) {

+				if (la.kind == 52) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(54);

+					Expect(53);

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

 					

 				} else {

@@ -1383,7 +1361,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			  r = new TypeRhs(newToken, ty, initCall);

 			}

 			

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

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

 			Get();

 			x = t; 

 			Expression(out e);

@@ -1391,7 +1369,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(128);

+		} else SynErr(127);

 	}

 

 	void Guard(out Expression e) {

@@ -1403,7 +1381,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(129);

+		} else SynErr(128);

 		Expect(33);

 	}

 

@@ -1420,11 +1398,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expression(out e);

 			Expect(46);

 			body = new List<Statement>(); 

-			parseVarScope.PushMarker(); 

 			while (StartOf(9)) {

 				Stmt(body);

 			}

-			parseVarScope.PopMarker(); 

 			alternatives.Add(new GuardedAlternative(x, e, body)); 

 		}

 		Expect(8);

@@ -1435,14 +1411,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 		invariants = new List<MaybeFreeExpression/*!*/>();

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

 		

-		while (la.kind == 28 || la.kind == 31 || la.kind == 61) {

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

+		while (la.kind == 28 || la.kind == 31 || la.kind == 60) {

+			if (la.kind == 28 || la.kind == 60) {

 				isFree = false; 

 				if (la.kind == 28) {

 					Get();

 					isFree = true; 

 				}

-				Expect(61);

+				Expect(60);

 				Expression(out e);

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

 				Expect(15);

@@ -1467,29 +1443,24 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Statement/*!*/> body = new List<Statement/*!*/>();

 		

 		Expect(45);

-		x = t;  parseVarScope.PushMarker(); 

+		x = t; 

 		Ident(out id);

 		if (la.kind == 32) {

 			Get();

 			Ident(out arg);

-			arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

-			parseVarScope.Push(arg.val, arg.val); 

+			arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); 

 			while (la.kind == 19) {

 				Get();

 				Ident(out arg);

-				arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

-				parseVarScope.Push(arg.val, arg.val); 

+				arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); 

 			}

 			Expect(33);

 		}

 		Expect(46);

-		parseVarScope.PushMarker(); 

 		while (StartOf(9)) {

 			Stmt(body);

 		}

-		parseVarScope.PopMarker(); 

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

-		parseVarScope.PopMarker(); 

 	}

 

 	void AttributeArg(out Attributes.Argument/*!*/ arg) {

@@ -1500,13 +1471,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {

 			Expression(out e);

 			arg = new Attributes.Argument(e); 

-		} else SynErr(130);

+		} else SynErr(129);

 	}

 

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

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

 		ImpliesExpression(out e0);

-		while (la.kind == 68 || la.kind == 69) {

+		while (la.kind == 67 || la.kind == 68) {

 			EquivOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1517,7 +1488,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void ImpliesExpression(out Expression/*!*/ e0) {

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

 		LogicalExpression(out e0);

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

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

 			ImpliesOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1526,23 +1497,23 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 

 	void EquivOp() {

-		if (la.kind == 68) {

+		if (la.kind == 67) {

 			Get();

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

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

 			Get();

-		} else SynErr(131);

+		} else SynErr(130);

 	}

 

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

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

 		RelationalExpression(out e0);

 		if (StartOf(14)) {

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

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

 				AndOp();

 				x = t; 

 				RelationalExpression(out e1);

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

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

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

 					AndOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1553,7 +1524,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				x = t; 

 				RelationalExpression(out e1);

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

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

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

 					OrOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1564,11 +1535,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 

 	void ImpliesOp() {

-		if (la.kind == 70) {

+		if (la.kind == 69) {

 			Get();

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

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

 			Get();

-		} else SynErr(132);

+		} else SynErr(131);

 	}

 

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

@@ -1582,25 +1553,25 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 

 	void AndOp() {

-		if (la.kind == 72) {

+		if (la.kind == 71) {

 			Get();

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

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

 			Get();

-		} else SynErr(133);

+		} else SynErr(132);

 	}

 

 	void OrOp() {

-		if (la.kind == 74) {

+		if (la.kind == 73) {

 			Get();

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

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

 			Get();

-		} else SynErr(134);

+		} else SynErr(133);

 	}

 

 	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 == 85 || la.kind == 86) {

+		while (la.kind == 84 || la.kind == 85) {

 			AddOp(out x, out op);

 			Factor(out e1);

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

@@ -1610,7 +1581,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

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

 		switch (la.kind) {

-		case 76: {

+		case 75: {

 			Get();

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

 			break;

@@ -1625,59 +1596,59 @@ List<Expression/*!*/>/*!*/ decreases) {
 			x = t;  op = BinaryExpr.Opcode.Gt; 

 			break;

 		}

-		case 77: {

+		case 76: {

 			Get();

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

 			break;

 		}

-		case 78: {

+		case 77: {

 			Get();

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

 			break;

 		}

-		case 79: {

+		case 78: {

 			Get();

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

 			break;

 		}

-		case 80: {

+		case 79: {

 			Get();

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

 			break;

 		}

-		case 63: {

+		case 62: {

 			Get();

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

 			break;

 		}

-		case 81: {

+		case 80: {

 			Get();

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

 			break;

 		}

-		case 82: {

+		case 81: {

 			Get();

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

 			break;

 		}

-		case 83: {

+		case 82: {

 			Get();

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

 			break;

 		}

-		case 84: {

+		case 83: {

 			Get();

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

 			break;

 		}

-		default: SynErr(135); break;

+		default: SynErr(134); 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 == 42 || la.kind == 87 || la.kind == 88) {

+		while (la.kind == 42 || la.kind == 86 || la.kind == 87) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

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

@@ -1686,23 +1657,23 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	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 == 85) {

+		if (la.kind == 84) {

 			Get();

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

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

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

 			Get();

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

-		} else SynErr(136);

+		} else SynErr(135);

 	}

 

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

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

-		if (la.kind == 86) {

+		if (la.kind == 85) {

 			Get();

 			x = t; 

 			UnaryExpression(out e);

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

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

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

 			NegOp();

 			x = t; 

 			UnaryExpression(out e);

@@ -1711,15 +1682,15 @@ List<Expression/*!*/>/*!*/ decreases) {
 			EndlessExpression(out e);

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

 			DottedIdentifiersAndFunction(out e);

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

+			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

 		} else if (StartOf(13)) {

 			ConstAtomExpression(out e);

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

+			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

-		} else SynErr(137);

+		} else SynErr(136);

 	}

 

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

@@ -1727,21 +1698,21 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 42) {

 			Get();

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

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

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

 			Get();

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

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

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

 			Get();

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

-		} else SynErr(138);

+		} else SynErr(137);

 	}

 

 	void NegOp() {

-		if (la.kind == 89) {

+		if (la.kind == 88) {

 			Get();

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

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

 			Get();

-		} else SynErr(139);

+		} else SynErr(138);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -1749,20 +1720,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expression e0, e1;

 		e = dummyExpr;

 		

-		if (la.kind == 58) {

+		if (la.kind == 57) {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(98);

+			Expect(97);

 			Expression(out e0);

-			Expect(59);

+			Expect(58);

 			Expression(out e1);

 			e = new ITEExpr(x, e, e0, e1); 

 		} else if (StartOf(17)) {

 			QuantifierGuts(out e);

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

 			ComprehensionExpr(out e);

-		} else SynErr(140);

+		} else SynErr(139);

 	}

 

 	void DottedIdentifiersAndFunction(out Expression e) {

@@ -1772,7 +1743,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		Ident(out id);

 		idents.Add(id); 

-		while (la.kind == 55) {

+		while (la.kind == 54) {

 			Get();

 			Ident(out id);

 			idents.Add(id); 

@@ -1794,7 +1765,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Expression> multipleIndices = null;

 		bool func = false;

 		

-		if (la.kind == 55) {

+		if (la.kind == 54) {

 			Get();

 			Ident(out id);

 			if (la.kind == 32) {

@@ -1807,24 +1778,24 @@ List<Expression/*!*/>/*!*/ decreases) {
 				e = new FunctionCallExpr(id, id.val, e, args); 

 			}

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

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

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

 			Get();

 			x = t; 

 			if (StartOf(8)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (la.kind == 99) {

+				if (la.kind == 98) {

 					Get();

 					anyDots = true; 

 					if (StartOf(8)) {

 						Expression(out ee);

 						e1 = ee; 

 					}

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

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

 					Get();

 					Expression(out ee);

 					e1 = ee; 

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

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

 					while (la.kind == 19) {

 						Get();

 						Expression(out ee);

@@ -1835,12 +1806,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(141);

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

+				} else SynErr(140);

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

 				Get();

 				Expression(out ee);

 				anyDots = true;  e1 = ee; 

-			} else SynErr(142);

+			} else SynErr(141);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

@@ -1863,8 +1834,8 @@ List<Expression/*!*/>/*!*/ decreases) {
 			  }

 			}

 			

-			Expect(54);

-		} else SynErr(143);

+			Expect(53);

+		} else SynErr(142);

 	}

 

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

@@ -1873,17 +1844,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 		e = dummyExpr;

 		

 		switch (la.kind) {

-		case 91: {

+		case 90: {

 			Get();

 			e = new LiteralExpr(t, false); 

 			break;

 		}

-		case 92: {

+		case 91: {

 			Get();

 			e = new LiteralExpr(t, true); 

 			break;

 		}

-		case 93: {

+		case 92: {

 			Get();

 			e = new LiteralExpr(t); 

 			break;

@@ -1893,12 +1864,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new LiteralExpr(t, n); 

 			break;

 		}

-		case 94: {

+		case 93: {

 			Get();

 			e = new ThisExpr(t); 

 			break;

 		}

-		case 95: {

+		case 94: {

 			Get();

 			x = t; 

 			Expect(32);

@@ -1907,7 +1878,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new FreshExpr(x, e); 

 			break;

 		}

-		case 96: {

+		case 95: {

 			Get();

 			x = t; 

 			Expect(32);

@@ -1916,7 +1887,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new AllocatedExpr(x, e); 

 			break;

 		}

-		case 97: {

+		case 96: {

 			Get();

 			x = t; 

 			Expect(32);

@@ -1943,14 +1914,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(8);

 			break;

 		}

-		case 53: {

+		case 52: {

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

 			if (StartOf(8)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(54);

+			Expect(53);

 			break;

 		}

 		case 32: {

@@ -1961,7 +1932,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(33);

 			break;

 		}

-		default: SynErr(144); break;

+		default: SynErr(143); break;

 		}

 	}

 

@@ -1986,20 +1957,19 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expression range = null;

 		Expression/*!*/ body;

 		

-		if (la.kind == 100 || la.kind == 101) {

+		if (la.kind == 99 || la.kind == 100) {

 			Forall();

 			x = t;  univ = true; 

-		} else if (la.kind == 102 || la.kind == 103) {

+		} else if (la.kind == 101 || la.kind == 102) {

 			Exists();

 			x = t; 

-		} else SynErr(145);

-		parseVarScope.PushMarker(); 

+		} else SynErr(144);

 		IdentTypeOptional(out bv);

-		bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 

+		bvars.Add(bv); 

 		while (la.kind == 19) {

 			Get();

 			IdentTypeOptional(out bv);

-			bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 

+			bvars.Add(bv); 

 		}

 		while (la.kind == 7) {

 			AttributeOrTrigger(ref attrs, ref trigs);

@@ -2015,7 +1985,6 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else {

 		  q = new ExistsExpr(x, bvars, range, body, trigs, attrs);

 		}

-		parseVarScope.PopMarker();

 		

 	}

 

@@ -2029,40 +1998,38 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		Expect(37);

 		x = t; 

-		parseVarScope.PushMarker(); 

 		IdentTypeOptional(out bv);

-		bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 

+		bvars.Add(bv); 

 		while (la.kind == 19) {

 			Get();

 			IdentTypeOptional(out bv);

-			bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 

+			bvars.Add(bv); 

 		}

 		Expect(17);

 		Expression(out range);

-		if (la.kind == 104 || la.kind == 105) {

+		if (la.kind == 103 || la.kind == 104) {

 			QSep();

 			Expression(out body);

 		}

 		if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }

 		q = new SetComprehension(x, bvars, range, body);

-		parseVarScope.PopMarker();

 		

 	}

 

 	void Forall() {

-		if (la.kind == 100) {

+		if (la.kind == 99) {

 			Get();

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

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

 			Get();

-		} else SynErr(146);

+		} else SynErr(145);

 	}

 

 	void Exists() {

-		if (la.kind == 102) {

+		if (la.kind == 101) {

 			Get();

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

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

 			Get();

-		} else SynErr(147);

+		} else SynErr(146);

 	}

 

 	void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {

@@ -2075,16 +2042,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 			es = new List<Expression/*!*/>(); 

 			Expressions(es);

 			trigs = new Triggers(es, trigs); 

-		} else SynErr(148);

+		} else SynErr(147);

 		Expect(8);

 	}

 

 	void QSep() {

-		if (la.kind == 104) {

+		if (la.kind == 103) {

 			Get();

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

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

 			Get();

-		} else SynErr(149);

+		} else SynErr(148);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2119,25 +2086,25 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 

 	static readonly bool[,]/*!*/ set = {

-		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

-		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,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, 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, T,T,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, 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,T,T,T, 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,T, 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,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,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,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,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, 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, 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,T,T,x, x,x,x,T, x,x,x,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,T,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, 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,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},

-		{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, x,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, T,x,x,T, T,T,T,x, x,T,x,x, x,T,T,x, T,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,x,T, x,x,x,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,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, 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,x, x,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},

-		{x,T,T,x, x,x,x,T, x,x,x,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, 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,T, T,T,T,T, T,T,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, 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,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,T,x, x,x,x,T, x,x,x,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, 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,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, 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,T, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x,x, x,x,x,x, x,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,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, 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,x,x,x, 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,T,T,x, T,x,x,T, x,x,x,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,T,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, 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,T,T,T, T,T,T,T, T,T,x,x, T,T,T,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,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,T,T, T,T,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, 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,T,T,T, 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,T, 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,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,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,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,T,x,T, 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, 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,T,T,x, x,x,x,T, x,x,x,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,T,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,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, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},

+		{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, x,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, T,x,x,T, T,T,x,x, T,x,x,x, T,T,x,T, 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,x,T, x,x,x,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,T,x,x, x,x,T,x, x,x,x,x, x,x,x,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,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},

+		{x,T,T,x, x,x,x,T, x,x,x,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, 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,T,T, T,T,T,T, T,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, 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, 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,T,x, x,x,x,T, x,x,x,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, 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,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, 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,T,x, x,x,x,x, x,x,x,x, x,x,x,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,x,x,x, x,x,x,x, x,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,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,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,x,x,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,T,T,x, T,x,x,T, x,x,x,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,T,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,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, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}

 

 	};

 } // end Parser

@@ -2209,109 +2176,108 @@ public class Errors {
 			case 44: s = "\"match\" expected"; break;

 			case 45: s = "\"case\" expected"; break;

 			case 46: s = "\"=>\" expected"; break;

-			case 47: s = "\"call\" expected"; break;

-			case 48: s = "\"label\" expected"; break;

-			case 49: s = "\"break\" expected"; break;

-			case 50: s = "\"return\" expected"; break;

-			case 51: s = "\":=\" expected"; break;

-			case 52: s = "\"new\" expected"; break;

-			case 53: s = "\"[\" expected"; break;

-			case 54: s = "\"]\" expected"; break;

-			case 55: s = "\".\" expected"; break;

-			case 56: s = "\"choose\" expected"; break;

-			case 57: s = "\"havoc\" expected"; break;

-			case 58: s = "\"if\" expected"; break;

-			case 59: s = "\"else\" expected"; break;

-			case 60: s = "\"while\" expected"; break;

-			case 61: s = "\"invariant\" expected"; break;

-			case 62: s = "\"foreach\" expected"; break;

-			case 63: s = "\"in\" expected"; break;

-			case 64: s = "\"assert\" expected"; break;

-			case 65: s = "\"assume\" expected"; break;

-			case 66: s = "\"use\" expected"; break;

-			case 67: s = "\"print\" expected"; break;

-			case 68: s = "\"<==>\" expected"; break;

-			case 69: s = "\"\\u21d4\" expected"; break;

-			case 70: s = "\"==>\" expected"; break;

-			case 71: s = "\"\\u21d2\" expected"; break;

-			case 72: s = "\"&&\" expected"; break;

-			case 73: s = "\"\\u2227\" expected"; break;

-			case 74: s = "\"||\" expected"; break;

-			case 75: s = "\"\\u2228\" expected"; break;

-			case 76: s = "\"==\" 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 = "\"!in\" expected"; break;

-			case 82: s = "\"\\u2260\" expected"; break;

-			case 83: s = "\"\\u2264\" expected"; break;

-			case 84: s = "\"\\u2265\" expected"; break;

-			case 85: s = "\"+\" expected"; break;

-			case 86: s = "\"-\" expected"; break;

-			case 87: s = "\"/\" expected"; break;

-			case 88: s = "\"%\" expected"; break;

-			case 89: s = "\"!\" expected"; break;

-			case 90: s = "\"\\u00ac\" expected"; break;

-			case 91: s = "\"false\" expected"; break;

-			case 92: s = "\"true\" expected"; break;

-			case 93: s = "\"null\" expected"; break;

-			case 94: s = "\"this\" expected"; break;

-			case 95: s = "\"fresh\" expected"; break;

-			case 96: s = "\"allocated\" expected"; break;

-			case 97: s = "\"old\" expected"; break;

-			case 98: s = "\"then\" expected"; break;

-			case 99: s = "\"..\" expected"; break;

-			case 100: s = "\"forall\" expected"; break;

-			case 101: s = "\"\\u2200\" expected"; break;

-			case 102: s = "\"exists\" expected"; break;

-			case 103: s = "\"\\u2203\" expected"; break;

-			case 104: s = "\"::\" expected"; break;

-			case 105: s = "\"\\u2022\" expected"; break;

-			case 106: s = "??? expected"; break;

-			case 107: s = "invalid DatatypeDecl"; break;

-			case 108: s = "invalid ClassMemberDecl"; break;

-			case 109: s = "invalid FunctionDecl"; break;

+			case 47: s = "\"label\" expected"; break;

+			case 48: s = "\"break\" expected"; break;

+			case 49: s = "\"return\" expected"; break;

+			case 50: s = "\":=\" expected"; break;

+			case 51: s = "\"new\" expected"; break;

+			case 52: s = "\"[\" expected"; break;

+			case 53: s = "\"]\" expected"; break;

+			case 54: s = "\".\" expected"; break;

+			case 55: s = "\"choose\" expected"; break;

+			case 56: s = "\"havoc\" expected"; break;

+			case 57: s = "\"if\" expected"; break;

+			case 58: s = "\"else\" expected"; break;

+			case 59: s = "\"while\" expected"; break;

+			case 60: s = "\"invariant\" expected"; break;

+			case 61: s = "\"foreach\" expected"; break;

+			case 62: s = "\"in\" expected"; break;

+			case 63: s = "\"assert\" expected"; break;

+			case 64: s = "\"assume\" expected"; break;

+			case 65: s = "\"use\" expected"; break;

+			case 66: s = "\"print\" expected"; break;

+			case 67: s = "\"<==>\" expected"; break;

+			case 68: s = "\"\\u21d4\" expected"; break;

+			case 69: s = "\"==>\" expected"; break;

+			case 70: s = "\"\\u21d2\" expected"; break;

+			case 71: s = "\"&&\" expected"; break;

+			case 72: s = "\"\\u2227\" expected"; break;

+			case 73: s = "\"||\" expected"; break;

+			case 74: s = "\"\\u2228\" expected"; break;

+			case 75: s = "\"==\" expected"; break;

+			case 76: s = "\"<=\" expected"; break;

+			case 77: s = "\">=\" expected"; break;

+			case 78: s = "\"!=\" expected"; break;

+			case 79: s = "\"!!\" expected"; break;

+			case 80: s = "\"!in\" expected"; break;

+			case 81: s = "\"\\u2260\" expected"; break;

+			case 82: s = "\"\\u2264\" expected"; break;

+			case 83: s = "\"\\u2265\" expected"; break;

+			case 84: s = "\"+\" expected"; break;

+			case 85: s = "\"-\" expected"; break;

+			case 86: s = "\"/\" expected"; break;

+			case 87: s = "\"%\" expected"; break;

+			case 88: s = "\"!\" expected"; break;

+			case 89: s = "\"\\u00ac\" expected"; break;

+			case 90: s = "\"false\" expected"; break;

+			case 91: s = "\"true\" expected"; break;

+			case 92: s = "\"null\" expected"; break;

+			case 93: s = "\"this\" expected"; break;

+			case 94: s = "\"fresh\" expected"; break;

+			case 95: s = "\"allocated\" expected"; break;

+			case 96: s = "\"old\" expected"; break;

+			case 97: s = "\"then\" expected"; break;

+			case 98: s = "\"..\" expected"; break;

+			case 99: s = "\"forall\" expected"; break;

+			case 100: s = "\"\\u2200\" expected"; break;

+			case 101: s = "\"exists\" expected"; break;

+			case 102: s = "\"\\u2203\" expected"; break;

+			case 103: s = "\"::\" expected"; break;

+			case 104: s = "\"\\u2022\" expected"; break;

+			case 105: s = "??? expected"; break;

+			case 106: s = "invalid DatatypeDecl"; break;

+			case 107: s = "invalid ClassMemberDecl"; break;

+			case 108: s = "invalid FunctionDecl"; break;

+			case 109: s = "invalid MethodDecl"; break;

 			case 110: s = "invalid MethodDecl"; break;

-			case 111: s = "invalid MethodDecl"; break;

-			case 112: s = "invalid TypeAndToken"; break;

+			case 111: s = "invalid TypeAndToken"; break;

+			case 112: s = "invalid MethodSpec"; break;

 			case 113: s = "invalid MethodSpec"; break;

-			case 114: s = "invalid MethodSpec"; break;

-			case 115: s = "invalid ReferenceType"; break;

-			case 116: s = "invalid FunctionSpec"; break;

-			case 117: s = "invalid FunctionBody"; break;

-			case 118: s = "invalid PossiblyWildFrameExpression"; break;

-			case 119: s = "invalid PossiblyWildExpression"; break;

-			case 120: s = "invalid MatchOrExpr"; break;

-			case 121: s = "invalid OneStmt"; break;

-			case 122: s = "invalid UpdateStmt"; break;

+			case 114: s = "invalid ReferenceType"; break;

+			case 115: s = "invalid FunctionSpec"; break;

+			case 116: s = "invalid FunctionBody"; break;

+			case 117: s = "invalid PossiblyWildFrameExpression"; break;

+			case 118: s = "invalid PossiblyWildExpression"; break;

+			case 119: s = "invalid MatchOrExpr"; break;

+			case 120: s = "invalid OneStmt"; break;

+			case 121: s = "invalid UpdateStmt"; break;

+			case 122: s = "invalid IfStmt"; break;

 			case 123: s = "invalid IfStmt"; break;

-			case 124: s = "invalid IfStmt"; break;

-			case 125: s = "invalid WhileStmt"; break;

-			case 126: s = "invalid ForeachStmt"; break;

-			case 127: s = "invalid Lhs"; break;

-			case 128: s = "invalid Rhs"; break;

-			case 129: s = "invalid Guard"; break;

-			case 130: s = "invalid AttributeArg"; break;

-			case 131: s = "invalid EquivOp"; break;

-			case 132: s = "invalid ImpliesOp"; break;

-			case 133: s = "invalid AndOp"; break;

-			case 134: s = "invalid OrOp"; break;

-			case 135: s = "invalid RelOp"; break;

-			case 136: s = "invalid AddOp"; break;

-			case 137: s = "invalid UnaryExpression"; break;

-			case 138: s = "invalid MulOp"; break;

-			case 139: s = "invalid NegOp"; break;

-			case 140: s = "invalid EndlessExpression"; break;

+			case 124: s = "invalid WhileStmt"; break;

+			case 125: s = "invalid ForeachStmt"; break;

+			case 126: s = "invalid Lhs"; break;

+			case 127: s = "invalid Rhs"; break;

+			case 128: s = "invalid Guard"; break;

+			case 129: s = "invalid AttributeArg"; break;

+			case 130: s = "invalid EquivOp"; break;

+			case 131: s = "invalid ImpliesOp"; break;

+			case 132: s = "invalid AndOp"; break;

+			case 133: s = "invalid OrOp"; break;

+			case 134: s = "invalid RelOp"; break;

+			case 135: s = "invalid AddOp"; break;

+			case 136: s = "invalid UnaryExpression"; break;

+			case 137: s = "invalid MulOp"; break;

+			case 138: s = "invalid NegOp"; break;

+			case 139: s = "invalid EndlessExpression"; break;

+			case 140: s = "invalid Suffix"; break;

 			case 141: s = "invalid Suffix"; break;

 			case 142: s = "invalid Suffix"; break;

-			case 143: s = "invalid Suffix"; break;

-			case 144: s = "invalid ConstAtomExpression"; break;

-			case 145: s = "invalid QuantifierGuts"; break;

-			case 146: s = "invalid Forall"; break;

-			case 147: s = "invalid Exists"; break;

-			case 148: s = "invalid AttributeOrTrigger"; break;

-			case 149: s = "invalid QSep"; break;

+			case 143: s = "invalid ConstAtomExpression"; break;

+			case 144: s = "invalid QuantifierGuts"; break;

+			case 145: s = "invalid Forall"; break;

+			case 146: s = "invalid Exists"; break;

+			case 147: s = "invalid AttributeOrTrigger"; break;

+			case 148: s = "invalid QSep"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 9b931f73..8722cd63 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1234,6 +1234,9 @@ namespace Microsoft.Dafny {
               var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, s.Rhss[i]);

               s.ResolvedStatements.Add(a);

             }

+            if (s.Lhss.Count != 1) {

+              Error(s, "multi-assignments not yet supported");  // TODO

+            }

           }

         } else {

           // if there was an effectful RHS, that must be the only RHS

@@ -1251,14 +1254,15 @@ namespace Microsoft.Dafny {
           } else {

             // a call statement

             if (ErrorCount == prevErrorCount) {

-#if !FULL_LHS_SUPPORT_FOR_CALLS

               var idLhss = new List<IdentifierExpr>();

               foreach (var ll in s.Lhss) {

-                var ie = (IdentifierExpr)ll.Resolved;  // TODO: the CallStmt should handle all LHS's, not just identifier expressions

-                Contract.Assert(ie != null);

-                idLhss.Add(ie);

+                var ie = ll.Resolved as IdentifierExpr;  // TODO: the CallStmt should handle all LHS's, not just identifier expressions

+                if (ie == null) {

+                  Error(ll, "actual out-parameters of calls must be variables, not fields");

+                } else {

+                  idLhss.Add(ie);

+                }

               }

-#endif

               var a = new CallStmt(callRhs.Tok, idLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);

               s.ResolvedStatements.Add(a);

             }

@@ -1736,11 +1740,15 @@ namespace Microsoft.Dafny {
           if (callee.IsStatic) {

             Error(s.Tok, "a method called as an initialization method must not be 'static'");

           }

-        } else  if (!scope.AllowInstance && !callee.IsStatic && s.Receiver is ThisExpr) {

-          // The call really needs an instance, but that instance is given as 'this', which is not

-          // available in this context.  For more details, see comment in the resolution of a

-          // FunctionCallExpr.

-          Error(s.Receiver, "'this' is not allowed in a 'static' context");

+        } else if (!callee.IsStatic) {

+          if (!scope.AllowInstance && s.Receiver is ThisExpr) {

+            // The call really needs an instance, but that instance is given as 'this', which is not

+            // available in this context.  For more details, see comment in the resolution of a

+            // FunctionCallExpr.

+            Error(s.Receiver, "'this' is not allowed in a 'static' context");

+          } else if (s.Receiver is StaticReceiverExpr) {

+            Error(s.Receiver, "call to instance method requires an instance");

+          }

         }

         // build the type substitution map

         Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();

@@ -2653,15 +2661,19 @@ namespace Microsoft.Dafny {
           Error(e, "wrong number of function arguments (got {0}, expected {1})", e.Args.Count, function.Formals.Count);

         } else {

           Contract.Assert(ctype != null);  // follows from postcondition of ResolveMember

-          if (!scope.AllowInstance && !function.IsStatic && e.Receiver is ThisExpr) {

-            // The call really needs an instance, but that instance is given as 'this', which is not

-            // available in this context.  In most cases, occurrences of 'this' inside e.Receiver would

-            // have been caught in the recursive call to resolve e.Receiver, but not the specific case

-            // of e.Receiver being 'this' (explicitly or implicitly), for that case needs to be allowed

-            // in the event that a class function calls another class function (and note that we need the

-            // type of the receiver in order to find the method, so we could not have made this check

-            // earlier).

-            Error(e.Receiver, "'this' is not allowed in a 'static' context");

+          if (!function.IsStatic) {

+            if (!scope.AllowInstance && e.Receiver is ThisExpr) {

+              // The call really needs an instance, but that instance is given as 'this', which is not

+              // available in this context.  In most cases, occurrences of 'this' inside e.Receiver would

+              // have been caught in the recursive call to resolve e.Receiver, but not the specific case

+              // of e.Receiver being 'this' (explicitly or implicitly), for that case needs to be allowed

+              // in the event that a static function calls another static function (and note that we need the

+              // type of the receiver in order to find the method, so we could not have made this check

+              // earlier).

+              Error(e.Receiver, "'this' is not allowed in a 'static' context");

+            } else if (e.Receiver is StaticReceiverExpr) {

+              Error(e.Receiver, "call to instance function requires an instance");

+            }

           }

           // build the type substitution map

           Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();

diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index ba5a745d..7d750553 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 = 106;

-	const int noSym = 106;

+	const int maxT = 105;

+	const int noSym = 105;

 

 

 	[ContractInvariantMethod]

@@ -515,33 +515,32 @@ public class Scanner {
 			case "reads": t.kind = 41; break;

 			case "match": t.kind = 44; break;

 			case "case": t.kind = 45; break;

-			case "call": t.kind = 47; break;

-			case "label": t.kind = 48; break;

-			case "break": t.kind = 49; break;

-			case "return": t.kind = 50; break;

-			case "new": t.kind = 52; break;

-			case "choose": t.kind = 56; break;

-			case "havoc": t.kind = 57; break;

-			case "if": t.kind = 58; break;

-			case "else": t.kind = 59; break;

-			case "while": t.kind = 60; break;

-			case "invariant": t.kind = 61; break;

-			case "foreach": t.kind = 62; break;

-			case "in": t.kind = 63; break;

-			case "assert": t.kind = 64; break;

-			case "assume": t.kind = 65; break;

-			case "use": t.kind = 66; break;

-			case "print": t.kind = 67; break;

-			case "false": t.kind = 91; break;

-			case "true": t.kind = 92; break;

-			case "null": t.kind = 93; break;

-			case "this": t.kind = 94; break;

-			case "fresh": t.kind = 95; break;

-			case "allocated": t.kind = 96; break;

-			case "old": t.kind = 97; break;

-			case "then": t.kind = 98; break;

-			case "forall": t.kind = 100; break;

-			case "exists": t.kind = 102; break;

+			case "label": t.kind = 47; break;

+			case "break": t.kind = 48; break;

+			case "return": t.kind = 49; break;

+			case "new": t.kind = 51; break;

+			case "choose": t.kind = 55; break;

+			case "havoc": t.kind = 56; break;

+			case "if": t.kind = 57; break;

+			case "else": t.kind = 58; break;

+			case "while": t.kind = 59; break;

+			case "invariant": t.kind = 60; break;

+			case "foreach": t.kind = 61; break;

+			case "in": t.kind = 62; break;

+			case "assert": t.kind = 63; break;

+			case "assume": t.kind = 64; break;

+			case "use": t.kind = 65; break;

+			case "print": t.kind = 66; break;

+			case "false": t.kind = 90; break;

+			case "true": t.kind = 91; break;

+			case "null": t.kind = 92; break;

+			case "this": t.kind = 93; break;

+			case "fresh": t.kind = 94; break;

+			case "allocated": t.kind = 95; break;

+			case "old": t.kind = 96; break;

+			case "then": t.kind = 97; break;

+			case "forall": t.kind = 99; break;

+			case "exists": t.kind = 101; break;

 			default: break;

 		}

 	}

@@ -661,70 +660,70 @@ public class Scanner {
 			case 25:

 				{t.kind = 46; break;}

 			case 26:

-				{t.kind = 51; break;}

+				{t.kind = 50; break;}

 			case 27:

-				{t.kind = 53; break;}

+				{t.kind = 52; break;}

 			case 28:

-				{t.kind = 54; break;}

+				{t.kind = 53; break;}

 			case 29:

 				if (ch == '>') {AddCh(); goto case 30;}

 				else {goto case 0;}

 			case 30:

-				{t.kind = 68; break;}

+				{t.kind = 67; break;}

 			case 31:

-				{t.kind = 69; break;}

+				{t.kind = 68; break;}

 			case 32:

-				{t.kind = 70; break;}

+				{t.kind = 69; break;}

 			case 33:

-				{t.kind = 71; break;}

+				{t.kind = 70; break;}

 			case 34:

 				if (ch == '&') {AddCh(); goto case 35;}

 				else {goto case 0;}

 			case 35:

-				{t.kind = 72; break;}

+				{t.kind = 71; break;}

 			case 36:

-				{t.kind = 73; break;}

+				{t.kind = 72; break;}

 			case 37:

-				{t.kind = 74; break;}

+				{t.kind = 73; break;}

 			case 38:

-				{t.kind = 75; break;}

+				{t.kind = 74; break;}

 			case 39:

-				{t.kind = 78; break;}

+				{t.kind = 77; break;}

 			case 40:

-				{t.kind = 79; break;}

+				{t.kind = 78; break;}

 			case 41:

-				{t.kind = 80; break;}

+				{t.kind = 79; break;}

 			case 42:

 				if (ch == 'n') {AddCh(); goto case 43;}

 				else {goto case 0;}

 			case 43:

-				{t.kind = 81; break;}

+				{t.kind = 80; break;}

 			case 44:

-				{t.kind = 82; break;}

+				{t.kind = 81; break;}

 			case 45:

-				{t.kind = 83; break;}

+				{t.kind = 82; break;}

 			case 46:

-				{t.kind = 84; break;}

+				{t.kind = 83; break;}

 			case 47:

-				{t.kind = 85; break;}

+				{t.kind = 84; break;}

 			case 48:

-				{t.kind = 86; break;}

+				{t.kind = 85; break;}

 			case 49:

-				{t.kind = 87; break;}

+				{t.kind = 86; break;}

 			case 50:

-				{t.kind = 88; break;}

+				{t.kind = 87; break;}

 			case 51:

-				{t.kind = 90; break;}

+				{t.kind = 89; break;}

 			case 52:

-				{t.kind = 99; break;}

+				{t.kind = 98; break;}

 			case 53:

-				{t.kind = 101; break;}

+				{t.kind = 100; break;}

 			case 54:

-				{t.kind = 103; break;}

+				{t.kind = 102; break;}

 			case 55:

-				{t.kind = 104; break;}

+				{t.kind = 103; break;}

 			case 56:

-				{t.kind = 105; break;}

+				{t.kind = 104; break;}

 			case 57:

 				recEnd = pos; recKind = 16;

 				if (ch == '>') {AddCh(); goto case 25;}

@@ -748,23 +747,23 @@ public class Scanner {
 				if (ch == '=') {AddCh(); goto case 39;}

 				else {t.kind = 24; break;}

 			case 62:

-				recEnd = pos; recKind = 55;

+				recEnd = pos; recKind = 54;

 				if (ch == '.') {AddCh(); goto case 52;}

-				else {t.kind = 55; break;}

+				else {t.kind = 54; break;}

 			case 63:

-				recEnd = pos; recKind = 89;

+				recEnd = pos; recKind = 88;

 				if (ch == '=') {AddCh(); goto case 40;}

 				else if (ch == '!') {AddCh(); goto case 41;}

 				else if (ch == 'i') {AddCh(); goto case 42;}

-				else {t.kind = 89; break;}

+				else {t.kind = 88; break;}

 			case 64:

-				recEnd = pos; recKind = 76;

+				recEnd = pos; recKind = 75;

 				if (ch == '>') {AddCh(); goto case 32;}

-				else {t.kind = 76; break;}

+				else {t.kind = 75; break;}

 			case 65:

-				recEnd = pos; recKind = 77;

+				recEnd = pos; recKind = 76;

 				if (ch == '=') {AddCh(); goto case 29;}

-				else {t.kind = 77; break;}

+				else {t.kind = 76; break;}

 

 		}

 		t.val = new String(tval, 0, tlen);

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 28281820..ca19af7b 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -2983,8 +2983,7 @@ namespace Microsoft.Dafny {
         locals.Add(var);

         

       } else if (stmt is CallStmt) {

-        CallStmt s = (CallStmt)stmt;

-        TrCallStmt(s, builder, locals, etran, null);

+        TrCallStmt((CallStmt)stmt, builder, locals, etran, null);

         

       } else if (stmt is BlockStmt) {

         foreach (Statement ss in ((BlockStmt)stmt).Body) {