Boogie: Commented out all occurences of repeated inherited contracts - makes fewer error messages when compiling with runtime checking on.

26 files changed, 1728 insertions, 1638 deletions

diff --git a/Source/AIFramework/Lattice.cs b/Source/AIFramework/Lattice.cs
index 78f87421..8d7f6c45 100644
--- a/Source/AIFramework/Lattice.cs
+++ b/Source/AIFramework/Lattice.cs
@@ -792,7 +792,7 @@ namespace Microsoft.AbstractInterpretationFramework {
 

     public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {

       //Contract.Requires(args != null);

-      Contract.Requires(f != null);

+      //Contract.Requires(f != null);

       understandsCount++;

       return lattice.Understands(f, args);

     }

diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs
index 169156b0..b3c702d7 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.cs
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs
@@ -329,7 +329,7 @@ namespace Microsoft.AbstractInterpretationFramework {
     }

 

     public override string/*!*/ ToString(Element/*!*/ element) {

-      Contract.Requires(element != null);

+      //Contract.Requires(element != null);

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

       Elt e = (Elt)element;

 

@@ -416,8 +416,8 @@ namespace Microsoft.AbstractInterpretationFramework {
     /// Perform the pointwise widening of the elements in the map

     /// </summary>

     public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {

-      Contract.Requires((second != null));

-      Contract.Requires((first != null));

+      //Contract.Requires((second != null));

+      //Contract.Requires((first != null));

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

       Elt a = (Elt)first;

       Elt b = (Elt)second;

@@ -568,7 +568,7 @@ namespace Microsoft.AbstractInterpretationFramework {
     }

 

     public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {

-      Contract.Requires(element != null);

+      //Contract.Requires(element != null);

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

       if (IsTop(element)) {

         return propExprFactory.True;

@@ -765,8 +765,8 @@ namespace Microsoft.AbstractInterpretationFramework {
 

 

     public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {

-      Contract.Requires(args != null);

-      Contract.Requires(f != null);

+      //Contract.Requires(args != null);

+      //Contract.Requires(f != null);

       return f.Equals(Prop.And) ||

              f.Equals(Value.Eq) ||

              microLattice.Understands(f, args);

diff --git a/Source/AbsInt/ExprFactories.cs b/Source/AbsInt/ExprFactories.cs
index 7979f061..34564cac 100644
--- a/Source/AbsInt/ExprFactories.cs
+++ b/Source/AbsInt/ExprFactories.cs
@@ -27,42 +27,42 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     }

 

     public AI.IFunApp Not(AI.IExpr p) {

-      Contract.Requires(p != null);

+      //Contract.Requires(p != null);

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

 

       return Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, IExpr2Expr(p));

     }

 

     public AI.IFunApp And(AI.IExpr p, AI.IExpr q) {

-      Contract.Requires(p != null);

-      Contract.Requires(q != null);

+      //Contract.Requires(p != null);

+      //Contract.Requires(q != null);

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

 

       return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));

     }

 

     public AI.IFunApp Or(AI.IExpr p, AI.IExpr q) {

-      Contract.Requires(p != null);

-      Contract.Requires(q != null);

+      //Contract.Requires(p != null);

+      //Contract.Requires(q != null);

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

       return Expr.Binary(BinaryOperator.Opcode.Or, IExpr2Expr(p), IExpr2Expr(q));

     }

 

     public AI.IFunApp Implies(AI.IExpr p, AI.IExpr q) {

-      Contract.Requires(p != null);

-      Contract.Requires(q != null);

+      //Contract.Requires(p != null);

+      //Contract.Requires(q != null);

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

       return Expr.Binary(BinaryOperator.Opcode.Imp, IExpr2Expr(p), IExpr2Expr(q));

     }

 

     public AI.IFunApp Exists(AI.IFunction p) {

-      Contract.Requires(p != null);

+      //Contract.Requires(p != null);

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

 

       return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;

     }

     public AI.IFunApp Exists(AI.AIType paramType, AI.FunctionBody bodygen) {

-      Contract.Requires(bodygen != null);

+      //Contract.Requires(bodygen != null);

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

 

       // generate a fresh new variable

@@ -74,13 +74,13 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     }

 

     public AI.IFunApp Forall(AI.IFunction p) {

-      Contract.Requires(p != null);

+      //Contract.Requires(p != null);

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

 

       return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;

     }

     public AI.IFunApp Forall(AI.AIType paramType, AI.FunctionBody bodygen) {

-      Contract.Requires(bodygen != null);

+      //Contract.Requires(bodygen != null);

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

 

       // generate a fresh new variable

@@ -116,15 +116,15 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 

   public class BoogieValueFactory : BoogieFactory, AI.IValueExprFactory {

     public AI.IFunApp Eq(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

+      //Contract.Requires(e0 != null);

+      //Contract.Requires(e1 != null);

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

 

       return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));

     }

     public AI.IFunApp Neq(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

+      //Contract.Requires(e0 != null);

+      //Contract.Requires(e1 != null);

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

       return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));

     }

@@ -132,15 +132,15 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 

   public class BoogieNullnessFactory : BoogieFactory, AI.INullnessFactory {

     public AI.IFunApp Eq(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

+      //Contract.Requires(e0 != null);

+      //Contract.Requires(e1 != null);

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

       return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));

     }

 

     public AI.IFunApp Neq(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

+      //Contract.Requires(e0 != null);

+      //Contract.Requires(e1 != null);

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

       return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));

     }

@@ -163,14 +163,14 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 

   public class BoogieLinearFactory : BoogieIntFactory, AI.ILinearExprFactory {

     public AI.IFunApp AtMost(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

+      //Contract.Requires(e0 != null);

+      //Contract.Requires(e1 != null);

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

       return Expr.Le(IExpr2Expr(e0), IExpr2Expr(e1));

     }

     public AI.IFunApp Add(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

+      //Contract.Requires(e0 != null);

+      //Contract.Requires(e1 != null);

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

       return Expr.Add(IExpr2Expr(e0), IExpr2Expr(e1));

     }

@@ -208,8 +208,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       }

     }

     public AI.IFunApp And(AI.IExpr p, AI.IExpr q) {

-      Contract.Requires(p != null);

-      Contract.Requires(q != null);

+      //Contract.Requires(p != null);

+      //Contract.Requires(q != null);

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

 

       return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));

@@ -232,7 +232,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     /// </summary>

     [Pure]

     public bool IsTypeConstant(AI.IExpr t) {

-      Contract.Requires(t != null);

+      //Contract.Requires(t != null);

       Contract.Ensures(Contract.Result<bool>() == (t is Constant));

       return t is Constant;

     }

@@ -242,8 +242,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     /// </summary>

     [Pure]

     public bool IsTypeEqual(AI.IExpr t0, AI.IExpr t1) {

-      Contract.Requires(t0 != null);

-      Contract.Requires(t1 != null);

+      //Contract.Requires(t0 != null);

+      //Contract.Requires(t1 != null);

       Constant c0 = t0 as Constant;

       Constant c1 = t1 as Constant;

       return c0 != null && c1 != null && c0 == c1;

@@ -254,8 +254,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     /// </summary>

     [Pure]

     public bool IsSubType(AI.IExpr t0, AI.IExpr t1) {

-      Contract.Requires(t0 != null);

-      Contract.Requires(t1 != null);

+      //Contract.Requires(t0 != null);

+      //Contract.Requires(t1 != null);

 

       Contract.Assert(false);  // BUGBUG: TODO

       throw new cce.UnreachableException();

@@ -266,8 +266,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     /// that "t0" and "t1" both represent types.

     /// </summary>

     public AI.IExpr JoinTypes(AI.IExpr t0, AI.IExpr t1) {

-      Contract.Requires(t0 != null);

-      Contract.Requires(t1 != null);

+      //Contract.Requires(t0 != null);

+      //Contract.Requires(t1 != null);

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

 

 

@@ -279,8 +279,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       //PM: We need this assume because Boogie does not yet allow us to use the

       //PM: inherited precondition "requires IsTypeConstant(type)".

       //PM: Note that that precondition is currently commented out.

-      Contract.Requires(e != null);

-      Contract.Requires(type != null);

+      //Contract.Requires(e != null);

+      //Contract.Requires(type != null);

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

 

       Contract.Assume(type is Constant);

@@ -295,12 +295,13 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     }

 

     public AI.IFunApp IsA(AI.IExpr e, AI.IExpr type) {

+      //Contract.Requires(e != null);

+      //Contract.Requires(type != null);

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

       //PM: We need this assume because Boogie does not yet allow us to use the

       //PM: inherited precondition "requires IsTypeConstant(type)".

       //PM: Note that that precondition is currently commented out.

-      Contract.Requires(e != null);

-      Contract.Requires(type != null);

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

+      

 

       Contract.Assume(type is Constant);

       Contract.Assert(false);

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index e8fdc385..1f5dca86 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1121,7 +1121,7 @@ namespace Microsoft.Boogie {
     }

 

     public override void Emit(TokenTextWriter stream, int level) {

-      Contract.Requires(stream != null);

+      //Contract.Requires(stream != null);

       stream.Write(this, level, "var ");

       EmitAttributes(stream);

       EmitVitals(stream, level);

@@ -1135,7 +1135,7 @@ namespace Microsoft.Boogie {
       this.TypedIdent.Emit(stream);

     }

     public override void Resolve(ResolutionContext rc) {

-      Contract.Requires(rc != null);

+      //Contract.Requires(rc != null);

       this.TypedIdent.Resolve(rc);

     }

     public void ResolveWhere(ResolutionContext rc) {

@@ -1146,13 +1146,13 @@ namespace Microsoft.Boogie {
       ResolveAttributes(rc);

     }

     public override void Typecheck(TypecheckingContext tc) {

-      Contract.Requires(tc != null);

+      //Contract.Requires(tc != null);

       TypecheckAttributes(tc);

       this.TypedIdent.Typecheck(tc);

     }

     [Pure]

     public object DoVisit(AI.ExprVisitor visitor) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

       return visitor.VisitVariable(this);

     }

   }

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index f5771f7f..3797d551 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -598,7 +598,7 @@ namespace Microsoft.Boogie {
       }

     }

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

-      Contract.Requires(args != null);

+      //Contract.Requires(args != null);

       Contract.Ensures(Contract.Result<Microsoft.AbstractInterpretationFramework.IFunApp>() != null);

       Contract.Assert(args.Count == 0);

       return this;

@@ -622,7 +622,7 @@ namespace Microsoft.Boogie {
     }

     [Pure]

     public object DoVisit(AI.ExprVisitor visitor) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

       return visitor.VisitFunApp(this);

     }

 

@@ -923,14 +923,14 @@ namespace Microsoft.Boogie {
       }

 

       public AI.IFunApp CloneWithArguments(IList newargs) {

-        Contract.Requires(newargs != null);

+        //Contract.Requires(newargs != null);

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

         return this;

       }

 

       [Pure]

       public object DoVisit(AI.ExprVisitor visitor) {

-        Contract.Requires(visitor != null);

+        //Contract.Requires(visitor != null);

         return visitor.VisitFunApp(this);

       }

 

@@ -1038,11 +1038,11 @@ namespace Microsoft.Boogie {
     }

     [Pure]

     public object DoVisit(AI.ExprVisitor visitor) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

       return visitor.VisitFunApp(this);

     }

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

-      Contract.Requires(args != null);

+      //Contract.Requires(args != null);

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

       Contract.Assume(args.Count == 1);

       AI.IExpr/*!*/ iexpr = (AI.IExpr)cce.NonNull(args[0]);

@@ -1985,7 +1985,7 @@ namespace Microsoft.Boogie {
 

     virtual public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

       //Contract.Requires(stream != null);

-      Contract.Requires(args != null);

+      //Contract.Requires(args != null);

       this.name.Emit(stream, 0xF0, false);

       stream.Write("(");

       args.Emit(stream);

@@ -1993,7 +1993,7 @@ namespace Microsoft.Boogie {
     }

     public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {

       //Contract.Requires(subjectForErrorReporting != null);

-      Contract.Requires(rc != null);

+      //Contract.Requires(rc != null);

       if (Func != null) {

         // already resolved

         return;

@@ -2291,14 +2291,14 @@ namespace Microsoft.Boogie {
       }

     }

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

-      Contract.Requires(args != null);

+      //Contract.Requires(args != null);

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

       return new NAryExpr(this.tok, this.Fun, BoogieFactory.IExprArray2ExprSeq(args));

     }

 

     [Pure]

     public object DoVisit(AI.ExprVisitor visitor) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

       return visitor.VisitFunApp(this);

     }

 

@@ -2715,7 +2715,7 @@ namespace Microsoft.Boogie {
 

     public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {

       //Contract.Requires(subjectForErrorReporting != null);

-      Contract.Requires(rc != null);

+      //Contract.Requires(rc != null);

       // PR: nothing?

     }

 

@@ -2810,7 +2810,7 @@ namespace Microsoft.Boogie {
     }

     [Pure]

     public object DoVisit(AI.ExprVisitor visitor) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

       return this;

     }

 

@@ -3013,7 +3013,7 @@ namespace Microsoft.Boogie {
       }

     }

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

-      Contract.Requires(args != null);

+      //Contract.Requires(args != null);

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

       AI.IFunApp retFun;

 

@@ -3033,7 +3033,7 @@ namespace Microsoft.Boogie {
 

     [Pure]

     public object DoVisit(AI.ExprVisitor visitor) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

       return visitor.VisitFunApp(this);

     }

 

@@ -3161,7 +3161,7 @@ namespace Microsoft.Boogie {
       }

     }

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

-      Contract.Requires(args != null);

+      //Contract.Requires(args != null);

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

       AI.IFunApp/*!*/ retFun;

 

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index c30211ca..e677f85c 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -257,7 +257,7 @@ namespace Microsoft.Boogie {
 

       [Pure]

       public object DoVisit(AI.ExprVisitor visitor) {

-        Contract.Requires(visitor != null);

+        //Contract.Requires(visitor != null);

         return visitor.VisitFunApp(this);

       }

 

@@ -284,7 +284,7 @@ namespace Microsoft.Boogie {
       }

 

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

-        Contract.Requires(args != null);

+        //Contract.Requires(args != null);

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

         Contract.Assume(args.Count == 1);

 

@@ -336,7 +336,7 @@ namespace Microsoft.Boogie {
 

       [Pure]

       public object DoVisit(AI.ExprVisitor visitor) {

-        Contract.Requires(visitor != null);

+        //Contract.Requires(visitor != null);

         return visitor.VisitFunction(this);

       }

 

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

       }

       public AI.IFunction CloneWithBody(AI.IExpr body) {

-        Contract.Requires(body != null);

+        //Contract.Requires(body != null);

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

         BinderExpr realquant;

 

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 7f3baa67..288f5769 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -904,7 +904,7 @@ namespace Microsoft.Boogie {
     public override bool Unify(Type that, TypeVariableSeq unifiableVariables, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {

       //Contract.Requires(unifiableVariables != null);

       //Contract.Requires(that != null);

-      Contract.Requires(cce.NonNullElements(unifier));

+      //Contract.Requires(cce.NonNullElements(unifier));

       // an idempotent substitution that describes the

       // unification result up to a certain point

 

@@ -1068,7 +1068,7 @@ namespace Microsoft.Boogie {
                                IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {

       //Contract.Requires(that != null);

       //Contract.Requires(unifiableVariables != null);

-      Contract.Requires(cce.NonNullElements(unifier));

+      //Contract.Requires(cce.NonNullElements(unifier));

       that = that.Expanded;

       if (that is TypeProxy || that is TypeVariable) {

         return that.Unify(this, unifiableVariables, unifier);

@@ -1218,9 +1218,9 @@ Contract.Requires(that != null);
     public override bool Equals(Type that,

                                 TypeVariableSeq/*!*/ thisBoundVariables,

                                 TypeVariableSeq/*!*/ thatBoundVariables) {

-      Contract.Requires(thisBoundVariables != null);

-      Contract.Requires(thatBoundVariables != null);

-      Contract.Requires(that != null);

+      //Contract.Requires(thisBoundVariables != null);

+      //Contract.Requires(thatBoundVariables != null);

+      //Contract.Requires(that != null);

       System.Diagnostics.Debug.Fail("UnresolvedTypeIdentifier.Equals should never be called");

       return false; // to make the compiler happy      

     }

@@ -1230,9 +1230,9 @@ Contract.Requires(that != null);
     public override bool Unify(Type that,

                                TypeVariableSeq/*!*/ unifiableVariables,

                                IDictionary<TypeVariable/*!*/, Type/*!*/> result) {

-      Contract.Requires(unifiableVariables != null);

-      Contract.Requires(cce.NonNullElements(result));

-      Contract.Requires(that != null);

+      //Contract.Requires(unifiableVariables != null);

+      //Contract.Requires(cce.NonNullElements(result));

+      //Contract.Requires(that != null);

       {

         Contract.Assert(false);

         throw new cce.UnreachableException();

@@ -1254,7 +1254,7 @@ Contract.Requires(that != null);
     //-----------  Substitution of free variables with types not containing bound variables  -----------------

 

     public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {

-      Contract.Requires(cce.NonNullElements(subst));

+      //Contract.Requires(cce.NonNullElements(subst));

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

       {

         Contract.Assert(false);

@@ -1266,7 +1266,7 @@ Contract.Requires(that != null);
 

     [Pure]

     public override int GetHashCode(TypeVariableSeq boundVariables) {

-      Contract.Requires(boundVariables != null);

+      //Contract.Requires(boundVariables != null);

       {

         Contract.Assert(false);

         throw new cce.UnreachableException();

@@ -1276,7 +1276,7 @@ Contract.Requires(that != null);
     //-----------  Resolution  ----------------------------------

 

     public override Type ResolveType(ResolutionContext rc) {

-      Contract.Requires(rc != null);

+      //Contract.Requires(rc != null);

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

       // first case: the type name denotes a bitvector-type

       if (Name.StartsWith("bv") && Name.Length > 2) {

@@ -1392,7 +1392,7 @@ Contract.Requires(that != null);
     }

 

     public override Absy StdDispatch(StandardVisitor visitor) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

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

       return visitor.VisitUnresolvedTypeIdentifier(this);

     }

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 240920c5..4eafdbbb 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -18,7 +18,7 @@ namespace Microsoft.Boogie {
     }

 

     public override Implementation VisitImplementation(Implementation node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       //Console.WriteLine("Procedure {0}", node.Name);

       Implementation/*!*/ impl = base.VisitImplementation(node);

@@ -181,7 +181,7 @@ namespace Microsoft.Boogie {
     }

 

     public override Expr VisitOldExpr(OldExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       insideOldExpr++;

       node.Expr = this.VisitExpr(node.Expr);

@@ -190,7 +190,7 @@ namespace Microsoft.Boogie {
     }

 

     public override Expr VisitIdentifierExpr(IdentifierExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       if (node.Decl != null) {

         usedVars.Add(node.Decl);

diff --git a/Source/Provers/Isabelle/Prover.cs b/Source/Provers/Isabelle/Prover.cs
index 696095eb..3544458e 100644
--- a/Source/Provers/Isabelle/Prover.cs
+++ b/Source/Provers/Isabelle/Prover.cs
@@ -936,7 +936,7 @@ namespace Microsoft.Boogie.Isabelle {
     public bool VisitBvConcatOp(VCExprNAry node, B2I b2i) {

       //Contract.Requires(node != null);

       //Contract.Requires(b2i != null);

-      Contract.Requires(node.Length >= 2);

+      //Contract.Requires(node.Length >= 2);

 

       VCExpr child1 = node[0];

       Contract.Assert(child1 != null);

diff --git a/Source/Provers/Simplify/Prover.cs b/Source/Provers/Simplify/Prover.cs
index b789e588..e4a72a89 100644
--- a/Source/Provers/Simplify/Prover.cs
+++ b/Source/Provers/Simplify/Prover.cs
@@ -507,7 +507,7 @@ namespace Microsoft.Boogie.Simplify {
 

     protected override void DoBeginCheck(string descriptiveName, string formula) {

       //Contract.Requires(descriptiveName != null);

-      Contract.Requires(formula != null);

+      //Contract.Requires(formula != null);

       //simplify.Refresh();

       //this.Comment("@@@@ Virtual Memory:  " + simplify.PeakVirtualMemorySize64);

       //this.Comment("@@@@ Working Set:  " + simplify.PeakWorkingSet64);

diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index d300a685..1f563c0f 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -384,7 +384,7 @@ namespace Microsoft.Boogie.Simplify {
     public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {

       //Contract.Requires(descriptiveName != null);

       //Contract.Requires(vc != null);

-      Contract.Requires(handler != null);

+      //Contract.Requires(handler != null);

       this.NewProblem(descriptiveName);

       this.proverException = null;

 

diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs
index 3675f6a7..638acdb0 100644
--- a/Source/Provers/Z3/Inspector.cs
+++ b/Source/Provers/Z3/Inspector.cs
@@ -36,7 +36,7 @@ void ObjectInvariant()
     }

     

     protected override bool StandardResult(VCExpr node, bool arg) {

-      Contract.Requires(node!=null);

+      //Contract.Requires(node!=null);

       VCExprNAry nary = node as VCExprNAry;

       if (nary != null) {

         VCExprLabelOp lab = nary.Op as VCExprLabelOp;

diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index c93b364d..a36ca87a 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -234,8 +234,8 @@ namespace Microsoft.Boogie.Z3
     }

 

     protected override void DoBeginCheck(string descriptiveName, string formula) {

-      Contract.Requires(descriptiveName != null);

-      Contract.Requires(formula != null);

+      //Contract.Requires(descriptiveName != null);

+      //Contract.Requires(formula != null);

       ToWriteLine(formula);

       ToWriteLine(String.Format(";   END OF FORMULA {0} - {1}", NumFormulasChecked.ToString(), descriptiveName));

       ToFlush();

@@ -254,7 +254,7 @@ namespace Microsoft.Boogie.Z3
     }

 

     public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler) {

-      Contract.Requires(handler != null);

+      //Contract.Requires(handler != null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       //ProverOutcome outcome;

       bool isInvalid = false;

@@ -920,7 +920,7 @@ namespace Microsoft.Boogie.Z3
     }

 

     public override void Print(TextWriter writer) {

-      Contract.Requires(writer != null);

+      //Contract.Requires(writer != null);

       if (CommandLineOptions.Clo.PrintErrorModel == 4) {

         PrintReadableModel(writer);

         return;

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 3813c63b..9289b5b7 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -53,7 +53,7 @@ void ObjectInvariant()
     }

     

     protected override Microsoft.Boogie.Simplify.ProverProcess CreateProverProcess(string proverPath) {

-    Contract.Requires(proverPath!= null);

+    //Contract.Requires(proverPath!= null);

     Contract.Ensures(Contract.Result<Microsoft.Boogie.Simplify.ProverProcess>() != null);

 

 

@@ -66,7 +66,7 @@ void ObjectInvariant()
     }

 

     protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {

-      Contract.Requires(opts != null);

+      //Contract.Requires(opts != null);

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

 

       return new Z3VCExprTranslator(gen, (Z3InstanceOptions) opts);

@@ -74,9 +74,9 @@ void ObjectInvariant()
 

     public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)

     {

-      Contract.Requires(descriptiveName != null);

-      Contract.Requires(vc != null);

-      Contract.Requires(handler != null);

+      //Contract.Requires(descriptiveName != null);

+      //Contract.Requires(vc != null);

+      //Contract.Requires(handler != null);

       FireUpInspector();

       if (inspector != null) {

         inspector.NewProblem(descriptiveName, vc, handler);

@@ -115,7 +115,7 @@ void ObjectInvariant()
 

     protected override bool Parse(string opt)

     {

-      Contract.Requires(opt!=null);

+      //Contract.Requires(opt!=null);

       return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||

              ParseString(opt, "INSPECTOR", ref Inspector) ||

              ParseBool(opt, "DIST", ref DistZ3) ||

@@ -211,7 +211,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
     } }

 

     public override LineariserOptions AddLetVariable(VCExprVar furtherVar) {

-      Contract.Requires(furtherVar != null);

+      //Contract.Requires(furtherVar != null);

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

 

       List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();

@@ -221,7 +221,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
     }

     

     public override LineariserOptions AddLetVariables(List<VCExprVar/*!>!*/> furtherVars) {

-      Contract.Requires(furtherVars != null);

+      //Contract.Requires(furtherVars != null);

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

 

       List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/> ();

@@ -292,14 +292,14 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
 

     public override string Lookup(VCExprVar var)

     {

-      Contract.Requires(var != null);

+      //Contract.Requires(var != null);

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

 

       return Namer.Lookup(var);

     }

     

     public override string translate(VCExpr expr, int polarity) {

-      Contract.Requires(expr != null);

+      //Contract.Requires(expr != null);

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

 

       DateTime start = DateTime.Now;

@@ -385,8 +385,8 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
 

     public override object SpawnProver(ProverOptions popts, object ctxt)

     {

-      Contract.Requires(popts != null);

-      Contract.Requires(ctxt != null);

+      //Contract.Requires(popts != null);

+      //Contract.Requires(ctxt != null);

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

 

       Z3InstanceOptions opts = cce.NonNull((Z3InstanceOptions)popts);

@@ -396,8 +396,8 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
     }

 

     public override object NewProverContext(ProverOptions options) {

-      Contract.Requires(options != null);

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

+      //Contract.Requires(options != null);

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

 

       if (CommandLineOptions.Clo.BracketIdsInVC < 0) {

         CommandLineOptions.Clo.BracketIdsInVC = 0;

diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs
index 7cdc6f4f..cd01e325 100644
--- a/Source/Provers/Z3/TypeDeclCollector.cs
+++ b/Source/Provers/Z3/TypeDeclCollector.cs
@@ -73,7 +73,7 @@ void ObjectInvariant()
 

     // not used

     protected override bool StandardResult(VCExpr node, bool arg) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

       return true;

     }

 

diff --git a/Source/VCExpr/BigLiteralAbstracter.cs b/Source/VCExpr/BigLiteralAbstracter.cs
index 63d87e17..7eb93541 100644
--- a/Source/VCExpr/BigLiteralAbstracter.cs
+++ b/Source/VCExpr/BigLiteralAbstracter.cs
@@ -15,23 +15,24 @@ using Microsoft.Basetypes;
 // constants. This is necessary for Simplify, which cannot deal with

 // literals larger than 32 bits

 

-namespace Microsoft.Boogie.VCExprAST

-{

+namespace Microsoft.Boogie.VCExprAST {

 

   public class BigLiteralAbstracter : MutatingVCExprVisitor<bool>, ICloneable {

 

-    public BigLiteralAbstracter(VCExpressionGenerator gen) :base(gen){

+    public BigLiteralAbstracter(VCExpressionGenerator gen)

+      : base(gen) {

       Contract.Requires(gen != null);

       DummyVar = gen.Variable("x", Type.Int);

-      IncAxioms = new List<VCExpr> ();

-      Literals = new List<KeyValuePair<BigNum, VCExprVar>> ();

+      IncAxioms = new List<VCExpr>();

+      Literals = new List<KeyValuePair<BigNum, VCExprVar>>();

     }

 

-    private BigLiteralAbstracter(BigLiteralAbstracter abstracter) :base(abstracter.Gen){

+    private BigLiteralAbstracter(BigLiteralAbstracter abstracter)

+      : base(abstracter.Gen) {

       Contract.Requires(abstracter != null);

       DummyVar = abstracter.DummyVar;

-      IncAxioms = new List<VCExpr> (abstracter.IncAxioms);

-      Literals = new List<KeyValuePair<BigNum, VCExprVar>> (abstracter.Literals);

+      IncAxioms = new List<VCExpr>(abstracter.IncAxioms);

+      Literals = new List<KeyValuePair<BigNum, VCExprVar>>(abstracter.Literals);

     }

 

     public Object Clone() {

@@ -59,10 +60,9 @@ namespace Microsoft.Boogie.VCExprAST
     private readonly List<VCExpr/*!*/>/*!*/ IncAxioms;

 

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(cce.NonNullElements(IncAxioms));

-}

+    void ObjectInvariant() {

+      Contract.Invariant(cce.NonNullElements(IncAxioms));

+    }

 

     private void AddAxiom(VCExpr/*!*/ axiom) {

       Contract.Requires(axiom != null);

@@ -72,7 +72,7 @@ void ObjectInvariant()
     // Return all axioms that were added since the last time NewAxioms

     // was called

     public VCExpr GetNewAxioms() {

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

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

       VCExpr res = Gen.NAry(VCExpressionGenerator.AndOp, IncAxioms);

       IncAxioms.Clear();

       return res;

@@ -86,39 +86,38 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
     private readonly List<KeyValuePair<BigNum, VCExprVar/*!*/>>/*!*/ Literals;

 

     [ContractInvariantMethod]

-void ObjectInvariat() 

-{

-    Contract.Invariant(Literals!=null);

-      Contract.Invariant(Contract.ForAll(Literals,i=>i.Value!=null));

-}

+    void ObjectInvariat() {

+      Contract.Invariant(Literals != null);

+      Contract.Invariant(Contract.ForAll(Literals, i => i.Value != null));

+    }

+

 

-    

     private class EntryComparerC : IComparer<KeyValuePair<BigNum, VCExprVar/*!*/>> {

       public int Compare(KeyValuePair<BigNum, VCExprVar/*!*/> a,

-                         KeyValuePair<BigNum, VCExprVar/*!*/> b) {Contract.Requires(a.Value!=null);

-        Contract.Requires(b.Value!=null);

+                         KeyValuePair<BigNum, VCExprVar/*!*/> b) {

+        //Contract.Requires(a.Value!=null);

+        //Contract.Requires(b.Value!=null);

         return a.Key.CompareTo(b.Key);

       }

     }

 

-    private static readonly EntryComparerC EntryComparer = new EntryComparerC ();

+    private static readonly EntryComparerC EntryComparer = new EntryComparerC();

 

     // variable used when searching for entries in the literal list

     private readonly VCExprVar/*!*/ DummyVar;

     [ContractInvariantMethod]

-void ObjectInvarint() 

-{

-    Contract.Invariant(DummyVar!=null);

-}

+    void ObjectInvarint() {

+      Contract.Invariant(DummyVar != null);

+    }

 

 

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

-    

+

     // Construct an expression to represent the given (large) integer

     // literal. Constants are defined and axiomatised if necessary

     private VCExpr Represent(BigNum lit) {

-Contract.Requires((NegConstantDistance > lit || lit > ConstantDistance));

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

+      Contract.Requires((NegConstantDistance > lit || lit > ConstantDistance));

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

 

       if (lit.IsNegative)

         return Gen.Function(VCExpressionGenerator.SubOp,

@@ -128,14 +127,14 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
     }

 

     private VCExpr RepresentPos(BigNum lit) {

-Contract.Requires((lit > ConstantDistance));

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

-      

+      Contract.Requires((lit > ConstantDistance));

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

+

       int index = GetIndexFor(lit);

       if (index >= 0)

         // precise match

         return Literals[index].Value;

-      

+

       // check whether a constant is defined that is at most

       // ConstantDistance away from lit

       index = ~index;

@@ -168,33 +167,33 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
     }

 

     private VCExpr AddConstantFor(BigNum lit) {

-Contract.Requires((lit > ConstantDistance));

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

-      

+      Contract.Requires((lit > ConstantDistance));

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

+

       VCExprVar res = Gen.Variable("int#" + lit, Type.Int);

       int index = GetIndexFor(lit);

       Contract.Assert(index < 0);

       index = ~index;

 

       Literals.Insert(index, new KeyValuePair<BigNum, VCExprVar>(lit, res));

-      

+

       // relate the new constant to the predecessor and successor

       if (index > 0)

         DefineRelationship(Literals[index - 1].Value, Literals[index - 1].Key,

                            res, lit);

       else

         DefineRelationship(Gen.Integer(BigNum.ZERO), BigNum.ZERO, res, lit);

-        

+

       if (index < Literals.Count - 1)

         DefineRelationship(res, lit,

                            Literals[index + 1].Value, Literals[index + 1].Key);

 

       return res;

     }

-    

+

     private void DefineRelationship(VCExpr/*!*/ aExpr, BigNum aValue,

-                                    VCExpr/*!*/ bExpr, BigNum bValue)

-      {Contract.Requires(aValue < bValue);

+                                    VCExpr/*!*/ bExpr, BigNum bValue) {

+      Contract.Requires(aValue < bValue);

       Contract.Requires(aExpr != null);

       Contract.Requires(bExpr != null);

 

@@ -219,7 +218,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
 

     public override VCExpr Visit(VCExprLiteral node, bool arg) {

       Contract.Requires(node != null);

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

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

       VCExprIntLit intLit = node as VCExprIntLit;

       if (intLit != null) {

         if (NegConstantDistance > intLit.Val || intLit.Val > ConstantDistance)

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index a2b0c041..b90196e2 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -200,10 +200,10 @@ namespace Microsoft.Boogie.VCExprAST {
         VCExprVar res;

         foreach (Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/ d in Mapping) {

           //Contract.Assert(cce.NonNullElements(d));

-            if (d.TryGetValue(boogieVar, out res)) {

-               Contract.Assert(res != null);

-               return res;

-            }

+          if (d.TryGetValue(boogieVar, out res)) {

+            Contract.Assert(res != null);

+            return res;

+          }

         }

         return null;

       }

@@ -288,7 +288,7 @@ namespace Microsoft.Boogie.VCExprAST {
     ///////////////////////////////////////////////////////////////////////////////////

 

     public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Push(TranslateLiteralExpr(node));

       return node;

@@ -317,7 +317,7 @@ namespace Microsoft.Boogie.VCExprAST {
     ///////////////////////////////////////////////////////////////////////////////////

 

     public override AIVariableExpr VisitAIVariableExpr(AIVariableExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

@@ -326,7 +326,7 @@ namespace Microsoft.Boogie.VCExprAST {
     ///////////////////////////////////////////////////////////////////////////////////

 

     public override Expr VisitIdentifierExpr(IdentifierExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assume(node.Decl != null);   // the expression has to be resolved

       Push(LookupVariable(node.Decl));

@@ -340,7 +340,7 @@ namespace Microsoft.Boogie.VCExprAST {
     // causes it to become "x0". So we just remove old expressions with a visitor

     // before transforming it into a VCExpr.

     public override Expr VisitOldExpr(OldExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

@@ -349,7 +349,7 @@ namespace Microsoft.Boogie.VCExprAST {
     ///////////////////////////////////////////////////////////////////////////////////

 

     public override Expr VisitNAryExpr(NAryExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Push(TranslateNAryExpr(node));

       return node;

@@ -399,21 +399,21 @@ namespace Microsoft.Boogie.VCExprAST {
     ///////////////////////////////////////////////////////////////////////////////////

 

     public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Push(TranslateQuantifierExpr(node));

       return node;

     }

 

     public override ExistsExpr VisitExistsExpr(ExistsExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       node = (ExistsExpr)this.VisitQuantifierExpr(node);

       return node;

     }

 

     public override ForallExpr VisitForallExpr(ForallExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       node = (ForallExpr)this.VisitQuantifierExpr(node);

       return node;

@@ -509,32 +509,32 @@ namespace Microsoft.Boogie.VCExprAST {
     ///////////////////////////////////////////////////////////////////////////////////

 

     public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Push(TranslateBvExtractExpr(node));

       return node;

     }

 

-    private VCExpr TranslateBvExtractExpr(BvExtractExpr node){

-Contract.Requires(node != null);

-Contract.Requires((node.Start <= node.End));

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

-VCExpr/*!*/ bv = Translate(node.Bitvector);

-      return Gen.BvExtract(bv,cce.NonNull(node.Bitvector.Type).BvBits, node.Start, node.End);

+    private VCExpr TranslateBvExtractExpr(BvExtractExpr node) {

+      Contract.Requires(node != null);

+      Contract.Requires((node.Start <= node.End));

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

+      VCExpr/*!*/ bv = Translate(node.Bitvector);

+      return Gen.BvExtract(bv, cce.NonNull(node.Bitvector.Type).BvBits, node.Start, node.End);

     }

 

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

 

     public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Push(TranslateBvConcatExpr(node));

       return node;

     }

 

-    private VCExpr TranslateBvConcatExpr(BvConcatExpr node){

-Contract.Requires(node != null);

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

+    private VCExpr TranslateBvConcatExpr(BvConcatExpr node) {

+      Contract.Requires(node != null);

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

       VCExpr/*!*/ bv0 = Translate(node.E0);

       VCExpr/*!*/ bv1 = Translate(node.E1);

       return Gen.BvConcat(bv0, bv1);

@@ -544,60 +544,59 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
     // all the other cases should never happen

 

     public override Cmd VisitAssertCmd(AssertCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Cmd VisitAssignCmd(AssignCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Cmd VisitAssumeCmd(AssumeCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override AtomicRE VisitAtomicRE(AtomicRE node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Axiom VisitAxiom(Axiom node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Type VisitBasicType(BasicType node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Type VisitBvType(BvType node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Block VisitBlock(Block node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     CodeExprConverter codeExprConverter = null;

-    public void SetCodeExprConverter(CodeExprConverter f){

+    public void SetCodeExprConverter(CodeExprConverter f) {

       this.codeExprConverter = f;

     }

-    public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr)

-    {

-      Contract.Requires(codeExpr != null);

+    public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr) {

+      //Contract.Requires(codeExpr != null);

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

 

       Contract.Assume(codeExprConverter != null);

@@ -609,271 +608,271 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
       return codeExpr;

     }

     public override BlockSeq VisitBlockSeq(BlockSeq blockSeq) {

-      Contract.Requires(blockSeq != null);

+      //Contract.Requires(blockSeq != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override List<Block/*!*/>/*!*/ VisitBlockList(List<Block/*!*/>/*!*/ blocks) {

-      Contract.Requires(cce.NonNullElements(blocks));

+      //Contract.Requires(cce.NonNullElements(blocks));

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override BoundVariable VisitBoundVariable(BoundVariable node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Cmd VisitCallCmd(CallCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Cmd VisitCallForallCmd(CallForallCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {

-      Contract.Requires(cmdSeq != null);

+      //Contract.Requires(cmdSeq != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Choice VisitChoice(Choice node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Cmd VisitCommentCmd(CommentCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Constant VisitConstant(Constant node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override CtorType VisitCtorType(CtorType node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Declaration VisitDeclaration(Declaration node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override List<Declaration/*!*/>/*!*/ VisitDeclarationList(List<Declaration/*!*/>/*!*/ declarationList) {

-      Contract.Requires(cce.NonNullElements(declarationList));

+      //Contract.Requires(cce.NonNullElements(declarationList));

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Declaration>>()));

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Requires VisitRequires(Requires @requires) {

-      Contract.Requires(@requires != null);

+      //Contract.Requires(@requires != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) {

-      Contract.Requires(requiresSeq != null);

+      //Contract.Requires(requiresSeq != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Ensures VisitEnsures(Ensures @ensures) {

-      Contract.Requires(@ensures != null);

+      //Contract.Requires(@ensures != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) {

-      Contract.Requires(ensuresSeq != null);

+      //Contract.Requires(ensuresSeq != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Formal VisitFormal(Formal node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Function VisitFunction(Function node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override GlobalVariable VisitGlobalVariable(GlobalVariable node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override GotoCmd VisitGotoCmd(GotoCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Cmd VisitHavocCmd(HavocCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Implementation VisitImplementation(Implementation node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override LocalVariable VisitLocalVariable(LocalVariable node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override MapType VisitMapType(MapType node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Procedure VisitProcedure(Procedure node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Program VisitProgram(Program node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Cmd VisitRE(RE node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override RESeq VisitRESeq(RESeq reSeq) {

-      Contract.Requires(reSeq != null);

+      //Contract.Requires(reSeq != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override ReturnCmd VisitReturnCmd(ReturnCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Sequential VisitSequential(Sequential node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Cmd VisitStateCmd(StateCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override TransferCmd VisitTransferCmd(TransferCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Trigger VisitTrigger(Trigger node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Type VisitType(Type node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override TypedIdent VisitTypedIdent(TypedIdent node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Type VisitTypeVariable(TypeVariable node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Variable VisitVariable(Variable node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override VariableSeq VisitVariableSeq(VariableSeq variableSeq) {

-      Contract.Requires(variableSeq != null);

+      //Contract.Requires(variableSeq != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

     public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

@@ -924,13 +923,13 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
     }

 

 

-    public VCExpr Translate(IAppliable app, Type ty, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs){

-Contract.Requires(ty != null);

-Contract.Requires(app != null);

-Contract.Requires(cce.NonNullElements(typeArgs));

-Contract.Requires(cce.NonNullElements(args));

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

-    

+    public VCExpr Translate(IAppliable app, Type ty, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {

+      Contract.Requires(ty != null);

+      Contract.Requires(app != null);

+      Contract.Requires(cce.NonNullElements(typeArgs));

+      Contract.Requires(cce.NonNullElements(args));

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

+

       List<VCExpr/*!*/>/*!*/ oldArgs = this.args;

       List<Type/*!*/>/*!*/ oldTypeArgs = this.typeArgs;

       this.args = args;

@@ -946,45 +945,45 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
 

 

     public VCExpr Visit(UnaryOperator unaryOperator) {

-      Contract.Requires(unaryOperator != null);

+      //Contract.Requires(unaryOperator != null);

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

       Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Not && this.args.Count == 1);

       return Gen.Not(this.args);

     }

 

     public VCExpr Visit(BinaryOperator binaryOperator) {

-      Contract.Requires(binaryOperator != null);

+      //Contract.Requires(binaryOperator != null);

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

       return TranslateBinaryOperator(binaryOperator, this.args);

     }

 

     public VCExpr Visit(FunctionCall functionCall) {

-      Contract.Requires(functionCall != null);

+      //Contract.Requires(functionCall != null);

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

       return TranslateFunctionCall(functionCall, this.args, this.typeArgs);

     }

 

     public VCExpr Visit(MapSelect mapSelect) {

-      Contract.Requires(mapSelect != null);

+      //Contract.Requires(mapSelect != null);

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

       return Gen.Select(this.args, this.typeArgs);

     }

 

     public VCExpr Visit(MapStore mapStore) {

-      Contract.Requires(mapStore != null);

+      //Contract.Requires(mapStore != null);

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

       return Gen.Store(this.args, this.typeArgs);

     }

 

     public VCExpr Visit(TypeCoercion typeCoercion) {

-      Contract.Requires(typeCoercion != null);

+      //Contract.Requires(typeCoercion != null);

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

       Contract.Assert(this.args.Count == 1);

       return this.args[0];

     }

 

     public VCExpr Visit(IfThenElse ite) {

-      Contract.Requires(ite != null);

+      //Contract.Requires(ite != null);

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

       return Gen.Function(VCExpressionGenerator.IfThenElseOp, this.args);

     }

@@ -1038,12 +1037,12 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
 

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

 

-    private VCExpr/*!*/ TranslateFunctionCall(FunctionCall app, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs){

+    private VCExpr/*!*/ TranslateFunctionCall(FunctionCall app, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {

       Contract.Requires(cce.NonNullElements(args));

       Contract.Requires(cce.NonNullElements(typeArgs));

-Contract.Requires(app != null);

+      Contract.Requires(app != null);

       Contract.Requires((app.Func != null));

-Contract.Ensures(Contract.Result<VCExpr>() != null);    // resolution must have happened

+      Contract.Ensures(Contract.Result<VCExpr>() != null);    // resolution must have happened

 

       VCExpr res = ApplyExpansion(app, args, typeArgs);

       if (res != null)

@@ -1053,8 +1052,8 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);    // resolution must have
       return Gen.Function(functionOp, args, typeArgs);

     }

 

-    private VCExpr ApplyExpansion(FunctionCall app, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs){

-Contract.Requires(app != null);

+    private VCExpr ApplyExpansion(FunctionCall app, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {

+      Contract.Requires(app != null);

       Contract.Requires(cce.NonNullElements(args));

       Contract.Requires(cce.NonNullElements(typeArgs));

       Contract.Assert(app.Func != null);    // resolution must have happened

diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index 693fcf76..45eeda43 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -14,18 +14,17 @@ using Microsoft.Boogie.VCExprAST;
 

 // a naive method to turn VCExprs into strings that can be fed into Simplify

 

-namespace Microsoft.Boogie.VCExprAST

-{

+namespace Microsoft.Boogie.VCExprAST {

   [ContractClassFor(typeof(LineariserOptions))]

-  public abstract class LinOptContracts:LineariserOptions{

-    public LinOptContracts() : base(true) {

+  public abstract class LinOptContracts : LineariserOptions {

+    public LinOptContracts()

+      : base(true) {

     }

-    public override LineariserOptions  SetAsTerm(bool newVal)

-{

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

-  throw new NotImplementedException();

-}

-    

+    public override LineariserOptions SetAsTerm(bool newVal) {

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

+      throw new NotImplementedException();

+    }

+

   }

 

   // Options for the linearisation. Here one can choose, for instance,

@@ -36,52 +35,72 @@ namespace Microsoft.Boogie.VCExprAST
     public readonly bool AsTerm;

     public abstract LineariserOptions/*!*/ SetAsTerm(bool newVal);

 

-    public abstract bool QuantifierIds { get; }

+    public abstract bool QuantifierIds {

+      get;

+    }

 

-    public virtual bool UseWeights { get { return false; } }

+    public virtual bool UseWeights {

+      get {

+        return false;

+      }

+    }

 

-    public virtual bool InverseImplies { get { return false; } }

+    public virtual bool InverseImplies {

+      get {

+        return false;

+      }

+    }

 

     // whether to include type specifications in quantifiers

-    public abstract bool UseTypes { get; }

+    public abstract bool UseTypes {

+      get;

+    }

 

-    public virtual CommandLineOptions.BvHandling Bitvectors { get {

-      return CommandLineOptions.BvHandling.None;

-    } }

+    public virtual CommandLineOptions.BvHandling Bitvectors {

+      get {

+        return CommandLineOptions.BvHandling.None;

+      }

+    }

 

     // variables representing formulas in let-bindings have to be

     // printed in a different way than other variables

-    public virtual List<VCExprVar/*!*/>/*!*/ LetVariables { get {Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));

-      return EmptyList;

-    } }

+    public virtual List<VCExprVar/*!*/>/*!*/ LetVariables {

+      get {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));

+        return EmptyList;

+      }

+    }

 

-    public virtual LineariserOptions AddLetVariable(VCExprVar furtherVar){

-Contract.Requires(furtherVar != null);

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

+    public virtual LineariserOptions AddLetVariable(VCExprVar furtherVar) {

+      Contract.Requires(furtherVar != null);

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

       return this;

     }

 

-	public virtual LineariserOptions AddLetVariables(List<VCExprVar/*!*/>/*!*/ furtherVars){

-Contract.Requires(cce.NonNullElements(furtherVars));

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

+    public virtual LineariserOptions AddLetVariables(List<VCExprVar/*!*/>/*!*/ furtherVars) {

+      Contract.Requires(cce.NonNullElements(furtherVars));

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

       return this;

     }

-    

+

     private static readonly List<VCExprVar/*!*/>/*!*/ EmptyList = new List<VCExprVar/*!*/>();

     [ContractInvariantMethod]

-void ObjectInvarinat() 

-{

-    Contract.Invariant(EmptyList!=null);

-}

+    void ObjectInvarinat() {

+      Contract.Invariant(EmptyList != null);

+    }

 

 

-    public bool NativeBv { get {

-      return Bitvectors == CommandLineOptions.BvHandling.Z3Native;

-    } }

+    public bool NativeBv {

+      get {

+        return Bitvectors == CommandLineOptions.BvHandling.Z3Native;

+      }

+    }

 

-    public bool IntBv { get {

-      return Bitvectors == CommandLineOptions.BvHandling.ToInt;

-    } }

+    public bool IntBv {

+      get {

+        return Bitvectors == CommandLineOptions.BvHandling.ToInt;

+      }

+    }

 

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

 

@@ -89,23 +108,28 @@ void ObjectInvarinat()
       this.AsTerm = asTerm;

     }

 

-    public static readonly LineariserOptions SimplifyDefault = new SimplifyOptions (false);

-    internal static readonly LineariserOptions SimplifyDefaultTerm = new SimplifyOptions (true);

+    public static readonly LineariserOptions SimplifyDefault = new SimplifyOptions(false);

+    internal static readonly LineariserOptions SimplifyDefaultTerm = new SimplifyOptions(true);

 

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

 

     private class SimplifyOptions : LineariserOptions {

-      internal SimplifyOptions(bool asTerm):base(asTerm) {

-        

+      internal SimplifyOptions(bool asTerm)

+        : base(asTerm) {

+

+      }

+      public override bool QuantifierIds {

+        get {

+          return false;

+        }

+      }

+      public override bool UseTypes {

+        get {

+          return false;

+        }

       }

-      public override bool QuantifierIds { get {

-        return false;

-      } }

-      public override bool UseTypes { get {

-        return false;

-      } }

       public override LineariserOptions SetAsTerm(bool newVal) {

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

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

         if (newVal)

           return SimplifyDefaultTerm;

         else

@@ -119,21 +143,21 @@ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
   // Lineariser for expressions. The result (bool) is currently not used for anything

   public class SimplifyLikeExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> {

 

-    public static string ToSimplifyString(VCExpr e, UniqueNamer namer){

-Contract.Requires(namer != null);

-Contract.Requires(e != null);

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

+    public static string ToSimplifyString(VCExpr e, UniqueNamer namer) {

+      Contract.Requires(namer != null);

+      Contract.Requires(e != null);

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

       return ToString(e, LineariserOptions.SimplifyDefault, namer);

     }

 

-    public static string ToString(VCExpr/*!*/ e, LineariserOptions/*!*/ options,UniqueNamer/*!*/ namer) {

+    public static string ToString(VCExpr/*!*/ e, LineariserOptions/*!*/ options, UniqueNamer/*!*/ namer) {

       Contract.Requires(e != null);

       Contract.Requires(options != null);

       Contract.Requires(namer != null);

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

 

       StringWriter sw = new StringWriter();

-      SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser (sw, namer);

+      SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser(sw, namer);

       lin.Linearise(e, options);

       return sw.ToString();

     }

@@ -141,60 +165,62 @@ Contract.Ensures(Contract.Result<string>() != null);
     ////////////////////////////////////////////////////////////////////////////////////////

 

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(wr!=null);

+    void ObjectInvariant() {

+      Contract.Invariant(wr != null);

       Contract.Invariant(Namer != null);

-}

+    }

 

     private readonly TextWriter/*!*/ wr;

     private SimplifyLikeOpLineariser OpLinObject = null;

-    private IVCExprOpVisitor<bool, LineariserOptions/*!*/>/*!*/ OpLineariser { get {Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>()!=null);

-      if (OpLinObject == null)

-        OpLinObject = new SimplifyLikeOpLineariser (this, wr);

-      return OpLinObject;

-    } }

+    private IVCExprOpVisitor<bool, LineariserOptions/*!*/>/*!*/ OpLineariser {

+      get {

+        Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>() != null);

+        if (OpLinObject == null)

+          OpLinObject = new SimplifyLikeOpLineariser(this, wr);

+        return OpLinObject;

+      }

+    }

 

     internal readonly UniqueNamer Namer;

 

-    public SimplifyLikeExprLineariser(TextWriter wr, UniqueNamer namer){

-Contract.Requires(namer != null);

-Contract.Requires(wr != null);

+    public SimplifyLikeExprLineariser(TextWriter wr, UniqueNamer namer) {

+      Contract.Requires(namer != null);

+      Contract.Requires(wr != null);

       this.wr = wr;

       this.Namer = namer;

     }

 

-    public void Linearise(VCExpr expr, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(expr != null);

+    public void Linearise(VCExpr expr, LineariserOptions options) {

+      Contract.Requires(options != null);

+      Contract.Requires(expr != null);

       expr.Accept<bool, LineariserOptions>(this, options);

     }

 

-    public void LineariseAsTerm(VCExpr expr, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(expr != null);

+    public void LineariseAsTerm(VCExpr expr, LineariserOptions options) {

+      Contract.Requires(options != null);

+      Contract.Requires(expr != null);

       Linearise(expr, options.SetAsTerm(true));

     }

 

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

 

-    public static string MakeIdPrintable(string s){

-Contract.Requires(s != null);

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

+    public static string MakeIdPrintable(string s) {

+      Contract.Requires(s != null);

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

       // make sure that no keywords are used as identifiers

-      switch(s) {

-      case andName:

-      case orName:

-      case notName:

-      case impliesName:

-      case iffName:

-      case eqName:

-      case neqName:

-      case distinctName:

-      case TRUEName:

-      case FALSEName:

-        s = "nonkeyword_" + s;

-        break;

+      switch (s) {

+        case andName:

+        case orName:

+        case notName:

+        case impliesName:

+        case iffName:

+        case eqName:

+        case neqName:

+        case distinctName:

+        case TRUEName:

+        case FALSEName:

+          s = "nonkeyword_" + s;

+          break;

       }

 

       if (CommandLineOptions.Clo.BracketIdsInVC == 0) {

@@ -242,29 +268,26 @@ Contract.Ensures(Contract.Result<string>() != null);
       }

     }

 

-    private static void TypeToStringHelper(Type t, StringBuilder sb)

-    {

+    private static void TypeToStringHelper(Type t, StringBuilder sb) {

       Contract.Requires(t != null);

 

       TypeSynonymAnnotation syn = t as TypeSynonymAnnotation;

       if (syn != null) {

         TypeToStringHelper(syn.ExpandedType, sb);

-      }

-      else {

+      } else {

         if (t.IsMap) {

           MapType m = t.AsMap;

           sb.Append('[');

           for (int i = 0; i < m.MapArity; ++i) {

-            if (i != 0) sb.Append(',');

+            if (i != 0)

+              sb.Append(',');

             TypeToStringHelper(m.Arguments[i], sb);

           }

           sb.Append(']');

           TypeToStringHelper(m.Result, sb);

-        }

-        else if (t.IsBool || t.IsInt || t.IsBv) {

+        } else if (t.IsBool || t.IsInt || t.IsBv) {

           sb.Append(TypeToString(t));

-        }

-        else {

+        } else {

           System.IO.StringWriter buffer = new System.IO.StringWriter();

           using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

             t.Emit(stream);

@@ -276,8 +299,7 @@ Contract.Ensures(Contract.Result<string>() != null);
     }

 

 

-    public static string TypeToString(Type t)

-    {

+    public static string TypeToString(Type t) {

       Contract.Requires(t != null);

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

 

@@ -294,39 +316,39 @@ Contract.Ensures(Contract.Result<string>() != null);
       }

     }

 

-    public static string BvConcatOpName(VCExprNAry node){

-Contract.Requires(node != null);

-Contract.Requires((node.Op is VCExprBvConcatOp));

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

+    public static string BvConcatOpName(VCExprNAry node) {

+      Contract.Requires(node != null);

+      Contract.Requires((node.Op is VCExprBvConcatOp));

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

       int bits1 = node[0].Type.BvBits;

       int bits2 = node[1].Type.BvBits;

       return "$bv" + (bits1 + bits2) + "_concat[" + bits1 + "." + bits2 + "]";

     }

 

-    public static string BvExtractOpName(VCExprNAry node){

-Contract.Requires(node != null);

-Contract.Requires(node.Op is VCExprBvExtractOp);

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

+    public static string BvExtractOpName(VCExprNAry node) {

+      Contract.Requires(node != null);

+      Contract.Requires(node.Op is VCExprBvExtractOp);

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

       VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;

       return "$bv" + node.Type.BvBits + "_extract" + op.Total + "[" + op.Start + ":" + op.End + "]";

     }

 

-    public static string StoreOpName(VCExprNAry node){

-Contract.Requires(node != null);

-Contract.Requires((node.Op is VCExprStoreOp));

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

+    public static string StoreOpName(VCExprNAry node) {

+      Contract.Requires(node != null);

+      Contract.Requires((node.Op is VCExprStoreOp));

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

       return "Store_" + TypeToString(node[0].Type);

     }

 

-    public static string SelectOpName(VCExprNAry node){

-Contract.Requires(node != null);

-Contract.Requires((node.Op is VCExprSelectOp));

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

+    public static string SelectOpName(VCExprNAry node) {

+      Contract.Requires(node != null);

+      Contract.Requires((node.Op is VCExprSelectOp));

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

       return "Select_" + TypeToString(node[0].Type);

     }

-    

-    internal void WriteId(string s){

-Contract.Requires(s != null);

+

+    internal void WriteId(string s) {

+      Contract.Requires(s != null);

       wr.Write(MakeIdPrintable(s));

     }

 

@@ -343,7 +365,7 @@ Contract.Requires(s != null);
     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

@@ -373,25 +395,25 @@ Contract.Requires(s != null);
     internal const string intDivName = "/";

     internal const string intModName = "%";

 

-    internal void AssertAsTerm(string x, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(x != null);

+    internal void AssertAsTerm(string x, LineariserOptions options) {

+      Contract.Requires(options != null);

+      Contract.Requires(x != null);

       if (!options.AsTerm)

         System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!");

     }

 

-    internal void AssertAsFormula(string x, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(x != null);

+    internal void AssertAsFormula(string x, LineariserOptions options) {

+      Contract.Requires(options != null);

+      Contract.Requires(x != null);

       if (options.AsTerm)

         System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!");

     }

 

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

 

-    public bool Visit(VCExprLiteral node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+    public bool Visit(VCExprLiteral node, LineariserOptions options) {

+      //Contract.Requires(options != null);

+      //Contract.Requires(node != null);

       if (options.AsTerm) {

 

         if (node == VCExpressionGenerator.True)

@@ -425,9 +447,9 @@ Contract.Requires(node != null);
 

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

 

-    public bool Visit(VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+      //Contract.Requires(options != null);

+      //Contract.Requires(node != null);

       VCExprOp op = node.Op;

       Contract.Assert(op != null);

 

@@ -438,11 +460,11 @@ Contract.Requires(node != null);
 

         wr.Write("({0}",

                  op.Equals(VCExpressionGenerator.AndOp) ? andName : orName);

-        IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node);

+        IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);

         Contract.Assert(enumerator != null);

         while (enumerator.MoveNext()) {

           VCExprNAry naryExpr = enumerator.Current as VCExprNAry;

-          if (naryExpr == null ||  !naryExpr.Op.Equals(op)) {

+          if (naryExpr == null || !naryExpr.Op.Equals(op)) {

             wr.Write(" ");

             Linearise(cce.NonNull((VCExpr)enumerator.Current), options);

           }

@@ -458,24 +480,24 @@ Contract.Requires(node != null);
 

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

 

-    public bool Visit(VCExprVar node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+    public bool Visit(VCExprVar node, LineariserOptions options) {

+      //Contract.Requires(options != null);

+      //Contract.Requires(node != null);

       string printedName = Namer.GetName(node, node.Name);

       Contract.Assert(printedName != null);

 

       if (options.AsTerm ||

-          // variables for formulas bound in a let-binding are never

-          // written as an equation

+        // variables for formulas bound in a let-binding are never

+        // written as an equation

           options.LetVariables.Contains(node) ||

-          // if variables are properly typed, they cannot be written as

-          // equation either

+        // if variables are properly typed, they cannot be written as

+        // equation either

           options.UseTypes) {

         WriteId(printedName);

       } else {

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

         WriteId(printedName);

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

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

       }

 

       return true;

@@ -483,71 +505,71 @@ Contract.Requires(node != null);
 

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

 

-    public bool Visit(VCExprQuantifier node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+    public bool Visit(VCExprQuantifier node, LineariserOptions options) {

+      //Contract.Requires(options != null);

+      //Contract.Requires(node != null);

       AssertAsFormula(node.Quan.ToString(), options);

       Contract.Assert(node.TypeParameters.Count == 0);

 

-      Namer.PushScope(); try {

+      Namer.PushScope();

+      try {

 

-      string kind = node.Quan == Quantifier.ALL ? "FORALL" : "EXISTS";

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

+        string kind = node.Quan == Quantifier.ALL ? "FORALL" : "EXISTS";

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

 

-      for (int i = 0; i < node.BoundVars.Count; i++) 

-        {

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

           VCExprVar var = node.BoundVars[i];

-        Contract.Assert(var != null);

+          Contract.Assert(var != null);

           string printedName = Namer.GetLocalName(var, var.Name);

-        Contract.Assert(printedName != null);

+          Contract.Assert(printedName != null);

           if (i != 0)

             wr.Write(" ");

           WriteId(printedName);

           if (options.UseTypes)

             wr.Write(" :TYPE {0}", TypeToString(var.Type));

         }

-      wr.Write(") ");

-        

-      WriteTriggers(node.Triggers, options);

-        

-      if (options.QuantifierIds) {

-        // only needed for Z3

-        VCQuantifierInfos infos = node.Infos;

-        Contract.Assert(infos != null);

-        if (infos.qid != null) {

-          wr.Write("(QID ");

-          wr.Write(infos.qid);

-          wr.Write(") ");

-        }

-        if (0 <= infos.uniqueId) {

-          wr.Write("(SKOLEMID ");

-          wr.Write(infos.uniqueId);

-          wr.Write(") ");

+        wr.Write(") ");

+

+        WriteTriggers(node.Triggers, options);

+

+        if (options.QuantifierIds) {

+          // only needed for Z3

+          VCQuantifierInfos infos = node.Infos;

+          Contract.Assert(infos != null);

+          if (infos.qid != null) {

+            wr.Write("(QID ");

+            wr.Write(infos.qid);

+            wr.Write(") ");

+          }

+          if (0 <= infos.uniqueId) {

+            wr.Write("(SKOLEMID ");

+            wr.Write(infos.uniqueId);

+            wr.Write(") ");

+          }

         }

-     }

 

-     if (options.UseWeights) {

-        int weight = QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);

-        if (weight != 1) {

-          wr.Write("(WEIGHT ");

-          wr.Write(weight);

-          wr.Write(") ");

+        if (options.UseWeights) {

+          int weight = QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);

+          if (weight != 1) {

+            wr.Write("(WEIGHT ");

+            wr.Write(weight);

+            wr.Write(") ");

+          }

         }

-      }

 

-      Linearise(node.Body, options);

-      wr.Write(")");

+        Linearise(node.Body, options);

+        wr.Write(")");

 

-      return true;

+        return true;

 

       } finally {

         Namer.PopScope();

       }

     }

 

-    private void WriteTriggers(List<VCTrigger/*!*/>/*!*/ triggers, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(cce.NonNullElements(triggers));

+    private void WriteTriggers(List<VCTrigger/*!*/>/*!*/ triggers, LineariserOptions options) {

+      Contract.Requires(options != null);

+      Contract.Requires(cce.NonNullElements(triggers));

       // first, count how many neg/pos triggers there are

       int negTriggers = 0;

       int posTriggers = 0;

@@ -568,7 +590,8 @@ Contract.Requires(cce.NonNullElements(triggers));
             if (vcTrig.Exprs.Count > 1) {

               wr.Write(" (MPAT");

             }

-            foreach (VCExpr e in vcTrig.Exprs) {Contract.Assert(e != null);

+            foreach (VCExpr e in vcTrig.Exprs) {

+              Contract.Assert(e != null);

               wr.Write(" ");

               LineariseAsTerm(e, options);

             }

@@ -598,37 +621,39 @@ Contract.Requires(cce.NonNullElements(triggers));
 

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

 

-    public bool Visit(VCExprLet node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

-      Namer.PushScope(); try {

+    public bool Visit(VCExprLet node, LineariserOptions options) {

+      //Contract.Requires(options != null);

+      //Contract.Requires(node != null);

+      Namer.PushScope();

+      try {

 

-      wr.Write("(LET (");

+        wr.Write("(LET (");

 

-      LineariserOptions optionsWithVars = options.AddLetVariables(node.BoundVars);

+        LineariserOptions optionsWithVars = options.AddLetVariables(node.BoundVars);

         Contract.Assert(optionsWithVars != null);

-	  

-      string s = "(";

-      foreach (VCExprLetBinding b in node) {Contract.Assert(b != null);

-        wr.Write(s);

-        string printedName = Namer.GetLocalName(b.V, b.V.Name);

-

-        bool formula = b.V.Type.IsBool;

-        if (formula)

-          wr.Write("FORMULA ");

-        else

-          wr.Write("TERM ");

-        WriteId(printedName);

-        wr.Write(" ");

-        Linearise(b.E, optionsWithVars.SetAsTerm(!formula));

+

+        string s = "(";

+        foreach (VCExprLetBinding b in node) {

+          Contract.Assert(b != null);

+          wr.Write(s);

+          string printedName = Namer.GetLocalName(b.V, b.V.Name);

+

+          bool formula = b.V.Type.IsBool;

+          if (formula)

+            wr.Write("FORMULA ");

+          else

+            wr.Write("TERM ");

+          WriteId(printedName);

+          wr.Write(" ");

+          Linearise(b.E, optionsWithVars.SetAsTerm(!formula));

+          wr.Write(")");

+          s = " (";

+        }

+        wr.Write(") ");

+        Linearise(node.Body, optionsWithVars);

         wr.Write(")");

-        s = " (";

-      }

-      wr.Write(") ");

-      Linearise(node.Body, optionsWithVars);

-      wr.Write(")");

 

-      return true;

+        return true;

 

       } finally {

         Namer.PopScope();

@@ -648,50 +673,50 @@ Contract.Requires(node != null);
       private readonly SimplifyLikeExprLineariser/*!*/ ExprLineariser;

       private readonly TextWriter/*!*/ wr;

 

-      public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser ExprLineariser, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(ExprLineariser != null);

+      public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser ExprLineariser, TextWriter wr) {

+        Contract.Requires(wr != null);

+        Contract.Requires(ExprLineariser != null);

         this.ExprLineariser = ExprLineariser;

         this.wr = wr;

       }

 

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

 

-      private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms){

-Contract.Requires(options != null);

-Contract.Requires(op != null);

-Contract.Requires(cce.NonNullElements(args));

+      private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms) {

+        Contract.Requires(options != null);

+        Contract.Requires(op != null);

+        Contract.Requires(cce.NonNullElements(args));

         WriteApplication(op, op, args, options, argsAsTerms);

       }

 

-      private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args,LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(op != null);

-Contract.Requires(cce.NonNullElements(args));

+      private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {

+        Contract.Requires(options != null);

+        Contract.Requires(op != null);

+        Contract.Requires(cce.NonNullElements(args));

         WriteApplication(op, op, args, options, options.AsTerm);

       }

 

-      private void WriteTermApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args,LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(op != null);

-Contract.Requires(cce.NonNullElements(args));

+      private void WriteTermApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {

+        Contract.Requires(options != null);

+        Contract.Requires(op != null);

+        Contract.Requires(cce.NonNullElements(args));

         ExprLineariser.AssertAsTerm(op, options);

         WriteApplication(op, op, args, options, options.AsTerm);

       }

 

-      private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(predOp != null);

-Contract.Requires(termOp != null);

-Contract.Requires(cce.NonNullElements(args));

+      private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {

+        Contract.Requires(options != null);

+        Contract.Requires(predOp != null);

+        Contract.Requires(termOp != null);

+        Contract.Requires(cce.NonNullElements(args));

         WriteApplication(termOp, predOp, args, options, options.AsTerm);

       }

 

-      private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms){

-Contract.Requires(options != null);

-Contract.Requires(predOp != null);

-Contract.Requires(termOp != null);

-Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the arguments?

+      private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms) {

+        Contract.Requires(options != null);

+        Contract.Requires(predOp != null);

+        Contract.Requires(termOp != null);

+        Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the arguments?

         wr.Write("({0}", options.AsTerm ? termOp : predOp);

 

         LineariserOptions newOptions = options.SetAsTerm(argsAsTerms);

@@ -701,17 +726,17 @@ Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the
           wr.Write(" ");

           ExprLineariser.Linearise(e, newOptions);

         }

-        

+

         wr.Write(")");

       }

 

       // write an application that can only be a term.

       // if the expression is supposed to be printed as a formula,

       // it is turned into an equation (EQ (f args) |@true|)

-      private void WriteApplicationTermOnly(string termOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(termOp != null);

-Contract.Requires(cce.NonNullElements(args));

+      private void WriteApplicationTermOnly(string termOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {

+        Contract.Requires(options != null);

+        Contract.Requires(termOp != null);

+        Contract.Requires(cce.NonNullElements(args));

         if (!options.AsTerm)

           // Write: (EQ (f args) |@true|)

           // where "args" are written as terms

@@ -724,17 +749,17 @@ Contract.Requires(cce.NonNullElements(args));
       }

 

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

-      

-      public bool VisitNotOp     (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(boolNotName, notName, node, options);      // arguments can be both terms and formulas

         return true;

       }

 

-      public bool VisitEqOp      (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         if (options.AsTerm) {

           // use equality on terms, also if the arguments have type bool

           WriteApplication(termEqName, node, options);

@@ -753,9 +778,9 @@ Contract.Requires(node != null);
         return true;

       }

 

-      public bool VisitNeqOp     (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         if (options.AsTerm) {

           // use equality on terms, also if the arguments have type bool

           WriteApplication(termNeqName, node, options);

@@ -771,29 +796,29 @@ Contract.Requires(node != null);
             WriteApplication(neqName, node, options, true);

           }

         }

-        

+

         return true;

       }

 

-      public bool VisitAndOp     (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         Contract.Assert(options.AsTerm);

         WriteApplication(boolAndName, andName, node, options);        // arguments can be both terms and formulas

         return true;

       }

 

-      public bool VisitOrOp      (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         Contract.Assert(options.AsTerm);

         WriteApplication(boolOrName, orName, node, options);        // arguments can be both terms and formulas

         return true;

       }

 

-      public bool VisitImpliesOp (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         if (options.AsTerm) {

           wr.Write("({0} ({1} ", boolOrName, boolNotName);

           ExprLineariser.Linearise(node[0], options);

@@ -807,16 +832,16 @@ Contract.Requires(node != null);
           ExprLineariser.Linearise(node[0], options);

           wr.Write("))");

         } else {

-          WriteApplication(impliesName, node, options);          

+          WriteApplication(impliesName, node, options);

         }

         return true;

       }

 

-      public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         ExprLineariser.AssertAsFormula(distinctName, options);

-        

+

         if (node.Length < 2) {

           ExprLineariser.Linearise(VCExpressionGenerator.True, options);

         } else {

@@ -832,19 +857,20 @@ Contract.Requires(node != null);
         return true;

       }

 

-      public bool VisitLabelOp   (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         VCExprLabelOp op = (VCExprLabelOp)node.Op;

         Contract.Assert(op != null);

         wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label));

-        ExprLineariser.Linearise(node[0], options); wr.Write(")");

+        ExprLineariser.Linearise(node[0], options);

+        wr.Write(")");

         return true;

       }

 

-      public bool VisitSelectOp  (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         wr.Write("(" + SelectOpName(node));

         foreach (VCExpr/*!*/ e in node) {

           Contract.Assert(e != null);

@@ -855,9 +881,9 @@ Contract.Requires(node != null);
         return true;

       }

 

-      public bool VisitStoreOp   (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         wr.Write("(" + StoreOpName(node));

         foreach (VCExpr e in node) {

           Contract.Assert(e != null);

@@ -868,31 +894,31 @@ Contract.Requires(node != null);
         return true;

       }

 

-      public bool VisitBvOp      (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication("$make_bv" + node.Type.BvBits, node, options);

         return true;

       }

 

-      public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(BvExtractOpName(node), node, options);

         return true;

       }

 

-      public bool VisitBvConcatOp (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(BvConcatOpName(node), node, options);

         return true;

       }

 

-      public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

-        

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+

         wr.Write("(ITE ");

         ExprLineariser.Linearise(node[0], options.SetAsTerm(false));

         wr.Write(" ");

@@ -905,8 +931,8 @@ Contract.Requires(node != null);
       }

 

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

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

         VCExprCustomOp op = (VCExprCustomOp)node.Op;

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

         foreach (VCExpr arg in node) {

@@ -917,9 +943,9 @@ Contract.Requires(node != null);
         return true;

       }

 

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

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         if (CommandLineOptions.Clo.ReflectAdd) {

           WriteTermApplication(intAddNameReflect, node, options);

         } else {

@@ -928,79 +954,79 @@ Contract.Requires(node != null);
         return true;

       }

 

-      public bool VisitSubOp           (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(intSubName, node, options);

         return true;

       }

 

-      public bool VisitMulOp           (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(intMulName, node, options);

         return true;

       }

 

-      public bool VisitDivOp           (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(intDivName, node, options);

         return true;

       }

 

-      public bool VisitModOp           (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(intModName, node, options);

         return true;

       }

 

-      public bool VisitLtOp            (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(termLessName, lessName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitLeOp            (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(termAtmostName, atmostName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitGtOp            (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(termGreaterName, greaterName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitGeOp            (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(termAtleastName, atleastName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitSubtypeOp       (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(subtypeName, node, options, true);               // arguments are always terms

         return true;

       }

 

-      public bool VisitSubtype3Op       (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(subtypeArgsName, node, options, true);               // arguments are always terms

         return true;

       }

 

-      public bool VisitBoogieFunctionOp (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

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

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;

         Contract.Assert(op != null);

         string funcName = op.Func.Name;

@@ -1008,7 +1034,8 @@ Contract.Requires(node != null);
         string bvzName = op.Func.FindStringAttribute("external");

         string printedName = ExprLineariser.Namer.GetName(op.Func, funcName);

         Contract.Assert(printedName != null);

-        if (bvzName != null) printedName = bvzName;

+        if (bvzName != null)

+          printedName = bvzName;

 

         if (options.UseTypes) {

           // we use term notation for arguments whose type is not bool, and

@@ -1022,7 +1049,7 @@ Contract.Requires(node != null);
             wr.Write(" ");

             ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));

           }

-        

+

           wr.Write(")");

         } else {

           // arguments are always terms

@@ -1031,7 +1058,7 @@ Contract.Requires(node != null);
         }

         return true;

       }

-      

+

     }

   }

 

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 7fc8073a..89c615ad 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -571,17 +571,22 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<VCExpr>() != null);

       return Quantify(Quantifier.ALL, typeParams, vars, triggers, infos, body);

     }

-    public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, string qid, VCExpr body){

-Contract.Requires(body != null);Contract.Requires(qid != null);Contract.Requires(cce.NonNullElements(triggers));Contract.Requires(cce.NonNullElements(vars));

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

-return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,

-                      triggers, new VCQuantifierInfos (qid, -1, false, null), body);

-    }

-    public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body){

-Contract.Requires(body != null);Contract.Requires(cce.NonNullElements(triggers));Contract.Requires(cce.NonNullElements(vars));

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

-return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,

-                      triggers, new VCQuantifierInfos (null, -1, false, null), body);

+    public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, string qid, VCExpr body) {

+      Contract.Requires(body != null);

+      Contract.Requires(qid != null);

+      Contract.Requires(cce.NonNullElements(triggers));

+      Contract.Requires(cce.NonNullElements(vars));

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

+      return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,

+                            triggers, new VCQuantifierInfos(qid, -1, false, null), body);

+    }

+    public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body) {

+      Contract.Requires(body != null);

+      Contract.Requires(cce.NonNullElements(triggers));

+      Contract.Requires(cce.NonNullElements(vars));

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

+      return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,

+                            triggers, new VCQuantifierInfos(null, -1, false, null), body);

     }

     public VCExpr Forall(VCExprVar var, VCTrigger trigger, VCExpr body) {

       Contract.Requires(body != null);

@@ -599,13 +604,13 @@ return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
       Contract.Ensures(Contract.Result<VCExpr>() != null);

       return Quantify(Quantifier.EX, typeParams, vars, triggers, infos, body);

     }

-    public VCExpr Exists(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body){

-Contract.Requires(body != null);

+    public VCExpr Exists(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body) {

+      Contract.Requires(body != null);

       Contract.Requires(cce.NonNullElements(triggers));

       Contract.Requires(cce.NonNullElements(vars));

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

-      return Quantify(Quantifier.EX, new List<TypeVariable/*!*/> (), vars,

-                      triggers, new VCQuantifierInfos (null, -1, false, null), body);

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

+      return Quantify(Quantifier.EX, new List<TypeVariable/*!*/>(), vars,

+                      triggers, new VCQuantifierInfos(null, -1, false, null), body);

     }

     public VCExpr Exists(VCExprVar var, VCTrigger trigger, VCExpr body) {

       Contract.Requires(body != null);

@@ -679,11 +684,11 @@ namespace Microsoft.Boogie.VCExprAST {
       return res;

     }

 

-    public static TypeSeq ToTypeSeq(VCExpr[] exprs, int startIndex){

-Contract.Requires(exprs != null);

-Contract.Requires((Contract.ForAll(0,exprs.Length, i=> exprs[i] != null)));

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

-TypeSeq/*!*/ res = new TypeSeq();

+    public static TypeSeq ToTypeSeq(VCExpr[] exprs, int startIndex) {

+      Contract.Requires(exprs != null);

+      Contract.Requires((Contract.ForAll(0, exprs.Length, i => exprs[i] != null)));

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

+      TypeSeq/*!*/ res = new TypeSeq();

       for (int i = startIndex; i < exprs.Length; ++i)

         res.Add(cce.NonNull(exprs[i]).Type);

       return res;

@@ -760,14 +765,15 @@ TypeSeq/*!*/ res = new TypeSeq();
       this.LitType = type;

     }

     public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

       return visitor.Visit(this, arg);

     }

   }

 

   public class VCExprIntLit : VCExprLiteral {

     public readonly BigNum Val;

-    internal VCExprIntLit(BigNum val) :base(Type.Int){

+    internal VCExprIntLit(BigNum val)

+      : base(Type.Int) {

       this.Val = val;

     }

     [Pure]

@@ -899,7 +905,7 @@ TypeSeq/*!*/ res = new TypeSeq();
       this.Op = op;

     }

     public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

       return visitor.Visit(this, arg);

     }

     public Result Accept<Result, Arg>(IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {

@@ -944,7 +950,8 @@ TypeSeq/*!*/ res = new TypeSeq();
       }

     }

 

-    internal VCExprNullary(VCExprOp op):base(op) {

+    internal VCExprNullary(VCExprOp op)

+      : base(op) {

       Contract.Requires(op != null);

       Contract.Requires(op.Arity == 0 && op.TypeParamArity == 0);

       this.ExprType = op.InferType(EMPTY_VCEXPR_LIST, EMPTY_TYPE_LIST);

@@ -984,21 +991,23 @@ TypeSeq/*!*/ res = new TypeSeq();
       }

     }

 

-    internal VCExprUnary(VCExprOp op, List<VCExpr> arguments) :base(op){

+    internal VCExprUnary(VCExprOp op, List<VCExpr> arguments)

+      : base(op) {

       Contract.Requires(op != null);

       Contract.Requires(cce.NonNullElements(arguments));

       Contract.Requires(op.Arity == 1 && op.TypeParamArity == 0 && arguments.Count == 1);

-      

+

       this.Argument = arguments[0];

       this.ExprType =

         op.InferType(arguments, EMPTY_TYPE_LIST);

     }

 

-    internal VCExprUnary(VCExprOp op, VCExpr argument) :base(op){

+    internal VCExprUnary(VCExprOp op, VCExpr argument)

+      : base(op) {

       Contract.Requires(argument != null);

       Contract.Requires(op != null);

       Contract.Requires(op.Arity == 1 && op.TypeParamArity == 0);

-      

+

       this.Argument = argument;

       // PR: could be optimised so that the argument does

       // not have to be boxed in an array each time

@@ -1049,17 +1058,19 @@ TypeSeq/*!*/ res = new TypeSeq();
       }

     }

 

-    internal VCExprBinary(VCExprOp op, List<VCExpr> arguments) :base(op){

+    internal VCExprBinary(VCExprOp op, List<VCExpr> arguments)

+      : base(op) {

       Contract.Requires(op != null);

       Contract.Requires(cce.NonNullElements(arguments));

       Contract.Requires(op.Arity == 2 && op.TypeParamArity == 0 && arguments.Count == 2);

-      

+

       this.Argument0 = arguments[0];

       this.Argument1 = arguments[1];

       this.ExprType = op.InferType(arguments, EMPTY_TYPE_LIST);

     }

 

-    internal VCExprBinary(VCExprOp op, VCExpr argument0, VCExpr argument1) :base(op){

+    internal VCExprBinary(VCExprOp op, VCExpr argument0, VCExpr argument1)

+      : base(op) {

       Contract.Requires(argument1 != null);

       Contract.Requires(argument0 != null);

       Contract.Requires(op != null);

@@ -1109,7 +1120,8 @@ TypeSeq/*!*/ res = new TypeSeq();
       }

     }

 

-    internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments) :base(op){

+    internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments)

+      : base(op) {

       Contract.Requires(op != null);

       Contract.Requires(cce.NonNullElements(arguments));

       //this(op, arguments, EMPTY_TYPE_LIST);

@@ -1117,7 +1129,8 @@ TypeSeq/*!*/ res = new TypeSeq();
       this.TypeArgumentsAttr = EMPTY_TYPE_LIST;

       this.ExprType = op.InferType(arguments, TypeArgumentsAttr);

     }

-    internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments, List<Type/*!*/>/*!*/ typeArguments):base(op){

+    internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments, List<Type/*!*/>/*!*/ typeArguments)

+      : base(op) {

       Contract.Requires(op != null);

       Contract.Requires(cce.NonNullElements(typeArguments));

       Contract.Requires(cce.NonNullElements(arguments));

@@ -1227,8 +1240,8 @@ TypeSeq/*!*/ res = new TypeSeq();
       }

     }

     public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

-      Contract.Requires(cce.NonNullElements(typeArgs));

-      Contract.Requires(cce.NonNullElements(args));

+      //Contract.Requires(cce.NonNullElements(typeArgs));

+      //Contract.Requires(cce.NonNullElements(args));

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

       return OpType;

     }

@@ -1241,7 +1254,8 @@ TypeSeq/*!*/ res = new TypeSeq();
   }

 

   public class VCExprDistinctOp : VCExprNAryOp {

-    internal VCExprDistinctOp(int arity) :base(arity, Type.Bool){

+    internal VCExprDistinctOp(int arity)

+      : base(arity, Type.Bool) {

     }

     [Pure]

     [Reads(ReadsAttribute.Reads.Nothing)]

@@ -1258,8 +1272,8 @@ TypeSeq/*!*/ res = new TypeSeq();
     }

     public override Result Accept<Result, Arg>

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

-      Contract.Requires(visitor != null);

-      Contract.Requires(expr != null);

+      //Contract.Requires(visitor != null);

+      //Contract.Requires(expr != null);

       return visitor.VisitDistinctOp(expr, arg);

     }

   }

@@ -1276,8 +1290,8 @@ TypeSeq/*!*/ res = new TypeSeq();
       }

     }

     public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

-      Contract.Requires(cce.NonNullElements(typeArgs));

-      Contract.Requires(cce.NonNullElements(args));

+      //Contract.Requires(cce.NonNullElements(typeArgs));

+      //Contract.Requires(cce.NonNullElements(args));

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

       return args[0].Type;

     }

@@ -1312,8 +1326,8 @@ TypeSeq/*!*/ res = new TypeSeq();
     }

     public override Result Accept<Result, Arg>

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

-      Contract.Requires(visitor != null);

-      Contract.Requires(expr != null);

+      //Contract.Requires(visitor != null);

+      //Contract.Requires(expr != null);

       return visitor.VisitLabelOp(expr, arg);

     }

   }

@@ -1332,10 +1346,10 @@ TypeSeq/*!*/ res = new TypeSeq();
       }

     }

 

-    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs){

-Contract.Requires(cce.NonNullElements(typeArgs));

-Contract.Requires(cce.NonNullElements(args));

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

+    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

+      //Contract.Requires(cce.NonNullElements(typeArgs));

+      //Contract.Requires(cce.NonNullElements(args));

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

       MapType/*!*/ mapType = args[0].Type.AsMap;

       Contract.Assert(TypeParamArity == mapType.TypeParameters.Length);

       IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();

@@ -1366,8 +1380,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
     }

     public override Result Accept<Result, Arg>

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

-      Contract.Requires(visitor != null);

-      Contract.Requires(expr != null);

+      //Contract.Requires(visitor != null);

+      //Contract.Requires(expr != null);

       return visitor.VisitSelectOp(expr, arg);

     }

   }

@@ -1389,8 +1403,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
     }

 

     public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

-      Contract.Requires(cce.NonNullElements(typeArgs));

-      Contract.Requires(cce.NonNullElements(args));

+      //Contract.Requires(cce.NonNullElements(typeArgs));

+      //Contract.Requires(cce.NonNullElements(args));

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

       return args[0].Type;

     }

@@ -1416,8 +1430,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
     }

     public override Result Accept<Result, Arg>

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

-      Contract.Requires(visitor != null);

-      Contract.Requires(expr != null);

+      //Contract.Requires(visitor != null);

+      //Contract.Requires(expr != null);

       return visitor.VisitStoreOp(expr, arg);

     }

   }

@@ -1434,8 +1448,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
       }

     }

     public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

-      Contract.Requires(cce.NonNullElements(typeArgs));

-      Contract.Requires(cce.NonNullElements(args));

+      //Contract.Requires(cce.NonNullElements(typeArgs));

+      //Contract.Requires(cce.NonNullElements(args));

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

       return args[1].Type;

     }

@@ -1458,8 +1472,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
     }

     public override Result Accept<Result, Arg>

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

-      Contract.Requires(visitor != null);

-      Contract.Requires(expr != null);

+      //Contract.Requires(visitor != null);

+      //Contract.Requires(expr != null);

       return visitor.VisitIfThenElseOp(expr, arg);

     }

   }

@@ -1469,11 +1483,10 @@ Contract.Ensures(Contract.Result<Type>() != null);
     int arity;

     public readonly Type/*!*/ Type;

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(Name!=null);

+    void ObjectInvariant() {

+      Contract.Invariant(Name != null);

       Contract.Invariant(Type != null);

-}

+    }

 

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

       Contract.Requires(name != null);

@@ -1482,7 +1495,8 @@ void ObjectInvariant()
       this.arity = arity;

       this.Type = type;

     }

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

+    [Pure]

+    [Reads(ReadsAttribute.Reads.Nothing)]

     public override bool Equals(object that) {

       if (Object.ReferenceEquals(this, that))

         return true;

@@ -1491,15 +1505,26 @@ void ObjectInvariant()
         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) {Contract.Requires((cce.NonNullElements(args)));

-Contract.Requires((cce.NonNullElements(typeArgs)));

-Contract.Ensures(Contract.Result<Type>() != null); return 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) {

+      //Contract.Requires((cce.NonNullElements(args)));

+      //Contract.Requires((cce.NonNullElements(typeArgs)));

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

+      return Type;

+    }

     public override Result Accept<Result, Arg>

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

-      Contract.Requires(expr != null);

-      Contract.Requires(visitor != null);

+      //Contract.Requires(expr != null);

+      //Contract.Requires(visitor != null);

       return visitor.VisitCustomOp(expr, arg);

     }

   }

@@ -1521,8 +1546,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
       }

     }

     public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

-      Contract.Requires(cce.NonNullElements(typeArgs));

-      Contract.Requires(cce.NonNullElements(args));

+      //Contract.Requires(cce.NonNullElements(typeArgs));

+      //Contract.Requires(cce.NonNullElements(args));

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

       return Type.GetBvType(Bits);

     }

@@ -1546,8 +1571,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
     }

     public override Result Accept<Result, Arg>

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

-      Contract.Requires(visitor != null);

-      Contract.Requires(expr != null);

+      //Contract.Requires(visitor != null);

+      //Contract.Requires(expr != null);

       return visitor.VisitBvOp(expr, arg);

     }

   }

@@ -1568,8 +1593,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
       }

     }

     public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

-      Contract.Requires(cce.NonNullElements(typeArgs));

-      Contract.Requires(cce.NonNullElements(args));

+      //Contract.Requires(cce.NonNullElements(typeArgs));

+      //Contract.Requires(cce.NonNullElements(args));

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

       return Type.GetBvType(End - Start);

     }

@@ -1598,8 +1623,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
     }

     public override Result Accept<Result, Arg>

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

-      Contract.Requires(visitor != null);

-      Contract.Requires(expr != null);

+      //Contract.Requires(visitor != null);

+      //Contract.Requires(expr != null);

       return visitor.VisitBvExtractOp(expr, arg);

     }

   }

@@ -1619,8 +1644,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
       }

     }

     public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

-      Contract.Requires(cce.NonNullElements(typeArgs));

-      Contract.Requires(cce.NonNullElements(args));

+      //Contract.Requires(cce.NonNullElements(typeArgs));

+      //Contract.Requires(cce.NonNullElements(args));

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

       return Type.GetBvType(args[0].Type.BvBits + args[1].Type.BvBits);

     }

@@ -1648,8 +1673,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
     }

     public override Result Accept<Result, Arg>

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

-      Contract.Requires(visitor != null);

-      Contract.Requires(expr != null);

+      //Contract.Requires(visitor != null);

+      //Contract.Requires(expr != null);

       return visitor.VisitBvConcatOp(expr, arg);

     }

   }

@@ -1675,10 +1700,10 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
         return Func.TypeParameters.Length;

       }

     }

-    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs){

-Contract.Requires(cce.NonNullElements(typeArgs));

-Contract.Requires(cce.NonNullElements(args));

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

+    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

+      //Contract.Requires(cce.NonNullElements(typeArgs));

+      //Contract.Requires(cce.NonNullElements(args));

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

       Contract.Assert(TypeParamArity == Func.TypeParameters.Length);

       if (TypeParamArity == 0)

         return cce.NonNull(Func.OutParams[0]).TypedIdent.Type;

@@ -1710,8 +1735,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
     }

     public override Result Accept<Result, Arg>

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

-      Contract.Requires(visitor != null);

-      Contract.Requires(expr != null);

+      //Contract.Requires(visitor != null);

+      //Contract.Requires(expr != null);

       return visitor.VisitBoogieFunctionOp(expr, arg);

     }

   }

@@ -1745,7 +1770,7 @@ Contract.Ensures(Contract.Result<Type>() != null);
       this.VarType = type;

     }

     public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

       return visitor.Visit(this, arg);

     }

   }

@@ -1870,19 +1895,20 @@ Contract.Ensures(Contract.Result<Type>() != null);
         HelperFuns.PolyHash(123, 11, Triggers);

     }

 

-    internal VCExprQuantifier(Quantifier kind, List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ boundVars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) :base(typeParams, boundVars, body){

+    internal VCExprQuantifier(Quantifier kind, List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ boundVars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body)

+      : base(typeParams, boundVars, body) {

       Contract.Requires(body != null);

       Contract.Requires(infos != null);

       Contract.Requires(cce.NonNullElements(triggers));

       Contract.Requires(cce.NonNullElements(boundVars));

       Contract.Requires(cce.NonNullElements(typeParams));

-      

+

       this.Quan = kind;

       this.Triggers = triggers;

       this.Infos = infos;

     }

     public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

       return visitor.Visit(this, arg);

     }

   }

@@ -1978,22 +2004,23 @@ Contract.Ensures(Contract.Result<Type>() != null);
       return Bindings.GetEnumerator();

     }

 

-    private static List<VCExprVar/*!*/>/*!*/ toSeq(List<VCExprLetBinding/*!*/>/*!*/ bindings){

-Contract.Requires(cce.NonNullElements(bindings));

-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));

-      List<VCExprVar> res = new List<VCExprVar> ();

+    private static List<VCExprVar/*!*/>/*!*/ toSeq(List<VCExprLetBinding/*!*/>/*!*/ bindings) {

+      Contract.Requires(cce.NonNullElements(bindings));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));

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

       foreach (VCExprLetBinding/*!*/ b in bindings)

         res.Add(b.V);

       return res;

     }

 

-    internal VCExprLet(List<VCExprLetBinding/*!*/>/*!*/ bindings, VCExpr/*!*/ body) :base(new List<TypeVariable/*!*/>(), toSeq(bindings), body){

+    internal VCExprLet(List<VCExprLetBinding/*!*/>/*!*/ bindings, VCExpr/*!*/ body)

+      : base(new List<TypeVariable/*!*/>(), toSeq(bindings), body) {

       Contract.Requires(cce.NonNullElements(bindings));

       Contract.Requires(body != null);

       this.Bindings = bindings;

     }

     public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {

-      Contract.Requires(visitor != null);

+      //Contract.Requires(visitor != null);

       return visitor.Visit(this, arg);

     }

   }

diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index c79c08db..adb3b27e 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -14,50 +14,44 @@ using Microsoft.Basetypes;
 // A simple visitor for turning a VCExpr into a human-readable string

 // (S-expr syntax)

 

-namespace Microsoft.Boogie.VCExprAST

-{

+namespace Microsoft.Boogie.VCExprAST {

 

   public class VCExprPrinter : IVCExprVisitor<bool, TextWriter/*!*/> {

     private VCExprOpPrinter OpPrinterVar = null;

-    private VCExprOpPrinter/*!*/ OpPrinter { get {Contract.Ensures(Contract.Result<VCExprOpPrinter>() != null);

+    private VCExprOpPrinter/*!*/ OpPrinter {

+      get {

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

 

-      if (OpPrinterVar == null)

-        OpPrinterVar = new VCExprOpPrinter(this);

-      return OpPrinterVar;

-    } }

+        if (OpPrinterVar == null)

+          OpPrinterVar = new VCExprOpPrinter(this);

+        return OpPrinterVar;

+      }

+    }

 

-    public void Print(VCExpr expr, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(expr != null);

+    public void Print(VCExpr expr, TextWriter wr) {

+      Contract.Requires(wr != null);

+      Contract.Requires(expr != null);

       expr.Accept<bool, TextWriter/*!*/>(this, wr);

     }

 

-    public bool Visit(VCExprLiteral node, TextWriter wr)

-    {

-        Contract.Requires(wr != null);

-        Contract.Requires(node != null);

-        if (node == VCExpressionGenerator.True)

-        {

-            wr.Write("true");

-        }

-        else if (node == VCExpressionGenerator.False)

-        {

-            wr.Write("false");

-        }

-        else if (node is VCExprIntLit)

-        {

-            wr.Write(((VCExprIntLit)node).Val);

-        }

-        else

-        {

-            Contract.Assert(false); throw new cce.UnreachableException();

-        }

-        return true;

+    public bool Visit(VCExprLiteral node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      if (node == VCExpressionGenerator.True) {

+        wr.Write("true");

+      } else if (node == VCExpressionGenerator.False) {

+        wr.Write("false");

+      } else if (node is VCExprIntLit) {

+        wr.Write(((VCExprIntLit)node).Val);

+      } else {

+        Contract.Assert(false);

+        throw new cce.UnreachableException();

+      }

+      return true;

     }

-    public bool Visit(VCExprNAry node, TextWriter wr)

-    {

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool Visit(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       VCExprOp/*!*/ op = node.Op;

       Contract.Assert(op != null);

 

@@ -67,7 +61,7 @@ Contract.Requires(node != null);
 

         wr.Write("({0}",

                  op.Equals(VCExpressionGenerator.AndOp) ? "And" : "Or");

-        IEnumerator/*!*/ enumerator = new VCExprNAryUniformOpEnumerator (node);

+        IEnumerator/*!*/ enumerator = new VCExprNAryUniformOpEnumerator(node);

         Contract.Assert(enumerator != null);

         while (enumerator.MoveNext()) {

           VCExprNAry naryExpr = enumerator.Current as VCExprNAry;

@@ -84,15 +78,15 @@ Contract.Requires(node != null);
 

       return node.Accept<bool, TextWriter/*!*/>(OpPrinter, wr);

     }

-    public bool Visit(VCExprVar node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool Visit(VCExprVar node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       wr.Write(node.Name);

       return true;

     }

-    public bool Visit(VCExprQuantifier node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool Visit(VCExprQuantifier node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       string/*!*/ quan = node.Quan == Quantifier.ALL ? "Forall" : "Exists";

       Contract.Assert(quan != null);

 

@@ -101,8 +95,8 @@ Contract.Requires(node != null);
       if (node.TypeParameters.Count > 0) {

         wr.Write("<");

         string/*!*/ sep = "";

-        foreach(TypeVariable/*!*/ v in node.TypeParameters){

-Contract.Assert(v != null);

+        foreach (TypeVariable/*!*/ v in node.TypeParameters) {

+          Contract.Assert(v != null);

           wr.Write(sep);

           sep = ", ";

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

@@ -112,27 +106,27 @@ Contract.Assert(v != null);
 

       if (node.BoundVars.Count > 0) {

         string/*!*/ sep = "";

-        foreach(VCExprVar/*!*/ v in node.BoundVars){

-Contract.Assert(v != null);

+        foreach (VCExprVar/*!*/ v in node.BoundVars) {

+          Contract.Assert(v != null);

           wr.Write(sep);

           sep = ", ";

           Print(v, wr);

         }

         wr.Write(" ");

       }

-      

+

       wr.Write(":: ");

 

       if (node.Triggers.Count > 0) {

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

         string/*!*/ sep = "";

-        foreach(VCTrigger/*!*/ t in node.Triggers){

-Contract.Assert(t != null);

+        foreach (VCTrigger/*!*/ t in node.Triggers) {

+          Contract.Assert(t != null);

           wr.Write(sep);

           sep = ", ";

           string/*!*/ sep2 = "";

-          foreach(VCExpr/*!*/ e in t.Exprs){

-Contract.Assert(e != null);

+          foreach (VCExpr/*!*/ e in t.Exprs) {

+            Contract.Assert(e != null);

             wr.Write(sep2);

             sep2 = "+";

             Print(e, wr);

@@ -145,14 +139,14 @@ Contract.Assert(e != null);
       wr.Write(")");

       return true;

     }

-    public bool Visit(VCExprLet node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool Visit(VCExprLet node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       wr.Write("(Let ");

 

       string/*!*/ sep = "";

-      foreach(VCExprLetBinding/*!*/ b in node){

-Contract.Assert(b != null);

+      foreach (VCExprLetBinding/*!*/ b in node) {

+        Contract.Assert(b != null);

         wr.Write(sep);

         sep = ", ";

         Print(b.V, wr);

@@ -175,18 +169,18 @@ Contract.Assert(b != null);
     }

 

 

-    public VCExprOpPrinter(VCExprPrinter exprPrinter){

-Contract.Requires(exprPrinter != null);

+    public VCExprOpPrinter(VCExprPrinter exprPrinter) {

+      Contract.Requires(exprPrinter != null);

       this.ExprPrinter = exprPrinter;

     }

 

-    private bool PrintNAry(string op, VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

-Contract.Requires(op != null);

+    private bool PrintNAry(string op, VCExprNAry node, TextWriter wr) {

+      Contract.Requires(wr != null);

+      Contract.Requires(node != null);

+      Contract.Requires(op != null);

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

-      foreach(VCExpr/*!*/ arg in node){

-Contract.Assert(arg != null);

+      foreach (VCExpr/*!*/ arg in node) {

+        Contract.Assert(arg != null);

         wr.Write(" ");

         ExprPrinter.Print(arg, wr);

       }

@@ -194,148 +188,150 @@ Contract.Assert(arg != null);
       return true;

     }

 

-    public bool VisitNotOp    (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitNotOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("!", node, wr);

     }

-    public bool VisitEqOp     (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitEqOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("==", node, wr);

     }

-    public bool VisitNeqOp    (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitNeqOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("!=", node, wr);

     }

-    public bool VisitAndOp    (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

-      Contract.Assert(false); throw new cce.UnreachableException();

-    }

-    public bool VisitOrOp     (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

-      Contract.Assert(false); throw new cce.UnreachableException();

-    }

-    public bool VisitImpliesOp (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitAndOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      Contract.Assert(false);

+      throw new cce.UnreachableException();

+    }

+    public bool VisitOrOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      Contract.Assert(false);

+      throw new cce.UnreachableException();

+    }

+    public bool VisitImpliesOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("Implies", node, wr);

     }

-    public bool VisitDistinctOp (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitDistinctOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("Distinct", node, wr);

     }

-    public bool VisitLabelOp  (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

-VCExprLabelOp/*!*/ op = (VCExprLabelOp)node.Op;

-Contract.Assert(op != null);

+    public bool VisitLabelOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      VCExprLabelOp/*!*/ op = (VCExprLabelOp)node.Op;

+      Contract.Assert(op != null);

       return PrintNAry("Label " + op.label, node, wr);

     }

-    public bool VisitSelectOp (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitSelectOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("Select", node, wr);

     }

-    public bool VisitStoreOp  (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitStoreOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("Store", node, wr);

     }

-    public bool VisitBvOp     (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitBvOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("Bv", node, wr);

     }

-    public bool VisitBvExtractOp(VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitBvExtractOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("BvExtract", node, wr);

     }

-    public bool VisitBvConcatOp (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitBvConcatOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("BvConcat", node, wr);

     }

-    public bool VisitIfThenElseOp(VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitIfThenElseOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

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

     }

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

-      Contract.Requires(node!=null);

-      Contract.Requires(wr != null);

+      //Contract.Requires(node!=null);

+      //Contract.Requires(wr != null);

       VCExprCustomOp op = (VCExprCustomOp)node.Op;

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

     }

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

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

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

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       if (CommandLineOptions.Clo.ReflectAdd) {

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

       } else {

         return PrintNAry("+", node, wr);

       }

     }

-    public bool VisitSubOp          (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitSubOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("-", node, wr);

     }

-    public bool VisitMulOp          (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitMulOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("*", node, wr);

     }

-    public bool VisitDivOp          (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitDivOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("/", node, wr);

     }

-    public bool VisitModOp          (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitModOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("%", node, wr);

     }

-    public bool VisitLtOp           (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitLtOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("<", node, wr);

     }

-    public bool VisitLeOp           (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitLeOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("<=", node, wr);

     }

-    public bool VisitGtOp           (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitGtOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry(">", node, wr);

     }

-    public bool VisitGeOp           (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitGeOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry(">=", node, wr);

     }

-    public bool VisitSubtypeOp      (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitSubtypeOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("<:", node, wr);

     }

-    public bool VisitSubtype3Op     (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

+    public bool VisitSubtype3Op(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

       return PrintNAry("<::", node, wr);

     }

-    public bool VisitBoogieFunctionOp (VCExprNAry node, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(node != null);

-VCExprBoogieFunctionOp/*!*/ op = (VCExprBoogieFunctionOp)node.Op;

-Contract.Assert(op != null);

+    public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      VCExprBoogieFunctionOp/*!*/ op = (VCExprBoogieFunctionOp)node.Op;

+      Contract.Assert(op != null);

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

     }

   }

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index e87b04ce..3e65ec23 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -17,7 +17,7 @@ namespace Microsoft.Boogie.VCExprAST {
   using Microsoft.Boogie;

 

   [ContractClass(typeof(IVCExprVisitorContracts<,>))]

-  public interface IVCExprVisitor<Result,Arg> {

+  public interface IVCExprVisitor<Result, Arg> {

     Result Visit(VCExprLiteral/*!*/ node, Arg arg);

     Result Visit(VCExprNAry/*!*/ node, Arg arg);

     Result Visit(VCExprVar/*!*/ node, Arg arg);

@@ -25,7 +25,7 @@ namespace Microsoft.Boogie.VCExprAST {
     Result Visit(VCExprLet/*!*/ node, Arg arg);

   }

   [ContractClassFor(typeof(IVCExprVisitor<,>))]

-  public abstract class IVCExprVisitorContracts<Result,Arg> : IVCExprVisitor<Result,Arg> {

+  public abstract class IVCExprVisitorContracts<Result, Arg> : IVCExprVisitor<Result, Arg> {

     #region IVCExprVisitor Members

 

     public Result Visit(VCExprLiteral node, Arg arg) {

@@ -83,10 +83,10 @@ 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);

+    Result VisitCustomOp(VCExprNAry node, Arg arg);

   }

   [ContractClassFor(typeof(IVCExprOpVisitor<,>))]

-  public abstract class IVCExprOpVisitorContracts<Result, Arg>:IVCExprOpVisitor<Result,Arg> {

+  public abstract class IVCExprOpVisitorContracts<Result, Arg> : IVCExprOpVisitor<Result, Arg> {

     #region IVCExprOpVisitor<Result,Arg> Members

 

     public Result VisitNotOp(VCExprNAry node, Arg arg) {

@@ -248,23 +248,22 @@ namespace Microsoft.Boogie.VCExprAST {
     }

 

     public virtual Result Visit(VCExprLiteral node, Arg arg) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

       return StandardResult(node, arg);

     }

 

-    public virtual Result Visit(VCExprNAry node, Arg arg){

-Contract.Requires(node != null);

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

+      //Contract.Requires(node != null);

       Result res = StandardResult(node, arg);

 

 

       if (node.TypeParamArity == 0 &&

           (node.Op == VCExpressionGenerator.AndOp ||

-           node.Op == VCExpressionGenerator.OrOp  ||

-           node.Op == VCExpressionGenerator.ImpliesOp))

-      {

+           node.Op == VCExpressionGenerator.OrOp ||

+           node.Op == VCExpressionGenerator.ImpliesOp)) {

         Contract.Assert(node.Op != null);

         VCExprOp op = node.Op;

-        

+

         IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);

         enumerator.MoveNext();  // skip the node itself

 

@@ -278,34 +277,40 @@ Contract.Requires(node != null);
           }

         }

       } else {

-        foreach (VCExpr e in node){Contract.Assert(e != null);

-          e.Accept(this, arg);}

+        foreach (VCExpr e in node) {

+          Contract.Assert(e != null);

+          e.Accept(this, arg);

+        }

       }

 

       return res;

     }

 

     public virtual Result Visit(VCExprVar node, Arg arg) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

       return StandardResult(node, arg);

     }

-    public virtual Result Visit(VCExprQuantifier node, Arg arg){

-Contract.Requires(node != null);

+    public virtual Result Visit(VCExprQuantifier node, Arg arg) {

+      //Contract.Requires(node != null);

       Result res = StandardResult(node, arg);

-      foreach (VCTrigger/*!*/ trigger in node.Triggers){Contract.Assert(trigger != null);

-      foreach (VCExpr/*!*/ expr in trigger.Exprs) {

-        Contract.Assert(expr != null);

-          expr.Accept(this, arg);}}

+      foreach (VCTrigger/*!*/ trigger in node.Triggers) {

+        Contract.Assert(trigger != null);

+        foreach (VCExpr/*!*/ expr in trigger.Exprs) {

+          Contract.Assert(expr != null);

+          expr.Accept(this, arg);

+        }

+      }

       node.Body.Accept(this, arg);

       return res;

     }

-    public virtual Result Visit(VCExprLet node, Arg arg){

-Contract.Requires(node != null);

+    public virtual Result Visit(VCExprLet node, Arg arg) {

+      //Contract.Requires(node != null);

       Result res = StandardResult(node, arg);

       // visit the bound expressions first

       foreach (VCExprLetBinding/*!*/ binding in node) {

         Contract.Assert(binding != null);

-        binding.E.Accept(this, arg);}

+        binding.E.Accept(this, arg);

+      }

       node.Body.Accept(this, arg);

       return res;

     }

@@ -333,8 +338,8 @@ Contract.Requires(node != null);
       Contract.Invariant(cce.NonNullElements(ExprTodo));

     }

 

-    public VCExprNAryEnumerator(VCExprNAry completeExpr){

-Contract.Requires(completeExpr != null);

+    public VCExprNAryEnumerator(VCExprNAry completeExpr) {

+      Contract.Requires(completeExpr != null);

       this.CompleteExpr = completeExpr;

       Stack<VCExpr/*!*/>/*!*/ exprTodo = new Stack<VCExpr/*!*/>();

       exprTodo.Push(completeExpr);

@@ -395,7 +400,7 @@ Contract.Requires(completeExpr != null);
       this.Op = completeExpr.Op;

     }

     protected override bool Descend(VCExprNAry expr) {

-      Contract.Requires(expr != null);

+      //Contract.Requires(expr != null);

       return expr.Op.Equals(Op) &&

         // we never skip nodes with type parameters

         // (those are too interesting ...)

@@ -456,33 +461,42 @@ Contract.Requires(completeExpr != null);
         dict[sym] = n - 1;

     }

 

-    public override Result Visit(VCExprQuantifier node, Arg arg){

-Contract.Requires(node != null);

+    public override Result Visit(VCExprQuantifier node, Arg arg) {

+      Contract.Requires(node != null);

       // we temporarily add bound (term and type) variables to the

       // corresponding lists

-      foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null);

-        AddBoundVar<VCExprVar>(BoundTermVarsDict, v);}

-      foreach (TypeVariable/*!*/ v in node.TypeParameters){Contract.Assert(v != null);

-        AddBoundVar<TypeVariable>(BoundTypeVarsDict, v);}

+      foreach (VCExprVar/*!*/ v in node.BoundVars) {

+        Contract.Assert(v != null);

+        AddBoundVar<VCExprVar>(BoundTermVarsDict, v);

+      }

+      foreach (TypeVariable/*!*/ v in node.TypeParameters) {

+        Contract.Assert(v != null);

+        AddBoundVar<TypeVariable>(BoundTypeVarsDict, v);

+      }

 

       Result res;

       try {

         res = VisitAfterBinding(node, arg);

       } finally {

-        foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null);

-          RemoveBoundVar<VCExprVar>(BoundTermVarsDict, v);}

+        foreach (VCExprVar/*!*/ v in node.BoundVars) {

+          Contract.Assert(v != null);

+          RemoveBoundVar<VCExprVar>(BoundTermVarsDict, v);

+        }

         foreach (TypeVariable/*!*/ v in node.TypeParameters) {

           Contract.Assert(v != null);

-          RemoveBoundVar<TypeVariable>(BoundTypeVarsDict, v);}

+          RemoveBoundVar<TypeVariable>(BoundTypeVarsDict, v);

+        }

       }

       return res;

     }

-    public override Result Visit(VCExprLet node, Arg arg){

-Contract.Requires(node != null);

+    public override Result Visit(VCExprLet node, Arg arg) {

+      Contract.Requires(node != null);

       // we temporarily add bound term variables to the

       // corresponding lists

-      foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null);

-        AddBoundVar<VCExprVar>(BoundTermVarsDict, v);}

+      foreach (VCExprVar/*!*/ v in node.BoundVars) {

+        Contract.Assert(v != null);

+        AddBoundVar<VCExprVar>(BoundTermVarsDict, v);

+      }

 

       Result res;

       try {

@@ -529,34 +543,38 @@ Contract.Requires(node != null);
     }

 

     public virtual Result Visit(VCExprLiteral node, Arg arg) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

       return CombineResults(new List<Result>(), arg);

     }

-    public virtual Result Visit(VCExprNAry node, Arg arg){

-Contract.Requires(node != null);

-      List<Result>/*!*/ results = new List<Result> ();

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

+      //Contract.Requires(node != null);

+      List<Result>/*!*/ results = new List<Result>();

       foreach (VCExpr/*!*/ subnode in node) {

         Contract.Assert(subnode != null);

-        results.Add(subnode.Accept(this, arg));}

+        results.Add(subnode.Accept(this, arg));

+      }

       return CombineResults(results, arg);

     }

     public virtual Result Visit(VCExprVar node, Arg arg) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

       return CombineResults(new List<Result>(), arg);

     }

-    public virtual Result Visit(VCExprQuantifier node, Arg arg){

-Contract.Requires(node != null);

-      List<Result>/*!*/ result = new List<Result> ();

+    public virtual Result Visit(VCExprQuantifier node, Arg arg) {

+      //Contract.Requires(node != null);

+      List<Result>/*!*/ result = new List<Result>();

       result.Add(node.Body.Accept(this, arg));

-      foreach (VCTrigger/*!*/ trigger in node.Triggers){Contract.Assert(trigger != null);

-      foreach (VCExpr/*!*/ expr in trigger.Exprs) {

-        Contract.Assert(expr != null);

-          result.Add(expr.Accept(this, arg));}}

+      foreach (VCTrigger/*!*/ trigger in node.Triggers) {

+        Contract.Assert(trigger != null);

+        foreach (VCExpr/*!*/ expr in trigger.Exprs) {

+          Contract.Assert(expr != null);

+          result.Add(expr.Accept(this, arg));

+        }

+      }

       return CombineResults(result, arg);

     }

-    public virtual Result Visit(VCExprLet node, Arg arg){

-Contract.Requires(node != null);

-      List<Result>/*!*/ results = new List<Result> ();

+    public virtual Result Visit(VCExprLet node, Arg arg) {

+      //Contract.Requires(node != null);

+      List<Result>/*!*/ results = new List<Result>();

       // visit the bound expressions first

       foreach (VCExprLetBinding/*!*/ binding in node) {

         Contract.Assert(binding != null);

@@ -575,160 +593,161 @@ Contract.Requires(node != null);
   }

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

 

-    public class SizeComputingVisitor : TraversingVCExprVisitor<bool, bool> {

+  public class SizeComputingVisitor : TraversingVCExprVisitor<bool, bool> {

 

-      private int Size = 0;

+    private int Size = 0;

 

-      public static int ComputeSize(VCExpr expr) {

-        Contract.Requires(expr != null);

-        SizeComputingVisitor/*!*/ visitor = new SizeComputingVisitor();

-        visitor.Traverse(expr, true);

-        return visitor.Size;

-      }

+    public static int ComputeSize(VCExpr expr) {

+      Contract.Requires(expr != null);

+      SizeComputingVisitor/*!*/ visitor = new SizeComputingVisitor();

+      visitor.Traverse(expr, true);

+      return visitor.Size;

+    }

 

-      protected override bool StandardResult(VCExpr node, bool arg) {

-        Contract.Requires(node != null);

-        Size = Size + 1;

-        return true;

-      }

+    protected override bool StandardResult(VCExpr node, bool arg) {

+      //Contract.Requires(node != null);

+      Size = Size + 1;

+      return true;

     }

+  }

 

-    ////////////////////////////////////////////////////////////////////////////

+  ////////////////////////////////////////////////////////////////////////////

 

-    // Collect all free term and type variables in a VCExpr. Type variables

-    // can occur free either in the types of bound variables, or in the type

-    // parameters of VCExprNAry.

-

-    // the result and argument (of type bool) are not used currently

-    public class FreeVariableCollector : BoundVarTraversingVCExprVisitor<bool, bool> {

-      public readonly Dictionary<VCExprVar/*!*/, object>/*!*/ FreeTermVars = new Dictionary<VCExprVar/*!*/, object>();

-      public readonly List<TypeVariable/*!*/>/*!*/ FreeTypeVars = new List<TypeVariable/*!*/>();

-      [ContractInvariantMethod]

-      void ObjectInvariant() {

-        Contract.Invariant(cce.NonNullElements(FreeTermVars));

-        Contract.Invariant(cce.NonNullElements(FreeTypeVars));

-      }

+  // Collect all free term and type variables in a VCExpr. Type variables

+  // can occur free either in the types of bound variables, or in the type

+  // parameters of VCExprNAry.

+

+  // the result and argument (of type bool) are not used currently

+  public class FreeVariableCollector : BoundVarTraversingVCExprVisitor<bool, bool> {

+    public readonly Dictionary<VCExprVar/*!*/, object>/*!*/ FreeTermVars = new Dictionary<VCExprVar/*!*/, object>();

+    public readonly List<TypeVariable/*!*/>/*!*/ FreeTypeVars = new List<TypeVariable/*!*/>();

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(cce.NonNullElements(FreeTermVars));

+      Contract.Invariant(cce.NonNullElements(FreeTypeVars));

+    }

 

 

-      // not used

-      protected override bool StandardResult(VCExpr node, bool arg) {

-        Contract.Requires(node != null);

-        return true;

-      }

+    // not used

+    protected override bool StandardResult(VCExpr node, bool arg) {

+      //Contract.Requires(node != null);

+      return true;

+    }

 

-      public static Dictionary<VCExprVar/*!*/, object/*!*/>/*!*/ FreeTermVariables(VCExpr node) {

-        Contract.Requires(node != null);

-        Contract.Ensures(cce.NonNullElements(Contract.Result<Dictionary<VCExprVar, object>>()));

-        FreeVariableCollector collector = new FreeVariableCollector();

-        collector.Traverse(node, true);

-        return collector.FreeTermVars;

-      }

+    public static Dictionary<VCExprVar/*!*/, object/*!*/>/*!*/ FreeTermVariables(VCExpr node) {

+      Contract.Requires(node != null);

+      Contract.Ensures(cce.NonNullElements(Contract.Result<Dictionary<VCExprVar, object>>()));

+      FreeVariableCollector collector = new FreeVariableCollector();

+      collector.Traverse(node, true);

+      return collector.FreeTermVars;

+    }

 

-      public static List<TypeVariable/*!*/>/*!*/ FreeTypeVariables(VCExpr node) {

-        Contract.Requires(node != null);

-        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));

-        FreeVariableCollector collector = new FreeVariableCollector();

-        collector.Traverse(node, true);

-        return collector.FreeTypeVars;

-      }

+    public static List<TypeVariable/*!*/>/*!*/ FreeTypeVariables(VCExpr node) {

+      Contract.Requires(node != null);

+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));

+      FreeVariableCollector collector = new FreeVariableCollector();

+      collector.Traverse(node, true);

+      return collector.FreeTypeVars;

+    }

 

-      public void Reset() {

-        FreeTermVars.Clear();

-        FreeTypeVars.Clear();

-      }

+    public void Reset() {

+      FreeTermVars.Clear();

+      FreeTypeVars.Clear();

+    }

 

-      public void Collect(VCExpr node) {

-        Contract.Requires(node != null);

-        Traverse(node, true);

-      }

+    public void Collect(VCExpr node) {

+      Contract.Requires(node != null);

+      Traverse(node, true);

+    }

 

-      public void Collect(Type type) {

-        Contract.Requires(type != null);

-        AddTypeVariables(type.FreeVariables.ToList());

-      }

+    public void Collect(Type type) {

+      Contract.Requires(type != null);

+      AddTypeVariables(type.FreeVariables.ToList());

+    }

 

-      /////////////////////////////////////////////////////////////////////////

+    /////////////////////////////////////////////////////////////////////////

 

-      private void CollectTypeVariables(IEnumerable<VCExprVar/*!*/>/*!*/ boundVars){Contract.Requires(cce.NonNullElements(boundVars));

+    private void CollectTypeVariables(IEnumerable<VCExprVar/*!*/>/*!*/ boundVars) {

+      Contract.Requires(cce.NonNullElements(boundVars));

       foreach (VCExprVar/*!*/ var in boundVars) {

         Contract.Assert(var != null);

         Collect(var.Type);

       }

     }

 

-      private void AddTypeVariables(IEnumerable<TypeVariable/*!*/>/*!*/ typeVars) {

-        Contract.Requires(cce.NonNullElements(typeVars));

-        foreach (TypeVariable/*!*/ tvar in typeVars) {

-          Contract.Assert(tvar != null);

-          if (!BoundTypeVars.Contains(tvar) && !FreeTypeVars.Contains(tvar))

-            FreeTypeVars.Add(tvar);

-        }

+    private void AddTypeVariables(IEnumerable<TypeVariable/*!*/>/*!*/ typeVars) {

+      Contract.Requires(cce.NonNullElements(typeVars));

+      foreach (TypeVariable/*!*/ tvar in typeVars) {

+        Contract.Assert(tvar != null);

+        if (!BoundTypeVars.Contains(tvar) && !FreeTypeVars.Contains(tvar))

+          FreeTypeVars.Add(tvar);

       }

+    }

 

-      public override bool Visit(VCExprVar node, bool arg) {

-        Contract.Requires(node != null);

-        if (!BoundTermVars.Contains(node) && !FreeTermVars.ContainsKey(node)) {

-          FreeTermVars.Add(node, null);

-          Collect(node.Type);

-        }

-        return true;

+    public override bool Visit(VCExprVar node, bool arg) {

+      Contract.Requires(node != null);

+      if (!BoundTermVars.Contains(node) && !FreeTermVars.ContainsKey(node)) {

+        FreeTermVars.Add(node, null);

+        Collect(node.Type);

       }

+      return true;

+    }

 

-      public override bool Visit(VCExprNAry node, bool arg) {

-        Contract.Requires(node != null);

-        foreach (Type/*!*/ t in node.TypeArguments) {

-          Contract.Assert(t != null);

-          Collect(t);

-        }

-        return base.Visit(node, arg);

+    public override bool Visit(VCExprNAry node, bool arg) {

+      Contract.Requires(node != null);

+      foreach (Type/*!*/ t in node.TypeArguments) {

+        Contract.Assert(t != null);

+        Collect(t);

       }

+      return base.Visit(node, arg);

+    }

 

-      protected override bool VisitAfterBinding(VCExprQuantifier node, bool arg) {

-        Contract.Requires(node != null);

-        CollectTypeVariables(node.BoundVars);

-        return base.VisitAfterBinding(node, arg);

-      }

+    protected override bool VisitAfterBinding(VCExprQuantifier node, bool arg) {

+      //Contract.Requires(node != null);

+      CollectTypeVariables(node.BoundVars);

+      return base.VisitAfterBinding(node, arg);

+    }

 

-      protected override bool VisitAfterBinding(VCExprLet node, bool arg) {

-        Contract.Requires(node != null);

-        CollectTypeVariables(node.BoundVars);

-        return base.VisitAfterBinding(node, arg);

-      }

+    protected override bool VisitAfterBinding(VCExprLet node, bool arg) {

+      //Contract.Requires(node != null);

+      CollectTypeVariables(node.BoundVars);

+      return base.VisitAfterBinding(node, arg);

     }

+  }

 

-    ////////////////////////////////////////////////////////////////////////////

-    // Framework for mutating VCExprs

-

-    // The Visit implementations in the following visitor work

-    // recursively, apart from the implementation for VCExprNAry that

-    // uses its own stack when applied to nested nodes with the same

-    // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary

-    // to avoid stack overflows (like in TraversingVCExprVisitor)

-

-    public abstract class MutatingVCExprVisitor<Arg>

-                          : IVCExprVisitor<VCExpr/*!*/, Arg> {

-      protected readonly VCExpressionGenerator/*!*/ Gen;

-      [ContractInvariantMethod]

-      void ObjectInvariant() {

-        Contract.Invariant(Gen != null);

-      }

+  ////////////////////////////////////////////////////////////////////////////

+  // Framework for mutating VCExprs

 

+  // The Visit implementations in the following visitor work

+  // recursively, apart from the implementation for VCExprNAry that

+  // uses its own stack when applied to nested nodes with the same

+  // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary

+  // to avoid stack overflows (like in TraversingVCExprVisitor)

 

-      public MutatingVCExprVisitor(VCExpressionGenerator gen) {

-        Contract.Requires(gen != null);

-        this.Gen = gen;

-      }

+  public abstract class MutatingVCExprVisitor<Arg>

+                        : IVCExprVisitor<VCExpr/*!*/, Arg> {

+    protected readonly VCExpressionGenerator/*!*/ Gen;

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(Gen != null);

+    }

 

-      public VCExpr Mutate(VCExpr expr, Arg arg) {

-        Contract.Requires(expr != null);

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

-        return expr.Accept(this, arg);

-      }

 

-      public List<VCExpr/*!*/>/*!*/ MutateSeq(IEnumerable<VCExpr/*!*/>/*!*/ exprs, Arg arg){

-Contract.Requires(cce.NonNullElements(exprs));

-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));

-      List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/> ();

+    public MutatingVCExprVisitor(VCExpressionGenerator gen) {

+      Contract.Requires(gen != null);

+      this.Gen = gen;

+    }

+

+    public VCExpr Mutate(VCExpr expr, Arg arg) {

+      Contract.Requires(expr != null);

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

+      return expr.Accept(this, arg);

+    }

+

+    public List<VCExpr/*!*/>/*!*/ MutateSeq(IEnumerable<VCExpr/*!*/>/*!*/ exprs, Arg arg) {

+      Contract.Requires(cce.NonNullElements(exprs));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));

+      List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>();

       foreach (VCExpr/*!*/ expr in exprs) {

         Contract.Assert(expr != null);

         res.Add(expr.Accept(this, arg));

@@ -736,13 +755,14 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
       return res;

     }

 

-      private List<VCExpr/*!*/>/*!*/ MutateList(List<VCExpr/*!*/>/*!*/ exprs, Arg arg){

-Contract.Requires(cce.NonNullElements(exprs));

-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));

+    private List<VCExpr/*!*/>/*!*/ MutateList(List<VCExpr/*!*/>/*!*/ exprs, Arg arg) {

+      Contract.Requires(cce.NonNullElements(exprs));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));

       bool changed = false;

-      List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/> ();

-      foreach (VCExpr/*!*/ expr in exprs) {Contract.Assert(expr != null);

-      VCExpr/*!*/ newExpr = expr.Accept(this, arg);

+      List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>();

+      foreach (VCExpr/*!*/ expr in exprs) {

+        Contract.Assert(expr != null);

+        VCExpr/*!*/ newExpr = expr.Accept(this, arg);

         if (!Object.ReferenceEquals(expr, newExpr))

           changed = true;

         res.Add(newExpr);

@@ -752,65 +772,65 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
       return res;

     }

 

-      public virtual VCExpr Visit(VCExprLiteral node, Arg arg) {

-        Contract.Requires(node != null);

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

-        return node;

-      }

+    public virtual VCExpr Visit(VCExprLiteral node, Arg arg) {

+      //Contract.Requires(node != null);

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

+      return node;

+    }

 

-      ////////////////////////////////////////////////////////////////////////////

-

-      // Special element used to mark the positions in the todo-stack where

-      // results have to be popped from the result-stack.

-      private static readonly VCExpr/*!*/ CombineResultsMarker = new VCExprLiteral(Type.Bool);

-

-      // The todo-stack contains records of the shape

-      //

-      //     arg0

-      //     arg1

-      //     arg2

-      //     ...

-      //     CombineResultsMarker

-      //     f(arg0, arg1, arg2, ...)               (the original expression)

-

-      private readonly Stack<VCExpr/*!*/>/*!*/ NAryExprTodoStack = new Stack<VCExpr/*!*/>();

-      private readonly Stack<VCExpr/*!*/>/*!*/ NAryExprResultStack = new Stack<VCExpr/*!*/>();

-      [ContractInvariantMethod]

-      void ObjectInvarianta() {

-        Contract.Invariant(cce.NonNullElements(NAryExprResultStack));

-        Contract.Invariant(cce.NonNullElements(NAryExprTodoStack));

-      }

+    ////////////////////////////////////////////////////////////////////////////

+

+    // Special element used to mark the positions in the todo-stack where

+    // results have to be popped from the result-stack.

+    private static readonly VCExpr/*!*/ CombineResultsMarker = new VCExprLiteral(Type.Bool);

+

+    // The todo-stack contains records of the shape

+    //

+    //     arg0

+    //     arg1

+    //     arg2

+    //     ...

+    //     CombineResultsMarker

+    //     f(arg0, arg1, arg2, ...)               (the original expression)

+

+    private readonly Stack<VCExpr/*!*/>/*!*/ NAryExprTodoStack = new Stack<VCExpr/*!*/>();

+    private readonly Stack<VCExpr/*!*/>/*!*/ NAryExprResultStack = new Stack<VCExpr/*!*/>();

+    [ContractInvariantMethod]

+    void ObjectInvarianta() {

+      Contract.Invariant(cce.NonNullElements(NAryExprResultStack));

+      Contract.Invariant(cce.NonNullElements(NAryExprTodoStack));

+    }

 

 

-      private void PushTodo(VCExprNAry exprTodo) {

-        Contract.Requires(exprTodo != null);

-        NAryExprTodoStack.Push(exprTodo);

-        NAryExprTodoStack.Push(CombineResultsMarker);

-        for (int i = exprTodo.Arity - 1; i >= 0; --i)

-          NAryExprTodoStack.Push(exprTodo[i]);

-      }

+    private void PushTodo(VCExprNAry exprTodo) {

+      Contract.Requires(exprTodo != null);

+      NAryExprTodoStack.Push(exprTodo);

+      NAryExprTodoStack.Push(CombineResultsMarker);

+      for (int i = exprTodo.Arity - 1; i >= 0; --i)

+        NAryExprTodoStack.Push(exprTodo[i]);

+    }

 

-      public virtual VCExpr Visit(VCExprNAry node, Arg arg){

-Contract.Requires(node != null);

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

+    public virtual VCExpr Visit(VCExprNAry node, Arg arg) {

+      //Contract.Requires(node != null);

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

       VCExprOp/*!*/ op = node.Op;

-        Contract.Assert(op != null);

+      Contract.Assert(op != null);

       int initialStackSize = NAryExprTodoStack.Count;

       int initialResultStackSize = NAryExprResultStack.Count;

 

       PushTodo(node);

-      

+

       while (NAryExprTodoStack.Count > initialStackSize) {

         VCExpr/*!*/ subExpr = NAryExprTodoStack.Pop();

         Contract.Assert(subExpr != null);

-        

+

         if (Object.ReferenceEquals(subExpr, CombineResultsMarker)) {

           //

           // assemble a result

           VCExprNAry/*!*/ originalExpr = (VCExprNAry)NAryExprTodoStack.Pop();

           Contract.Assert(originalExpr != null);

           bool changed = false;

-          List<VCExpr/*!*/>/*!*/ newSubExprs = new List<VCExpr/*!*/> ();

+          List<VCExpr/*!*/>/*!*/ newSubExprs = new List<VCExpr/*!*/>();

 

           for (int i = op.Arity - 1; i >= 0; --i) {

             VCExpr/*!*/ nextSubExpr = NAryExprResultStack.Pop();

@@ -819,15 +839,15 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
               changed = true;

             newSubExprs.Insert(0, nextSubExpr);

           }

-          

+

           NAryExprResultStack.Push(UpdateModifiedNode(originalExpr, newSubExprs, changed, arg));

           //

         } else {

           //

           VCExprNAry narySubExpr = subExpr as VCExprNAry;

           if (narySubExpr != null && narySubExpr.Op.Equals(op) &&

-              // as in VCExprNAryUniformOpEnumerator, all expressions with

-              // type parameters are allowed to be inspected more closely

+            // as in VCExprNAryUniformOpEnumerator, all expressions with

+            // type parameters are allowed to be inspected more closely

               narySubExpr.TypeParamArity == 0) {

             PushTodo(narySubExpr);

           } else {

@@ -841,37 +861,37 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
       return NAryExprResultStack.Pop();

     }

 

-      protected virtual VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, // has any of the subexpressions changed? 

-                                                   bool changed,

-                                                   Arg arg) {

-        Contract.Requires(cce.NonNullElements(newSubExprs));

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

+    protected virtual VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, // has any of the subexpressions changed? 

+                                                 bool changed,

+                                                 Arg arg) {

+      Contract.Requires(cce.NonNullElements(newSubExprs));

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

 

-        if (changed)

-          return Gen.Function(originalNode.Op,

-                              newSubExprs, originalNode.TypeArguments);

-        else

-          return originalNode;

-      }

+      if (changed)

+        return Gen.Function(originalNode.Op,

+                            newSubExprs, originalNode.TypeArguments);

+      else

+        return originalNode;

+    }

 

-      ////////////////////////////////////////////////////////////////////////////

+    ////////////////////////////////////////////////////////////////////////////

 

-      public virtual VCExpr Visit(VCExprVar node, Arg arg) {

-        Contract.Requires(node != null);

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

-        return node;

-      }

+    public virtual VCExpr Visit(VCExprVar node, Arg arg) {

+      //Contract.Requires(node != null);

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

+      return node;

+    }

 

-      protected List<VCTrigger/*!*/>/*!*/ MutateTriggers(List<VCTrigger/*!*/>/*!*/ triggers, Arg arg){

-Contract.Requires(cce.NonNullElements(triggers));

-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));

-      List<VCTrigger/*!*/>/*!*/ newTriggers = new List<VCTrigger/*!*/> ();

+    protected List<VCTrigger/*!*/>/*!*/ MutateTriggers(List<VCTrigger/*!*/>/*!*/ triggers, Arg arg) {

+      Contract.Requires(cce.NonNullElements(triggers));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));

+      List<VCTrigger/*!*/>/*!*/ newTriggers = new List<VCTrigger/*!*/>();

       bool changed = false;

       foreach (VCTrigger/*!*/ trigger in triggers) {

         Contract.Assert(trigger != null);

         List<VCExpr/*!*/>/*!*/ exprs = trigger.Exprs;

         List<VCExpr/*!*/>/*!*/ newExprs = MutateList(exprs, arg);

-        

+

         if (Object.ReferenceEquals(exprs, newExprs)) {

           newTriggers.Add(trigger);

         } else {

@@ -884,15 +904,15 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));
       return newTriggers;

     }

 

-      public virtual VCExpr Visit(VCExprQuantifier node, Arg arg){

-Contract.Requires(node != null);

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

+    public virtual VCExpr Visit(VCExprQuantifier node, Arg arg) {

+      //Contract.Requires(node != null);

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

       bool changed = false;

 

       VCExpr/*!*/ body = node.Body;

-        Contract.Assert(body != null);

+      Contract.Assert(body != null);

       VCExpr/*!*/ newbody = body.Accept(this, arg);

-        Contract.Assert(newbody != null);

+      Contract.Assert(newbody != null);

       if (!Object.ReferenceEquals(body, newbody))

         changed = true;

 

@@ -910,9 +930,9 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
                           newTriggers, node.Infos, newbody);

     }

 

-      public virtual VCExpr Visit(VCExprLet node, Arg arg){

-Contract.Requires(node != null);

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

+    public virtual VCExpr Visit(VCExprLet node, Arg arg) {

+      //Contract.Requires(node != null);

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

       bool changed = false;

 

       VCExpr/*!*/ body = node.Body;

@@ -920,7 +940,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
       if (!Object.ReferenceEquals(body, newbody))

         changed = true;

 

-      List<VCExprLetBinding/*!*/>/*!*/ newbindings = new List<VCExprLetBinding/*!*/> ();

+      List<VCExprLetBinding/*!*/>/*!*/ newbindings = new List<VCExprLetBinding/*!*/>();

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

         VCExprLetBinding/*!*/ binding = node[i];

         Contract.Assert(binding != null);

@@ -938,29 +958,29 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
         return node;

       return Gen.Let(newbindings, newbody);

     }

-    }

+  }

 

-    ////////////////////////////////////////////////////////////////////////////

-    // Substitutions and a visitor for applying substitutions. A substitution can

-    // substitute both type variables and term variables

-

-    public class VCExprSubstitution {

-      private readonly List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ TermSubsts;

-      [ContractInvariantMethod]

-      void TermSubstsInvariantMethod() {

-        Contract.Invariant(TermSubsts != null && Contract.ForAll(TermSubsts, i => cce.NonNullElements(i)));

-      }

-      private readonly List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>/*!*/ TypeSubsts;

-      [ContractInvariantMethod]

-      void TypeSubstsInvariantMethod() {

-        Contract.Invariant(TermSubsts != null && Contract.ForAll(TypeSubsts, i => cce.NonNullElements(i)));

-      }

+  ////////////////////////////////////////////////////////////////////////////

+  // Substitutions and a visitor for applying substitutions. A substitution can

+  // substitute both type variables and term variables

+

+  public class VCExprSubstitution {

+    private readonly List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ TermSubsts;

+    [ContractInvariantMethod]

+    void TermSubstsInvariantMethod() {

+      Contract.Invariant(TermSubsts != null && Contract.ForAll(TermSubsts, i => cce.NonNullElements(i)));

+    }

+    private readonly List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>/*!*/ TypeSubsts;

+    [ContractInvariantMethod]

+    void TypeSubstsInvariantMethod() {

+      Contract.Invariant(TermSubsts != null && Contract.ForAll(TypeSubsts, i => cce.NonNullElements(i)));

+    }

 

-      public VCExprSubstitution(IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ termSubst, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst) {

+    public VCExprSubstitution(IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ termSubst, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst) {

       Contract.Requires(cce.NonNullElements(termSubst));

       Contract.Requires(cce.NonNullElements(typeSubst));

       List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ termSubsts =

-        new List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/> ();

+        new List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>();

       termSubsts.Add(termSubst);

       List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>/*!*/ typeSubsts =

         new List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>();

@@ -969,185 +989,190 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
       this.TypeSubsts = typeSubsts;

     }

 

-      public VCExprSubstitution() :this(new Dictionary<VCExprVar/*!*/, VCExpr/*!*/>(), new Dictionary<TypeVariable/*!*/, Type/*!*/>()){

-        

+    public VCExprSubstitution()

+      : this(new Dictionary<VCExprVar/*!*/, VCExpr/*!*/>(), new Dictionary<TypeVariable/*!*/, Type/*!*/>()) {

+

     }

 

-      public void PushScope() {

-      TermSubsts.Add(new Dictionary<VCExprVar/*!*/, VCExpr/*!*/> ());

+    public void PushScope() {

+      TermSubsts.Add(new Dictionary<VCExprVar/*!*/, VCExpr/*!*/>());

       TypeSubsts.Add(new Dictionary<TypeVariable/*!*/, Type/*!*/>());

     }

 

-      public void PopScope() {

-        TermSubsts.RemoveAt(TermSubsts.Count - 1);

-        TypeSubsts.RemoveAt(TypeSubsts.Count - 1);

-      }

+    public void PopScope() {

+      TermSubsts.RemoveAt(TermSubsts.Count - 1);

+      TypeSubsts.RemoveAt(TypeSubsts.Count - 1);

+    }

 

-      public VCExpr this[VCExprVar/*!*/ var] {

-        get {

-          Contract.Requires(var != null);

-          VCExpr res;

-          for (int i = TermSubsts.Count - 1; i >= 0; --i) {

-            if (TermSubsts[i].TryGetValue(var, out res))

-              return res;

-          }

-          return null;

-        }

-        set {

-          TermSubsts[TermSubsts.Count - 1][var] = cce.NonNull(value);

+    public VCExpr this[VCExprVar/*!*/ var] {

+      get {

+        Contract.Requires(var != null);

+        VCExpr res;

+        for (int i = TermSubsts.Count - 1; i >= 0; --i) {

+          if (TermSubsts[i].TryGetValue(var, out res))

+            return res;

         }

+        return null;

       }

-

-      public Type this[TypeVariable/*!*/ var] {

-        get {

-          Contract.Requires(var != null);

-          Type res;

-          for (int i = TypeSubsts.Count - 1; i >= 0; --i) {

-            if (TypeSubsts[i].TryGetValue(var, out res))

-              return res;

-          }

-          return null;

-        }

-        set {

-          TypeSubsts[TypeSubsts.Count - 1][var] = cce.NonNull(value);

-        }

+      set {

+        TermSubsts[TermSubsts.Count - 1][var] = cce.NonNull(value);

       }

+    }

 

-      public bool ContainsKey(VCExprVar var) {

+    public Type this[TypeVariable/*!*/ var] {

+      get {

         Contract.Requires(var != null);

-        return this[var] != null;

+        Type res;

+        for (int i = TypeSubsts.Count - 1; i >= 0; --i) {

+          if (TypeSubsts[i].TryGetValue(var, out res))

+            return res;

+        }

+        return null;

       }

-

-      public bool ContainsKey(TypeVariable var) {

-        Contract.Requires(var != null);

-        return this[var] != null;

+      set {

+        TypeSubsts[TypeSubsts.Count - 1][var] = cce.NonNull(value);

       }

+    }

 

-      public bool TermSubstIsEmpty {

-        get {

-          return Contract.ForAll(TermSubsts, dict => dict.Count == 0);

-        }

+    public bool ContainsKey(VCExprVar var) {

+      Contract.Requires(var != null);

+      return this[var] != null;

+    }

+

+    public bool ContainsKey(TypeVariable var) {

+      Contract.Requires(var != null);

+      return this[var] != null;

+    }

+

+    public bool TermSubstIsEmpty {

+      get {

+        return Contract.ForAll(TermSubsts, dict => dict.Count == 0);

       }

+    }

 

-      public bool TypeSubstIsEmpty {

-        get {

-          return Contract.ForAll(TypeSubsts, dict => dict.Count == 0);

-        }

+    public bool TypeSubstIsEmpty {

+      get {

+        return Contract.ForAll(TypeSubsts, dict => dict.Count == 0);

       }

+    }

 

-      public IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ ToTypeSubst {

-        get {

-          Contract.Ensures(cce.NonNullElements(Contract.Result < IDictionary<TypeVariable, Type>>()));

-          IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ res = new Dictionary<TypeVariable/*!*/, Type/*!*/>();

-          foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {

-            foreach (KeyValuePair<TypeVariable/*!*/, Type/*!*/> pair in dict) {

-              Contract.Assert(cce.NonNullElements(pair));

-              // later ones overwrite earlier ones

-              res[pair.Key] = pair.Value;

-            }

+    public IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ ToTypeSubst {

+      get {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IDictionary<TypeVariable, Type>>()));

+        IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ res = new Dictionary<TypeVariable/*!*/, Type/*!*/>();

+        foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {

+          foreach (KeyValuePair<TypeVariable/*!*/, Type/*!*/> pair in dict) {

+            Contract.Assert(cce.NonNullElements(pair));

+            // later ones overwrite earlier ones

+            res[pair.Key] = pair.Value;

           }

-          return res;

         }

+        return res;

       }

+    }

 

-      // the variables that are not mapped to themselves

-      public IEnumerable<VCExprVar/*!*/>/*!*/ TermDomain {

-        get {Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<VCExprVar>>()));

-      Dictionary<VCExprVar/*!*/, bool>/*!*/ domain = new Dictionary<VCExprVar/*!*/, bool> ();

-      foreach (IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ dict in TermSubsts) {

-        Contract.Assert(dict != null);

-        foreach (VCExprVar/*!*/ var in dict.Keys) {

-          Contract.Assert(var != null);

-          if (!var.Equals(this[var]))

-            domain.Add(var, true);

-        }

-      }

-      return domain.Keys;

+    // the variables that are not mapped to themselves

+    public IEnumerable<VCExprVar/*!*/>/*!*/ TermDomain {

+      get {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<VCExprVar>>()));

+        Dictionary<VCExprVar/*!*/, bool>/*!*/ domain = new Dictionary<VCExprVar/*!*/, bool>();

+        foreach (IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ dict in TermSubsts) {

+          Contract.Assert(dict != null);

+          foreach (VCExprVar/*!*/ var in dict.Keys) {

+            Contract.Assert(var != null);

+            if (!var.Equals(this[var]))

+              domain.Add(var, true);

+          }

         }

+        return domain.Keys;

       }

+    }

 

-      // the variables that are not mapped to themselves

-      public IEnumerable<TypeVariable/*!*/>/*!*/ TypeDomain {

-        get {Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<TypeVariable>>()));

-      Dictionary<TypeVariable/*!*/, bool>/*!*/ domain = new Dictionary<TypeVariable/*!*/, bool> ();

-      foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {

-        Contract.Assert(dict != null);

-        foreach (TypeVariable/*!*/ var in dict.Keys) {

-          Contract.Assert(var != null);

-          if (!var.Equals(this[var]))

-            domain.Add(var, true);

+    // the variables that are not mapped to themselves

+    public IEnumerable<TypeVariable/*!*/>/*!*/ TypeDomain {

+      get {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<TypeVariable>>()));

+        Dictionary<TypeVariable/*!*/, bool>/*!*/ domain = new Dictionary<TypeVariable/*!*/, bool>();

+        foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {

+          Contract.Assert(dict != null);

+          foreach (TypeVariable/*!*/ var in dict.Keys) {

+            Contract.Assert(var != null);

+            if (!var.Equals(this[var]))

+              domain.Add(var, true);

+          }

         }

+        return domain.Keys;

       }

-      return domain.Keys;

     }

-      }

 

-      public FreeVariableCollector/*!*/ Codomains {

-        get {Contract.Ensures(Contract.Result<FreeVariableCollector>() != null);

+    public FreeVariableCollector/*!*/ Codomains {

+      get {

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

 

-        FreeVariableCollector/*!*/ coll = new FreeVariableCollector ();

+        FreeVariableCollector/*!*/ coll = new FreeVariableCollector();

         foreach (VCExprVar/*!*/ var in TermDomain)

           coll.Collect(cce.NonNull(this)[var]);

         foreach (TypeVariable/*!*/ var in TypeDomain)

           coll.Collect(cce.NonNull(this)[var]);

         return coll;

       }

-      }

+    }

 

-      public VCExprSubstitution Clone() {

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

-      VCExprSubstitution/*!*/ res = new VCExprSubstitution ();

+    public VCExprSubstitution Clone() {

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

+      VCExprSubstitution/*!*/ res = new VCExprSubstitution();

       foreach (IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ dict in TermSubsts)

         res.TermSubsts.Add(HelperFuns.Clone(dict));

       foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts)

         res.TypeSubsts.Add(HelperFuns.Clone(dict));

       return res;

     }

-    }

+  }

 

-    /////////////////////////////////////////////////////////////////////////////////

+  /////////////////////////////////////////////////////////////////////////////////

 

-    public class SubstitutingVCExprVisitor

-                 : MutatingVCExprVisitor<VCExprSubstitution/*!*/> {

-      public SubstitutingVCExprVisitor(VCExpressionGenerator gen) :base(gen){

-        Contract.Requires(gen != null);

-        

-      }

+  public class SubstitutingVCExprVisitor

+               : MutatingVCExprVisitor<VCExprSubstitution/*!*/> {

+    public SubstitutingVCExprVisitor(VCExpressionGenerator gen)

+      : base(gen) {

+      Contract.Requires(gen != null);

+

+    }

 

-      // when descending across a binder, we have to check that no collisions

-      // or variable capture can occur. if this might happen, we replace the

-      // term and type variables bound by the binder with fresh variables

-      private bool CollisionPossible(IEnumerable<TypeVariable/*!*/>/*!*/ typeParams, IEnumerable<VCExprVar/*!*/>/*!*/ boundVars, VCExprSubstitution/*!*/ substitution) {

+    // when descending across a binder, we have to check that no collisions

+    // or variable capture can occur. if this might happen, we replace the

+    // term and type variables bound by the binder with fresh variables

+    private bool CollisionPossible(IEnumerable<TypeVariable/*!*/>/*!*/ typeParams, IEnumerable<VCExprVar/*!*/>/*!*/ boundVars, VCExprSubstitution/*!*/ substitution) {

       Contract.Requires(cce.NonNullElements(typeParams));

       Contract.Requires(cce.NonNullElements(boundVars));

       Contract.Requires(substitution != null);

       // variables can be shadowed by a binder

-      if (Contract.Exists(typeParams, var=> substitution.ContainsKey(var)) ||

-          Contract.Exists(boundVars, var=> substitution.ContainsKey(var)))

+      if (Contract.Exists(typeParams, var => substitution.ContainsKey(var)) ||

+          Contract.Exists(boundVars, var => substitution.ContainsKey(var)))

         return true;

       // compute the codomain of the substitution

       FreeVariableCollector coll = substitution.Codomains;

       Contract.Assert(coll != null);

       // variables could be captured when applying the substitution

-      return Contract.Exists(typeParams, var=> coll.FreeTypeVars.Contains(var)) ||

-             Contract.Exists(boundVars, var=> coll.FreeTermVars.ContainsKey(var));

+      return Contract.Exists(typeParams, var => coll.FreeTypeVars.Contains(var)) ||

+             Contract.Exists(boundVars, var => coll.FreeTermVars.ContainsKey(var));

     }

 

-      // can be overwritten if names of bound variables are to be changed

-      protected virtual string ChooseNewVariableName(string oldName) {

-        Contract.Requires(oldName != null);

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

-        return oldName;

-      }

+    // can be overwritten if names of bound variables are to be changed

+    protected virtual string ChooseNewVariableName(string oldName) {

+      Contract.Requires(oldName != null);

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

+      return oldName;

+    }

 

-      // handle type parameters in VCExprNAry

-      protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, bool changed, VCExprSubstitution/*!*/ substitution) {

-      Contract.Requires(originalNode != null);

-      Contract.Requires(cce.NonNullElements(newSubExprs));

-      Contract.Requires(substitution != null);

+    // handle type parameters in VCExprNAry

+    protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, bool changed, VCExprSubstitution/*!*/ substitution) {

+      //Contract.Requires(originalNode != null);

+      //Contract.Requires(cce.NonNullElements(newSubExprs));

+      //Contract.Requires(substitution != null);

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

 

-      List<Type/*!*/>/*!*/ typeParams = new List<Type/*!*/> ();

+      List<Type/*!*/>/*!*/ typeParams = new List<Type/*!*/>();

       foreach (Type/*!*/ t in originalNode.TypeArguments) {

         Contract.Assert(t != null);

         Type/*!*/ newType = t.Substitute(substitution.ToTypeSubst);

@@ -1162,272 +1187,273 @@ Contract.Ensures(Contract.Result<VCExprSubstitution>() != null);
         return originalNode;

     }

 

-      public override VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution) {

-        Contract.Requires(node != null);

-        Contract.Requires(substitution != null);

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

+    public override VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution) {

+      Contract.Requires(node != null);

+      Contract.Requires(substitution != null);

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

 

-        // the default is to refresh bound variables only if necessary

-        // because of collisions

-        return Visit(node, substitution, false);

-      }

+      // the default is to refresh bound variables only if necessary

+      // because of collisions

+      return Visit(node, substitution, false);

+    }

 

-      public VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution, bool refreshBoundVariables) {

-        Contract.Requires(node != null);

-        Contract.Requires(substitution != null);

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

-

-        substitution.PushScope();

-        try {

-

-          List<TypeVariable/*!*/>/*!*/ typeParams = node.TypeParameters;

-          Contract.Assert(cce.NonNullElements(typeParams));

-          bool refreshAllVariables = refreshBoundVariables ||

-                                     CollisionPossible(node.TypeParameters, node.BoundVars, substitution);

-          if (refreshAllVariables) {

-            // we introduce fresh type variables to ensure that none gets captured

-            typeParams = new List<TypeVariable/*!*/>();

-            foreach (TypeVariable/*!*/ var in node.TypeParameters) {

-              Contract.Assert(var != null);

-              TypeVariable/*!*/ freshVar =

-                new TypeVariable(Token.NoToken, ChooseNewVariableName(var.Name));

-              Contract.Assert(freshVar != null);

-              typeParams.Add(freshVar);

-              substitution[var] = freshVar;

-              // this might overwrite other elements of the substitution, deliberately

-            }

-          }

+    public VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution, bool refreshBoundVariables) {

+      Contract.Requires(node != null);

+      Contract.Requires(substitution != null);

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

+

+      substitution.PushScope();

+      try {

 

-          List<VCExprVar/*!*/>/*!*/ boundVars = node.BoundVars;

-          Contract.Assert(cce.NonNullElements(boundVars));

-          if (refreshAllVariables || !substitution.TypeSubstIsEmpty) {

-            // collisions are possible, or we also substitute type variables. in this case

-            // the bound term variables have to be replaced with fresh variables with the

-            // right types

-            boundVars = new List<VCExprVar/*!*/>();

-            IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;

-            Contract.Assert(cce.NonNullElements(typeSubst));

-            foreach (VCExprVar/*!*/ var in node.BoundVars) {

-              Contract.Assert(var != null);

-              VCExprVar/*!*/ freshVar =

-                Gen.Variable(ChooseNewVariableName(var.Name),

-                             var.Type.Substitute(typeSubst));

-              Contract.Assert(freshVar != null);

-              boundVars.Add(freshVar);

-              substitution[var] = freshVar;

-              // this might overwrite other elements of the substitution, deliberately

-            }

+        List<TypeVariable/*!*/>/*!*/ typeParams = node.TypeParameters;

+        Contract.Assert(cce.NonNullElements(typeParams));

+        bool refreshAllVariables = refreshBoundVariables ||

+                                   CollisionPossible(node.TypeParameters, node.BoundVars, substitution);

+        if (refreshAllVariables) {

+          // we introduce fresh type variables to ensure that none gets captured

+          typeParams = new List<TypeVariable/*!*/>();

+          foreach (TypeVariable/*!*/ var in node.TypeParameters) {

+            Contract.Assert(var != null);

+            TypeVariable/*!*/ freshVar =

+              new TypeVariable(Token.NoToken, ChooseNewVariableName(var.Name));

+            Contract.Assert(freshVar != null);

+            typeParams.Add(freshVar);

+            substitution[var] = freshVar;

+            // this might overwrite other elements of the substitution, deliberately

           }

+        }

 

-          List<VCTrigger/*!*/>/*!*/ newTriggers = new List<VCTrigger/*!*/>();

-          foreach (VCTrigger/*!*/ trigger in node.Triggers) {

-            Contract.Assert(trigger != null);

-            newTriggers.Add(Gen.Trigger(trigger.Pos, MutateSeq(trigger.Exprs, substitution)));

+        List<VCExprVar/*!*/>/*!*/ boundVars = node.BoundVars;

+        Contract.Assert(cce.NonNullElements(boundVars));

+        if (refreshAllVariables || !substitution.TypeSubstIsEmpty) {

+          // collisions are possible, or we also substitute type variables. in this case

+          // the bound term variables have to be replaced with fresh variables with the

+          // right types

+          boundVars = new List<VCExprVar/*!*/>();

+          IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;

+          Contract.Assert(cce.NonNullElements(typeSubst));

+          foreach (VCExprVar/*!*/ var in node.BoundVars) {

+            Contract.Assert(var != null);

+            VCExprVar/*!*/ freshVar =

+              Gen.Variable(ChooseNewVariableName(var.Name),

+                           var.Type.Substitute(typeSubst));

+            Contract.Assert(freshVar != null);

+            boundVars.Add(freshVar);

+            substitution[var] = freshVar;

+            // this might overwrite other elements of the substitution, deliberately

           }

+        }

 

-          VCExpr/*!*/ newBody = Mutate(node.Body, substitution);

-          Contract.Assert(newBody != null);

+        List<VCTrigger/*!*/>/*!*/ newTriggers = new List<VCTrigger/*!*/>();

+        foreach (VCTrigger/*!*/ trigger in node.Triggers) {

+          Contract.Assert(trigger != null);

+          newTriggers.Add(Gen.Trigger(trigger.Pos, MutateSeq(trigger.Exprs, substitution)));

+        }

 

-          return Gen.Quantify(node.Quan, typeParams, boundVars,

-                              newTriggers, node.Infos, newBody);

+        VCExpr/*!*/ newBody = Mutate(node.Body, substitution);

+        Contract.Assert(newBody != null);

 

-        } finally {

-          substitution.PopScope();

-        }

-      }

+        return Gen.Quantify(node.Quan, typeParams, boundVars,

+                            newTriggers, node.Infos, newBody);

 

-      public override VCExpr Visit(VCExprVar node, VCExprSubstitution substitution) {

-        Contract.Requires(substitution != null);

-        Contract.Requires(node != null);

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

-        VCExpr res = substitution[node];

-        if (res != null)

-          return res;

-        return node;

+      } finally {

+        substitution.PopScope();

       }

+    }

 

-      public override VCExpr Visit(VCExprLet node, VCExprSubstitution substitution) {

-        Contract.Requires(substitution != null);

-        Contract.Requires(node != null);

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

-        // the default is to refresh bound variables only if necessary

-        // because of collisions

-        return Visit(node, substitution, false);

-      }

+    public override VCExpr Visit(VCExprVar node, VCExprSubstitution substitution) {

+      Contract.Requires(substitution != null);

+      Contract.Requires(node != null);

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

+      VCExpr res = substitution[node];

+      if (res != null)

+        return res;

+      return node;

+    }

+

+    public override VCExpr Visit(VCExprLet node, VCExprSubstitution substitution) {

+      Contract.Requires(substitution != null);

+      Contract.Requires(node != null);

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

+      // the default is to refresh bound variables only if necessary

+      // because of collisions

+      return Visit(node, substitution, false);

+    }

 

-      public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refreshBoundVariables){

-Contract.Requires(substitution != null);

-Contract.Requires(node != null);

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

+    public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refreshBoundVariables) {

+      Contract.Requires(substitution != null);

+      Contract.Requires(node != null);

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

       // let-expressions do not have type parameters (fortunately ...)

-      substitution.PushScope (); try {

+      substitution.PushScope();

+      try {

 

-      bool refreshAllVariables =

-        refreshBoundVariables ||

-        !substitution.TypeSubstIsEmpty ||

-        CollisionPossible(new List<TypeVariable/*!*/> (), node.BoundVars, substitution);

+        bool refreshAllVariables =

+          refreshBoundVariables ||

+          !substitution.TypeSubstIsEmpty ||

+          CollisionPossible(new List<TypeVariable/*!*/>(), node.BoundVars, substitution);

 

-      List<VCExprVar/*!*/>/*!*/ newBoundVars = node.BoundVars;

+        List<VCExprVar/*!*/>/*!*/ newBoundVars = node.BoundVars;

         Contract.Assert(cce.NonNullElements(newBoundVars));

-      if (refreshAllVariables) {

-        // collisions are possible, or we also substitute type variables. in this case

-        // the bound term variables have to be replaced with fresh variables with the

-        // right types

-        newBoundVars = new List<VCExprVar/*!*/> ();

-        IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;

-        Contract.Assert(cce.NonNullElements(typeSubst));

-        foreach (VCExprVar/*!*/ var in node.BoundVars) {

-          Contract.Assert(var != null);

-          VCExprVar/*!*/ freshVar =

-            Gen.Variable(ChooseNewVariableName(var.Name),

-                         var.Type.Substitute(typeSubst));

-          Contract.Assert(freshVar != null);

-          newBoundVars.Add(freshVar);

-          substitution[var] = freshVar;

-          // this might overwrite other elements of the substitution, deliberately

+        if (refreshAllVariables) {

+          // collisions are possible, or we also substitute type variables. in this case

+          // the bound term variables have to be replaced with fresh variables with the

+          // right types

+          newBoundVars = new List<VCExprVar/*!*/>();

+          IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;

+          Contract.Assert(cce.NonNullElements(typeSubst));

+          foreach (VCExprVar/*!*/ var in node.BoundVars) {

+            Contract.Assert(var != null);

+            VCExprVar/*!*/ freshVar =

+              Gen.Variable(ChooseNewVariableName(var.Name),

+                           var.Type.Substitute(typeSubst));

+            Contract.Assert(freshVar != null);

+            newBoundVars.Add(freshVar);

+            substitution[var] = freshVar;

+            // this might overwrite other elements of the substitution, deliberately

+          }

         }

-      }

 

-      List<VCExprLetBinding/*!*/>/*!*/ newbindings = new List<VCExprLetBinding/*!*/> ();

-      for (int i = 0; i < node.Length; ++i) {

-        VCExprLetBinding/*!*/ binding = node[i];

-        Contract.Assert(binding != null);

-        newbindings.Add(Gen.LetBinding(newBoundVars[i], Mutate(binding.E, substitution)));

-      }

+        List<VCExprLetBinding/*!*/>/*!*/ newbindings = new List<VCExprLetBinding/*!*/>();

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

+          VCExprLetBinding/*!*/ binding = node[i];

+          Contract.Assert(binding != null);

+          newbindings.Add(Gen.LetBinding(newBoundVars[i], Mutate(binding.E, substitution)));

+        }

 

-      VCExpr/*!*/ newBody = Mutate(node.Body, substitution);

-      Contract.Assert(newBody != null);

-      return Gen.Let(newbindings, newBody);

+        VCExpr/*!*/ newBody = Mutate(node.Body, substitution);

+        Contract.Assert(newBody != null);

+        return Gen.Let(newbindings, newBody);

 

       } finally {

         substitution.PopScope();

       }

     }

-    }

+  }

 

-    ////////////////////////////////////////////////////////////////////////////

-    [ContractClassFor(typeof(StandardVCExprOpVisitor<,>))]

-    public abstract class StandardVCExprOpVisitorContracts<Result, Arg> : StandardVCExprOpVisitor<Result, Arg> {

-      protected override Result StandardResult(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        throw new NotImplementedException();

-      }

+  ////////////////////////////////////////////////////////////////////////////

+  [ContractClassFor(typeof(StandardVCExprOpVisitor<,>))]

+  public abstract class StandardVCExprOpVisitorContracts<Result, Arg> : StandardVCExprOpVisitor<Result, Arg> {

+    protected override Result StandardResult(VCExprNAry node, Arg arg) {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

     }

+  }

 

 

-    [ContractClass(typeof(StandardVCExprOpVisitorContracts<,>))]

-    public abstract class StandardVCExprOpVisitor<Result, Arg>

-                          : IVCExprOpVisitor<Result, Arg> {

-      protected abstract Result StandardResult(VCExprNAry/*!*/ node, Arg arg);

+  [ContractClass(typeof(StandardVCExprOpVisitorContracts<,>))]

+  public abstract class StandardVCExprOpVisitor<Result, Arg>

+                        : IVCExprOpVisitor<Result, Arg> {

+    protected abstract Result StandardResult(VCExprNAry/*!*/ node, Arg arg);

 

-      public virtual Result VisitNotOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitEqOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitNeqOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitAndOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitOrOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitImpliesOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitDistinctOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitLabelOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitSelectOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitStoreOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitBvOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitBvExtractOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitBvConcatOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitIfThenElseOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

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

-        Contract.Requires(node != null);

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

+      //Contract.Requires(node != null);

       return StandardResult(node, arg);

     }

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

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitSubOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitMulOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitDivOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitModOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitLtOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitLeOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitGtOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitGeOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitSubtypeOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitSubtype3Op(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

-      public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {

-        Contract.Requires(node != null);

-        return StandardResult(node, arg);

-      }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

     }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

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

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

+  }

 

-  }
\ No newline at end of file
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index d5505dd4..d30c93e9 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -14,26 +14,23 @@ using Microsoft.Boogie.AbstractInterpretation;
 using Microsoft.Boogie.VCExprAST;

 using Microsoft.Basetypes;

 

-namespace Microsoft.Boogie

-{

+namespace Microsoft.Boogie {

   /// <summary>

   /// Interface to the theorem prover specialized to Boogie.

   ///

   /// This class creates the appropriate background axioms.  There

   /// should be one instance per BoogiePL program.

   /// </summary>

-  public sealed class Checker 

-  {

+  public sealed class Checker {

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(gen!=null);

+    void ObjectInvariant() {

+      Contract.Invariant(gen != null);

       Contract.Invariant(thmProver != null);

       Contract.Invariant(ProverDone != null);

-}

+    }

 

     private readonly VCExpressionGenerator gen;

-    

+

     private ProverInterface thmProver;

     private CommandLineOptions.BvHandling bitvectors;

     private int timeout;

@@ -50,34 +47,37 @@ void ObjectInvariant()
 

     public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);

 

-    private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl)

-    {

-      if (impl == null) return CommandLineOptions.Clo.Bitvectors;

+    private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) {

+      if (impl == null)

+        return CommandLineOptions.Clo.Bitvectors;

       bool force_int = false;

       bool force_native = false;

       cce.NonNull(impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int);

       impl.Proc.CheckBooleanAttribute("forceBvZ3Native", ref force_native);

       impl.CheckBooleanAttribute("forceBvInt", ref force_int);

       impl.CheckBooleanAttribute("forceBvZ3Native", ref force_native);

-      if (force_native) return CommandLineOptions.BvHandling.Z3Native;

-      if (force_int) return CommandLineOptions.BvHandling.ToInt;

+      if (force_native)

+        return CommandLineOptions.BvHandling.Z3Native;

+      if (force_int)

+        return CommandLineOptions.BvHandling.ToInt;

       return CommandLineOptions.Clo.Bitvectors;

     }

 

-    public bool WillingToHandle(Implementation impl, int timeout)

-    {

+    public bool WillingToHandle(Implementation impl, int timeout) {

       return !closed && timeout == this.timeout && bitvectors == BvHandlingForImpl(impl);

     }

 

-    public VCExpressionGenerator VCExprGen

-    {

-      get {Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);

- return this.gen; }

+    public VCExpressionGenerator VCExprGen {

+      get {

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

+        return this.gen;

+      }

     }

-    public ProverInterface TheoremProver

-    {

-      get {Contract.Ensures(Contract.Result<ProverInterface>() != null);

- return this.thmProver; }

+    public ProverInterface TheoremProver {

+      get {

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

+        return this.thmProver;

+      }

     }

 

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

@@ -85,10 +85,9 @@ void ObjectInvariant()
 

     private struct ContextCacheKey {

       [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(program!=null);

-}

+      void ObjectInvariant() {

+        Contract.Invariant(program != null);

+      }

 

       public readonly Program program;

       public readonly CommandLineOptions.BvHandling bitvectors;

@@ -100,7 +99,8 @@ void ObjectInvariant()
         this.bitvectors = bitvectors;

       }

 

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

+      [Pure]

+      [Reads(ReadsAttribute.Reads.Nothing)]

       public override bool Equals(object that) {

         if (that is ContextCacheKey) {

           ContextCacheKey thatKey = (ContextCacheKey)that;

@@ -121,8 +121,7 @@ void ObjectInvariant()
     /// <summary>

     /// Constructor.  Initialize a checker with the program and log file.

     /// </summary>

-    public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout)

-    {

+    public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout) {

       Contract.Requires(vcgen != null);

       Contract.Requires(prog != null);

       this.bitvectors = BvHandlingForImpl(impl);

@@ -143,14 +142,14 @@ void ObjectInvariant()
       }

       options.BitVectors = this.bitvectors;

 

-      ContextCacheKey key = new ContextCacheKey (prog, this.bitvectors);

+      ContextCacheKey key = new ContextCacheKey(prog, this.bitvectors);

       ProverContext ctx;

       ProverInterface prover;

 

       if (vcgen.CheckerCommonState == null) {

-        vcgen.CheckerCommonState = new Dictionary<ContextCacheKey, ProverContext> ();

+        vcgen.CheckerCommonState = new Dictionary<ContextCacheKey, ProverContext>();

       }

-      IDictionary<ContextCacheKey, ProverContext>/*!>!*/ cachedContexts = (IDictionary<ContextCacheKey, ProverContext/*!*/>) vcgen.CheckerCommonState;

+      IDictionary<ContextCacheKey, ProverContext>/*!>!*/ cachedContexts = (IDictionary<ContextCacheKey, ProverContext/*!*/>)vcgen.CheckerCommonState;

 

       if (cachedContexts.TryGetValue(key, out ctx)) {

         ctx = (ProverContext)cce.NonNull(ctx).Clone();

@@ -203,7 +202,7 @@ void ObjectInvariant()
           CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);

         cachedContexts.Add(key, cce.NonNull((ProverContext)ctx.Clone()));

       }

-      

+

       this.thmProver = prover;

       this.gen = prover.VCExprGen;

 

@@ -214,8 +213,7 @@ void ObjectInvariant()
     /// <summary>

     /// Clean-up.

     /// </summary>

-    public void Close()

-    {

+    public void Close() {

       this.closed = true;

       thmProver.Close();

     }

@@ -224,35 +222,37 @@ void ObjectInvariant()
     /// Push a Verification Condition as an Axiom 

     /// (Required for Doomed Program Point detection)

     /// </summary>

-    public void PushVCExpr(VCExpr vc)

-    {

+    public void PushVCExpr(VCExpr vc) {

       Contract.Requires(vc != null);

       //thmProver.Context.AddAxiom(vc);

       thmProver.PushVCExpression(vc);

     }

 

-    public bool IsBusy

-    {

-      get { return busy; }

+    public bool IsBusy {

+      get {

+        return busy;

+      }

     }

 

-    public bool Closed

-    {

-      get { return closed; }

+    public bool Closed {

+      get {

+        return closed;

+      }

     }

 

-    public bool HasOutput

-    {

-      get { return hasOutput; }

+    public bool HasOutput {

+      get {

+        return hasOutput;

+      }

     }

 

-    public TimeSpan ProverRunTime

-    {

-      get { return proverRunTime; }

+    public TimeSpan ProverRunTime {

+      get {

+        return proverRunTime;

+      }

     }

 

-    private void WaitForOutput(object dummy)

-    {

+    private void WaitForOutput(object dummy) {

       try {

         outcome = thmProver.CheckOutcome(cce.NonNull(handler));

       } catch (UnexpectedProverOutputException e) {

@@ -277,20 +277,20 @@ void ObjectInvariant()
           break;

       }

 

-      Contract.Assert( busy);

+      Contract.Assert(busy);

       hasOutput = true;

       proverRunTime = DateTime.Now - proverStart;

 

       ProverDone.Set();

     }

-    

-    public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler){

+

+    public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {

       Contract.Requires(descriptiveName != null);

       Contract.Requires(vc != null);

       Contract.Requires(handler != null);

-      

-      Contract.Requires( !IsBusy);

-      Contract.Assert( !busy);

+

+      Contract.Requires(!IsBusy);

+      Contract.Assert(!busy);

       busy = true;

       hasOutput = false;

       outputExn = null;

@@ -303,11 +303,11 @@ void ObjectInvariant()
       ThreadPool.QueueUserWorkItem(WaitForOutput);

     }

 

-    public ProverInterface.Outcome ReadOutcome(){

-      

-      Contract.Requires( IsBusy);

-      Contract.Requires( HasOutput);

-      Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);

+    public ProverInterface.Outcome ReadOutcome() {

+

+      Contract.Requires(IsBusy);

+      Contract.Requires(HasOutput);

+      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       hasOutput = false;

       busy = false;

 

@@ -318,7 +318,7 @@ void ObjectInvariant()
       return outcome;

     }

   }

-  

+

   // -----------------------------------------------------------------------------------------------

   // -----------------------------------------------------------------------------------------------

   // -----------------------------------------------------------------------------------------------

@@ -331,21 +331,20 @@ void ObjectInvariant()
     public Dictionary<string/*!*/, List<List<int>>/*!*/>/*!*/ definedFunctions;

 

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(cce.NonNullElements(identifierToPartition));

+    void ObjectInvariant() {

+      Contract.Invariant(cce.NonNullElements(identifierToPartition));

       Contract.Invariant(partitionToIdentifiers != null);

-      Contract.Invariant(Contract.ForAll(partitionToIdentifiers,i=>cce.NonNullElements(i)));

+      Contract.Invariant(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i)));

       Contract.Invariant(partitionToValue != null);

       Contract.Invariant(valueToPartition != null);

       Contract.Invariant(cce.NonNullElements(definedFunctions));

-}

+    }

 

 

     public ErrorModel(Dictionary<string, int> identifierToPartition, List<List<string>> partitionToIdentifiers, List<Object> partitionToValue, Dictionary<object, int> valueToPartition, Dictionary<string, List<List<int>>> definedFunctions) {

       Contract.Requires(cce.NonNullElements(identifierToPartition));

       Contract.Requires(partitionToIdentifiers != null);

-      Contract.Requires(Contract.ForAll(partitionToIdentifiers,i=>cce.NonNullElements(i)));

+      Contract.Requires(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i)));

       Contract.Requires(partitionToValue != null);

       Contract.Requires(valueToPartition != null);

       Contract.Requires(cce.NonNullElements(definedFunctions));

@@ -356,39 +355,41 @@ void ObjectInvariant()
       this.definedFunctions = definedFunctions;

     }

 

-    public virtual void Print(TextWriter writer) {Contract.Requires(writer != null); }

-    

-    public int LookupPartitionValue(int partition)

-    {

-      BigNum bignum = (BigNum) cce.NonNull(partitionToValue)[partition];

+    public virtual void Print(TextWriter writer) {

+      Contract.Requires(writer != null);

+    }

+

+    public int LookupPartitionValue(int partition) {

+      BigNum bignum = (BigNum)cce.NonNull(partitionToValue)[partition];

       return bignum.ToInt;

     }

-        

-    public int LookupControlFlowFunctionAt(int cfc, int id)

-    {

+

+    public int LookupControlFlowFunctionAt(int cfc, int id) {

       List<List<int>> tuples = this.definedFunctions["ControlFlow"];

       Contract.Assert(tuples != null);

-      foreach (List<int> tuple in tuples)

-      {

-        if (tuple == null) continue;

-        if (tuple.Count != 3) continue;

+      foreach (List<int> tuple in tuples) {

+        if (tuple == null)

+          continue;

+        if (tuple.Count != 3)

+          continue;

         if (LookupPartitionValue(tuple[0]) == cfc && LookupPartitionValue(tuple[1]) == id)

           return LookupPartitionValue(tuple[2]);

       }

-      Contract.Assert(false);throw new cce.UnreachableException();

+      Contract.Assert(false);

+      throw new cce.UnreachableException();

       return 0;

     }

-    

+

     private string LookupSkolemConstant(string name) {

       Contract.Requires(name != null);

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

 

-      foreach (string functionName in identifierToPartition.Keys)

-      {

+      foreach (string functionName in identifierToPartition.Keys) {

         Contract.Assert(functionName != null);

 

         int index = functionName.LastIndexOf("!");

-        if (index == -1) continue;

+        if (index == -1)

+          continue;

         string newFunctionName = cce.NonNull(functionName.Remove(index));

         if (newFunctionName.Equals(name))

           return functionName;

@@ -399,67 +400,62 @@ void ObjectInvariant()
       Contract.Requires(name != null);

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

 

-      foreach (string functionName in definedFunctions.Keys)

-      {

+      foreach (string functionName in definedFunctions.Keys) {

         Contract.Assert(functionName != null);

         int index = functionName.LastIndexOf("!");

-        if (index == -1) continue;

+        if (index == -1)

+          continue;

         string newFunctionName = cce.NonNull(functionName.Remove(index));

         if (newFunctionName.Equals(name))

           return functionName;

       }

       return "";

     }

-    public int LookupSkolemFunctionAt(string functionName, List<int> values)

-      

-    {

-      Contract.Requires(functionName!= null);

+    public int LookupSkolemFunctionAt(string functionName, List<int> values) {

+      Contract.Requires(functionName != null);

       Contract.Requires(values != null);

 

       string actualFunctionName = LookupSkolemFunction(functionName);

       Contract.Assert(actualFunctionName != null);

-      if (actualFunctionName.Equals(""))

-      {

+      if (actualFunctionName.Equals("")) {

         // The skolem function is actually a skolem constant

         actualFunctionName = LookupSkolemConstant(functionName);

-        Contract.Assert( !actualFunctionName.Equals(""));

+        Contract.Assert(!actualFunctionName.Equals(""));

         return identifierToPartition[actualFunctionName];

       }

       List<List<int>> tuples = this.definedFunctions[actualFunctionName];

-      Contract.Assert( tuples.Count > 0);

+      Contract.Assert(tuples.Count > 0);

       // the last tuple is a dummy tuple

-      for (int n = 0; n < tuples.Count - 1; n++)

-      {

+      for (int n = 0; n < tuples.Count - 1; n++) {

         List<int> tuple = cce.NonNull(tuples[n]);

-        Contract.Assert( tuple.Count - 1 <= values.Count);

-        for (int i = 0, j = 0; i < values.Count; i++)

-        {

+        Contract.Assert(tuple.Count - 1 <= values.Count);

+        for (int i = 0, j = 0; i < values.Count; i++) {

           if (values[i] == tuple[j]) {

             // succeeded in matching tuple[j]

             j++;

-            if (j == tuple.Count-1) return tuple[tuple.Count - 1];

+            if (j == tuple.Count - 1)

+              return tuple[tuple.Count - 1];

           }

         }

       }

-      Contract.Assert(false);throw new cce.UnreachableException();

+      Contract.Assert(false);

+      throw new cce.UnreachableException();

       return 0;

     }

-    

-    public List<object>/*!>!*/ PartitionsToValues(List<int> args)

-    {

+

+    public List<object>/*!>!*/ PartitionsToValues(List<int> args) {

       Contract.Requires(args != null);

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<object>>()));

 

       List<object> vals = new List<object>();

-      foreach(int i in args)

-      {

+      foreach (int i in args) {

         object o = cce.NonNull(partitionToValue[i]);

         if (o is bool) {

           vals.Add(o);

         } else if (o is BigNum) {

           vals.Add(o);

         } else if (o is List<List<int>>) {

-          List<List<int>> array = (List<List<int>>) o;

+          List<List<int>> array = (List<List<int>>)o;

           List<List<object>> arrayVal = new List<List<object>>();

           foreach (List<int> tuple in array) {

             Contract.Assert(tuple != null);

@@ -472,30 +468,33 @@ void ObjectInvariant()
           }

           vals.Add(arrayVal);

         } else {

-          Contract.Assert(false);throw new cce.UnreachableException();

+          Contract.Assert(false);

+          throw new cce.UnreachableException();

         }

       }

       return vals;

     }

   }

 

-  public abstract class ProverInterface

-  {

-    public enum Outcome { Valid, Invalid, TimeOut, OutOfMemory, Undetermined }

-    public class ErrorHandler

-    {

-      public virtual void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel)

-      {

+  public abstract class ProverInterface {

+    public enum Outcome {

+      Valid,

+      Invalid,

+      TimeOut,

+      OutOfMemory,

+      Undetermined

+    }

+    public class ErrorHandler {

+      public virtual void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel) {

         Contract.Requires(cce.NonNullElements(labels));

       }

 

-      public virtual void OnResourceExceeded(string message)

-      {

-        Contract.Requires(message!=null);

+      public virtual void OnResourceExceeded(string message) {

+        Contract.Requires(message != null);

       }

 

       public virtual void OnProverWarning(string message)

-          //modifies Console.Out.*, Console.Error.*;

+        //modifies Console.Out.*, Console.Error.*;

       {

         Contract.Requires(message != null);

         switch (CommandLineOptions.Clo.PrintProverWarnings) {

@@ -508,13 +507,13 @@ void ObjectInvariant()
             Console.Error.WriteLine("Prover warning: " + message);

             break;

           default:

-             Contract.Assume( false);throw new cce.UnreachableException();  // unexpected case

+            Contract.Assume(false);

+            throw new cce.UnreachableException();  // unexpected case

         }

       }

 

 

-      public virtual Absy Label2Absy(string label)

-      {

+      public virtual Absy Label2Absy(string label) {

         Contract.Requires(label != null);

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

 

@@ -529,26 +528,40 @@ void ObjectInvariant()
     }

     public virtual void Close() {

     }

-    

+

     /// <summary>

     /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)

     /// for now it is only implemented by ProcessTheoremProver and still requires some

     /// testing

     /// </summary>    

-    public virtual void PushVCExpression(VCExpr vc) {Contract.Requires(vc != null);}

-    public virtual string VCExpressionToString(VCExpr vc) {Contract.Requires(vc != null);Contract.Ensures(Contract.Result<string>() != null); return ""; }

-    public virtual void Pop()

-    {Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);}

-    public virtual int NumAxiomsPushed() 

-    { return 0; }

-    public virtual int FlushAxiomsToTheoremProver() 

-    { Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);return 0; }

-    

-        

-    public abstract ProverContext Context { get; }

-public abstract VCExpressionGenerator VCExprGen { get; }

+    public virtual void PushVCExpression(VCExpr vc) {

+      Contract.Requires(vc != null);

+    }

+    public virtual string VCExpressionToString(VCExpr vc) {

+      Contract.Requires(vc != null);

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

+      return "";

+    }

+    public virtual void Pop() {

+      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+    }

+    public virtual int NumAxiomsPushed() {

+      return 0;

+    }

+    public virtual int FlushAxiomsToTheoremProver() {

+      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+      return 0;

+    }

+

+

+    public abstract ProverContext Context {

+      get;

+    }

+    public abstract VCExpressionGenerator VCExprGen {

+      get;

+    }

   }

-  public class ProverInterfaceContracts:ProverInterface{

+  public class ProverInterfaceContracts : ProverInterface {

     public override ProverContext Context {

       get {

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

@@ -563,32 +576,34 @@ public abstract VCExpressionGenerator VCExprGen { get; }
         throw new NotImplementedException();

       }

     }

-    public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler){/*Contract.Requires(descriptiveName != null);*/ Contract.Requires(vc != null);Contract.Requires(handler != null);throw new NotImplementedException();}

+    public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {/*Contract.Requires(descriptiveName != null);*/

+      //Contract.Requires(vc != null);

+      //Contract.Requires(handler != null);

+      throw new NotImplementedException();

+    }

     [NoDefaultContract]

-    public override Outcome CheckOutcome(ErrorHandler handler){

-    //Contract.Requires(handler != null);

-      Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);

-    throw new NotImplementedException();}

+    public override Outcome CheckOutcome(ErrorHandler handler) {

+      //Contract.Requires(handler != null);

+      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+      throw new NotImplementedException();

+    }

   }

 

-    

 

-  public class ProverException : Exception 

-  {

-    public ProverException(string s) : base(s)

-    {            

+

+  public class ProverException : Exception {

+    public ProverException(string s)

+      : base(s) {

     }

   }

-  public class UnexpectedProverOutputException : ProverException, Microsoft.Contracts.ICheckedException

-  {

-    public UnexpectedProverOutputException(string s) : base(s)

-    {

+  public class UnexpectedProverOutputException : ProverException, Microsoft.Contracts.ICheckedException {

+    public UnexpectedProverOutputException(string s)

+      : base(s) {

     }

   }

-  public class ProverDiedException : UnexpectedProverOutputException

-  {

-    public ProverDiedException() : base("Prover died with no further output, perhaps it ran out of memory or was killed.")

-    {

+  public class ProverDiedException : UnexpectedProverOutputException {

+    public ProverDiedException()

+      : base("Prover died with no further output, perhaps it ran out of memory or was killed.") {

     }

   }

 }

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 209248ed..90ed5d5c 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -722,12 +722,12 @@ namespace VC {
 

       public readonly List<Counterexample>/*!>!*/ examples = new List<Counterexample>();

       public override void OnCounterexample(Counterexample ce, string/*?*/ reason) {

-        Contract.Requires(ce != null);

+        //Contract.Requires(ce != null);

         examples.Add(ce);

       }

 

       public override void OnUnreachableCode(Implementation impl) {

-        Contract.Requires(impl != null);

+        //Contract.Requires(impl != null);

         System.Console.WriteLine("found unreachable code:");

         EmitImpl(impl, false);

         // TODO report error about next to last in seq

diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/VCGeneration/DoomErrorHandler.cs
index 0bcf15f8..12936c1f 100644
--- a/Source/VCGeneration/DoomErrorHandler.cs
+++ b/Source/VCGeneration/DoomErrorHandler.cs
@@ -41,7 +41,7 @@ void ObjectInvariant()
         }

         

         public override Absy Label2Absy(string label) {

-          Contract.Requires(label != null);

+          //Contract.Requires(label != null);

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

 

           int id = int.Parse(label);

@@ -49,7 +49,7 @@ void ObjectInvariant()
         }

         

         public override void OnProverWarning(string msg) {

-          Contract.Requires(msg != null);

+          //Contract.Requires(msg != null);

           this.callback.OnWarning(msg);

         }

    

@@ -75,7 +75,7 @@ void ObjectInvariant()
         }

         

         public override void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel) {

-          Contract.Requires(labels != null);

+          //Contract.Requires(labels != null);

           

         m_CurrentTrace.Clear();

         //Console.Write("Used Blocks: ");

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 9ca934b2..a053a153 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -780,7 +780,7 @@ namespace VC {
         }

 

         public override Absy Label2Absy(string label) {

-          Contract.Requires(label != null);

+          //Contract.Requires(label != null);

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

 

           int id = int.Parse(label);

@@ -788,7 +788,7 @@ namespace VC {
         }

 

         public override void OnProverWarning(string msg) {

-          Contract.Requires(msg != null);

+          //Contract.Requires(msg != null);

           this.callback.OnWarning(msg);

         }

       }

@@ -1721,9 +1721,9 @@ namespace VC {
     }

 

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

-      Contract.Requires(impl != null);

-      Contract.Requires(program != null);

-      Contract.Requires(callback != null);

+      //Contract.Requires(impl != null);

+      //Contract.Requires(program != null);

+      //Contract.Requires(callback != null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       if (impl.SkipVerification) {

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

@@ -1888,9 +1888,9 @@ namespace VC {
     }

 

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

-      Contract.Requires(impl != null);

-      Contract.Requires(program != null);

-      Contract.Requires(callback != null);

+      //Contract.Requires(impl != null);

+      //Contract.Requires(program != null);

+      //Contract.Requires(callback != null);

       Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);

        // This flag control the nature of queries made by StratifiedVerifyImplementation

        // true: incremental search; false: in-place inlining

@@ -2738,8 +2738,8 @@ namespace VC {
                                                     bool changed,

                                                     bool arg) 

       {

-        Contract.Requires(originalNode != null);

-        Contract.Requires(cce.NonNullElements(newSubExprs));

+        //Contract.Requires(originalNode != null);

+        //Contract.Requires(cce.NonNullElements(newSubExprs));

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

 

         VCExpr ret;

@@ -2821,7 +2821,7 @@ namespace VC {
                                                     bool changed,

                                                     bool arg) 

       {

-        Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null);

+        //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null);

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

 

         VCExpr ret;

@@ -2911,7 +2911,7 @@ namespace VC {
       }

 

       public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel) {

-        Contract.Requires(cce.NonNullElements(labels));

+        //Contract.Requires(cce.NonNullElements(labels));

         if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {

           errModel.Print(ErrorReporter.ModelWriter);

           ErrorReporter.ModelWriter.Flush();

@@ -2955,7 +2955,7 @@ namespace VC {
       }

 

       public override Absy Label2Absy(string label) {

-        Contract.Requires(label != null);

+        //Contract.Requires(label != null);

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

 

         int id = int.Parse(label);

@@ -2963,12 +2963,12 @@ namespace VC {
       }

 

       public override void OnResourceExceeded(string msg) {

-        Contract.Requires(msg != null);

+        //Contract.Requires(msg != null);

         resourceExceededMessage = msg;

       }

 

       public override void OnProverWarning(string msg) {

-        Contract.Requires(msg != null);

+        //Contract.Requires(msg != null);

         callback.OnWarning(msg);

       }

     }

@@ -2996,7 +2996,7 @@ namespace VC {
       }

 

       public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel) {

-        Contract.Requires(cce.NonNullElements(labels));

+        //Contract.Requires(cce.NonNullElements(labels));

         // We ignore the error model here for enhanced error message purposes.

         // It is only printed to the command line.

         if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {

@@ -3092,7 +3092,7 @@ namespace VC {
       }

 

       public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel) {

-        Contract.Requires(cce.NonNullElements(labels));

+        //Contract.Requires(cce.NonNullElements(labels));

         if (underapproximationMode) {

           if (errModel == null)

             return;

@@ -3266,7 +3266,7 @@ namespace VC {
       }

 

       public override Absy Label2Absy(string label) {

-        Contract.Requires(label != null);

+        //Contract.Requires(label != null);

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

 

         int id = int.Parse(label);

@@ -3285,12 +3285,12 @@ namespace VC {
       }

 

       public override void OnResourceExceeded(string msg) {

-        Contract.Requires(msg != null);

+        //Contract.Requires(msg != null);

         //resourceExceededMessage = msg;

       }

 

       public override void OnProverWarning(string msg) {

-        Contract.Requires(msg != null);

+        //Contract.Requires(msg != null);

         callback.OnWarning(msg);

       }

     }

diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
index 12543cd5..c1547009 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/VCGeneration/VCDoomed.cs
@@ -283,9 +283,9 @@ namespace VC {
     ///

     /// </summary>

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

-      Contract.Requires(impl != null);

-      Contract.Requires(program != null);

-      Contract.Requires(callback != null);

+      //Contract.Requires(impl != null);

+      //Contract.Requires(program != null);

+      //Contract.Requires(callback != null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

 

       UseItAsDebugger = CommandLineOptions.Clo.useDoomDebug;