From d2cd087ebd9ff568c1712254eab864aeb4205e02 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 26 Oct 2011 21:20:44 -0700
Subject: Dafny: removed Dafny's "foreach" statements (replaced by the new
 "parallel" statement)

---
 Source/Dafny/Compiler.cs   |  59 ------
 Source/Dafny/Dafny.atg     |  32 +--
 Source/Dafny/DafnyAst.cs   |  34 ---
 Source/Dafny/Parser.cs     | 500 ++++++++++++++++++++-------------------------
 Source/Dafny/Printer.cs    |  21 --
 Source/Dafny/Resolver.cs   |  59 ------
 Source/Dafny/Scanner.cs    | 201 +++++++++---------
 Source/Dafny/Translator.cs | 126 ------------
 8 files changed, 328 insertions(+), 704 deletions(-)

(limited to 'Source')

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 52a4578c..9938d30a 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -690,12 +690,6 @@ namespace Microsoft.Dafny {
             CheckHasNoAssumes(s);
           }
         }
-      } else if (stmt is ForeachStmt) {
-        ForeachStmt s = (ForeachStmt)stmt;
-        foreach (PredicateStmt t in s.BodyPrefix) {
-          CheckHasNoAssumes(t);
-        }
-        CheckHasNoAssumes(s.GivenBody);
       } else if (stmt is ParallelStmt) {
         var s = (ParallelStmt)stmt;
         CheckHasNoAssumes(s.Body);
@@ -1031,59 +1025,6 @@ namespace Microsoft.Dafny {
         Indent(indent);
         wr.WriteLine("}");
 
-      } else if (stmt is ForeachStmt) {
-        ForeachStmt s = (ForeachStmt)stmt;
-        // List<Pair<TType,RhsType>> pendingUpdates = new List<Pair<TType,RhsType>>();
-        // foreach (TType x in S) {
-        //   if (Range(x)) {
-        //     assert/assume ...;
-        //     pendingUpdates.Add(new Pair(x,RHS));
-        //   }
-        // }
-        // foreach (Pair<TType,RhsType> p in pendingUpdates) {
-        //   p.Car.m = p.Cdr;
-        // }
-        string pu = "_pendingUpdates" + tmpVarCount;
-        string pr = "_pair" + tmpVarCount;
-        tmpVarCount++;
-        string TType = TypeName(s.BoundVar.Type);
-        string RhsType = TypeName(cce.NonNull(s.BodyAssign.Lhs.Type));
-
-        Indent(indent);
-        wr.WriteLine("List<Pair<{0},{1}>> {2} = new List<Pair<{0},{1}>>();", TType, RhsType, pu);
-
-        Indent(indent);
-        wr.Write("foreach ({0} @{1} in (", TType, s.BoundVar.Name);
-        TrExpr(s.Collection);
-        wr.WriteLine(").Elements) {");
-
-        Indent(indent + IndentAmount);
-        wr.Write("if (");
-        TrExpr(s.Range);
-        wr.WriteLine(") {");
-
-        foreach (PredicateStmt p in s.BodyPrefix) {
-          TrStmt(p, indent + 2*IndentAmount);
-        }
-        Indent(indent + 2*IndentAmount);
-        wr.Write("{0}.Add(new Pair<{1},{2}>(@{3}, ", pu, TType, RhsType, s.BoundVar.Name);
-        ExprRhs rhsExpr = s.BodyAssign.Rhs as ExprRhs;
-        if (rhsExpr != null) {
-          TrExpr(rhsExpr.Expr);
-        } else {
-          wr.Write(DefaultValue(s.BodyAssign.Lhs.Type));
-        }
-        wr.WriteLine("))");
-
-        Indent(indent + IndentAmount);  wr.WriteLine("}");
-        Indent(indent);  wr.WriteLine("}");
-
-        Indent(indent);  wr.WriteLine("foreach (Pair<{0},{1}> {2} in {3}) {{", TType, RhsType, pr, pu);
-        Indent(indent + IndentAmount);
-        FieldSelectExpr fse = (FieldSelectExpr)s.BodyAssign.Lhs;
-        wr.WriteLine("{0}.Car.{1} = {0}.Cdr;", pr, fse.FieldName);
-        Indent(indent);  wr.WriteLine("}");
-
       } else if (stmt is MatchStmt) {
         MatchStmt s = (MatchStmt)stmt;
         // Type source = e;
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 0092b4d9..9de1421b 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -631,7 +631,6 @@ OneStmt<out Statement/*!*/ s>
   | IfStmt<out s>
   | WhileStmt<out s>
   | MatchStmt<out s>
-  | ForeachStmt<out s>
   | ParallelStmt<out s>
   | "label"                            (. x = t; .)
     Ident<out id> ":"
@@ -886,36 +885,7 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
   (. c = new MatchCaseStmt(x, id.val, arguments, body); .)
   .
 /*------------------------------------------------------------------------*/
-ForeachStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
-     IToken/*!*/ x, boundVar;
-     Type/*!*/ ty;
-     Expression/*!*/ collection;
-     Expression/*!*/ range;
-     List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();
-     Statement bodyAssign = null;
-  .)
-  "foreach"                                    (. x = t;
-                                                  range = new LiteralExpr(x, true);
-                                                  ty = new InferredTypeProxy();
-                                               .)
-  "(" Ident<out boundVar>
-      [ ":" Type<out ty> ]
-      "in" Expression<out collection>
-      [ "|" Expression<out range> ]
-  ")"
-  "{"
-    { AssertStmt<out s>                        (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
-    | AssumeStmt<out s>                        (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
-    }
-    UpdateStmt<out s>                          (. bodyAssign = s; .)
-  "}"                                          (. if (bodyAssign != null) {
-                                                    s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
-                                                  } else {
-                                                    s = dummyStmt;  // some error occurred in parsing the bodyAssign
-                                                  }
-                                               .)
-  .
+
 AssertStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; .)
   "assert"                                     (. x = t; .)
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index d9d5c486..88862483 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1753,40 +1753,6 @@ namespace Microsoft.Dafny {
     }
   }
 
-  public class ForeachStmt : Statement
-  {
-    public readonly BoundVar/*!*/ BoundVar;
-    public readonly Expression/*!*/ Collection;
-    public readonly Expression/*!*/ Range;
-    public readonly List<PredicateStmt/*!*/>/*!*/ BodyPrefix;
-    public readonly Statement GivenBody;  // used only until resolution; afterwards, use BodyAssign
-    public AssignStmt/*!*/ BodyAssign;  // filled in during resolution
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(BoundVar != null);
-      Contract.Invariant(Collection != null);
-      Contract.Invariant(Range != null);
-      Contract.Invariant(cce.NonNullElements(BodyPrefix));
-      Contract.Invariant(GivenBody != null);
-    }
-
-    public ForeachStmt(IToken tok, BoundVar boundVar, Expression collection, Expression range,
-      List<PredicateStmt/*!*/>/*!*/ bodyPrefix, Statement givenBody)
-      : base(tok) {
-      Contract.Requires(tok != null);
-      Contract.Requires(boundVar != null);
-      Contract.Requires(collection != null);
-      Contract.Requires(range != null);
-      Contract.Requires(cce.NonNullElements(bodyPrefix));
-      Contract.Requires(givenBody != null);
-      this.BoundVar = boundVar;
-      this.Collection = collection;
-      this.Range = range;
-      this.BodyPrefix = bodyPrefix;
-      this.GivenBody = givenBody;
-    }
-  }
-
   public class ParallelStmt : Statement
   {
     public readonly List<BoundVar/*!*/> BoundVars;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 483217e5..57f4c46e 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -18,12 +18,12 @@ public class Parser {
 	public const int _digits = 2;
 	public const int _arrayToken = 3;
 	public const int _string = 4;
-	public const int maxT = 105;
+	public const int maxT = 104;
 
 	const bool T = true;
 	const bool x = false;
 	const int minErrDist = 2;
-	
+
 	public Scanner/*!*/ scanner;
 	public Errors/*!*/  errors;
 
@@ -134,10 +134,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (errDist >= minErrDist) errors.SemErr(t, msg);
 		errDist = 0;
 	}
-	
-    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
-      Contract.Requires(tok != null);
-      Contract.Requires(msg != null);
+
+	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+	  Contract.Requires(tok != null);
+	  Contract.Requires(msg != null);
 	  errors.SemErr(tok, msg);
 	}
 
@@ -150,15 +150,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			la = t;
 		}
 	}
-	
+
 	void Expect (int n) {
 		if (la.kind==n) Get(); else { SynErr(n); }
 	}
-	
+
 	bool StartOf (int s) {
 		return set[s, la.kind];
 	}
-	
+
 	void ExpectWeak (int n, int follow) {
 		if (la.kind == n) Get();
 		else {
@@ -182,7 +182,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}
 	}
 
-	
+
 	void Dafny() {
 		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
 		Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;
@@ -375,7 +375,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			mm.Add(m); 
 		} else if (la.kind == 20) {
 			CouplingInvDecl(mmod, mm);
-		} else SynErr(106);
+		} else SynErr(105);
 	}
 
 	void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -490,7 +490,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		} else if (la.kind == 10) {
 			Get();
 			isRefinement = true; 
-		} else SynErr(107);
+		} else SynErr(106);
 		if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
 		if (isConstructor) {
 		  if (mmod.IsGhost) {
@@ -728,7 +728,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			ReferenceType(out tok, out ty);
 			break;
 		}
-		default: SynErr(108); break;
+		default: SynErr(107); break;
 		}
 	}
 
@@ -779,12 +779,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Expression(out e);
 				Expect(17);
 				ens.Add(new MaybeFreeExpression(e, isFree)); 
-			} else SynErr(109);
+			} else SynErr(108);
 		} else if (la.kind == 32) {
 			Get();
 			DecreasesList(decreases, false);
 			Expect(17);
-		} else SynErr(110);
+		} else SynErr(109);
 	}
 
 	void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -874,7 +874,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				GenericInstantiation(gt);
 			}
 			ty = new UserDefinedType(tok, tok.val, gt); 
-		} else SynErr(111);
+		} else SynErr(110);
 	}
 
 	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
@@ -906,7 +906,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 			DecreasesList(decreases, false);
 			Expect(17);
-		} else SynErr(112);
+		} else SynErr(111);
 	}
 
 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -925,7 +925,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			fe = new FrameExpression(new WildcardExpr(t), null); 
 		} else if (StartOf(6)) {
 			FrameExpression(out fe);
-		} else SynErr(113);
+		} else SynErr(112);
 	}
 
 	void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -936,7 +936,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new WildcardExpr(t); 
 		} else if (StartOf(6)) {
 			Expression(out e);
-		} else SynErr(114);
+		} else SynErr(113);
 	}
 
 	void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -957,19 +957,19 @@ List<Expression/*!*/>/*!*/ decreases) {
 			BlockStmt(out s, out bodyStart, out bodyEnd);
 			break;
 		}
-		case 64: {
+		case 62: {
 			AssertStmt(out s);
 			break;
 		}
-		case 65: {
+		case 63: {
 			AssumeStmt(out s);
 			break;
 		}
-		case 66: {
+		case 64: {
 			PrintStmt(out s);
 			break;
 		}
-		case 1: case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {
+		case 1: case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
 			UpdateStmt(out s);
 			break;
 		}
@@ -989,11 +989,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			MatchStmt(out s);
 			break;
 		}
-		case 62: {
-			ForeachStmt(out s);
-			break;
-		}
-		case 67: {
+		case 65: {
 			ParallelStmt(out s);
 			break;
 		}
@@ -1017,7 +1013,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 					Get();
 					breakCount++; 
 				}
-			} else SynErr(115);
+			} else SynErr(114);
 			Expect(17);
 			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 
 			break;
@@ -1026,13 +1022,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 			ReturnStmt(out s);
 			break;
 		}
-		default: SynErr(116); break;
+		default: SynErr(115); break;
 		}
 	}
 
 	void AssertStmt(out Statement/*!*/ s) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; 
-		Expect(64);
+		Expect(62);
 		x = t; 
 		Expression(out e);
 		Expect(17);
@@ -1041,7 +1037,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 
 	void AssumeStmt(out Statement/*!*/ s) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; 
-		Expect(65);
+		Expect(63);
 		x = t; 
 		Expression(out e);
 		Expect(17);
@@ -1052,7 +1048,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(66);
+		Expect(64);
 		x = t; 
 		AttributeArg(out arg);
 		args.Add(arg); 
@@ -1097,7 +1093,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 22) {
 			Get();
 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 
-		} else SynErr(117);
+		} else SynErr(116);
 		s = new UpdateStmt(x, lhss, rhss); 
 	}
 
@@ -1170,13 +1166,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 				} else if (la.kind == 7) {
 					BlockStmt(out s, out bodyStart, out bodyEnd);
 					els = s; 
-				} else SynErr(118);
+				} else SynErr(117);
 			}
 			ifStmt = new IfStmt(x, guard, thn, els); 
 		} else if (la.kind == 7) {
 			AlternativeBlock(out alternatives);
 			ifStmt = new AlternativeStmt(x, alternatives); 
-		} else SynErr(119);
+		} else SynErr(118);
 	}
 
 	void WhileStmt(out Statement/*!*/ stmt) {
@@ -1202,7 +1198,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			LoopSpec(out invariants, out decreases, out mod);
 			AlternativeBlock(out alternatives);
 			stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); 
-		} else SynErr(120);
+		} else SynErr(119);
 	}
 
 	void MatchStmt(out Statement/*!*/ s) {
@@ -1221,54 +1217,6 @@ List<Expression/*!*/>/*!*/ decreases) {
 		s = new MatchStmt(x, e, cases); 
 	}
 
-	void ForeachStmt(out Statement/*!*/ s) {
-		Contract.Ensures(Contract.ValueAtReturn(out s) != null);
-		IToken/*!*/ x, boundVar;
-		Type/*!*/ ty;
-		Expression/*!*/ collection;
-		Expression/*!*/ range;
-		List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();
-		Statement bodyAssign = null;
-		
-		Expect(62);
-		x = t;
-		range = new LiteralExpr(x, true);
-		ty = new InferredTypeProxy();
-		
-		Expect(33);
-		Ident(out boundVar);
-		if (la.kind == 22) {
-			Get();
-			Type(out ty);
-		}
-		Expect(63);
-		Expression(out collection);
-		if (la.kind == 16) {
-			Get();
-			Expression(out range);
-		}
-		Expect(34);
-		Expect(7);
-		while (la.kind == 64 || la.kind == 65) {
-			if (la.kind == 64) {
-				AssertStmt(out s);
-				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 
-			} else {
-				AssumeStmt(out s);
-				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 
-			}
-		}
-		UpdateStmt(out s);
-		bodyAssign = s; 
-		Expect(8);
-		if (bodyAssign != null) {
-		 s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
-		} else {
-		  s = dummyStmt;  // some error occurred in parsing the bodyAssign
-		}
-		
-	}
-
 	void ParallelStmt(out Statement/*!*/ s) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);
 		IToken/*!*/ x;
@@ -1281,7 +1229,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Statement/*!*/ block;
 		IToken bodyStart, bodyEnd;
 		
-		Expect(67);
+		Expect(65);
 		x = t; 
 		Expect(33);
 		QuantifierDomain(out bvars, out attrs, out range);
@@ -1371,7 +1319,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(6)) {
 			Expression(out e);
 			r = new ExprRhs(e); 
-		} else SynErr(121);
+		} else SynErr(120);
 	}
 
 	void Lhs(out Expression e) {
@@ -1388,7 +1336,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			while (la.kind == 51 || la.kind == 53) {
 				Suffix(ref e);
 			}
-		} else SynErr(122);
+		} else SynErr(121);
 	}
 
 	void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1411,7 +1359,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(6)) {
 			Expression(out ee);
 			e = ee; 
-		} else SynErr(123);
+		} else SynErr(122);
 		Expect(34);
 	}
 
@@ -1510,7 +1458,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(6)) {
 			Expression(out e);
 			arg = new Attributes.Argument(t, e); 
-		} else SynErr(124);
+		} else SynErr(123);
 	}
 
 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1538,7 +1486,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	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 == 66 || la.kind == 67) {
 			EquivOp();
 			x = t; 
 			ImpliesExpression(out e1);
@@ -1549,7 +1497,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 == 68 || la.kind == 69) {
 			ImpliesOp();
 			x = t; 
 			ImpliesExpression(out e1);
@@ -1558,23 +1506,23 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}
 
 	void EquivOp() {
-		if (la.kind == 68) {
+		if (la.kind == 66) {
 			Get();
-		} else if (la.kind == 69) {
+		} else if (la.kind == 67) {
 			Get();
-		} else SynErr(125);
+		} else SynErr(124);
 	}
 
 	void LogicalExpression(out Expression/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 
 		RelationalExpression(out e0);
 		if (StartOf(13)) {
-			if (la.kind == 72 || la.kind == 73) {
+			if (la.kind == 70 || la.kind == 71) {
 				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 == 70 || la.kind == 71) {
 					AndOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1585,7 +1533,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 == 72 || la.kind == 73) {
 					OrOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1596,11 +1544,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}
 
 	void ImpliesOp() {
-		if (la.kind == 70) {
+		if (la.kind == 68) {
 			Get();
-		} else if (la.kind == 71) {
+		} else if (la.kind == 69) {
 			Get();
-		} else SynErr(126);
+		} else SynErr(125);
 	}
 
 	void RelationalExpression(out Expression/*!*/ e) {
@@ -1694,25 +1642,25 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}
 
 	void AndOp() {
-		if (la.kind == 72) {
+		if (la.kind == 70) {
 			Get();
-		} else if (la.kind == 73) {
+		} else if (la.kind == 71) {
 			Get();
-		} else SynErr(127);
+		} else SynErr(126);
 	}
 
 	void OrOp() {
-		if (la.kind == 74) {
+		if (la.kind == 72) {
 			Get();
-		} else if (la.kind == 75) {
+		} else if (la.kind == 73) {
 			Get();
-		} else SynErr(128);
+		} else SynErr(127);
 	}
 
 	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); 
@@ -1725,7 +1673,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		IToken y;
 		
 		switch (la.kind) {
-		case 76: {
+		case 74: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Eq; 
 			break;
@@ -1740,35 +1688,35 @@ List<Expression/*!*/>/*!*/ decreases) {
 			x = t;  op = BinaryExpr.Opcode.Gt; 
 			break;
 		}
-		case 77: {
+		case 75: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Le; 
 			break;
 		}
-		case 78: {
+		case 76: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		case 79: {
+		case 77: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Neq; 
 			break;
 		}
-		case 80: {
+		case 78: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Disjoint; 
 			break;
 		}
-		case 63: {
+		case 79: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.In; 
 			break;
 		}
-		case 81: {
+		case 80: {
 			Get();
 			x = t;  y = Token.NoToken; 
-			if (la.kind == 63) {
+			if (la.kind == 79) {
 				Get();
 				y = t; 
 			}
@@ -1783,29 +1731,29 @@ List<Expression/*!*/>/*!*/ decreases) {
 			
 			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(129); break;
+		default: SynErr(128); 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 == 44 || la.kind == 87 || la.kind == 88) {
+		while (la.kind == 44 || la.kind == 86 || la.kind == 87) {
 			MulOp(out x, out op);
 			UnaryExpression(out e1);
 			e0 = new BinaryExpr(x, op, e0, e1); 
@@ -1814,33 +1762,33 @@ 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(130);
+		} else SynErr(129);
 	}
 
 	void UnaryExpression(out Expression/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; 
 		switch (la.kind) {
-		case 86: {
+		case 85: {
 			Get();
 			x = t; 
 			UnaryExpression(out e);
 			e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); 
 			break;
 		}
-		case 81: case 89: {
+		case 80: case 88: {
 			NegOp();
 			x = t; 
 			UnaryExpression(out e);
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 
 			break;
 		}
-		case 38: case 55: case 61: case 99: case 100: case 101: case 102: {
+		case 38: case 55: case 61: case 98: case 99: case 100: case 101: {
 			EndlessExpression(out e);
 			break;
 		}
@@ -1859,14 +1807,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 			MultiSetExpr(out e);
 			break;
 		}
-		case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {
+		case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
 			ConstAtomExpression(out e);
 			while (la.kind == 51 || la.kind == 53) {
 				Suffix(ref e);
 			}
 			break;
 		}
-		default: SynErr(131); break;
+		default: SynErr(130); break;
 		}
 	}
 
@@ -1875,21 +1823,21 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 44) {
 			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(132);
+		} else SynErr(131);
 	}
 
 	void NegOp() {
-		if (la.kind == 81) {
+		if (la.kind == 80) {
 			Get();
-		} else if (la.kind == 89) {
+		} else if (la.kind == 88) {
 			Get();
-		} else SynErr(133);
+		} else SynErr(132);
 	}
 
 	void EndlessExpression(out Expression e) {
@@ -1901,7 +1849,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 			x = t; 
 			Expression(out e);
-			Expect(97);
+			Expect(96);
 			Expression(out e0);
 			Expect(56);
 			Expression(out e1);
@@ -1912,7 +1860,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			QuantifierGuts(out e);
 		} else if (la.kind == 38) {
 			ComprehensionExpr(out e);
-		} else SynErr(134);
+		} else SynErr(133);
 	}
 
 	void DottedIdentifiersAndFunction(out Expression e) {
@@ -1963,7 +1911,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (StartOf(6)) {
 				Expression(out ee);
 				e0 = ee; 
-				if (la.kind == 98) {
+				if (la.kind == 97) {
 					Get();
 					anyDots = true; 
 					if (StartOf(6)) {
@@ -1985,15 +1933,15 @@ List<Expression/*!*/>/*!*/ decreases) {
 						multipleIndices.Add(ee);
 						
 					}
-				} else SynErr(135);
-			} else if (la.kind == 98) {
+				} else SynErr(134);
+			} else if (la.kind == 97) {
 				Get();
 				anyDots = true; 
 				if (StartOf(6)) {
 					Expression(out ee);
 					e1 = ee; 
 				}
-			} else SynErr(136);
+			} else SynErr(135);
 			if (multipleIndices != null) {
 			 e = new MultiSelectExpr(x, e, multipleIndices);
 			 // make sure an array class with this dimensionality exists
@@ -2017,7 +1965,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}
 			
 			Expect(52);
-		} else SynErr(137);
+		} else SynErr(136);
 	}
 
 	void DisplayExpr(out Expression e) {
@@ -2041,7 +1989,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}
 			e = new SeqDisplayExpr(x, elements); 
 			Expect(52);
-		} else SynErr(138);
+		} else SynErr(137);
 	}
 
 	void MultiSetExpr(out Expression e) {
@@ -2067,7 +2015,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(34);
 		} else if (StartOf(16)) {
 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 
-		} else SynErr(139);
+		} else SynErr(138);
 	}
 
 	void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2076,17 +2024,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 		e = dummyExpr;
 		
 		switch (la.kind) {
-		case 90: {
+		case 89: {
 			Get();
 			e = new LiteralExpr(t, false); 
 			break;
 		}
-		case 91: {
+		case 90: {
 			Get();
 			e = new LiteralExpr(t, true); 
 			break;
 		}
-		case 92: {
+		case 91: {
 			Get();
 			e = new LiteralExpr(t); 
 			break;
@@ -2096,12 +2044,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new LiteralExpr(t, n); 
 			break;
 		}
-		case 93: {
+		case 92: {
 			Get();
 			e = new ThisExpr(t); 
 			break;
 		}
-		case 94: {
+		case 93: {
 			Get();
 			x = t; 
 			Expect(33);
@@ -2110,7 +2058,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new FreshExpr(x, e); 
 			break;
 		}
-		case 95: {
+		case 94: {
 			Get();
 			x = t; 
 			Expect(33);
@@ -2119,7 +2067,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new AllocatedExpr(x, e); 
 			break;
 		}
-		case 96: {
+		case 95: {
 			Get();
 			x = t; 
 			Expect(33);
@@ -2144,7 +2092,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(34);
 			break;
 		}
-		default: SynErr(140); break;
+		default: SynErr(139); break;
 		}
 	}
 
@@ -2181,13 +2129,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expression range;
 		Expression/*!*/ body;
 		
-		if (la.kind == 99 || la.kind == 100) {
+		if (la.kind == 98 || la.kind == 99) {
 			Forall();
 			x = t;  univ = true; 
-		} else if (la.kind == 101 || la.kind == 102) {
+		} else if (la.kind == 100 || la.kind == 101) {
 			Exists();
 			x = t; 
-		} else SynErr(141);
+		} else SynErr(140);
 		QuantifierDomain(out bvars, out attrs, out range);
 		QSep();
 		Expression(out body);
@@ -2218,7 +2166,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		}
 		Expect(16);
 		Expression(out range);
-		if (la.kind == 103 || la.kind == 104) {
+		if (la.kind == 102 || la.kind == 103) {
 			QSep();
 			Expression(out body);
 		}
@@ -2253,27 +2201,27 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}
 
 	void Forall() {
-		if (la.kind == 99) {
+		if (la.kind == 98) {
 			Get();
-		} else if (la.kind == 100) {
+		} else if (la.kind == 99) {
 			Get();
-		} else SynErr(142);
+		} else SynErr(141);
 	}
 
 	void Exists() {
-		if (la.kind == 101) {
+		if (la.kind == 100) {
 			Get();
-		} else if (la.kind == 102) {
+		} else if (la.kind == 101) {
 			Get();
-		} else SynErr(143);
+		} else SynErr(142);
 	}
 
 	void QSep() {
-		if (la.kind == 103) {
+		if (la.kind == 102) {
 			Get();
-		} else if (la.kind == 104) {
+		} else if (la.kind == 103) {
 			Get();
-		} else SynErr(144);
+		} else SynErr(143);
 	}
 
 	void AttributeBody(ref Attributes attrs) {
@@ -2300,32 +2248,32 @@ List<Expression/*!*/>/*!*/ decreases) {
 
 	public void Parse() {
 		la = new Token();
-		la.val = "";		
+		la.val = "";
 		Get();
 		Dafny();
 
-    Expect(0);
+		Expect(0);
 	}
-	
+
 	static readonly bool[,]/*!*/ set = {
-		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
-		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
-		{x,x,x,x, 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,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,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,T,T,x, x,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
-		{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,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,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,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,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
-		{x,x,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,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, 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,T,T,x, x,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, 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,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
-		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T, T,x,x,x, x,x,x,x, T,T,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,T,T,x, x,x,x,T, T,x,x},
-		{x,T,T,x, T,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}
+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+		{x,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,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,T,T,x, x,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+		{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,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,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
+		{x,T,T,x, x,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+		{x,x,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,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+		{x,T,T,x, x,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,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, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T, T,x,x,x, x,x,x,x, T,T,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},
+		{x,T,T,x, T,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
 
 	};
 } // end Parser
@@ -2334,18 +2282,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 public class Errors {
 	public int count = 0;                                    // number of errors detected
 	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream
-  public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
-  public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-  
+	public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+	public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
 	public void SynErr(string filename, int line, int col, int n) {
-    SynErr(filename, line, col, GetSyntaxErrorString(n));
-  }
-	public virtual void SynErr(string filename, int line, int col, string msg) {
-	  Contract.Requires(msg != null);
+		SynErr(filename, line, col, GetSyntaxErrorString(n));
+	}
+
+	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
+		Contract.Requires(msg != null);
 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
 		count++;
-  }
-  string GetSyntaxErrorString(int n) {
+	}
+
+	string GetSyntaxErrorString(int n) {
 		string s;
 		switch (n) {
 			case 0: s = "EOF expected"; break;
@@ -2410,93 +2360,92 @@ public class Errors {
 			case 59: s = "\"while\" expected"; break;
 			case 60: s = "\"invariant\" expected"; break;
 			case 61: s = "\"match\" 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 = "\"print\" expected"; break;
-			case 67: s = "\"parallel\" 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 = "\"!\" 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 = "\"\\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 ClassMemberDecl"; break;
-			case 107: s = "invalid MethodDecl"; break;
-			case 108: s = "invalid TypeAndToken"; break;
+			case 62: s = "\"assert\" expected"; break;
+			case 63: s = "\"assume\" expected"; break;
+			case 64: s = "\"print\" expected"; break;
+			case 65: s = "\"parallel\" expected"; break;
+			case 66: s = "\"<==>\" expected"; break;
+			case 67: s = "\"\\u21d4\" expected"; break;
+			case 68: s = "\"==>\" expected"; break;
+			case 69: s = "\"\\u21d2\" expected"; break;
+			case 70: s = "\"&&\" expected"; break;
+			case 71: s = "\"\\u2227\" expected"; break;
+			case 72: s = "\"||\" expected"; break;
+			case 73: s = "\"\\u2228\" expected"; break;
+			case 74: s = "\"==\" 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 = "\"in\" expected"; break;
+			case 80: s = "\"!\" 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 = "\"\\u00ac\" expected"; break;
+			case 89: s = "\"false\" expected"; break;
+			case 90: s = "\"true\" expected"; break;
+			case 91: s = "\"null\" expected"; break;
+			case 92: s = "\"this\" expected"; break;
+			case 93: s = "\"fresh\" expected"; break;
+			case 94: s = "\"allocated\" expected"; break;
+			case 95: s = "\"old\" expected"; break;
+			case 96: s = "\"then\" expected"; break;
+			case 97: s = "\"..\" expected"; break;
+			case 98: s = "\"forall\" expected"; break;
+			case 99: s = "\"\\u2200\" expected"; break;
+			case 100: s = "\"exists\" expected"; break;
+			case 101: s = "\"\\u2203\" expected"; break;
+			case 102: s = "\"::\" expected"; break;
+			case 103: s = "\"\\u2022\" expected"; break;
+			case 104: s = "??? expected"; break;
+			case 105: s = "invalid ClassMemberDecl"; break;
+			case 106: s = "invalid MethodDecl"; break;
+			case 107: s = "invalid TypeAndToken"; break;
+			case 108: s = "invalid MethodSpec"; break;
 			case 109: s = "invalid MethodSpec"; break;
-			case 110: s = "invalid MethodSpec"; break;
-			case 111: s = "invalid ReferenceType"; break;
-			case 112: s = "invalid FunctionSpec"; break;
-			case 113: s = "invalid PossiblyWildFrameExpression"; break;
-			case 114: s = "invalid PossiblyWildExpression"; break;
+			case 110: s = "invalid ReferenceType"; break;
+			case 111: s = "invalid FunctionSpec"; break;
+			case 112: s = "invalid PossiblyWildFrameExpression"; break;
+			case 113: s = "invalid PossiblyWildExpression"; break;
+			case 114: s = "invalid OneStmt"; break;
 			case 115: s = "invalid OneStmt"; break;
-			case 116: s = "invalid OneStmt"; break;
-			case 117: s = "invalid UpdateStmt"; break;
+			case 116: s = "invalid UpdateStmt"; break;
+			case 117: s = "invalid IfStmt"; break;
 			case 118: s = "invalid IfStmt"; break;
-			case 119: s = "invalid IfStmt"; break;
-			case 120: s = "invalid WhileStmt"; break;
-			case 121: s = "invalid Rhs"; break;
-			case 122: s = "invalid Lhs"; break;
-			case 123: s = "invalid Guard"; break;
-			case 124: s = "invalid AttributeArg"; break;
-			case 125: s = "invalid EquivOp"; break;
-			case 126: s = "invalid ImpliesOp"; break;
-			case 127: s = "invalid AndOp"; break;
-			case 128: s = "invalid OrOp"; break;
-			case 129: s = "invalid RelOp"; break;
-			case 130: s = "invalid AddOp"; break;
-			case 131: s = "invalid UnaryExpression"; break;
-			case 132: s = "invalid MulOp"; break;
-			case 133: s = "invalid NegOp"; break;
-			case 134: s = "invalid EndlessExpression"; break;
+			case 119: s = "invalid WhileStmt"; break;
+			case 120: s = "invalid Rhs"; break;
+			case 121: s = "invalid Lhs"; break;
+			case 122: s = "invalid Guard"; break;
+			case 123: s = "invalid AttributeArg"; break;
+			case 124: s = "invalid EquivOp"; break;
+			case 125: s = "invalid ImpliesOp"; break;
+			case 126: s = "invalid AndOp"; break;
+			case 127: s = "invalid OrOp"; break;
+			case 128: s = "invalid RelOp"; break;
+			case 129: s = "invalid AddOp"; break;
+			case 130: s = "invalid UnaryExpression"; break;
+			case 131: s = "invalid MulOp"; break;
+			case 132: s = "invalid NegOp"; break;
+			case 133: s = "invalid EndlessExpression"; break;
+			case 134: s = "invalid Suffix"; break;
 			case 135: s = "invalid Suffix"; break;
 			case 136: s = "invalid Suffix"; break;
-			case 137: s = "invalid Suffix"; break;
-			case 138: s = "invalid DisplayExpr"; break;
-			case 139: s = "invalid MultiSetExpr"; break;
-			case 140: s = "invalid ConstAtomExpression"; break;
-			case 141: s = "invalid QuantifierGuts"; break;
-			case 142: s = "invalid Forall"; break;
-			case 143: s = "invalid Exists"; break;
-			case 144: s = "invalid QSep"; break;
+			case 137: s = "invalid DisplayExpr"; break;
+			case 138: s = "invalid MultiSetExpr"; break;
+			case 139: s = "invalid ConstAtomExpression"; break;
+			case 140: s = "invalid QuantifierGuts"; break;
+			case 141: s = "invalid Forall"; break;
+			case 142: s = "invalid Exists"; break;
+			case 143: s = "invalid QSep"; break;
 
 			default: s = "error " + n; break;
 		}
-    return s;
+		return s;
 	}
 
 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors
@@ -2504,8 +2453,9 @@ public class Errors {
 		Contract.Requires(msg != null);
 		SemErr(tok.filename, tok.line, tok.col, msg);
 	}
+
 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
-	  Contract.Requires(msg != null);
+		Contract.Requires(msg != null);
 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
 		count++;
 	}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index f9f1eca0..7f7ba963 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -541,27 +541,6 @@ namespace Microsoft.Dafny {
         Indent(indent);
         wr.Write("}");
 
-      } else if (stmt is ForeachStmt) {
-        ForeachStmt s = (ForeachStmt)stmt;
-        wr.Write("foreach ({0} in ", s.BoundVar.Name);
-        PrintExpression(s.Collection);
-        if (!LiteralExpr.IsTrue(s.Range)) {
-          wr.Write(" | ");
-          PrintExpression(s.Range);
-        }
-        wr.WriteLine(") {");
-        int ind = indent + IndentAmount;
-        foreach (PredicateStmt t in s.BodyPrefix) {
-          Indent(ind);
-          PrintStatement(t, ind);
-          wr.WriteLine();
-        }
-        Indent(ind);
-        PrintStatement(s.GivenBody, ind);
-        wr.WriteLine();
-        Indent(indent);
-        wr.Write("}");
-
       } else if (stmt is ParallelStmt) {
         var s = (ParallelStmt)stmt;
         wr.Write("parallel (");
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index e053f212..a3668619 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1474,62 +1474,6 @@ namespace Microsoft.Dafny {
           // any type is fine
         }
 
-      } else if (stmt is ForeachStmt) {
-        ForeachStmt s = (ForeachStmt)stmt;
-
-        ResolveExpression(s.Collection, true);
-        Contract.Assert(s.Collection.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(s.Collection.Type, new CollectionTypeProxy(s.BoundVar.Type))) {
-          Error(s.Collection, "The type is expected to be a collection of {0} (instead got {1})", s.BoundVar.Type, s.Collection.Type);
-        }
-
-        scope.PushMarker();
-        bool b = scope.Push(s.BoundVar.Name, s.BoundVar);
-        Contract.Assert(b);  // since we just pushed a marker, we expect the Push to succeed
-        ResolveType(s.BoundVar.tok, s.BoundVar.Type);
-        int prevErrorCount = ErrorCount;
-
-        ResolveExpression(s.Range, true);
-        Contract.Assert(s.Range.Type != null);  // follows from postcondition of ResolveExpression
-        if (!UnifyTypes(s.Range.Type, Type.Bool)) {
-          Error(s.Range, "range condition is expected to be of type {0}, but is {1}", Type.Bool, s.Range.Type);
-        }
-        bool successfullyResolvedCollectionAndRange = ErrorCount == prevErrorCount;
-
-        foreach (PredicateStmt ss in s.BodyPrefix) {
-          ResolveStatement(ss, specContextOnly, method);
-        }
-
-        bool specOnly = specContextOnly ||
-                        (successfullyResolvedCollectionAndRange && (UsesSpecFeatures(s.Collection) || UsesSpecFeatures(s.Range)));
-        s.IsGhost = specOnly;
-        ResolveStatement(s.GivenBody, specOnly, method);
-        // check for correct usage of BoundVar in LHS and RHS of this assignment
-        if (s.GivenBody is AssignStmt) {
-          s.BodyAssign = (AssignStmt)s.GivenBody;
-        } else if (s.GivenBody is ConcreteSyntaxStatement) {
-          var css = (ConcreteSyntaxStatement)s.GivenBody;
-          if (css.ResolvedStatements.Count == 1 && css.ResolvedStatements[0] is AssignStmt) {
-            s.BodyAssign = (AssignStmt)css.ResolvedStatements[0];
-          }
-        }
-        if (s.BodyAssign == null) {
-          Error(s, "update statement inside foreach must be a single assignment statement");
-        } else {
-          FieldSelectExpr lhs = s.BodyAssign.Lhs as FieldSelectExpr;
-          IdentifierExpr obj = lhs == null ? null : lhs.Obj as IdentifierExpr;
-          if (obj == null || obj.Var != s.BoundVar) {
-            Error(s, "assignment inside foreach must assign to a field of the bound variable of the foreach statement");
-          } else {
-            var rhs = s.BodyAssign.Rhs as ExprRhs;
-            if (rhs != null && rhs.Expr is UnaryExpr && ((UnaryExpr)rhs.Expr).Op == UnaryExpr.Opcode.SetChoose) {
-              Error(s, "foreach statement does not support 'choose' statements");
-            }
-          }
-        }
-
-        scope.PopMarker();
-
       } else if (stmt is ParallelStmt) {
         var s = (ParallelStmt)stmt;
 
@@ -2151,9 +2095,6 @@ namespace Microsoft.Dafny {
           }
         }
 
-      } else if (stmt is ForeachStmt) {
-        Error(stmt, "foreach statement not allowed in body of parallel statement");
-
       } else if (stmt is ParallelStmt) {
         var s = (ParallelStmt)stmt;
         switch (s.Kind) {
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index ae887c47..634abf45 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
 	//    a) whole stream in buffer
 	//    b) part of stream in buffer
 	// 2) non seekable stream (network, console)
-  
+
 	public const int EOF = 65535 + 1; // char.MaxValue + 1;
 	const int MIN_BUFFER_LENGTH = 1024; // 1KB
 	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,15 +31,17 @@ public class Buffer {
 	Stream/*!*/ stream;      // input stream (seekable)
 	bool isUserStream;  // was the stream opened by the user?
 
-[ContractInvariantMethod]
-void ObjectInvariant(){
-  Contract.Invariant(buf != null);
-  Contract.Invariant(stream != null);}
-    [NotDelayed]
-	public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
+	[ContractInvariantMethod]
+	void ObjectInvariant(){
+		Contract.Invariant(buf != null);
+		Contract.Invariant(stream != null);
+	}
+
+//  [NotDelayed]
+	public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
 	  Contract.Requires(s != null);
 		stream = s; this.isUserStream = isUserStream;
-		
+
 		int fl, bl;
 		if (s.CanSeek) {
 			fl = (int) s.Length;
@@ -51,12 +53,12 @@ void ObjectInvariant(){
 
 		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
 		fileLen = fl;  bufLen = bl;
-		
+
 		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
 		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
 		if (bufLen == fileLen && s.CanSeek) Close();
 	}
-	
+
 	protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
 	  Contract.Requires(b != null);
 		buf = b.buf;
@@ -73,14 +75,14 @@ void ObjectInvariant(){
 	}
 
 	~Buffer() { Close(); }
-	
+
 	protected void Close() {
 		if (!isUserStream && stream != null) {
 			stream.Close();
 			//stream = null;
 		}
 	}
-	
+
 	public virtual int Read () {
 		if (bufPos < bufLen) {
 			return buf[bufPos++];
@@ -100,7 +102,7 @@ void ObjectInvariant(){
 		Pos = curPos;
 		return ch;
 	}
-	
+
 	public string/*!*/ GetString (int beg, int end) {
 	  Contract.Ensures(Contract.Result<string>() != null);
 		int len = 0;
@@ -139,7 +141,7 @@ void ObjectInvariant(){
 			}
 		}
 	}
-	
+
 	// Read the next chunk of bytes from the stream, increases the buffer
 	// if needed and updates the fields fileLen and bufLen.
 	// Returns the number of bytes read.
@@ -209,23 +211,24 @@ public class UTF8Buffer: Buffer {
 public class Scanner {
 	const char EOL = '\n';
 	const int eofSym = 0; /* pdt */
-	const int maxT = 105;
-	const int noSym = 105;
-
-
-[ContractInvariantMethod]
-void objectInvariant(){
-  Contract.Invariant(buffer!=null);
-  Contract.Invariant(t != null);
-  Contract.Invariant(start != null);
-  Contract.Invariant(tokens != null);
-  Contract.Invariant(pt != null);
-  Contract.Invariant(tval != null);
-  Contract.Invariant(Filename != null);
-  Contract.Invariant(errorHandler != null);
-}
+	const int maxT = 104;
+	const int noSym = 104;
+
+
+	[ContractInvariantMethod]
+	void objectInvariant(){
+		Contract.Invariant(buffer!=null);
+		Contract.Invariant(t != null);
+		Contract.Invariant(start != null);
+		Contract.Invariant(tokens != null);
+		Contract.Invariant(pt != null);
+		Contract.Invariant(tval != null);
+		Contract.Invariant(Filename != null);
+		Contract.Invariant(errorHandler != null);
+	}
+
 	public Buffer/*!*/ buffer; // scanner buffer
-	
+
 	Token/*!*/ t;          // current token
 	int ch;           // current input character
 	int pos;          // byte position of current character
@@ -236,13 +239,13 @@ void objectInvariant(){
 
 	Token/*!*/ tokens;     // list of tokens already peeked (first token is a dummy)
 	Token/*!*/ pt;         // current peek token
-	
+
 	char[]/*!*/ tval = new char[128]; // text of current token
 	int tlen;         // length of current token
-	
+
 	private string/*!*/ Filename;
 	private Errors/*!*/ errorHandler;
-	
+
 	static Scanner() {
 		start = new Hashtable(128);
 		for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -290,9 +293,9 @@ void objectInvariant(){
 		start[Buffer.EOF] = -1;
 
 	}
-	
-	[NotDelayed]
-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
+
+//	[NotDelayed]
+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
 	  Contract.Requires(fileName != null);
 	  Contract.Requires(errorHandler != null);
 		this.errorHandler = errorHandler;
@@ -302,15 +305,14 @@ void objectInvariant(){
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
 			buffer = new Buffer(stream, false);
 			Filename = fileName;
-			
 			Init();
 		} catch (IOException) {
 			throw new FatalError("Cannot open file " + fileName);
 		}
 	}
-	
-	[NotDelayed]
-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
+
+//	[NotDelayed]
+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
 	  Contract.Requires(s != null);
 	  Contract.Requires(errorHandler != null);
 	  Contract.Requires(fileName != null);
@@ -319,10 +321,9 @@ void objectInvariant(){
 		buffer = new Buffer(s, true);
 		this.errorHandler = errorHandler;
 		this.Filename = fileName;
-		
 		Init();
 	}
-	
+
 	void Init() {
 		pos = -1; line = 1; col = 0;
 		oldEols = 0;
@@ -343,11 +344,11 @@ void objectInvariant(){
 	Contract.Ensures(Contract.Result<string>() != null);
 	  int p = buffer.Pos;
 	  int ch = buffer.Read();
-      // replace isolated '\r' by '\n' in order to make
+	  // replace isolated '\r' by '\n' in order to make
 	  // eol handling uniform across Windows, Unix and Mac
 	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
 	  while (ch != EOL && ch != Buffer.EOF){
-	    ch = buffer.Read();
+		ch = buffer.Read();
 		// replace isolated '\r' by '\n' in order to make
 		// eol handling uniform across Windows, Unix and Mac
 		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -358,7 +359,7 @@ void objectInvariant(){
 	}
 
 	void NextCh() {
-		if (oldEols > 0) { ch = EOL; oldEols--; } 
+		if (oldEols > 0) { ch = EOL; oldEols--; }
 		else {
 //			pos = buffer.Pos;
 //			ch = buffer.Read(); col++;
@@ -366,9 +367,9 @@ void objectInvariant(){
 //			// eol handling uniform across Windows, Unix and Mac
 //			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
 //			if (ch == EOL) { line++; col = 0; }
-			
+
 			while (true) {
-			    pos = buffer.Pos;
+				pos = buffer.Pos;
 				ch = buffer.Read(); col++;
 				// replace isolated '\r' by '\n' in order to make
 				// eol handling uniform across Windows, Unix and Mac
@@ -418,7 +419,7 @@ void objectInvariant(){
 				return;
 			  }
 
-			
+
 		}
 
 	}
@@ -525,22 +526,21 @@ void objectInvariant(){
 			case "while": t.kind = 59; break;
 			case "invariant": t.kind = 60; break;
 			case "match": 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 "print": t.kind = 66; break;
-			case "parallel": t.kind = 67; 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;
+			case "assert": t.kind = 62; break;
+			case "assume": t.kind = 63; break;
+			case "print": t.kind = 64; break;
+			case "parallel": t.kind = 65; break;
+			case "in": t.kind = 79; break;
+			case "false": t.kind = 89; break;
+			case "true": t.kind = 90; break;
+			case "null": t.kind = 91; break;
+			case "this": t.kind = 92; break;
+			case "fresh": t.kind = 93; break;
+			case "allocated": t.kind = 94; break;
+			case "old": t.kind = 95; break;
+			case "then": t.kind = 96; break;
+			case "forall": t.kind = 98; break;
+			case "exists": t.kind = 100; break;
 			default: break;
 		}
 	}
@@ -557,10 +557,13 @@ void objectInvariant(){
 		t.pos = pos; t.col = col; t.line = line;
 		t.filename = this.Filename;
 		int state;
-		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
+		if (start.ContainsKey(ch)) {
+			Contract.Assert(start[ch] != null);
+			state = (int) start[ch];
+		}
 		else { state = 0; }
 		tlen = 0; AddCh();
-		
+
 		switch (state) {
 			case -1: { t.kind = eofSym; break; } // NextCh already done
 			case 0: {
@@ -666,56 +669,56 @@ void objectInvariant(){
 				if (ch == '>') {AddCh(); goto case 30;}
 				else {goto case 0;}
 			case 30:
-				{t.kind = 68; break;}
+				{t.kind = 66; break;}
 			case 31:
-				{t.kind = 69; break;}
+				{t.kind = 67; break;}
 			case 32:
-				{t.kind = 70; break;}
+				{t.kind = 68; break;}
 			case 33:
-				{t.kind = 71; break;}
+				{t.kind = 69; break;}
 			case 34:
 				if (ch == '&') {AddCh(); goto case 35;}
 				else {goto case 0;}
 			case 35:
-				{t.kind = 72; break;}
+				{t.kind = 70; break;}
 			case 36:
-				{t.kind = 73; break;}
+				{t.kind = 71; break;}
 			case 37:
-				{t.kind = 74; break;}
+				{t.kind = 72; break;}
 			case 38:
-				{t.kind = 75; break;}
+				{t.kind = 73; break;}
 			case 39:
-				{t.kind = 78; break;}
+				{t.kind = 76; break;}
 			case 40:
-				{t.kind = 79; break;}
+				{t.kind = 77; break;}
 			case 41:
-				{t.kind = 80; break;}
+				{t.kind = 78; break;}
 			case 42:
-				{t.kind = 82; break;}
+				{t.kind = 81; break;}
 			case 43:
-				{t.kind = 83; break;}
+				{t.kind = 82; break;}
 			case 44:
-				{t.kind = 84; break;}
+				{t.kind = 83; break;}
 			case 45:
-				{t.kind = 85; break;}
+				{t.kind = 84; break;}
 			case 46:
-				{t.kind = 86; break;}
+				{t.kind = 85; break;}
 			case 47:
-				{t.kind = 87; break;}
+				{t.kind = 86; break;}
 			case 48:
-				{t.kind = 88; break;}
+				{t.kind = 87; break;}
 			case 49:
-				{t.kind = 89; break;}
+				{t.kind = 88; break;}
 			case 50:
-				{t.kind = 98; break;}
+				{t.kind = 97; break;}
 			case 51:
-				{t.kind = 100; break;}
+				{t.kind = 99; break;}
 			case 52:
-				{t.kind = 102; break;}
+				{t.kind = 101; break;}
 			case 53:
-				{t.kind = 103; break;}
+				{t.kind = 102; break;}
 			case 54:
-				{t.kind = 104; break;}
+				{t.kind = 103; break;}
 			case 55:
 				recEnd = pos; recKind = 15;
 				if (ch == '>') {AddCh(); goto case 28;}
@@ -743,31 +746,31 @@ void objectInvariant(){
 				if (ch == '.') {AddCh(); goto case 50;}
 				else {t.kind = 53; break;}
 			case 61:
-				recEnd = pos; recKind = 81;
+				recEnd = pos; recKind = 80;
 				if (ch == '=') {AddCh(); goto case 40;}
 				else if (ch == '!') {AddCh(); goto case 41;}
-				else {t.kind = 81; break;}
+				else {t.kind = 80; break;}
 			case 62:
-				recEnd = pos; recKind = 76;
+				recEnd = pos; recKind = 74;
 				if (ch == '>') {AddCh(); goto case 32;}
-				else {t.kind = 76; break;}
+				else {t.kind = 74; break;}
 			case 63:
-				recEnd = pos; recKind = 77;
+				recEnd = pos; recKind = 75;
 				if (ch == '=') {AddCh(); goto case 29;}
-				else {t.kind = 77; break;}
+				else {t.kind = 75; break;}
 
 		}
 		t.val = new String(tval, 0, tlen);
 		return t;
 	}
-	
+
 	private void SetScannerBehindT() {
 		buffer.Pos = t.pos;
 		NextCh();
 		line = t.line; col = t.col;
 		for (int i = 0; i < tlen; i++) NextCh();
 	}
-	
+
 	// get the next token (possibly a token already seen during peeking)
 	public Token/*!*/ Scan () {
 	 Contract.Ensures(Contract.Result<Token>() != null);
@@ -788,7 +791,7 @@ void objectInvariant(){
 			}
 			pt = pt.next;
 		} while (pt.kind > maxT); // skip pragmas
-	
+
 		return pt;
 	}
 
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 9e28a6ec..61f3dad3 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3190,132 +3190,6 @@ namespace Microsoft.Dafny {
           delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, e); },
           builder, locals, etran);
 
-      } else if (stmt is ForeachStmt) {
-        AddComment(builder, stmt, "foreach statement");
-        ForeachStmt s = (ForeachStmt)stmt;
-        // assert/assume (forall o: ref ::  o != null && o in S && Range(o) ==> Expr);
-        // assert (forall o: ref :: o != null && o in S && Range(o)  ==> IsTotal(RHS));
-        // assert (forall o: ref :: o != null && o in S && Range(o)  ==> $_Frame[o,F]);  // this checks the enclosing modifies clause
-        // var oldHeap := $Heap;
-        // havoc $Heap;
-        // assume $HeapSucc(oldHeap, $Heap);
-        // assume (forall<alpha> o: ref, f: Field alpha ::  $Heap[o,f] = oldHeap[o,f] || (f = F && o != null && o in S && Range(o)));
-        // assume (forall o: ref ::  o != null && o in S && Range(o) ==> $Heap[o,F] =  RHS[$Heap := oldHeap]);
-        // Note, $Heap[o,alloc] is intentionally omitted from the antecedent of the quantifier in the previous line.  That
-        // allocatedness property should hold automatically, because the set/seq quantified is a program expression, which
-        // will have been constructed from allocated objects.
-        // For sets, "o in S" means just that.  For sequences, "o in S" is:
-        //   (exists i :: { Seq#Index(S,i) }  0 <= i && i < Seq#Length(S) && Seq#Index(S,i) == o)
-
-        Bpl.BoundVariable oVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, s.BoundVar.UniqueName, TrType(s.BoundVar.Type)));
-        Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(stmt.Tok, oVar);
-
-        // colection
-        TrStmt_CheckWellformed(s.Collection, builder, locals, etran, true);
-        Bpl.Expr oInS;
-        if (s.Collection.Type is SetType) {
-          oInS = etran.TrInSet(stmt.Tok, o, s.Collection, ((SetType)s.Collection.Type).Arg);
-        } else if (s.Collection.Type is MultiSetType) {
-          // should not be reached.
-          Contract.Assert(false);
-          throw new cce.UnreachableException();
-        } else {
-          Bpl.BoundVariable iVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$i", Bpl.Type.Int));
-          Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(stmt.Tok, iVar);
-          Bpl.Expr S = etran.TrExpr(s.Collection);
-          Bpl.Expr range = InSeqRange(stmt.Tok, i, S, true, null, false);
-          Bpl.Expr Si = FunctionCall(stmt.Tok, BuiltinFunction.SeqIndex, predef.BoxType, S, i);
-          Bpl.Trigger tr = new Bpl.Trigger(stmt.Tok, true, new Bpl.ExprSeq(Si));
-          // TODO: in the next line, the == should be replaced by something that understands extensionality, for sets and sequences
-          var boxO = etran.BoxIfNecessary(stmt.Tok, o, ((SeqType)s.Collection.Type).Arg);
-          oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, boxO)));
-        }
-        oInS = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS);
-
-        // range
-        Bpl.Expr qr = new Bpl.ForallExpr(s.Range.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(s.Range, etran)));
-        builder.Add(AssertNS(s.Range.tok, qr, "range expression must be well defined"));
-        oInS = Bpl.Expr.And(oInS, etran.TrExpr(s.Range));
-
-        // sequence of asserts and assumes and uses
-        foreach (PredicateStmt ps in s.BodyPrefix) {
-          if (ps is AssertStmt || CommandLineOptions.Clo.DisallowSoundnessCheating) {
-            Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(ps.Expr, etran)));
-            builder.Add(AssertNS(ps.Expr.tok, q, "assert condition must be well defined"));  // totality check
-            bool splitHappened;
-            var ss = TrSplitExpr(ps.Expr, etran, out splitHappened);
-            if (!splitHappened) {
-              Bpl.Expr e = etran.TrExpr(ps.Expr);
-              q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));
-              builder.Add(Assert(ps.Expr.tok, q, "assertion violation"));
-            } else {
-              foreach (var split in ss) {
-                if (!split.IsFree) {
-                  q = new Bpl.ForallExpr(split.E.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, split.E));
-                  builder.Add(AssertNS(split.E.tok, q, "assertion violation"));
-                }
-              }
-              Bpl.Expr e = etran.TrExpr(ps.Expr);
-              q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));
-              builder.Add(new Bpl.AssumeCmd(ps.Expr.tok, q));
-            }
-          } else if (ps is AssumeStmt) {
-            Bpl.Expr eIsTotal = IsTotal(ps.Expr, etran);
-            Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, eIsTotal));
-            builder.Add(AssertNS(ps.Expr.tok, q, "assume condition must be well defined"));  // totality check
-          } else {
-            Contract.Assert(false);
-          }
-          Bpl.Expr enchilada = etran.TrExpr(ps.Expr);  // the whole enchilada
-          Bpl.Expr qEnchilada = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, enchilada));
-          builder.Add(new Bpl.AssumeCmd(ps.Expr.tok, qEnchilada));
-        }
-
-        // Check RHS of assignment to be well defined
-        ExprRhs rhsExpr = s.BodyAssign.Rhs as ExprRhs;
-        if (rhsExpr != null) {
-          // assert (forall o: ref :: o != null && o in S && Range(o) ==> IsTotal(RHS));
-          Bpl.Expr bbb = Bpl.Expr.Imp(oInS, IsTotal(rhsExpr.Expr, etran));
-          Bpl.Expr qqq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), bbb);
-          builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined"));  // totality check
-        }
-
-        // Here comes:  assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);
-        Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o, GetField((FieldSelectExpr)s.BodyAssign.Lhs)));
-        Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
-        builder.Add(Assert(s.BodyAssign.Tok, qq, "foreach assignment may update an object not in the enclosing method's modifies clause"));
-
-        // Set up prevHeap
-        Bpl.IdentifierExpr prevHeap = GetPrevHeapVar_IdExpr(stmt.Tok, locals);
-        builder.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, prevHeap, etran.HeapExpr));
-        builder.Add(new Bpl.HavocCmd(stmt.Tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
-        builder.Add(new Bpl.AssumeCmd(stmt.Tok, FunctionCall(stmt.Tok, BuiltinFunction.HeapSucc, null, prevHeap, etran.HeapExpr)));
-
-        // Here comes:  assume (forall<alpha> o: ref, f: Field alpha ::  $Heap[o,f] = oldHeap[o,f] || (f = F && o != null && o in S && Range(o)));
-        Bpl.TypeVariable alpha = new Bpl.TypeVariable(stmt.Tok, "alpha");
-        Bpl.BoundVariable fVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$f", predef.FieldName(stmt.Tok, alpha)));
-        Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(stmt.Tok, fVar);
-        Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(stmt.Tok, etran.HeapExpr, o, f);
-        Bpl.Expr oldHeapOF = ExpressionTranslator.ReadHeap(stmt.Tok, prevHeap, o, f);
-        body = Bpl.Expr.Or(
-          Bpl.Expr.Eq(heapOF, oldHeapOF),
-          Bpl.Expr.And(
-            Bpl.Expr.Eq(f, GetField((FieldSelectExpr)s.BodyAssign.Lhs)),
-            oInS));
-        qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), body);
-        builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
-
-        // Here comes:  assume (forall o: ref ::  o != null && o in S && Range(o) ==> $Heap[o,F] =  RHS[$Heap := oldHeap]);
-        if (rhsExpr != null) {
-          Bpl.Expr heapOField = ExpressionTranslator.ReadHeap(stmt.Tok, etran.HeapExpr, o, GetField((FieldSelectExpr)(s.BodyAssign).Lhs));
-          ExpressionTranslator oldEtran = new ExpressionTranslator(this, predef, prevHeap);
-          body = Bpl.Expr.Imp(oInS, Bpl.Expr.Eq(heapOField, oldEtran.TrExpr(rhsExpr.Expr)));
-          qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
-          builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
-        }
-
-        builder.Add(CaptureState(stmt.Tok));
-
       } else if (stmt is ParallelStmt) {
         AddComment(builder, stmt, "parallel statement");
         var s = (ParallelStmt)stmt;
-- 
cgit v1.2.3