Merge

1 files changed, 82 insertions, 72 deletions

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index e33e03ea..49e02bd8 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1056,11 +1056,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s = bs; 

 			break;

 		}

-		case 65: {

+		case 66: {

 			AssertStmt(out s);

 			break;

 		}

-		case 66: {

+		case 54: {

 			AssumeStmt(out s);

 			break;

 		}

@@ -1076,15 +1076,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			VarDeclStatement(out s);

 			break;

 		}

-		case 58: {

+		case 59: {

 			IfStmt(out s);

 			break;

 		}

-		case 62: {

+		case 63: {

 			WhileStmt(out s);

 			break;

 		}

-		case 64: {

+		case 65: {

 			MatchStmt(out s);

 			break;

 		}

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

 		Expression/*!*/ e = null; Attributes attrs = null;

 		

-		Expect(65);

+		Expect(66);

 		x = t; s = null;

 		while (IsAttribute()) {

 			Attribute(ref attrs);

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

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

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

-		Expect(66);

+		Expect(54);

 		x = t; 

 		Expression(out e);

 		Expect(18);

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

 		IToken x;

 		Attributes attrs = null;

+		IToken suchThatAssume = null;

 		Expression suchThat = null;

 		

 		Lhs(out e);

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

 				Get();

 				x = t; 

+				if (la.kind == 54) {

+					Get();

+					suchThatAssume = t; 

+				}

 				Expression(out suchThat);

 			} else SynErr(145);

 			Expect(18);

@@ -1226,7 +1231,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

 		} else SynErr(146);

 		if (suchThat != null) {

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

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

 		} else {

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

 		}

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

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

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

+		IToken suchThatAssume = null;

 		Expression suchThat = null;

 		

 		if (la.kind == 8) {

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

 				Get();

 				assignTok = t; 

+				if (la.kind == 54) {

+					Get();

+					suchThatAssume = t; 

+				}

 				Expression(out suchThat);

 			}

 		}

@@ -1281,7 +1291,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		 foreach (var lhs in lhss) {

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

 		 }

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

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

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

 		 update = null;

 		} else {

@@ -1306,7 +1316,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		ifStmt = dummyStmt;  // to please the compiler

 		

-		Expect(58);

+		Expect(59);

 		x = t; 

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

 			if (la.kind == 33) {

@@ -1316,9 +1326,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				guardOmitted = true; 

 			}

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

-			if (la.kind == 59) {

+			if (la.kind == 60) {

 				Get();

-				if (la.kind == 58) {

+				if (la.kind == 59) {

 					IfStmt(out s);

 					els = s; 

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

@@ -1351,7 +1361,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

 		

-		Expect(62);

+		Expect(63);

 		x = t; 

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

 			if (la.kind == 33) {

@@ -1395,11 +1405,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);

 		Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;

 		List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>(); 

-		Expect(64);

+		Expect(65);

 		x = t; 

 		Expression(out e);

 		Expect(6);

-		while (la.kind == 60) {

+		while (la.kind == 61) {

 			CaseStatement(out c);

 			cases.Add(c); 

 		}

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

 		Attributes attrs = null;

 		

-		if (la.kind == 54) {

+		if (la.kind == 55) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

-			if (la.kind == 33 || la.kind == 43 || la.kind == 55) {

-				if (la.kind == 55) {

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

+				if (la.kind == 56) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(56);

+					Expect(57);

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

 					

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

@@ -1527,7 +1537,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 r = new TypeRhs(newToken, ty, initCall);

 			}

 			

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

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

 			Get();

 			x = t; 

 			Expression(out e);

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

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e);

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

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

 				Suffix(ref e);

 			}

 		} else if (StartOf(15)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

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

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

 				Suffix(ref e);

 			}

 		} else SynErr(152);

@@ -1593,11 +1603,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Statement> body;

 		

 		Expect(6);

-		while (la.kind == 60) {

+		while (la.kind == 61) {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(61);

+			Expect(62);

 			body = new List<Statement>(); 

 			while (StartOf(10)) {

 				Stmt(body);

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

 		

 		while (StartOf(16)) {

-			if (la.kind == 29 || la.kind == 63) {

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

 				Invariant(out invariant);

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

 				Expect(18);

@@ -1653,12 +1663,12 @@ 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 == 29 || la.kind == 63)) {SynErr(159); Get();}

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

 		if (la.kind == 29) {

 			Get();

 			isFree = true; 

 		}

-		Expect(63);

+		Expect(64);

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

@@ -1673,7 +1683,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

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

 		

-		Expect(60);

+		Expect(61);

 		x = t; 

 		Ident(out id);

 		if (la.kind == 33) {

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

 			Expect(34);

 		}

-		Expect(61);

+		Expect(62);

 		while (StartOf(10)) {

 			Stmt(body);

 		}

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

 			break;

 		}

-		case 19: case 38: case 58: case 64: case 65: case 66: case 101: case 102: case 103: case 104: {

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

 			EndlessExpression(out e);

 			break;

 		}

 		case 1: {

 			DottedIdentifiersAndFunction(out e);

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

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

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 6: case 55: {

+		case 6: case 56: {

 			DisplayExpr(out e);

 			break;

 		}

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

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

 			ConstAtomExpression(out e);

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

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

 				Suffix(ref e);

 			}

 			break;

@@ -2096,18 +2106,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<BoundVar> letVars;  List<Expression> letRHSs;

 		

 		switch (la.kind) {

-		case 58: {

+		case 59: {

 			Get();

 			x = t; 

 			Expression(out e);

 			Expect(99);

 			Expression(out e0);

-			Expect(59);

+			Expect(60);

 			Expression(out e1);

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

 			break;

 		}

-		case 64: {

+		case 65: {

 			MatchExpression(out e);

 			break;

 		}

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

 			break;

 		}

-		case 65: {

+		case 66: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -2128,7 +2138,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new AssertExpr(x, e0, e1); 

 			break;

 		}

-		case 66: {

+		case 54: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -2208,7 +2218,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				e = new FunctionCallExpr(id, id.val, e, openParen, args); 

 			}

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

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

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

 			Get();

 			x = t; 

 			if (StartOf(9)) {

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

 					Expression(out ee);

 					e1 = ee; 

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

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

 					while (la.kind == 20) {

 						Get();

 						Expression(out ee);

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

 			}

 			

-			Expect(56);

+			Expect(57);

 		} else SynErr(173);

 	}

 

@@ -2284,14 +2294,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new SetDisplayExpr(x, elements);

 			Expect(7);

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

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

 			Get();

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

 			if (StartOf(9)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(56);

+			Expect(57);

 		} else SynErr(174);

 	}

 

@@ -2329,14 +2339,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Expect(41);

 		x = t; 

-		if (la.kind == 55) {

+		if (la.kind == 56) {

 			Get();

 			elements = new List<ExpressionPair/*!*/>(); 

 			if (StartOf(9)) {

 				MapLiteralExpressions(out elements);

 			}

 			e = new MapDisplayExpr(x, elements);

-			Expect(56);

+			Expect(57);

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

 			BoundVar/*!*/ bv;

 			List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

@@ -2472,10 +2482,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();

 		

-		Expect(64);

+		Expect(65);

 		x = t; 

 		Expression(out e);

-		while (la.kind == 60) {

+		while (la.kind == 61) {

 			CaseExpression(out c);

 			cases.Add(c); 

 		}

@@ -2542,7 +2552,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

 		Expression/*!*/ body;

 		

-		Expect(60);

+		Expect(61);

 		x = t; 

 		Ident(out id);

 		if (la.kind == 33) {

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

 			Expect(34);

 		}

-		Expect(61);

+		Expect(62);

 		Expression(out body);

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

 	}

@@ -2610,7 +2620,7 @@ 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,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

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

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

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

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

@@ -2619,18 +2629,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

 	};

 } // end Parser

@@ -2709,19 +2719,19 @@ public class Errors {
 			case 51: s = "\"return\" expected"; break;

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

 			case 53: s = "\":|\" expected"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 			case 68: s = "\"parallel\" expected"; break;

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