From d9f2a82a417703f3669ba8399dcc8bcf34c3d742 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 26 May 2011 00:02:57 -0700
Subject: Dafny: retired the "call" keyword

---
 Dafny/Dafny.atg                               |  77 +--
 Dafny/Parser.cs                               | 714 ++++++++++++--------------
 Dafny/Resolver.cs                             |  50 +-
 Dafny/Scanner.cs                              | 129 +++--
 Dafny/Translator.cs                           |   3 +-
 Test/VSComp2010/Problem1-SumMax.dfy           |   2 +-
 Test/VSComp2010/Problem2-Invert.dfy           |   6 +-
 Test/VSComp2010/Problem3-FindZero.dfy         |  10 +-
 Test/VSComp2010/Problem4-Queens.dfy           |  10 +-
 Test/VSComp2010/Problem5-DoubleEndedQueue.dfy |  16 +-
 Test/VSI-Benchmarks/b1.dfy                    |  28 +-
 Test/VSI-Benchmarks/b2.dfy                    |  16 +-
 Test/VSI-Benchmarks/b3.dfy                    |  14 +-
 Test/VSI-Benchmarks/b4.dfy                    |   6 +-
 Test/VSI-Benchmarks/b5.dfy                    |  36 +-
 Test/VSI-Benchmarks/b6.dfy                    |  16 +-
 Test/VSI-Benchmarks/b7.dfy                    |  23 +-
 Test/VSI-Benchmarks/b8.dfy                    |  42 +-
 Test/dafny0/Answer                            |  86 ++--
 Test/dafny0/Basics.dfy                        |  10 +-
 Test/dafny0/Comprehensions.dfy                |  10 +-
 Test/dafny0/Modules0.dfy                      |  34 +-
 Test/dafny0/Modules1.dfy                      |   8 +-
 Test/dafny0/MultiDimArray.dfy                 |   2 +-
 Test/dafny0/NatTypes.dfy                      |   8 +-
 Test/dafny0/ResolutionErrors.dfy              |  10 +-
 Test/dafny0/Simple.dfy                        |   6 +-
 Test/dafny0/SmallTests.dfy                    |  14 +-
 Test/dafny0/Termination.dfy                   |  21 +-
 Test/dafny0/TypeAntecedents.dfy               |   4 +-
 Test/dafny0/TypeParameters.dfy                |  14 +-
 Test/dafny0/TypeTests.dfy                     |   4 +-
 Test/dafny1/BinaryTree.dfy                    |  33 +-
 Test/dafny1/ExtensibleArray.dfy               |  22 +-
 Test/dafny1/FindZero.dfy                      |   4 +-
 Test/dafny1/Induction.dfy                     |  14 +-
 Test/dafny1/MatrixFun.dfy                     |  12 +-
 Test/dafny1/PriorityQueue.dfy                 |   8 +-
 Test/dafny1/Queue.dfy                         |  36 +-
 Test/dafny1/SchorrWaite.dfy                   |   4 +-
 Test/dafny1/SeparationLogicList.dfy           |   4 +-
 Test/dafny1/Substitution.dfy                  |  14 +-
 Test/dafny1/SumOfCubes.dfy                    |  22 +-
 Test/dafny1/TerminationDemos.dfy              |   6 +-
 Test/dafny1/UltraFilter.dfy                   |  10 +-
 Test/dafny1/pow2.dfy                          |   8 +-
 Test/vacid0/Composite.dfy                     |  30 +-
 Test/vacid0/SparseArray.dfy                   |   8 +-
 48 files changed, 807 insertions(+), 857 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) {
diff --git a/Test/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy
index 1b105ac1..3db9bf72 100644
--- a/Test/VSComp2010/Problem1-SumMax.dfy
+++ b/Test/VSComp2010/Problem1-SumMax.dfy
@@ -38,6 +38,6 @@ method Main()
   a[7] := 1;
   a[8] := 10;
   a[9] := 6;
-  call s, m := M(10, a);
+  var s, m := M(10, a);
   print "N = ", a.Length, "  sum = ", s, "  max = ", m, "\n";
 }
diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy
index bf6aca37..2a262d70 100644
--- a/Test/VSComp2010/Problem2-Invert.dfy
+++ b/Test/VSComp2010/Problem2-Invert.dfy
@@ -61,11 +61,11 @@ method Main()
   a[8] := 5;
   a[9] := 6;
   var b := new int[10];
-  call M(10, a, b);
+  M(10, a, b);
   print "a:\n";
-  call PrintArray(a);
+  PrintArray(a);
   print "b:\n";
-  call PrintArray(b);
+  PrintArray(b);
 }
 
 method PrintArray(a: array<int>)
diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy
index 03e6bdfe..3d24255d 100644
--- a/Test/VSComp2010/Problem3-FindZero.dfy
+++ b/Test/VSComp2010/Problem3-FindZero.dfy
@@ -82,11 +82,11 @@ static method Search(ll: Node) returns (r: int)
 method Main()
 {
   var list: Node := null;
-  call list := list.Cons(0, list);
-  call list := list.Cons(5, list);
-  call list := list.Cons(0, list);
-  call list := list.Cons(8, list);
-  call r := Search(list);
+  list := list.Cons(0, list);
+  list := list.Cons(5, list);
+  list := list.Cons(0, list);
+  list := list.Cons(8, list);
+  var r := Search(list);
   print "Search returns ", r, "\n";
   assert r == 1;
 }
diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy
index ef084674..2f21b7a1 100644
--- a/Test/VSComp2010/Problem4-Queens.dfy
+++ b/Test/VSComp2010/Problem4-Queens.dfy
@@ -39,7 +39,7 @@ method Search(N: int) returns (success: bool, board: seq<int>)
                   ==>
                   (exists p :: 0 <= p && p < N && !IsConsistent(B, p)));
 {
-  call success, board := SearchAux(N, []);
+  success, board := SearchAux(N, []);
 }
 
 // Given a board, this function says whether or not the queen placed in column 'pos'
@@ -110,7 +110,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
 
         // Thus, we meet the precondition of 'SearchAux' on 'candidateBoard', so let's search
         // for a solution that extends 'candidateBoard'.
-        call s, b := SearchAux(N, candidateBoard);
+        var s, b := SearchAux(N, candidateBoard);
         if (s) {
           // The recursive call to 'SearchAux' found consistent positions for all remaining columns
           newBoard := b;
@@ -137,11 +137,11 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
 
 method Main()
 {
-  call s, b := Search(2);
+  var s, b := Search(2);
   print "N=2 returns ", s, "\n";
-  call s, b := Search(4);
+  s, b := Search(4);
   print "N=4 returns ", s, "\n";
-  call PrintSeq(b);
+  PrintSeq(b);
 }
 
 method PrintSeq(b: seq<int>)
diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
index df8cb1b7..0e141927 100644
--- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
@@ -46,8 +46,8 @@ class AmortizedQueue<T> {
       front := f;
       rear := r;
     } else {
-      call rr := r.Reverse();
-      call ff := f.Concat(rr);
+      var rr := r.Reverse();
+      var ff := f.Concat(rr);
       front := ff;
 
       rear := new LinkedList<T>.Init();
@@ -75,7 +75,7 @@ class AmortizedQueue<T> {
     requires Valid();
     ensures r != null && r.Valid() && r.List == List + [item];
   {
-    call rr := rear.Cons(item);
+    var rr := rear.Cons(item);
     r := new AmortizedQueue<T>.InitFromPieces(front, rr);
   }
 }
@@ -133,8 +133,8 @@ class LinkedList<T> {
     if (length == 0) {
       r := end;
     } else {
-      call c := tail.Concat(end);
-      call r := c.Cons(head);
+      var c := tail.Concat(end);
+      r := c.Cons(head);
     }
   }
 
@@ -148,10 +148,10 @@ class LinkedList<T> {
     if (length == 0) {
       r := this;
     } else {
-      call r := tail.Reverse();
+      r := tail.Reverse();
       var e := new LinkedList<T>.Init();
-      call e := e.Cons(head);
-      call r := r.Concat(e);
+      e := e.Cons(head);
+      r := r.Concat(e);
     }
   }
 
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy
index cd4a18c2..3bd2bf43 100644
--- a/Test/VSI-Benchmarks/b1.dfy
+++ b/Test/VSI-Benchmarks/b1.dfy
@@ -35,37 +35,37 @@ method Mul(x: int, y: int) returns (r: int)
   if (x == 0) {
     r := 0;
   } else if (x < 0) {
-    call r := Mul(-x, y);
+    r := Mul(-x, y);
     r := -r;
   } else {
-    call r := Mul(x-1, y);
-    call r := Add(r, y);
+    r := Mul(x-1, y);
+    r := Add(r, y);
   }
 }
 
 // ---------------------------
 
 method Main() {
-  call TestAdd(3, 180);
-  call TestAdd(3, -180);
-  call TestAdd(0, 1);
+  TestAdd(3, 180);
+  TestAdd(3, -180);
+  TestAdd(0, 1);
 
-  call TestMul(3, 180);
-  call TestMul(3, -180);
-  call TestMul(180, 3);
-  call TestMul(-180, 3);
-  call TestMul(0, 1);
-  call TestMul(1, 0);
+  TestMul(3, 180);
+  TestMul(3, -180);
+  TestMul(180, 3);
+  TestMul(-180, 3);
+  TestMul(0, 1);
+  TestMul(1, 0);
 }
 
 method TestAdd(x: int, y: int) {
   print x, " + ", y, " = ";
-  call z := Add(x, y);
+  var z := Add(x, y);
   print z, "\n";
 }
 
 method TestMul(x: int, y: int) {
   print x, " * ", y, " = ";
-  call z := Mul(x, y);
+  var z := Mul(x, y);
   print z, "\n";
 }
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 6c6f11b3..3046621b 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -38,13 +38,13 @@ method Main() {
   a[2] := -2;
   a[3] := 0;
   a[4] := 25;
-  call TestSearch(a, 4);
-  call TestSearch(a, -8);
-  call TestSearch(a, -2);
-  call TestSearch(a, 0);
-  call TestSearch(a, 23);
-  call TestSearch(a, 25);
-  call TestSearch(a, 27);
+  TestSearch(a, 4);
+  TestSearch(a, -8);
+  TestSearch(a, -2);
+  TestSearch(a, 0);
+  TestSearch(a, 23);
+  TestSearch(a, 25);
+  TestSearch(a, 27);
 }
 
 method TestSearch(a: array<int>, key: int)
@@ -52,6 +52,6 @@ method TestSearch(a: array<int>, key: int)
   requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]);
 {
   var b := new Benchmark2;
-  call r := b.BinarySearch(a, key);
+  var r := b.BinarySearch(a, key);
   print "Looking for key=", key, ", result=", r, "\n";
 }
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 3f30c4b5..3de94555 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -87,10 +87,10 @@ class Benchmark3 {
       invariant (forall i :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
       invariant (forall i :: 0 <= i && i < |p| ==> q.contents[i] == old(q.contents)[p[i]]);
     {  
-      call m,k := RemoveMin(q);
+      var m,k := RemoveMin(q);
       perm := perm + [p[k]]; //adds index of min to perm
       p := p[k+1..] + p[..k]; //remove index of min from p  
-      call r.Enqueue(m);
+      r.Enqueue(m);
       pperm := pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] + [pperm[k]];
     }
   }
@@ -116,8 +116,8 @@ class Benchmark3 {
       invariant 0 <= k && k < |old(q.contents)| && old(q.contents)[k] == m;
       invariant (forall i :: 0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far
     {
-      call x:= q.Dequeue();
-      call q.Enqueue(x);
+      var x := q.Dequeue();
+      q.Enqueue(x);
       if (x < m) { k := j; m := x; }
       j := j+1;
     }
@@ -127,11 +127,11 @@ class Benchmark3 {
       invariant j <= k;
       invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; 
     {
-      call x := q.Dequeue();
-      call q.Enqueue(x);
+      var x := q.Dequeue();
+      q.Enqueue(x);
       j := j+1;
     }
 
-    call m:= q.Dequeue();
+    m := q.Dequeue();
   }
 }
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index 9f7e272e..b70ff4d0 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -54,7 +54,7 @@ class Map<Key,Value> {
     ensures !present ==> key !in Keys;
     ensures present ==> (exists i :: 0 <= i && i < |Keys| && Keys[i] == key && Values[i] == val);
   {
-    call p, n, prev := FindIndex(key);
+    var p, n, prev := FindIndex(key);
     if (p == null) {
       present := false;
     } else {
@@ -74,7 +74,7 @@ class Map<Key,Value> {
                     Keys[j] == old(Keys)[j] && Values[j] == old(Values)[j]));
     ensures key !in old(Keys) ==> Keys == [key] + old(Keys) && Values == [val] + old(Values);
   {
-    call p, n, prev := FindIndex(key);
+    var p, n, prev := FindIndex(key);
     if (p == null) {
       var h := new Node<Key,Value>;
       h.key := key;  h.val := val;  h.next := head;
@@ -107,7 +107,7 @@ class Map<Key,Value> {
               Keys[h..] == old(Keys)[h+1..] &&
               Values[h..] == old(Values)[h+1..]);
   {
-    call p, n, prev := FindIndex(key);
+    var p, n, prev := FindIndex(key);
     if (p != null) {
       Keys := Keys[..n] + Keys[n+1..];
       Values := Values[..n] + Values[n+1..];
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index d9bd36f5..cd132ef3 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -98,9 +98,9 @@ class Queue<T> {
     ensures Valid() && fresh(footprint - old(footprint));
     ensures contents == old(contents)[1..] + old(contents)[..1];
   {
-    call t := Front();
-    call Dequeue();
-    call Enqueue(t);
+    var t := Front();
+    Dequeue();
+    Enqueue(t);
   }
 
   method RotateAny()
@@ -112,9 +112,9 @@ class Queue<T> {
     ensures (exists i :: 0 <= i && i <= |contents| &&
               contents == old(contents)[i..] + old(contents)[..i]);
   {
-    call t := Front();
-    call Dequeue();
-    call Enqueue(t);
+    var t := Front();
+    Dequeue();
+    Enqueue(t);
   }
 
 }
@@ -152,18 +152,18 @@ class Main<U> {
     var q0 := new Queue<T>.Init();
     var q1 := new Queue<T>.Init();
 
-    call q0.Enqueue(t);
-    call q0.Enqueue(u);
+    q0.Enqueue(t);
+    q0.Enqueue(u);
 
-    call q1.Enqueue(v);
+    q1.Enqueue(v);
 
     assert |q0.contents| == 2;
 
-    call w := q0.Front();
+    var w := q0.Front();
     assert w == t;
-    call q0.Dequeue();
+    q0.Dequeue();
 
-    call w := q0.Front();
+    w := q0.Front();
     assert w == u;
 
     assert |q0.contents| == 1;
@@ -179,18 +179,18 @@ class Main<U> {
     ensures fresh(q0.footprint - old(q0.footprint));
     ensures fresh(q1.footprint - old(q1.footprint));
   {
-    call q0.Enqueue(t);
-    call q0.Enqueue(u);
+    q0.Enqueue(t);
+    q0.Enqueue(u);
 
-    call q1.Enqueue(v);
+    q1.Enqueue(v);
 
     assert |q0.contents| == 2;
 
-    call w := q0.Front();
+    var w := q0.Front();
     assert w == t;
-    call q0.Dequeue();
+    q0.Dequeue();
 
-    call w := q0.Front();
+    w := q0.Front();
     assert w == u;
 
     assert |q0.contents| == 1;
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index 13086f28..fda9ca74 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -107,14 +107,14 @@ class Client
   method Main()
   {
     var c := new Collection<int>.Init();
-    call c.Add(33);
-    call c.Add(45);
-    call c.Add(78);
+    c.Add(33);
+    c.Add(45);
+    c.Add(78);
     
     var s := [];
     
-    call iter := c.GetIterator();
-    call b := iter.MoveNext();
+    var iter := c.GetIterator();
+    var b := iter.MoveNext();
     
     while (b)
       invariant iter.Valid() && b == iter.HasCurrent() && fresh(iter.footprint);
@@ -123,13 +123,13 @@ class Client
       invariant iter.c == c;
       decreases |c.elements| - iter.pos;
     {   
-      call x := iter.GetCurrent();
+      var x := iter.GetCurrent();
       s := s + [x];
-      call b := iter.MoveNext();
+      b := iter.MoveNext();
     }
     
     assert s == c.elements; //verifies that the iterator returns the correct things
-    call c.Add(100);
+    c.Add(100);
   }
   
 }
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index 2304e602..f34f5c00 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -119,33 +119,34 @@ class Client {
   method Main()
   {
     var rd := new Stream;
-    call rd.Open();
+    rd.Open();
     
     var q := new Queue<int>;  
     while (true)
       invariant rd.Valid() && fresh(rd.footprint) && fresh(q);
       decreases |rd.stream|;
     {
-      call eos := rd.AtEndOfStream();
+      var eos := rd.AtEndOfStream();
       if (eos) {
         break;
       }
         
-      call ch := rd.GetChar();  
-      call q.Enqueue(ch);  
+      var ch := rd.GetChar();  
+      q.Enqueue(ch);  
     }
       
-    call rd.Close();
-    call q,perm := Sort(q);
+    rd.Close();
+    var perm;
+    q,perm := Sort(q);
       
-    var wr:= new Stream;
-    call wr.Create();
+    var wr := new Stream;
+    wr.Create();
     while (0 < |q.contents|)
       invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;
     {
-      call ch := q.Dequeue();  
-      call wr.PutChar(ch);    
+      var ch := q.Dequeue();  
+      wr.PutChar(ch);    
     }
-    call wr.Close();
+    wr.Close();
   }
 }
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 3438d6e0..0c9d1186 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -46,7 +46,7 @@ class Glossary {
   method Main()
   {
     var rs:= new ReaderStream;
-    call rs.Open();
+    rs.Open();
     var glossary := new Map<Word,seq<Word>>.Init();
     var q := new Queue<Word>.Init();
     
@@ -60,21 +60,22 @@ class Glossary {
       invariant q.contents == glossary.keys;
       decreases *;  // we leave out the decreases clause - unbounded stream
     {
-      call term,definition := readDefinition(rs);
+      var term,definition := readDefinition(rs);
       if (term == null) {
         break;
       }
-      call present, d := glossary.Find(term);
+      var present, d := glossary.Find(term);
       if (!present) {
-        call glossary.Add(term,definition);
-        call q.Enqueue(term);
+        glossary.Add(term,definition);
+        q.Enqueue(term);
       }
     }    
     
-    call rs.Close();
-    call q,p := Sort(q);
+    rs.Close();
+    var p;
+    q,p := Sort(q);
     var wr := new WriterStream;
-    call wr.Create();
+    wr.Create();
     
     while (0 < |q.contents|)
       invariant wr.Valid() && fresh(wr.footprint);
@@ -84,12 +85,12 @@ class Glossary {
       invariant q !in wr.footprint;
       invariant (forall k :: k in q.contents ==> k in glossary.keys);
     {
-      call term := q.Dequeue();
-      call present,definition := glossary.Find(term);
+      var term := q.Dequeue();
+      var present,definition := glossary.Find(term);
       assert present;
       
       // write term with a html anchor
-      call wr.PutWordInsideTag(term, term);
+      wr.PutWordInsideTag(term, term);
       var i := 0;
 
       var qcon := q.contents;
@@ -103,19 +104,20 @@ class Glossary {
         invariant (forall k :: k in q.contents ==> k in glossary.keys);
       {
         var w := definition[i];
-        call present, d := glossary.Find(w);
+        var d;
+        present, d := glossary.Find(w);
         if (present)
         {
-          call wr. PutWordInsideHyperlink(w, w);
+          wr. PutWordInsideHyperlink(w, w);
         }
         else 
         {
-          call wr. PutWord(w);
+          wr. PutWord(w);
         }
         i:= i +1;
       }
     }
-    call wr.Close();          
+    wr.Close();          
   }
     
 
@@ -125,7 +127,7 @@ class Glossary {
     ensures rs.Valid() && fresh(rs.footprint - old(rs.footprint));
     ensures term != null ==> null !in definition;
   {
-    call term := rs.GetWord();
+    term := rs.GetWord();
     if (term != null)
     {
       definition := [];
@@ -134,7 +136,7 @@ class Glossary {
         invariant null !in definition;
         decreases *;  // we leave out the decreases clause - unbounded stream
       {
-        call w := rs.GetWord();
+        var w := rs.GetWord();
         if (w == null)
         {
           break;
@@ -273,7 +275,7 @@ class Map<Key,Value> {
     ensures present ==> (exists i :: 0 <= i && i < |keys| &&
                                      keys[i] == key && values[i] == val);
   {
-    call j := FindIndex(key);
+    var j := FindIndex(key);
     if (j == -1) {
       present := false;
     } else {
@@ -292,7 +294,7 @@ class Map<Key,Value> {
               (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));
     ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];
   {
-    call j := FindIndex(key);
+    var j := FindIndex(key);
     if (j == -1) {
       keys := keys + [key];
       values := values + [val];
@@ -321,7 +323,7 @@ class Map<Key,Value> {
               keys[h..] == old(keys)[h+1..] &&
               values[h..] == old(values)[h+1..]);
   {
-    call j := FindIndex(key);
+    var j := FindIndex(key);
     if (0 <= j) {
       keys := keys[..j] + keys[j+1..];
       values := values[..j] + values[j+1..];
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 289a597d..efcfa8bb 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -22,10 +22,10 @@ class MyClass<T, U> {
       } else {
         this.x := x + 0;
       }
-      call t, u, v := M(true, lotsaObjects);
+      t, u, v := M(true, lotsaObjects);
       var to: MyClass<T,U>;
-      call to, u, v := M(true, lotsaObjects);
-      call to, u, v := to.M(true, lotsaObjects);
+      to, u, v := this.M(true, lotsaObjects);
+      to, u, v := to.M(true, lotsaObjects);
       assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
     }
   }
@@ -70,9 +70,9 @@ TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, g
 TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
 TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
 TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)
-TypeTests.dfy(11,4): Error: incorrect type of method in-parameter 0 (expected int, got bool)
-TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 0 (expected int, got C)
-TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C, got int)
+TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
 TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed
 TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
 TypeTests.dfy(55,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
@@ -85,12 +85,12 @@ TypeTests.dfy(80,17): Error: a method called as an initialization method must no
 TypeTests.dfy(89,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
 TypeTests.dfy(90,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
 TypeTests.dfy(96,9): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(97,6): Error: sorry, cannot instantiate 'array' type with a subrange type
-TypeTests.dfy(98,6): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(97,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(98,8): Error: sorry, cannot instantiate 'array' type with a subrange type
 22 resolution/type errors detected in TypeTests.dfy
 
 -------------------- NatTypes.dfy --------------------
-NatTypes.dfy(7,10): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
 Execution trace:
     (0,0): anon0
 NatTypes.dfy(31,5): Error: value assigned to a nat must be non-negative
@@ -119,7 +119,7 @@ Execution trace:
     (0,0): anon0
     (0,0): anon5_Else
     (0,0): anon6_Then
-NatTypes.dfy(89,9): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(89,16): Error: value assigned to a nat must be non-negative
 Execution trace:
     (0,0): anon0
     (0,0): anon3_Then
@@ -160,11 +160,11 @@ Execution trace:
     (0,0): anon0
     (0,0): anon4_Else
     (0,0): anon3
-SmallTests.dfy(129,7): Error: call may violate caller's modifies clause
+SmallTests.dfy(129,9): Error: call may violate caller's modifies clause
 Execution trace:
     (0,0): anon0
     (0,0): anon3_Then
-SmallTests.dfy(131,7): Error: call may violate caller's modifies clause
+SmallTests.dfy(131,9): Error: call may violate caller's modifies clause
 Execution trace:
     (0,0): anon0
     (0,0): anon3_Else
@@ -402,7 +402,7 @@ Execution trace:
 Dafny program verifier finished with 3 verified, 3 errors
 
 -------------------- ResolutionErrors.dfy --------------------
-ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'class' context
+ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'static' context
 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
 ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
 ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
@@ -410,9 +410,11 @@ ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got arra
 ResolutionErrors.dfy(45,14): Error: a field must be selected via an object, not just a class name
 ResolutionErrors.dfy(46,7): Error: unresolved identifier: F
 ResolutionErrors.dfy(47,14): Error: an instance function must be selected via an object, not just a class name
+ResolutionErrors.dfy(47,7): Error: call to instance function requires an instance
 ResolutionErrors.dfy(48,7): Error: unresolved identifier: G
-ResolutionErrors.dfy(50,2): Error: member M does not exist in class _default
-ResolutionErrors.dfy(52,2): Error: member N does not exist in class _default
+ResolutionErrors.dfy(50,7): Error: unresolved identifier: M
+ResolutionErrors.dfy(51,7): Error: call to instance method requires an instance
+ResolutionErrors.dfy(52,7): Error: unresolved identifier: N
 ResolutionErrors.dfy(55,8): Error: non-function expression is called with parameters
 ResolutionErrors.dfy(56,14): Error: member z does not exist in class Global
 ResolutionErrors.dfy(75,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
@@ -420,7 +422,7 @@ ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype construc
 ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
 ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
 ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
-18 resolution/type errors detected in ResolutionErrors.dfy
+20 resolution/type errors detected in ResolutionErrors.dfy
 
 -------------------- Array.dfy --------------------
 Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause
@@ -512,11 +514,11 @@ Dafny program verifier finished with 7 verified, 1 error
 Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
 Modules0.dfy(13,7): Error: module T named among imports does not exist
 Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G
-Modules0.dfy(51,6): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
-Modules0.dfy(62,6): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
-Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
-Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
-Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts
+Modules0.dfy(51,8): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
+Modules0.dfy(62,9): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
+Modules0.dfy(72,9): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
+Modules0.dfy(91,6): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
+Modules0.dfy(116,11): Error: ghost variables are allowed only in specification contexts
 Modules0.dfy(130,11): Error: old expressions are allowed only in specification and ghost contexts
 Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification and ghost contexts
 Modules0.dfy(132,11): Error: allocated expressions are allowed only in specification and ghost contexts
@@ -599,57 +601,57 @@ Execution trace:
 Dafny program verifier finished with 15 verified, 6 errors
 
 -------------------- Termination.dfy --------------------
-Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(103,3): Error: cannot prove termination; try supplying a decreases clause for the loop
 Execution trace:
     (0,0): anon0
-    Termination.dfy(102,3): anon7_LoopHead
+    Termination.dfy(103,3): anon7_LoopHead
     (0,0): anon7_LoopBody
-    Termination.dfy(102,3): anon8_Else
+    Termination.dfy(103,3): anon8_Else
     (0,0): anon3
-    Termination.dfy(102,3): anon9_Else
+    Termination.dfy(103,3): anon9_Else
     (0,0): anon5
-Termination.dfy(110,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(111,3): Error: cannot prove termination; try supplying a decreases clause for the loop
 Execution trace:
     (0,0): anon0
-    Termination.dfy(110,3): anon9_LoopHead
+    Termination.dfy(111,3): anon9_LoopHead
     (0,0): anon9_LoopBody
-    Termination.dfy(110,3): anon10_Else
+    Termination.dfy(111,3): anon10_Else
     (0,0): anon11_Then
     (0,0): anon5
-    Termination.dfy(110,3): anon12_Else
+    Termination.dfy(111,3): anon12_Else
     (0,0): anon7
-Termination.dfy(119,3): Error: decreases expression might not decrease
+Termination.dfy(120,3): Error: decreases expression might not decrease
 Execution trace:
     (0,0): anon0
-    Termination.dfy(119,3): anon9_LoopHead
+    Termination.dfy(120,3): anon9_LoopHead
     (0,0): anon9_LoopBody
-    Termination.dfy(119,3): anon10_Else
+    Termination.dfy(120,3): anon10_Else
     (0,0): anon11_Then
     (0,0): anon5
-    Termination.dfy(119,3): anon12_Else
+    Termination.dfy(120,3): anon12_Else
     (0,0): anon7
-Termination.dfy(120,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
+Termination.dfy(121,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
 Execution trace:
     (0,0): anon0
-    Termination.dfy(119,3): anon9_LoopHead
+    Termination.dfy(120,3): anon9_LoopHead
     (0,0): anon9_LoopBody
-    Termination.dfy(119,3): anon10_Else
+    Termination.dfy(120,3): anon10_Else
     (0,0): anon11_Then
     (0,0): anon5
-    Termination.dfy(119,3): anon12_Else
+    Termination.dfy(120,3): anon12_Else
     (0,0): anon7
-Termination.dfy(248,35): Error: cannot prove termination; try supplying a decreases clause
+Termination.dfy(249,35): Error: cannot prove termination; try supplying a decreases clause
 Execution trace:
     (0,0): anon6_Else
     (0,0): anon7_Else
     (0,0): anon8_Then
-Termination.dfy(288,3): Error: decreases expression might not decrease
+Termination.dfy(289,3): Error: decreases expression might not decrease
 Execution trace:
     (0,0): anon0
-    Termination.dfy(288,3): anon10_LoopHead
+    Termination.dfy(289,3): anon10_LoopHead
     (0,0): anon10_LoopBody
-    Termination.dfy(288,3): anon11_Else
-    Termination.dfy(288,3): anon12_Else
+    Termination.dfy(289,3): anon11_Else
+    Termination.dfy(289,3): anon12_Else
     (0,0): anon13_Else
     (0,0): anon8
 
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index 1eeb2d92..e6b9a87d 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -23,19 +23,19 @@ method TestCalls(k: nat) {
   ghost var r: int;
   ghost var s := Global.G(k);
 
-//  call r := Global.N(k);
+//  r := Global.N(k);
 //  assert r == s;
 
-  call r := g.N(k);
+  r := g.N(k);
   assert r == s;
-  call r := h.N(k);
+  r := h.N(k);
   assert r == s;
 
   g := null;
-  call r := g.N(k);
+  r := g.N(k);
   assert r == s;
 
-//  call r := Global.N(r);
+//  r := Global.N(r);
   if (k == 0) {
     assert r == s;
   } else {
diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy
index 8629a418..d53fb6a5 100644
--- a/Test/dafny0/Comprehensions.dfy
+++ b/Test/dafny0/Comprehensions.dfy
@@ -16,14 +16,14 @@ function method Id(x: int): int { x }  // for triggering
 method Main()
 {
   var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;
-  call PrintSet(q);
+  PrintSet(q);
   q := set b: bool | true :: if b then 3 else 7;
-  call PrintSet(q);
+  PrintSet(q);
   var m := set k | k in q :: 2*k;
-  call PrintSet(m);
-  call PrintSet(set k | k in q && k % 2 == 0);
+  PrintSet(m);
+  PrintSet(set k | k in q && k % 2 == 0);
   var sq := [30, 40, 20];
-  call PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
+  PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
   var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;
 }
 
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index 59052ac2..01e14585 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -38,17 +38,17 @@ module J imports G, M {
 module X2 imports X1 {
   class MyClass2 {
     method Down(x1: MyClass1, x0: MyClass0) {
-      call x1.Down(x0);
+      x1.Down(x0);
     }
     method WayDown(x0: MyClass0, g: ClassG) {
-      call x0.Down();
-      call g.T();  // allowed, because this follows import relation
+      x0.Down();
+      g.T();  // allowed, because this follows import relation
       var t := g.TFunc();  // allowed, because this follows import relation
     }
     method Up() {
     }
     method Somewhere(y: MyClassY) {
-      call y.M();  // error: does not follow import relation
+      y.M();  // error: does not follow import relation
     }
   }
 }
@@ -56,10 +56,10 @@ module X2 imports X1 {
 module X1 imports X0 {
   class MyClass1 {
     method Down(x0: MyClass0) {
-      call x0.Down();
+      x0.Down();
     }
     method Up(x2: MyClass2) {
-      call x2.Up();  // error: does not follow import relation
+      x2.Up();  // error: does not follow import relation
     }
   }
 }
@@ -69,7 +69,7 @@ module X0 {
     method Down() {
     }
     method Up(x1: MyClass1, x2: MyClass2) {
-      call x1.Up(x2);  // error: does not follow import relation
+      x1.Up(x2);  // error: does not follow import relation
     }
   }
 }
@@ -78,7 +78,7 @@ module YY {
   class MyClassY {
     method M() { }
     method P(g: ClassG) {
-      call g.T();  // allowed, because this follows import relation
+      g.T();  // allowed, because this follows import relation
       var t := g.TFunc();  // allowed, because this follows import relation
     }
   }
@@ -88,20 +88,20 @@ class ClassG {
   method T() { }
   function method TFunc(): int { 10 }
   method V(y: MyClassY) {
-    call y.M();  // error: does not follow import relation
+    y.M();  // error: does not follow import relation
   }
 }
 
 method Ping() {
-  call Pong();  // allowed: intra-module call
+  Pong();  // allowed: intra-module call
 }
 
 method Pong() {
-  call Ping();  // allowed: intra-module call
+  Ping();  // allowed: intra-module call
 }
 
 method ProcG(g: ClassG) {
-  call g.T();  // allowed: intra-module call
+  g.T();  // allowed: intra-module call
   var t := g.TFunc();  // allowed: intra-module call
 }
 
@@ -111,11 +111,11 @@ class Ghosty {
   method Caller() {
     var x := 3;
     ghost var y := 3;
-    call Callee(x, y);  // fine
-    call Callee(x, x);  // fine
-    call Callee(y, x);  // error: cannot pass in ghost to a physical formal
-    call Theorem(x);  // fine
-    call Theorem(y);  // fine, because it's a ghost method
+    Callee(x, y);  // fine
+    Callee(x, x);  // fine
+    Callee(y, x);  // error: cannot pass in ghost to a physical formal
+    Theorem(x);  // fine
+    Theorem(y);  // fine, because it's a ghost method
   }
   method Callee(a: int, ghost b: int) { }
   ghost method Theorem(a: int) { }
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index cfefa7fa..ff84b84b 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -37,7 +37,7 @@ method Proc0(x: int)
   decreases x;
 {
   if (0 <= x) {
-    call Proc1(x - 1);
+    Proc1(x - 1);
   }
 }
 
@@ -45,18 +45,18 @@ method Proc1(x: int)
   decreases x;
 {
   if (0 <= x) {
-    call Proc0(x - 1);
+    Proc0(x - 1);
   }
 }
 
 method Botch0(x: int)
   decreases x;
 {
-  call Botch1(x - 1);  // error: failure to keep termination metric bounded
+  Botch1(x - 1);  // error: failure to keep termination metric bounded
 }
 
 method Botch1(x: int)
   decreases x;
 {
-  call Botch0(x);  // error: failure to decrease termination metric
+  Botch0(x);  // error: failure to decrease termination metric
 }
diff --git a/Test/dafny0/MultiDimArray.dfy b/Test/dafny0/MultiDimArray.dfy
index ba5dc9da..ff30ef8a 100644
--- a/Test/dafny0/MultiDimArray.dfy
+++ b/Test/dafny0/MultiDimArray.dfy
@@ -74,7 +74,7 @@ class A {
       var s := z[1,2,4];  // first three powers of 2 (tra-la-la)
       var some: A;
       f[i,j,k] := some;
-      call M3(i-1, j, k);
+      M3(i-1, j, k);
       assert s == z[1,2,4];
       if (*) {
         assert f[i,j,k] == some;  // error: the recursive call may have modified any element in 'f'
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 161ac22f..e4d0cbe7 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -3,8 +3,8 @@ method M(n: nat) {
 }
 
 method Main() {
-  call M(25);
-  call M(-25);  // error: cannot pass -25 as a nat
+  M(25);
+  M(-25);  // error: cannot pass -25 as a nat
 }
 
 var f: nat;
@@ -34,7 +34,7 @@ method CheckField(x: nat, y: int)
 method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
   if (0 < i) {
     var n: nat := 5;
-    call j := Generic(i-1, n, -4);
+    var j := Generic(i-1, n, -4);
     assert 0 <= j;  // error: the result is an int, not a nat
     var q := FenEric(n, -4);
     assert 0 <= q;  // error: the result is an int, not a nat
@@ -65,7 +65,7 @@ method MatchIt(list: List<object>) returns (k: nat)
   match (list) {
     case Nil =>
     case Cons(n, extra, tail) =>
-      call w := MatchIt(tail);
+      var w := MatchIt(tail);
       assert 0 <= w;
       assert 0 <= n;  // fine
       assert 0 <= n - 10;  // error: possible assertion failure
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index b33d4d54..56d7575f 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -47,10 +47,10 @@ method TestNameResolution0() {
   z := Global.F(2);  // error: invocation of instance function requires an instance
   z := G(2);  // error: cannot resolve G
   z := Global.G(2);
-  call z := M(2);  // error: cannot resolve M
-//  call z := Global.M(2);  // error: call to instance method requires an instance
-  call z := N(1);  // error: cannot resolve N
-//  call z := Global.N(1);
+  z := M(2);  // error: cannot resolve M
+  z := Global.M(2);  // error: call to instance method requires an instance
+  z := N(1);  // error: cannot resolve N
+  z := Global.N(1);
 
   z := z(5);  // error: using local as if it were a function
   z := Global.z;  // error: class Global does not have a member z
@@ -59,7 +59,7 @@ method TestNameResolution0() {
   z := Global.X;  // this means the instance field X of the object stored in the local variable 'Global'
   var gg: Global := null;
   var y := gg.G(5);
-  call y := gg.N(5);
+  y := gg.N(5);
 }
 
 datatype Abc = Abel | Benny | Cecilia(y: int) | David(x: int) | Eleanor;
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy
index 930c4253..e1416094 100644
--- a/Test/dafny0/Simple.dfy
+++ b/Test/dafny0/Simple.dfy
@@ -20,10 +20,10 @@ class MyClass<T,U> {
       } else {
         this.x := x + 0;
       }
-      call t, u, v := M(true, lotsaObjects);
+      t, u, v := M(true, lotsaObjects);
       var to: MyClass<T,U>;
-      call to, u, v := this.M(true, lotsaObjects);
-      call to, u, v := to.M(true, lotsaObjects);
+      to, u, v := this.M(true, lotsaObjects);
+      to, u, v := to.M(true, lotsaObjects);
       assert v[x] != null ==> null !in v[2..x][1..][5 := v[this.x]][..10];
     }
   }
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 3359cff1..fcc764aa 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -109,11 +109,11 @@ class Modifies {
   method B(p: Modifies)
     modifies this;
   {
-    call A(this);
+    A(this);
     if (p == this) {
-      call p.A(p);
+      p.A(p);
     }
-    call A(p);  // error: may violate modifies clause
+    A(p);  // error: may violate modifies clause
   }
 
   method C(b: bool)
@@ -126,9 +126,9 @@ class Modifies {
     requires p != null;
   {
     if (y == 3) {
-      call p.C(true);  // error: may violate modifies clause
+      p.C(true);  // error: may violate modifies clause
     } else {
-      call p.C(false);  // error: may violation modifies clause (the check is done without regard
+      p.C(false);  // error: may violation modifies clause (the check is done without regard
                         // for the postcondition, which also makes sense, since there may, in
                         // principle, be other fields of the object that are not constrained by the
                         // postcondition)
@@ -138,7 +138,7 @@ class Modifies {
   method E()
     modifies this;
   {
-    call A(null);  // allowed
+    A(null);  // allowed
   }
 
   method F(s: set<Modifies>)
@@ -164,7 +164,7 @@ class Modifies {
       foreach (m in s) {
         m.x := m.x + 1;
       }
-      call F(s);
+      F(s);
     }
     foreach (m in s) {
       assert m.x < m.x + 10;  // nothing wrong with asserting something
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 5d411eb3..155fbaef 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -28,8 +28,8 @@ class Termination {
   }
 
   method Lex() {
-    call x := Update();
-    call y := Update();
+    var x := Update();
+    var y := Update();
     while (!(x == 0 && y == 0))
       invariant 0 <= x && 0 <= y;
       decreases x, y;
@@ -38,7 +38,7 @@ class Termination {
         y := y - 1;
       } else {
         x := x - 1;
-        call y := Update();
+        y := Update();
       }
     }
   }
@@ -82,7 +82,8 @@ class Termination {
     while (l != List.Nil)
       decreases l;
     {
-      call x, l := Traverse(l);
+      var x;
+      x, l := Traverse(l);
     }
   }
 
@@ -204,7 +205,7 @@ method OuterOld(a: int)
   decreases a, true;
 {
   count := count + 1;
-  call InnerOld(a, count);
+  InnerOld(a, count);
 }
 
 method InnerOld(a: int, b: int)
@@ -213,9 +214,9 @@ method InnerOld(a: int, b: int)
 {
   count := count + 1;
   if (b == 0 && 1 <= a) {
-    call OuterOld(a - 1);
+    OuterOld(a - 1);
   } else if (1 <= b) {
-    call InnerOld(a, b - 1);
+    InnerOld(a, b - 1);
   }
 }
 
@@ -225,7 +226,7 @@ method Outer(a: int)
   modifies this;
 {
   count := count + 1;
-  call Inner(a, count);
+  Inner(a, count);
 }
 
 method Inner(a: int, b: int)
@@ -233,9 +234,9 @@ method Inner(a: int, b: int)
 {
   count := count + 1;
   if (b == 0 && 1 <= a) {
-    call Outer(a - 1);
+    Outer(a - 1);
   } else if (1 <= b) {
-    call Inner(a, b - 1);
+    Inner(a, b - 1);
   }
 }
 
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index a932eccf..38050b88 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -35,7 +35,7 @@ method BadLemma(c0: Color, c1: Color)
 }
 
 method Main() {
-  call BadLemma(Color.Yellow, Color.Blue);
+  BadLemma(Color.Yellow, Color.Blue);
   assert false;  // this shows how things can really go wrong if BadLemma verified successfully
 }
 
@@ -68,7 +68,7 @@ method M(list: List, S: set<MyClass>) returns (ret: int)
         assert false;  // error
       }
   }
-  call k := N();
+  var k := N();
   assert k.H() == 5;
   ghost var l := NF();
   assert l != null ==> l.H() == 5;
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index a044341e..a3698dc0 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -13,7 +13,7 @@ class C<U> {
   method Main(u: U)
   {
     var t := F(3,u) && F(this,u);
-    call kz := M(t,u);
+    var kz := M(t,u);
     assert kz && (G() || !G());
   }
 
@@ -30,14 +30,14 @@ class SetTest {
   method Good()
   {
     var s := {2, 5, 3};
-    call t := Add(s, 7);
+    var t := Add(s, 7);
     assert {5,7,2,3} == t;
   }
 
   method Bad()
   {
     var s := {2, 50, 3};
-    call t := Add(s, 7);
+    var t := Add(s, 7);
     assert {5,7,2,3} == t;  // error
   }
 }
@@ -52,14 +52,14 @@ class SequenceTest {
   method Good()
   {
     var s := [2, 5, 3];
-    call t := Add(s, 7);
+    var t := Add(s, 7);
     assert [2,5,3,7] == t;
   }
 
   method Bad()
   {
     var s := [2, 5, 3];
-    call t := Add(s, 7);
+    var t := Add(s, 7);
     assert [2,5,7,3] == t || [2,5,3] == t;  // error
   }
 }
@@ -92,7 +92,7 @@ class CClient {
     }
     c.x := 5;
     c.x := c.x;
-    call z := c.M(c, 17);
+    var z := c.M(c, 17);
     assert z == c.x;
   }
 }
@@ -170,7 +170,7 @@ method TyKn_Main(k0: TyKn_K) {
 
   assert c.x != null ==> c.x.F() == 176;  // the Dafny encoding needs the canCall mechanism to verify this
   assert c.G() != null ==> c.G().F() == 176;  // ditto
-  call k2 := c.M();
+  var k2 := c.M();
   assert k2 != null ==> k2.F() == 176;  // the canCall mechanism does the trick here, but so does the encoding
                                         // via k2's where clause
 }
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 7deeb0a1..21f0dda8 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -8,8 +8,8 @@ class C {
 
   method Caller()
   {
-    call m,n := M(true);  // error on in-parameter
-    call n,m := M(m);  // 2 errors on out-parameters
+    var m,n := M(true);  // error on in-parameter
+    n,m := M(m);  // 2 errors on out-parameters
   }
 }
 
diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy
index b4980d4b..88b06605 100644
--- a/Test/dafny1/BinaryTree.dfy
+++ b/Test/dafny1/BinaryTree.dfy
@@ -32,7 +32,7 @@ class IntSet {
     if (root == null) {
       present := false;
     } else {
-      call present := root.Find(x);
+      present := root.Find(x);
     }
   }
 
@@ -42,7 +42,7 @@ class IntSet {
     ensures Valid() && fresh(Repr - old(Repr));
     ensures Contents == old(Contents) + {x};
   { 
-    call t := InsertHelper(x, root);
+    var t := InsertHelper(x, root);
     root := t;
     Contents := root.Contents;
     Repr := root.Repr + {this};
@@ -64,12 +64,12 @@ class IntSet {
     } else {
       if (x < n.data) {
         assert n.right == null || n.right.Valid();
-        call t := InsertHelper(x, n.left);
+        var t := InsertHelper(x, n.left);
         n.left := t;
         n.Repr := n.Repr + n.left.Repr;
       } else {
         assert n.left == null || n.left.Valid();
-        call t := InsertHelper(x, n.right);
+        var t := InsertHelper(x, n.right);
         n.right := t;
         n.Repr := n.Repr + n.right.Repr;
       }
@@ -85,7 +85,7 @@ class IntSet {
     ensures Contents == old(Contents) - {x};
   {
     if (root != null) {
-      call newRoot := root.Remove(x);
+      var newRoot := root.Remove(x);
       root := newRoot;
       if (root == null) {
         Contents := {};
@@ -152,9 +152,9 @@ class Node {
     if (x == data) {
       present := true;
     } else if (left != null && x < data) {
-      call present := left.Find(x);
+      present := left.Find(x);
     } else if (right != null && data < x) {
-      call present := right.Find(x);
+      present := right.Find(x);
     } else {
       present := false;
     }
@@ -171,12 +171,12 @@ class Node {
   {
     node := this;
     if (left != null && x < data) {
-      call t := left.Remove(x);
+      var t := left.Remove(x);
       left := t;
       Contents := Contents - {x};
       if (left != null) { Repr := Repr + left.Repr; }
     } else if (right != null && data < x) {
-      call t := right.Remove(x);
+      var t := right.Remove(x);
       right := t;
       Contents := Contents - {x};
       if (right != null) { Repr := Repr + right.Repr; }
@@ -189,7 +189,7 @@ class Node {
         node := left;
       } else {
         // rotate
-        call min, r := right.RemoveMin();
+        var min, r := right.RemoveMin();
         data := min;  right := r;
         Contents := Contents - {x};
         if (right != null) { Repr := Repr + right.Repr; }
@@ -211,7 +211,8 @@ class Node {
       min := data;
       node := right;
     } else {
-      call min, t := left.RemoveMin();
+      var t;
+      min, t := left.RemoveMin();
       left := t;
       node := this;
       Contents := Contents - {min};
@@ -225,9 +226,9 @@ class Main {
   {
     var s := new IntSet.Init();
 
-    call s.Insert(12);
-    call s.Insert(24);
-    call present := s.Find(x);
+    s.Insert(12);
+    s.Insert(24);
+    var present := s.Find(x);
     assert present <==> x == 12 || x == 24;
   }
 
@@ -235,8 +236,8 @@ class Main {
     requires s != null && s.Valid();
     modifies s.Repr;
   {
-    call s.Insert(x);
-    call s.Insert(24);
+    s.Insert(x);
+    s.Insert(24);
     assert old(s.Contents) - {x,24} == s.Contents - {x,24};
   }
 }
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index 089a72c4..2dc49cd9 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -57,7 +57,7 @@ class ExtensibleArray<T> {
     if (M <= i) {
       t := elements[i - M];
     } else {
-      call arr := more.Get(i / 256);
+      var arr := more.Get(i / 256);
       t := arr[i % 256];
     }
   }
@@ -72,7 +72,7 @@ class ExtensibleArray<T> {
     if (M <= i) {
       elements[i - M] := t;
     } else {
-      call arr := more.Get(i / 256);
+      var arr := more.Get(i / 256);
       arr[i % 256] := t;
     }
     Contents := Contents[i := t];
@@ -94,7 +94,7 @@ class ExtensibleArray<T> {
         Repr := Repr + {more} + more.Repr;
       }
       // "elements" is full, so move it into "more" and allocate a new array
-      call more.Append(elements);
+      more.Append(elements);
       Repr := Repr + more.Repr;
       M := M + 256;
       elements := new T[256];
@@ -113,14 +113,14 @@ method Main() {
     invariant a.Valid() && fresh(a.Repr);
     invariant |a.Contents| == n;
   {
-    call a.Append(n);
+    a.Append(n);
     n := n + 1;
   }
-  call k := a.Get(570); print k, "\n";
-  call k := a.Get(0); print k, "\n";
-  call k := a.Get(1000); print k, "\n";
-  call a.Set(1000, 23);
-  call k := a.Get(0); print k, "\n";
-  call k := a.Get(1000); print k, "\n";
-  call k := a.Get(66000); print k, "\n";
+  var k := a.Get(570); print k, "\n";
+  k := a.Get(0); print k, "\n";
+  k := a.Get(1000); print k, "\n";
+  a.Set(1000, 23);
+  k := a.Get(0); print k, "\n";
+  k := a.Get(1000); print k, "\n";
+  k := a.Get(66000); print k, "\n";
 }
diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index cff8b934..76e67205 100644
--- a/Test/dafny1/FindZero.dfy
+++ b/Test/dafny1/FindZero.dfy
@@ -9,7 +9,7 @@ method FindZero(a: array<int>) returns (r: int)
     invariant forall i :: 0 <= i && i < n && i < a.Length ==> a[i] != 0;
   {
     if (a[n] == 0) { r := n; return; }
-    call Lemma(a, n, a[n]);
+    Lemma(a, n, a[n]);
     n := n + a[n];
   }
   r := -1;
@@ -25,6 +25,6 @@ ghost method Lemma(a: array<int>, k: int, m: int)
 {
   if (0 < m && k < a.Length) {
     assert a[k] != 0;
-    call Lemma(a, k+1, m-1);
+    Lemma(a, k+1, m-1);
   }
 }
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 0e4c58e0..2c90769b 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -24,8 +24,8 @@ class IntegerInduction {
     ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
   {
     if (n != 0) {
-      call Theorem0(n-1);
-      call Lemma(n-1);
+      Theorem0(n-1);
+      Lemma(n-1);
     }
   }
 
@@ -33,7 +33,7 @@ class IntegerInduction {
     requires 0 <= n;
     ensures 2 * Gauss(n) == n*(n+1);
   {
-    if (n != 0) { call Lemma(n-1); }
+    if (n != 0) { Lemma(n-1); }
   }
 
   // Here is another proof.  It states the lemma as part of the theorem, and
@@ -45,7 +45,7 @@ class IntegerInduction {
     ensures 2 * Gauss(n) == n*(n+1);
   {
     if (n != 0) {
-      call Theorem1(n-1);
+      Theorem1(n-1);
     }
   }
 
@@ -64,7 +64,7 @@ class IntegerInduction {
     ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
   {
     if (n != 0) {
-      call Theorem2(n-1);
+      Theorem2(n-1);
 
       assert (forall m :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));
     }
@@ -84,7 +84,7 @@ class IntegerInduction {
     ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
   {
     if (n != 0) {
-      call Theorem3(n-1);
+      Theorem3(n-1);
     }
   }
 
@@ -112,7 +112,7 @@ class IntegerInduction {
     if (*) {
       assert (forall m :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));
     } else {
-      call Theorem4();
+      Theorem4();
     }
   }
 
diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy
index 86ad451d..81b3f4c9 100644
--- a/Test/dafny1/MatrixFun.dfy
+++ b/Test/dafny1/MatrixFun.dfy
@@ -64,20 +64,20 @@ method Main()
   B[0,0] := true;  B[0,1] := false;  B[0,2] := false;  B[0,3] := true;  B[0,4] := false;
   B[1,0] := true;  B[1,1] := true;   B[1,2] := true;   B[1,3] := true;  B[1,4] := false;
   print "Before:\n";
-  call PrintMatrix(B);
-  call MirrorImage(B);
+  PrintMatrix(B);
+  MirrorImage(B);
   print "Mirror image:\n";
-  call PrintMatrix(B);
+  PrintMatrix(B);
 
   var A := new int[3,3];
   A[0,0] := 5;  A[0,1] := 7;  A[0,2] := 9;
   A[1,0] := 6;  A[1,1] := 2;  A[1,2] := 3;
   A[2,0] := 7;  A[2,1] := 1;  A[2,2] := 0;
   print "Before:\n";
-  call PrintMatrix(A);
-  call Flip(A);
+  PrintMatrix(A);
+  Flip(A);
   print "Flip:\n";
-  call PrintMatrix(A);
+  PrintMatrix(A);
 }
 
 method PrintMatrix<T>(m: array2<T>)
diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index db1c60fa..6e19ab8f 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -41,7 +41,7 @@ class PriorityQueue {
   {
     n := n + 1;
     a[n] := x;
-    call SiftUp(n);
+    SiftUp(n);
   }
 
   method SiftUp(k: int)
@@ -76,7 +76,7 @@ class PriorityQueue {
     x := a[1];
     a[1] := a[n];
     n := n - 1;
-    call SiftDown(1);
+    SiftDown(1);
   }
 
   method SiftDown(k: int)
@@ -156,7 +156,7 @@ class PriorityQueue_Alternative {
   {
     n := n + 1;
     a[n] := x;
-    call SiftUp();
+    SiftUp();
   }
 
   method SiftUp()
@@ -189,7 +189,7 @@ class PriorityQueue_Alternative {
     x := a[1];
     a[1] := a[n];
     n := n - 1;
-    call SiftDown();
+    SiftDown();
   }
 
   method SiftDown()
diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy
index 0ee953e1..bfb588be 100644
--- a/Test/dafny1/Queue.dfy
+++ b/Test/dafny1/Queue.dfy
@@ -48,9 +48,9 @@ class Queue<T> {
     ensures Valid() && fresh(footprint - old(footprint));
     ensures contents == old(contents)[1..] + old(contents)[..1];
   {
-    call t := Front();
-    call Dequeue();
-    call Enqueue(t);
+    var t := Front();
+    Dequeue();
+    Enqueue(t);
   }
 
   method RotateAny()
@@ -62,9 +62,9 @@ class Queue<T> {
     ensures (exists i :: 0 <= i && i <= |contents| &&
               contents == old(contents)[i..] + old(contents)[..i]);
   {
-    call t := Front();
-    call Dequeue();
-    call Enqueue(t);
+    var t := Front();
+    Dequeue();
+    Enqueue(t);
   }
 
   method IsEmpty() returns (isEmpty: bool)
@@ -152,18 +152,18 @@ class Main<U> {
     var q0 := new Queue<T>.Init();
     var q1 := new Queue<T>.Init();
 
-    call q0.Enqueue(t);
-    call q0.Enqueue(u);
+    q0.Enqueue(t);
+    q0.Enqueue(u);
 
-    call q1.Enqueue(v);
+    q1.Enqueue(v);
 
     assert |q0.contents| == 2;
 
-    call w := q0.Front();
+    var w := q0.Front();
     assert w == t;
-    call q0.Dequeue();
+    q0.Dequeue();
 
-    call w := q0.Front();
+    w := q0.Front();
     assert w == u;
 
     assert |q0.contents| == 1;
@@ -179,18 +179,18 @@ class Main<U> {
     ensures fresh(q0.footprint - old(q0.footprint));
     ensures fresh(q1.footprint - old(q1.footprint));
   {
-    call q0.Enqueue(t);
-    call q0.Enqueue(u);
+    q0.Enqueue(t);
+    q0.Enqueue(u);
 
-    call q1.Enqueue(v);
+    q1.Enqueue(v);
 
     assert |q0.contents| == 2;
 
-    call w := q0.Front();
+    var w := q0.Front();
     assert w == t;
-    call q0.Dequeue();
+    q0.Dequeue();
 
-    call w := q0.Front();
+    w := q0.Front();
     assert w == u;
 
     assert |q0.contents| == 1;
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 33442219..95cdab89 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -26,7 +26,7 @@ class Main {
                 n.childrenVisited == old(n.childrenVisited) &&
                 n.children == old(n.children));
   {
-    call RecursiveMarkWorker(root, S, {});
+    RecursiveMarkWorker(root, S, {});
   }
 
   method RecursiveMarkWorker(root: Node, ghost S: set<Node>, ghost stackNodes: set<Node>)
@@ -67,7 +67,7 @@ class Main {
       {
         var c := root.children[i];
         if (c != null) {
-          call RecursiveMarkWorker(c, S, stackNodes + {root});
+          RecursiveMarkWorker(c, S, stackNodes + {root});
         }
         i := i + 1;
       }
diff --git a/Test/dafny1/SeparationLogicList.dfy b/Test/dafny1/SeparationLogicList.dfy
index 7828a54e..56a64bd6 100644
--- a/Test/dafny1/SeparationLogicList.dfy
+++ b/Test/dafny1/SeparationLogicList.dfy
@@ -28,7 +28,7 @@ class Node<T> {
       l.next := null;
       S := {l};
     } else {
-      call l, S := Cons(x, null, [], {});
+      l, S := Cons(x, null, [], {});
     }
   }
 
@@ -75,7 +75,7 @@ class ListNode<T> {
       l.Repr := {l};
       l.Contents := [x];
     } else {
-      call l := Cons(x, null);
+      l := Cons(x, null);
     }
   }
 
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 5cee5f6a..d3e0e82e 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -31,7 +31,7 @@ static ghost method Theorem(e: Expr, v: int, val: int)
     case Const(c) =>
     case Var(x) =>
     case Nary(op, args) =>
-      call Lemma(args, v, val);
+      Lemma(args, v, val);
   }
 }
 
@@ -41,8 +41,8 @@ static ghost method Lemma(l: List, v: int, val: int)
   match l {
     case Nil =>
     case Cons(e, tail) =>
-      call Theorem(e, v, val);
-      call Lemma(tail, v, val);
+      Theorem(e, v, val);
+      Lemma(tail, v, val);
   }
 }
 
@@ -80,11 +80,11 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
     case Var(x) =>
     case Nary(op, args) =>
       ghost var seArgs := SubstSeq(e, args, v, val);
-      call LemmaSeq(e, args, v, val);
+      LemmaSeq(e, args, v, val);
 
       ghost var se := Substitute(e, v, val);
       ghost var seArgs2 := SubstSeq(se, seArgs, v, val);
-      call LemmaSeq(se, seArgs, v, val);
+      LemmaSeq(se, seArgs, v, val);
 
       var N := |args|;
       var j := 0;
@@ -92,7 +92,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
         invariant j <= N;
         invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);
       {
-        call TheoremSeq(args[j], v, val);
+        TheoremSeq(args[j], v, val);
         j := j + 1;
       }
       assert seArgs == seArgs2;
@@ -107,6 +107,6 @@ static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>,
 {
   if (q == []) {
   } else {
-    call LemmaSeq(parent, q[..|q|-1], v, val);
+    LemmaSeq(parent, q[..|q|-1], v, val);
   }
 }
diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy
index 2fecaee5..7ed7ce9b 100644
--- a/Test/dafny1/SumOfCubes.dfy
+++ b/Test/dafny1/SumOfCubes.dfy
@@ -10,19 +10,19 @@ class SumOfCubes {
     requires 0 <= n && n <= m;
     ensures r == SumEmUp(n, m);
   {
-    call a := SocuFromZero(m);
-    call b := SocuFromZero(n);
+    var a := SocuFromZero(m);
+    var b := SocuFromZero(n);
     r := a - b;
-    call Lemma0(n, m);
+    Lemma0(n, m);
   }
 
   static method SocuFromZero(k: int) returns (r: int)
     requires 0 <= k;
     ensures r == SumEmUp(0, k);
   {
-    call g := Gauss(k);
+    var g := Gauss(k);
     r := g * g;
-    call Lemma1(k);
+    Lemma1(k);
   }
 
   ghost static method Lemma0(n: int, m: int)
@@ -36,9 +36,9 @@ class SumOfCubes {
     {
       k := k + 1;
     }
-    call Lemma3(0, n);
-    call Lemma3(n, k);
-    call Lemma3(0, k);
+    Lemma3(0, n);
+    Lemma3(n, k);
+    Lemma3(0, k);
   }
 
   static function GSum(k: int): int
@@ -52,7 +52,7 @@ class SumOfCubes {
     ensures r == GSum(k);
   {
     r := k * (k - 1) / 2;
-    call Lemma2(k);
+    Lemma2(k);
   }
 
   ghost static method Lemma1(k: int)
@@ -64,10 +64,10 @@ class SumOfCubes {
       invariant i <= k;
       invariant SumEmDown(0, i) == GSum(i) * GSum(i);
     {
-      call Lemma2(i);
+      Lemma2(i);
       i := i + 1;
     }
-    call Lemma3(0, k);
+    Lemma3(0, k);
   }
 
   ghost static method Lemma2(k: int)
diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index 49f5a075..0aa36a10 100644
--- a/Test/dafny1/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -58,10 +58,10 @@ class Ackermann {
     if (m == 0) {
       r := n + 1;
     } else if (n == 0) {
-      call r := ComputeAck(m - 1, 1);
+      r := ComputeAck(m - 1, 1);
     } else {
-      call s := ComputeAck(m, n - 1);
-      call r := ComputeAck(m - 1, s);
+      var s := ComputeAck(m, n - 1);
+      r := ComputeAck(m - 1, s);
     }
   }
 }
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index 61e86836..189ff2b5 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -22,9 +22,9 @@ class UltraFilter<G> {
   {
     if (M !in f) {
       // instantiate 'g' with the following 'h'
-      call h := H(f, S, M);
-      call Lemma_HIsFilter(h, f, S, M);
-      call Lemma_FHOrdering0(h, f, S, M);
+      var h := H(f, S, M);
+      Lemma_HIsFilter(h, f, S, M);
+      Lemma_FHOrdering0(h, f, S, M);
     }
   }
 
@@ -44,9 +44,9 @@ class UltraFilter<G> {
     // call Lemma_H1(h, f, S, M, *, *);
     assume (forall C, D :: C in h && D in h ==> C * D in h);
 
-    call Lemma_H2(h, f, S, M);
+    Lemma_H2(h, f, S, M);
 
-    call Lemma_H3(h, f, S, M);
+    Lemma_H3(h, f, S, M);
   }
 
   method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)
diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy
index 52cddaac..c7e4bc63 100644
--- a/Test/dafny1/pow2.dfy
+++ b/Test/dafny1/pow2.dfy
@@ -36,7 +36,7 @@ ghost method Lemma(n: int)
   ensures pow2_slow(n) == Square(pow2_slow(n/2));
 {
   if (n != 0) {
-    call Lemma(n-2);
+    Lemma(n-2);
   }
 }
 
@@ -46,9 +46,9 @@ ghost method Theorem(n: int)
 {
   if (n == 0) {
   } else if (IsEven(n)) {
-    call Lemma(n);
-    call Theorem(n/2);
+    Lemma(n);
+    Theorem(n/2);
   } else {
-    call Theorem(n-1);
+    Theorem(n-1);
   }
 }
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy
index 95ad12fa..ed376931 100644
--- a/Test/vacid0/Composite.dfy
+++ b/Test/vacid0/Composite.dfy
@@ -44,7 +44,7 @@ class Composite {
   {
     var delta := x - val;
     val := x;
-    call Adjust(delta, S, S);
+    Adjust(delta, S, S);
   }
 
   method Add(ghost S: set<Composite>, child: Composite, ghost U: set<Composite>)
@@ -73,7 +73,7 @@ class Composite {
       right := child;
     }
     child.parent := this;
-    call Adjust(child.sum, S, S+U);
+    Adjust(child.sum, S, S+U);
   }
 
   method Dislodge(ghost S: set<Composite>)
@@ -97,7 +97,7 @@ class Composite {
         p.right := null;
       }
       var delta := -sum;
-      call p.Adjust(delta, S - {this}, S);
+      p.Adjust(delta, S - {this}, S);
     }
   }
 
@@ -138,35 +138,35 @@ method Main()
   var c0 := new Composite.Init(57);
 
   var c1 := new Composite.Init(12);
-  call c0.Add({c0}, c1, {c1});
+  c0.Add({c0}, c1, {c1});
 
   var c2 := new Composite.Init(48);
 
   var c3 := new Composite.Init(48);
-  call c2.Add({c2}, c3, {c3});
-  call c0.Add({c0,c1}, c2, {c2,c3});
+  c2.Add({c2}, c3, {c3});
+  c0.Add({c0,c1}, c2, {c2,c3});
 
   ghost var S := {c0, c1, c2, c3};
-  call c1.Update(100, S);
-  call c2.Update(102, S);
+  c1.Update(100, S);
+  c2.Update(102, S);
 
-  call c2.Dislodge(S);
-  call c2.Update(496, S);
-  call c0.Update(0, S);
+  c2.Dislodge(S);
+  c2.Update(496, S);
+  c0.Update(0, S);
 }
 
 method Harness() {
   var a := new Composite.Init(5);
   var b := new Composite.Init(7);
-  call a.Add({a}, b, {b});
+  a.Add({a}, b, {b});
   assert a.sum == 12;
 
-  call b.Update(17, {a,b});
+  b.Update(17, {a,b});
   assert a.sum == 22;
 
   var c := new Composite.Init(10);
-  call b.Add({a,b}, c, {c});
-  call b.Dislodge({a,b,c});
+  b.Add({a,b}, c, {c});
+  b.Dislodge({a,b,c});
   assert b.sum == 27;
 }
 
diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy
index 2c217264..989ddfc6 100644
--- a/Test/vacid0/SparseArray.dfy
+++ b/Test/vacid0/SparseArray.dfy
@@ -37,11 +37,9 @@ class SparseArray<T> {
     ensures |Contents| == N && this.zero == zero;
     ensures (forall x :: x in Contents ==> x == zero);
   {
-    var aa;
-    var ii;
-    call aa := AllocateArray(N);  this.a := aa;
-    call ii := AllocateArray(N);  this.b := ii;
-    call ii := AllocateArray(N);  this.c := ii;
+    var aa := AllocateArray(N);  this.a := aa;
+    var bb := AllocateArray(N);  this.b := bb;
+    bb := AllocateArray(N);  this.c := bb;
     this.n := 0;
 
     // initialize ghost variable Contents to a sequence of length N containing only zero's,
-- 
cgit v1.2.3