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

25 files changed, 1168 insertions, 1047 deletions

diff --git a/Source/AIFramework/Expr.ssc b/Source/AIFramework/Expr.ssc
index 42621239..1f21f84a 100644
--- a/Source/AIFramework/Expr.ssc
+++ b/Source/AIFramework/Expr.ssc
@@ -26,7 +26,7 @@ namespace Microsoft.AbstractInterpretationFramework
     ///  AST nodes as AIF expressions.

     /// 

     ///  This only serves as a place for operations on expressions.  Clients

-    ///  should implement directly either IVariable or IFunApp.

+    ///  should implement directly IVariable, IFunApp, ...

     /// </summary>

     public interface IExpr

     {

@@ -90,6 +90,14 @@ namespace Microsoft.AbstractInterpretationFramework
     }

 

     /// <summary>

+    /// An interface representing an expression that at any moment could, in principle, evaluate

+    /// to a different value.  That is, the abstract interpreter should treat these IExpr's

+    /// as unknown values.  They are used when there is no other IExpr corresponding to the

+    /// expression to be modeled.

+    /// </summary>

+    public interface IUnknown : IExpr {}

+    

+    /// <summary>

     /// An abstract class that provides an interface for expression visitors.

     /// </summary>

     public abstract class ExprVisitor

@@ -147,6 +155,10 @@ namespace Microsoft.AbstractInterpretationFramework
                 else

                     result = fun.CloneWithBody(Substitute(subst, var, fun.Body));

             }

+            else if (inexpr is IUnknown)

+            {

+                result = inexpr;

+            }

             else

             {

                 assert false;

diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.ssc b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
index c0293493..ab030b59 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.ssc
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
@@ -78,7 +78,7 @@ namespace Microsoft.AbstractInterpretationFramework
 

             public bool IsBottom { 

                  get { 

-                   return this.constraints == null;
+                   return this.constraints == null;

                  } 

             }

 

@@ -89,7 +89,7 @@ namespace Microsoft.AbstractInterpretationFramework
                   requires !this.IsBottom;

                 { 

                   assume this.constraints != null;

-                  return (!) this.constraints.Keys;
+                  return (!) this.constraints.Keys;

                 } 

             }

 

@@ -117,7 +117,7 @@ namespace Microsoft.AbstractInterpretationFramework
                 requires !this.IsBottom;

                 { 

                   assume this.constraints != null;

-                  return (Element)constraints[key];
+                  return (Element)constraints[key];

                 } 

             }

 

@@ -303,7 +303,7 @@ namespace Microsoft.AbstractInterpretationFramework
             }

             Elt! join = new Elt(newMap);

         

-            // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
+            // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));

 

             return join;

         }

@@ -368,9 +368,9 @@ namespace Microsoft.AbstractInterpretationFramework
             }

             Element! widen= new Elt(newMap);

       

-            // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
+            // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));

 

-            return widen;
+            return widen;

         }

 

         internal static ISet/*<IVariable!>*/! VariablesInExpression(IExpr! e, ISet/*<IVariable!>*/! ignoreVars)

@@ -400,6 +400,10 @@ namespace Microsoft.AbstractInterpretationFramework
                 // Ignore the bound variable

                 s.AddAll(VariablesInExpression(lambda.Body, (!) Set.Union(ignoreVars, x)));

             }

+            else if (e is IUnknown)

+            {

+                // skip (actually, it would be appropriate to return the universal set of all variables)

+            }

             else

             {

                 Debug.Assert(false, "case not handled: " + e);

@@ -482,7 +486,7 @@ namespace Microsoft.AbstractInterpretationFramework
           else 

           {

             IExpr! left = (IExpr!) fun.Arguments[0];

-            IExpr! right = (IExpr!) fun.Arguments[1];
+            IExpr! right = (IExpr!) fun.Arguments[1];

 

             if(!(left is IVariable || right is IVariable))    // At least one of the two operands must be a variable

               return false;

@@ -493,7 +497,7 @@ namespace Microsoft.AbstractInterpretationFramework
                 || fun.FunctionSymbol.Equals(Int.Mul)

                 || fun.FunctionSymbol.Equals(Int.Div)

                 || fun.FunctionSymbol.Equals(Int.Mod))

-              return IsArithmeticExpr(left) && IsArithmeticExpr(right);
+              return IsArithmeticExpr(left) && IsArithmeticExpr(right);

             else 

               return false;

           } 

@@ -592,6 +596,12 @@ namespace Microsoft.AbstractInterpretationFramework
                        );

             }

 

+            // else

+            

+            if (expr is IUnknown) {

+              return expr;

+            }

+

             else

             {

                 throw

diff --git a/Source/AbsInt/LoopInvariantsOnDemand.cs b/Source/AbsInt/LoopInvariantsOnDemand.cs
index 49958289..5bb5916d 100644
--- a/Source/AbsInt/LoopInvariantsOnDemand.cs
+++ b/Source/AbsInt/LoopInvariantsOnDemand.cs
@@ -55,6 +55,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
         return VisitFunApp((AI.IFunApp)expr);

       else if (expr is AI.IFunction)

         return VisitFunction((AI.IFunction)expr);

+      else if (expr is AI.IUnknown)

+        return null;

       else {

         Contract.Assert(false);

         throw new cce.UnreachableException();

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;

     }

   }

 }

diff --git a/Source/Dafny.sln b/Source/Dafny.sln
index e900840a..e3bc28cd 100644
--- a/Source/Dafny.sln
+++ b/Source/Dafny.sln
@@ -27,6 +27,7 @@ Global
 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Mixed Platforms.Build.0 = Release|Any CPU

 		{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|.NET.ActiveCfg = Debug|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|.NET.Build.0 = Debug|Any CPU

 		{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

 		{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Any CPU.Build.0 = Debug|Any CPU

 		{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

diff --git a/Source/Provers/Isabelle/Prover.cs b/Source/Provers/Isabelle/Prover.cs
index 5fb9404d..dedfbc09 100644
--- a/Source/Provers/Isabelle/Prover.cs
+++ b/Source/Provers/Isabelle/Prover.cs
@@ -961,6 +961,31 @@ namespace Microsoft.Boogie.Isabelle {
       return Write(b2i, B2I.Kind.IfThenElse, node);

     }

 

+    public bool VisitCustomOp(VCExprNAry node, B2I b2i) {

+      Contract.Requires(node != null);

+      Contract.Requires(b2i != null);

+      VCExprCustomOp op = (VCExprCustomOp)node.Op;

+

+      Contract.Assert(op.Arity == node.Length);

+      b2i.Write(B2I.Kind.Function, op.Name + " " + node.Length);

+      if (b2i.Context.AllTypes) {

+        b2i.Indent(2);

+

+        // pick the types from the actual arguments

+        foreach (VCExpr arg in node) {

+          Contract.Assert(arg != null);

+          b2i.Write(arg.Type);

+        }

+        b2i.Unindent();

+      }

+      if (b2i.Context.AllTypes) {

+        b2i.Indent(2);

+        b2i.Write(op.Type);

+        b2i.Unindent();

+      }

+      WriteArguments(b2i, node);

+      return true;

+    }

 

     public bool VisitHeapSuccessionOp(VCExprNAry node, B2I b2i) {

       Contract.Requires(node != null);

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 376e93df..73ae55a9 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -642,6 +642,15 @@ void ObjectInvariant()
         return true;

       }

 

+      public bool VisitCustomOp(VCExprNAry node, LineariserOptions options) {

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+

+        VCExprCustomOp op = (VCExprCustomOp)node.Op;

+        WriteApplicationTermOnly(op.Name, node, options);

+        return true;

+      }

+

       public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options) {

         Contract.Requires(node != null);

         Contract.Requires(options != null);

diff --git a/Source/VCExpr/Boogie2VCExpr.ssc b/Source/VCExpr/Boogie2VCExpr.ssc
index 4e848c82..df966c2d 100644
--- a/Source/VCExpr/Boogie2VCExpr.ssc
+++ b/Source/VCExpr/Boogie2VCExpr.ssc
@@ -40,6 +40,8 @@ namespace Microsoft.Boogie.VCExprAST
     }

   }

 

+  public delegate VCExpr! CodeExprConverter(CodeExpr! codeExpr, Hashtable/*<Block, VCExprVar!>*/! blockVariables, List<VCExprLetBinding!>! bindings);

+

   public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {

     // Stack on which the various Visit-methods put the result of the translation

     private readonly Stack<VCExpr!>! SubExpressions = new Stack<VCExpr!> ();

@@ -477,9 +479,19 @@ namespace Microsoft.Boogie.VCExprAST
     {

       assert false;

     }

-    public override Expr! VisitBlockExpr(BlockExpr! node)

+    CodeExprConverter codeExprConverter = null;

+    public void SetCodeExprConverter(CodeExprConverter f){

+      this.codeExprConverter = f;

+    }

+    public override Expr! VisitCodeExpr(CodeExpr! codeExpr)

     {

-      assert false;

+      assume codeExprConverter != null;

+

+      Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();

+      List<VCExprLetBinding!> bindings = new List<VCExprLetBinding!>();

+      VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings);

+      Push(e);

+      return codeExpr;

     }

     public override BlockSeq! VisitBlockSeq(BlockSeq! blockSeq)

     {

diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc
index 52c51c3e..30779f22 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.ssc
+++ b/Source/VCExpr/SimplifyLikeLineariser.ssc
@@ -262,7 +262,7 @@ namespace Microsoft.Boogie.VCExprAST
     internal const string! eqName = "EQ"; // equality

     internal const string! neqName = "NEQ"; // inequality

     internal const string! lessName = "<";

-    internal const string! greaterName = ">";
+    internal const string! greaterName = ">";

     internal const string! atmostName = "<=";

     internal const string! atleastName = ">=";

     internal const string! TRUEName = "TRUE"; // nullary predicate that is always true

@@ -377,7 +377,7 @@ namespace Microsoft.Boogie.VCExprAST
       } else {

         wr.Write("({0} ", eqName);

         WriteId(printedName);

-        wr.Write(" {0})", boolTrueName);
+        wr.Write(" {0})", boolTrueName);

       }

 

       return true;

@@ -663,7 +663,7 @@ namespace Microsoft.Boogie.VCExprAST
           ExprLineariser.Linearise(node[0], options);

           wr.Write("))");

         } else {

-          WriteApplication(impliesName, node, options);
+          WriteApplication(impliesName, node, options);

         }

         return true;

       }

@@ -740,6 +740,17 @@ namespace Microsoft.Boogie.VCExprAST
         return true;

       }

 

+      public bool VisitCustomOp (VCExprNAry! node, LineariserOptions! options) {

+        VCExprCustomOp op = (VCExprCustomOp)node.Op;

+        wr.Write("({0}", op.Name);

+        foreach (VCExpr arg in node) {

+          wr.Write(" ");

+          ExprLineariser.Linearise(arg, options);

+        }

+        wr.Write(")");

+        return true;

+      }

+

       public bool VisitAddOp            (VCExprNAry! node, LineariserOptions! options) {

         if (CommandLineOptions.Clo.ReflectAdd) {

           WriteTermApplication(intAddNameReflect, node, options);

diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc
index 8ea6ff81..e0852071 100644
--- a/Source/VCExpr/TypeErasure.ssc
+++ b/Source/VCExpr/TypeErasure.ssc
@@ -131,7 +131,7 @@ namespace Microsoft.Boogie.TypeErasure
       List<VCExprVar!>! res = new List<VCExprVar!> (types.Count);

       for (int i = 0; i < types.Count; ++i)

         res.Add(gen.Variable(baseName + i, types[i]));

-      return res;
+      return res;

     }

   }

 

@@ -318,7 +318,7 @@ namespace Microsoft.Boogie.TypeErasure
         Typed2UntypedVariables.Add(var, res);

         AddVarTypeAxiom(res, var.Type);

       }

-      return (!)res;
+      return (!)res;

     }

 

     protected abstract void AddVarTypeAxiom(VCExprVar! var, Type! originalType);

@@ -371,7 +371,7 @@ namespace Microsoft.Boogie.TypeErasure
       CurrentCtorNum = BigNum.ZERO;

       TypeCtorReprs = new Dictionary<TypeCtorDecl!, TypeCtorRepr> ();

       TypeVariableMapping = new Dictionary<TypeVariable!, VCExprVar!> ();

-      Typed2UntypedVariables = new Dictionary<VCExprVar!, VCExprVar!> ();
+      Typed2UntypedVariables = new Dictionary<VCExprVar!, VCExprVar!> ();

 

       TypeCtorDecl! uDecl = new TypeCtorDecl(Token.NoToken, "U", 0);

       UDecl = uDecl;

@@ -847,7 +847,7 @@ namespace Microsoft.Boogie.TypeErasure
       VCExprVar res;

       if (!bindings.VCExprVarBindings.TryGetValue(node, out res))

         return AxBuilder.Typed2Untyped(node);

-      return (!)res;
+      return (!)res;

     }

 

     ////////////////////////////////////////////////////////////////////////////

@@ -863,7 +863,7 @@ namespace Microsoft.Boogie.TypeErasure
                                                       VariableBindings! bindings) {

       List<VCExprVar!>! newBoundVars = new List<VCExprVar!> (oldBoundVars.Count);

       foreach (VCExprVar! var in oldBoundVars) {

-        Type! newType = AxBuilder.TypeAfterErasure(var.Type);
+        Type! newType = AxBuilder.TypeAfterErasure(var.Type);

         VCExprVar! newVar = Gen.Variable(var.Name, newType);

         newBoundVars.Add(newVar);

         bindings.VCExprVarBindings.Add(var, newVar);

@@ -899,7 +899,7 @@ namespace Microsoft.Boogie.TypeErasure
       foreach (VCExprVar! var in node.BoundVars) {

         Type! newType =

           castVariables.Contains(var) ? AxBuilder.U

-                                      : AxBuilder.TypeAfterErasure(var.Type);
+                                      : AxBuilder.TypeAfterErasure(var.Type);

         VCExprVar! newVar = Gen.Variable(var.Name, newType);

         newBoundVars.Add(newVar);

         newBindings.VCExprVarBindings.Add(var, newVar);

@@ -985,7 +985,7 @@ namespace Microsoft.Boogie.TypeErasure
           forall{int i in (1:node.Arity); node[i].Type.Equals(oldType)})

         return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, oldType));

       else

-        return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U));
+        return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U));

     }

 

     ///////////////////////////////////////////////////////////////////////////

@@ -1027,6 +1027,10 @@ namespace Microsoft.Boogie.TypeErasure
       newArgs[2] = AxBuilder.Cast(newArgs[2], t);

       return Gen.Function(node.Op, newArgs);

     }

+    public override VCExpr! VisitCustomOp         (VCExprNAry! node, VariableBindings! bindings) {

+      List<VCExpr!>! newArgs = MutateSeq(node, bindings, 0);

+      return Gen.Function(node.Op, newArgs);

+    }

     public override VCExpr! VisitAddOp            (VCExprNAry! node, VariableBindings! bindings) {

       return CastArguments(node, Type.Int, bindings, 0);

     }

diff --git a/Source/VCExpr/VCExprAST.ssc b/Source/VCExpr/VCExprAST.ssc
index 1a81d4a0..7e5b31f1 100644
--- a/Source/VCExpr/VCExprAST.ssc
+++ b/Source/VCExpr/VCExprAST.ssc
@@ -240,6 +240,8 @@ namespace Microsoft.Boogie
     // the type of the compared terms

     public static readonly VCExprOp! Subtype3Op       = new VCExprNAryOp (3, Type.Bool);

     public static readonly VCExprOp! IfThenElseOp     = new VCExprIfThenElseOp();

+    

+    public static readonly VCExprOp! TickleBoolOp     = new VCExprCustomOp("tickleBool", 1, Type.Bool);

 

     public VCExprOp! BoogieFunctionOp(Function! func) {

       return new VCExprBoogieFunctionOp(func);

@@ -1036,6 +1038,33 @@ namespace Microsoft.Boogie.VCExprAST
       return visitor.VisitIfThenElseOp(expr, arg);

     }

   }

+  

+  public class VCExprCustomOp : VCExprOp {

+    public readonly string! Name;

+    int arity;

+    public readonly Type! Type;

+    public VCExprCustomOp(string! name, int arity, Type! type) {

+      this.Name = name;

+      this.arity = arity;

+      this.Type = type;

+    }

+    [Pure][Reads(ReadsAttribute.Reads.Nothing)]

+    public override bool Equals(object that) {

+      if (Object.ReferenceEquals(this, that))

+        return true;

+      VCExprCustomOp t = that as VCExprCustomOp;

+      if (t == null)

+        return false;

+      return this.Name == t.Name && this.arity == t.arity && this.Type == t.Type;

+    }

+    public override int Arity { get { return arity; } }

+    public override int TypeParamArity { get { return 0; } }

+    public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) { return Type; }

+    public override Result Accept<Result, Arg>

+           (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {

+      return visitor.VisitCustomOp(expr, arg);

+    }

+  }

 

   /////////////////////////////////////////////////////////////////////////////////

   // Bitvector operators

diff --git a/Source/VCExpr/VCExprASTPrinter.ssc b/Source/VCExpr/VCExprASTPrinter.ssc
index ca8ec11a..796a2b4e 100644
--- a/Source/VCExpr/VCExprASTPrinter.ssc
+++ b/Source/VCExpr/VCExprASTPrinter.ssc
@@ -196,6 +196,10 @@ namespace Microsoft.Boogie.VCExprAST
     public bool VisitIfThenElseOp(VCExprNAry! node, TextWriter! wr) {

       return PrintNAry("if-then-else", node, wr);

     }

+    public bool VisitCustomOp(VCExprNAry! node, TextWriter! wr) {

+      VCExprCustomOp op = (VCExprCustomOp)node.Op;

+      return PrintNAry(op.Name, node, wr);

+    }

     public bool VisitAddOp            (VCExprNAry! node, TextWriter! wr) {

       if (CommandLineOptions.Clo.ReflectAdd) {

         return PrintNAry("Reflect$Add", node, wr);

diff --git a/Source/VCExpr/VCExprASTVisitors.ssc b/Source/VCExpr/VCExprASTVisitors.ssc
index e1885f3a..c9d56962 100644
--- a/Source/VCExpr/VCExprASTVisitors.ssc
+++ b/Source/VCExpr/VCExprASTVisitors.ssc
@@ -52,6 +52,7 @@ namespace Microsoft.Boogie.VCExprAST
     Result VisitSubtype3Op       (VCExprNAry! node, Arg arg);

     Result VisitBoogieFunctionOp (VCExprNAry! node, Arg arg);

     Result VisitIfThenElseOp     (VCExprNAry! node, Arg arg);

+    Result VisitCustomOp         (VCExprNAry! node, Arg arg);

   }

 

   //////////////////////////////////////////////////////////////////////////////

@@ -959,6 +960,9 @@ namespace Microsoft.Boogie.VCExprAST
     public virtual Result VisitIfThenElseOp (VCExprNAry! node, Arg arg) {

       return StandardResult(node, arg);

     }

+    public virtual Result VisitCustomOp     (VCExprNAry! node, Arg arg) {

+      return StandardResult(node, arg);

+    }

     public virtual Result VisitAddOp            (VCExprNAry! node, Arg arg) {

       return StandardResult(node, arg);

     }

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index b5f35b1e..dea7a445 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -278,7 +278,7 @@ namespace VC {
     }

 

     protected readonly List<Checker>/*!>!*/ checkers = new List<Checker>();

-    protected Implementation current_impl = null;

+    protected VariableSeq CurrentLocalVariables = null;

 

     // shared across each implementation; created anew for each implementation

     protected Hashtable /*Variable -> int*/ variable2SequenceNumber;

@@ -357,20 +357,20 @@ namespace VC {
 

     #region Methods for injecting pre- and postconditions

     private static void

-      ThreadInBlockExpr(Implementation impl,

-                        Block targetBlock,

-                        BlockExpr blockExpr,

-                        bool replaceWithAssert,

-                        TokenTextWriter debugWriter) {

+      ThreadInCodeExpr(Implementation impl,

+                       Block targetBlock,

+                       CodeExpr codeExpr,

+                       bool replaceWithAssert,

+                       TokenTextWriter debugWriter) {

       Contract.Requires(impl != null);

-      Contract.Requires(blockExpr != null);

+      Contract.Requires(codeExpr != null);

       Contract.Requires(targetBlock != null);

-      // Go through blockExpr and for all blocks that have a "return e"

+      // Go through codeExpr and for all blocks that have a "return e"

       // as their transfer command:

       //   Replace all "return e" with "assert/assume e"

       //   Change the transfer command to "goto targetBlock"

-      // Then add all of the blocks in blockExpr to the implementation (at the end)

-      foreach (Block b in blockExpr.Blocks) {

+      // Then add all of the blocks in codeExpr to the implementation (at the end)

+      foreach (Block b in codeExpr.Blocks) {

         Contract.Assert(b != null);

         ReturnExprCmd rec = b.TransferCmd as ReturnExprCmd;

         if (rec != null) { // otherwise it is a goto command

@@ -391,7 +391,7 @@ namespace VC {
         impl.Blocks.Add(b);

       }

       if (debugWriter != null) {

-        blockExpr.Emit(debugWriter, 1, false);

+        codeExpr.Emit(debugWriter, 1, false);

       }

       return;

     }

@@ -442,31 +442,10 @@ namespace VC {
       {

         Contract.Assert(req != null);

         Expr e = Substituter.Apply(formalProcImplSubst, req.Condition);

-        BlockExpr be = e as BlockExpr;

-        if (be == null) {

-          // This is the normal case, where the precondition is an ordinary expression

-          Cmd c = new AssumeCmd(req.tok, e);

-          insertionPoint.Cmds.Add(c);

-          if (debugWriter != null) {

-            c.Emit(debugWriter, 1);

-          }

-        } else {

-          // This is a BlockExpr, so append all of its blocks (changing return expressions

-          // to assume statements), make the insertion-point block goto the head block of the

-          // BlockExpr, and create a new empty block as the current insertion point.

-          // Here goes:  First, create the new block, which will become the new insertion

-          // point and which will serve as a target for the BlockExpr.  Move the goto's from

-          // the current insertion point to this new block.

-          Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new CmdSeq(), insertionPoint.TransferCmd);

-          k++;

-          // Second, append the BlockExpr blocks to the implementation's blocks

-          ThreadInBlockExpr(impl, nextIP, be, false, debugWriter);

-          // Third, make the old insertion-point block goto the entry block of the BlockExpr

-          Block beEntry = cce.NonNull(be.Blocks[0]);

-          insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(beEntry.Label), new BlockSeq(beEntry));

-          beEntry.Predecessors.Add(insertionPoint);

-          // Fourth, update the insertion point

-          insertionPoint = nextIP;

+        Cmd c = new AssumeCmd(req.tok, e);

+        insertionPoint.Cmds.Add(c);

+        if (debugWriter != null) {

+          c.Emit(debugWriter, 1);

         }

       }

       origStartBlock.Predecessors.Add(insertionPoint);

@@ -512,7 +491,7 @@ namespace VC {
         Contract.Assert(ens != null);

         if (!ens.Free) { // skip free ensures clauses

           Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition);

-          BlockExpr be = ens.Condition as BlockExpr;

+          CodeExpr be = ens.Condition as CodeExpr;

           if (be == null) {

             // This is the normal case, where the postcondition is an ordinary expression

             Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone());

@@ -524,17 +503,17 @@ namespace VC {
               c.Emit(debugWriter, 1);

             }

           } else {

-            // This is a BlockExpr, so append all of its blocks (changing return expressions

+            // This is a CodeExpr, so append all of its blocks (changing return expressions

             // to assert statements), insert a goto to its head block from the current insertion

             // point, and create a new empty block as the current insertion point.

             // Here goes:  First, create the new block, which will become the new insertion

-            // point and which will serve as a target for the BlockExpr.  Steal the TransferCmd

+            // point and which will serve as a target for the CodeExpr.  Steal the TransferCmd

             // from insertionPoint, since insertionPoint's TransferCmd will soon be replaced anyhow.

             Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new CmdSeq(), insertionPoint.TransferCmd);

             k++;

-            // Second, append the BlockExpr blocks to the implementation's blocks

-            ThreadInBlockExpr(impl, nextIP, be, true, debugWriter);

-            // Third, make the old insertion-point block goto the entry block of the BlockExpr

+            // Second, append the CodeExpr blocks to the implementation's blocks

+            ThreadInCodeExpr(impl, nextIP, be, true, debugWriter);

+            // Third, make the old insertion-point block goto the entry block of the CodeExpr

             Block beEntry = cce.NonNull(be.Blocks[0]);

             insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(beEntry.Label), new BlockSeq(beEntry));

             beEntry.Predecessors.Add(insertionPoint);

@@ -691,6 +670,14 @@ namespace VC {
       return whereClauses;

     }

 

+    protected static void RestoreParamWhereClauses(Implementation impl) {

+      Contract.Requires(impl != null);

+      // We no longer need the where clauses on the out parameters, so we remove them to restore the situation from before VC generation

+      foreach (Formal f in impl.OutParams) {

+        Contract.Assert(f != null);

+        f.TypedIdent.WhereExpr = null;

+      }

+    }

     #endregion

 

 

@@ -848,7 +835,7 @@ namespace VC {
 

     protected Variable CreateIncarnation(Variable x, Absy a) {

       Contract.Requires(this.variable2SequenceNumber != null);

-      Contract.Requires(this.current_impl != null);

+      Contract.Requires(this.CurrentLocalVariables != null);

       Contract.Requires(a is Block || a is AssignCmd || a is HavocCmd);

 

       Contract.Requires(x != null);

@@ -862,8 +849,7 @@ namespace VC {
         -1;

       Variable v = new Incarnation(x, currentIncarnationNumber + 1);

       variable2SequenceNumber[x] = currentIncarnationNumber + 1;

-      Contract.Assert(current_impl != null);  // otherwise, the field current_impl wasn't set

-      current_impl.LocVars.Add(v);

+      CurrentLocalVariables.Add(v);

       incarnationOriginMap.Add((Incarnation)v, a);

       return v;

     }

@@ -962,12 +948,7 @@ namespace VC {
           IdentifierExpr v_prime_exp = new IdentifierExpr(v_prime.tok, v_prime);

           #endregion

           #region Create the assume command itself

-          Expr e = Expr.Binary(Token.NoToken,

-            BinaryOperator.Opcode.Eq,

-            v_prime_exp,

-            pred_incarnation_exp

-            );

-          AssumeCmd ac = new AssumeCmd(v.tok, e);

+          AssumeCmd ac = new AssumeCmd(v.tok, TypedExprEq(v_prime_exp, pred_incarnation_exp));

           pred.Cmds.Add(ac);

           #endregion

           #endregion

@@ -989,22 +970,46 @@ namespace VC {
 

       CmdSeq passiveCmds = new CmdSeq();

       foreach (Cmd c in b.Cmds) {

-        Contract.Assert(b != null); // walk forward over the commands because the map gets modified in a forward direction      

+        Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction      

         TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds);

       }

       b.Cmds = passiveCmds;

 

+      if (b.TransferCmd is ReturnExprCmd) {

+        ReturnExprCmd rec = (ReturnExprCmd)b.TransferCmd.Clone();

+        Substitution incarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap);

+        rec.Expr = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, rec.Expr);

+        b.TransferCmd = rec;

+      }

       #endregion

     }

 

     protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation impl) {

       Contract.Requires(impl != null);

+

+      Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies);

+

+      RestoreParamWhereClauses(impl);

+

+      #region Debug Tracing

+      if (CommandLineOptions.Clo.TraceVerify) {

+        Console.WriteLine("after conversion to passive commands");

+        EmitImpl(impl, true);

+      }

+      #endregion

+

+      return r;

+    }

+

+    protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies) {

+      Contract.Requires(blocks != null);

+      Contract.Requires(modifies != null);

       #region Convert to Passive Commands

 

       #region Topological sort -- need to process in a linearization of the partial order

       Graph<Block> dag = new Graph<Block>();

-      dag.AddSource(cce.NonNull(impl.Blocks[0])); // there is always at least one node in the graph

-      foreach (Block b in impl.Blocks) {

+      dag.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph

+      foreach (Block b in blocks) {

         GotoCmd gtc = b.TransferCmd as GotoCmd;

         if (gtc != null) {

           Contract.Assume(gtc.labelTargets != null);

@@ -1016,13 +1021,11 @@ namespace VC {
       }

       IEnumerable sortedNodes = dag.TopologicalSort();

       Contract.Assert(sortedNodes != null);

-      // assume sortedNodes != null;

       #endregion

 

       // Create substitution for old expressions

       Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();

-      Contract.Assume(impl.Proc != null);

-      foreach (IdentifierExpr ie in impl.Proc.Modifies) {

+      foreach (IdentifierExpr ie in modifies) {

         Contract.Assert(ie != null);

         if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))

           oldFrameMap.Add(ie.Decl, ie);

@@ -1049,21 +1052,8 @@ namespace VC {
       // Verify that exitBlock is indeed the unique exit block

       Contract.Assert(exitBlock != null);

       Contract.Assert(exitBlock.TransferCmd is ReturnCmd);

-

-      // We no longer need the where clauses on the out parameters, so we remove them to restore the situation from before VC generation

-      foreach (Formal f in impl.OutParams) {

-        Contract.Assert(f != null);

-        f.TypedIdent.WhereExpr = null;

-      }

       #endregion Convert to Passive Commands

 

-      #region Debug Tracing

-      if (CommandLineOptions.Clo.TraceVerify) {

-        Console.WriteLine("after conversion to passive commands");

-        EmitImpl(impl, true);

-      }

-      #endregion

-

       return (Hashtable)block2Incarnation[exitBlock];

     }

 

@@ -1095,7 +1085,7 @@ namespace VC {
       }

       #endregion

       #region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below]

- else if (c is AssignCmd) {

+      else if (c is AssignCmd) {

         AssignCmd assign = ((AssignCmd)c).AsSimpleAssignCmd; // first remove map assignments

         Contract.Assert(assign != null);

         #region Substitute all variables in E with the current map

@@ -1143,7 +1133,7 @@ namespace VC {
             }

             #endregion

             #region Create an assume command with the new variable

-            assumptions.Add(Expr.Eq(x_prime_exp, copies[i]));

+            assumptions.Add(TypedExprEq(x_prime_exp, copies[i]));

             #endregion

           }

         }

@@ -1165,7 +1155,7 @@ namespace VC {
       }

       #endregion

       #region havoc w |--> assume whereClauses, out := in( w |-> w' )

- else if (c is HavocCmd) {

+      else if (c is HavocCmd) {

         if (this.preHavocIncarnationMap == null)      // Save a copy of the incarnation map (at the top of a sequence of havoc statements)

           this.preHavocIncarnationMap = (Hashtable)incarnationMap.Clone();

 

@@ -1196,7 +1186,7 @@ namespace VC {
         }

       }

       #endregion

- else if (c is CommentCmd) {

+      else if (c is CommentCmd) {

         // comments are just for debugging and don't affect verification

       } else if (c is SugaredCmd) {

         SugaredCmd sug = (SugaredCmd)c;

@@ -1228,7 +1218,7 @@ namespace VC {
         }

       }

       #region There shouldn't be any other types of commands at this point

- else {

+      else {

         Debug.Fail("Internal Error: Passive transformation handed a command that is not one of assert,assume,havoc,assign.");

       }

       #endregion

@@ -1242,6 +1232,15 @@ namespace VC {
       #endregion

     }

 

+    NAryExpr TypedExprEq(Expr e0, Expr e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      NAryExpr e = Expr.Eq(e0, e1);

+      e.Type = Bpl.Type.Bool;

+      e.TypeParameters = SimpleTypeParamInstantiation.EMPTY;

+      return e;

+    }

+

     /// <summary>

     /// Creates a new block to add to impl.Blocks, where impl is the implementation that contains

     /// succ.  Caller must do the add to impl.Blocks.

@@ -1295,11 +1294,11 @@ namespace VC {
       return newBlock;

     }

 

-    protected void AddBlocksBetween(Implementation impl) {

-      Contract.Requires(impl != null);

+    protected void AddBlocksBetween(List<Block> blocks) {

+      Contract.Requires(blocks != null);

       #region Introduce empty blocks between join points and their multi-successor predecessors

       List<Block> tweens = new List<Block>();

-      foreach (Block b in impl.Blocks) {

+      foreach (Block b in blocks) {

         int nPreds = b.Predecessors.Length;

         if (nPreds > 1) {

           // b is a join point (i.e., it has more than one predecessor)

@@ -1311,9 +1310,9 @@ namespace VC {
           }

         }

       }

-      impl.Blocks.AddRange(tweens);  // must wait until iteration is done before changing the list

+      blocks.AddRange(tweens);  // must wait until iteration is done before changing the list

       #endregion

     }

 

   }

-}
\ No newline at end of file
+}

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 287d3a27..8ea18f3b 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -40,11 +40,8 @@ namespace VC {
         this.GenerateVCsForLazyInlining(program);

       }

       if (CommandLineOptions.Clo.StratifiedInlining > 0) {

-

         this.GenerateVCsForStratifiedInlining(program);

-

       }

-      // base();

     }

 

     private static AssumeCmd AssertTurnedIntoAssume(AssertCmd assrt) {

@@ -143,7 +140,7 @@ namespace VC {
           Contract.Assert(v != null);

           functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type), true));

         }

-        TypedIdent ti = new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool);

+        TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);

         Contract.Assert(ti != null);

         Formal returnVar = new Formal(Token.NoToken, ti, false);

         Contract.Assert(returnVar != null);

@@ -650,7 +647,7 @@ namespace VC {
           System.Console.WriteLine(" --- smoke #{0}, before passify", id);

           Emit();

         }

-        parent.current_impl = impl;

+        parent.CurrentLocalVariables = impl.LocVars;

         parent.PassifyImpl(impl, program);

         Hashtable label2Absy;

         Checker ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);

@@ -666,7 +663,7 @@ namespace VC {
         ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));

         ch.ProverDone.WaitOne();

         ProverInterface.Outcome outcome = ch.ReadOutcome();

-        parent.current_impl = null;

+        parent.CurrentLocalVariables = null;

 

         DateTime end = DateTime.Now;

         TimeSpan elapsed = end - start;

@@ -1150,7 +1147,7 @@ namespace VC {
 

         if (allow_small) {

           foreach (Block ch in Exits(b)) {

-            Contract.Assert(b != null);

+            Contract.Assert(ch != null);

             if (b == split_block && assumized_branches.Contains(ch))

               continue;

             ComputeBlockSetsHelper(ch, allow_small);

@@ -1541,9 +1538,52 @@ namespace VC {
         impl.Blocks = blocks;

 

         checker = parent.FindCheckerFor(impl, timeout);

+        Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();

+

+        ProverInterface tp = checker.TheoremProver;

+        ProverContext ctx = tp.Context;

+        Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;

+        bet.SetCodeExprConverter(

+          new CodeExprConverter(

+          delegate (CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings) {

+            VCGen vcgen = new VCGen(new Program(), null, false);

+            vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();

+            vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();

+            vcgen.CurrentLocalVariables = codeExpr.LocVars;

+            // codeExpr.Blocks.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

+

+            vcgen.ComputePredecessors(codeExpr.Blocks);

+            vcgen.AddBlocksBetween(codeExpr.Blocks);

+            Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq());

+            VCExpr startCorrect = VCGen.LetVC(

+		      codeExpr.Blocks[0],

+              null,

+              label2absy,

+		      blockVariables,

+		      bindings,

+		      ctx);

+            VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);

+

+            if (vcgen.CurrentLocalVariables.Length != 0) {

+              Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;

+              List<VCExprVar> boundVars = new List<VCExprVar>();

+              foreach (Variable v in vcgen.CurrentLocalVariables) {

+                Contract.Assert(v != null);

+                VCExprVar ev = translator.LookupVariable(v);

+                Contract.Assert(ev != null);

+                boundVars.Add(ev);

+                if (v.TypedIdent.Type.Equals(Bpl.Type.Bool)) {

+                  // add an antecedent (tickleBool ev) to help the prover find a possible trigger

+                  vce = checker.VCExprGen.Implies(checker.VCExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce);

+                }

+              }

+              vce = checker.VCExprGen.Forall(boundVars, new List<VCTrigger>(), vce);

+            }

+            return vce;

+          }

+		  ));

 

-        Hashtable/*<int, Absy!>*/ label2absy;

-        VCExpr vc = parent.GenerateVC(impl, null, out label2absy, checker);

+        VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker);

         Contract.Assert(vc != null);

 

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

@@ -1618,17 +1658,25 @@ namespace VC {
     #endregion

 

 

-    protected VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch) {

+    protected VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)

+    {

       Contract.Requires(impl != null);

       Contract.Requires(ch != null);

       Contract.Ensures(Contract.ValueAtReturn(out label2absy) != null);

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

 

+      label2absy = new Hashtable/*<int, Absy!>*/();

+      return GenerateVCAux(impl, controlFlowVariable, label2absy, ch);

+    }

+

+    protected VCExpr GenerateVCAux(Implementation/*!*/ impl, Variable controlFlowVariable, Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch) {

+      Contract.Requires(impl != null);

+      Contract.Requires(ch != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

 

       TypecheckingContext tc = new TypecheckingContext(null);

       impl.Typecheck(tc);

 

-      label2absy = new Hashtable/*<int, Absy!>*/();

       VCExpr vc;

       switch (CommandLineOptions.Clo.vcVariety) {

         case CommandLineOptions.VCVariety.Structured:

@@ -1676,9 +1724,9 @@ namespace VC {
 

     public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback){

       Contract.Requires(impl != null);

-       Contract.Requires(program != null);

+      Contract.Requires(program != null);

       Contract.Requires(callback != null);

-      Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);

+      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       if (impl.SkipVerification) {

         return Outcome.Inconclusive; // not sure about this one

       } 

@@ -2140,7 +2188,7 @@ namespace VC {
     }

 

     // Return the VC for the impl (don't pass it to the theorem prover).

-    // GetVC is a cheap imitation of VerifyImplementatio, except that the VC is not passed to the theorem prover.

+    // GetVC is a cheap imitation of VerifyImplementation, except that the VC is not passed to the theorem prover.

     private void GetVC(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback, out VCExpr/*!*/ vc, out Hashtable/*<int, Absy!>*//*!*/ label2absy, out StratifiedInliningErrorReporter/*!*/ reporter) {

       Contract.Requires(impl != null);

       Contract.Requires(program != null);

@@ -2914,7 +2962,7 @@ namespace VC {
     Contract.Requires(program != null);

       impl.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

 

-      current_impl = impl;

+      CurrentLocalVariables = impl.LocVars;

       variable2SequenceNumber = new Hashtable/*Variable -> int*/();

       incarnationOriginMap = new Dictionary<Incarnation, Absy>();

 

@@ -3124,7 +3172,7 @@ namespace VC {
     {

       Contract.Requires(impl != null);

       Contract.Requires(program != null);

-    Contract.Ensures(Contract.Result<Hashtable>() != null);

+      Contract.Ensures(Contract.Result<Hashtable>() != null);

 

       Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = new Hashtable/*TransferCmd->ReturnCmd*/();

       Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);

@@ -3157,7 +3205,6 @@ namespace VC {
             cc.Add(c);

           }

         }

-

         // add cc and the preconditions to new blocks preceding impl.Blocks[0]

         InjectPreconditions(impl, cc);

 

@@ -3192,7 +3239,7 @@ namespace VC {
       }

       #endregion

 

-      AddBlocksBetween(impl);

+      AddBlocksBetween(impl.Blocks);

       

       #region Debug Tracing

       if (CommandLineOptions.Clo.TraceVerify) 

@@ -3207,6 +3254,7 @@ namespace VC {
       }

       

       Hashtable exitIncarnationMap = Convert2PassiveCmd(impl);

+

       if (implName2LazyInliningInfo != null && implName2LazyInliningInfo.ContainsKey(impl.Name))

       {

         LazyInliningInfo info = implName2LazyInliningInfo[impl.Name];

@@ -3296,7 +3344,7 @@ namespace VC {
       Contract.Requires(program != null);

       Contract.Requires(implName != null);

       Contract.Requires(values != null);

-    Contract.Ensures(Contract.Result<Counterexample>() != null);

+      Contract.Ensures(Contract.Result<Counterexample>() != null);

 

       VCExprTranslator vcExprTranslator = cce.NonNull(context.exprTranslator);

       Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;

@@ -4280,15 +4328,14 @@ namespace VC {
     //    }

 

     static VCExpr LetVC(Block startBlock,

-                         Variable controlFlowVariable,

-                         Hashtable/*<int, Absy!>*/ label2absy,

-                         ProverContext proverCtxt) {

+                        Variable controlFlowVariable,

+                        Hashtable/*<int, Absy!>*/ label2absy,

+                        ProverContext proverCtxt) {

       Contract.Requires(startBlock != null);

       Contract.Requires(controlFlowVariable != null);

       Contract.Requires(label2absy != null);

       Contract.Requires(proverCtxt != null);

 

-

       Contract.Ensures(Contract.Result<VCExpr>() != null);

 

       Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();

@@ -4298,11 +4345,11 @@ namespace VC {
     }

 

     static VCExpr LetVC(Block block,

-                         Variable controlFlowVariable,

-                         Hashtable/*<int, Absy!>*/ label2absy,

-                         Hashtable/*<Block, VCExprVar!>*/ blockVariables,

-                         List<VCExprLetBinding/*!*/>/*!*/ bindings,

-                         ProverContext proverCtxt)

+                        Variable controlFlowVariable,

+                        Hashtable/*<int, Absy!>*/ label2absy,

+                        Hashtable/*<Block, VCExprVar!>*/ blockVariables,

+                        List<VCExprLetBinding/*!*/>/*!*/ bindings,

+                        ProverContext proverCtxt)

     {

       Contract.Requires(block != null);

       Contract.Requires(controlFlowVariable != null);

@@ -4311,7 +4358,7 @@ namespace VC {
       Contract.Requires(cce.NonNullElements(bindings));

       Contract.Requires(proverCtxt != null);

 

-    Contract.Ensures(Contract.Result<VCExpr>() != null);

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

 

       VCExpressionGenerator gen = proverCtxt.ExprGen;

       Contract.Assert(gen != null);

@@ -4326,7 +4373,12 @@ namespace VC {
         VCExpr SuccCorrect;

         GotoCmd gotocmd = block.TransferCmd as GotoCmd;

         if (gotocmd == null) {

-          SuccCorrect = VCExpressionGenerator.True;

+          ReturnExprCmd re = block.TransferCmd as ReturnExprCmd;

+          if (re == null) {

+            SuccCorrect = VCExpressionGenerator.True;

+          } else {

+            SuccCorrect = proverCtxt.BoogieExprTranslator.Translate(re.Expr);

+          }

         } else {

           Contract.Assert( gotocmd.labelTargets != null);

           List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);

@@ -4364,7 +4416,7 @@ namespace VC {
       Contract.Requires(label2absy != null);

       Contract.Requires(blockEquations != null);

       Contract.Requires(proverCtxt != null);

-    Contract.Ensures(Contract.Result<VCExpr>() != null);

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

 

       VCExpressionGenerator gen = proverCtxt.ExprGen;

       Contract.Assert(gen != null);

@@ -4807,9 +4859,17 @@ namespace VC {
 

       Contract.Ensures(Contract.Result<Graph<Block>>() != null);

 

+      return GraphFromBlocks(impl.Blocks);

+    }

+

+    static Graph<Block> GraphFromBlocks(List<Block> blocks) {

+      Contract.Requires(blocks != null);

+

+      Contract.Ensures(Contract.Result<Graph<Block>>() != null);

+

       Graph<Block> g = new Graph<Block>();

-      g.AddSource(cce.NonNull(impl.Blocks[0])); // there is always at least one node in the graph

-      foreach (Block b in impl.Blocks) {

+      g.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph

+      foreach (Block b in blocks) {

         Contract.Assert(b != null);

         GotoCmd gtc = b.TransferCmd as GotoCmd;

         if (gtc != null) {

diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
index d44547a8..12543cd5 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/VCGeneration/VCDoomed.cs
@@ -331,7 +331,6 @@ namespace VC {
 

       PassifyProgram(impl);

 

-

       #endregion

       //EmitImpl(impl,false);

 

@@ -1284,7 +1283,7 @@ namespace VC {
       Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);

       Contract.Assert(exitBlock != null);

 

-      AddBlocksBetween(impl);

+      AddBlocksBetween(impl.Blocks);

 

       #region Insert pre- and post-conditions and where clauses as assume and assert statements

       {

@@ -1323,9 +1322,8 @@ namespace VC {
       Contract.Requires(impl != null);

       Contract.Ensures(Contract.Result<Hashtable>() != null);

 

-      current_impl = impl;

+      CurrentLocalVariables = impl.LocVars;

       Convert2PassiveCmd(impl);

-      impl = current_impl;

       return new Hashtable();

     }

 

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 64cc5c09..d29223a9 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -15,11 +15,11 @@ namespace VC {
   public class VCContext 

   {

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(Label2absy!=null);

+    void ObjectInvariant() 

+    {

+      Contract.Invariant(Label2absy!=null);

       Contract.Invariant(Ctxt != null);

-}

+    }

 

     [Rep] public readonly Hashtable/*<int, Absy!>*/ Label2absy;

     [Rep] public readonly ProverContext Ctxt;

@@ -52,9 +52,9 @@ void ObjectInvariant()
     public static VCExpr Block(Block b, VCExpr N, VCContext ctxt)

       //modifies ctxt.*;

     {

-    Contract.Requires(b != null);

-    Contract.Requires(N != null);

-    Contract.Requires(ctxt != null);

+      Contract.Requires(b != null);

+      Contract.Requires(N != null);

+      Contract.Requires(ctxt != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

 

       VCExpressionGenerator gen = ctxt.Ctxt.ExprGen;