diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index f2ffdba46..56183e37b 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -229,8 +229,7 @@ private void CheckAsyncToSyncSafety(ActionDecl actionDecl, HashSet<string> refin
               Error(callCmd, "unable to eliminate pending async since a global is modified subsequently");
             }
           }
-          var assignedVariables = new List<Variable>();
-          cmd.AddAssignedVariables(assignedVariables);
+          var assignedVariables = cmd.GetAssignedVariables().ToList();
           if (assignedVariables.OfType<GlobalVariable>().Any())
           {
             modifiedGlobals = true;
diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
index 483652543..307f898cf 100644
--- a/Source/Core/AST/Absy.cs
+++ b/Source/Core/AST/Absy.cs
@@ -2042,6 +2042,7 @@ public DatatypeConstructor(Function func)
 
   public class Function : DeclWithFormals
   {
+    public bool AlwaysRevealed;
     public string Comment;
 
     public Expr Body; // Only set if the function is declared with {:inline}
@@ -2121,7 +2122,7 @@ public override void Emit(TokenTextWriter stream, int level)
         stream.WriteLine(this, level, "// " + Comment);
       }
 
-      stream.Write(this, level, "function ");
+      stream.Write(this, level, (AlwaysRevealed ? "revealed " : "") + "function ");
       EmitAttributes(stream);
       if (Body != null && !QKeyValue.FindBoolAttribute(Attributes, "inline"))
       {
@@ -3823,10 +3824,9 @@ public RE()
     {
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars)
     {
-      //Contract.Requires(vars != null);
-      throw new NotImplementedException();
+      throw new NotSupportedException();
     }
   }
 
diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs
index 85d35413d..fb84e2a35 100644
--- a/Source/Core/AST/AbsyCmd.cs
+++ b/Source/Core/AST/AbsyCmd.cs
@@ -1108,7 +1108,6 @@ void ObjectInvariant()
       Contract.Invariant(cce.NonNullElements(Invariants));
     }
 
-
     public WhileCmd(IToken tok, [Captured] Expr guard, List<PredicateCmd> invariants, List<CallCmd> yields, StmtList body)
       : base(tok)
     {
@@ -1205,10 +1204,8 @@ public override void Emit(TokenTextWriter stream, int level)
       throw new NotImplementedException();
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
-      Contract.Requires(vars != null);
-      throw new NotImplementedException();
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
+      throw new NotSupportedException();
     }
   }
 
@@ -1352,14 +1349,22 @@ public Cmd(IToken /*!*/ tok)
     }
 
     public abstract void Emit(TokenTextWriter /*!*/ stream, int level);
-    public abstract void AddAssignedVariables(List<Variable> /*!*/ vars);
+
+    /// <summary>
+    /// Should only be called after resolution
+    /// </summary>
+    public IEnumerable<Variable> GetAssignedVariables() {
+      List<IdentifierExpr> ids = new();
+      AddAssignedIdentifiers(ids);
+      return ids.Select(id => id.Decl);
+    }
+    
+    public abstract void AddAssignedIdentifiers(List<IdentifierExpr> /*!*/ vars);
 
     public void CheckAssignments(TypecheckingContext tc)
     {
       Contract.Requires(tc != null);
-      List<Variable> /*!*/
-        vars = new List<Variable>();
-      this.AddAssignedVariables(vars);
+      var /*!*/ vars = GetAssignedVariables().ToList();
       foreach (Variable /*!*/ v in vars)
       {
         Contract.Assert(v != null);
@@ -1527,9 +1532,8 @@ public override void Emit(TokenTextWriter stream, int level)
     public override void Resolve(ResolutionContext rc)
     {
     }
-
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
+    
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
     }
 
     public override void Typecheck(TypecheckingContext tc)
@@ -1777,12 +1781,10 @@ public override void Typecheck(TypecheckingContext tc)
       }
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
       foreach (AssignLhs /*!*/ l in Lhss)
       {
-        Contract.Assert(l != null);
-        vars.Add(l.DeepAssignedVariable);
+        vars.Add(l.DeepAssignedIdentifier);
       }
     }
 
@@ -2307,9 +2309,8 @@ public Expr Rhs
 
     public IEnumerable<IdentifierExpr> UnpackedLhs => lhs.Args.Cast<IdentifierExpr>();
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
-      lhs.Args.Cast<IdentifierExpr>().ForEach(arg => vars.Add(arg.Decl));
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
+      lhs.Args.Cast<IdentifierExpr>().ForEach(vars.Add);
     }
 
     public override void Emit(TokenTextWriter stream, int level)
@@ -2423,21 +2424,19 @@ public override void Resolve(ResolutionContext rc)
       rc.PopVarContext();
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
-      //Contract.Requires(vars != null);
-      List<Variable> vs = new List<Variable>();
-      foreach (Cmd cmd in this.Cmds)
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
+      var vs = new List<IdentifierExpr>();
+      foreach (Cmd cmd in Cmds)
       {
         Contract.Assert(cmd != null);
-        cmd.AddAssignedVariables(vs);
+        cmd.AddAssignedIdentifiers(vs);
       }
 
       var localsSet = new HashSet<Variable>(this.Locals);
-      foreach (Variable v in vs)
+      foreach (var v in vs)
       {
-        Contract.Assert(v != null);
-        if (!localsSet.Contains(v))
+        Debug.Assert(v.Decl != null);
+        if (!localsSet.Contains(v.Decl))
         {
           vars.Add(v);
         }
@@ -2773,11 +2772,10 @@ public override void Typecheck(TypecheckingContext tc)
       }
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
       foreach (CallCmd callCmd in CallCmds)
       {
-        callCmd.AddAssignedVariables(vars);
+        callCmd.AddAssignedIdentifiers(vars);
       }
     }
 
@@ -2860,6 +2858,7 @@ void ObjectInvariant()
       Contract.Invariant(Expr != null);
     }
 
+    
     public PredicateCmd(IToken /*!*/ tok, Expr /*!*/ expr)
       : base(tok)
     {
@@ -2900,8 +2899,7 @@ public override void Resolve(ResolutionContext rc)
       }
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
     }
   }
 
@@ -3335,8 +3333,7 @@ public override Absy StdDispatch(StandardVisitor visitor)
 
   public class HavocCmd : Cmd
   {
-    private List<IdentifierExpr> /*!*/
-      _vars;
+    private List<IdentifierExpr> /*!*/ _vars;
 
     public List<IdentifierExpr> /*!*/ Vars
     {
@@ -3384,13 +3381,11 @@ public override void Resolve(ResolutionContext rc)
       }
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
-      //Contract.Requires(vars != null);
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
       foreach (IdentifierExpr /*!*/ e in this.Vars)
       {
         Contract.Assert(e != null);
-        vars.Add(e.Decl);
+        vars.Add(e);
       }
     }
 
diff --git a/Source/Core/AST/CallCmd.cs b/Source/Core/AST/CallCmd.cs
index 12646a965..d39768d22 100644
--- a/Source/Core/AST/CallCmd.cs
+++ b/Source/Core/AST/CallCmd.cs
@@ -540,8 +540,8 @@ private void TypecheckCallCmdInActionDecl(TypecheckingContext tc)
     }
   }
 
-  public override void AddAssignedVariables(List<Variable> vars)
-  {
+  public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
+    
     if (this.IsAsync)
     {
       return;
@@ -551,7 +551,7 @@ public override void AddAssignedVariables(List<Variable> vars)
     {
       if (e != null)
       {
-        vars.Add(e.Decl);
+        vars.Add(e);
       }
     }
 
@@ -559,12 +559,12 @@ public override void AddAssignedVariables(List<Variable> vars)
     foreach (IdentifierExpr /*!*/ e in this.Proc.Modifies)
     {
       Contract.Assert(e != null);
-      vars.Add(e.Decl);
+      vars.Add(e);
     }
 
     if (AssignedAssumptionVariable != null)
     {
-      vars.Add(AssignedAssumptionVariable);
+      vars.Add(new IdentifierExpr(tok, AssignedAssumptionVariable));
     }
   }
 
diff --git a/Source/Core/AST/ChangeScope.cs b/Source/Core/AST/ChangeScope.cs
index b04922bd4..1d9580e7a 100644
--- a/Source/Core/AST/ChangeScope.cs
+++ b/Source/Core/AST/ChangeScope.cs
@@ -28,7 +28,7 @@ public override void Emit(TokenTextWriter stream, int level) {
     stream.WriteLine(";");
   }
 
-  public override void AddAssignedVariables(List<Variable> vars) {
+  public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
   }
 
   public override Absy StdDispatch(StandardVisitor visitor) {
diff --git a/Source/Core/AST/HideRevealCmd.cs b/Source/Core/AST/HideRevealCmd.cs
index 49a47d958..48953b4f9 100644
--- a/Source/Core/AST/HideRevealCmd.cs
+++ b/Source/Core/AST/HideRevealCmd.cs
@@ -44,8 +44,7 @@ public override void Emit(TokenTextWriter stream, int level)
     stream.WriteLine(";");
   }
 
-  public override void AddAssignedVariables(List<Variable> vars)
-  {
+  public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
   }
 
   public override Absy StdDispatch(StandardVisitor visitor)
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 66c5789aa..b850527c2 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -459,7 +459,10 @@ Function<.out List<Declaration>/*!*/ ds.>
      Expr definition = null;
      Expr/*!*/ tmp;
      Axiom ax;
+     bool revealed = false;
   .)
+  [ "revealed"                         (. revealed = true; .) 
+  ]
   "function" { Attribute<ref kv> } Ident<out z>
   [ TypeParams<out typeParamTok, out typeParams> ]
   "("
@@ -483,6 +486,7 @@ Function<.out List<Declaration>/*!*/ ds.>
     }
     Function/*!*/ func = new Function(z, z.val, typeParams, arguments,
                                       new Formal(retTyd.tok, retTyd, false, argKv), null, kv);
+    func.AlwaysRevealed = revealed;
     foreach(var axiom in axioms) {
         ds.Add(axiom);
         func.OtherDefinitionAxioms.Add(axiom);
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 0094b0fc3..ff6ecb84f 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -36,7 +36,7 @@ public class Parser {
 	public const int _decimal = 5;
 	public const int _dec_float = 6;
 	public const int _float = 7;
-	public const int maxT = 124;
+	public const int maxT = 125;
 
 	const bool _T = true;
 	const bool _x = false;
@@ -255,7 +255,7 @@ void BoogiePL() {
 				
 				break;
 			}
-			case 28: {
+			case 28: case 29: {
 				Function(out ds);
 				foreach(Bpl.Declaration/*!*/ d in ds){
 				 Contract.Assert(d != null);
@@ -264,12 +264,12 @@ void BoogiePL() {
 				
 				break;
 			}
-			case 30: case 31: {
+			case 31: case 32: {
 				Axiom(out ax);
 				Pgm.AddTopLevelDeclaration(ax); 
 				break;
 			}
-			case 32: {
+			case 33: {
 				UserDefinedTypes(out ts);
 				foreach(Declaration/*!*/ td in ts){
 				 Contract.Assert(td != null);
@@ -278,7 +278,7 @@ void BoogiePL() {
 				
 				break;
 			}
-			case 34: {
+			case 35: {
 				Datatype(out dt);
 				Pgm.AddTopLevelDeclaration(dt); 
 				break;
@@ -294,7 +294,7 @@ void BoogiePL() {
 			}
 			case 8: {
 				Get();
-				if (la.kind == 35) {
+				if (la.kind == 36) {
 					YieldInvariantDecl(out yi);
 					Pgm.AddTopLevelDeclaration(yi); 
 				} else if (StartOf(2)) {
@@ -304,12 +304,12 @@ void BoogiePL() {
 					 Pgm.AddTopLevelDeclaration(im);
 					}
 					
-				} else SynErr(125);
+				} else SynErr(126);
 				break;
 			}
-			case 36: case 37: case 38: case 42: case 43: case 44: case 45: case 46: {
+			case 37: case 38: case 39: case 43: case 44: case 45: case 46: case 47: {
 				Pure(ref isPure);
-				if (la.kind == 46) {
+				if (la.kind == 47) {
 					Procedure(isPure, out pr, out im);
 					Pgm.AddTopLevelDeclaration(pr);
 					if (im != null) {
@@ -328,10 +328,10 @@ void BoogiePL() {
 					}
 					isPure = false;
 					
-				} else SynErr(126);
+				} else SynErr(127);
 				break;
 			}
-			case 51: {
+			case 52: {
 				Implementation(out nnim);
 				Pgm.AddTopLevelDeclaration(nnim); 
 				break;
@@ -362,12 +362,12 @@ void Consts(out List<Declaration>/*!*/ ds) {
 		} else if (la.kind == 25) {
 			Get();
 			Expect(26);
-			while (la.kind == 30 || la.kind == 31) {
+			while (la.kind == 31 || la.kind == 32) {
 				Axiom(out axiom);
 				axioms.Add(axiom); ds.Add(axiom); 
 			}
 			Expect(27);
-		} else SynErr(127);
+		} else SynErr(128);
 		foreach(TypedIdent/*!*/ x in xs){
 		 Contract.Assert(x != null);
 		 var constant = new Constant(y, x, u, kv, axioms);
@@ -391,8 +391,13 @@ void Function(out List<Declaration>/*!*/ ds) {
 		Expr definition = null;
 		Expr/*!*/ tmp;
 		Axiom ax;
+		bool revealed = false;
 		
-		Expect(28);
+		if (la.kind == 28) {
+			Get();
+			revealed = true; 
+		}
+		Expect(29);
 		while (la.kind == 26) {
 			Attribute(ref kv);
 		}
@@ -412,7 +417,7 @@ void Function(out List<Declaration>/*!*/ ds) {
 		}
 		Expect(12);
 		argKv = null; 
-		if (la.kind == 29) {
+		if (la.kind == 30) {
 			Get();
 			Expect(11);
 			VarOrType(out retTyd, out argKv);
@@ -421,7 +426,7 @@ void Function(out List<Declaration>/*!*/ ds) {
 			Get();
 			Type(out retTy);
 			retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); 
-		} else SynErr(128);
+		} else SynErr(129);
 		if (la.kind == 26) {
 			Get();
 			Expression(out tmp);
@@ -430,7 +435,7 @@ void Function(out List<Declaration>/*!*/ ds) {
 			if (la.kind == 25) {
 				Get();
 				Expect(26);
-				while (la.kind == 30 || la.kind == 31) {
+				while (la.kind == 31 || la.kind == 32) {
 					Axiom(out ax);
 					axioms.Add(ax); 
 				}
@@ -439,20 +444,21 @@ void Function(out List<Declaration>/*!*/ ds) {
 		} else if (la.kind == 25) {
 			Get();
 			Expect(26);
-			while (la.kind == 30 || la.kind == 31) {
+			while (la.kind == 31 || la.kind == 32) {
 				Axiom(out ax);
 				axioms.Add(ax); 
 			}
 			Expect(27);
 		} else if (la.kind == 10) {
 			Get();
-		} else SynErr(129);
+		} else SynErr(130);
 		if (retTyd == null) {
 		 // construct a dummy type for the case of syntax error
 		 retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
 		}
 		Function/*!*/ func = new Function(z, z.val, typeParams, arguments,
 		                                 new Formal(retTyd.tok, retTyd, false, argKv), null, kv);
+		func.AlwaysRevealed = revealed;
 		foreach(var axiom in axioms) {
 		   ds.Add(axiom);
 		   func.OtherDefinitionAxioms.Add(axiom);
@@ -515,11 +521,11 @@ void Axiom(out Axiom/*!*/ m) {
 		Expr/*!*/ e; 
 		QKeyValue kv = null; 
 		bool canHide = false; 
-		if (la.kind == 30) {
+		if (la.kind == 31) {
 			Get();
 			canHide = true; 
 		}
-		Expect(31);
+		Expect(32);
 		while (la.kind == 26) {
 			Attribute(ref kv);
 		}
@@ -531,7 +537,7 @@ void Axiom(out Axiom/*!*/ m) {
 
 	void UserDefinedTypes(out List<Declaration/*!*/>/*!*/ ts) {
 		Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> (); 
-		Expect(32);
+		Expect(33);
 		while (la.kind == 26) {
 			Attribute(ref kv);
 		}
@@ -547,7 +553,7 @@ void UserDefinedTypes(out List<Declaration/*!*/>/*!*/ ts) {
 
 	void Datatype(out DatatypeTypeCtorDecl datatypeTypeCtorDecl) {
 		QKeyValue kv = null; IToken/*!*/ typeParamTok, name; List<TypeVariable> typeParams = new List<TypeVariable>(); 
-		Expect(34);
+		Expect(35);
 		while (la.kind == 26) {
 			Attribute(ref kv);
 		}
@@ -577,14 +583,14 @@ void GlobalVars(out List<Variable>/*!*/ ds) {
 
 	void YieldInvariantDecl(out YieldInvariantDecl yieldInvariant) {
 		List<Requires> invariants = new List<Requires>(); QKeyValue kv = null; IToken name = null; List<Variable> ins; 
-		Expect(35);
+		Expect(36);
 		while (la.kind == 26) {
 			Attribute(ref kv);
 		}
 		Ident(out name);
 		ProcFormals(true, true, out ins);
 		Expect(10);
-		while (la.kind == 35) {
+		while (la.kind == 36) {
 			Invariant(invariants);
 		}
 		yieldInvariant = new YieldInvariantDecl(name, name.val, ins, invariants, kv); 
@@ -609,13 +615,13 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl)
 		if (StartOf(5)) {
 			MoverQualifier(ref moverType);
 		}
-		Expect(46);
+		Expect(47);
 		while (la.kind == 26) {
 			Attribute(ref kv);
 		}
 		Ident(out name);
 		ProcFormals(true, true, out ins);
-		if (la.kind == 29) {
+		if (la.kind == 30) {
 			Get();
 			ProcFormals(false, true, out outs);
 		}
@@ -632,12 +638,12 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl)
 			impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
 			                         locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
 			
-		} else SynErr(130);
+		} else SynErr(131);
 		ypDecl = new YieldProcedureDecl(name, name.val, moverType, ins, outs, pre, mods, post, yieldRequires, yieldEnsures, yieldPreserves, refinedAction, kv); 
 	}
 
 	void Pure(ref bool isPure) {
-		if (la.kind == 36) {
+		if (la.kind == 37) {
 			Get();
 			isPure = true; 
 		}
@@ -655,7 +661,7 @@ void Procedure(bool isPure, out Procedure/*!*/ proc, out /*maybe null*/ Implemen
 		QKeyValue kv = null;
 		impl = null;
 		
-		Expect(46);
+		Expect(47);
 		ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);
 		if (la.kind == 10) {
 			Get();
@@ -670,7 +676,7 @@ void Procedure(bool isPure, out Procedure/*!*/ proc, out /*maybe null*/ Implemen
 			impl = new Implementation(x, x.val, typeParams.ConvertAll(tp => new TypeVariable(tp.tok, tp.Name)),
 			                         Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
 			
-		} else SynErr(131);
+		} else SynErr(132);
 		proc = new Procedure(x, x.val, typeParams, ins, outs, isPure, pre, mods, post, kv); 
 	}
 
@@ -692,20 +698,20 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl,
 		datatypeTypeCtorDecl = null;
 		impl = null;
 		
-		if (la.kind == 37) {
+		if (la.kind == 38) {
 			Get();
 			isAsync = true; 
 		}
 		if (StartOf(5)) {
 			MoverQualifier(ref moverType);
 		}
-		Expect(38);
+		Expect(39);
 		while (la.kind == 26) {
 			Attribute(ref kv);
 		}
 		Ident(out name);
 		ProcFormals(true, true, out ins);
-		if (la.kind == 29) {
+		if (la.kind == 30) {
 			Get();
 			ProcFormals(false, true, out outs);
 		}
@@ -722,7 +728,7 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl,
 			impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
 			                              locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
 			
-		} else SynErr(132);
+		} else SynErr(133);
 		if (isPure) {
 		 if (moverType == MoverType.None)
 		 {
@@ -761,7 +767,7 @@ void Implementation(out Implementation/*!*/ impl) {
 		StmtList/*!*/ stmtList;
 		QKeyValue kv;
 		
-		Expect(51);
+		Expect(52);
 		ProcSignature(false, out x, out typeParams, out ins, out outs, out kv);
 		ImplBody(out locals, out stmtList);
 		impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); 
@@ -860,7 +866,7 @@ void Type(out Bpl.Type/*!*/ ty) {
 			ty = new UnresolvedTypeIdentifier (tok, tok.val, args); 
 		} else if (la.kind == 19 || la.kind == 21) {
 			MapType(out ty);
-		} else SynErr(133);
+		} else SynErr(134);
 	}
 
 	void AttributesIdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
@@ -896,7 +902,7 @@ void IdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIde
 	void Expression(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		ImpliesExpression(false, out e0);
-		while (la.kind == 73 || la.kind == 74) {
+		while (la.kind == 74 || la.kind == 75) {
 			EquivOp();
 			x = t; 
 			ImpliesExpression(false, out e1);
@@ -919,7 +925,7 @@ void TypeAtom(out Bpl.Type/*!*/ ty) {
 			Get();
 			Type(out ty);
 			Expect(12);
-		} else SynErr(134);
+		} else SynErr(135);
 	}
 
 	void Ident(out IToken/*!*/ x) {
@@ -929,47 +935,47 @@ void Ident(out IToken/*!*/ x) {
 			Get();
 			break;
 		}
-		case 45: {
+		case 46: {
 			Get();
 			t.kind = _ident; 
 			break;
 		}
-		case 44: {
+		case 45: {
 			Get();
 			t.kind = _ident; 
 			break;
 		}
-		case 42: {
+		case 43: {
 			Get();
 			t.kind = _ident; 
 			break;
 		}
-		case 43: {
+		case 44: {
 			Get();
 			t.kind = _ident; 
 			break;
 		}
-		case 61: {
+		case 62: {
 			Get();
 			t.kind = _ident; 
 			break;
 		}
-		case 62: {
+		case 63: {
 			Get();
 			t.kind = _ident; 
 			break;
 		}
-		case 64: {
+		case 65: {
 			Get();
 			t.kind = _ident; 
 			break;
 		}
-		case 63: {
+		case 64: {
 			Get();
 			t.kind = _ident; 
 			break;
 		}
-		default: SynErr(135); break;
+		default: SynErr(136); break;
 		}
 		x = t;
 		if (x.val.StartsWith("\\"))
@@ -995,7 +1001,7 @@ void TypeArgs(List<Bpl.Type>/*!*/ ts) {
 		} else if (la.kind == 19 || la.kind == 21) {
 			MapType(out ty);
 			ts.Add(ty); 
-		} else SynErr(136);
+		} else SynErr(137);
 	}
 
 	void MapType(out Bpl.Type/*!*/ ty) {
@@ -1082,7 +1088,7 @@ void UserDefinedType(out Declaration/*!*/ decl, QKeyValue kv) {
 		if (StartOf(14)) {
 			WhiteSpaceIdents(out paramTokens);
 		}
-		if (la.kind == 33) {
+		if (la.kind == 34) {
 			Get();
 			Type(out body);
 			synonym = true; 
@@ -1133,7 +1139,7 @@ void Constructor(DatatypeTypeCtorDecl datatypeTypeCtorDecl) {
 
 	void Invariant(List<Requires> invariants) {
 		Expr e; IToken tok = null; QKeyValue kv = null; 
-		Expect(35);
+		Expect(36);
 		tok = t; 
 		while (la.kind == 26) {
 			Attribute(ref kv);
@@ -1144,40 +1150,40 @@ void Invariant(List<Requires> invariants) {
 	}
 
 	void MoverQualifier(ref MoverType moverType) {
-		if (la.kind == 42) {
+		if (la.kind == 43) {
 			Get();
 			moverType = MoverType.Left; 
-		} else if (la.kind == 43) {
+		} else if (la.kind == 44) {
 			Get();
 			moverType = MoverType.Right; 
-		} else if (la.kind == 44) {
+		} else if (la.kind == 45) {
 			Get();
 			moverType = MoverType.Both; 
-		} else if (la.kind == 45) {
+		} else if (la.kind == 46) {
 			Get();
 			moverType = MoverType.Atomic; 
-		} else SynErr(137);
+		} else SynErr(138);
 	}
 
 	void SpecAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List<IdentifierExpr> mods, List<ActionDeclRef> creates, List<Requires> requires, List<CallCmd> yieldRequires, List<AssertCmd> asserts) {
-		if (la.kind == 40) {
+		if (la.kind == 41) {
 			SpecRefinedAction(ref refinedAction);
 			IToken m; 
-			if (la.kind == 41) {
+			if (la.kind == 42) {
 				Get();
 				Ident(out m);
 				invariantAction = new ActionDeclRef(m, m.val); 
 			}
 			Expect(10);
-		} else if (la.kind == 53) {
+		} else if (la.kind == 54) {
 			SpecModifies(mods);
-		} else if (la.kind == 39) {
+		} else if (la.kind == 40) {
 			SpecCreates(creates);
-		} else if (la.kind == 48) {
+		} else if (la.kind == 49) {
 			SpecYieldRequires(requires, yieldRequires);
-		} else if (la.kind == 47) {
+		} else if (la.kind == 48) {
 			SpecAsserts(asserts);
-		} else SynErr(138);
+		} else SynErr(139);
 	}
 
 	void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {
@@ -1190,7 +1196,7 @@ void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {
 	}
 
 	void SpecCreates(List<ActionDeclRef> creates) {
-		Expect(39);
+		Expect(40);
 		List<IToken> cs; 
 		Idents(out cs);
 		foreach(IToken c in cs) { creates.Add(new ActionDeclRef(c, c.val)); } 
@@ -1199,7 +1205,7 @@ void SpecCreates(List<ActionDeclRef> creates) {
 
 	void SpecRefinedAction(ref ActionDeclRef refinedAction) {
 		IToken m; QKeyValue kv = null; 
-		Expect(40);
+		Expect(41);
 		while (la.kind == 26) {
 			Attribute(ref kv);
 		}
@@ -1214,7 +1220,7 @@ void SpecRefinedAction(ref ActionDeclRef refinedAction) {
 
 	void SpecModifies(List<IdentifierExpr> mods) {
 		List<IToken> ms; 
-		Expect(53);
+		Expect(54);
 		if (StartOf(14)) {
 			Idents(out ms);
 			foreach(IToken m in ms) { mods.Add(new IdentifierExpr(m, m.val)); } 
@@ -1224,7 +1230,7 @@ void SpecModifies(List<IdentifierExpr> mods) {
 
 	void SpecYieldRequires(List<Requires> pre, List<CallCmd> yieldRequires ) {
 		Expr e; Cmd cmd; Token tok; QKeyValue kv = null; 
-		Expect(48);
+		Expect(49);
 		tok = t; 
 		if (StartOf(16)) {
 			while (la.kind == 26) {
@@ -1232,16 +1238,16 @@ void SpecYieldRequires(List<Requires> pre, List<CallCmd> yieldRequires ) {
 			}
 			Proposition(out e);
 			pre.Add(new Requires(tok, false, e, null, kv)); 
-		} else if (la.kind == 37 || la.kind == 52 || la.kind == 70) {
+		} else if (la.kind == 38 || la.kind == 53 || la.kind == 71) {
 			CallCmd(out cmd);
 			yieldRequires.Add((CallCmd)cmd); 
-		} else SynErr(139);
+		} else SynErr(140);
 		Expect(10);
 	}
 
 	void SpecAsserts(List<AssertCmd> asserts ) {
 		Expr e; Token tok; QKeyValue kv = null; 
-		Expect(47);
+		Expect(48);
 		tok = t; 
 		while (la.kind == 26) {
 			Attribute(ref kv);
@@ -1252,18 +1258,18 @@ void SpecAsserts(List<AssertCmd> asserts ) {
 	}
 
 	void SpecYieldPrePost(ref ActionDeclRef refinedAction, List<Requires> pre, List<Ensures> post, List<CallCmd> yieldRequires, List<CallCmd> yieldEnsures, List<CallCmd> yieldPreserves, List<IdentifierExpr> mods) {
-		if (la.kind == 40) {
+		if (la.kind == 41) {
 			SpecRefinedAction(ref refinedAction);
 			Expect(10);
-		} else if (la.kind == 48) {
-			SpecYieldRequires(pre, yieldRequires);
 		} else if (la.kind == 49) {
-			SpecYieldEnsures(post, yieldEnsures);
+			SpecYieldRequires(pre, yieldRequires);
 		} else if (la.kind == 50) {
+			SpecYieldEnsures(post, yieldEnsures);
+		} else if (la.kind == 51) {
 			SpecYieldPreserves(yieldPreserves);
-		} else if (la.kind == 53) {
+		} else if (la.kind == 54) {
 			SpecModifies(mods);
-		} else SynErr(140);
+		} else SynErr(141);
 	}
 
 	void CallCmd(out Cmd c) {
@@ -1273,15 +1279,15 @@ void CallCmd(out Cmd c) {
 		bool isFree = false;
 		c = null;
 		
-		if (la.kind == 37) {
+		if (la.kind == 38) {
 			Get();
 			isAsync = true; 
 		}
-		if (la.kind == 52) {
+		if (la.kind == 53) {
 			Get();
 			isFree = true; 
 		}
-		Expect(70);
+		Expect(71);
 		x = t; 
 		CallParams(isAsync, isFree, x, out c);
 		
@@ -1289,7 +1295,7 @@ void CallCmd(out Cmd c) {
 
 	void SpecYieldEnsures(List<Ensures> post, List<CallCmd> yieldEnsures ) {
 		Expr e; Cmd cmd; Token tok; QKeyValue kv = null; 
-		Expect(49);
+		Expect(50);
 		tok = t; 
 		if (StartOf(16)) {
 			while (la.kind == 26) {
@@ -1297,16 +1303,16 @@ void SpecYieldEnsures(List<Ensures> post, List<CallCmd> yieldEnsures ) {
 			}
 			Proposition(out e);
 			post.Add(new Ensures(tok, false, e, null, kv)); 
-		} else if (la.kind == 37 || la.kind == 52 || la.kind == 70) {
+		} else if (la.kind == 38 || la.kind == 53 || la.kind == 71) {
 			CallCmd(out cmd);
 			yieldEnsures.Add((CallCmd)cmd); 
-		} else SynErr(141);
+		} else SynErr(142);
 		Expect(10);
 	}
 
 	void SpecYieldPreserves(List<CallCmd> yieldPreserves ) {
 		Cmd cmd; Token tok; 
-		Expect(50);
+		Expect(51);
 		tok = t; 
 		CallCmd(out cmd);
 		yieldPreserves.Add((CallCmd)cmd); 
@@ -1326,26 +1332,26 @@ void ProcSignature(bool allowWhereClausesOnFormals, out IToken/*!*/ name, out Li
 			TypeParams(out typeParamTok, out typeParams);
 		}
 		ProcFormals(true, allowWhereClausesOnFormals, out ins);
-		if (la.kind == 29) {
+		if (la.kind == 30) {
 			Get();
 			ProcFormals(false, allowWhereClausesOnFormals, out outs);
 		}
 	}
 
 	void Spec(List<Requires> pre, List<IdentifierExpr> mods, List<Ensures> post) {
-		if (la.kind == 53) {
+		if (la.kind == 54) {
 			SpecModifies(mods);
-		} else if (la.kind == 52) {
+		} else if (la.kind == 53) {
 			Get();
 			SpecPrePost(true, pre, post);
-		} else if (la.kind == 48 || la.kind == 49) {
+		} else if (la.kind == 49 || la.kind == 50) {
 			SpecPrePost(false, pre, post);
-		} else SynErr(142);
+		} else SynErr(143);
 	}
 
 	void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
 		Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; 
-		if (la.kind == 48) {
+		if (la.kind == 49) {
 			Get();
 			tok = t; 
 			while (la.kind == 26) {
@@ -1354,7 +1360,7 @@ void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
 			Proposition(out e);
 			Expect(10);
 			pre.Add(new Requires(tok, free, e, null, kv)); 
-		} else if (la.kind == 49) {
+		} else if (la.kind == 50) {
 			Get();
 			tok = t; 
 			while (la.kind == 26) {
@@ -1363,7 +1369,7 @@ void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
 			Proposition(out e);
 			Expect(10);
 			post.Add(new Ensures(tok, free, e, null, kv)); 
-		} else SynErr(143);
+		} else SynErr(144);
 	}
 
 	void StmtList(out StmtList/*!*/ stmtList) {
@@ -1399,7 +1405,7 @@ void StmtList(out StmtList/*!*/ stmtList) {
 				 cs = new List<Cmd>();
 				}
 				
-			} else if (la.kind == 56 || la.kind == 58 || la.kind == 60) {
+			} else if (la.kind == 57 || la.kind == 59 || la.kind == 61) {
 				StructuredCmd(out ecn);
 				ec = ecn;
 				if (startToken == null) { startToken = ec.tok;  cs = new List<Cmd>(); }
@@ -1444,8 +1450,8 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 		HideRevealCmd.Modes mode;
 		IdentifierExpr hideRevealId = null;
 		
-		if (la.kind == 61 || la.kind == 62) {
-			if (la.kind == 61) {
+		if (la.kind == 62 || la.kind == 63) {
+			if (la.kind == 62) {
 				Get();
 				mode = HideRevealCmd.Modes.Reveal; 
 			} else {
@@ -1455,22 +1461,22 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 			if (la.kind == 1) {
 				Get();
 				hideRevealId = new IdentifierExpr(t, t.val); 
-			} else if (la.kind == 59) {
+			} else if (la.kind == 60) {
 				Get();
-			} else SynErr(144);
+			} else SynErr(145);
 			c = hideRevealId == null ? new HideRevealCmd(t, mode) : new HideRevealCmd(hideRevealId, mode); 
 			Expect(10);
-		} else if (la.kind == 63) {
+		} else if (la.kind == 64) {
 			Get();
 			c = new ChangeScope(t, ChangeScope.Modes.Pop); 
 			Expect(10);
-		} else if (la.kind == 64) {
+		} else if (la.kind == 65) {
 			Get();
 			c = new ChangeScope(t, ChangeScope.Modes.Push); 
 			Expect(10);
 		} else if (StartOf(14)) {
 			LabelOrAssign(out c, out label);
-		} else if (la.kind == 65) {
+		} else if (la.kind == 66) {
 			Get();
 			x = t; 
 			while (la.kind == 26) {
@@ -1479,7 +1485,7 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 			Proposition(out e);
 			c = new AssertCmd(x, e, kv); 
 			Expect(10);
-		} else if (la.kind == 66) {
+		} else if (la.kind == 67) {
 			Get();
 			x = t; 
 			while (la.kind == 26) {
@@ -1488,7 +1494,7 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 			Proposition(out e);
 			c = new AssumeCmd(x, e, kv); 
 			Expect(10);
-		} else if (la.kind == 67) {
+		} else if (la.kind == 68) {
 			Get();
 			x = t; 
 			Idents(out xs);
@@ -1500,30 +1506,30 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 			}
 			c = new HavocCmd(x,ids);
 			
-		} else if (la.kind == 37 || la.kind == 52 || la.kind == 70) {
+		} else if (la.kind == 38 || la.kind == 53 || la.kind == 71) {
 			CallCmd(out cn);
 			Expect(10);
 			c = cn; 
-		} else if (la.kind == 71) {
+		} else if (la.kind == 72) {
 			ParCallCmd(out cn);
 			c = cn; 
-		} else SynErr(145);
+		} else SynErr(146);
 	}
 
 	void StructuredCmd(out StructuredCmd/*!*/ ec) {
 		Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd;  Contract.Assume(cce.IsPeerConsistent(ec));
 		IfCmd/*!*/ ifcmd;  WhileCmd/*!*/ wcmd;  BreakCmd/*!*/ bcmd;
 		
-		if (la.kind == 56) {
+		if (la.kind == 57) {
 			IfCmd(out ifcmd);
 			ec = ifcmd; 
-		} else if (la.kind == 58) {
+		} else if (la.kind == 59) {
 			WhileCmd(out wcmd);
 			ec = wcmd; 
-		} else if (la.kind == 60) {
+		} else if (la.kind == 61) {
 			BreakCmd(out bcmd);
 			ec = bcmd; 
-		} else SynErr(146);
+		} else SynErr(147);
 	}
 
 	void TransferCmd(out TransferCmd/*!*/ tc) {
@@ -1531,7 +1537,7 @@ void TransferCmd(out TransferCmd/*!*/ tc) {
 		Token y;  List<IToken>/*!*/ xs;
 		List<String> ss = new List<String>();
 		
-		if (la.kind == 54) {
+		if (la.kind == 55) {
 			Get();
 			y = t; 
 			Idents(out xs);
@@ -1540,10 +1546,10 @@ void TransferCmd(out TransferCmd/*!*/ tc) {
 			 ss.Add(s.val); }
 			tc = new GotoCmd(y, ss);
 			
-		} else if (la.kind == 55) {
+		} else if (la.kind == 56) {
 			Get();
 			tc = new ReturnCmd(t); 
-		} else SynErr(147);
+		} else SynErr(148);
 		Expect(10);
 	}
 
@@ -1554,21 +1560,21 @@ void IfCmd(out IfCmd/*!*/ ifcmd) {
 		IfCmd/*!*/ elseIf;  IfCmd elseIfOption = null;
 		StmtList/*!*/ els;  StmtList elseOption = null;
 		
-		Expect(56);
+		Expect(57);
 		x = t; 
 		Guard(out guard);
 		Expect(26);
 		StmtList(out thn);
-		if (la.kind == 57) {
+		if (la.kind == 58) {
 			Get();
-			if (la.kind == 56) {
+			if (la.kind == 57) {
 				IfCmd(out elseIf);
 				elseIfOption = elseIf; 
 			} else if (la.kind == 26) {
 				Get();
 				StmtList(out els);
 				elseOption = els; 
-			} else SynErr(148);
+			} else SynErr(149);
 		}
 		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); 
 	}
@@ -1581,17 +1587,17 @@ void WhileCmd(out WhileCmd wcmd) {
 		StmtList body;
 		QKeyValue kv = null;
 		
-		Expect(58);
+		Expect(59);
 		x = t; 
 		Guard(out guard);
 		Contract.Assume(guard == null || cce.Owner.None(guard)); 
-		while (la.kind == 35 || la.kind == 52) {
+		while (la.kind == 36 || la.kind == 53) {
 			isFree = false; z = la/*lookahead token*/; 
-			if (la.kind == 52) {
+			if (la.kind == 53) {
 				Get();
 				isFree = true;  
 			}
-			Expect(35);
+			Expect(36);
 			while (la.kind == 26) {
 				Attribute(ref kv);
 			}
@@ -1604,10 +1610,10 @@ void WhileCmd(out WhileCmd wcmd) {
 				}
 				kv = null;
 				
-			} else if (la.kind == 37 || la.kind == 52 || la.kind == 70) {
+			} else if (la.kind == 38 || la.kind == 53 || la.kind == 71) {
 				CallCmd(out cmd);
 				yields.Add((CallCmd)cmd); 
-			} else SynErr(149);
+			} else SynErr(150);
 			Expect(10);
 		}
 		Expect(26);
@@ -1619,7 +1625,7 @@ void BreakCmd(out BreakCmd/*!*/ bcmd) {
 		Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x;  IToken/*!*/ y;
 		string breakLabel = null;
 		
-		Expect(60);
+		Expect(61);
 		x = t; 
 		if (StartOf(14)) {
 			Ident(out y);
@@ -1632,13 +1638,13 @@ void BreakCmd(out BreakCmd/*!*/ bcmd) {
 	void Guard(out Expr e) {
 		Expr/*!*/ ee;  e = null; 
 		Expect(11);
-		if (la.kind == 59) {
+		if (la.kind == 60) {
 			Get();
 			e = null; 
 		} else if (StartOf(19)) {
 			Expression(out ee);
 			e = ee; 
-		} else SynErr(150);
+		} else SynErr(151);
 		Expect(12);
 	}
 
@@ -1664,7 +1670,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 			Expect(12);
 			lhsExpr = new NAryExpr(x, new FunctionCall(new IdentifierExpr(id, id.val)), ids.Select(id => new IdentifierExpr(id, id.val)).ToList<Expr>());
 			
-			Expect(68);
+			Expect(69);
 			x = t; /* use location of := */ 
 			while (la.kind == 26) {
 				Attribute(ref kv);
@@ -1676,7 +1682,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 		} else if (StartOf(20)) {
 			lhss = new List<AssignLhs/*!*/>(); 
 			lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); 
-			while (la.kind == 19 || la.kind == 69) {
+			while (la.kind == 19 || la.kind == 70) {
 				if (la.kind == 19) {
 					MapAssignIndex(out y, out indexes);
 					lhs = new MapAssignLhs(y, lhs, indexes); 
@@ -1690,7 +1696,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 				Get();
 				Ident(out id);
 				lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); 
-				while (la.kind == 19 || la.kind == 69) {
+				while (la.kind == 19 || la.kind == 70) {
 					if (la.kind == 19) {
 						MapAssignIndex(out y, out indexes);
 						lhs = new MapAssignLhs(y, lhs, indexes); 
@@ -1701,7 +1707,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 				}
 				lhss.Add(lhs); 
 			}
-			Expect(68);
+			Expect(69);
 			x = t; /* use location of := */ 
 			while (la.kind == 26) {
 				Attribute(ref kv);
@@ -1716,7 +1722,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 			}
 			Expect(10);
 			c = new AssignCmd(x, lhss, rhss, kv); 
-		} else SynErr(151);
+		} else SynErr(152);
 	}
 
 	void ParCallCmd(out Cmd d) {
@@ -1725,11 +1731,11 @@ void ParCallCmd(out Cmd d) {
 		Cmd c = null;
 		List<CallCmd> callCmds = new List<CallCmd>();
 		
-		Expect(71);
+		Expect(72);
 		x = t; 
 		CallParams(false, false, x, out c);
 		callCmds.Add((CallCmd)c); 
-		while (la.kind == 72) {
+		while (la.kind == 73) {
 			Get();
 			CallParams(false, false, x, out c);
 			callCmds.Add((CallCmd)c); 
@@ -1758,7 +1764,7 @@ void MapAssignIndex(out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes) {
 
 	void FieldAccess(out IToken x, out FieldAccess fieldAccess) {
 		Contract.Ensures(Contract.ValueAtReturn(out fieldAccess) != null); IToken id; 
-		Expect(69);
+		Expect(70);
 		x = t; 
 		Ident(out id);
 		fieldAccess = new FieldAccess(id, id.val); 
@@ -1790,7 +1796,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
 			}
 			Expect(12);
 			c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; 
-		} else if (la.kind == 14 || la.kind == 68) {
+		} else if (la.kind == 14 || la.kind == 69) {
 			ids.Add(new IdentifierExpr(first, first.val)); 
 			if (la.kind == 14) {
 				Get();
@@ -1802,7 +1808,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
 					ids.Add(new IdentifierExpr(p, p.val)); 
 				}
 			}
-			Expect(68);
+			Expect(69);
 			Ident(out first);
 			Expect(11);
 			if (StartOf(19)) {
@@ -1816,7 +1822,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
 			}
 			Expect(12);
 			c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; 
-		} else SynErr(152);
+		} else SynErr(153);
 	}
 
 	void Expressions(out List<Expr>/*!*/ es) {
@@ -1834,7 +1840,7 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		LogicalExpression(out e0);
 		if (StartOf(21)) {
-			if (la.kind == 75 || la.kind == 76) {
+			if (la.kind == 76 || la.kind == 77) {
 				ImpliesOp();
 				x = t; 
 				ImpliesExpression(true, out e1);
@@ -1846,7 +1852,7 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) {
 				x = t; 
 				LogicalExpression(out e1);
 				e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); 
-				while (la.kind == 77 || la.kind == 78) {
+				while (la.kind == 78 || la.kind == 79) {
 					ExpliesOp();
 					x = t; 
 					LogicalExpression(out e1);
@@ -1857,23 +1863,23 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) {
 	}
 
 	void EquivOp() {
-		if (la.kind == 73) {
+		if (la.kind == 74) {
 			Get();
-		} else if (la.kind == 74) {
+		} else if (la.kind == 75) {
 			Get();
-		} else SynErr(153);
+		} else SynErr(154);
 	}
 
 	void LogicalExpression(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		RelationalExpression(out e0);
 		if (StartOf(22)) {
-			if (la.kind == 79 || la.kind == 80) {
+			if (la.kind == 80 || la.kind == 81) {
 				AndOp();
 				x = t; 
 				RelationalExpression(out e1);
 				e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); 
-				while (la.kind == 79 || la.kind == 80) {
+				while (la.kind == 80 || la.kind == 81) {
 					AndOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1884,7 +1890,7 @@ void LogicalExpression(out Expr/*!*/ e0) {
 				x = t; 
 				RelationalExpression(out e1);
 				e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); 
-				while (la.kind == 81 || la.kind == 82) {
+				while (la.kind == 82 || la.kind == 83) {
 					OrOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1895,19 +1901,19 @@ void LogicalExpression(out Expr/*!*/ e0) {
 	}
 
 	void ImpliesOp() {
-		if (la.kind == 75) {
+		if (la.kind == 76) {
 			Get();
-		} else if (la.kind == 76) {
+		} else if (la.kind == 77) {
 			Get();
-		} else SynErr(154);
+		} else SynErr(155);
 	}
 
 	void ExpliesOp() {
-		if (la.kind == 77) {
+		if (la.kind == 78) {
 			Get();
-		} else if (la.kind == 78) {
+		} else if (la.kind == 79) {
 			Get();
-		} else SynErr(155);
+		} else SynErr(156);
 	}
 
 	void RelationalExpression(out Expr/*!*/ e0) {
@@ -1921,25 +1927,25 @@ void RelationalExpression(out Expr/*!*/ e0) {
 	}
 
 	void AndOp() {
-		if (la.kind == 79) {
+		if (la.kind == 80) {
 			Get();
-		} else if (la.kind == 80) {
+		} else if (la.kind == 81) {
 			Get();
-		} else SynErr(156);
+		} else SynErr(157);
 	}
 
 	void OrOp() {
-		if (la.kind == 81) {
+		if (la.kind == 82) {
 			Get();
-		} else if (la.kind == 82) {
+		} else if (la.kind == 83) {
 			Get();
-		} else SynErr(157);
+		} else SynErr(158);
 	}
 
 	void BvTerm(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		Term(out e0);
-		while (la.kind == 90) {
+		while (la.kind == 91) {
 			Get();
 			x = t; 
 			Term(out e1);
@@ -1950,7 +1956,7 @@ void BvTerm(out Expr/*!*/ e0) {
 	void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
 		switch (la.kind) {
-		case 83: {
+		case 84: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Eq; 
 			break;
@@ -1965,44 +1971,44 @@ void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 			x = t; op=BinaryOperator.Opcode.Gt; 
 			break;
 		}
-		case 84: {
+		case 85: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Le; 
 			break;
 		}
-		case 85: {
+		case 86: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Ge; 
 			break;
 		}
-		case 86: {
+		case 87: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Neq; 
 			break;
 		}
-		case 87: {
+		case 88: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Neq; 
 			break;
 		}
-		case 88: {
+		case 89: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Le; 
 			break;
 		}
-		case 89: {
+		case 90: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Ge; 
 			break;
 		}
-		default: SynErr(158); break;
+		default: SynErr(159); break;
 		}
 	}
 
 	void Term(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; 
 		Factor(out e0);
-		while (la.kind == 91 || la.kind == 92) {
+		while (la.kind == 92 || la.kind == 93) {
 			AddOp(out x, out op);
 			Factor(out e1);
 			e0 = Expr.Binary(x, op, e0, e1); 
@@ -2021,19 +2027,19 @@ void Factor(out Expr/*!*/ e0) {
 
 	void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
-		if (la.kind == 91) {
+		if (la.kind == 92) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Add; 
-		} else if (la.kind == 92) {
+		} else if (la.kind == 93) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Sub; 
-		} else SynErr(159);
+		} else SynErr(160);
 	}
 
 	void Power(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		IsConstructor(out e0);
-		if (la.kind == 96) {
+		if (la.kind == 97) {
 			Get();
 			x = t; 
 			Power(out e1);
@@ -2043,25 +2049,25 @@ void Power(out Expr/*!*/ e0) {
 
 	void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
-		if (la.kind == 59) {
+		if (la.kind == 60) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Mul; 
-		} else if (la.kind == 93) {
+		} else if (la.kind == 94) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Div; 
-		} else if (la.kind == 94) {
+		} else if (la.kind == 95) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Mod; 
-		} else if (la.kind == 95) {
+		} else if (la.kind == 96) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.RealDiv; 
-		} else SynErr(160);
+		} else SynErr(161);
 	}
 
 	void IsConstructor(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x, id; 
 		UnaryExpression(out e0);
-		if (la.kind == 97) {
+		if (la.kind == 98) {
 			Get();
 			x = t; 
 			Ident(out id);
@@ -2075,27 +2081,27 @@ void UnaryExpression(out Expr/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
 		e = dummyExpr;
 		
-		if (la.kind == 92) {
+		if (la.kind == 93) {
 			Get();
 			x = t; 
 			UnaryExpression(out e);
 			e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); 
-		} else if (la.kind == 98 || la.kind == 99) {
+		} else if (la.kind == 99 || la.kind == 100) {
 			NegOp();
 			x = t; 
 			UnaryExpression(out e);
 			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); 
 		} else if (StartOf(25)) {
 			CoercionExpression(out e);
-		} else SynErr(161);
+		} else SynErr(162);
 	}
 
 	void NegOp() {
-		if (la.kind == 98) {
+		if (la.kind == 99) {
 			Get();
-		} else if (la.kind == 99) {
+		} else if (la.kind == 100) {
 			Get();
-		} else SynErr(162);
+		} else SynErr(163);
 	}
 
 	void CoercionExpression(out Expr/*!*/ e) {
@@ -2119,7 +2125,7 @@ void CoercionExpression(out Expr/*!*/ e) {
 				 e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
 				}
 				
-			} else SynErr(163);
+			} else SynErr(164);
 		}
 	}
 
@@ -2131,7 +2137,7 @@ void ArrayExpression(out Expr/*!*/ e) {
 		List<Expr>/*!*/ allArgs = dummyExprSeq;
 		
 		AtomExpression(out e);
-		while (la.kind == 19 || la.kind == 69) {
+		while (la.kind == 19 || la.kind == 70) {
 			if (la.kind == 19) {
 				Get();
 				x = t; allArgs = new List<Expr> ();
@@ -2153,7 +2159,7 @@ void ArrayExpression(out Expr/*!*/ e) {
 							allArgs.Add(e1);
 							
 						}
-						if (la.kind == 68) {
+						if (la.kind == 69) {
 							Get();
 							Expression(out e1);
 							if (bvExtract || e1 is BvBounds)
@@ -2186,12 +2192,12 @@ void ArrayExpression(out Expr/*!*/ e) {
 				} else if (la.kind == 11) {
 					Get();
 					Ident(out id);
-					Expect(68);
+					Expect(69);
 					x = t; 
 					Expression(out e1);
 					Expect(12);
 					e = new NAryExpr(x, new FieldUpdate(id, id.val), new List<Expr> { e, e1 }); 
-				} else SynErr(164);
+				} else SynErr(165);
 			}
 		}
 	}
@@ -2218,18 +2224,18 @@ void AtomExpression(out Expr/*!*/ e) {
 		List<Block/*!*/>/*!*/ blocks;
 		
 		switch (la.kind) {
-		case 100: {
+		case 101: {
 			Get();
 			e = new LiteralExpr(t, false); 
 			break;
 		}
-		case 101: {
+		case 102: {
 			Get();
 			e = new LiteralExpr(t, true); 
 			break;
 		}
-		case 102: case 103: {
-			if (la.kind == 102) {
+		case 103: case 104: {
+			if (la.kind == 103) {
 				Get();
 			} else {
 				Get();
@@ -2237,8 +2243,8 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, RoundingMode.RNE); 
 			break;
 		}
-		case 104: case 105: {
-			if (la.kind == 104) {
+		case 105: case 106: {
+			if (la.kind == 105) {
 				Get();
 			} else {
 				Get();
@@ -2246,8 +2252,8 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, RoundingMode.RNA); 
 			break;
 		}
-		case 106: case 107: {
-			if (la.kind == 106) {
+		case 107: case 108: {
+			if (la.kind == 107) {
 				Get();
 			} else {
 				Get();
@@ -2255,8 +2261,8 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, RoundingMode.RTP); 
 			break;
 		}
-		case 108: case 109: {
-			if (la.kind == 108) {
+		case 109: case 110: {
+			if (la.kind == 109) {
 				Get();
 			} else {
 				Get();
@@ -2264,8 +2270,8 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, RoundingMode.RTN); 
 			break;
 		}
-		case 110: case 111: {
-			if (la.kind == 110) {
+		case 111: case 112: {
+			if (la.kind == 111) {
 				Get();
 			} else {
 				Get();
@@ -2298,7 +2304,7 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, t.val.Trim('"')); 
 			break;
 		}
-		case 1: case 42: case 43: case 44: case 45: case 61: case 62: case 63: case 64: {
+		case 1: case 43: case 44: case 45: case 46: case 62: case 63: case 64: case 65: {
 			Ident(out x);
 			id = new IdentifierExpr(x, x.val);  e = id; 
 			if (la.kind == 11) {
@@ -2308,12 +2314,12 @@ void AtomExpression(out Expr/*!*/ e) {
 					e = new NAryExpr(x, new FunctionCall(id), es); 
 				} else if (la.kind == 12) {
 					e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); 
-				} else SynErr(165);
+				} else SynErr(166);
 				Expect(12);
 			}
 			break;
 		}
-		case 112: {
+		case 113: {
 			Get();
 			x = t; 
 			Expect(11);
@@ -2346,19 +2352,19 @@ void AtomExpression(out Expr/*!*/ e) {
 				Expression(out e);
 				if (e is BvBounds)
 				 this.SemErr("parentheses around bitvector bounds are not allowed"); 
-			} else if (la.kind == 116 || la.kind == 117) {
+			} else if (la.kind == 117 || la.kind == 118) {
 				Forall();
 				x = t; 
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
 				if (typeParams.Count + ds.Count > 0)
 				 e = new ForallExpr(x, typeParams, ds, kv, trig, e); 
-			} else if (la.kind == 118 || la.kind == 119) {
+			} else if (la.kind == 119 || la.kind == 120) {
 				Exists();
 				x = t; 
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
 				if (typeParams.Count + ds.Count > 0)
 				 e = new ExistsExpr(x, typeParams, ds, kv, trig, e); 
-			} else if (la.kind == 120 || la.kind == 121) {
+			} else if (la.kind == 121 || la.kind == 122) {
 				Lambda();
 				x = t; 
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
@@ -2368,20 +2374,20 @@ void AtomExpression(out Expr/*!*/ e) {
 				 e = new LambdaExpr(x, typeParams, ds, kv, e); 
 			} else if (la.kind == 9) {
 				LetExpr(out e);
-			} else SynErr(166);
+			} else SynErr(167);
 			Expect(12);
 			break;
 		}
-		case 56: {
+		case 57: {
 			IfThenElseExpression(out e);
 			break;
 		}
-		case 113: {
+		case 114: {
 			CodeExpression(out locals, out blocks);
 			e = new CodeExpr(locals, blocks); 
 			break;
 		}
-		default: SynErr(167); break;
+		default: SynErr(168); break;
 		}
 	}
 
@@ -2393,7 +2399,7 @@ void Dec(out BigDec n) {
 		} else if (la.kind == 6) {
 			Get();
 			s = t.val; 
-		} else SynErr(168);
+		} else SynErr(169);
 		try {
 		 n = BigDec.FromString(s);
 		} catch (FormatException) {
@@ -2433,11 +2439,11 @@ void BvLit(out BigNum n, out int m) {
 	}
 
 	void Forall() {
-		if (la.kind == 116) {
+		if (la.kind == 117) {
 			Get();
-		} else if (la.kind == 117) {
+		} else if (la.kind == 118) {
 			Get();
-		} else SynErr(169);
+		} else SynErr(170);
 	}
 
 	void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,
@@ -2455,7 +2461,7 @@ void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out L
 			}
 		} else if (StartOf(12)) {
 			BoundVars(out ds);
-		} else SynErr(170);
+		} else SynErr(171);
 		QSep();
 		while (la.kind == 26) {
 			AttributeOrTrigger(ref kv, ref trig);
@@ -2464,19 +2470,19 @@ void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out L
 	}
 
 	void Exists() {
-		if (la.kind == 118) {
+		if (la.kind == 119) {
 			Get();
-		} else if (la.kind == 119) {
+		} else if (la.kind == 120) {
 			Get();
-		} else SynErr(171);
+		} else SynErr(172);
 	}
 
 	void Lambda() {
-		if (la.kind == 120) {
+		if (la.kind == 121) {
 			Get();
-		} else if (la.kind == 121) {
+		} else if (la.kind == 122) {
 			Get();
-		} else SynErr(172);
+		} else SynErr(173);
 	}
 
 	void LetExpr(out Expr/*!*/ letexpr) {
@@ -2497,7 +2503,7 @@ void LetExpr(out Expr/*!*/ letexpr) {
 			LetVar(out v);
 			ds.Add(v); 
 		}
-		Expect(68);
+		Expect(69);
 		Expression(out e0);
 		rhss.Add(e0); 
 		while (la.kind == 14) {
@@ -2518,12 +2524,12 @@ void IfThenElseExpression(out Expr/*!*/ e) {
 		IToken/*!*/ tok;
 		Expr/*!*/ e0, e1, e2;
 		e = dummyExpr; 
-		Expect(56);
+		Expect(57);
 		tok = t; 
 		Expression(out e0);
-		Expect(115);
+		Expect(116);
 		Expression(out e1);
-		Expect(57);
+		Expect(58);
 		Expression(out e2);
 		e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>{ e0, e1, e2 }); 
 	}
@@ -2532,7 +2538,7 @@ void CodeExpression(out List<Variable>/*!*/ locals, out List<Block/*!*/>/*!*/ bl
 		Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List<Variable>(); Block/*!*/ b;
 		blocks = new List<Block/*!*/>();
 		
-		Expect(113);
+		Expect(114);
 		while (la.kind == 9) {
 			LocalVars(locals);
 		}
@@ -2542,7 +2548,7 @@ void CodeExpression(out List<Variable>/*!*/ locals, out List<Block/*!*/>/*!*/ bl
 			SpecBlock(out b);
 			blocks.Add(b); 
 		}
-		Expect(114);
+		Expect(115);
 	}
 
 	void SpecBlock(out Block/*!*/ b) {
@@ -2566,7 +2572,7 @@ void SpecBlock(out Block/*!*/ b) {
 			}
 			
 		}
-		if (la.kind == 54) {
+		if (la.kind == 55) {
 			Get();
 			y = t; 
 			Idents(out xs);
@@ -2575,11 +2581,11 @@ void SpecBlock(out Block/*!*/ b) {
 			 ss.Add(s.val); }
 			b = new Block(x,x.val,cs,new GotoCmd(y,ss));
 			
-		} else if (la.kind == 55) {
+		} else if (la.kind == 56) {
 			Get();
 			Expression(out e);
 			b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); 
-		} else SynErr(173);
+		} else SynErr(174);
 		Expect(10);
 	}
 
@@ -2636,7 +2642,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
 			 trig.AddLast(new Trigger(tok, true, es, null));
 			}
 			
-		} else SynErr(174);
+		} else SynErr(175);
 		Expect(27);
 	}
 
@@ -2651,15 +2657,15 @@ void AttributeParameter(out object/*!*/ o) {
 		} else if (StartOf(19)) {
 			Expression(out e);
 			o = e; 
-		} else SynErr(175);
+		} else SynErr(176);
 	}
 
 	void QSep() {
-		if (la.kind == 122) {
+		if (la.kind == 123) {
 			Get();
-		} else if (la.kind == 123) {
+		} else if (la.kind == 124) {
 			Get();
-		} else SynErr(176);
+		} else SynErr(177);
 	}
 
 	void LetVar(out Variable/*!*/ v) {
@@ -2688,33 +2694,33 @@ public void Parse() {
 	}
 
 	static readonly bool[,]/*!*/ set = {
-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_T, _x,_x,_x,_x, _T,_x,_T,_T, _T,_x,_T,_x, _T,_T,_T,_x, _x,_x,_T,_T, _T,_T,_T,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_T,_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,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_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, _T,_x,_x,_x, _x,_x,_x,_x, _T,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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,_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,_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,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_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,_T,_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,_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,_T, _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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_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,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_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,_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,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_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, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_T, _T,_T,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _T,_x,_T,_x, _T,_T,_T,_T, _T,_T,_T,_T, _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,_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,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _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,_T,_T,_T, _T,_T,_T,_T, _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, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_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, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _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,_T,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_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,_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,_T,_T,_T, _T,_T,_T,_T, _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, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_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, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
-		{_x,_T,_T,_T, _T,_T,_T,_T, _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, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _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, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_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, _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,_T, _x,_x,_x,_x, _T,_T,_x,_T, _T,_T,_x,_T, _x,_T,_T,_T, _x,_x,_x,_T, _T,_T,_T,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_T,_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,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_x,_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,_T,_x,_x, _x,_x,_x,_x, _x,_T,_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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_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,_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,_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,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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, _T,_T,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_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,_T,_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,_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,_T, _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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_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,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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, _T,_T,_T,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_T,_x,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_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,_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,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_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,_T,_T,_T, _T,_T,_T,_T, _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, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_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,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_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,_T,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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,_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,_T,_T,_T, _T,_T,_T,_T, _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, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_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,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
+		{_x,_T,_T,_T, _T,_T,_T,_T, _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, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_T, _T,_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,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}
 
 	};
 } // end Parser
@@ -2767,155 +2773,156 @@ string GetSyntaxErrorString(int n) {
 			case 25: s = "\"uses\" expected"; break;
 			case 26: s = "\"{\" expected"; break;
 			case 27: s = "\"}\" expected"; break;
-			case 28: s = "\"function\" expected"; break;
-			case 29: s = "\"returns\" expected"; break;
-			case 30: s = "\"hideable\" expected"; break;
-			case 31: s = "\"axiom\" expected"; break;
-			case 32: s = "\"type\" expected"; break;
-			case 33: s = "\"=\" expected"; break;
-			case 34: s = "\"datatype\" expected"; break;
-			case 35: s = "\"invariant\" expected"; break;
-			case 36: s = "\"pure\" expected"; break;
-			case 37: s = "\"async\" expected"; break;
-			case 38: s = "\"action\" expected"; break;
-			case 39: s = "\"creates\" expected"; break;
-			case 40: s = "\"refines\" expected"; break;
-			case 41: s = "\"using\" expected"; break;
-			case 42: s = "\"left\" expected"; break;
-			case 43: s = "\"right\" expected"; break;
-			case 44: s = "\"both\" expected"; break;
-			case 45: s = "\"atomic\" expected"; break;
-			case 46: s = "\"procedure\" expected"; break;
-			case 47: s = "\"asserts\" expected"; break;
-			case 48: s = "\"requires\" expected"; break;
-			case 49: s = "\"ensures\" expected"; break;
-			case 50: s = "\"preserves\" expected"; break;
-			case 51: s = "\"implementation\" expected"; break;
-			case 52: s = "\"free\" expected"; break;
-			case 53: s = "\"modifies\" expected"; break;
-			case 54: s = "\"goto\" expected"; break;
-			case 55: s = "\"return\" expected"; break;
-			case 56: s = "\"if\" expected"; break;
-			case 57: s = "\"else\" expected"; break;
-			case 58: s = "\"while\" expected"; break;
-			case 59: s = "\"*\" expected"; break;
-			case 60: s = "\"break\" expected"; break;
-			case 61: s = "\"reveal\" expected"; break;
-			case 62: s = "\"hide\" expected"; break;
-			case 63: s = "\"pop\" expected"; break;
-			case 64: s = "\"push\" expected"; break;
-			case 65: s = "\"assert\" expected"; break;
-			case 66: s = "\"assume\" expected"; break;
-			case 67: s = "\"havoc\" expected"; break;
-			case 68: s = "\":=\" expected"; break;
-			case 69: s = "\"->\" expected"; break;
-			case 70: s = "\"call\" expected"; break;
-			case 71: s = "\"par\" expected"; break;
-			case 72: s = "\"|\" expected"; break;
-			case 73: s = "\"<==>\" expected"; break;
-			case 74: s = "\"\\u21d4\" expected"; break;
-			case 75: s = "\"==>\" expected"; break;
-			case 76: s = "\"\\u21d2\" expected"; break;
-			case 77: s = "\"<==\" expected"; break;
-			case 78: s = "\"\\u21d0\" expected"; break;
-			case 79: s = "\"&&\" expected"; break;
-			case 80: s = "\"\\u2227\" expected"; break;
-			case 81: s = "\"||\" expected"; break;
-			case 82: s = "\"\\u2228\" expected"; break;
-			case 83: s = "\"==\" expected"; break;
-			case 84: s = "\"<=\" expected"; break;
-			case 85: s = "\">=\" expected"; break;
-			case 86: s = "\"!=\" expected"; break;
-			case 87: s = "\"\\u2260\" expected"; break;
-			case 88: s = "\"\\u2264\" expected"; break;
-			case 89: s = "\"\\u2265\" expected"; break;
-			case 90: s = "\"++\" expected"; break;
-			case 91: s = "\"+\" expected"; break;
-			case 92: s = "\"-\" expected"; break;
-			case 93: s = "\"div\" expected"; break;
-			case 94: s = "\"mod\" expected"; break;
-			case 95: s = "\"/\" expected"; break;
-			case 96: s = "\"**\" expected"; break;
-			case 97: s = "\"is\" expected"; break;
-			case 98: s = "\"!\" expected"; break;
-			case 99: s = "\"\\u00ac\" expected"; break;
-			case 100: s = "\"false\" expected"; break;
-			case 101: s = "\"true\" expected"; break;
-			case 102: s = "\"roundNearestTiesToEven\" expected"; break;
-			case 103: s = "\"RNE\" expected"; break;
-			case 104: s = "\"roundNearestTiesToAway\" expected"; break;
-			case 105: s = "\"RNA\" expected"; break;
-			case 106: s = "\"roundTowardPositive\" expected"; break;
-			case 107: s = "\"RTP\" expected"; break;
-			case 108: s = "\"roundTowardNegative\" expected"; break;
-			case 109: s = "\"RTN\" expected"; break;
-			case 110: s = "\"roundTowardZero\" expected"; break;
-			case 111: s = "\"RTZ\" expected"; break;
-			case 112: s = "\"old\" expected"; break;
-			case 113: s = "\"|{\" expected"; break;
-			case 114: s = "\"}|\" expected"; break;
-			case 115: s = "\"then\" expected"; break;
-			case 116: s = "\"forall\" expected"; break;
-			case 117: s = "\"\\u2200\" expected"; break;
-			case 118: s = "\"exists\" expected"; break;
-			case 119: s = "\"\\u2203\" expected"; break;
-			case 120: s = "\"lambda\" expected"; break;
-			case 121: s = "\"\\u03bb\" expected"; break;
-			case 122: s = "\"::\" expected"; break;
-			case 123: s = "\"\\u2022\" expected"; break;
-			case 124: s = "??? expected"; break;
-			case 125: s = "invalid BoogiePL"; break;
+			case 28: s = "\"revealed\" expected"; break;
+			case 29: s = "\"function\" expected"; break;
+			case 30: s = "\"returns\" expected"; break;
+			case 31: s = "\"hideable\" expected"; break;
+			case 32: s = "\"axiom\" expected"; break;
+			case 33: s = "\"type\" expected"; break;
+			case 34: s = "\"=\" expected"; break;
+			case 35: s = "\"datatype\" expected"; break;
+			case 36: s = "\"invariant\" expected"; break;
+			case 37: s = "\"pure\" expected"; break;
+			case 38: s = "\"async\" expected"; break;
+			case 39: s = "\"action\" expected"; break;
+			case 40: s = "\"creates\" expected"; break;
+			case 41: s = "\"refines\" expected"; break;
+			case 42: s = "\"using\" expected"; break;
+			case 43: s = "\"left\" expected"; break;
+			case 44: s = "\"right\" expected"; break;
+			case 45: s = "\"both\" expected"; break;
+			case 46: s = "\"atomic\" expected"; break;
+			case 47: s = "\"procedure\" expected"; break;
+			case 48: s = "\"asserts\" expected"; break;
+			case 49: s = "\"requires\" expected"; break;
+			case 50: s = "\"ensures\" expected"; break;
+			case 51: s = "\"preserves\" expected"; break;
+			case 52: s = "\"implementation\" expected"; break;
+			case 53: s = "\"free\" expected"; break;
+			case 54: s = "\"modifies\" expected"; break;
+			case 55: s = "\"goto\" expected"; break;
+			case 56: s = "\"return\" expected"; break;
+			case 57: s = "\"if\" expected"; break;
+			case 58: s = "\"else\" expected"; break;
+			case 59: s = "\"while\" expected"; break;
+			case 60: s = "\"*\" expected"; break;
+			case 61: s = "\"break\" expected"; break;
+			case 62: s = "\"reveal\" expected"; break;
+			case 63: s = "\"hide\" expected"; break;
+			case 64: s = "\"pop\" expected"; break;
+			case 65: s = "\"push\" expected"; break;
+			case 66: s = "\"assert\" expected"; break;
+			case 67: s = "\"assume\" expected"; break;
+			case 68: s = "\"havoc\" expected"; break;
+			case 69: s = "\":=\" expected"; break;
+			case 70: s = "\"->\" expected"; break;
+			case 71: s = "\"call\" expected"; break;
+			case 72: s = "\"par\" expected"; break;
+			case 73: s = "\"|\" expected"; break;
+			case 74: s = "\"<==>\" expected"; break;
+			case 75: s = "\"\\u21d4\" expected"; break;
+			case 76: s = "\"==>\" expected"; break;
+			case 77: s = "\"\\u21d2\" expected"; break;
+			case 78: s = "\"<==\" expected"; break;
+			case 79: s = "\"\\u21d0\" expected"; break;
+			case 80: s = "\"&&\" expected"; break;
+			case 81: s = "\"\\u2227\" expected"; break;
+			case 82: s = "\"||\" expected"; break;
+			case 83: s = "\"\\u2228\" expected"; break;
+			case 84: s = "\"==\" expected"; break;
+			case 85: s = "\"<=\" expected"; break;
+			case 86: s = "\">=\" expected"; break;
+			case 87: s = "\"!=\" expected"; break;
+			case 88: s = "\"\\u2260\" expected"; break;
+			case 89: s = "\"\\u2264\" expected"; break;
+			case 90: s = "\"\\u2265\" expected"; break;
+			case 91: s = "\"++\" expected"; break;
+			case 92: s = "\"+\" expected"; break;
+			case 93: s = "\"-\" expected"; break;
+			case 94: s = "\"div\" expected"; break;
+			case 95: s = "\"mod\" expected"; break;
+			case 96: s = "\"/\" expected"; break;
+			case 97: s = "\"**\" expected"; break;
+			case 98: s = "\"is\" expected"; break;
+			case 99: s = "\"!\" expected"; break;
+			case 100: s = "\"\\u00ac\" expected"; break;
+			case 101: s = "\"false\" expected"; break;
+			case 102: s = "\"true\" expected"; break;
+			case 103: s = "\"roundNearestTiesToEven\" expected"; break;
+			case 104: s = "\"RNE\" expected"; break;
+			case 105: s = "\"roundNearestTiesToAway\" expected"; break;
+			case 106: s = "\"RNA\" expected"; break;
+			case 107: s = "\"roundTowardPositive\" expected"; break;
+			case 108: s = "\"RTP\" expected"; break;
+			case 109: s = "\"roundTowardNegative\" expected"; break;
+			case 110: s = "\"RTN\" expected"; break;
+			case 111: s = "\"roundTowardZero\" expected"; break;
+			case 112: s = "\"RTZ\" expected"; break;
+			case 113: s = "\"old\" expected"; break;
+			case 114: s = "\"|{\" expected"; break;
+			case 115: s = "\"}|\" expected"; break;
+			case 116: s = "\"then\" expected"; break;
+			case 117: s = "\"forall\" expected"; break;
+			case 118: s = "\"\\u2200\" expected"; break;
+			case 119: s = "\"exists\" expected"; break;
+			case 120: s = "\"\\u2203\" expected"; break;
+			case 121: s = "\"lambda\" expected"; break;
+			case 122: s = "\"\\u03bb\" expected"; break;
+			case 123: s = "\"::\" expected"; break;
+			case 124: s = "\"\\u2022\" expected"; break;
+			case 125: s = "??? expected"; break;
 			case 126: s = "invalid BoogiePL"; break;
-			case 127: s = "invalid Consts"; break;
-			case 128: s = "invalid Function"; break;
+			case 127: s = "invalid BoogiePL"; break;
+			case 128: s = "invalid Consts"; break;
 			case 129: s = "invalid Function"; break;
-			case 130: s = "invalid YieldProcedureDecl"; break;
-			case 131: s = "invalid Procedure"; break;
-			case 132: s = "invalid ActionDecl"; break;
-			case 133: s = "invalid Type"; break;
-			case 134: s = "invalid TypeAtom"; break;
-			case 135: s = "invalid Ident"; break;
-			case 136: s = "invalid TypeArgs"; break;
-			case 137: s = "invalid MoverQualifier"; break;
-			case 138: s = "invalid SpecAction"; break;
-			case 139: s = "invalid SpecYieldRequires"; break;
-			case 140: s = "invalid SpecYieldPrePost"; break;
-			case 141: s = "invalid SpecYieldEnsures"; break;
-			case 142: s = "invalid Spec"; break;
-			case 143: s = "invalid SpecPrePost"; break;
-			case 144: s = "invalid LabelOrCmd"; break;
+			case 130: s = "invalid Function"; break;
+			case 131: s = "invalid YieldProcedureDecl"; break;
+			case 132: s = "invalid Procedure"; break;
+			case 133: s = "invalid ActionDecl"; break;
+			case 134: s = "invalid Type"; break;
+			case 135: s = "invalid TypeAtom"; break;
+			case 136: s = "invalid Ident"; break;
+			case 137: s = "invalid TypeArgs"; break;
+			case 138: s = "invalid MoverQualifier"; break;
+			case 139: s = "invalid SpecAction"; break;
+			case 140: s = "invalid SpecYieldRequires"; break;
+			case 141: s = "invalid SpecYieldPrePost"; break;
+			case 142: s = "invalid SpecYieldEnsures"; break;
+			case 143: s = "invalid Spec"; break;
+			case 144: s = "invalid SpecPrePost"; break;
 			case 145: s = "invalid LabelOrCmd"; break;
-			case 146: s = "invalid StructuredCmd"; break;
-			case 147: s = "invalid TransferCmd"; break;
-			case 148: s = "invalid IfCmd"; break;
-			case 149: s = "invalid WhileCmd"; break;
-			case 150: s = "invalid Guard"; break;
-			case 151: s = "invalid LabelOrAssign"; break;
-			case 152: s = "invalid CallParams"; break;
-			case 153: s = "invalid EquivOp"; break;
-			case 154: s = "invalid ImpliesOp"; break;
-			case 155: s = "invalid ExpliesOp"; break;
-			case 156: s = "invalid AndOp"; break;
-			case 157: s = "invalid OrOp"; break;
-			case 158: s = "invalid RelOp"; break;
-			case 159: s = "invalid AddOp"; break;
-			case 160: s = "invalid MulOp"; break;
-			case 161: s = "invalid UnaryExpression"; break;
-			case 162: s = "invalid NegOp"; break;
-			case 163: s = "invalid CoercionExpression"; break;
-			case 164: s = "invalid ArrayExpression"; break;
-			case 165: s = "invalid AtomExpression"; break;
+			case 146: s = "invalid LabelOrCmd"; break;
+			case 147: s = "invalid StructuredCmd"; break;
+			case 148: s = "invalid TransferCmd"; break;
+			case 149: s = "invalid IfCmd"; break;
+			case 150: s = "invalid WhileCmd"; break;
+			case 151: s = "invalid Guard"; break;
+			case 152: s = "invalid LabelOrAssign"; break;
+			case 153: s = "invalid CallParams"; break;
+			case 154: s = "invalid EquivOp"; break;
+			case 155: s = "invalid ImpliesOp"; break;
+			case 156: s = "invalid ExpliesOp"; break;
+			case 157: s = "invalid AndOp"; break;
+			case 158: s = "invalid OrOp"; break;
+			case 159: s = "invalid RelOp"; break;
+			case 160: s = "invalid AddOp"; break;
+			case 161: s = "invalid MulOp"; break;
+			case 162: s = "invalid UnaryExpression"; break;
+			case 163: s = "invalid NegOp"; break;
+			case 164: s = "invalid CoercionExpression"; break;
+			case 165: s = "invalid ArrayExpression"; break;
 			case 166: s = "invalid AtomExpression"; break;
 			case 167: s = "invalid AtomExpression"; break;
-			case 168: s = "invalid Dec"; break;
-			case 169: s = "invalid Forall"; break;
-			case 170: s = "invalid QuantifierBody"; break;
-			case 171: s = "invalid Exists"; break;
-			case 172: s = "invalid Lambda"; break;
-			case 173: s = "invalid SpecBlock"; break;
-			case 174: s = "invalid AttributeOrTrigger"; break;
-			case 175: s = "invalid AttributeParameter"; break;
-			case 176: s = "invalid QSep"; break;
+			case 168: s = "invalid AtomExpression"; break;
+			case 169: s = "invalid Dec"; break;
+			case 170: s = "invalid Forall"; break;
+			case 171: s = "invalid QuantifierBody"; break;
+			case 172: s = "invalid Exists"; break;
+			case 173: s = "invalid Lambda"; break;
+			case 174: s = "invalid SpecBlock"; break;
+			case 175: s = "invalid AttributeOrTrigger"; break;
+			case 176: s = "invalid AttributeParameter"; break;
+			case 177: s = "invalid QSep"; break;
 
 			default: s = "error " + n; break;
 		}
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index 6bd51d22a..97b05c8ab 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -220,8 +220,8 @@ public override int Read() {
 public class Scanner {
 	const char EOL = '\n';
 	const int eofSym = 0; /* pdt */
-	const int maxT = 124;
-	const int noSym = 124;
+	const int maxT = 125;
+	const int noSym = 125;
 
 
 	[ContractInvariantMethod]
@@ -522,66 +522,67 @@ void CheckLiteral() {
 			case "const": t.kind = 23; break;
 			case "unique": t.kind = 24; break;
 			case "uses": t.kind = 25; break;
-			case "function": t.kind = 28; break;
-			case "returns": t.kind = 29; break;
-			case "hideable": t.kind = 30; break;
-			case "axiom": t.kind = 31; break;
-			case "type": t.kind = 32; break;
-			case "datatype": t.kind = 34; break;
-			case "invariant": t.kind = 35; break;
-			case "pure": t.kind = 36; break;
-			case "async": t.kind = 37; break;
-			case "action": t.kind = 38; break;
-			case "creates": t.kind = 39; break;
-			case "refines": t.kind = 40; break;
-			case "using": t.kind = 41; break;
-			case "left": t.kind = 42; break;
-			case "right": t.kind = 43; break;
-			case "both": t.kind = 44; break;
-			case "atomic": t.kind = 45; break;
-			case "procedure": t.kind = 46; break;
-			case "asserts": t.kind = 47; break;
-			case "requires": t.kind = 48; break;
-			case "ensures": t.kind = 49; break;
-			case "preserves": t.kind = 50; break;
-			case "implementation": t.kind = 51; break;
-			case "free": t.kind = 52; break;
-			case "modifies": t.kind = 53; break;
-			case "goto": t.kind = 54; break;
-			case "return": t.kind = 55; break;
-			case "if": t.kind = 56; break;
-			case "else": t.kind = 57; break;
-			case "while": t.kind = 58; break;
-			case "break": t.kind = 60; break;
-			case "reveal": t.kind = 61; break;
-			case "hide": t.kind = 62; break;
-			case "pop": t.kind = 63; break;
-			case "push": t.kind = 64; break;
-			case "assert": t.kind = 65; break;
-			case "assume": t.kind = 66; break;
-			case "havoc": t.kind = 67; break;
-			case "call": t.kind = 70; break;
-			case "par": t.kind = 71; break;
-			case "div": t.kind = 93; break;
-			case "mod": t.kind = 94; break;
-			case "is": t.kind = 97; break;
-			case "false": t.kind = 100; break;
-			case "true": t.kind = 101; break;
-			case "roundNearestTiesToEven": t.kind = 102; break;
-			case "RNE": t.kind = 103; break;
-			case "roundNearestTiesToAway": t.kind = 104; break;
-			case "RNA": t.kind = 105; break;
-			case "roundTowardPositive": t.kind = 106; break;
-			case "RTP": t.kind = 107; break;
-			case "roundTowardNegative": t.kind = 108; break;
-			case "RTN": t.kind = 109; break;
-			case "roundTowardZero": t.kind = 110; break;
-			case "RTZ": t.kind = 111; break;
-			case "old": t.kind = 112; break;
-			case "then": t.kind = 115; break;
-			case "forall": t.kind = 116; break;
-			case "exists": t.kind = 118; break;
-			case "lambda": t.kind = 120; break;
+			case "revealed": t.kind = 28; break;
+			case "function": t.kind = 29; break;
+			case "returns": t.kind = 30; break;
+			case "hideable": t.kind = 31; break;
+			case "axiom": t.kind = 32; break;
+			case "type": t.kind = 33; break;
+			case "datatype": t.kind = 35; break;
+			case "invariant": t.kind = 36; break;
+			case "pure": t.kind = 37; break;
+			case "async": t.kind = 38; break;
+			case "action": t.kind = 39; break;
+			case "creates": t.kind = 40; break;
+			case "refines": t.kind = 41; break;
+			case "using": t.kind = 42; break;
+			case "left": t.kind = 43; break;
+			case "right": t.kind = 44; break;
+			case "both": t.kind = 45; break;
+			case "atomic": t.kind = 46; break;
+			case "procedure": t.kind = 47; break;
+			case "asserts": t.kind = 48; break;
+			case "requires": t.kind = 49; break;
+			case "ensures": t.kind = 50; break;
+			case "preserves": t.kind = 51; break;
+			case "implementation": t.kind = 52; break;
+			case "free": t.kind = 53; break;
+			case "modifies": t.kind = 54; break;
+			case "goto": t.kind = 55; break;
+			case "return": t.kind = 56; break;
+			case "if": t.kind = 57; break;
+			case "else": t.kind = 58; break;
+			case "while": t.kind = 59; break;
+			case "break": t.kind = 61; break;
+			case "reveal": t.kind = 62; break;
+			case "hide": t.kind = 63; break;
+			case "pop": t.kind = 64; break;
+			case "push": t.kind = 65; break;
+			case "assert": t.kind = 66; break;
+			case "assume": t.kind = 67; break;
+			case "havoc": t.kind = 68; break;
+			case "call": t.kind = 71; break;
+			case "par": t.kind = 72; break;
+			case "div": t.kind = 94; break;
+			case "mod": t.kind = 95; break;
+			case "is": t.kind = 98; break;
+			case "false": t.kind = 101; break;
+			case "true": t.kind = 102; break;
+			case "roundNearestTiesToEven": t.kind = 103; break;
+			case "RNE": t.kind = 104; break;
+			case "roundNearestTiesToAway": t.kind = 105; break;
+			case "RNA": t.kind = 106; break;
+			case "roundTowardPositive": t.kind = 107; break;
+			case "RTP": t.kind = 108; break;
+			case "roundTowardNegative": t.kind = 109; break;
+			case "RTN": t.kind = 110; break;
+			case "roundTowardZero": t.kind = 111; break;
+			case "RTZ": t.kind = 112; break;
+			case "old": t.kind = 113; break;
+			case "then": t.kind = 116; break;
+			case "forall": t.kind = 117; break;
+			case "exists": t.kind = 119; break;
+			case "lambda": t.kind = 121; break;
 			default: break;
 		}
 	}
@@ -865,67 +866,67 @@ void CheckLiteral() {
 			case 67:
 				{t.kind = 26; break;}
 			case 68:
-				{t.kind = 68; break;}
-			case 69:
 				{t.kind = 69; break;}
+			case 69:
+				{t.kind = 70; break;}
 			case 70:
-				{t.kind = 73; break;}
-			case 71:
 				{t.kind = 74; break;}
-			case 72:
+			case 71:
 				{t.kind = 75; break;}
-			case 73:
+			case 72:
 				{t.kind = 76; break;}
+			case 73:
+				{t.kind = 77; break;}
 			case 74:
-				{t.kind = 78; break;}
+				{t.kind = 79; break;}
 			case 75:
 				if (ch == '&') {AddCh(); goto case 76;}
 				else {goto case 0;}
 			case 76:
-				{t.kind = 79; break;}
-			case 77:
 				{t.kind = 80; break;}
-			case 78:
+			case 77:
 				{t.kind = 81; break;}
-			case 79:
+			case 78:
 				{t.kind = 82; break;}
+			case 79:
+				{t.kind = 83; break;}
 			case 80:
-				{t.kind = 85; break;}
-			case 81:
 				{t.kind = 86; break;}
-			case 82:
+			case 81:
 				{t.kind = 87; break;}
-			case 83:
+			case 82:
 				{t.kind = 88; break;}
-			case 84:
+			case 83:
 				{t.kind = 89; break;}
-			case 85:
+			case 84:
 				{t.kind = 90; break;}
+			case 85:
+				{t.kind = 91; break;}
 			case 86:
-				{t.kind = 95; break;}
-			case 87:
 				{t.kind = 96; break;}
+			case 87:
+				{t.kind = 97; break;}
 			case 88:
-				{t.kind = 99; break;}
+				{t.kind = 100; break;}
 			case 89:
-				{t.kind = 113; break;}
-			case 90:
 				{t.kind = 114; break;}
+			case 90:
+				{t.kind = 115; break;}
 			case 91:
-				{t.kind = 117; break;}
+				{t.kind = 118; break;}
 			case 92:
-				{t.kind = 119; break;}
+				{t.kind = 120; break;}
 			case 93:
-				{t.kind = 121; break;}
-			case 94:
 				{t.kind = 122; break;}
-			case 95:
+			case 94:
 				{t.kind = 123; break;}
+			case 95:
+				{t.kind = 124; break;}
 			case 96:
-				recEnd = pos; recKind = 92;
+				recEnd = pos; recKind = 93;
 				if (ch == '0') {AddCh(); goto case 16;}
 				else if (ch == '>') {AddCh(); goto case 69;}
-				else {t.kind = 92; break;}
+				else {t.kind = 93; break;}
 			case 97:
 				recEnd = pos; recKind = 13;
 				if (ch == '=') {AddCh(); goto case 68;}
@@ -944,38 +945,38 @@ void CheckLiteral() {
 				if (ch == '|') {AddCh(); goto case 90;}
 				else {t.kind = 27; break;}
 			case 101:
-				recEnd = pos; recKind = 33;
+				recEnd = pos; recKind = 34;
 				if (ch == '=') {AddCh(); goto case 107;}
-				else {t.kind = 33; break;}
+				else {t.kind = 34; break;}
 			case 102:
-				recEnd = pos; recKind = 59;
+				recEnd = pos; recKind = 60;
 				if (ch == '*') {AddCh(); goto case 87;}
-				else {t.kind = 59; break;}
+				else {t.kind = 60; break;}
 			case 103:
-				recEnd = pos; recKind = 72;
+				recEnd = pos; recKind = 73;
 				if (ch == '|') {AddCh(); goto case 78;}
 				else if (ch == '{') {AddCh(); goto case 89;}
-				else {t.kind = 72; break;}
+				else {t.kind = 73; break;}
 			case 104:
-				recEnd = pos; recKind = 98;
+				recEnd = pos; recKind = 99;
 				if (ch == '=') {AddCh(); goto case 81;}
-				else {t.kind = 98; break;}
+				else {t.kind = 99; break;}
 			case 105:
-				recEnd = pos; recKind = 91;
+				recEnd = pos; recKind = 92;
 				if (ch == '+') {AddCh(); goto case 85;}
-				else {t.kind = 91; break;}
+				else {t.kind = 92; break;}
 			case 106:
-				recEnd = pos; recKind = 84;
+				recEnd = pos; recKind = 85;
 				if (ch == '=') {AddCh(); goto case 108;}
-				else {t.kind = 84; break;}
+				else {t.kind = 85; break;}
 			case 107:
-				recEnd = pos; recKind = 83;
+				recEnd = pos; recKind = 84;
 				if (ch == '>') {AddCh(); goto case 72;}
-				else {t.kind = 83; break;}
+				else {t.kind = 84; break;}
 			case 108:
-				recEnd = pos; recKind = 77;
+				recEnd = pos; recKind = 78;
 				if (ch == '>') {AddCh(); goto case 70;}
-				else {t.kind = 77; break;}
+				else {t.kind = 78; break;}
 
 		}
 		t.val = new String(tval, 0, tlen);
diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
index d6377e52c..d81beeac1 100644
--- a/Source/Directory.Build.props
+++ b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.2.4</Version>
+    <Version>3.2.5</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>
diff --git a/Source/VCGeneration/LoopExtractor.cs b/Source/VCGeneration/LoopExtractor.cs
index be25d0ae5..5966f7498 100644
--- a/Source/VCGeneration/LoopExtractor.cs
+++ b/Source/VCGeneration/LoopExtractor.cs
@@ -160,7 +160,7 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G
           foreach (Cmd /*!*/ cmd in block.Cmds)
           {
             Contract.Assert(cmd != null);
-            cmd.AddAssignedVariables(targets);
+            targets.AddRange(cmd.GetAssignedVariables());
 
             VariableCollector c = new VariableCollector();
             c.Visit(cmd);
diff --git a/Source/VCGeneration/Prune/Pruner.cs b/Source/VCGeneration/Prune/Pruner.cs
index 969054063..165eb5239 100644
--- a/Source/VCGeneration/Prune/Pruner.cs
+++ b/Source/VCGeneration/Prune/Pruner.cs
@@ -77,8 +77,7 @@ public static IEnumerable<Declaration> GetLiveDeclarations(VCGenOptions options,
       return program.TopLevelDeclarations.Where(d => 
         d is not Constant && d is not Axiom && d is not Function || reachableDeclarations.Contains(d));
 
-      bool TraverseDeclaration(object parent, object child)
-      {
+      bool TraverseDeclaration(object parent, object child) {
         return parent is not Function function || child is not Axiom axiom || revealedState.IsRevealed(function)
                || !axiom.CanHide;
       }
diff --git a/Source/VCGeneration/Prune/RevealedAnalysis.cs b/Source/VCGeneration/Prune/RevealedAnalysis.cs
index 59adfe6a0..5e671b9ba 100644
--- a/Source/VCGeneration/Prune/RevealedAnalysis.cs
+++ b/Source/VCGeneration/Prune/RevealedAnalysis.cs
@@ -9,7 +9,7 @@ namespace VCGeneration.Prune;
 
 record RevealedState(HideRevealCmd.Modes Mode, IImmutableSet<Function> Offset) {
   public bool IsRevealed(Function function) {
-    return (Mode == HideRevealCmd.Modes.Hide) == Offset.Contains(function);
+    return (Mode == HideRevealCmd.Modes.Hide) == Offset.Contains(function) || function.AlwaysRevealed;
   }
 
   public static readonly RevealedState AllRevealed = new(HideRevealCmd.Modes.Reveal, ImmutableHashSet<Function>.Empty);
diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs
index d9f14c4c7..c8bf280c3 100644
--- a/Source/VCGeneration/VerificationConditionGenerator.cs
+++ b/Source/VCGeneration/VerificationConditionGenerator.cs
@@ -973,16 +973,16 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary<Block, List<
     public static List<Variable> VarsAssignedInLoop(Graph<Block> g, Block header)
     {
       List<Variable> varsToHavoc = new List<Variable>();
-      foreach (Block backEdgeNode in cce.NonNull(g.BackEdgeNodes(header)))
+      foreach (var backEdgeNode in cce.NonNull(g.BackEdgeNodes(header)))
       {
         Contract.Assert(backEdgeNode != null);
         foreach (Block b in g.NaturalLoops(header, backEdgeNode))
         {
           Contract.Assert(b != null);
-          foreach (Cmd c in b.Cmds)
+          foreach (var c in b.Cmds)
           {
             Contract.Assert(c != null);
-            c.AddAssignedVariables(varsToHavoc);
+            varsToHavoc.AddRange(c.GetAssignedVariables());
           }
         }
       }
diff --git a/Test/pruning/Reveal.bpl b/Test/pruning/Reveal.bpl
index 1a2284226..ae9f1893a 100644
--- a/Test/pruning/Reveal.bpl
+++ b/Test/pruning/Reveal.bpl
@@ -57,4 +57,13 @@ procedure HideSpecific() {
   hide inner;
   reveal inner;
   assert inner(3) == 42;
+}
+
+revealed function alwaysRevealed(x: int): int uses {
+  hideable axiom (forall x: int :: {alwaysRevealed(x)} alwaysRevealed(x) == 42);
+}
+
+procedure AlwaysRevealed() {
+  hide *;
+  assert alwaysRevealed(3) == 42;
 }
\ No newline at end of file
diff --git a/Test/pruning/Reveal.bpl.expect b/Test/pruning/Reveal.bpl.expect
index dc4452ef0..9fb3cf217 100644
--- a/Test/pruning/Reveal.bpl.expect
+++ b/Test/pruning/Reveal.bpl.expect
@@ -3,4 +3,4 @@ Reveal.bpl(29,7): Error: this assertion could not be proved
 Reveal.bpl(31,7): Error: this assertion could not be proved
 Reveal.bpl(42,3): Error: this assertion could not be proved
 
-Boogie program verifier finished with 2 verified, 4 errors
+Boogie program verifier finished with 3 verified, 4 errors