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

1 files changed, 654 insertions, 628 deletions

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