Boogie: Added boolean code expressions (sans well-formedness checks on the input).

9 files changed, 843 insertions, 902 deletions

diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc
index fbc2d253..22d21f0c 100644
--- a/Source/Core/Absy.ssc
+++ b/Source/Core/Absy.ssc
@@ -881,7 +881,7 @@ namespace Microsoft.Boogie
           p.Parent.Emit(stream);

         }

         if (ChildrenComplete)

-          stream.Write(this, level, " complete");
+          stream.Write(this, level, " complete");

       }

       

       stream.WriteLine(";");

@@ -1119,7 +1119,7 @@ namespace Microsoft.Boogie
     // Register all type parameters at the resolution context

     protected void RegisterTypeParameters(ResolutionContext! rc) {

       foreach (TypeVariable! v in TypeParameters)

-        rc.AddTypeBinder(v);
+        rc.AddTypeBinder(v);

     }

 

     protected void SortTypeParams() {

@@ -1812,7 +1812,7 @@ namespace Microsoft.Boogie
           v.ResolveWhere(rc);

         }

 

-        rc.StartProcedureContext();

+        rc.PushProcedureContext();

         foreach (Block b in Blocks) 

         {

           b.Register(rc);

@@ -1827,7 +1827,7 @@ namespace Microsoft.Boogie
         }

         rc.StateMode = ResolutionContext.State.Single;

       

-        rc.EndProcedureContext();

+        rc.PopProcedureContext();

         rc.PopVarContext();

 

         Type.CheckBoundVariableOccurrences(TypeParameters,

diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc
index b24e83e3..7aa3e1fc 100644
--- a/Source/Core/AbsyCmd.ssc
+++ b/Source/Core/AbsyCmd.ssc
@@ -1467,7 +1467,7 @@ namespace Microsoft.Boogie
       int previousTypeBinderState = rc.TypeBinderState;

       try {

         foreach (TypeVariable! v in Proc.TypeParameters)

-          rc.AddTypeBinder(v);
+          rc.AddTypeBinder(v);

         Type.CheckBoundVariableOccurrences(Proc.TypeParameters,

                                            formalInTypes, formalOutTypes,

                                            this.tok, "types of given arguments",

@@ -1578,7 +1578,7 @@ namespace Microsoft.Boogie
       // cins   : new variables created just for this call, one per ains

       // cframe : new variables created just for this call, to keep track of OLD values

       // couts  : new variables created just for this call, one per aouts

-      // WildcarVars : new variables created just for this call, one per null in ains

+      // WildcardVars : new variables created just for this call, one per null in ains

       

       #region Create cins; each one is an incarnation of the corresponding in parameter

       VariableSeq! cins = new VariableSeq();

diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc
index 5947c822..250820ed 100644
--- a/Source/Core/AbsyExpr.ssc
+++ b/Source/Core/AbsyExpr.ssc
@@ -81,19 +81,19 @@ namespace Microsoft.Boogie
 

     // Handy syntactic sugar follows:

 

-    public static NAryExpr! Binary (IToken! x, BinaryOperator.Opcode op, Expr! e1, Expr! e2) 

+    public static NAryExpr! Unary (IToken! x, UnaryOperator.Opcode op, Expr! e1) 

     {

-      return new NAryExpr(x, new BinaryOperator(x, op), new ExprSeq(e1, e2));

+      return new NAryExpr(x, new UnaryOperator(x, op), new ExprSeq(e1));

     }

 

-    public static NAryExpr! Unary (IToken! x, UnaryOperator.Opcode op, Expr! e1) 

+    public static NAryExpr! Binary (IToken! x, BinaryOperator.Opcode op, Expr! e0, Expr! e1) 

     {

-      return new NAryExpr(x, new UnaryOperator(x, op), new ExprSeq(e1));

+      return new NAryExpr(x, new BinaryOperator(x, op), new ExprSeq(e0, e1));

     }

 

-    public static NAryExpr! Binary (BinaryOperator.Opcode op, Expr! e1, Expr! e2) 

+    public static NAryExpr! Binary (BinaryOperator.Opcode op, Expr! e0, Expr! e1) 

     {

-      return new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, op), new ExprSeq(e1, e2));

+      return Binary(Token.NoToken, op, e0, e1);

     }

 

     public static NAryExpr! Eq (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Eq, e1, e2); }

@@ -115,7 +115,7 @@ namespace Microsoft.Boogie
       else { return Binary(BinaryOperator.Opcode.Or, e1, e2); }

     }

     public static Expr! Not (Expr! e1) {

-        NAryExpr nary = e1 as NAryExpr;
+        NAryExpr nary = e1 as NAryExpr;

         

         if (e1 == true_) { return false_; }

         else if (e1 == false_) { return true_; }

@@ -480,7 +480,7 @@ namespace Microsoft.Boogie
     public override bool Equals(object obj)

     {

       BvConst other = obj as BvConst;

-      if (other == null) return false;
+      if (other == null) return false;

 

       return Bits == other.Bits && Value == other.Value;

     }

@@ -1375,8 +1375,8 @@ namespace Microsoft.Boogie
         case Opcode.Imp: if (e1 is bool && e2 is bool) { return ! (bool)e1 || (bool)e2; } break;

         case Opcode.Iff: if (e1 is bool && e2 is bool) { return e1 == e2; } break;

 

-        case Opcode.Eq: return Equals(e1,e2);
-        case Opcode.Neq: return ! Equals(e1,e2);
+        case Opcode.Eq: return Equals(e1,e2);

+        case Opcode.Neq: return ! Equals(e1,e2);

 

         case Opcode.Subtype: throw new System.NotImplementedException();

       }

@@ -1942,7 +1942,7 @@ namespace Microsoft.Boogie
         return null;

       }

       

-      return ((!)args[0]).Type;
+      return ((!)args[0]).Type;

     }

 

     public Type Typecheck(ref ExprSeq! args,

@@ -2071,25 +2071,22 @@ namespace Microsoft.Boogie
   

 

 

-  public class BlockExpr : Expr

+  public class CodeExpr : Expr, AI.IUnknown

   {

     public VariableSeq! LocVars;

     [Rep]

-    public BlockSeq! Blocks;

-    public BlockExpr(VariableSeq! localVariables, BlockSeq! blocks)

+    public List<Block!>! Blocks;

+    public CodeExpr(VariableSeq! localVariables, List<Block!>! blocks)

       : base(Token.NoToken)

+      requires 0 < blocks.Count;

     {

       LocVars = localVariables;

       Blocks = blocks;

     }

-    public override AI.IExpr! IExpr {

-        get {

-          // An BlockExpr has no AI.IExpr representation

-          assert false;

-          throw new System.Exception(); // make compiler shut up

-          return Expr.False;

-        }

-    }

+

+    public override AI.IExpr! IExpr { get { return this; } }

+    [Pure] public object DoVisit(AI.ExprVisitor! visitor) { return this; }

+    

     public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {

       // Treat a BlockEexpr as if it has no free variables at all

     }

@@ -2097,7 +2094,7 @@ namespace Microsoft.Boogie
     {

       //level++;

       int level = 0;

-      stream.WriteLine(level, "{0}", '{');

+      stream.WriteLine(level, "|{");

 

       if (this.LocVars.Length > 0) 

       {

@@ -2112,7 +2109,7 @@ namespace Microsoft.Boogie
       }

 

       stream.WriteLine();

-      stream.WriteLine(level, "{0}", '}');

+      stream.WriteLine(level, "}|");

 

       stream.WriteLine();

       stream.WriteLine();

@@ -2128,7 +2125,7 @@ namespace Microsoft.Boogie
         v.Resolve(rc);

       }

 

-      rc.StartProcedureContext();

+      rc.PushProcedureContext();

       foreach (Block! b in Blocks) 

       {

         b.Register(rc);

@@ -2139,7 +2136,7 @@ namespace Microsoft.Boogie
         b.Resolve(rc);

       }

       

-      rc.EndProcedureContext();

+      rc.PopProcedureContext();

       rc.PopVarContext();

     }

 

@@ -2160,7 +2157,7 @@ namespace Microsoft.Boogie
 

     public override Absy! StdDispatch(StandardVisitor! visitor)

     {

-      return visitor.VisitBlockExpr(this);

+      return visitor.VisitCodeExpr(this);

     }

   }

 

@@ -2272,7 +2269,7 @@ namespace Microsoft.Boogie
     }

     public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args)

     {

-      AI.IFunApp! retFun;
+      AI.IFunApp! retFun;

     

       if(args.Count == 3)

       {      

@@ -2403,7 +2400,7 @@ namespace Microsoft.Boogie
     }

     public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args)

     {

-      AI.IFunApp! retFun;
+      AI.IFunApp! retFun;

     

       if(args.Count == 2)

       {      

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 42f9f735..fe302acb 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -38,7 +38,6 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines,
 

 

   FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);

-//  Scanner scanner = new Scanner(stream);

   

   if (defines == null) {

     defines = new List<string!>();

@@ -49,9 +48,6 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines,
   Errors errors = new Errors();

   Scanner scanner = new Scanner(ms, errors, filename);

 

-/*  

-  Scanner scanner = new Scanner(filename);

-*/

   Parser parser = new Parser(scanner, errors);

   Pgm = new Program(); // reset the global variable

     parser.Parse();

@@ -65,48 +61,7 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines,
       program = null;

       return parser.errors.count;

     }

-/*

-  using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

-    Buffer.Fill(reader);

-    Scanner.Init(filename);

-    return Parse(out program);

-  }

-*/

-}

-

-///<summary>

-///Returns the number of parsing errors encountered.  If 0, "program" returns as

-///the parsed program.

-///Note: first initialize the Scanner.

-///</summary>

-//public static int Parse (out /*maybe null*/ Program program) {

-//  Pgm = new Program(); // reset the global variable

-//    Parse();

-//    if (Errors.count == 0)

-//    {

-//      program = Pgm;

-//      return 0;

-//    }

-//    else

-//    {

-//      program = null;

-//      return Errors.count;

-//    }

-//}

-

-/*

-public static int ParseProposition (string! text, out Expr! expression)

-{

-  Buffer.Fill(text);

-  Scanner.Init(string.Format("\"{0}\"", text));

-

-  Errors.SynErr = new ErrorProc(SynErr);

-  la = new Token();

-  Get();

-  Proposition(out expression);

-  return Errors.count;

 }

-*/

 

 // Class to represent the bounds of a bitvector expression t[a:b].

 // Objects of this class only exist during parsing and are directly

@@ -639,60 +594,13 @@ SpecPrePost<bool free, RequiresSeq! pre, EnsuresSeq! post>
 = (. Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null; .)

   ( "requires"              (. tok = t; .)

     { Attribute<ref kv> }

-    (Proposition<out e> ";"  (. pre.Add(new Requires(tok, free, e, null, kv)); .)

-    |

-     SpecBody<out locals, out blocks> ";"

-                            (. pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv)); .)

-    )

+    Proposition<out e> ";"  (. pre.Add(new Requires(tok, free, e, null, kv)); .)

   | "ensures"               (. tok = t; .)

     { Attribute<ref kv> }

-    (Proposition<out e> ";"  (. post.Add(new Ensures(tok, free, e, null, kv)); .)

-    |

-     SpecBody<out locals, out blocks> ";"

-                            (. post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv)); .)

-    )

+    Proposition<out e> ";"  (. post.Add(new Ensures(tok, free, e, null, kv)); .)

   )

   .

 

-SpecBody<out VariableSeq! locals, out BlockSeq! blocks>

-= (. locals = new VariableSeq(); Block! b; .)

-  "{{"

-  { LocalVars<locals> }

-  SpecBlock<out b>          (. blocks = new BlockSeq(b); .)

-  { SpecBlock<out b>        (. blocks.Add(b); .)

-  }

-  "}}"

-  .

-

-SpecBlock<out Block! b>

-= (. IToken! x; IToken! y;

-     Cmd c;  IToken label;

-     CmdSeq cs = new CmdSeq();

-     TokenSeq! xs;

-     StringSeq ss = new StringSeq();

-     b = dummyBlock;

-     Expr! e;

-  .)

-  Ident<out x> ":"

-  { LabelOrCmd<out c, out label>

-                       (. if (c != null) {

-                            assert label == null;

-                            cs.Add(c);

-                          } else {

-                            assert label != null;

-                            this.SemErr("SpecBlock's can only have one label");

-                          }

-                       .)

-  }

-  ( "goto"             (. y = t; .)

-    Idents<out xs>     (. foreach (IToken! s in xs) { ss.Add(s.val); }

-                          b = new Block(x,x.val,cs,new GotoCmd(y,ss));

-                       .)

-  | "return" Expression<out e>

-                       (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .)

-  ) ";"

-  .

-

 /*------------------------------------------------------------------------*/

 

 ImplBody<out VariableSeq! locals, out StmtList! stmtList>

@@ -891,21 +799,29 @@ LabelOrCmd<out Cmd c, out IToken label>
 

 LabelOrAssign<out Cmd c, out IToken label>

 /* ensures (c == null) != (label != null) */

-= (. IToken! id; IToken! x; Expr! e, e0;

+= (. IToken! id; IToken! x, y; Expr! e, e0;

      c = dummyCmd;  label = null;

      AssignLhs! lhs;

      List<AssignLhs!>! lhss;

      List<Expr!>! rhss;

+     List<Expr!>! indexes;

   .)

   Ident<out id>              (. x = t; .)

   ( ":"                      (. c = null;  label = x; .)

-  | 

-    MapAssignIndexes<id, out lhs>    (. lhss = new List<AssignLhs!> ();

-                                        lhss.Add(lhs); .)

+

+  | (. lhss = new List<AssignLhs!>(); .)

+    (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)

+

+    { MapAssignIndex<out y, out indexes>    (. lhs = new MapAssignLhs(y, lhs, indexes); .) }

+    (. lhss.Add(lhs); .)

+

     { ","

       Ident<out id>

-      MapAssignIndexes<id, out lhs>  (. lhss.Add(lhs); .)

+      (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)

+      { MapAssignIndex<out y, out indexes>    (. lhs = new MapAssignLhs(y, lhs, indexes); .) }

+      (. lhss.Add(lhs); .)

     }

+

     ":="                     (. x = t; /* use location of := */ .)

     Expression<out e0>       (. rhss = new List<Expr!> ();

                                 rhss.Add(e0); .)

@@ -916,27 +832,18 @@ LabelOrAssign<out Cmd c, out IToken label>
   )

   .

 

-MapAssignIndexes<IToken! assignedVariable, out AssignLhs! lhs>

-= (. IToken! x;

-     AssignLhs! runningLhs =

-       new SimpleAssignLhs(assignedVariable,

-                           new IdentifierExpr(assignedVariable, assignedVariable.val));

-     List<Expr!>! indexes;

-     Expr! e0;

+MapAssignIndex<.out IToken! x, out List<Expr!>! indexes.>

+= (. indexes = new List<Expr!> ();

+     Expr! e;

   .)

-  {

-    "["                        (. x = t;

-                                  indexes = new List<Expr!> (); .)

-      [

-        Expression<out e0>     (. indexes.Add(e0); .)

-        { ","

-          Expression<out e0>   (. indexes.Add(e0); .)

-        }

-      ]     

-    "]"                        (. runningLhs =

-                                    new MapAssignLhs (x, runningLhs, indexes);  .)

-  }

-                               (. lhs = runningLhs; .)

+  "["                        (. x = t; .)

+    [

+      Expression<out e>      (. indexes.Add(e); .)

+      { ","

+        Expression<out e>    (. indexes.Add(e); .)

+      }

+    ]

+  "]"

   .

 

 /*------------------------------------------------------------------------*/

@@ -1296,6 +1203,8 @@ AtomExpression<out Expr! e>
      Bpl.Type! ty;

      QKeyValue kv;

      e = dummyExpr;

+     VariableSeq! locals;

+     List<Block!>! blocks;

   .)

   ( "false"           (. e = new LiteralExpr(t, false); .)

   | "true"            (. e = new LiteralExpr(t, true); .)

@@ -1335,9 +1244,52 @@ AtomExpression<out Expr! e>
         )

     ")"

   | IfThenElseExpression<out e>

+  | CodeExpression<out locals, out blocks> (. e = new CodeExpr(locals, blocks); .)

   )

   .

 

+CodeExpression<.out VariableSeq! locals, out List<Block!>! blocks.>

+= (. locals = new VariableSeq(); Block! b;

+     blocks = new List<Block!>();

+  .)

+  "|{"

+  { LocalVars<locals> }

+  SpecBlock<out b>          (. blocks.Add(b); .)

+  { SpecBlock<out b>        (. blocks.Add(b); .)

+  }

+  "}|"

+  .

+

+SpecBlock<out Block! b>

+= (. IToken! x; IToken! y;

+     Cmd c;  IToken label;

+     CmdSeq cs = new CmdSeq();

+     TokenSeq! xs;

+     StringSeq ss = new StringSeq();

+     b = dummyBlock;

+     Expr! e;

+  .)

+  Ident<out x> ":"

+  { LabelOrCmd<out c, out label>

+                       (. if (c != null) {

+                            assert label == null;

+                            cs.Add(c);

+                          } else {

+                            assert label != null;

+                            SemErr("SpecBlock's can only have one label");

+                          }

+                       .)

+  }

+  ( "goto"             (. y = t; .)

+    Idents<out xs>     (. foreach (IToken! s in xs) { ss.Add(s.val); }

+                          b = new Block(x,x.val,cs,new GotoCmd(y,ss));

+                       .)

+  | "return" Expression<out e>

+                       (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .)

+  )

+  ";"

+  .

+

 Attribute<ref QKeyValue kv>

 = (. Trigger trig = null; .)

   AttributeOrTrigger<ref kv, ref trig> (.  if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); .)

diff --git a/Source/Core/Duplicator.ssc b/Source/Core/Duplicator.ssc
index 667eaf5e..f265ee35 100644
--- a/Source/Core/Duplicator.ssc
+++ b/Source/Core/Duplicator.ssc
@@ -52,9 +52,35 @@ namespace Microsoft.Boogie
     {

       return base.VisitBlock ((Block)node.Clone());

     }

+    public override Expr! VisitCodeExpr(CodeExpr! node)

+    {

+      CodeExpr clone = (CodeExpr)base.VisitCodeExpr((CodeExpr)node.Clone());

+      // Before returning, fix up the resolved goto targets

+      assert node.Blocks.Count == clone.Blocks.Count;

+      Dictionary<Block,Block> subst = new Dictionary<Block,Block>();

+      for (int i = 0; i < node.Blocks.Count; i++) {

+        subst.Add(node.Blocks[i], clone.Blocks[i]);

+      }

+      foreach (Block! b in clone.Blocks) {

+        GotoCmd g = b.TransferCmd as GotoCmd;

+        if (g != null) {

+          BlockSeq targets = new BlockSeq();

+          foreach (Block t in (!)g.labelTargets) {

+            Block nt = subst[t];

+            targets.Add(nt);

+          }

+          g.labelTargets = targets;

+        }

+      }

+      return clone; 

+    }

     public override BlockSeq! VisitBlockSeq(BlockSeq! blockSeq)

     {

-      return base.VisitBlockSeq (blockSeq);

+      return base.VisitBlockSeq (new BlockSeq(blockSeq));

+    }

+    public override List<Block!>! VisitBlockList(List<Block!>! blocks)

+    {

+      return base.VisitBlockList (new List<Block!>(blocks));

     }

     public override BoundVariable! VisitBoundVariable(BoundVariable! node)

     {

@@ -206,6 +232,10 @@ namespace Microsoft.Boogie
     {

       return base.VisitReturnCmd ((ReturnCmd) node.Clone());

     }

+    public override ReturnExprCmd! VisitReturnExprCmd(ReturnExprCmd! node)

+    {

+      return base.VisitReturnExprCmd((ReturnExprCmd)node.Clone());

+    }

     public override Sequential! VisitSequential(Sequential! node)

     {

       return base.VisitSequential ((Sequential) node.Clone());

@@ -245,11 +275,11 @@ namespace Microsoft.Boogie
     }

     public override Cmd! VisitAssertRequiresCmd(AssertRequiresCmd! node)

     {

-      return base.VisitAssertRequiresCmd((AssertRequiresCmd)node.Clone());
+      return base.VisitAssertRequiresCmd((AssertRequiresCmd)node.Clone());

     }

     public override Cmd! VisitAssertEnsuresCmd(AssertEnsuresCmd! node)

     {

-      return base.VisitAssertEnsuresCmd((AssertEnsuresCmd)node.Clone());
+      return base.VisitAssertEnsuresCmd((AssertEnsuresCmd)node.Clone());

     }    

     public override Ensures! VisitEnsures(Ensures! node)

     {

diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc
index 432c5ab2..68148acf 100644
--- a/Source/Core/Parser.ssc
+++ b/Source/Core/Parser.ssc
@@ -57,7 +57,6 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines,
 

 

   FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);

-//  Scanner scanner = new Scanner(stream);

   

   if (defines == null) {

     defines = new List<string!>();

@@ -68,9 +67,6 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines,
   Errors errors = new Errors();

   Scanner scanner = new Scanner(ms, errors, filename);

 

-/*  

-  Scanner scanner = new Scanner(filename);

-*/

   Parser parser = new Parser(scanner, errors);

   Pgm = new Program(); // reset the global variable

     parser.Parse();

@@ -84,49 +80,8 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines,
       program = null;

       return parser.errors.count;

     }

-/*

-  using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

-    Buffer.Fill(reader);

-    Scanner.Init(filename);

-    return Parse(out program);

-  }

-*/

 }

 

-///<summary>

-///Returns the number of parsing errors encountered.  If 0, "program" returns as

-///the parsed program.

-///Note: first initialize the Scanner.

-///</summary>

-//public static int Parse (out /*maybe null*/ Program program) {

-//  Pgm = new Program(); // reset the global variable

-//    Parse();

-//    if (Errors.count == 0)

-//    {

-//      program = Pgm;

-//      return 0;

-//    }

-//    else

-//    {

-//      program = null;

-//      return Errors.count;

-//    }

-//}

-

-/*

-public static int ParseProposition (string! text, out Expr! expression)

-{

-  Buffer.Fill(text);

-  Scanner.Init(string.Format("\"{0}\"", text));

-

-  Errors.SynErr = new ErrorProc(SynErr);

-  la = new Token();

-  Get();

-  Proposition(out expression);

-  return Errors.count;

-}

-*/

-

 // Class to represent the bounds of a bitvector expression t[a:b].

 // Objects of this class only exist during parsing and are directly

 // turned into BvExtract before they get anywhere else

@@ -241,7 +196,7 @@ private class BvBounds : Expr {
 			}

 			case 27: {

 				Axiom(out ax);

-				Pgm.TopLevelDeclarations.Add(ax);
+				Pgm.TopLevelDeclarations.Add(ax); 

 				break;

 			}

 			case 28: {

@@ -267,7 +222,7 @@ private class BvBounds : Expr {
 			}

 			case 31: {

 				Implementation(out nnim);

-				Pgm.TopLevelDeclarations.Add(nnim);
+				Pgm.TopLevelDeclarations.Add(nnim); 

 				break;

 			}

 			}

@@ -280,15 +235,15 @@ private class BvBounds : Expr {
 		ds = new VariableSeq();

 		bool u = false; QKeyValue kv = null;

 		bool ChildrenComplete = false;

-		List<ConstantParent!> Parents = null;
+		List<ConstantParent!> Parents = null; 

 		Expect(19);

-		y = t;
+		y = t; 

 		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

 		if (la.kind == 20) {

 			Get();

-			u = true;
+			u = true;  

 		}

 		IdsType(out xs);

 		if (la.kind == 21) {

@@ -339,11 +294,11 @@ private class BvBounds : Expr {
 		Expect(8);

 		if (StartOf(2)) {

 			VarOrType(out tyd);

-			arguments.Add(new Formal(tyd.tok, tyd, true));
+			arguments.Add(new Formal(tyd.tok, tyd, true)); 

 			while (la.kind == 11) {

 				Get();

 				VarOrType(out tyd);

-				arguments.Add(new Formal(tyd.tok, tyd, true));
+				arguments.Add(new Formal(tyd.tok, tyd, true)); 

 			}

 		}

 		Expect(9);

@@ -352,16 +307,16 @@ private class BvBounds : Expr {
 			Expect(8);

 			VarOrType(out tyd);

 			Expect(9);

-			retTyd = tyd;
+			retTyd = tyd; 

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

 			Get();

 			Type(out retTy);

-			retTyd = new TypedIdent(retTy.tok, "", retTy);
+			retTyd = new TypedIdent(retTy.tok, "", retTy); 

 		} else SynErr(89);

 		if (la.kind == 25) {

 			Get();

 			Expression(out tmp);

-			definition = tmp;
+			definition = tmp; 

 			Expect(26);

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

 			Get();

@@ -440,35 +395,35 @@ private class BvBounds : Expr {
 	}

 

 	void Axiom(out Axiom! m) {

-		Expr! e; QKeyValue kv = null;
+		Expr! e; QKeyValue kv = null; 

 		Expect(27);

 		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

-		IToken! x = t;
+		IToken! x = t; 

 		Proposition(out e);

 		Expect(7);

-		m = new Axiom(x,e, null, kv);
+		m = new Axiom(x,e, null, kv); 

 	}

 

 	void UserDefinedTypes(out List<Declaration!>! ts) {

-		Declaration! decl; QKeyValue kv = null; ts = new List<Declaration!> ();
+		Declaration! decl; QKeyValue kv = null; ts = new List<Declaration!> (); 

 		Expect(28);

 		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

 		UserDefinedType(out decl, kv);

-		ts.Add(decl);
+		ts.Add(decl);  

 		while (la.kind == 11) {

 			Get();

 			UserDefinedType(out decl, kv);

-			ts.Add(decl);
+			ts.Add(decl);  

 		}

 		Expect(7);

 	}

 

 	void GlobalVars(out VariableSeq! ds) {

-		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null;
+		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null; 

 		Expect(6);

 		while (la.kind == 25) {

 			Attribute(ref kv);

@@ -507,10 +462,10 @@ private class BvBounds : Expr {
 			}

 			ImplBody(out locals, out stmtList);

 			impl = new Implementation(x, x.val, typeParams,

-			                         Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
+			                         Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors); 

 			

 		} else SynErr(91);

-		proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
+		proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); 

 	}

 

 	void Implementation(out Implementation! impl) {

@@ -524,13 +479,13 @@ private class BvBounds : Expr {
 		Expect(31);

 		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);
+		impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); 

 	}

 

 	void Attribute(ref QKeyValue kv) {

-		Trigger trig = null;
+		Trigger trig = null; 

 		AttributeOrTrigger(ref kv, ref trig);

-		if (trig != null) this.SemErr("only attributes, not triggers, allowed here");
+		if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); 

 	}

 

 	void IdsTypeWheres(bool allowWhereClauses, TypedIdentSeq! tyds) {

@@ -542,7 +497,7 @@ private class BvBounds : Expr {
 	}

 

 	void LocalVars(VariableSeq! ds) {

-		TypedIdentSeq! tyds = new TypedIdentSeq(); QKeyValue kv = null;
+		TypedIdentSeq! tyds = new TypedIdentSeq(); QKeyValue kv = null; 

 		Expect(6);

 		while (la.kind == 25) {

 			Attribute(ref kv);

@@ -556,7 +511,7 @@ private class BvBounds : Expr {
 	}

 

 	void ProcFormals(bool incoming, bool allowWhereClauses, out VariableSeq! ds) {

-		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq();
+		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); 

 		Expect(8);

 		if (la.kind == 1) {

 			IdsTypeWheres(allowWhereClauses, tyds);

@@ -569,7 +524,7 @@ private class BvBounds : Expr {
 	}

 

 	void BoundVars(IToken! x, out VariableSeq! ds) {

-		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq();
+		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); 

 		IdsTypeWheres(false, tyds);

 		foreach (TypedIdent! tyd in tyds) {

 		 ds.Add(new BoundVariable(tyd.tok, tyd));

@@ -578,7 +533,7 @@ private class BvBounds : Expr {
 	}

 

 	void IdsType(out TypedIdentSeq! tyds) {

-		TokenSeq! ids;  Bpl.Type! ty;
+		TokenSeq! ids;  Bpl.Type! ty; 

 		Idents(out ids);

 		Expect(10);

 		Type(out ty);

@@ -590,34 +545,34 @@ private class BvBounds : Expr {
 	}

 

 	void Idents(out TokenSeq! xs) {

-		IToken! id; xs = new TokenSeq();
+		IToken! id; xs = new TokenSeq(); 

 		Ident(out id);

-		xs.Add(id);
+		xs.Add(id); 

 		while (la.kind == 11) {

 			Get();

 			Ident(out id);

-			xs.Add(id);
+			xs.Add(id); 

 		}

 	}

 

 	void Type(out Bpl.Type! ty) {

-		IToken! tok; ty = dummyType;
+		IToken! tok; ty = dummyType; 

 		if (la.kind == 8 || la.kind == 13 || la.kind == 14) {

 			TypeAtom(out ty);

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

 			Ident(out tok);

-			TypeSeq! args = new TypeSeq ();
+			TypeSeq! args = new TypeSeq (); 

 			if (StartOf(2)) {

 				TypeArgs(args);

 			}

-			ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
+			ty = new UnresolvedTypeIdentifier (tok, tok.val, args); 

 		} else if (la.kind == 15 || la.kind == 17) {

 			MapType(out ty);

 		} else SynErr(92);

 	}

 

 	void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {

-		TokenSeq! ids;  Bpl.Type! ty;  Expr wh = null;  Expr! nne;
+		TokenSeq! ids;  Bpl.Type! ty;  Expr wh = null;  Expr! nne; 

 		Idents(out ids);

 		Expect(10);

 		Type(out ty);

@@ -638,24 +593,24 @@ private class BvBounds : Expr {
 	}

 

 	void Expression(out Expr! e0) {

-		IToken! x; Expr! e1;
+		IToken! x; Expr! e1; 

 		ImpliesExpression(false, out e0);

-		while (la.kind == 52 || la.kind == 53) {

+		while (la.kind == 50 || la.kind == 51) {

 			EquivOp();

-			x = t;
+			x = t; 

 			ImpliesExpression(false, out e1);

-			e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1);
+			e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); 

 		}

 	}

 

 	void TypeAtom(out Bpl.Type! ty) {

-		ty = dummyType;
+		ty = dummyType; 

 		if (la.kind == 13) {

 			Get();

-			ty = new BasicType(t, SimpleType.Int);
+			ty = new BasicType(t, SimpleType.Int); 

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

 			Get();

-			ty = new BasicType(t, SimpleType.Bool);
+			ty = new BasicType(t, SimpleType.Bool); 

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

 			Get();

 			Type(out ty);

@@ -672,23 +627,23 @@ private class BvBounds : Expr {
 	}

 

 	void TypeArgs(TypeSeq! ts) {

-		IToken! tok; Type! ty;
+		IToken! tok; Type! ty; 

 		if (la.kind == 8 || la.kind == 13 || la.kind == 14) {

 			TypeAtom(out ty);

-			ts.Add(ty);
+			ts.Add(ty); 

 			if (StartOf(2)) {

 				TypeArgs(ts);

 			}

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

 			Ident(out tok);

 			TypeSeq! args = new TypeSeq ();

-			ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args));
+			ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); 

 			if (StartOf(2)) {

 				TypeArgs(ts);

 			}

 		} else if (la.kind == 15 || la.kind == 17) {

 			MapType(out ty);

-			ts.Add(ty);
+			ts.Add(ty); 

 		} else SynErr(94);

 	}

 

@@ -701,10 +656,10 @@ private class BvBounds : Expr {
 		

 		if (la.kind == 17) {

 			TypeParams(out nnTok, out typeParameters);

-			tok = nnTok;
+			tok = nnTok; 

 		}

 		Expect(15);

-		if (tok == null) tok = t;
+		if (tok == null) tok = t;  

 		if (StartOf(2)) {

 			Types(arguments);

 		}

@@ -715,9 +670,9 @@ private class BvBounds : Expr {
 	}

 

 	void TypeParams(out IToken! tok, out Bpl.TypeVariableSeq! typeParams) {

-		TokenSeq! typeParamToks;
+		TokenSeq! typeParamToks; 

 		Expect(17);

-		tok = t;
+		tok = t;  

 		Idents(out typeParamToks);

 		Expect(18);

 		typeParams = new TypeVariableSeq ();

@@ -727,13 +682,13 @@ private class BvBounds : Expr {
 	}

 

 	void Types(TypeSeq! ts) {

-		Bpl.Type! ty;
+		Bpl.Type! ty; 

 		Type(out ty);

-		ts.Add(ty);
+		ts.Add(ty); 

 		while (la.kind == 11) {

 			Get();

 			Type(out ty);

-			ts.Add(ty);
+			ts.Add(ty); 

 		}

 	}

 

@@ -741,40 +696,40 @@ private class BvBounds : Expr {
 		ChildrenComplete = false;

 		Parents = null;

 		bool u;

-		IToken! parent;
+		IToken! parent; 

 		Expect(21);

 		Parents = new List<ConstantParent!> ();

-		u = false;
+		u = false; 

 		if (la.kind == 1 || la.kind == 20) {

 			if (la.kind == 20) {

 				Get();

-				u = true;
+				u = true; 

 			}

 			Ident(out parent);

 			Parents.Add(new ConstantParent (

-			           new IdentifierExpr(parent, parent.val), u));
+			           new IdentifierExpr(parent, parent.val), u)); 

 			while (la.kind == 11) {

 				Get();

-				u = false;
+				u = false; 

 				if (la.kind == 20) {

 					Get();

-					u = true;
+					u = true; 

 				}

 				Ident(out parent);

 				Parents.Add(new ConstantParent (

-				           new IdentifierExpr(parent, parent.val), u));
+				           new IdentifierExpr(parent, parent.val), u)); 

 			}

 		}

 		if (la.kind == 22) {

 			Get();

-			ChildrenComplete = true;
+			ChildrenComplete = true; 

 		}

 	}

 

 	void VarOrType(out TypedIdent! tyd) {

-		string! varName = ""; Bpl.Type! ty; IToken! tok;
+		string! varName = ""; Bpl.Type! ty; IToken! tok; 

 		Type(out ty);

-		tok = ty.tok;
+		tok = ty.tok; 

 		if (la.kind == 10) {

 			Get();

 			if (ty is UnresolvedTypeIdentifier &&

@@ -786,7 +741,7 @@ private class BvBounds : Expr {
 			

 			Type(out ty);

 		}

-		tyd = new TypedIdent(tok, varName, ty);
+		tyd = new TypedIdent(tok, varName, ty); 

 	}

 

 	void Proposition(out Expr! e) {

@@ -795,7 +750,7 @@ private class BvBounds : Expr {
 

 	void UserDefinedType(out Declaration! decl, QKeyValue kv) {

 		IToken! id; IToken! id2; TokenSeq! paramTokens = new TokenSeq ();

-		Type! body = dummyType; bool synonym = false;
+		Type! body = dummyType; bool synonym = false; 

 		Ident(out id);

 		if (la.kind == 1) {

 			WhiteSpaceIdents(out paramTokens);

@@ -803,7 +758,7 @@ private class BvBounds : Expr {
 		if (la.kind == 29) {

 			Get();

 			Type(out body);

-			synonym = true;
+			synonym = true; 

 		}

 		if (synonym) {

 		 TypeVariableSeq! typeParams = new TypeVariableSeq();

@@ -817,19 +772,19 @@ private class BvBounds : Expr {
 	}

 

 	void WhiteSpaceIdents(out TokenSeq! xs) {

-		IToken! id; xs = new TokenSeq();
+		IToken! id; xs = new TokenSeq(); 

 		Ident(out id);

-		xs.Add(id);
+		xs.Add(id); 

 		while (la.kind == 1) {

 			Ident(out id);

-			xs.Add(id);
+			xs.Add(id); 

 		}

 	}

 

 	void ProcSignature(bool allowWhereClausesOnFormals, out IToken! name, out TypeVariableSeq! typeParams,

 out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {

 		IToken! typeParamTok; typeParams = new TypeVariableSeq();

-		outs = new VariableSeq(); kv = null;
+		outs = new VariableSeq(); kv = null; 

 		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

@@ -845,7 +800,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 	}

 

 	void Spec(RequiresSeq! pre, IdentifierExprSeq! mods, EnsuresSeq! post) {

-		TokenSeq! ms;
+		TokenSeq! ms; 

 		if (la.kind == 32) {

 			Get();

 			if (la.kind == 1) {

@@ -865,7 +820,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 	}

 

 	void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {

-		locals = new VariableSeq();
+		locals = new VariableSeq(); 

 		Expect(25);

 		while (la.kind == 6) {

 			LocalVars(locals);

@@ -874,133 +829,26 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 	}

 

 	void SpecPrePost(bool free, RequiresSeq! pre, EnsuresSeq! post) {

-		Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null;
+		Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null; 

 		if (la.kind == 34) {

 			Get();

-			tok = t;
+			tok = t; 

 			while (la.kind == 25) {

 				Attribute(ref kv);

 			}

-			if (StartOf(5)) {

-				Proposition(out e);

-				Expect(7);

-				pre.Add(new Requires(tok, free, e, null, kv));
-			} else if (la.kind == 36) {

-				SpecBody(out locals, out blocks);

-				Expect(7);

-				pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv));
-			} else SynErr(96);

+			Proposition(out e);

+			Expect(7);

+			pre.Add(new Requires(tok, free, e, null, kv)); 

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

 			Get();

-			tok = t;
-			while (la.kind == 25) {

-				Attribute(ref kv);

-			}

-			if (StartOf(5)) {

-				Proposition(out e);

-				Expect(7);

-				post.Add(new Ensures(tok, free, e, null, kv));
-			} else if (la.kind == 36) {

-				SpecBody(out locals, out blocks);

-				Expect(7);

-				post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv));
-			} else SynErr(97);

-		} else SynErr(98);

-	}

-

-	void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {

-		locals = new VariableSeq(); Block! b;
-		Expect(36);

-		while (la.kind == 6) {

-			LocalVars(locals);

-		}

-		SpecBlock(out b);

-		blocks = new BlockSeq(b);
-		while (la.kind == 1) {

-			SpecBlock(out b);

-			blocks.Add(b);
-		}

-		Expect(37);

-	}

-

-	void SpecBlock(out Block! b) {

-		IToken! x; IToken! y;

-		Cmd c;  IToken label;

-		CmdSeq cs = new CmdSeq();

-		TokenSeq! xs;

-		StringSeq ss = new StringSeq();

-		b = dummyBlock;

-		Expr! e;

-		

-		Ident(out x);

-		Expect(10);

-		while (StartOf(6)) {

-			LabelOrCmd(out c, out label);

-			if (c != null) {

-			 assert label == null;

-			 cs.Add(c);

-			} else {

-			  assert label != null;

-			  this.SemErr("SpecBlock's can only have one label");

-			}

-			

-		}

-		if (la.kind == 38) {

-			Get();

-			y = t;
-			Idents(out xs);

-			foreach (IToken! s in xs) { ss.Add(s.val); }

-			b = new Block(x,x.val,cs,new GotoCmd(y,ss));

-			

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

-			Get();

-			Expression(out e);

-			b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
-		} else SynErr(99);

-		Expect(7);

-	}

-

-	void LabelOrCmd(out Cmd c, out IToken label) {

-		IToken! x; Expr! e;

-		TokenSeq! xs;

-		IdentifierExprSeq ids;

-		c = dummyCmd;  label = null;

-		Cmd! cn;

-		QKeyValue kv = null;

-		

-		if (la.kind == 1) {

-			LabelOrAssign(out c, out label);

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

-			Get();

-			x = t;
+			tok = t; 

 			while (la.kind == 25) {

 				Attribute(ref kv);

 			}

 			Proposition(out e);

-			c = new AssertCmd(x,e, kv);
 			Expect(7);

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

-			Get();

-			x = t;
-			Proposition(out e);

-			c = new AssumeCmd(x,e);
-			Expect(7);

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

-			Get();

-			x = t;
-			Idents(out xs);

-			Expect(7);

-			ids = new IdentifierExprSeq();

-			foreach (IToken! y in xs) {

-			  ids.Add(new IdentifierExpr(y, y.val));

-			}

-			c = new HavocCmd(x,ids);

-			

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

-			CallCmd(out cn);

-			Expect(7);

-			c = cn;
-		} else SynErr(100);

+			post.Add(new Ensures(tok, free, e, null, kv)); 

+		} else SynErr(96);

 	}

 

 	void StmtList(out StmtList! stmtList) {

@@ -1013,7 +861,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		StructuredCmd ec = null;  StructuredCmd! ecn;

 		TransferCmd tc = null;  TransferCmd! tcn;

 		

-		while (StartOf(7)) {

+		while (StartOf(5)) {

 			if (StartOf(6)) {

 				LabelOrCmd(out c, out label);

 				if (c != null) {

@@ -1037,7 +885,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				  cs = new CmdSeq();

 				}

 				

-			} else if (la.kind == 40 || la.kind == 42 || la.kind == 45) {

+			} else if (la.kind == 38 || la.kind == 40 || la.kind == 43) {

 				StructuredCmd(out ecn);

 				ec = ecn;

 				if (startToken == null) { startToken = ec.tok;  cs = new CmdSeq(); }

@@ -1072,20 +920,63 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		  

 	}

 

+	void LabelOrCmd(out Cmd c, out IToken label) {

+		IToken! x; Expr! e;

+		TokenSeq! xs;

+		IdentifierExprSeq ids;

+		c = dummyCmd;  label = null;

+		Cmd! cn;

+		QKeyValue kv = null;

+		

+		if (la.kind == 1) {

+			LabelOrAssign(out c, out label);

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

+			Get();

+			x = t; 

+			while (la.kind == 25) {

+				Attribute(ref kv);

+			}

+			Proposition(out e);

+			c = new AssertCmd(x,e, kv); 

+			Expect(7);

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

+			Get();

+			x = t; 

+			Proposition(out e);

+			c = new AssumeCmd(x,e); 

+			Expect(7);

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

+			Get();

+			x = t; 

+			Idents(out xs);

+			Expect(7);

+			ids = new IdentifierExprSeq();

+			foreach (IToken! y in xs) {

+			  ids.Add(new IdentifierExpr(y, y.val));

+			}

+			c = new HavocCmd(x,ids);

+			

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

+			CallCmd(out cn);

+			Expect(7);

+			c = cn; 

+		} else SynErr(97);

+	}

+

 	void StructuredCmd(out StructuredCmd! ec) {

 		ec = dummyStructuredCmd;  assume ec.IsPeerConsistent;

 		IfCmd! ifcmd;  WhileCmd! wcmd;  BreakCmd! bcmd;

 		

-		if (la.kind == 40) {

+		if (la.kind == 38) {

 			IfCmd(out ifcmd);

-			ec = ifcmd;
-		} else if (la.kind == 42) {

+			ec = ifcmd; 

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

 			WhileCmd(out wcmd);

-			ec = wcmd;
-		} else if (la.kind == 45) {

+			ec = wcmd; 

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

 			BreakCmd(out bcmd);

-			ec = bcmd;
-		} else SynErr(101);

+			ec = bcmd; 

+		} else SynErr(98);

 	}

 

 	void TransferCmd(out TransferCmd! tc) {

@@ -1093,17 +984,17 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		Token y;  TokenSeq! xs;

 		StringSeq ss = new StringSeq();

 		

-		if (la.kind == 38) {

+		if (la.kind == 36) {

 			Get();

-			y = t;
+			y = t; 

 			Idents(out xs);

 			foreach (IToken! s in xs) { ss.Add(s.val); }

 			tc = new GotoCmd(y, ss);

 			

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

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

 			Get();

-			tc = new ReturnCmd(t);
-		} else SynErr(102);

+			tc = new ReturnCmd(t); 

+		} else SynErr(99);

 		Expect(7);

 	}

 

@@ -1114,23 +1005,23 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		IfCmd! elseIf;  IfCmd elseIfOption = null;

 		StmtList! els;  StmtList elseOption = null;

 		

-		Expect(40);

-		x = t;
+		Expect(38);

+		x = t; 

 		Guard(out guard);

 		Expect(25);

 		StmtList(out thn);

-		if (la.kind == 41) {

+		if (la.kind == 39) {

 			Get();

-			if (la.kind == 40) {

+			if (la.kind == 38) {

 				IfCmd(out elseIf);

-				elseIfOption = elseIf;
+				elseIfOption = elseIf; 

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

 				Get();

 				StmtList(out els);

-				elseOption = els;
-			} else SynErr(103);

+				elseOption = els; 

+			} else SynErr(100);

 		}

-		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
+		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); 

 	}

 

 	void WhileCmd(out WhileCmd! wcmd) {

@@ -1139,17 +1030,17 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		List<PredicateCmd!> invariants = new List<PredicateCmd!>();

 		StmtList! body;

 		

-		Expect(42);

-		x = t;
+		Expect(40);

+		x = t; 

 		Guard(out guard);

-		assume guard == null || Owner.None(guard);
-		while (la.kind == 33 || la.kind == 43) {

-			isFree = false; z = la/*lookahead token*/;
+		assume guard == null || Owner.None(guard); 

+		while (la.kind == 33 || la.kind == 41) {

+			isFree = false; z = la/*lookahead token*/; 

 			if (la.kind == 33) {

 				Get();

-				isFree = true;
+				isFree = true;  

 			}

-			Expect(43);

+			Expect(41);

 			Expression(out e);

 			if (isFree) {

 			 invariants.Add(new AssumeCmd(z, e));

@@ -1161,71 +1052,80 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		}

 		Expect(25);

 		StmtList(out body);

-		wcmd = new WhileCmd(x, guard, invariants, body);
+		wcmd = new WhileCmd(x, guard, invariants, body); 

 	}

 

 	void BreakCmd(out BreakCmd! bcmd) {

 		IToken! x;  IToken! y;

 		string breakLabel = null;

 		

-		Expect(45);

-		x = t;
+		Expect(43);

+		x = t; 

 		if (la.kind == 1) {

 			Ident(out y);

-			breakLabel = y.val;
+			breakLabel = y.val; 

 		}

 		Expect(7);

-		bcmd = new BreakCmd(x, breakLabel);
+		bcmd = new BreakCmd(x, breakLabel); 

 	}

 

 	void Guard(out Expr e) {

-		Expr! ee;  e = null;
+		Expr! ee;  e = null; 

 		Expect(8);

-		if (la.kind == 44) {

+		if (la.kind == 42) {

 			Get();

-			e = null;
-		} else if (StartOf(5)) {

+			e = null; 

+		} else if (StartOf(7)) {

 			Expression(out ee);

-			e = ee;
-		} else SynErr(104);

+			e = ee; 

+		} else SynErr(101);

 		Expect(9);

 	}

 

 	void LabelOrAssign(out Cmd c, out IToken label) {

-		IToken! id; IToken! x; Expr! e, e0;

+		IToken! id; IToken! x, y; Expr! e, e0;

 		c = dummyCmd;  label = null;

 		AssignLhs! lhs;

 		List<AssignLhs!>! lhss;

 		List<Expr!>! rhss;

+		List<Expr!>! indexes;

 		

 		Ident(out id);

-		x = t;
+		x = t; 

 		if (la.kind == 10) {

 			Get();

-			c = null;  label = x;
-		} else if (la.kind == 11 || la.kind == 15 || la.kind == 49) {

-			MapAssignIndexes(id, out lhs);

-			lhss = new List<AssignLhs!> ();

-			lhss.Add(lhs);
+			c = null;  label = x; 

+		} else if (la.kind == 11 || la.kind == 15 || la.kind == 47) {

+			lhss = new List<AssignLhs!>(); 

+			lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); 

+			while (la.kind == 15) {

+				MapAssignIndex(out y, out indexes);

+				lhs = new MapAssignLhs(y, lhs, indexes); 

+			}

+			lhss.Add(lhs); 

 			while (la.kind == 11) {

 				Get();

 				Ident(out id);

-				MapAssignIndexes(id, out lhs);

-				lhss.Add(lhs);
+				lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); 

+				while (la.kind == 15) {

+					MapAssignIndex(out y, out indexes);

+					lhs = new MapAssignLhs(y, lhs, indexes); 

+				}

+				lhss.Add(lhs); 

 			}

-			Expect(49);

+			Expect(47);

 			x = t; /* use location of := */ 

 			Expression(out e0);

 			rhss = new List<Expr!> ();

-			rhss.Add(e0);
+			rhss.Add(e0); 

 			while (la.kind == 11) {

 				Get();

 				Expression(out e0);

-				rhss.Add(e0);
+				rhss.Add(e0); 

 			}

 			Expect(7);

-			c = new AssignCmd(x, lhss, rhss);
-		} else SynErr(105);

+			c = new AssignCmd(x, lhss, rhss); 

+		} else SynErr(102);

 	}

 

 	void CallCmd(out Cmd! c) {

@@ -1236,8 +1136,8 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		Expr en;  List<Expr> args;

 		c = dummyCmd;

 		

-		Expect(50);

-		x = t;
+		Expect(48);

+		x = t; 

 		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

@@ -1247,17 +1147,17 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				Get();

 				if (StartOf(8)) {

 					CallForallArg(out en);

-					es.Add(en);
+					es.Add(en); 

 					while (la.kind == 11) {

 						Get();

 						CallForallArg(out en);

-						es.Add(en);
+						es.Add(en); 

 					}

 				}

 				Expect(9);

-				c = new CallCmd(x, first.val, es, ids, kv);
-			} else if (la.kind == 11 || la.kind == 49) {

-				ids.Add(new IdentifierExpr(first, first.val));
+				c = new CallCmd(x, first.val, es, ids, kv); 

+			} else if (la.kind == 11 || la.kind == 47) {

+				ids.Add(new IdentifierExpr(first, first.val)); 

 				if (la.kind == 11) {

 					Get();

 					CallOutIdent(out p);

@@ -1278,40 +1178,40 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 						

 					}

 				}

-				Expect(49);

+				Expect(47);

 				Ident(out first);

 				Expect(8);

 				if (StartOf(8)) {

 					CallForallArg(out en);

-					es.Add(en);
+					es.Add(en); 

 					while (la.kind == 11) {

 						Get();

 						CallForallArg(out en);

-						es.Add(en);
+						es.Add(en); 

 					}

 				}

 				Expect(9);

-				c = new CallCmd(x, first.val, es, ids, kv);
-			} else SynErr(106);

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

+				c = new CallCmd(x, first.val, es, ids, kv); 

+			} else SynErr(103);

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

 			Get();

 			Ident(out first);

 			Expect(8);

-			args = new List<Expr>();
+			args = new List<Expr>(); 

 			if (StartOf(8)) {

 				CallForallArg(out en);

-				args.Add(en);
+				args.Add(en); 

 				while (la.kind == 11) {

 					Get();

 					CallForallArg(out en);

-					args.Add(en);
+					args.Add(en); 

 				}

 			}

 			Expect(9);

-			c = new CallForallCmd(x, first.val, args, kv);
-		} else if (la.kind == 44) {

+			c = new CallForallCmd(x, first.val, args, kv); 

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

 			Get();

-			ids.Add(null);
+			ids.Add(null); 

 			if (la.kind == 11) {

 				Get();

 				CallOutIdent(out p);

@@ -1332,330 +1232,320 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 					

 				}

 			}

-			Expect(49);

+			Expect(47);

 			Ident(out first);

 			Expect(8);

 			if (StartOf(8)) {

 				CallForallArg(out en);

-				es.Add(en);
+				es.Add(en); 

 				while (la.kind == 11) {

 					Get();

 					CallForallArg(out en);

-					es.Add(en);
+					es.Add(en); 

 				}

 			}

 			Expect(9);

-			c = new CallCmd(x, first.val, es, ids, kv);
-		} else SynErr(107);

+			c = new CallCmd(x, first.val, es, ids, kv); 

+		} else SynErr(104);

 	}

 

-	void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) {

-		IToken! x;

-		AssignLhs! runningLhs =

-		  new SimpleAssignLhs(assignedVariable,

-		                      new IdentifierExpr(assignedVariable, assignedVariable.val));

-		List<Expr!>! indexes;

-		Expr! e0;

+	void MapAssignIndex(out IToken! x, out List<Expr!>! indexes) {

+		indexes = new List<Expr!> ();

+		Expr! e;

 		

-		while (la.kind == 15) {

-			Get();

-			x = t;

-			indexes = new List<Expr!> ();
-			if (StartOf(5)) {

-				Expression(out e0);

-				indexes.Add(e0);
-				while (la.kind == 11) {

-					Get();

-					Expression(out e0);

-					indexes.Add(e0);
-				}

+		Expect(15);

+		x = t; 

+		if (StartOf(7)) {

+			Expression(out e);

+			indexes.Add(e); 

+			while (la.kind == 11) {

+				Get();

+				Expression(out e);

+				indexes.Add(e); 

 			}

-			Expect(16);

-			runningLhs =

-			 new MapAssignLhs (x, runningLhs, indexes);
 		}

-		lhs = runningLhs;
+		Expect(16);

 	}

 

 	void CallForallArg(out Expr exprOptional) {

 		exprOptional = null;

 		Expr! e;

 		

-		if (la.kind == 44) {

+		if (la.kind == 42) {

 			Get();

-		} else if (StartOf(5)) {

+		} else if (StartOf(7)) {

 			Expression(out e);

-			exprOptional = e;
-		} else SynErr(108);

+			exprOptional = e; 

+		} else SynErr(105);

 	}

 

 	void CallOutIdent(out IToken id) {

 		id = null;

 		IToken! p;

 		

-		if (la.kind == 44) {

+		if (la.kind == 42) {

 			Get();

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

 			Ident(out p);

-			id = p;
-		} else SynErr(109);

+			id = p; 

+		} else SynErr(106);

 	}

 

 	void Expressions(out ExprSeq! es) {

-		Expr! e; es = new ExprSeq();
+		Expr! e; es = new ExprSeq(); 

 		Expression(out e);

-		es.Add(e);
+		es.Add(e); 

 		while (la.kind == 11) {

 			Get();

 			Expression(out e);

-			es.Add(e);
+			es.Add(e); 

 		}

 	}

 

 	void ImpliesExpression(bool noExplies, out Expr! e0) {

-		IToken! x; Expr! e1;
+		IToken! x; Expr! e1; 

 		LogicalExpression(out e0);

 		if (StartOf(9)) {

-			if (la.kind == 54 || la.kind == 55) {

+			if (la.kind == 52 || la.kind == 53) {

 				ImpliesOp();

-				x = t;
+				x = t; 

 				ImpliesExpression(true, out e1);

-				e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1);
+				e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1); 

 			} else {

 				ExpliesOp();

 				if (noExplies)

 				 this.SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");

-				x = t;
+				x = t; 

 				LogicalExpression(out e1);

-				e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
-				while (la.kind == 56 || la.kind == 57) {

+				e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); 

+				while (la.kind == 54 || la.kind == 55) {

 					ExpliesOp();

-					x = t;
+					x = t; 

 					LogicalExpression(out e1);

-					e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
+					e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); 

 				}

 			}

 		}

 	}

 

 	void EquivOp() {

-		if (la.kind == 52) {

+		if (la.kind == 50) {

 			Get();

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

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

 			Get();

-		} else SynErr(110);

+		} else SynErr(107);

 	}

 

 	void LogicalExpression(out Expr! e0) {

-		IToken! x; Expr! e1; BinaryOperator.Opcode op;
+		IToken! x; Expr! e1; BinaryOperator.Opcode op; 

 		RelationalExpression(out e0);

 		if (StartOf(10)) {

-			if (la.kind == 58 || la.kind == 59) {

+			if (la.kind == 56 || la.kind == 57) {

 				AndOp();

-				x = t;
+				x = t; 

 				RelationalExpression(out e1);

-				e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
-				while (la.kind == 58 || la.kind == 59) {

+				e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); 

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

 					AndOp();

-					x = t;
+					x = t; 

 					RelationalExpression(out e1);

-					e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
+					e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); 

 				}

 			} else {

 				OrOp();

-				x = t;
+				x = t; 

 				RelationalExpression(out e1);

-				e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
-				while (la.kind == 60 || la.kind == 61) {

+				e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); 

+				while (la.kind == 58 || la.kind == 59) {

 					OrOp();

-					x = t;
+					x = t; 

 					RelationalExpression(out e1);

-					e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
+					e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); 

 				}

 			}

 		}

 	}

 

 	void ImpliesOp() {

-		if (la.kind == 54) {

+		if (la.kind == 52) {

 			Get();

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

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

 			Get();

-		} else SynErr(111);

+		} else SynErr(108);

 	}

 

 	void ExpliesOp() {

-		if (la.kind == 56) {

+		if (la.kind == 54) {

 			Get();

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

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

 			Get();

-		} else SynErr(112);

+		} else SynErr(109);

 	}

 

 	void RelationalExpression(out Expr! e0) {

-		IToken! x; Expr! e1; BinaryOperator.Opcode op;
+		IToken! x; Expr! e1; BinaryOperator.Opcode op; 

 		BvTerm(out e0);

 		if (StartOf(11)) {

 			RelOp(out x, out op);

 			BvTerm(out e1);

-			e0 = Expr.Binary(x, op, e0, e1);
+			e0 = Expr.Binary(x, op, e0, e1); 

 		}

 	}

 

 	void AndOp() {

-		if (la.kind == 58) {

+		if (la.kind == 56) {

 			Get();

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

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

 			Get();

-		} else SynErr(113);

+		} else SynErr(110);

 	}

 

 	void OrOp() {

-		if (la.kind == 60) {

+		if (la.kind == 58) {

 			Get();

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

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

 			Get();

-		} else SynErr(114);

+		} else SynErr(111);

 	}

 

 	void BvTerm(out Expr! e0) {

-		IToken! x; Expr! e1;
+		IToken! x; Expr! e1; 

 		Term(out e0);

-		while (la.kind == 70) {

+		while (la.kind == 68) {

 			Get();

-			x = t;
+			x = t; 

 			Term(out e1);

-			e0 = new BvConcatExpr(x, e0, e1);
+			e0 = new BvConcatExpr(x, e0, e1); 

 		}

 	}

 

 	void RelOp(out IToken! x, out BinaryOperator.Opcode op) {

-		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
+		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 

 		switch (la.kind) {

-		case 62: {

+		case 60: {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Eq;
+			x = t; op=BinaryOperator.Opcode.Eq; 

 			break;

 		}

 		case 17: {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Lt;
+			x = t; op=BinaryOperator.Opcode.Lt; 

 			break;

 		}

 		case 18: {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Gt;
+			x = t; op=BinaryOperator.Opcode.Gt; 

 			break;

 		}

-		case 63: {

+		case 61: {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Le;
+			x = t; op=BinaryOperator.Opcode.Le; 

 			break;

 		}

-		case 64: {

+		case 62: {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Ge;
+			x = t; op=BinaryOperator.Opcode.Ge; 

 			break;

 		}

-		case 65: {

+		case 63: {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Neq;
+			x = t; op=BinaryOperator.Opcode.Neq; 

 			break;

 		}

-		case 66: {

+		case 64: {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Subtype;
+			x = t; op=BinaryOperator.Opcode.Subtype; 

 			break;

 		}

-		case 67: {

+		case 65: {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Neq;
+			x = t; op=BinaryOperator.Opcode.Neq; 

 			break;

 		}

-		case 68: {

+		case 66: {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Le;
+			x = t; op=BinaryOperator.Opcode.Le; 

 			break;

 		}

-		case 69: {

+		case 67: {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Ge;
+			x = t; op=BinaryOperator.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(115); break;

+		default: SynErr(112); break;

 		}

 	}

 

 	void Term(out Expr! e0) {

-		IToken! x; Expr! e1; BinaryOperator.Opcode op;
+		IToken! x; Expr! e1; BinaryOperator.Opcode op; 

 		Factor(out e0);

-		while (la.kind == 71 || la.kind == 72) {

+		while (la.kind == 69 || la.kind == 70) {

 			AddOp(out x, out op);

 			Factor(out e1);

-			e0 = Expr.Binary(x, op, e0, e1);
+			e0 = Expr.Binary(x, op, e0, e1); 

 		}

 	}

 

 	void Factor(out Expr! e0) {

-		IToken! x; Expr! e1; BinaryOperator.Opcode op;
+		IToken! x; Expr! e1; BinaryOperator.Opcode op; 

 		UnaryExpression(out e0);

-		while (la.kind == 44 || la.kind == 73 || la.kind == 74) {

+		while (la.kind == 42 || la.kind == 71 || la.kind == 72) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

-			e0 = Expr.Binary(x, op, e0, e1);
+			e0 = Expr.Binary(x, op, e0, e1); 

 		}

 	}

 

 	void AddOp(out IToken! x, out BinaryOperator.Opcode op) {

-		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
-		if (la.kind == 71) {

+		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 

+		if (la.kind == 69) {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Add;
-		} else if (la.kind == 72) {

+			x = t; op=BinaryOperator.Opcode.Add; 

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

 			Get();

-			x = t; op=BinaryOperator.Opcode.Sub;
-		} else SynErr(116);

+			x = t; op=BinaryOperator.Opcode.Sub; 

+		} else SynErr(113);

 	}

 

 	void UnaryExpression(out Expr! e) {

 		IToken! x;

 		e = dummyExpr;

 		

-		if (la.kind == 72) {

+		if (la.kind == 70) {

 			Get();

-			x = t;
+			x = t; 

 			UnaryExpression(out e);

-			e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e);
-		} else if (la.kind == 75 || la.kind == 76) {

+			e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e); 

+		} else if (la.kind == 73 || la.kind == 74) {

 			NegOp();

-			x = t;
+			x = t; 

 			UnaryExpression(out e);

-			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
+			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); 

 		} else if (StartOf(12)) {

 			CoercionExpression(out e);

-		} else SynErr(117);

+		} else SynErr(114);

 	}

 

 	void MulOp(out IToken! x, out BinaryOperator.Opcode op) {

-		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
-		if (la.kind == 44) {

+		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 

+		if (la.kind == 42) {

 			Get();

-			x = t; op=BinaryOperator.Opcode.Mul;
-		} else if (la.kind == 73) {

+			x = t; op=BinaryOperator.Opcode.Mul; 

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

 			Get();

-			x = t; op=BinaryOperator.Opcode.Div;
-		} else if (la.kind == 74) {

+			x = t; op=BinaryOperator.Opcode.Div; 

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

 			Get();

-			x = t; op=BinaryOperator.Opcode.Mod;
-		} else SynErr(118);

+			x = t; op=BinaryOperator.Opcode.Mod; 

+		} else SynErr(115);

 	}

 

 	void NegOp() {

-		if (la.kind == 75) {

+		if (la.kind == 73) {

 			Get();

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

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

 			Get();

-		} else SynErr(119);

+		} else SynErr(116);

 	}

 

 	void CoercionExpression(out Expr! e) {

@@ -1666,10 +1556,10 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		ArrayExpression(out e);

 		while (la.kind == 10) {

 			Get();

-			x = t;
+			x = t; 

 			if (StartOf(2)) {

 				Type(out coercedTo);

-				e = Expr.CoerceType(x, e, coercedTo);
+				e = Expr.CoerceType(x, e, coercedTo); 

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

 				Nat(out bn);

 				if (!(e is LiteralExpr) || !((LiteralExpr)e).isBigNum) {

@@ -1679,7 +1569,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				  e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);

 				}

 				

-			} else SynErr(120);

+			} else SynErr(117);

 		}

 	}

 

@@ -1694,9 +1584,9 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 			x = t; allArgs = new ExprSeq ();

 			allArgs.Add(e);

-			store = false; bvExtract = false;
+			store = false; bvExtract = false; 

 			if (StartOf(13)) {

-				if (StartOf(5)) {

+				if (StartOf(7)) {

 					Expression(out index0);

 					if (index0 is BvBounds)

 					 bvExtract = true;

@@ -1711,7 +1601,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 						allArgs.Add(e1);

 						

 					}

-					if (la.kind == 49) {

+					if (la.kind == 47) {

 						Get();

 						Expression(out e1);

 						if (bvExtract || e1 is BvBounds)

@@ -1722,7 +1612,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				} else {

 					Get();

 					Expression(out e1);

-					allArgs.Add(e1); store = true;
+					allArgs.Add(e1); store = true; 

 				}

 			}

 			Expect(16);

@@ -1733,7 +1623,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			                        ((BvBounds)index0).Upper.ToIntSafe,

 			                        ((BvBounds)index0).Lower.ToIntSafe);

 			else

-			  e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);
+			  e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs); 

 			

 		}

 	}

@@ -1757,88 +1647,95 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		Bpl.Type! ty;

 		QKeyValue kv;

 		e = dummyExpr;

+		VariableSeq! locals;

+		List<Block!>! blocks;

 		

 		switch (la.kind) {

-		case 77: {

+		case 75: {

 			Get();

-			e = new LiteralExpr(t, false);
+			e = new LiteralExpr(t, false); 

 			break;

 		}

-		case 78: {

+		case 76: {

 			Get();

-			e = new LiteralExpr(t, true);
+			e = new LiteralExpr(t, true); 

 			break;

 		}

 		case 3: {

 			Nat(out bn);

-			e = new LiteralExpr(t, bn);
+			e = new LiteralExpr(t, bn); 

 			break;

 		}

 		case 2: {

 			BvLit(out bn, out n);

-			e = new LiteralExpr(t, bn, n);
+			e = new LiteralExpr(t, bn, n); 

 			break;

 		}

 		case 1: {

 			Ident(out x);

-			id = new IdentifierExpr(x, x.val);  e = id;
+			id = new IdentifierExpr(x, x.val);  e = id; 

 			if (la.kind == 8) {

 				Get();

-				if (StartOf(5)) {

+				if (StartOf(7)) {

 					Expressions(out es);

-					e = new NAryExpr(x, new FunctionCall(id), es);
+					e = new NAryExpr(x, new FunctionCall(id), es); 

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

-					e = new NAryExpr(x, new FunctionCall(id), new ExprSeq());
-				} else SynErr(121);

+					e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); 

+				} else SynErr(118);

 				Expect(9);

 			}

 			break;

 		}

-		case 79: {

+		case 77: {

 			Get();

-			x = t;
+			x = t; 

 			Expect(8);

 			Expression(out e);

 			Expect(9);

-			e = new OldExpr(x, e);
+			e = new OldExpr(x, e); 

 			break;

 		}

 		case 8: {

 			Get();

-			if (StartOf(5)) {

+			if (StartOf(7)) {

 				Expression(out e);

 				if (e is BvBounds)

 				 this.SemErr("parentheses around bitvector bounds " +

-				        "are not allowed");
-			} else if (la.kind == 51 || la.kind == 81) {

+				        "are not allowed"); 

+			} else if (la.kind == 49 || la.kind == 81) {

 				Forall();

-				x = t;
+				x = t; 

 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

 				if (typeParams.Length + ds.Length > 0)

-				 e = new ForallExpr(x, typeParams, ds, kv, trig, e);
+				 e = new ForallExpr(x, typeParams, ds, kv, trig, e); 

 			} else if (la.kind == 82 || la.kind == 83) {

 				Exists();

-				x = t;
+				x = t; 

 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

 				if (typeParams.Length + ds.Length > 0)

-				 e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
+				 e = new ExistsExpr(x, typeParams, ds, kv, trig, e); 

 			} else if (la.kind == 84 || la.kind == 85) {

 				Lambda();

-				x = t;
+				x = t; 

 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

 				if (trig != null)

 				 SemErr("triggers not allowed in lambda expressions");

 				if (typeParams.Length + ds.Length > 0)

-				  e = new LambdaExpr(x, typeParams, ds, kv, e);
-			} else SynErr(122);

+				  e = new LambdaExpr(x, typeParams, ds, kv, e); 

+			} else SynErr(119);

 			Expect(9);

 			break;

 		}

-		case 40: {

+		case 38: {

 			IfThenElseExpression(out e);

 			break;

 		}

-		default: SynErr(123); break;

+		case 78: {

+			CodeExpression(out locals, out blocks);

+			e = new CodeExpr(locals, blocks); 

+			break;

+		}

+		default: SynErr(120); break;

 		}

 	}

 

@@ -1859,11 +1756,11 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 	}

 

 	void Forall() {

-		if (la.kind == 51) {

+		if (la.kind == 49) {

 			Get();

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

 			Get();

-		} else SynErr(124);

+		} else SynErr(121);

 	}

 

 	void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,

@@ -1880,7 +1777,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			}

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

 			BoundVars(q, out ds);

-		} else SynErr(125);

+		} else SynErr(122);

 		QSep();

 		while (la.kind == 25) {

 			AttributeOrTrigger(ref kv, ref trig);

@@ -1893,7 +1790,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			Get();

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

 			Get();

-		} else SynErr(126);

+		} else SynErr(123);

 	}

 

 	void Lambda() {

@@ -1901,21 +1798,75 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			Get();

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

 			Get();

-		} else SynErr(127);

+		} else SynErr(124);

 	}

 

 	void IfThenElseExpression(out Expr! e) {

 		IToken! tok;

-		Expr! e0, e1, e2;
-		e = dummyExpr;
-		Expect(40);

-		tok = t;
+		Expr! e0, e1, e2; 

+		e = dummyExpr; 

+		Expect(38);

+		tok = t; 

 		Expression(out e0);

 		Expect(80);

 		Expression(out e1);

-		Expect(41);

+		Expect(39);

 		Expression(out e2);

-		e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2));
+		e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); 

+	}

+

+	void CodeExpression(out VariableSeq! locals, out List<Block!>! blocks) {

+		locals = new VariableSeq(); Block! b;

+		blocks = new List<Block!>();

+		

+		Expect(78);

+		while (la.kind == 6) {

+			LocalVars(locals);

+		}

+		SpecBlock(out b);

+		blocks.Add(b); 

+		while (la.kind == 1) {

+			SpecBlock(out b);

+			blocks.Add(b); 

+		}

+		Expect(79);

+	}

+

+	void SpecBlock(out Block! b) {

+		IToken! x; IToken! y;

+		Cmd c;  IToken label;

+		CmdSeq cs = new CmdSeq();

+		TokenSeq! xs;

+		StringSeq ss = new StringSeq();

+		b = dummyBlock;

+		Expr! e;

+		

+		Ident(out x);

+		Expect(10);

+		while (StartOf(6)) {

+			LabelOrCmd(out c, out label);

+			if (c != null) {

+			 assert label == null;

+			 cs.Add(c);

+			} else {

+			  assert label != null;

+			  SemErr("SpecBlock's can only have one label");

+			}

+			

+		}

+		if (la.kind == 36) {

+			Get();

+			y = t; 

+			Idents(out xs);

+			foreach (IToken! s in xs) { ss.Add(s.val); }

+			b = new Block(x,x.val,cs,new GotoCmd(y,ss));

+			

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

+			Get();

+			Expression(out e);

+			b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); 

+		} else SynErr(125);

+		Expect(7);

 	}

 

 	void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {

@@ -1924,18 +1875,18 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 		List<object!> parameters;  object! param;

 		

 		Expect(25);

-		tok = t;
+		tok = t; 

 		if (la.kind == 10) {

 			Get();

 			Expect(1);

-			key = t.val;  parameters = new List<object!>();
+			key = t.val;  parameters = new List<object!>(); 

 			if (StartOf(14)) {

 				AttributeParameter(out param);

-				parameters.Add(param);
+				parameters.Add(param); 

 				while (la.kind == 11) {

 					Get();

 					AttributeParameter(out param);

-					parameters.Add(param);
+					parameters.Add(param); 

 				}

 			}

 			if (key == "nopats") {

@@ -1957,13 +1908,13 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			  }

 			}

 			

-		} else if (StartOf(5)) {

+		} else if (StartOf(7)) {

 			Expression(out e);

-			es = new ExprSeq(e);
+			es = new ExprSeq(e); 

 			while (la.kind == 11) {

 				Get();

 				Expression(out e);

-				es.Add(e);
+				es.Add(e); 

 			}

 			if (trig==null) {

 			 trig = new Trigger(tok, true, es, null);

@@ -1971,7 +1922,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			  trig.AddLast(new Trigger(tok, true, es, null));

 			}

 			

-		} else SynErr(128);

+		} else SynErr(126);

 		Expect(26);

 	}

 

@@ -1981,11 +1932,11 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 		

 		if (la.kind == 4) {

 			Get();

-			o = t.val.Substring(1, t.val.Length-2);
-		} else if (StartOf(5)) {

+			o = t.val.Substring(1, t.val.Length-2); 

+		} else if (StartOf(7)) {

 			Expression(out e);

-			o = e;
-		} else SynErr(129);

+			o = e; 

+		} else SynErr(127);

 	}

 

 	void QSep() {

@@ -1993,7 +1944,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			Get();

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

 			Get();

-		} else SynErr(130);

+		} else SynErr(128);

 	}

 

 

@@ -2013,16 +1964,16 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 		{x,T,x,x, x,x,x,x, T,x,x,x, x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

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

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

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

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

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

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

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

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

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

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

 

 	};

 } // end Parser

@@ -2075,50 +2026,50 @@ public class Errors {
 			case 33: s = "\"free\" expected"; break;

 			case 34: s = "\"requires\" expected"; break;

 			case 35: s = "\"ensures\" expected"; break;

-			case 36: s = "\"{{\" expected"; break;

-			case 37: s = "\"}}\" expected"; break;

-			case 38: s = "\"goto\" expected"; break;

-			case 39: s = "\"return\" expected"; break;

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

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

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

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

-			case 44: s = "\"*\" expected"; break;

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

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

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

-			case 48: s = "\"havoc\" expected"; break;

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

-			case 50: s = "\"call\" expected"; break;

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

-			case 52: s = "\"<==>\" expected"; break;

-			case 53: s = "\"\\u21d4\" expected"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

-			case 67: s = "\"\\u2260\" expected"; break;

-			case 68: s = "\"\\u2264\" expected"; break;

-			case 69: s = "\"\\u2265\" expected"; break;

-			case 70: s = "\"++\" expected"; break;

-			case 71: s = "\"+\" expected"; break;

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

-			case 73: s = "\"/\" expected"; break;

-			case 74: s = "\"%\" expected"; break;

-			case 75: s = "\"!\" expected"; break;

-			case 76: s = "\"\\u00ac\" expected"; break;

-			case 77: s = "\"false\" expected"; break;

-			case 78: s = "\"true\" expected"; break;

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

+			case 36: s = "\"goto\" expected"; break;

+			case 37: s = "\"return\" expected"; break;

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

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

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

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

+			case 42: s = "\"*\" expected"; break;

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

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

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

+			case 46: s = "\"havoc\" expected"; break;

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

+			case 48: s = "\"call\" expected"; break;

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

+			case 50: s = "\"<==>\" expected"; break;

+			case 51: s = "\"\\u21d4\" expected"; break;

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

+			case 53: s = "\"\\u21d2\" expected"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

+			case 67: s = "\"\\u2265\" expected"; break;

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

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

+			case 70: s = "\"-\" expected"; break;

+			case 71: s = "\"/\" expected"; break;

+			case 72: s = "\"%\" expected"; break;

+			case 73: s = "\"!\" expected"; break;

+			case 74: s = "\"\\u00ac\" expected"; break;

+			case 75: s = "\"false\" expected"; break;

+			case 76: s = "\"true\" expected"; break;

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

+			case 78: s = "\"|{\" expected"; break;

+			case 79: s = "\"}|\" expected"; break;

 			case 80: s = "\"then\" expected"; break;

 			case 81: s = "\"\\u2200\" expected"; break;

 			case 82: s = "\"exists\" expected"; break;

@@ -2136,40 +2087,38 @@ public class Errors {
 			case 94: s = "invalid TypeArgs"; break;

 			case 95: s = "invalid Spec"; break;

 			case 96: s = "invalid SpecPrePost"; break;

-			case 97: s = "invalid SpecPrePost"; break;

-			case 98: s = "invalid SpecPrePost"; break;

-			case 99: s = "invalid SpecBlock"; break;

-			case 100: s = "invalid LabelOrCmd"; break;

-			case 101: s = "invalid StructuredCmd"; break;

-			case 102: s = "invalid TransferCmd"; break;

-			case 103: s = "invalid IfCmd"; break;

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

-			case 105: s = "invalid LabelOrAssign"; break;

-			case 106: s = "invalid CallCmd"; break;

-			case 107: s = "invalid CallCmd"; break;

-			case 108: s = "invalid CallForallArg"; break;

-			case 109: s = "invalid CallOutIdent"; break;

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

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

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

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

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

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

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

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

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

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

-			case 120: s = "invalid CoercionExpression"; break;

-			case 121: s = "invalid AtomExpression"; break;

-			case 122: s = "invalid AtomExpression"; break;

-			case 123: s = "invalid AtomExpression"; break;

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

-			case 125: s = "invalid QuantifierBody"; break;

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

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

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

-			case 129: s = "invalid AttributeParameter"; break;

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

+			case 97: s = "invalid LabelOrCmd"; break;

+			case 98: s = "invalid StructuredCmd"; break;

+			case 99: s = "invalid TransferCmd"; break;

+			case 100: s = "invalid IfCmd"; break;

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

+			case 102: s = "invalid LabelOrAssign"; break;

+			case 103: s = "invalid CallCmd"; break;

+			case 104: s = "invalid CallCmd"; break;

+			case 105: s = "invalid CallForallArg"; break;

+			case 106: s = "invalid CallOutIdent"; break;

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

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

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

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

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

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

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

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

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

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

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

+			case 118: s = "invalid AtomExpression"; break;

+			case 119: s = "invalid AtomExpression"; break;

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

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

+			case 122: s = "invalid QuantifierBody"; break;

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

+			case 124: s = "invalid Lambda"; break;

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

+			case 126: s = "invalid AttributeOrTrigger"; break;

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

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

 

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

 		}

diff --git a/Source/Core/ResolutionContext.ssc b/Source/Core/ResolutionContext.ssc
index bb1fc7c6..10ff7d87 100644
--- a/Source/Core/ResolutionContext.ssc
+++ b/Source/Core/ResolutionContext.ssc
@@ -410,26 +410,36 @@ namespace Microsoft.Boogie
 

         // ------------------------------  Blocks  ------------------------------

 

-        // blocks

-        [Microsoft.Contracts.SpecPublic]

-        /*maybe null*/ Hashtable /*string->Block*/ blocks;

+        class ProcedureContext {

+            public readonly Hashtable! /*string->Block!*/ Blocks;

+            public readonly ProcedureContext Next;

+            public ProcedureContext(ProcedureContext next) {

+                Blocks = new Hashtable /*string->Block!*/ ();

+                Next = next;

+            }

+        }

+        /*maybe null*/ ProcedureContext procedureContext;  // stack of procedure contexts

+        public bool HasProcedureContext {

+          get { return procedureContext != null; }

+        }

 

         /// <summary>

-        /// Requires there not to be a procedure context.  Creates one.

+        /// Pushes a new procedure context.

         /// </summary>

-        public void StartProcedureContext() 

+        public void PushProcedureContext() 

+          ensures HasProcedureContext;

         {

-            System.Diagnostics.Debug.Assert(blocks == null);

-            blocks = new Hashtable /*string->Block*/ ();

+          procedureContext = new ProcedureContext(procedureContext);

         }

 

         /// <summary>

-        /// Requires there to be a procedure context.  Removes it.

+        /// Requires there to be a procedure context.  Pops it.

         /// </summary>

-        public void EndProcedureContext() 

+        public void PopProcedureContext() 

+          requires HasProcedureContext;

         {

-            System.Diagnostics.Debug.Assert(blocks != null);

-            blocks = null;

+          assert procedureContext != null;  // follows from precondition

+          procedureContext = procedureContext.Next;

         }

 

         /// <summary>

@@ -437,8 +447,10 @@ namespace Microsoft.Boogie
         /// </summary>

         /// <param name="block"></param>

         public void AddBlock(Block! block) 

-          requires this.blocks != null;

+          requires HasProcedureContext;

         {

+            assert procedureContext != null;  // follows from precondition

+            Hashtable! /*string->Block!*/ blocks = procedureContext.Blocks;

             if (blocks[block.Label] != null) 

             {

                 Error(block, "more than one declaration of block name: {0}", block.Label);

@@ -457,8 +469,10 @@ namespace Microsoft.Boogie
         /// <param name="name"></param>

         /// <returns></returns>

         public Block LookUpBlock(string! name)

-          requires this.blocks != null;

+          requires HasProcedureContext;

         {

+            assert procedureContext != null;  // follows from precondition

+            Hashtable! /*string->Block!*/ blocks = procedureContext.Blocks;

             return (Block)blocks[name];

         }

 

diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc
index 97a2dfea..870720d3 100644
--- a/Source/Core/Scanner.ssc
+++ b/Source/Core/Scanner.ssc
@@ -237,40 +237,40 @@ public class Scanner {
 		for (int i = 126; i <= 126; ++i) start[i] = 2;

 		for (int i = 48; i <= 57; ++i) start[i] = 9;

 		for (int i = 34; i <= 34; ++i) start[i] = 6;

-		start[92] = 1;
-		start[59] = 10;
-		start[40] = 11;
-		start[41] = 12;
-		start[58] = 47;
-		start[44] = 13;
-		start[91] = 14;
-		start[93] = 15;
-		start[60] = 48;
-		start[62] = 49;
-		start[123] = 50;
-		start[125] = 51;
-		start[61] = 52;
-		start[42] = 18;
-		start[8660] = 21;
-		start[8658] = 23;
-		start[8656] = 24;
-		start[38] = 25;
-		start[8743] = 27;
-		start[124] = 28;
-		start[8744] = 30;
-		start[33] = 53;
-		start[8800] = 34;
-		start[8804] = 35;
-		start[8805] = 36;
-		start[43] = 54;
-		start[45] = 38;
-		start[47] = 39;
-		start[37] = 40;
-		start[172] = 41;
-		start[8704] = 42;
-		start[8707] = 43;
-		start[955] = 44;
-		start[8226] = 46;
+		start[92] = 1; 

+		start[59] = 10; 

+		start[40] = 11; 

+		start[41] = 12; 

+		start[58] = 47; 

+		start[44] = 13; 

+		start[91] = 14; 

+		start[93] = 15; 

+		start[60] = 48; 

+		start[62] = 49; 

+		start[123] = 16; 

+		start[125] = 50; 

+		start[61] = 51; 

+		start[42] = 17; 

+		start[8660] = 20; 

+		start[8658] = 22; 

+		start[8656] = 23; 

+		start[38] = 24; 

+		start[8743] = 26; 

+		start[124] = 52; 

+		start[8744] = 28; 

+		start[33] = 53; 

+		start[8800] = 32; 

+		start[8804] = 33; 

+		start[8805] = 34; 

+		start[43] = 54; 

+		start[45] = 36; 

+		start[47] = 37; 

+		start[37] = 38; 

+		start[172] = 39; 

+		start[8704] = 42; 

+		start[8707] = 43; 

+		start[955] = 44; 

+		start[8226] = 46; 

 		start[Buffer.EOF] = -1;

 

 	}

@@ -351,7 +351,7 @@ public class Scanner {
 				// eol handling uniform across Windows, Unix and Mac

 				if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 				if (ch == EOL) {

-					line++; col = 0;
+					line++; col = 0; 

 				} else if (ch == '#' && col == 1) {

 				  int prLine = line;

 				  int prColumn = 0;

@@ -480,21 +480,21 @@ public class Scanner {
 			case "free": t.kind = 33; break;

 			case "requires": t.kind = 34; break;

 			case "ensures": t.kind = 35; break;

-			case "goto": t.kind = 38; break;

-			case "return": t.kind = 39; break;

-			case "if": t.kind = 40; break;

-			case "else": t.kind = 41; break;

-			case "while": t.kind = 42; break;

-			case "invariant": t.kind = 43; break;

-			case "break": t.kind = 45; break;

-			case "assert": t.kind = 46; break;

-			case "assume": t.kind = 47; break;

-			case "havoc": t.kind = 48; break;

-			case "call": t.kind = 50; break;

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

-			case "false": t.kind = 77; break;

-			case "true": t.kind = 78; break;

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

+			case "goto": t.kind = 36; break;

+			case "return": t.kind = 37; break;

+			case "if": t.kind = 38; break;

+			case "else": t.kind = 39; break;

+			case "while": t.kind = 40; break;

+			case "invariant": t.kind = 41; break;

+			case "break": t.kind = 43; break;

+			case "assert": t.kind = 44; break;

+			case "assume": t.kind = 45; break;

+			case "havoc": t.kind = 46; break;

+			case "call": t.kind = 48; break;

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

+			case "false": t.kind = 75; break;

+			case "true": t.kind = 76; break;

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

 			case "then": t.kind = 80; break;

 			case "exists": t.kind = 82; break;

 			case "lambda": t.kind = 84; break;

@@ -510,7 +510,7 @@ public class Scanner {
 		int recKind = noSym;

 		int recEnd = pos;

 		t = new Token();

-		t.pos = pos; t.col = col; t.line = line;
+		t.pos = pos; t.col = col; t.line = line; 

 		t.filename = this.Filename;

 		int state;

 		if (start.ContainsKey(ch)) { state = (int) (!) start[ch]; }

@@ -572,37 +572,36 @@ public class Scanner {
 			case 15:

 				{t.kind = 16; break;}

 			case 16:

-				{t.kind = 36; break;}

+				{t.kind = 25; break;}

 			case 17:

-				{t.kind = 37; break;}

+				{t.kind = 42; break;}

 			case 18:

-				{t.kind = 44; break;}

+				{t.kind = 47; break;}

 			case 19:

-				{t.kind = 49; break;}

+				{t.kind = 50; break;}

 			case 20:

-				{t.kind = 52; break;}

+				{t.kind = 51; break;}

 			case 21:

-				{t.kind = 53; break;}

+				{t.kind = 52; break;}

 			case 22:

-				{t.kind = 54; break;}

+				{t.kind = 53; break;}

 			case 23:

 				{t.kind = 55; break;}

 			case 24:

-				{t.kind = 57; break;}

-			case 25:

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

+				if (ch == '&') {AddCh(); goto case 25;}

 				else {goto case 0;}

+			case 25:

+				{t.kind = 56; break;}

 			case 26:

-				{t.kind = 58; break;}

+				{t.kind = 57; break;}

 			case 27:

-				{t.kind = 59; break;}

+				{t.kind = 58; break;}

 			case 28:

-				if (ch == '|') {AddCh(); goto case 29;}

-				else {goto case 0;}

+				{t.kind = 59; break;}

 			case 29:

-				{t.kind = 60; break;}

+				{t.kind = 62; break;}

 			case 30:

-				{t.kind = 61; break;}

+				{t.kind = 63; break;}

 			case 31:

 				{t.kind = 64; break;}

 			case 32:

@@ -614,17 +613,17 @@ public class Scanner {
 			case 35:

 				{t.kind = 68; break;}

 			case 36:

-				{t.kind = 69; break;}

-			case 37:

 				{t.kind = 70; break;}

+			case 37:

+				{t.kind = 71; break;}

 			case 38:

 				{t.kind = 72; break;}

 			case 39:

-				{t.kind = 73; break;}

-			case 40:

 				{t.kind = 74; break;}

+			case 40:

+				{t.kind = 78; break;}

 			case 41:

-				{t.kind = 76; break;}

+				{t.kind = 79; break;}

 			case 42:

 				{t.kind = 81; break;}

 			case 43:

@@ -637,50 +636,50 @@ public class Scanner {
 				{t.kind = 87; break;}

 			case 47:

 				recEnd = pos; recKind = 10;

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

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

 				else if (ch == ':') {AddCh(); goto case 45;}

 				else {t.kind = 10; break;}

 			case 48:

 				recEnd = pos; recKind = 17;

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

-				else if (ch == ':') {AddCh(); goto case 33;}

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

 				else {t.kind = 17; break;}

 			case 49:

 				recEnd = pos; recKind = 18;

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

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

 				else {t.kind = 18; break;}

 			case 50:

-				recEnd = pos; recKind = 25;

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

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

-			case 51:

 				recEnd = pos; recKind = 26;

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

+				if (ch == '|') {AddCh(); goto case 41;}

 				else {t.kind = 26; break;}

-			case 52:

+			case 51:

 				recEnd = pos; recKind = 29;

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

 				else {t.kind = 29; break;}

+			case 52:

+				if (ch == '|') {AddCh(); goto case 27;}

+				else if (ch == '{') {AddCh(); goto case 40;}

+				else {goto case 0;}

 			case 53:

-				recEnd = pos; recKind = 75;

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

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

+				recEnd = pos; recKind = 73;

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

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

 			case 54:

-				recEnd = pos; recKind = 71;

-				if (ch == '+') {AddCh(); goto case 37;}

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

+				recEnd = pos; recKind = 69;

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

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

 			case 55:

-				recEnd = pos; recKind = 63;

+				recEnd = pos; recKind = 61;

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

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

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

 			case 56:

-				recEnd = pos; recKind = 62;

-				if (ch == '>') {AddCh(); goto case 22;}

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

+				recEnd = pos; recKind = 60;

+				if (ch == '>') {AddCh(); goto case 21;}

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

 			case 57:

-				recEnd = pos; recKind = 56;

-				if (ch == '>') {AddCh(); goto case 20;}

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

+				recEnd = pos; recKind = 54;

+				if (ch == '>') {AddCh(); goto case 19;}

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

 

 		}

 		t.val = new String(tval, 0, tlen);

diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc
index be39fb8f..10984ff3 100644
--- a/Source/Core/StandardVisitor.ssc
+++ b/Source/Core/StandardVisitor.ssc
@@ -58,12 +58,12 @@ namespace Microsoft.Boogie
     }

     public virtual AIVariableExpr! VisitAIVariableExpr(AIVariableExpr! node)

     {

-      return node;
+      return node;

     }

     public virtual Cmd! VisitAssertCmd(AssertCmd! node)

     {

       node.Expr = this.VisitExpr(node.Expr);

-      return node;
+      return node;

     }

     public virtual Cmd! VisitAssignCmd(AssignCmd! node)

     {

@@ -76,21 +76,21 @@ namespace Microsoft.Boogie
     public virtual Cmd! VisitAssumeCmd(AssumeCmd! node)

     {

       node.Expr = this.VisitExpr(node.Expr);

-      return node;
+      return node;

     }

     public virtual AtomicRE! VisitAtomicRE(AtomicRE! node)

     {

       node.b = this.VisitBlock(node.b);

-      return node;
+      return node;

     }

     public virtual Axiom! VisitAxiom(Axiom! node)

     {

       node.Expr = this.VisitExpr(node.Expr);

-      return node;
+      return node;

     }

     public virtual Type! VisitBasicType(BasicType! node)

     {

-      return this.VisitType(node);
+      return this.VisitType(node);

     }

     public virtual BvConcatExpr! VisitBvConcatExpr(BvConcatExpr! node)

     {

@@ -100,7 +100,7 @@ namespace Microsoft.Boogie
     }

     public virtual Type! VisitBvType(BvType! node)

     {

-      return this.VisitType(node);
+      return this.VisitType(node);

     }

     public virtual Type! VisitBvTypeProxy(BvTypeProxy! node)

     {

@@ -113,14 +113,14 @@ namespace Microsoft.Boogie
     public virtual Block! VisitBlock(Block! node)

     {

       node.Cmds = this.VisitCmdSeq(node.Cmds);

-      node.TransferCmd = this.VisitTransferCmd((!)node.TransferCmd);

-      return node;
+      node.TransferCmd = (TransferCmd)this.Visit((!)node.TransferCmd);

+      return node;

     }

-    public virtual Expr! VisitBlockExpr(BlockExpr! node)

+    public virtual Expr! VisitCodeExpr(CodeExpr! node)

     {

       node.LocVars = this.VisitVariableSeq(node.LocVars);

-      node.Blocks = this.VisitBlockSeq(node.Blocks);

-      return node;
+      node.Blocks = this.VisitBlockList(node.Blocks);

+      return node;

     }

     public virtual BlockSeq! VisitBlockSeq(BlockSeq! blockSeq)

     {

@@ -138,7 +138,7 @@ namespace Microsoft.Boogie
     public virtual BoundVariable! VisitBoundVariable(BoundVariable! node)

     {

       node = (BoundVariable) this.VisitVariable(node);

-      return node;
+      return node;

     }

     public virtual Cmd! VisitCallCmd(CallCmd! node)

     {

@@ -148,7 +148,7 @@ namespace Microsoft.Boogie
       for (int i = 0; i < node.Outs.Count; ++i)

         if (node.Outs[i] != null)

           node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr((!)node.Outs[i]);

-      return node;
+      return node;

     }

     public virtual Cmd! VisitCallForallCmd(CallForallCmd! node)

     {

@@ -162,7 +162,7 @@ namespace Microsoft.Boogie
       }

       node.Ins = elist;

       node.Proc = this.VisitProcedure((!)node.Proc);

-      return node;
+      return node;

     }

     public virtual CmdSeq! VisitCmdSeq(CmdSeq! cmdSeq)

     {

@@ -173,7 +173,7 @@ namespace Microsoft.Boogie
     public virtual Choice! VisitChoice(Choice! node)

     {

       node.rs = this.VisitRESeq(node.rs);

-      return node;
+      return node;

     }

     public virtual Cmd! VisitCommentCmd(CommentCmd! node)

     {

@@ -181,7 +181,7 @@ namespace Microsoft.Boogie
     }

     public virtual Constant! VisitConstant(Constant! node)

     {

-      return node;
+      return node;

     }

     public virtual CtorType! VisitCtorType(CtorType! node)

     {

@@ -191,29 +191,29 @@ namespace Microsoft.Boogie
     }

     public virtual Declaration! VisitDeclaration(Declaration! node)

     {

-      return node;
+      return node;

     }

     public virtual List<Declaration!>! VisitDeclarationList(List<Declaration!>! declarationList)

     {

       for (int i = 0, n = declarationList.Count; i < n; i++)

         declarationList[i] = (Declaration!) this.Visit(declarationList[i]);

-      return declarationList;
+      return declarationList;

     }

     public virtual DeclWithFormals! VisitDeclWithFormals(DeclWithFormals! node)

     {

       node.InParams = this.VisitVariableSeq(node.InParams);

       node.OutParams = this.VisitVariableSeq(node.OutParams);

-      return node;
+      return node;

     }

     public virtual ExistsExpr! VisitExistsExpr(ExistsExpr! node)

     {

       node = (ExistsExpr) this.VisitQuantifierExpr(node);

-      return node;
+      return node;

     }

     public virtual BvExtractExpr! VisitBvExtractExpr(BvExtractExpr! node)

     {

       node.Bitvector = this.VisitExpr(node.Bitvector);

-      return node;
+      return node;

     }

     public virtual Expr! VisitExpr(Expr! node)

     {

@@ -224,7 +224,7 @@ namespace Microsoft.Boogie
     {

       for (int i = 0, n = exprSeq.Length; i < n; i++)

         exprSeq[i] = this.VisitExpr( (!)exprSeq[i]);

-      return exprSeq;
+      return exprSeq;

     }

     public virtual Requires! VisitRequires(Requires! @requires)

     {

@@ -251,50 +251,50 @@ namespace Microsoft.Boogie
     public virtual ForallExpr! VisitForallExpr(ForallExpr! node)

     {

       node = (ForallExpr) this.VisitQuantifierExpr(node);

-      return node;
+      return node;

     }

     public virtual LambdaExpr! VisitLambdaExpr(LambdaExpr! node)

     {

       node = (LambdaExpr) this.VisitBinderExpr(node);

-      return node;
+      return node;

     }

     public virtual Formal! VisitFormal(Formal! node)

     {

-      return node;
+      return node;

     }

     public virtual Function! VisitFunction(Function! node)

     {

       node = (Function) this.VisitDeclWithFormals(node);

       if (node.Body != null)

         node.Body = this.VisitExpr(node.Body);

-      return node;
+      return node;

     }

     public virtual GlobalVariable! VisitGlobalVariable(GlobalVariable! node)

     {

       node = (GlobalVariable) this.VisitVariable(node);

-      return node;
+      return node;

     }

     public virtual GotoCmd! VisitGotoCmd(GotoCmd! node)

     {

-      node.labelTargets = this.VisitBlockSeq((!)node.labelTargets);

-      return node;
+      // do not visit the labelTargets, or control-flow loops will lead to a looping visitor

+      return node;

     }

     public virtual Cmd! VisitHavocCmd(HavocCmd! node)

     {

       node.Vars = this.VisitIdentifierExprSeq(node.Vars);

-      return node;
+      return node;

     }

     public virtual Expr! VisitIdentifierExpr(IdentifierExpr! node)

     {

       if (node.Decl != null)

         node.Decl = this.VisitVariable(node.Decl);

-      return node;
+      return node;

     }

     public virtual IdentifierExprSeq! VisitIdentifierExprSeq(IdentifierExprSeq! identifierExprSeq)

     {

       for (int i = 0, n = identifierExprSeq.Length; i < n; i++)

         identifierExprSeq[i] = (IdentifierExpr) this.VisitIdentifierExpr( (!)identifierExprSeq[i]);

-      return identifierExprSeq;
+      return identifierExprSeq;

     }

     public virtual Implementation! VisitImplementation(Implementation! node)

     {

@@ -302,16 +302,16 @@ namespace Microsoft.Boogie
       node.Blocks = this.VisitBlockList(node.Blocks);

       node.Proc = this.VisitProcedure((!)node.Proc);

       node = (Implementation) this.VisitDeclWithFormals(node); // do this first or last?

-      return node;
+      return node;

     }

     public virtual LiteralExpr! VisitLiteralExpr(LiteralExpr! node)

     {

-      return node;
+      return node;

     }

 

     public virtual LocalVariable! VisitLocalVariable(LocalVariable! node)

     {

-      return node;
+      return node;

     }

 

     public virtual AssignLhs! VisitMapAssignLhs(MapAssignLhs! node)

@@ -319,7 +319,7 @@ namespace Microsoft.Boogie
       node.Map = (AssignLhs!)this.Visit(node.Map);

       for (int i = 0; i < node.Indexes.Count; ++i)

         node.Indexes[i] = (Expr!)this.Visit(node.Indexes[i]);

-      return node;
+      return node;

     }

     public virtual MapType! VisitMapType(MapType! node)

     {

@@ -345,12 +345,12 @@ namespace Microsoft.Boogie
     public virtual Expr! VisitNAryExpr(NAryExpr! node)

     {

       node.Args = this.VisitExprSeq(node.Args);

-      return node;
+      return node;

     }

     public virtual Expr! VisitOldExpr(OldExpr! node)

     {

       node.Expr = this.VisitExpr(node.Expr);

-      return node;
+      return node;

     }

     public virtual Procedure! VisitProcedure(Procedure! node)

     {

@@ -359,19 +359,19 @@ namespace Microsoft.Boogie
       node.Modifies = this.VisitIdentifierExprSeq(node.Modifies);

       node.OutParams = this.VisitVariableSeq(node.OutParams);

       node.Requires = this.VisitRequiresSeq(node.Requires);

-      return node;
+      return node;

     }

     public virtual Program! VisitProgram(Program! node)

     {

       node.TopLevelDeclarations = this.VisitDeclarationList(node.TopLevelDeclarations);

-      return node;
+      return node;

     }

     public virtual BinderExpr! VisitBinderExpr(BinderExpr! node)

     {

       node.Body = this.VisitExpr(node.Body);

       node.Dummies = this.VisitVariableSeq(node.Dummies);

       //node.Type = this.VisitType(node.Type);

-      return node;
+      return node;

     }

     public virtual QuantifierExpr! VisitQuantifierExpr(QuantifierExpr! node)

     {

@@ -379,7 +379,7 @@ namespace Microsoft.Boogie
       if (node.Triggers != null) {

         node.Triggers = this.VisitTrigger(node.Triggers);

       }

-      return node;
+      return node;

     }

     public virtual Cmd! VisitRE(RE! node)

     {

@@ -389,11 +389,11 @@ namespace Microsoft.Boogie
     {

       for (int i = 0, n = reSeq.Length; i < n; i++)

         reSeq[i] = (RE) this.VisitRE( (!)reSeq[i]);

-      return reSeq;
+      return reSeq;

     }

     public virtual ReturnCmd! VisitReturnCmd(ReturnCmd! node)

     {

-      return (ReturnCmd) this.VisitTransferCmd(node);
+      return (ReturnCmd) this.VisitTransferCmd(node);

     }

     public virtual ReturnExprCmd! VisitReturnExprCmd(ReturnExprCmd! node)

     {

@@ -404,23 +404,23 @@ namespace Microsoft.Boogie
     {

       node.first = (RE) this.VisitRE(node.first);

       node.second = (RE) this.VisitRE(node.second);

-      return node;
+      return node;

     }

     public virtual AssignLhs! VisitSimpleAssignLhs(SimpleAssignLhs! node)

     {

       node.AssignedVariable =

         (IdentifierExpr) this.VisitIdentifierExpr(node.AssignedVariable);

-      return node;
+      return node;

     }

     public virtual Cmd! VisitStateCmd(StateCmd! node)

     {

       node.Locals = this.VisitVariableSeq(node.Locals);

       node.Cmds = this.VisitCmdSeq(node.Cmds);

-      return node;
+      return node;

     }

     public virtual TransferCmd! VisitTransferCmd(TransferCmd! node)

     {

-      return node;
+      return node;

     }

     public virtual Trigger! VisitTrigger(Trigger! node)

     {

@@ -433,17 +433,17 @@ namespace Microsoft.Boogie
         }

       }

       node.Tr = this.VisitExprSeq(node.Tr);

-      return node;
+      return node;

     }

     // called by default for all nullary type constructors and type variables

     public virtual Type! VisitType(Type! node)

     {

-      return node;
+      return node;

     }

     public virtual TypedIdent! VisitTypedIdent(TypedIdent! node)

     {

       node.Type = (Type)this.Visit(node.Type);

-      return node;
+      return node;

     }

     public virtual Declaration! VisitTypeCtorDecl(TypeCtorDecl! node)

     {

@@ -462,7 +462,7 @@ namespace Microsoft.Boogie
     }

     public virtual Type! VisitTypeVariable(TypeVariable! node)

     {

-      return this.VisitType(node);
+      return this.VisitType(node);

     }

     public virtual Type! VisitTypeProxy(TypeProxy! node)

     {

@@ -474,30 +474,30 @@ namespace Microsoft.Boogie
     }

     public virtual Type! VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier! node)

     {

-      return this.VisitType(node);
+      return this.VisitType(node);

     }

     public virtual Variable! VisitVariable(Variable! node)

     {

       node.TypedIdent = this.VisitTypedIdent(node.TypedIdent);

-      return node;
+      return node;

     }

     public virtual VariableSeq! VisitVariableSeq(VariableSeq! variableSeq)

     {

       for (int i = 0, n = variableSeq.Length; i < n; i++)

         variableSeq[i] = this.VisitVariable( (!)variableSeq[i]);

-      return variableSeq;
+      return variableSeq;

     }    

     public virtual Cmd! VisitAssertEnsuresCmd(AssertEnsuresCmd! node)

     {

       node.Ensures = this.VisitEnsures(node.Ensures);

       node.Expr = this.VisitExpr(node.Expr);

-      return node;
+      return node;

     }    

     public virtual Cmd! VisitAssertRequiresCmd(AssertRequiresCmd! node)

     {

       node.Requires = this.VisitRequires(node.Requires);

       node.Expr = this.VisitExpr(node.Expr);

-      return node;
+      return node;

     }

   }

 }