Dafny: removed allocated, changed semantics of fresh

-allocated(x) removed, as really only useful in old(...)
-old(allocated(x)) and !fresh(x) are equivalent (for x with type ref, set, sequence, and datatype).

12 files changed, 297 insertions, 399 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index aecb6fe7..506df4c6 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -247,10 +247,6 @@ namespace Microsoft.Dafny
         var e = (FreshExpr)expr;

         return new FreshExpr(Tok(e.tok), CloneExpr(e.E));

 

-      } else if (expr is AllocatedExpr) {

-        var e = (AllocatedExpr)expr;

-        return new AllocatedExpr(Tok(e.tok), CloneExpr(e.E));

-

       } else if (expr is UnaryExpr) {

         var e = (UnaryExpr)expr;

         return new UnaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E));

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 52639f07..adbad177 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1423,8 +1423,6 @@ ConstAtomExpression<out Expression/*!*/ e>
   | "this"                                     (. e = new ThisExpr(t); .)

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

     "(" Expression<out e> ")"                  (. e = new FreshExpr(x, e); .)

-  | "allocated"                                (. x = t; .)

-    "(" Expression<out e> ")"                  (. e = new AllocatedExpr(x, e); .)

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

     "(" Expression<out e> ")"                  (. e = new OldExpr(x, e); .)

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

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index bf2c7492..a019f068 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3125,26 +3125,6 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class AllocatedExpr : Expression

-  {

-    public readonly Expression E;

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(E != null);

-    }

-

-    public AllocatedExpr(IToken tok, Expression expr)

-      : base(tok) {

-      Contract.Requires(tok != null);

-      Contract.Requires(expr != null);

-      E = expr;

-    }

-

-    public override IEnumerable<Expression> SubExpressions {

-      get { yield return E; }

-    }

-  }

-

   public class UnaryExpr : Expression

   {

     public enum Opcode {

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index ad2009c2..74848d52 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -21,7 +21,7 @@ public class Parser {
 	public const int _colon = 5;

 	public const int _lbrace = 6;

 	public const int _rbrace = 7;

-	public const int maxT = 109;

+	public const int maxT = 108;

 

 	const bool T = true;

 	const bool x = false;

@@ -212,7 +212,7 @@ bool IsAttribute() {
 				defaultModule.TopLevelDecls.Add(at); 

 			} else if (StartOf(2)) {

 				ClassMemberDecl(membersDefaultClass, isGhost, false);

-			} else SynErr(110);

+			} else SynErr(109);

 		}

 		DefaultClassDecl defaultClass = null;

 		foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

@@ -275,7 +275,7 @@ bool IsAttribute() {
 					module.TopLevelDecls.Add(at); 

 				} else if (StartOf(2)) {

 					ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false);

-				} else SynErr(111);

+				} else SynErr(110);

 			}

 			Expect(7);

 			module.BodyEndTok = t;

@@ -295,7 +295,7 @@ bool IsAttribute() {
 			}

 			Expect(12);

 			submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment); 

-		} else SynErr(112);

+		} else SynErr(111);

 	}

 

 	void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {

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

 		IToken bodyStart;

 		

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

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

 		Expect(15);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

@@ -338,13 +338,13 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;  // dummy assignment

 		bool co = false;

 		

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

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

 		if (la.kind == 17) {

 			Get();

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

 			Get();

 			co = true; 

-		} else SynErr(115);

+		} else SynErr(114);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

@@ -359,7 +359,7 @@ bool IsAttribute() {
 			Get();

 			DatatypeMemberDecl(ctors);

 		}

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

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

 		Expect(12);

 		if (co) {

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

@@ -388,7 +388,7 @@ bool IsAttribute() {
 			eqSupport = TypeParameter.EqualitySupportValue.Required; 

 		}

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

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

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

 		Expect(12);

 	}

 

@@ -416,7 +416,7 @@ bool IsAttribute() {
 		} else if (la.kind == 28 || la.kind == 29) {

 			MethodDecl(mmod, allowConstructors, out m);

 			mm.Add(m); 

-		} else SynErr(118);

+		} else SynErr(117);

 	}

 

 	void Attribute(ref Attributes attrs) {

@@ -487,7 +487,7 @@ bool IsAttribute() {
 		Attributes attrs = null;

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

 		

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

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

 		Expect(20);

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

 		

@@ -501,7 +501,7 @@ bool IsAttribute() {
 			IdentType(out id, out ty);

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

 		}

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

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

 		Expect(12);

 	}

 

@@ -547,7 +547,7 @@ bool IsAttribute() {
 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(121);

+			} else SynErr(120);

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

 			Get();

 			isPredicate = true; 

@@ -576,7 +576,7 @@ bool IsAttribute() {
 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(122);

+			} else SynErr(121);

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

 			Get();

 			isCoPredicate = true; 

@@ -601,8 +601,8 @@ bool IsAttribute() {
 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(123);

-		} else SynErr(124);

+			} else SynErr(122);

+		} else SynErr(123);

 		decreases = isCoPredicate ? null : new List<Expression/*!*/>(); 

 		while (StartOf(4)) {

 			FunctionSpec(reqs, reads, ens, decreases);

@@ -645,7 +645,7 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

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

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

 		if (la.kind == 28) {

 			Get();

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

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

 			}

 			

-		} else SynErr(126);

+		} else SynErr(125);

 		if (isConstructor) {

 		 if (mmod.IsGhost) {

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

@@ -683,7 +683,7 @@ bool IsAttribute() {
 		} else if (la.kind == 31) {

 			Get();

 			signatureOmitted = true; openParen = Token.NoToken; 

-		} else SynErr(127);

+		} else SynErr(126);

 		while (StartOf(5)) {

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

 		}

@@ -877,7 +877,7 @@ bool IsAttribute() {
 			ReferenceType(out tok, out ty);

 			break;

 		}

-		default: SynErr(128); break;

+		default: SynErr(127); break;

 		}

 	}

 

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

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

 		

-		while (!(StartOf(7))) {SynErr(129); Get();}

+		while (!(StartOf(7))) {SynErr(128); Get();}

 		if (la.kind == 32) {

 			Get();

 			while (IsAttribute()) {

@@ -917,7 +917,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					mod.Add(fe); 

 				}

 			}

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

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

 			Expect(12);

 		} else if (la.kind == 33 || la.kind == 34 || la.kind == 35) {

 			if (la.kind == 33) {

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

 				Get();

 				Expression(out e);

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

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

 				Expect(12);

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

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

@@ -936,19 +936,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Attribute(ref ensAttrs);

 				}

 				Expression(out e);

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

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

 				Expect(12);

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

-			} else SynErr(133);

+			} else SynErr(132);

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

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref decAttrs);

 			}

 			DecreasesList(decreases, false);

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

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

 			Expect(12);

-		} else SynErr(135);

+		} else SynErr(134);

 	}

 

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

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

 			fieldName = id.val; 

 			fe = new FrameExpression(new ImplicitThisExpr(id), fieldName); 

-		} else SynErr(136);

+		} else SynErr(135);

 	}

 

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

@@ -1056,7 +1056,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				GenericInstantiation(gt);

 			}

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

-		} else SynErr(137);

+		} else SynErr(136);

 	}

 

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

@@ -1065,10 +1065,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Requires(decreases == null || cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe; 

 		if (la.kind == 34) {

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

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

 			Get();

 			Expression(out e);

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

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

 			Expect(12);

 			reqs.Add(e); 

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

@@ -1082,12 +1082,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					reads.Add(fe); 

 				}

 			}

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

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

 			Expect(12);

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

 			Get();

 			Expression(out e);

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

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

 			Expect(12);

 			ens.Add(e); 

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

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

 			

 			DecreasesList(decreases, false);

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

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

 			Expect(12);

-		} else SynErr(143);

+		} else SynErr(142);

 	}

 

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

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

 		} else if (StartOf(8)) {

 			FrameExpression(out fe);

-		} else SynErr(144);

+		} else SynErr(143);

 	}

 

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

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

 		} else if (StartOf(10)) {

 			Expression(out e);

-		} else SynErr(145);

+		} else SynErr(144);

 	}

 

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

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

 		int breakCount;

 		

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

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

 		switch (la.kind) {

 		case 6: {

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

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

 			break;

 		}

-		case 1: case 2: case 19: case 23: case 94: case 95: case 96: case 97: case 98: case 99: case 100: {

+		case 1: case 2: case 19: case 23: case 94: case 95: case 96: case 97: case 98: case 99: {

 			UpdateStmt(out s);

 			break;

 		}

@@ -1210,8 +1210,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Get();

 					breakCount++; 

 				}

-			} else SynErr(147);

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

+			} else SynErr(146);

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

 			Expect(12);

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

 			break;

@@ -1225,7 +1225,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(12);

 			break;

 		}

-		default: SynErr(149); break;

+		default: SynErr(148); break;

 		}

 	}

 

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

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

 			Get();

-		} else SynErr(150);

+		} else SynErr(149);

 		Expect(12);

 		if (e == null) {

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

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

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

 			Get();

-		} else SynErr(151);

+		} else SynErr(150);

 		if (e == null) {

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

 		} else {

@@ -1335,12 +1335,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					suchThatAssume = t; 

 				}

 				Expression(out suchThat);

-			} else SynErr(152);

+			} else SynErr(151);

 			Expect(12);

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

 			Get();

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

-		} else SynErr(153);

+		} else SynErr(152);

 		if (suchThat != null) {

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

 		} else {

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

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

 					els = bs; 

-				} else SynErr(154);

+				} else SynErr(153);

 			}

 			if (guardOmitted) {

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

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

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(155);

+		} else SynErr(154);

 	}

 

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

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

 				Get();

 				bodyOmitted = true; 

-			} else SynErr(156);

+			} else SynErr(155);

 			if (guardOmitted || bodyOmitted) {

 			 if (mod != null) {

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

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

 			AlternativeBlock(out alternatives);

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

-		} else SynErr(157);

+		} else SynErr(156);

 	}

 

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

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

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(158);

+		} else SynErr(157);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

@@ -1715,7 +1715,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			while (la.kind == 14 || la.kind == 59) {

 				Suffix(ref e);

 			}

-		} else SynErr(159);

+		} else SynErr(158);

 	}

 

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

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

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(160);

+		} else SynErr(159);

 		Expect(25);

 	}

 

@@ -1773,20 +1773,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (StartOf(16)) {

 			if (la.kind == 33 || la.kind == 67) {

 				Invariant(out invariant);

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

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

 				Expect(12);

 				invariants.Add(invariant); 

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

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

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

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

 				Expect(12);

 			} else {

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

@@ -1801,7 +1801,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						mod.Add(fe); 

 					}

 				}

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

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

 				Expect(12);

 			}

 		}

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

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

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

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

+		while (!(la.kind == 0 || la.kind == 33 || la.kind == 67)) {SynErr(165); Get();}

 		if (la.kind == 33) {

 			Get();

 			isFree = true; 

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

 			Expression(out e);

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

-		} else SynErr(167);

+		} else SynErr(166);

 	}

 

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

@@ -1910,7 +1910,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

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

 			Get();

-		} else SynErr(168);

+		} else SynErr(167);

 	}

 

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

@@ -1948,7 +1948,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

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

 			Get();

-		} else SynErr(169);

+		} else SynErr(168);

 	}

 

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

@@ -2046,7 +2046,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

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

 			Get();

-		} else SynErr(170);

+		} else SynErr(169);

 	}

 

 	void OrOp() {

@@ -2054,7 +2054,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

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

 			Get();

-		} else SynErr(171);

+		} else SynErr(170);

 	}

 

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

@@ -2146,7 +2146,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(172); break;

+		default: SynErr(171); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(173);

+		} else SynErr(172);

 	}

 

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

@@ -2188,7 +2188,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

-		case 20: case 40: case 51: case 57: case 62: case 68: case 69: case 103: case 104: case 105: case 106: {

+		case 20: case 40: case 51: case 57: case 62: case 68: case 69: case 102: case 103: case 104: case 105: {

 			EndlessExpression(out e);

 			break;

 		}

@@ -2211,14 +2211,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			MapExpr(out e);

 			break;

 		}

-		case 2: case 19: case 23: case 94: case 95: case 96: case 97: case 98: case 99: case 100: {

+		case 2: case 19: case 23: case 94: case 95: case 96: case 97: case 98: case 99: {

 			ConstAtomExpression(out e);

 			while (la.kind == 14 || la.kind == 59) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		default: SynErr(174); break;

+		default: SynErr(173); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(175);

+		} else SynErr(174);

 	}

 

 	void NegOp() {

@@ -2241,7 +2241,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

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

 			Get();

-		} else SynErr(176);

+		} else SynErr(175);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -2254,7 +2254,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(101);

+			Expect(100);

 			Expression(out e0);

 			Expect(63);

 			Expression(out e1);

@@ -2265,7 +2265,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			MatchExpression(out e);

 			break;

 		}

-		case 103: case 104: case 105: case 106: {

+		case 102: case 103: case 104: case 105: {

 			QuantifierGuts(out e);

 			break;

 		}

@@ -2299,7 +2299,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			NamedExpr(out e);

 			break;

 		}

-		default: SynErr(177); break;

+		default: SynErr(176); break;

 		}

 	}

 

@@ -2351,7 +2351,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (StartOf(10)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (la.kind == 102) {

+				if (la.kind == 101) {

 					Get();

 					anyDots = true; 

 					if (StartOf(10)) {

@@ -2373,15 +2373,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(178);

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

+				} else SynErr(177);

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

 				Get();

 				anyDots = true; 

 				if (StartOf(10)) {

 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(179);

+			} else SynErr(178);

 			if (multipleIndices != null) {

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

 			 // make sure an array class with this dimensionality exists

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

 			

 			Expect(60);

-		} else SynErr(180);

+		} else SynErr(179);

 	}

 

 	void DisplayExpr(out Expression e) {

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

 			e = new SeqDisplayExpr(x, elements); 

 			Expect(60);

-		} else SynErr(181);

+		} else SynErr(180);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2455,7 +2455,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(25);

 		} else if (StartOf(19)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

-		} else SynErr(182);

+		} else SynErr(181);

 	}

 

 	void MapExpr(out Expression e) {

@@ -2489,7 +2489,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new MapComprehension(x, bvars, range, body); 

 		} else if (StartOf(19)) {

 			SemErr("map must be followed by literal in brackets or comprehension."); 

-		} else SynErr(183);

+		} else SynErr(182);

 	}

 

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

@@ -2538,15 +2538,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(23);

 			Expression(out e);

 			Expect(25);

-			e = new AllocatedExpr(x, e); 

-			break;

-		}

-		case 100: {

-			Get();

-			x = t; 

-			Expect(23);

-			Expression(out e);

-			Expect(25);

 			e = new OldExpr(x, e); 

 			break;

 		}

@@ -2566,7 +2557,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(25);

 			break;

 		}

-		default: SynErr(184); break;

+		default: SynErr(183); break;

 		}

 	}

 

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

 

 	void QSep() {

-		if (la.kind == 107) {

+		if (la.kind == 106) {

 			Get();

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

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

 			Get();

-		} else SynErr(185);

+		} else SynErr(184);

 	}

 

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

@@ -2627,13 +2618,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression range;

 		Expression/*!*/ body;

 		

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

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

 			Forall();

 			x = t;  univ = true; 

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

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

 			Exists();

 			x = t; 

-		} else SynErr(186);

+		} else SynErr(185);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body);

@@ -2664,7 +2655,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		Expect(19);

 		Expression(out range);

-		if (la.kind == 107 || la.kind == 108) {

+		if (la.kind == 106 || la.kind == 107) {

 			QSep();

 			Expression(out body);

 		}

@@ -2743,19 +2734,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void Forall() {

-		if (la.kind == 103) {

+		if (la.kind == 102) {

 			Get();

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

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

 			Get();

-		} else SynErr(187);

+		} else SynErr(186);

 	}

 

 	void Exists() {

-		if (la.kind == 105) {

+		if (la.kind == 104) {

 			Get();

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

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

 			Get();

-		} else SynErr(188);

+		} else SynErr(187);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2791,27 +2782,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, T,x,x,T, x,x,x,x, T,T,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

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

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

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

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

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

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

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

+		{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

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

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

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

+		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}

 

 	};

 } // end Parser

@@ -2935,96 +2926,95 @@ public class Errors {
 			case 96: s = "\"null\" expected"; break;

 			case 97: s = "\"this\" expected"; break;

 			case 98: s = "\"fresh\" expected"; break;

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

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

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

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

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

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

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

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

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

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

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

-			case 110: s = "invalid Dafny"; break;

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

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

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

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

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

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

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

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

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

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

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

+			case 110: s = "invalid SubModuleDecl"; break;

 			case 111: s = "invalid SubModuleDecl"; break;

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

-			case 113: s = "this symbol not expected in ClassDecl"; break;

-			case 114: s = "this symbol not expected in DatatypeDecl"; break;

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

-			case 116: s = "this symbol not expected in DatatypeDecl"; break;

-			case 117: s = "this symbol not expected in ArbitraryTypeDecl"; break;

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

+			case 112: s = "this symbol not expected in ClassDecl"; break;

+			case 113: s = "this symbol not expected in DatatypeDecl"; break;

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

+			case 115: s = "this symbol not expected in DatatypeDecl"; break;

+			case 116: s = "this symbol not expected in ArbitraryTypeDecl"; break;

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

+			case 118: s = "this symbol not expected in FieldDecl"; break;

 			case 119: s = "this symbol not expected in FieldDecl"; break;

-			case 120: s = "this symbol not expected in FieldDecl"; break;

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

 			case 121: s = "invalid FunctionDecl"; break;

 			case 122: s = "invalid FunctionDecl"; break;

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

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

-			case 125: s = "this symbol not expected in MethodDecl"; break;

+			case 124: s = "this symbol not expected in MethodDecl"; break;

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

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

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

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

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

+			case 128: s = "this symbol not expected in MethodSpec"; break;

 			case 129: s = "this symbol not expected in MethodSpec"; break;

 			case 130: s = "this symbol not expected in MethodSpec"; break;

 			case 131: s = "this symbol not expected in MethodSpec"; break;

-			case 132: s = "this symbol not expected in MethodSpec"; break;

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

-			case 134: s = "this symbol not expected in MethodSpec"; break;

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

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

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

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

+			case 133: s = "this symbol not expected in MethodSpec"; break;

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

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

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

+			case 137: s = "this symbol not expected in FunctionSpec"; break;

 			case 138: s = "this symbol not expected in FunctionSpec"; break;

 			case 139: s = "this symbol not expected in FunctionSpec"; break;

 			case 140: s = "this symbol not expected in FunctionSpec"; break;

 			case 141: s = "this symbol not expected in FunctionSpec"; break;

-			case 142: s = "this symbol not expected in FunctionSpec"; break;

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

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

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

-			case 146: s = "this symbol not expected in OneStmt"; break;

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

-			case 148: s = "this symbol not expected in OneStmt"; break;

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

-			case 150: s = "invalid AssertStmt"; break;

-			case 151: s = "invalid AssumeStmt"; break;

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

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

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

+			case 145: s = "this symbol not expected in OneStmt"; break;

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

+			case 147: s = "this symbol not expected in OneStmt"; break;

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

+			case 149: s = "invalid AssertStmt"; break;

+			case 150: s = "invalid AssumeStmt"; break;

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

 			case 152: s = "invalid UpdateStmt"; break;

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

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

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

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

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

 			case 156: s = "invalid WhileStmt"; break;

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

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

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

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

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

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

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

+			case 160: s = "this symbol not expected in LoopSpec"; break;

 			case 161: s = "this symbol not expected in LoopSpec"; break;

 			case 162: s = "this symbol not expected in LoopSpec"; break;

 			case 163: s = "this symbol not expected in LoopSpec"; break;

 			case 164: s = "this symbol not expected in LoopSpec"; break;

-			case 165: s = "this symbol not expected in LoopSpec"; break;

-			case 166: s = "this symbol not expected in Invariant"; break;

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

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

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

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

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

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

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

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

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

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

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

+			case 165: s = "this symbol not expected in Invariant"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-			case 181: s = "invalid DisplayExpr"; break;

-			case 182: s = "invalid MultiSetExpr"; break;

-			case 183: s = "invalid MapExpr"; break;

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

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

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

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

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

+			case 180: s = "invalid DisplayExpr"; break;

+			case 181: s = "invalid MultiSetExpr"; break;

+			case 182: s = "invalid MapExpr"; break;

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

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

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

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

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

 

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

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 8d6fa510..c1f41b6e 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1014,11 +1014,6 @@ namespace Microsoft.Dafny {
         PrintExpression(((FreshExpr)expr).E);

         wr.Write(")");

 

-      } else if (expr is AllocatedExpr) {

-        wr.Write("allocated(");

-        PrintExpression(((AllocatedExpr)expr).E);

-        wr.Write(")");

-

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         if (e.Op == UnaryExpr.Opcode.SeqLength) {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 0761d865..b131912c 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -763,10 +763,6 @@ namespace Microsoft.Dafny
         var e = (FreshExpr)expr;

         return new FreshExpr((e.tok), CloneExpr(e.E));

 

-      } else if (expr is AllocatedExpr) {

-        var e = (AllocatedExpr)expr;

-        return new AllocatedExpr((e.tok), CloneExpr(e.E));

-

       } else if (expr is UnaryExpr) {

         var e = (UnaryExpr)expr;

         return new UnaryExpr((e.tok), e.Op, CloneExpr(e.E));

@@ -3912,17 +3908,13 @@ namespace Microsoft.Dafny
           // fine

         } else if (UserDefinedType.DenotesClass(t) != null) {

           // fine

+        } else if (t.IsDatatype) {

+          // fine, treat this as the datatype itself.

         } else {

           Error(expr, "the argument of a fresh expression must denote an object or a collection of objects (instead got {0})", e.E.Type);

         }

         expr.Type = Type.Bool;

 

-      } else if (expr is AllocatedExpr) {

-        AllocatedExpr e = (AllocatedExpr)expr;

-        ResolveExpression(e.E, twoState);

-        // e.E can be of any type

-        expr.Type = Type.Bool;

-

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         ResolveExpression(e.E, twoState);

@@ -4522,10 +4514,6 @@ namespace Microsoft.Dafny
         Error(expr, "fresh expressions are allowed only in specification and ghost contexts");

         return;

 

-      } else if (expr is AllocatedExpr) {

-        Error(expr, "allocated expressions are allowed only in specification and ghost contexts");

-        return;

-

       } else if (expr is PredicateExpr) {

         var e = (PredicateExpr)expr;

         // ignore the guard

@@ -5587,8 +5575,6 @@ namespace Microsoft.Dafny
         return UsesSpecFeatures(e.E);

       } else if (expr is FreshExpr) {

         return true;

-      } else if (expr is AllocatedExpr) {

-        return true;

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         return UsesSpecFeatures(e.E);

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 0433519d..6f5e1135 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/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 = 109;

-	const int noSym = 109;

+	const int maxT = 108;

+	const int noSym = 108;

 

 

 	[ContractInvariantMethod]

@@ -540,11 +540,10 @@ public class Scanner {
 			case "null": t.kind = 96; break;

 			case "this": t.kind = 97; break;

 			case "fresh": t.kind = 98; break;

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

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

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

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

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

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

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

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

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

 			default: break;

 		}

 	}

@@ -718,13 +717,13 @@ public class Scanner {
 			case 51:

 				{t.kind = 93; break;}

 			case 52:

-				{t.kind = 104; break;}

+				{t.kind = 103; break;}

 			case 53:

-				{t.kind = 106; break;}

+				{t.kind = 105; break;}

 			case 54:

-				{t.kind = 107; break;}

+				{t.kind = 106; break;}

 			case 55:

-				{t.kind = 108; break;}

+				{t.kind = 107; break;}

 			case 56:

 				recEnd = pos; recKind = 5;

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

@@ -762,9 +761,9 @@ public class Scanner {
 				if (ch == '>') {AddCh(); goto case 34;}

 				else {t.kind = 24; break;}

 			case 64:

-				recEnd = pos; recKind = 102;

+				recEnd = pos; recKind = 101;

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

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

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

 			case 65:

 				recEnd = pos; recKind = 80;

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

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 25524287..a8541293 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1869,9 +1869,6 @@ namespace Microsoft.Dafny {
       } else if (expr is FreshExpr) {

         FreshExpr e = (FreshExpr)expr;

         return IsTotal(e.E, etran);

-      } else if (expr is AllocatedExpr) {

-        AllocatedExpr e = (AllocatedExpr)expr;

-        return IsTotal(e.E, etran);

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         Bpl.Expr t = IsTotal(e.E, etran);

@@ -2042,9 +2039,6 @@ namespace Microsoft.Dafny {
       } else if (expr is FreshExpr) {

         FreshExpr e = (FreshExpr)expr;

         return CanCallAssumption(e.E, etran);

-      } else if (expr is AllocatedExpr) {

-        AllocatedExpr e = (AllocatedExpr)expr;

-        return CanCallAssumption(e.E, etran);

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         Bpl.Expr t = CanCallAssumption(e.E, etran);

@@ -2485,9 +2479,6 @@ namespace Microsoft.Dafny {
       } else if (expr is FreshExpr) {

         FreshExpr e = (FreshExpr)expr;

         CheckWellformed(e.E, options, locals, builder, etran);

-      } else if (expr is AllocatedExpr) {

-        AllocatedExpr e = (AllocatedExpr)expr;

-        CheckWellformed(e.E, options, locals, builder, etran);

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         CheckWellformed(e.E, options, locals, builder, etran);

@@ -6114,7 +6105,7 @@ namespace Microsoft.Dafny {
             Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInSet), oIsFresh);

             return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), body);

           } else if (e.E.Type is SeqType) {

-            // generate:  (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Unbox(Seq#Index(X,$i)) != null ==> !old($Heap)[Seq#Index(X,$i),alloc])

+            // generate:  (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Unbox(Seq#Index(X,$i)) != null && !old($Heap)[Seq#Index(X,$i),alloc])

             // TODO: trigger?

             Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int));

             Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar);

@@ -6122,20 +6113,18 @@ namespace Microsoft.Dafny {
             Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i);

             Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, XsubI));

             Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI), predef.Null);

-            Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh);

+            Bpl.Expr body = Bpl.Expr.And(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh);

             return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(iVar), body);

+          } else if (e.E.Type.IsDatatype) {

+            Bpl.Expr alloc = translator.FunctionCall(e.tok, BuiltinFunction.DtAlloc, null, TrExpr(e.E), Old.HeapExpr);

+            return Bpl.Expr.Not(alloc);

           } else {

-            // generate:  x == null || !old($Heap)[x]

-            Bpl.Expr oNull = Bpl.Expr.Eq(TrExpr(e.E), predef.Null);

+            // generate:  x != null && !old($Heap)[x]

+            Bpl.Expr oNull = Bpl.Expr.Neq(TrExpr(e.E), predef.Null);

             Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E)));

-            return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.Or, oNull, oIsFresh);

+            return Bpl.Expr.And(oNull, oIsFresh);

           }

 

-        } else if (expr is AllocatedExpr) {

-          AllocatedExpr e = (AllocatedExpr)expr;

-          Bpl.Expr wh = translator.GetWhereClause(e.tok, TrExpr(e.E), e.E.Type, this);

-          return wh == null ? Bpl.Expr.True : wh;

-

         } else if (expr is UnaryExpr) {

           UnaryExpr e = (UnaryExpr)expr;

           Bpl.Expr arg = TrExpr(e.E);

@@ -8389,12 +8378,6 @@ namespace Microsoft.Dafny {
           if (se != e.E) {

             newExpr = new FreshExpr(expr.tok, se);

           }

-        } else if (expr is AllocatedExpr) {

-          AllocatedExpr e = (AllocatedExpr)expr;

-          Expression se = Substitute(e.E);

-          if (se != e.E) {

-            newExpr = new AllocatedExpr(expr.tok, se);

-          }

         } else if (expr is UnaryExpr) {

           UnaryExpr e = (UnaryExpr)expr;

           Expression se = Substitute(e.E);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index cfa79f1a..e3246f8f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -190,42 +190,39 @@ Execution trace:
     (0,0): anon28_Then

     (0,0): anon29_Then

     (0,0): anon19

-SmallTests.dfy(199,14): Error: assertion violation

+SmallTests.dfy(195,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Then

-SmallTests.dfy(206,14): Error: assertion violation

+    (0,0): anon6_Then

+SmallTests.dfy(202,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Else

+    (0,0): anon6_Else

     (0,0): anon3

-    (0,0): anon13_Then

-SmallTests.dfy(226,12): Error: assertion violation

+    (0,0): anon7_Then

+SmallTests.dfy(204,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Else

+    (0,0): anon6_Else

     (0,0): anon3

-    (0,0): anon13_Else

-    (0,0): anon6

-    (0,0): anon14_Then

-    (0,0): anon11

-SmallTests.dfy(271,24): Error BP5002: A precondition for this call might not hold.

-SmallTests.dfy(249,30): Related location: This is the precondition that might not hold.

+    (0,0): anon7_Else

+SmallTests.dfy(250,24): Error BP5002: A precondition for this call might not hold.

+SmallTests.dfy(228,30): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(266,19): anon3_Else

+    SmallTests.dfy(245,19): anon3_Else

     (0,0): anon2

-SmallTests.dfy(376,12): Error: assertion violation

+SmallTests.dfy(355,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(386,12): Error: assertion violation

+SmallTests.dfy(365,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(396,6): Error: cannot prove termination; try supplying a decreases clause

+SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

-SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path.

-SmallTests.dfy(300,11): Related location: This is the postcondition that might not hold.

+SmallTests.dfy(285,3): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(279,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon18_Else

@@ -234,27 +231,27 @@ Execution trace:
     (0,0): anon24_Then

     (0,0): anon15

     (0,0): anon25_Else

-SmallTests.dfy(347,12): Error: assertion violation

+SmallTests.dfy(326,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

     (0,0): anon7

-SmallTests.dfy(354,10): Error: assertion violation

+SmallTests.dfy(333,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(364,4): Error: cannot prove termination; try supplying a decreases clause

+SmallTests.dfy(343,4): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

-SmallTests.dfy(408,10): Error BP5003: A postcondition might not hold on this return path.

-SmallTests.dfy(411,41): Related location: This is the postcondition that might not hold.

+SmallTests.dfy(387,10): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(390,41): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon6_Else

-SmallTests.dfy(561,12): Error: assertion violation

+SmallTests.dfy(540,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

-SmallTests.dfy(575,20): Error: left-hand sides 0 and 1 may refer to the same location

+SmallTests.dfy(554,20): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

@@ -266,11 +263,11 @@ Execution trace:
     (0,0): anon31_Then

     (0,0): anon32_Then

     (0,0): anon12

-SmallTests.dfy(577,15): Error: left-hand sides 1 and 2 may refer to the same location

+SmallTests.dfy(556,15): Error: left-hand sides 1 and 2 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

-    SmallTests.dfy(570,18): anon28_Else

+    SmallTests.dfy(549,18): anon28_Else

     (0,0): anon4

     (0,0): anon29_Else

     (0,0): anon7

@@ -282,10 +279,10 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(584,25): Error: target object may be null

+SmallTests.dfy(563,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(597,10): Error: assertion violation

+SmallTests.dfy(576,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

@@ -1648,42 +1645,39 @@ Execution trace:
     (0,0): anon28_Then

     (0,0): anon29_Then

     (0,0): anon19

-SmallTests.dfy(199,14): Error: assertion violation

+SmallTests.dfy(195,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Then

-SmallTests.dfy(206,14): Error: assertion violation

+    (0,0): anon6_Then

+SmallTests.dfy(202,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Else

+    (0,0): anon6_Else

     (0,0): anon3

-    (0,0): anon13_Then

-SmallTests.dfy(226,12): Error: assertion violation

+    (0,0): anon7_Then

+SmallTests.dfy(204,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Else

+    (0,0): anon6_Else

     (0,0): anon3

-    (0,0): anon13_Else

-    (0,0): anon6

-    (0,0): anon14_Then

-    (0,0): anon11

-SmallTests.dfy(271,24): Error BP5002: A precondition for this call might not hold.

-SmallTests.dfy(249,30): Related location: This is the precondition that might not hold.

+    (0,0): anon7_Else

+SmallTests.dfy(250,24): Error BP5002: A precondition for this call might not hold.

+SmallTests.dfy(228,30): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(266,19): anon3_Else

+    SmallTests.dfy(245,19): anon3_Else

     (0,0): anon2

-SmallTests.dfy(376,12): Error: assertion violation

+SmallTests.dfy(355,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(386,12): Error: assertion violation

+SmallTests.dfy(365,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(396,6): Error: cannot prove termination; try supplying a decreases clause

+SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

-SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path.

-SmallTests.dfy(300,11): Related location: This is the postcondition that might not hold.

+SmallTests.dfy(285,3): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(279,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon18_Else

@@ -1692,27 +1686,27 @@ Execution trace:
     (0,0): anon24_Then

     (0,0): anon15

     (0,0): anon25_Else

-SmallTests.dfy(347,12): Error: assertion violation

+SmallTests.dfy(326,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

     (0,0): anon7

-SmallTests.dfy(354,10): Error: assertion violation

+SmallTests.dfy(333,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(364,4): Error: cannot prove termination; try supplying a decreases clause

+SmallTests.dfy(343,4): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

-SmallTests.dfy(408,10): Error BP5003: A postcondition might not hold on this return path.

-SmallTests.dfy(411,41): Related location: This is the postcondition that might not hold.

+SmallTests.dfy(387,10): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(390,41): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon6_Else

-SmallTests.dfy(561,12): Error: assertion violation

+SmallTests.dfy(540,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

-SmallTests.dfy(575,20): Error: left-hand sides 0 and 1 may refer to the same location

+SmallTests.dfy(554,20): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

@@ -1724,11 +1718,11 @@ Execution trace:
     (0,0): anon31_Then

     (0,0): anon32_Then

     (0,0): anon12

-SmallTests.dfy(577,15): Error: left-hand sides 1 and 2 may refer to the same location

+SmallTests.dfy(556,15): Error: left-hand sides 1 and 2 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

-    SmallTests.dfy(570,18): anon28_Else

+    SmallTests.dfy(549,18): anon28_Else

     (0,0): anon4

     (0,0): anon29_Else

     (0,0): anon7

@@ -1740,10 +1734,10 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(584,25): Error: target object may be null

+SmallTests.dfy(563,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(597,10): Error: assertion violation

+SmallTests.dfy(576,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

@@ -1796,42 +1790,39 @@ Execution trace:
     (0,0): anon28_Then

     (0,0): anon29_Then

     (0,0): anon19

-out.tmp.dfy(202,14): Error: assertion violation

+out.tmp.dfy(199,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Then

-out.tmp.dfy(208,14): Error: assertion violation

+    (0,0): anon6_Then

+out.tmp.dfy(205,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Else

+    (0,0): anon6_Else

     (0,0): anon3

-    (0,0): anon13_Then

-out.tmp.dfy(229,12): Error: assertion violation

+    (0,0): anon7_Then

+out.tmp.dfy(207,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Else

+    (0,0): anon6_Else

     (0,0): anon3

-    (0,0): anon13_Else

-    (0,0): anon6

-    (0,0): anon14_Then

-    (0,0): anon11

-out.tmp.dfy(266,24): Error BP5002: A precondition for this call might not hold.

-out.tmp.dfy(247,30): Related location: This is the precondition that might not hold.

+    (0,0): anon7_Else

+out.tmp.dfy(245,24): Error BP5002: A precondition for this call might not hold.

+out.tmp.dfy(226,30): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

-    out.tmp.dfy(263,19): anon3_Else

+    out.tmp.dfy(242,19): anon3_Else

     (0,0): anon2

-out.tmp.dfy(286,12): Error: assertion violation

+out.tmp.dfy(265,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(296,12): Error: assertion violation

+out.tmp.dfy(275,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(306,6): Error: cannot prove termination; try supplying a decreases clause

+out.tmp.dfy(285,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

-out.tmp.dfy(422,3): Error BP5003: A postcondition might not hold on this return path.

-out.tmp.dfy(416,11): Related location: This is the postcondition that might not hold.

+out.tmp.dfy(401,3): Error BP5003: A postcondition might not hold on this return path.

+out.tmp.dfy(395,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon18_Else

@@ -1840,27 +1831,27 @@ Execution trace:
     (0,0): anon24_Then

     (0,0): anon15

     (0,0): anon25_Else

-out.tmp.dfy(446,12): Error: assertion violation

+out.tmp.dfy(425,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

     (0,0): anon7

-out.tmp.dfy(451,10): Error: assertion violation

+out.tmp.dfy(430,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(461,4): Error: cannot prove termination; try supplying a decreases clause

+out.tmp.dfy(440,4): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

-out.tmp.dfy(469,10): Error BP5003: A postcondition might not hold on this return path.

-out.tmp.dfy(470,41): Related location: This is the postcondition that might not hold.

+out.tmp.dfy(448,10): Error BP5003: A postcondition might not hold on this return path.

+out.tmp.dfy(449,41): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon6_Else

-out.tmp.dfy(507,12): Error: assertion violation

+out.tmp.dfy(486,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

-out.tmp.dfy(521,20): Error: left-hand sides 0 and 1 may refer to the same location

+out.tmp.dfy(500,20): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

@@ -1872,11 +1863,11 @@ Execution trace:
     (0,0): anon31_Then

     (0,0): anon32_Then

     (0,0): anon12

-out.tmp.dfy(523,15): Error: left-hand sides 1 and 2 may refer to the same location

+out.tmp.dfy(502,15): Error: left-hand sides 1 and 2 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

-    out.tmp.dfy(516,18): anon28_Else

+    out.tmp.dfy(495,18): anon28_Else

     (0,0): anon4

     (0,0): anon29_Else

     (0,0): anon7

@@ -1888,10 +1879,10 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-out.tmp.dfy(530,25): Error: target object may be null

+out.tmp.dfy(509,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(543,10): Error: assertion violation

+out.tmp.dfy(522,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 40df1135..e74a9943 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -188,42 +188,21 @@ class Modifies {
 class AllocatedTests {

   method M(r: AllocatedTests, k: Node, S: set<Node>, d: Lindgren)

   {

-    assert allocated(r);

-

     var n := new Node;

     var t := S + {n};

-    assert allocated(t);

-

-    assert allocated(d);

+    

     if (*) {

-      assert old(allocated(n));  // error: n was not allocated in the initial state

+      assert !fresh(n);  // error: n was not allocated in the initial state

     } else {

-      assert !old(allocated(n));  // correct

+      assert fresh(n);  // correct

     }

 

     var U := {k,n};

     if (*) {

-      assert old(allocated(U));  // error: n was not allocated initially

+      assert !fresh(U);  // error: n was not allocated initially

     } else {

-      assert !old(allocated(U));  // correct (note, the assertion does NOT say: everything was unallocated in the initial state)

-    }

-

-    assert allocated(6);

-    assert allocated(6);

-    assert allocated(null);

-    assert allocated(Lindgren.HerrNilsson);

-

-    match (d) {

-      case Pippi(n) => assert allocated(n);

-      case Longstocking(q, dd) => assert allocated(q); assert allocated(dd);

-      case HerrNilsson => assert old(allocated(d));

+      assert fresh(U);  // correct (note, the assertion does NOT say: everything was unallocated in the initial state)

     }

-    var ls := Lindgren.Longstocking([], d);

-    assert allocated(ls);

-    assert old(allocated(ls));

-

-    assert old(allocated(Lindgren.Longstocking([r], d)));

-    assert old(allocated(Lindgren.Longstocking([n], d)));  // error, because n was not allocated initially

   }

 }

 

diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy
index 5a4da8ce..094e7be7 100644
--- a/Test/dafny1/SchorrWaite-stages.dfy
+++ b/Test/dafny1/SchorrWaite-stages.dfy
@@ -213,9 +213,9 @@ ghost module M2 refines M1 {
       // references, we need to make sure we can deal with the proof obligation for the path

       // argument.  For this reason, we add invariants that say that "path" and the .pathFromRoot

       // field of all marked nodes contain values that make sense in the pre-state.

-      invariant old(allocated(path)) && old(ReachableVia(root, path, t, S));

+      invariant !fresh(path) && old(ReachableVia(root, path, t, S));

       invariant forall n :: n in S && n.marked ==> var pth := n.pathFromRoot;

-                  old(allocated(pth)) && old(ReachableVia(root, pth, n, S));

+                  !fresh(pth) && old(ReachableVia(root, pth, n, S));

       invariant forall n :: n in S && n.marked ==> old(Reachable(root, n, S));

 

       decreases *;  // keep postponing termination checking

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 8da32b05..18adf491 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -12,6 +12,7 @@ class Node {
 

 datatype Path = Empty | Extend(Path, Node);

 

+

 class Main {

   method RecursiveMark(root: Node, ghost S: set<Node>)

     requires root in S;

@@ -213,9 +214,9 @@ class Main {
                   (forall j :: 0 <= j && j < |n.children| ==>

                     j == n.childrenVisited || n.children[j] == old(n.children[j])));

       // every marked node is reachable:

-      invariant old(allocated(path));  // needed to show 'path' worthy as argument to old(Reachable(...))

+      invariant !fresh(path);  // needed to show 'path' worthy as argument to old(Reachable(...))

       invariant old(ReachableVia(root, path, t, S));

-      invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==> old(allocated(pth)));

+      invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==> !fresh(pth));

       invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==>

                   old(ReachableVia(root, pth, n, S)));

       invariant (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));