ExprSeq: farewell

20 files changed, 152 insertions, 197 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 23935658..29f826f7 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -398,9 +398,9 @@ namespace Microsoft.Boogie {
         Contract.Assert(header != null);

         List<Variable> inputs = new List<Variable>();

         List<Variable> outputs = new List<Variable>();

-        ExprSeq callInputs1 = new ExprSeq();

+        List<Expr> callInputs1 = new List<Expr>();

         List<IdentifierExpr> callOutputs1 = new List<IdentifierExpr>();

-        ExprSeq callInputs2 = new ExprSeq();

+        List<Expr> callInputs2 = new List<Expr>();

         List<IdentifierExpr> callOutputs2 = new List<IdentifierExpr>();

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

         List<Expr> rhss = new List<Expr>();

@@ -2134,7 +2134,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(definition != null);

 

       List<Variable> dummies = new List<Variable>();

-      ExprSeq callArgs = new ExprSeq();

+      List<Expr> callArgs = new List<Expr>();

       int i = 0;

       foreach (Formal/*!*/ f in InParams) {

         Contract.Assert(f != null);

@@ -2157,7 +2157,7 @@ namespace Microsoft.Boogie {
       if (quantifiedTypeVars.Count != 0 || dummies.Count != 0) {

         def = new ForallExpr(tok, quantifiedTypeVars, dummies,

                              kv,

-                             new Trigger(tok, true, new ExprSeq(call), null),

+                             new Trigger(tok, true, new List<Expr> { call }, null),

                              def);

       }

       DefinitionAxiom = new Axiom(tok, def);

@@ -3234,36 +3234,6 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class ExprSeq : List<Expr> {

-    public ExprSeq(params Expr[]/*!*/ args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public ExprSeq(ExprSeq/*!*/ exprSeq)

-      : base(exprSeq) {

-      Contract.Requires(exprSeq != null);

-    }

-

-    public static ExprSeq operator +(ExprSeq a, ExprSeq b) {

-      if (a == null)

-        throw new ArgumentNullException("a");

-      if (b == null)

-        throw new ArgumentNullException("b");

-      return Append(a, b);

-    }

-

-    public static ExprSeq Append(ExprSeq s, ExprSeq t) {

-      Contract.Requires(t != null);

-      Contract.Requires(s != null);

-      Expr[] n = new Expr[s.Count + t.Count];

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

-        n[i] = s[i];

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

-        n[s.Count + i] = t[i];

-      return new ExprSeq(n);

-    }

-  }

-

   public static class Emitter {

     public static void Declarations(List<Declaration/*!*/>/*!*/ decls, TokenTextWriter stream) {

       Contract.Requires(stream != null);

@@ -3292,7 +3262,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public static void Emit(this ExprSeq ts, TokenTextWriter stream) {

+    public static void Emit(this List<Expr> ts, TokenTextWriter stream) {

       Contract.Requires(stream != null);

       string sep = "";

       foreach (Expr/*!*/ e in ts) {

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index d1f3a845..57f48f02 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -981,7 +981,7 @@ namespace Microsoft.Boogie {
 

     public static AssignCmd/*!*/ MapAssign(IToken tok,

                                        IdentifierExpr/*!*/ map,

-                                       ExprSeq/*!*/ indexes, Expr/*!*/ rhs) {

+                                       List<Expr>/*!*/ indexes, Expr/*!*/ rhs) {

 

       Contract.Requires(tok != null);

       Contract.Requires(map != null);

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

 

       // we use the same typechecking code as in MapSelect

-      ExprSeq/*!*/ selectArgs = new ExprSeq();

+      List<Expr>/*!*/ selectArgs = new List<Expr>();

       foreach (Expr/*!*/ e in Indexes) {

         Contract.Assert(e != null);

         selectArgs.Add(e);

@@ -1756,21 +1756,6 @@ namespace Microsoft.Boogie {
         errorData = value;

       }

     }

-    public CallCmd(IToken tok, string callee, ExprSeq ins, List<IdentifierExpr> outs)

-      : this(tok, callee, ins.ToList(), outs.ToList()) {

-      Contract.Requires(outs != null);

-      Contract.Requires(ins != null);

-      Contract.Requires(callee != null);

-      Contract.Requires(tok != null);

-      //List<Expr>/*!*/ insList = new List<Expr>();

-      //List<IdentifierExpr>/*!*/ outsList = new List<IdentifierExpr>();

-      //foreach (Expr e in ins)

-      //  if(e!=null)

-      //  insList.Add(e);

-      //foreach (IdentifierExpr e in outs)

-      //  if(e!=null)

-      //  outsList.Add(e);

-    }

     public CallCmd(IToken tok, string callee, List<Expr> ins, List<IdentifierExpr> outs)

       : base(tok, null) {

       Contract.Requires(outs != null);

@@ -1987,7 +1972,7 @@ namespace Microsoft.Boogie {
 

       List<Type>/*!*/ formalInTypes = new List<Type>();

       List<Type>/*!*/ formalOutTypes = new List<Type>();

-      ExprSeq/*!*/ actualIns = new ExprSeq();

+      List<Expr>/*!*/ actualIns = new List<Expr>();

       List<IdentifierExpr>/*!*/ actualOuts = new List<IdentifierExpr>();

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

         if (Ins[i] != null) {

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index b3b2289b..dcc6d6e2 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -90,7 +90,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(e1 != null);

       Contract.Requires(x != null);

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

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

+      return new NAryExpr(x, new UnaryOperator(x, op), new List<Expr> { e1 });

     }

 

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

@@ -98,7 +98,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(e0 != null);

       Contract.Requires(x != null);

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

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

+      return new NAryExpr(x, new BinaryOperator(x, op), new List<Expr> { e0, e1 });

     }

 

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

@@ -339,7 +339,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(map != null);

       Contract.Requires(x != null);

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

-      ExprSeq/*!*/ allArgs = new ExprSeq();

+      List<Expr>/*!*/ allArgs = new List<Expr>();

       allArgs.Add(map);

       foreach (Expr/*!*/ a in args) {

         Contract.Assert(a != null);

@@ -376,7 +376,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(args.Length > 0);    // zero or more indices, plus the value

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

 

-      ExprSeq/*!*/ allArgs = new ExprSeq();

+      List<Expr>/*!*/ allArgs = new List<Expr>();

       allArgs.Add(map);

       foreach (Expr/*!*/ a in args) {

         Contract.Assert(a != null);

@@ -390,7 +390,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(subexpr != null);

       Contract.Requires(x != null);

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

-      ExprSeq/*!*/ args = new ExprSeq();

+      List<Expr>/*!*/ args = new List<Expr>();

       args.Add(subexpr);

       return new NAryExpr(x, new TypeCoercion(x, type), args);

     }

@@ -945,7 +945,7 @@ namespace Microsoft.Boogie {
     /// <param name="stream"></param>

     /// <param name="contextBindingStrength"></param>

     /// <param name="fragileContext"></param>

-    void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext);

+    void Emit(List<Expr>/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext);

 

     void Resolve(ResolutionContext/*!*/ rc, Expr/*!*/ subjectForErrorReporting);

 

@@ -968,14 +968,14 @@ namespace Microsoft.Boogie {
     /// </summary>

     /// <param name="args"></param>

     /// <param name="tc"></param>

-    Type Typecheck(ref ExprSeq/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc);

+    Type Typecheck(ref List<Expr>/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc);

 

     // Contract.Requires( Microsoft.SpecSharp.Collections.Reductions.Forall{Expr! arg in args; arg.Type != null});

 

     /// <summary>

     /// Returns the result type of the IAppliable, supposing the argument are of the correct types.

     /// </summary>

-    Type/*!*/ ShallowType(ExprSeq/*!*/ args);

+    Type/*!*/ ShallowType(List<Expr>/*!*/ args);

 

     T Dispatch<T>(IAppliableVisitor<T>/*!*/ visitor);

   }

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

     }

 

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

+    public void Emit(List<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

       Contract.Requires(args != null);

       Contract.Requires(stream != null);

       throw new NotImplementedException();

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

     }

 

-    public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

       Contract.Requires(args != null);

       Contract.Requires(tc != null);

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

@@ -1018,7 +1018,7 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();

     }

 

-    public Type ShallowType(ExprSeq args) {

+    public Type ShallowType(List<Expr> args) {

       Contract.Requires(args != null);

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

 

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

     }

 

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

+    public void Emit(List<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

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

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

       stream.SetToken(ref this.tok);

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

     }

 

-    public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

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

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

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

@@ -1173,7 +1173,7 @@ namespace Microsoft.Boogie {
         this.FunctionName, arg0type);

       return null;

     }

-    public Type ShallowType(ExprSeq args) {

+    public Type ShallowType(List<Expr> args) {

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

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

       switch (this.op) {

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

     }

 

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

+    public void Emit(List<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

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

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

       stream.SetToken(ref this.tok);

@@ -1444,7 +1444,7 @@ namespace Microsoft.Boogie {
         return 2;

       }

     }

-    public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

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

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

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

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

     }

 

-    public Type ShallowType(ExprSeq args) {

+    public Type ShallowType(List<Expr> args) {

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

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

       switch (this.op) {

@@ -1588,7 +1588,7 @@ namespace Microsoft.Boogie {
         case Opcode.Neq:

           if (arg0.Type != null && arg0.Type.IsBool && arg1.Type != null && arg1.Type.IsBool) {

             expr.Fun = new BinaryOperator(tok, Opcode.Iff);

-            arg1 = new NAryExpr(expr.tok, new UnaryOperator(tok, UnaryOperator.Opcode.Not), new ExprSeq(arg1));

+            arg1 = new NAryExpr(expr.tok, new UnaryOperator(tok, UnaryOperator.Opcode.Not), new List<Expr> { arg1 });

 

             // ugly ... there should be some more general approach,

             // e.g., to typecheck the whole expression again

@@ -1765,7 +1765,7 @@ namespace Microsoft.Boogie {
       return Func.GetHashCode();

     }

 

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

+    virtual public void Emit(List<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

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

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

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

@@ -1791,7 +1791,7 @@ namespace Microsoft.Boogie {
         return Func.InParams.Count;

       }

     }

-    public virtual Type Typecheck(ref ExprSeq actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public virtual Type Typecheck(ref List<Expr> actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

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

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

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

@@ -1824,7 +1824,7 @@ namespace Microsoft.Boogie {
         return actualResultType[0];

       }

     }

-    public Type ShallowType(ExprSeq args) {

+    public Type ShallowType(List<Expr> args) {

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

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

       Contract.Assume(name.Type != null);

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

     }

 

-    public void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream,

+    public void Emit(List<Expr>/*!*/ args, TokenTextWriter/*!*/ stream,

                      int contextBindingStrength, bool fragileContext) {

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

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

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

     }

 

-    public Type Typecheck(ref ExprSeq/*!*/ args,

+    public Type Typecheck(ref List<Expr>/*!*/ args,

                           out TypeParamInstantiation/*!*/ tpInstantiation,

                           TypecheckingContext/*!*/ tc) {

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

@@ -1912,7 +1912,7 @@ namespace Microsoft.Boogie {
       return this.Type;

     }

 

-    public Type ShallowType(ExprSeq args) {

+    public Type ShallowType(List<Expr> args) {

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

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

       return this.Type;

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

     }

 

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

+    virtual public void Emit(List<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

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

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

       stream.Write(this.name);

@@ -2005,7 +2005,7 @@ namespace Microsoft.Boogie {
       //Contract.Requires(rc != null);

     }

 

-    public virtual Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public virtual Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

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

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

       Contract.Ensures(args != null);

@@ -2022,7 +2022,7 @@ namespace Microsoft.Boogie {
       return this.type;

     }

 

-    public Type ShallowType(ExprSeq args) {

+    public Type ShallowType(List<Expr> args) {

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

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

       return this.type;

@@ -2038,7 +2038,7 @@ namespace Microsoft.Boogie {
     [Additive]

     [Peer]

     public IAppliable/*!*/ Fun;

-    public ExprSeq/*!*/ Args;

+    public List<Expr>/*!*/ Args;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Fun != null);

@@ -2051,7 +2051,7 @@ namespace Microsoft.Boogie {
     public TypeParamInstantiation TypeParameters = null;

 

     [Captured]

-    public NAryExpr(IToken/*!*/ tok, IAppliable/*!*/ fun, ExprSeq/*!*/ args)

+    public NAryExpr(IToken/*!*/ tok, IAppliable/*!*/ fun, List<Expr>/*!*/ args)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(fun != null);

@@ -2188,7 +2188,7 @@ namespace Microsoft.Boogie {
       return Arity.GetHashCode() * 2823;

     }

 

-    public void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream,

+    public void Emit(List<Expr>/*!*/ args, TokenTextWriter/*!*/ stream,

                      int contextBindingStrength, bool fragileContext) {

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

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

@@ -2196,7 +2196,7 @@ namespace Microsoft.Boogie {
       Emit(args, stream, contextBindingStrength, fragileContext, false);

     }

 

-    public static void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream,

+    public static void Emit(List<Expr>/*!*/ args, TokenTextWriter/*!*/ stream,

                             int contextBindingStrength, bool fragileContext,

                             bool withRhs) {

       Contract.Requires(args != null);

@@ -2248,7 +2248,7 @@ namespace Microsoft.Boogie {
       // the AssignCmd maps can also be

       // represented by non-expressions

                                  Absy/*!*/ map,

-                                 ExprSeq/*!*/ indexes,

+                                 List<Expr>/*!*/ indexes,

       // the type parameters, in this context, are the parameters of the

       // potentially polymorphic map type. Because it might happen that

       // the whole map type is unknown and represented using a MapTypeProxy,

@@ -2290,13 +2290,13 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

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

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

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

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

 

-      ExprSeq actualArgs = new ExprSeq();

+      List<Expr> actualArgs = new List<Expr>();

       for (int i = 1; i < args.Count; ++i)

         actualArgs.Add(args[i]);

 

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

     /// Returns the result type of the IAppliable, supposing the argument are of the correct types.

     /// </summary>

-    public Type ShallowType(ExprSeq args) {

+    public Type ShallowType(List<Expr> args) {

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

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

       Expr a0 = cce.NonNull(args[0]);

@@ -2369,7 +2369,7 @@ namespace Microsoft.Boogie {
       return Arity.GetHashCode() * 28231;

     }

 

-    public void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream,

+    public void Emit(List<Expr>/*!*/ args, TokenTextWriter/*!*/ stream,

                      int contextBindingStrength, bool fragileContext) {

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

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

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

 

     // it is assumed that each of the arguments has already been typechecked

-    public static Type Typecheck(ExprSeq/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation,

+    public static Type Typecheck(List<Expr>/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation,

                                  TypecheckingContext/*!*/ tc,

                                  IToken/*!*/ typeCheckingSubject,

                                  string/*!*/ opName) {

@@ -2401,7 +2401,7 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);

 

       // part of the type checking works exactly as for MapSelect

-      ExprSeq selectArgs = new ExprSeq();

+      List<Expr> selectArgs = new List<Expr>();

       for (int i = 1; i < args.Count - 1; ++i)

         selectArgs.Add(args[i]);

       Type resultType =

@@ -2424,7 +2424,7 @@ namespace Microsoft.Boogie {
       return cce.NonNull(args[0]).Type;

     }

 

-    public Type Typecheck(ref ExprSeq/*!*/ args,

+    public Type Typecheck(ref List<Expr>/*!*/ args,

                           out TypeParamInstantiation/*!*/ tpInstantiation,

                           TypecheckingContext/*!*/ tc) {

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

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

     /// Returns the result type of the IAppliable, supposing the argument are of the correct types.

     /// </summary>

-    public Type ShallowType(ExprSeq args) {

+    public Type ShallowType(List<Expr> args) {

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

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

       return cce.NonNull(args[0]).ShallowType;

@@ -2486,7 +2486,7 @@ namespace Microsoft.Boogie {
       return 1;

     }

 

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

+    public void Emit(List<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

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

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

       stream.SetToken(ref this.tok);

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

     }

 

-    public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

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

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

       Contract.Ensures(args != null);

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

     /// Returns the result type of the IAppliable, supposing the argument are of the correct types.

     /// </summary>

-    public Type ShallowType(ExprSeq args) {

+    public Type ShallowType(List<Expr> args) {

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

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

       return cce.NonNull(args[1]).ShallowType;

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 5fdc3e68..fe0748a9 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -326,7 +326,7 @@ namespace Microsoft.Boogie {
   public class Trigger : Absy {

     public readonly bool Pos;

     [Rep]

-    public ExprSeq/*!*/ Tr;

+    public List<Expr>/*!*/ Tr;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Tr != null);

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

     public Trigger Next;

 

-    public Trigger(IToken tok, bool pos, ExprSeq tr)

+    public Trigger(IToken tok, bool pos, List<Expr> tr)

       : this(tok, pos, tr, null) {

       Contract.Requires(tr != null);

       Contract.Requires(tok != null);

@@ -344,7 +344,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(pos || tr.Count == 1);

     }

 

-    public Trigger(IToken/*!*/ tok, bool pos, ExprSeq/*!*/ tr, Trigger next)

+    public Trigger(IToken/*!*/ tok, bool pos, List<Expr>/*!*/ tr, Trigger next)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(tr != null);

@@ -584,7 +584,7 @@ namespace Microsoft.Boogie {
         Contract.Ensures(Contract.Result<Expr>() != null);

         FunctionCall fn = node.Fun as FunctionCall;

         if (fn != null && cce.NonNull(fn.Func).NeverTrigger) {

-          parent.Triggers = new Trigger(fn.Func.tok, false, new ExprSeq(node), parent.Triggers);

+          parent.Triggers = new Trigger(fn.Func.tok, false, new List<Expr> { node} , parent.Triggers);

         }

         return base.VisitNAryExpr(node);

       }

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index e5fad05d..64c4b699 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -366,7 +366,7 @@ namespace Microsoft.Boogie {
     public static IDictionary<TypeVariable!, Type!>!

                   MatchArgumentTypes(TypeVariableSeq! typeParams,

                                      List<Type>! formalArgs,

-                                     ExprSeq! actualArgs,

+                                     List<Expr>! actualArgs,

                                      List<Type> formalOuts,

                                      List<IdentifierExpr> actualOuts,

                                      string! opName,

@@ -438,7 +438,7 @@ namespace Microsoft.Boogie {
     public static IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/

                   MatchArgumentTypes(TypeVariableSeq/*!*/ typeParams,

                                      List<Type>/*!*/ formalArgs,

-                                     ExprSeq/*!*/ actualArgs,

+                                     List<Expr>/*!*/ actualArgs,

                                      List<Type> formalOuts,

                                      List<IdentifierExpr> actualOuts,

                                      string/*!*/ opName,

@@ -508,7 +508,7 @@ namespace Microsoft.Boogie {
     public static List<Type> CheckArgumentTypes(TypeVariableSeq/*!*/ typeParams,

                                              out List<Type/*!*/>/*!*/ actualTypeParams,

                                              List<Type>/*!*/ formalIns,

-                                             ExprSeq/*!*/ actualIns,

+                                             List<Expr>/*!*/ actualIns,

                                              List<Type>/*!*/ formalOuts,

                                              List<IdentifierExpr> actualOuts,

                                              IToken/*!*/ typeCheckingSubject,

@@ -631,7 +631,7 @@ namespace Microsoft.Boogie {
 #else

     /// <summary>

     /// like Type.CheckArgumentTypes, but assumes no errors

-    /// (and only does arguments, not results; and takes actuals as List<Type>, not ExprSeq)

+    /// (and only does arguments, not results; and takes actuals as List<Type>, not List<Expr>)

     /// </summary>

     public static IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/

                   InferTypeParameters(TypeVariableSeq/*!*/ typeParams,

@@ -2354,7 +2354,7 @@ Contract.Requires(that != null);
       constraints.Add(c);

     }

 

-    public Type CheckArgumentTypes(ExprSeq/*!*/ actualArgs,

+    public Type CheckArgumentTypes(List<Expr>/*!*/ actualArgs,

                                    out TypeParamInstantiation/*!*/ tpInstantiation,

                                    IToken/*!*/ typeCheckingSubject,

                                    string/*!*/ opName,

@@ -3480,7 +3480,7 @@ Contract.Assert(var != null);
     //------------  result type. Null is returned if so many type checking

     //------------  errors occur that the situation is hopeless

 

-    public Type CheckArgumentTypes(ExprSeq/*!*/ actualArgs,

+    public Type CheckArgumentTypes(List<Expr>/*!*/ actualArgs,

                                    out TypeParamInstantiation/*!*/ tpInstantiation,

                                    IToken/*!*/ typeCheckingSubject,

                                    string/*!*/ opName,

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index dec0b3a8..294abba3 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -24,7 +24,7 @@ readonly Expr/*!*/ dummyExpr;
 readonly Cmd/*!*/ dummyCmd;

 readonly Block/*!*/ dummyBlock;

 readonly Bpl.Type/*!*/ dummyType;

-readonly Bpl.ExprSeq/*!*/ dummyExprSeq;

+readonly Bpl.List<Expr>/*!*/ dummyExprSeq;

 readonly TransferCmd/*!*/ dummyTransferCmd;

 readonly StructuredCmd/*!*/ dummyStructuredCmd;

 

@@ -86,7 +86,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)
   dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);

   dummyBlock = new Block(Token.NoToken, "dummyBlock", new List<Cmd>(), new ReturnCmd(Token.NoToken));

   dummyType = new BasicType(Token.NoToken, SimpleType.Bool);

-  dummyExprSeq = new ExprSeq ();

+  dummyExprSeq = new List<Expr> ();

   dummyTransferCmd = new ReturnCmd(Token.NoToken);

   dummyStructuredCmd = new BreakCmd(Token.NoToken, null);

 }

@@ -993,8 +993,8 @@ WhiteSpaceIdents<out List<IToken>/*!*/ xs>
   .

 

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

-Expressions<out ExprSeq/*!*/ es>

-= (. Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new ExprSeq(); .)

+Expressions<out List<Expr>/*!*/ es>

+= (. Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List<Expr>(); .)

   Expression<out e>             (. es.Add(e); .)

   { "," Expression<out e>       (. es.Add(e); .)

   }

@@ -1194,10 +1194,10 @@ ArrayExpression<out Expr/*!*/ e>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;

      Expr/*!*/ index0 = dummyExpr; Expr/*!*/ e1;

      bool store; bool bvExtract;

-     ExprSeq/*!*/ allArgs = dummyExprSeq;

+     List<Expr>/*!*/ allArgs = dummyExprSeq;

   .)

   AtomExpression<out e>

-  { "["        (. x = t; allArgs = new ExprSeq ();

+  { "["        (. x = t; allArgs = new List<Expr> ();

                   allArgs.Add(e);

                   store = false; bvExtract = false; .)

       [

@@ -1238,7 +1238,7 @@ ArrayExpression<out Expr/*!*/ e>
 /*------------------------------------------------------------------------*/

 AtomExpression<out Expr/*!*/ e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;

-     ExprSeq/*!*/ es;  List<Variable>/*!*/ ds;  Trigger trig;

+     List<Expr>/*!*/ es;  List<Variable>/*!*/ ds;  Trigger trig;

      TypeVariableSeq/*!*/ typeParams;

      IdentifierExpr/*!*/ id;

      QKeyValue kv;

@@ -1255,7 +1255,7 @@ AtomExpression<out Expr/*!*/ e>
   | Ident<out x>            (. id = new IdentifierExpr(x, x.val);  e = id; .)

     [ "("

       ( Expressions<out es> (. e = new NAryExpr(x, new FunctionCall(id), es); .)

-      | /* empty */         (. e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); .)

+      | /* empty */         (. e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); .)

       )

       ")"

     ]

@@ -1268,12 +1268,12 @@ AtomExpression<out Expr/*!*/ e>
   | "int"                   (. x = t; .)

     "("

     Expression<out e>

-    ")"                     (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new ExprSeq(e)); .)

+    ")"                     (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List<Expr>(e)); .)

 

   | "real"                  (. x = t; .)

     "("

     Expression<out e>

-    ")"                     (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new ExprSeq(e)); .)

+    ")"                     (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>(e)); .)

 

   | "(" ( Expression<out e>                 (. if (e is BvBounds)

                                                  this.SemErr("parentheses around bitvector bounds " +

@@ -1349,7 +1349,7 @@ Attribute<ref QKeyValue kv>
 .

 

 AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>

-= (. IToken/*!*/ tok;  Expr/*!*/ e;  ExprSeq/*!*/ es;

+= (. IToken/*!*/ tok;  Expr/*!*/ e;  List<Expr>/*!*/ es;

      string key;

      List<object/*!*/> parameters;  object/*!*/ param;

   .)

@@ -1364,9 +1364,9 @@ AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>
             if (parameters.Count == 1 && parameters[0] is Expr) {

               e = (Expr)parameters[0];

               if(trig==null){

-                trig = new Trigger(tok, false, new ExprSeq(e), null);

+                trig = new Trigger(tok, false, new List<Expr>(e), null);

               } else {

-                trig.AddLast(new Trigger(tok, false, new ExprSeq(e), null));

+                trig.AddLast(new Trigger(tok, false, new List<Expr>(e), null));

               }

             } else {

               this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter");

@@ -1380,7 +1380,7 @@ AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>
           }

        .)

      |

-       Expression<out e>       (. es = new ExprSeq(e); .)

+       Expression<out e>       (. es = new List<Expr>(e); .)

        { "," Expression<out e> (. es.Add(e); .)

        }                       (. if (trig==null) {

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

@@ -1408,7 +1408,7 @@ IfThenElseExpression<out Expr/*!*/ e>
      Expr/*!*/ e0, e1, e2;

      e = dummyExpr; .)

   "if" (. tok = t; .) Expression<out e0> "then" Expression<out e1> "else" Expression<out e2>

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

+  (. e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>(e0, e1, e2)); .)

   .

 

 

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 2d220a35..1d221bb7 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -159,10 +159,10 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Expr>() != null);

       return base.VisitExpr((Expr)node.Clone());

     }

-    public override ExprSeq VisitExprSeq(ExprSeq list) {

+    public override List<Expr> VisitExprSeq(List<Expr> list) {

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

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

-      return base.VisitExprSeq(new ExprSeq(list));

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

+      return base.VisitExprSeq(new List<Expr>(list));

     }

     public override ForallExpr VisitForallExpr(ForallExpr node) {

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

diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
index ede25c0e..a461db22 100644
--- a/Source/Core/LambdaHelper.cs
+++ b/Source/Core/LambdaHelper.cs
@@ -97,8 +97,8 @@ namespace Microsoft.Boogie {
           // this is ugly, the output will depend on hashing order

           Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();

           List<Variable> formals = new List<Variable>();

-          ExprSeq callArgs = new ExprSeq();

-          ExprSeq axCallArgs = new ExprSeq();

+          List<Expr> callArgs = new List<Expr>();

+          List<Expr> axCallArgs = new List<Expr>();

           List<Variable> dummies = new List<Variable>(lambda.Dummies);

           TypeVariableSeq freeTypeVars = new TypeVariableSeq();

           List<Type/*!*/> fnTypeVarActuals = new List<Type/*!*/>();

@@ -160,7 +160,7 @@ namespace Microsoft.Boogie {
           NAryExpr body = Expr.Eq(select, bb);

           body.Type = Type.Bool;

           body.TypeParameters = SimpleTypeParamInstantiation.EMPTY;

-          Trigger trig = new Trigger(select.tok, true, new ExprSeq(select));

+          Trigger trig = new Trigger(select.tok, true, new List<Expr> { select });

           lambdaAxioms.Add(new ForallExpr(tok, forallTypeVariables, dummies, lambda.Attributes, trig, body));

 

           NAryExpr call = new NAryExpr(tok, fcall, callArgs);

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 00caea52..5b9aee5f 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -425,7 +425,7 @@ namespace Microsoft.Boogie
                                 foreach (var domainName in linearDomains.Keys)

                                 {

                                     var domain = linearDomains[domainName];

-                                    callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)));

+                                    callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False }));

                                 }

                             }

                             else if (callCmd.InParallelWith != null)

@@ -435,7 +435,7 @@ namespace Microsoft.Boogie
                                     foreach (var domainName in linearDomains.Keys)

                                     {

                                         var domain = linearDomains[domainName];

-                                        callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)));

+                                        callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False }));

                                     }

                                     callCmd = callCmd.InParallelWith;

                                 }

@@ -452,7 +452,7 @@ namespace Microsoft.Boogie
                                     var domainName = FindDomainName(v);

                                     var domain = linearDomains[domainName];

                                     IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

-                                    domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName]));

+                                    domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName] });

                                 }

                                 foreach (var domainName in linearDomains.Keys)

                                 {

@@ -552,7 +552,7 @@ namespace Microsoft.Boogie
         public Expr Singleton(Expr e, string domainName)

         {

             var domain = linearDomains[domainName];

-            return Expr.Store(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)), e, Expr.True);

+            return Expr.Store(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False }), e, Expr.True);

         }

 

         List<AssignLhs> MkAssignLhss(params Variable[] args)

@@ -579,10 +579,10 @@ namespace Microsoft.Boogie
             foreach (Variable v in scope)

             {

                 IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

-                Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstInt), new ExprSeq(new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(count++))));

-                e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new ExprSeq(new IdentifierExpr(Token.NoToken, partition), e));

-                e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), e));

-                e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.True)));

+                Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstInt), new List<Expr>{ new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(count++)) } );

+                e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new List<Expr> { new IdentifierExpr(Token.NoToken, partition), e } );

+                e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), e } );

+                e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.True }));

                 disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr);

             }

             return new ExistsExpr(Token.NoToken, new List<Variable> { partition }, disjointExpr);

@@ -622,13 +622,13 @@ namespace Microsoft.Boogie
                 IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);

                 BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));

                 IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

-                var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new ExprSeq(aie, bie));

-                var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(mapApplTerm, xie));

+                var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new List<Expr> { aie, bie } );

+                var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie } );

                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or,

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));

+                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie } ),

+                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie} ));

                 var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null, 

-                                               new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)), 

+                                               new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }), 

                                                new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, axiomExpr));

@@ -650,13 +650,13 @@ namespace Microsoft.Boogie
                 IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);

                 BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));

                 IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

-                var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new ExprSeq(aie, bie));

-                var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(mapApplTerm, xie));

+                var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new List<Expr> { aie, bie });

+                var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie });

                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp,

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));

+                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),

+                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));

                 var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null,

-                                               new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)), 

+                                               new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }), 

                                                new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, axiomExpr));

@@ -674,12 +674,12 @@ namespace Microsoft.Boogie
                 BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));

                 IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

                 var trueTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), 

-                                           new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.True)), xie));

+                                           new List<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List<Expr> { Expr.True }), xie });

                 var trueAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { x }, trueTerm);

                 trueAxiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, trueAxiomExpr));

                 var falseTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),

-                                           new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.False)), xie)); 

+                                           new List<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List<Expr> { Expr.False }), xie }); 

                 var falseAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm));

                 falseAxiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, falseAxiomExpr));

@@ -701,13 +701,13 @@ namespace Microsoft.Boogie
                 IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);

                 BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));

                 IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

-                var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new ExprSeq(aie, bie));

-                var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(mapApplTerm, xie));

+                var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new List<Expr> { aie, bie });

+                var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie });

                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq,

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));

+                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),

+                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));

                 var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null, 

-                                               new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)), 

+                                               new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }), 

                                                new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, axiomExpr));

@@ -726,7 +726,7 @@ namespace Microsoft.Boogie
                 IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);

                 BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));

                 IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

-                var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new ExprSeq(aie)), xie));

+                var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new List<Expr> { aie }), xie });

                 var axiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { a, x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, axiomExpr));

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 4815c781..90cfce97 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -182,7 +182,7 @@ namespace Microsoft.Boogie
 

         private void AddCallToYieldProc(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)

         {

-            ExprSeq exprSeq = new ExprSeq();

+            List<Expr> exprSeq = new List<Expr>();

             foreach (string domainName in linearTypechecker.linearDomains.Keys)

             {

                 exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));

@@ -208,7 +208,7 @@ namespace Microsoft.Boogie
                 var domainName = linearTypechecker.FindDomainName(v);

                 var domain = linearTypechecker.linearDomains[domainName];

                 IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

-                domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName]));

+                domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName] });

             }

             return domainNameToExpr;

         }

@@ -597,7 +597,7 @@ namespace Microsoft.Boogie
                     if (domainName == null) continue;

                     var domain = linearTypechecker.linearDomains[domainName];

                     IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

-                    domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName]));

+                    domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName] });

                 }

                 foreach (string domainName in linearTypechecker.linearDomains.Keys)

                 {

@@ -744,7 +744,7 @@ namespace Microsoft.Boogie
                 int labelCount = 0;

                 foreach (Procedure proc in yieldCheckerProcs)

                 {

-                    ExprSeq exprSeq = new ExprSeq();

+                    List<Expr> exprSeq = new List<Expr>();

                     foreach (Variable v in inputs)

                     {

                         exprSeq.Add(new IdentifierExpr(Token.NoToken, v));

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 17e4b0fb..3064ae0f 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -44,7 +44,7 @@ readonly Expr/*!*/ dummyExpr;
 readonly Cmd/*!*/ dummyCmd;

 readonly Block/*!*/ dummyBlock;

 readonly Bpl.Type/*!*/ dummyType;

-readonly Bpl.ExprSeq/*!*/ dummyExprSeq;

+readonly List<Expr>/*!*/ dummyExprSeq;

 readonly TransferCmd/*!*/ dummyTransferCmd;

 readonly StructuredCmd/*!*/ dummyStructuredCmd;

 

@@ -106,7 +106,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)
   dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);

   dummyBlock = new Block(Token.NoToken, "dummyBlock", new List<Cmd>(), new ReturnCmd(Token.NoToken));

   dummyType = new BasicType(Token.NoToken, SimpleType.Bool);

-  dummyExprSeq = new ExprSeq ();

+  dummyExprSeq = new List<Expr> ();

   dummyTransferCmd = new ReturnCmd(Token.NoToken);

   dummyStructuredCmd = new BreakCmd(Token.NoToken, null);

 }

@@ -1324,8 +1324,8 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		} else SynErr(110);

 	}

 

-	void Expressions(out ExprSeq/*!*/ es) {

-		Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new ExprSeq(); 

+	void Expressions(out List<Expr>/*!*/ es) {

+		Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List<Expr>(); 

 		Expression(out e);

 		es.Add(e); 

 		while (la.kind == 12) {

@@ -1624,12 +1624,12 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;

 		Expr/*!*/ index0 = dummyExpr; Expr/*!*/ e1;

 		bool store; bool bvExtract;

-		ExprSeq/*!*/ allArgs = dummyExprSeq;

+		List<Expr>/*!*/ allArgs = dummyExprSeq;

 		

 		AtomExpression(out e);

 		while (la.kind == 17) {

 			Get();

-			x = t; allArgs = new ExprSeq ();

+			x = t; allArgs = new List<Expr> ();

 			allArgs.Add(e);

 			store = false; bvExtract = false; 

 			if (StartOf(15)) {

@@ -1688,7 +1688,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 

 	void AtomExpression(out Expr/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;

-		ExprSeq/*!*/ es;  List<Variable>/*!*/ ds;  Trigger trig;

+		List<Expr>/*!*/ es;  List<Variable>/*!*/ ds;  Trigger trig;

 		TypeVariableSeq/*!*/ typeParams;

 		IdentifierExpr/*!*/ id;

 		QKeyValue kv;

@@ -1731,7 +1731,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 					Expressions(out es);

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

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

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

+					e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); 

 				} else SynErr(122);

 				Expect(10);

 			}

@@ -1752,7 +1752,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 			Expect(9);

 			Expression(out e);

 			Expect(10);

-			e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new ExprSeq(e)); 

+			e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List<Expr> { e }); 

 			break;

 		}

 		case 15: {

@@ -1761,7 +1761,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 			Expect(9);

 			Expression(out e);

 			Expect(10);

-			e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new ExprSeq(e)); 

+			e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr> { e }); 

 			break;

 		}

 		case 9: {

@@ -1901,7 +1901,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		Expression(out e1);

 		Expect(41);

 		Expression(out e2);

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

+		e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr> { e0, e1, e2 }); 

 	}

 

 	void CodeExpression(out List<Variable>/*!*/ locals, out List<Block/*!*/>/*!*/ blocks) {

@@ -1961,7 +1961,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 	}

 

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

-		IToken/*!*/ tok;  Expr/*!*/ e;  ExprSeq/*!*/ es;

+		IToken/*!*/ tok;  Expr/*!*/ e;  List<Expr>/*!*/ es;

 		string key;

 		List<object/*!*/> parameters;  object/*!*/ param;

 		

@@ -1984,9 +1984,9 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 			 if (parameters.Count == 1 && parameters[0] is Expr) {

 			   e = (Expr)parameters[0];

 			   if(trig==null){

-			     trig = new Trigger(tok, false, new ExprSeq(e), null);

+			     trig = new Trigger(tok, false, new List<Expr> { e }, null);

 			   } else {

-			     trig.AddLast(new Trigger(tok, false, new ExprSeq(e), null));

+			     trig.AddLast(new Trigger(tok, false, new List<Expr> { e }, null));

 			   }

 			 } else {

 			   this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter");

@@ -2001,7 +2001,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 			

 		} else if (StartOf(9)) {

 			Expression(out e);

-			es = new ExprSeq(e); 

+			es = new List<Expr> { e }; 

 			while (la.kind == 12) {

 				Get();

 				Expression(out e);

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index d8707bc4..4a9ca7a3 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -29,9 +29,9 @@ namespace Microsoft.Boogie {
     public virtual void TransferStateTo(Visitor targetVisitor) {

     }

 

-    public virtual ExprSeq VisitExprSeq(ExprSeq list) {

+    public virtual List<Expr> VisitExprSeq(List<Expr> list) {

       Contract.Requires(list != null);

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

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

       for (int i = 0, n = list.Count; i < n; i++)

         list[i] = (Expr)this.Visit(cce.NonNull(list[i]));

       return list;

@@ -235,9 +235,9 @@ namespace Microsoft.Boogie {
       Expr e = (Expr)this.Visit(node);

       return e;

     }

-    public override ExprSeq VisitExprSeq(ExprSeq exprSeq) {

+    public override List<Expr> VisitExprSeq(List<Expr> exprSeq) {

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

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

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

       for (int i = 0, n = exprSeq.Count; i < n; i++)

         exprSeq[i] = this.VisitExpr(cce.NonNull(exprSeq[i]));

       return exprSeq;

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index 09b6664e..c14cb82e 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -369,7 +369,7 @@ namespace Microsoft.Boogie {
       } else if (e is NAryExpr) {

         NAryExpr ne = (NAryExpr)e;

         IAppliable fun = ne.Fun;

-        ExprSeq eSeq = ne.Args;

+        List<Expr> eSeq = ne.Args;

         if (fun != null) {

           if ((fun.FunctionName == "$Length" || fun.FunctionName == "$StringLength") && eSeq.Count == 1) {

             Expr e0 = eSeq[0];

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 192e9a68..7acd2f6f 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -167,7 +167,7 @@ namespace Microsoft.Boogie.Houdini {
                     var varList = new List<Expr>();

                     exprVars.Args.OfType<Expr>().Iter(v => varList.Add(v));

                     

-                    var args = new ExprSeq();

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

                     controlVar.InParams.Iter(v => args.Add(Expr.Ident(v)));

                     Expr term = Expr.Eq(new NAryExpr(Token.NoToken, new FunctionCall(controlVar), args),

                                  function2Value[tup.Item1].Gamma(varList));

@@ -175,7 +175,7 @@ namespace Microsoft.Boogie.Houdini {
                     if (controlVar.InParams.Count != 0)

                     {

                         term = new ForallExpr(Token.NoToken, new List<Variable>(controlVar.InParams.ToArray()),

-                            new Trigger(Token.NoToken, true, new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(controlVar), args))),

+                            new Trigger(Token.NoToken, true, new List<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(controlVar), args) }),

                             term);

                     }

 

@@ -883,7 +883,7 @@ namespace Microsoft.Boogie.Houdini {
                 functionsUsed.Add(Tuple.Create((node.Fun as FunctionCall).FunctionName, constant, node));

                 boolConstants.Add(constant);

 

-                var args = new ExprSeq();

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

                 bound.OfType<Variable>().Select(v => Expr.Ident(v)).Iter(v => args.Add(v));

                 return new NAryExpr(Token.NoToken, new FunctionCall(constant), args);

             }

@@ -1515,8 +1515,8 @@ namespace Microsoft.Boogie.Houdini {
                 if (!AbstractDomainFactory.bvslt.ContainsKey(bits))

                     throw new AbsHoudiniInternalError("No builtin function found for bv" + bits.ToString());

                 var bvslt = AbstractDomainFactory.bvslt[bits];

-                return new NAryExpr(Token.NoToken, new FunctionCall(bvslt), new ExprSeq(v,

-                    new LiteralExpr(Token.NoToken, Basetypes.BigNum.FromInt(1 << (upper+1)), 32)));

+                return new NAryExpr(Token.NoToken, new FunctionCall(bvslt), new List<Expr> { v,

+                    new LiteralExpr(Token.NoToken, Basetypes.BigNum.FromInt(1 << (upper+1)), 32) });

             }

             else

             {

@@ -2760,7 +2760,7 @@ namespace Microsoft.Boogie.Houdini {
             var function = new Function(Token.NoToken, impl.Name + summaryPredSuffix, functionInterfaceVars, returnVar);

             prover.Context.DeclareFunction(function, "");

 

-            ExprSeq exprs = new ExprSeq();

+            List<Expr> exprs = new List<Expr>();

             foreach (Variable v in vcgen.program.GlobalVariables())

             {

                 Contract.Assert(v != null);

diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs
index 2174c150..507aaf61 100644
--- a/Source/Predication/BlockPredicator.cs
+++ b/Source/Predication/BlockPredicator.cs
@@ -68,7 +68,7 @@ public class BlockPredicator {
                    new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>

                      new NAryExpr(Token.NoToken,

                        new IfThenElse(Token.NoToken),

-                       new ExprSeq(p, rhs, lhs.AsExpr))))));

+                       new List<Expr> { p, rhs, lhs.AsExpr })))));

     } else if (cmd is AssertCmd) {

       var aCmd = (AssertCmd)cmd;

       if (cmdSeq.Last() is AssignCmd &&

@@ -112,7 +112,7 @@ public class BlockPredicator {
         cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,

                                     new NAryExpr(Token.NoToken,

                                       new IfThenElse(Token.NoToken),

-                                      new ExprSeq(p, havocTempExpr, v))));

+                                      new List<Expr> { p, havocTempExpr, v })));

       }

     } else if (cmd is CallCmd) {

       Debug.Assert(useProcedurePredicates);

@@ -261,7 +261,7 @@ public class BlockPredicator {
     if (useProcedurePredicates) {

       return new NAryExpr(Token.NoToken,

                  new IfThenElse(Token.NoToken),

-                 new ExprSeq(fp, then, eElse));

+                 new List<Expr>{ fp, then, eElse });

     } else {

       return then;

     }

diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 8e1b960b..5222061f 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -86,7 +86,7 @@ public class SmartBlockPredicator {
                    new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>

                      new NAryExpr(Token.NoToken,

                        new IfThenElse(Token.NoToken),

-                       new ExprSeq(p, rhs, lhs.AsExpr))))));

+                       new List<Expr> { p, rhs, lhs.AsExpr })))));

     } else if (cmd is AssertCmd) {

       var aCmd = (AssertCmd)cmd;

       Expr newExpr = new EnabledReplacementVisitor(p).VisitExpr(aCmd.Expr);

@@ -119,7 +119,7 @@ public class SmartBlockPredicator {
         cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,

                                     new NAryExpr(Token.NoToken,

                                       new IfThenElse(Token.NoToken),

-                                      new ExprSeq(p, havocTempExpr, v))));

+                                      new List<Expr> { p, havocTempExpr, v })));

       }

     } else if (cmd is CommentCmd) {

       // skip

@@ -470,7 +470,7 @@ public class SmartBlockPredicator {
     if (myUseProcedurePredicates) {

       return new NAryExpr(Token.NoToken,

                  new IfThenElse(Token.NoToken),

-                 new ExprSeq(fp, then, eElse));

+                 new List<Expr> { fp, then, eElse });

     } else {

       return then;

     }

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 6dc69528..22ba09be 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -75,7 +75,7 @@ namespace Microsoft.Boogie.VCExprAST {
       return Pop();

     }

 

-    public List<VCExpr/*!*/>/*!*/ Translate(ExprSeq exprs) {

+    public List<VCExpr/*!*/>/*!*/ Translate(List<Expr> exprs) {

       Contract.Requires(exprs != null);

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

       List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>();

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 93de935d..36b8fbe5 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1431,7 +1431,7 @@ namespace VC {
         if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) {

           string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");

           if (description != null) {

-            Expr mv = new NAryExpr(pc.tok, new FunctionCall(ModelViewInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Ident(ModelViewInfo.MVState_ConstantDef), Bpl.Expr.Literal(mvInfo.CapturePoints.Count)));

+            Expr mv = new NAryExpr(pc.tok, new FunctionCall(ModelViewInfo.MVState_FunctionDef), new List<Expr> { Bpl.Expr.Ident(ModelViewInfo.MVState_ConstantDef), Bpl.Expr.Literal(mvInfo.CapturePoints.Count) });

             copy = Bpl.Expr.And(mv, copy);

             mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, new Dictionary<Variable, Expr>(incarnationMap)));

           }

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 3fe3910e..330ffe49 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -177,7 +177,7 @@ namespace Microsoft.Boogie
                 return;

 

             // collect the variables needed in the invariant

-            ExprSeq exprs = new ExprSeq();

+            List<Expr> exprs = new List<Expr>();

             List<Variable> vars = new List<Variable>();

             List<string> names = new List<string>();

 

@@ -283,7 +283,7 @@ namespace Microsoft.Boogie
             CurrentLocalVariables = impl.LocVars;

 

             // collect the variables needed in the invariant

-            ExprSeq exprs = new ExprSeq();

+            List<Expr> exprs = new List<Expr>();

             List<Variable> vars = new List<Variable>();

             List<string> names = new List<string>();

 

@@ -590,7 +590,7 @@ namespace Microsoft.Boogie
                     implName2StratifiedInliningInfo[impl.Name] = info;

                     // We don't need controlFlowVariable for stratified Inlining

                     //impl.LocVars.Add(info.controlFlowVariable);

-                    ExprSeq exprs = new ExprSeq();

+                    List<Expr> exprs = new List<Expr>();

 

                     if (mode != Mode.Boogie && QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))

                     {

@@ -660,7 +660,7 @@ namespace Microsoft.Boogie
                 var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

                 boogieContext.DeclareFunction(recordFunc, "");

 

-                var exprs = new ExprSeq();

+                var exprs = new List<Expr>();

                 exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));

 

                 Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index ef2cd1d1..7f5b3779 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -213,7 +213,7 @@ namespace VC {
       function = new Function(Token.NoToken, impl.Name, functionInterfaceVars, returnVar);

       vcgen.prover.Context.DeclareFunction(function, "");

 

-      ExprSeq exprs = new ExprSeq();

+      List<Expr> exprs = new List<Expr>();

       foreach (Variable v in vcgen.program.GlobalVariables()) {

         Contract.Assert(v != null);

         exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

@@ -343,7 +343,7 @@ namespace VC {
         var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

         prover.Context.DeclareFunction(recordFunc, "");

 

-        var exprs = new ExprSeq();

+        var exprs = new List<Expr>();

         exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));

 

         Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);