Started to remove ...Seq classes

34 files changed, 364 insertions, 399 deletions

diff --git a/Source/CodeContractsExtender/cce.cs b/Source/CodeContractsExtender/cce.cs
index 12163c40..02b80458 100644
--- a/Source/CodeContractsExtender/cce.cs
+++ b/Source/CodeContractsExtender/cce.cs
@@ -29,7 +29,7 @@ public static class cce {
     return collection != null && cce.NonNullElements(collection.Values);

   }

   //[Pure]

-  //public static bool NonNullElements(VariableSeq collection) {

+  //public static bool NonNullElements(List<Variable> collection) {

   //  return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);

   //}

   /// <summary>

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index ad0618f7..8654af37 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -385,8 +385,8 @@ namespace Microsoft.Boogie {
 

       bool detLoopExtract = CommandLineOptions.Clo.DeterministicExtractLoops;

 

-      Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToInputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();

-      Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToOutputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();

+      Dictionary<Block/*!*/, List<Variable>/*!*/>/*!*/ loopHeaderToInputs = new Dictionary<Block/*!*/, List<Variable>/*!*/>();

+      Dictionary<Block/*!*/, List<Variable>/*!*/>/*!*/ loopHeaderToOutputs = new Dictionary<Block/*!*/, List<Variable>/*!*/>();

       Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>();

       Dictionary<Block/*!*/, LoopProcedure/*!*/>/*!*/ loopHeaderToLoopProc = new Dictionary<Block/*!*/, LoopProcedure/*!*/>();

       Dictionary<Block/*!*/, CallCmd/*!*/>/*!*/ loopHeaderToCallCmd1 = new Dictionary<Block/*!*/, CallCmd/*!*/>();

@@ -396,17 +396,17 @@ namespace Microsoft.Boogie {
       foreach (Block/*!*/ header in g.Headers) {

         Contract.Assert(header != null);

         Contract.Assert(header != null);

-        VariableSeq inputs = new VariableSeq();

-        VariableSeq outputs = new VariableSeq();

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

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

         ExprSeq callInputs1 = new ExprSeq();

-        IdentifierExprSeq callOutputs1 = new IdentifierExprSeq();

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

         ExprSeq callInputs2 = new ExprSeq();

-        IdentifierExprSeq callOutputs2 = new IdentifierExprSeq();

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

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

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

         Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>(); // Variable -> IdentifierExpr

 

-        VariableSeq/*!*/ targets = new VariableSeq();

+        List<Variable>/*!*/ targets = new List<Variable>();

         HashSet<Variable> footprint = new HashSet<Variable>();

 

         foreach (Block/*!*/ b in g.BackEdgeNodes(header))

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

         }

 

-        IdentifierExprSeq/*!*/ globalMods = new IdentifierExprSeq();

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

         Set targetSet = new Set();

         foreach (Variable/*!*/ v in targets)

         {

@@ -532,8 +532,8 @@ namespace Microsoft.Boogie {
         HashSet<string> dummyBlocks = new HashSet<string>();

 

         CodeCopier codeCopier = new CodeCopier(loopHeaderToSubstMap[header]);  // fix me

-        VariableSeq inputs = loopHeaderToInputs[header];

-        VariableSeq outputs = loopHeaderToOutputs[header];

+        List<Variable> inputs = loopHeaderToInputs[header];

+        List<Variable> outputs = loopHeaderToOutputs[header];

         int si_unique_loc = 1; // Added by AL: to distinguish the back edges

         foreach (Block/*!*/ source in g.BackEdgeNodes(header)) {

           Contract.Assert(source != null);

@@ -586,7 +586,7 @@ namespace Microsoft.Boogie {
                             auxNewBlock.Cmds.Add(assignCmd);

                         }

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

-                        IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;

+                        List<IdentifierExpr>/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;

                         foreach (IdentifierExpr gl in globalsMods)

                             lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));

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

@@ -689,7 +689,7 @@ namespace Microsoft.Boogie {
         blocks.Add(exit);

         Implementation loopImpl =

             new Implementation(Token.NoToken, loopProc.Name,

-                                new TypeVariableSeq(), inputs, outputs, new VariableSeq(), blocks);

+                                new TypeVariableSeq(), inputs, outputs, new List<Variable>(), blocks);

         loopImpl.Proc = loopProc;

         loopImpls.Add(loopImpl);

 

@@ -1707,10 +1707,10 @@ namespace Microsoft.Boogie {
     /// and without any attributes.

     /// The Type of each Formal is cloned.

     /// </summary>

-    public static VariableSeq StripWhereClauses(VariableSeq w) {

+    public static List<Variable> StripWhereClauses(List<Variable> w) {

       Contract.Requires(w != null);

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

-      VariableSeq s = new VariableSeq();

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

+      List<Variable> s = new List<Variable>();

       foreach (Variable/*!*/ v in w) {

         Contract.Assert(v != null);

         Formal f = (Formal)v;

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

   public abstract class DeclWithFormals : NamedDeclaration {

     public TypeVariableSeq/*!*/ TypeParameters;

-    public /*readonly--except in StandardVisitor*/ VariableSeq/*!*/ InParams, OutParams;

+    public /*readonly--except in StandardVisitor*/ List<Variable>/*!*/ InParams, OutParams;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

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

 

     public DeclWithFormals(IToken tok, string name, TypeVariableSeq typeParams,

-                            VariableSeq inParams, VariableSeq outParams)

+                            List<Variable> inParams, List<Variable> outParams)

       : base(tok, name) {

       Contract.Requires(inParams != null);

       Contract.Requires(outParams != null);

@@ -1865,9 +1865,9 @@ namespace Microsoft.Boogie {
     }

 

     protected void SortTypeParams() {

-      TypeSeq/*!*/ allTypes = new TypeSeq(InParams.Select(Item => Item.TypedIdent.Type).ToArray());

+      List<Type>/*!*/ allTypes = new List<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray());

       Contract.Assert(allTypes != null);

-      allTypes.AddRange(new TypeSeq(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()));

+      allTypes.AddRange(new List<Type>(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()));

       TypeParameters = Type.SortTypeParams(TypeParameters, allTypes, null);

     }

 

@@ -1879,7 +1879,7 @@ namespace Microsoft.Boogie {
     /// context.

     /// </summary>

     /// <param name="rc"></param>

-    protected void RegisterFormals(VariableSeq formals, ResolutionContext rc) {

+    protected void RegisterFormals(List<Variable> formals, ResolutionContext rc) {

       Contract.Requires(rc != null);

       Contract.Requires(formals != null);

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

@@ -1895,7 +1895,7 @@ namespace Microsoft.Boogie {
     /// Resolves the where clauses (and attributes) of the formals.

     /// </summary>

     /// <param name="rc"></param>

-    protected void ResolveFormals(VariableSeq formals, ResolutionContext rc) {

+    protected void ResolveFormals(List<Variable> formals, ResolutionContext rc) {

       Contract.Requires(rc != null);

       Contract.Requires(formals != null);

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

@@ -1959,7 +1959,7 @@ namespace Microsoft.Boogie {
     public DatatypeSelector(Function constructor, int index)

       : base(constructor.InParams[index].tok, 

              constructor.InParams[index].Name + "#" + constructor.Name,

-             new VariableSeq(new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.OutParams[0].TypedIdent.Type), true)),

+             new List<Variable> { new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.OutParams[0].TypedIdent.Type), true) },

              new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.InParams[index].TypedIdent.Type), false)) 

     {

       this.constructor = constructor;

@@ -1974,7 +1974,7 @@ namespace Microsoft.Boogie {
     public DatatypeMembership(Function constructor)

       : base(constructor.tok, 

              "is#" + constructor.Name,

-             new VariableSeq(new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.OutParams[0].TypedIdent.Type), true)),

+             new List<Variable> { new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.OutParams[0].TypedIdent.Type), true) },

              new Formal(constructor.tok, new TypedIdent(constructor.tok, "", Type.Bool), false)) 

     {

       this.constructor = constructor;

@@ -1994,7 +1994,7 @@ namespace Microsoft.Boogie {
     private bool neverTrigger;

     private bool neverTriggerComputed;

 

-    public Function(IToken tok, string name, VariableSeq args, Variable result)

+    public Function(IToken tok, string name, List<Variable> args, Variable result)

       : this(tok, name, new TypeVariableSeq(), args, result, null) {

       Contract.Requires(result != null);

       Contract.Requires(args != null);

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

       //:this(tok, name, new TypeVariableSeq(), args, result, null);

     }

-    public Function(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq args, Variable result)

+    public Function(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> args, Variable result)

       : this(tok, name, typeParams, args, result, null) {

       Contract.Requires(result != null);

       Contract.Requires(args != null);

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

       //:this(tok, name, typeParams, args, result, null);

     }

-    public Function(IToken tok, string name, VariableSeq args, Variable result, string comment)

+    public Function(IToken tok, string name, List<Variable> args, Variable result, string comment)

       : this(tok, name, new TypeVariableSeq(), args, result, comment) {

       Contract.Requires(result != null);

       Contract.Requires(args != null);

@@ -2019,8 +2019,8 @@ namespace Microsoft.Boogie {
       Contract.Requires(tok != null);

       //:this(tok, name, new TypeVariableSeq(), args, result, comment);

     }

-    public Function(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq args, Variable/*!*/ result, string comment)

-      : base(tok, name, typeParams, args, new VariableSeq(result)) {

+    public Function(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> args, Variable/*!*/ result, string comment)

+      : base(tok, name, typeParams, args, new List<Variable> { result }) {

       Contract.Requires(result != null);

       Contract.Requires(args != null);

       Contract.Requires(typeParams != null);

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

       Comment = comment;

     }

-    public Function(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq args, Variable result,

+    public Function(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> args, Variable result,

                     string comment, QKeyValue kv)

       : this(tok, name, typeParams, args, result, comment) {

       Contract.Requires(args != null);

@@ -2091,8 +2091,8 @@ namespace Microsoft.Boogie {
         }

         rc.PopVarContext();

         Type.CheckBoundVariableOccurrences(TypeParameters,

-                                           new TypeSeq(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),

-                                           new TypeSeq(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),

+                                           new List<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),

+                                           new List<Type>(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),

                                            this.tok, "function arguments",

                                            rc);

       } finally {

@@ -2133,7 +2133,7 @@ namespace Microsoft.Boogie {
     public Axiom CreateDefinitionAxiom(Expr definition, QKeyValue kv = null) {

       Contract.Requires(definition != null);

 

-      VariableSeq dummies = new VariableSeq();

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

       ExprSeq callArgs = new ExprSeq();

       int i = 0;

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

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

 

   public class Macro : Function {

-    public Macro(IToken tok, string name, VariableSeq args, Variable result)

+    public Macro(IToken tok, string name, List<Variable> args, Variable result)

       : base(tok, name, args, result) { }

   }

 

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

   public class Procedure : DeclWithFormals {

     public List<Requires>/*!*/ Requires;

-    public IdentifierExprSeq/*!*/ Modifies;

+    public List<IdentifierExpr>/*!*/ Modifies;

     public List<Ensures>/*!*/ Ensures;

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -2378,8 +2378,8 @@ namespace Microsoft.Boogie {
     [Rep]

     public readonly ProcedureSummary/*!*/ Summary;

 

-    public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams,

-      List<Requires>/*!*/ requires, IdentifierExprSeq/*!*/ modifies, List<Ensures>/*!*/ ensures)

+    public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, List<Variable>/*!*/ inParams, List<Variable>/*!*/ outParams,

+      List<Requires>/*!*/ requires, List<IdentifierExpr>/*!*/ modifies, List<Ensures>/*!*/ ensures)

       : this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -2392,8 +2392,8 @@ namespace Microsoft.Boogie {
       //:this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null);

     }

 

-    public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams,

-      List<Requires>/*!*/ @requires, IdentifierExprSeq/*!*/ @modifies, List<Ensures>/*!*/ @ensures, QKeyValue kv

+    public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, List<Variable>/*!*/ inParams, List<Variable>/*!*/ outParams,

+      List<Requires>/*!*/ @requires, List<IdentifierExpr>/*!*/ @modifies, List<Ensures>/*!*/ @ensures, QKeyValue kv

       )

       : base(tok, name, typeParams, inParams, outParams) {

       Contract.Requires(tok != null);

@@ -2484,8 +2484,8 @@ namespace Microsoft.Boogie {
         ResolveAttributes(rc);

 

         Type.CheckBoundVariableOccurrences(TypeParameters,

-                                           new TypeSeq(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),

-                                           new TypeSeq(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),        

+                                           new List<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),

+                                           new List<Type>(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),        

                                            this.tok, "procedure arguments",

                                            rc);

 

@@ -2532,7 +2532,7 @@ namespace Microsoft.Boogie {
       private Dictionary<string, Block> blockLabelMap;

 

       public LoopProcedure(Implementation impl, Block header,

-                           VariableSeq inputs, VariableSeq outputs, IdentifierExprSeq globalMods)

+                           List<Variable> inputs, List<Variable> outputs, List<IdentifierExpr> globalMods)

           : base(Token.NoToken, impl.Name + "_loop_" + header.ToString(),

                new TypeVariableSeq(), inputs, outputs,

                new List<Requires>(), globalMods, new List<Ensures>())

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

 

   public class Implementation : DeclWithFormals {

-    public VariableSeq/*!*/ LocVars;

+    public List<Variable>/*!*/ LocVars;

     [Rep]

     public StmtList StructuredStmts;

     [Rep]

@@ -2568,7 +2568,7 @@ namespace Microsoft.Boogie {
     // Blocks before applying passification etc.

     // Both are used only when /inline is set.

     public List<Block/*!*/> OriginalBlocks;

-    public VariableSeq OriginalLocVars;

+    public List<Variable> OriginalLocVars;

 

     // Strongly connected components

     private StronglyConnectedComponents<Block/*!*/> scc;

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

     }

 

-    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)

+    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)

       : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) {

       Contract.Requires(structuredStmts != null);

       Contract.Requires(localVariables != null);

@@ -2653,7 +2653,7 @@ namespace Microsoft.Boogie {
       //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors());

     }

 

-    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts)

+    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts)

       : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()) {

       Contract.Requires(structuredStmts != null);

       Contract.Requires(localVariables != null);

@@ -2665,7 +2665,7 @@ namespace Microsoft.Boogie {
       //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors());

     }

 

-    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts, Errors errorHandler)

+    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts, Errors errorHandler)

       : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler) {

       Contract.Requires(errorHandler != null);

       Contract.Requires(structuredStmts != null);

@@ -2681,9 +2681,9 @@ namespace Microsoft.Boogie {
     public Implementation(IToken/*!*/ tok,

       string/*!*/ name,

       TypeVariableSeq/*!*/ typeParams,

-      VariableSeq/*!*/ inParams,

-      VariableSeq/*!*/ outParams,

-      VariableSeq/*!*/ localVariables,

+      List<Variable>/*!*/ inParams,

+      List<Variable>/*!*/ outParams,

+      List<Variable>/*!*/ localVariables,

       [Captured] StmtList/*!*/ structuredStmts,

       QKeyValue kv,

       Errors/*!*/ errorHandler)

@@ -2705,7 +2705,7 @@ namespace Microsoft.Boogie {
       Attributes = kv;

     }

 

-    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] List<Block/*!*/> block)

+    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] List<Block/*!*/> block)

       : this(tok, name, typeParams, inParams, outParams, localVariables, block, null) {

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

       Contract.Requires(localVariables != null);

@@ -2720,9 +2720,9 @@ namespace Microsoft.Boogie {
     public Implementation(IToken/*!*/ tok,

       string/*!*/ name,

       TypeVariableSeq/*!*/ typeParams,

-      VariableSeq/*!*/ inParams,

-      VariableSeq/*!*/ outParams,

-      VariableSeq/*!*/ localVariables,

+      List<Variable>/*!*/ inParams,

+      List<Variable>/*!*/ outParams,

+      List<Variable>/*!*/ localVariables,

       [Captured] List<Block/*!*/>/*!*/ blocks,

       QKeyValue kv)

       : base(tok, name, typeParams, inParams, outParams) {

@@ -2833,8 +2833,8 @@ namespace Microsoft.Boogie {
         rc.PopVarContext();

 

         Type.CheckBoundVariableOccurrences(TypeParameters,

-                                           new TypeSeq(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),

-                                           new TypeSeq(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),

+                                           new List<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),

+                                           new List<Type>(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),

                                            this.tok, "implementation arguments",

                                            rc);

       } finally {

@@ -2862,7 +2862,7 @@ namespace Microsoft.Boogie {
         Contract.Assert(v != null);

         v.Typecheck(tc);

       }

-      IdentifierExprSeq oldFrame = tc.Frame;

+      List<IdentifierExpr> oldFrame = tc.Frame;

       tc.Frame = Proc.Modifies;

       foreach (Block b in Blocks) {

         b.Typecheck(tc);

@@ -2870,7 +2870,7 @@ namespace Microsoft.Boogie {
       Contract.Assert(tc.Frame == Proc.Modifies);

       tc.Frame = oldFrame;

     }

-    void MatchFormals(VariableSeq/*!*/ implFormals, VariableSeq/*!*/ procFormals, string/*!*/ inout, TypecheckingContext/*!*/ tc) {

+    void MatchFormals(List<Variable>/*!*/ implFormals, List<Variable>/*!*/ procFormals, string/*!*/ inout, TypecheckingContext/*!*/ tc) {

       Contract.Requires(implFormals != null);

       Contract.Requires(procFormals != null);

       Contract.Requires(inout != null);

@@ -3214,28 +3214,6 @@ namespace Microsoft.Boogie {
   // Generic Sequences

   //---------------------------------------------------------------------

 

-  public sealed class VariableSeq : List<Variable> {

-    public VariableSeq(params Variable[]/*!*/ args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public VariableSeq(VariableSeq/*!*/ varSeq)

-      : base(varSeq) {

-      Contract.Requires(varSeq != null);

-    }

-  }

-

-  public sealed class TypeSeq : List<Type> {

-    public TypeSeq(params Type[]/*!*/ args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public TypeSeq(TypeSeq/*!*/ varSeq)

-      : base(varSeq) {

-      Contract.Requires(varSeq != null);

-    }

-  }

-

   public sealed class TypeVariableSeq : List<TypeVariable> {

     public TypeVariableSeq(params TypeVariable[]/*!*/ args)

       : base(args) {

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

   }

 

-  public sealed class IdentifierExprSeq : List<IdentifierExpr> {

-    public IdentifierExprSeq(params IdentifierExpr[]/*!*/ args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public IdentifierExprSeq(IdentifierExprSeq/*!*/ ideSeq)

-      : base(ideSeq) {

-      Contract.Requires(ideSeq != null);

-    }

-

-  }

-

-

   public sealed class CmdSeq : List<Cmd> {

     public CmdSeq(params Cmd[]/*!*/ args)

       : base(args) {

@@ -3367,7 +3332,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public static void Emit(this IdentifierExprSeq ids, TokenTextWriter stream, bool printWhereComments) {

+    public static void Emit(this List<IdentifierExpr> ids, TokenTextWriter stream, bool printWhereComments) {

       Contract.Requires(stream != null);

       string sep = "";

       foreach (IdentifierExpr/*!*/ e in ids) {

@@ -3384,7 +3349,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public static void Emit(this VariableSeq vs, TokenTextWriter stream, bool emitAttributes) {

+    public static void Emit(this List<Variable> vs, TokenTextWriter stream, bool emitAttributes) {

       Contract.Requires(stream != null);

       string sep = "";

       foreach (Variable/*!*/ v in vs) {

@@ -3395,7 +3360,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public static void Emit(this TypeSeq tys, TokenTextWriter stream, string separator) {

+    public static void Emit(this List<Type> tys, TokenTextWriter stream, string separator) {

       Contract.Requires(separator != null);

       Contract.Requires(stream != null);

       string sep = "";

@@ -3439,7 +3404,7 @@ namespace Microsoft.Boogie {
     public RE()

       : base(Token.NoToken) {

     }

-    public override void AddAssignedVariables(VariableSeq vars) {

+    public override void AddAssignedVariables(List<Variable> vars) {

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

       throw new NotImplementedException();

     }

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 1eb2ccc8..ace4e7b6 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -932,7 +932,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(stream != null);

       throw new NotImplementedException();

     }

-    public override void AddAssignedVariables(VariableSeq vars) {

+    public override void AddAssignedVariables(List<Variable> vars) {

       Contract.Requires(vars != null);

       throw new NotImplementedException();

     }

@@ -944,11 +944,11 @@ namespace Microsoft.Boogie {
       Contract.Assert(tok != null);

     }

     public abstract void Emit(TokenTextWriter/*!*/ stream, int level);

-    public abstract void AddAssignedVariables(VariableSeq/*!*/ vars);

+    public abstract void AddAssignedVariables(List<Variable>/*!*/ vars);

     public void CheckAssignments(TypecheckingContext tc)

     {

         Contract.Requires(tc != null);

-        VariableSeq/*!*/ vars = new VariableSeq();

+        List<Variable>/*!*/ vars = new List<Variable>();

         this.AddAssignedVariables(vars);

         foreach (Variable/*!*/ v in vars)

         {

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

           // nothing to typecheck

       }

-      public override void AddAssignedVariables(VariableSeq vars)

+      public override void AddAssignedVariables(List<Variable> vars)

       {

           // nothing to add

       }

@@ -1121,7 +1121,7 @@ namespace Microsoft.Boogie {
     public override void Resolve(ResolutionContext rc) {

       

     }

-    public override void AddAssignedVariables(VariableSeq vars) {

+    public override void AddAssignedVariables(List<Variable> vars) {

       

     }

     public override void Typecheck(TypecheckingContext tc) {

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

     }

 

-    public override void AddAssignedVariables(VariableSeq vars) {

+    public override void AddAssignedVariables(List<Variable> vars) {

       

       foreach (AssignLhs/*!*/ l in Lhss) {

         Contract.Assert(l != null);

@@ -1535,10 +1535,10 @@ namespace Microsoft.Boogie {
       Contract.Invariant(Cmds != null);

     }

 

-    public /*readonly, except for the StandardVisitor*/ VariableSeq/*!*/ Locals;

+    public /*readonly, except for the StandardVisitor*/ List<Variable>/*!*/ Locals;

     public /*readonly, except for the StandardVisitor*/ CmdSeq/*!*/ Cmds;

 

-    public StateCmd(IToken tok, VariableSeq/*!*/ locals, CmdSeq/*!*/ cmds)

+    public StateCmd(IToken tok, List<Variable>/*!*/ locals, CmdSeq/*!*/ cmds)

       : base(tok) {

       Contract.Requires(locals != null);

       Contract.Requires(cmds != null);

@@ -1561,9 +1561,9 @@ namespace Microsoft.Boogie {
       rc.PopVarContext();

     }

 

-    public override void AddAssignedVariables(VariableSeq vars) {

+    public override void AddAssignedVariables(List<Variable> vars) {

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

-      VariableSeq/*!*/ vs = new VariableSeq();

+      List<Variable>/*!*/ vs = new List<Variable>();

       foreach (Cmd/*!*/ cmd in this.Cmds) {

         Contract.Assert(cmd != null);

         cmd.AddAssignedVariables(vs);

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

 

     // We have to give the type explicitly, because the type of the formal "likeThisOne" can contain type variables

-    protected Variable CreateTemporaryVariable(VariableSeq tempVars, Variable likeThisOne, Type ty, TempVarKind kind) {

+    protected Variable CreateTemporaryVariable(List<Variable> tempVars, Variable likeThisOne, Type ty, TempVarKind kind) {

       Contract.Requires(ty != null);

       Contract.Requires(likeThisOne != null);

       Contract.Requires(tempVars != null);

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

       }

     }

-    public CallCmd(IToken tok, string callee, ExprSeq ins, IdentifierExprSeq outs)

+    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);

@@ -1930,8 +1930,8 @@ namespace Microsoft.Boogie {
       // actual i/o arguments. This is done already during resolution

       // because CheckBoundVariableOccurrences needs a resolution

       // context

-      TypeSeq/*!*/ formalInTypes = new TypeSeq();

-      TypeSeq/*!*/ formalOutTypes = new TypeSeq();

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

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

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

         if (Ins[i] != null)

           formalInTypes.Add(cce.NonNull(Proc.InParams[i]).TypedIdent.Type);

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

     }

 

-    public override void AddAssignedVariables(VariableSeq vars) {

+    public override void AddAssignedVariables(List<Variable> vars) {

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

       foreach (IdentifierExpr e in Outs) {

         if (e != null) {

@@ -1985,10 +1985,10 @@ namespace Microsoft.Boogie {
           e.Typecheck(tc);

       this.CheckAssignments(tc);

 

-      TypeSeq/*!*/ formalInTypes = new TypeSeq();

-      TypeSeq/*!*/ formalOutTypes = new TypeSeq();

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

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

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

-      IdentifierExprSeq/*!*/ actualOuts = new IdentifierExprSeq();

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

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

         if (Ins[i] != null) {

           formalInTypes.Add(cce.NonNull(Proc.InParams[i]).TypedIdent.Type);

@@ -2037,7 +2037,7 @@ namespace Microsoft.Boogie {
       Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();

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

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

-      VariableSeq/*!*/ tempVars = new VariableSeq();

+      List<Variable>/*!*/ tempVars = new List<Variable>();

 

       // proc P(ins) returns (outs)

       //   requires Pre

@@ -2057,8 +2057,8 @@ namespace Microsoft.Boogie {
       // WildcardVars : new variables created just for this call, one per null in ains

 

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

-      VariableSeq/*!*/ cins = new VariableSeq();

-      VariableSeq wildcardVars = new VariableSeq();

+      List<Variable>/*!*/ cins = new List<Variable>();

+      List<Variable> wildcardVars = new List<Variable>();

       Contract.Assume(this.Proc != null);

       for (int i = 0; i < this.Proc.InParams.Count; ++i) {

         Variable/*!*/ param = cce.NonNull(this.Proc.InParams[i]);

@@ -2095,7 +2095,7 @@ namespace Microsoft.Boogie {
           AssignCmd assign = Cmd.SimpleAssign(Token.NoToken, cin_exp, cce.NonNull(this.Ins[i]));

           newBlockBody.Add(assign);

         } else {

-          IdentifierExprSeq/*!*/ ies = new IdentifierExprSeq();

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

           ies.Add(cin_exp);

           HavocCmd havoc = new HavocCmd(Token.NoToken, ies);

           newBlockBody.Add(havoc);

@@ -2157,7 +2157,7 @@ namespace Microsoft.Boogie {
       #endregion

 

       #region cframe := frame (to hold onto frame values in case they are referred to in the postcondition)

-      IdentifierExprSeq havocVarExprs = new IdentifierExprSeq();

+      List<IdentifierExpr> havocVarExprs = new List<IdentifierExpr>();

 

       foreach (IdentifierExpr/*!*/ f in this.Proc.Modifies) {

         Contract.Assert(f != null);

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

       #endregion

       #region Create couts

-      VariableSeq/*!*/ couts = new VariableSeq();

+      List<Variable>/*!*/ couts = new List<Variable>();

       for (int i = 0; i < this.Proc.OutParams.Count; ++i) {

         Variable/*!*/ param = cce.NonNull(this.Proc.OutParams[i]);

         bool isWildcard = this.Outs[i] == null;

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

       Expr.Resolve(rc);

     }

-    public override void AddAssignedVariables(VariableSeq vars) {

+    public override void AddAssignedVariables(List<Variable> vars) {

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

     }

   }

@@ -2423,7 +2423,7 @@ namespace Microsoft.Boogie {
         l = GenerateBoundVarListForMining(e.Expr, l);

       } else if (expr is QuantifierExpr) {

         QuantifierExpr qe = (QuantifierExpr)expr;

-        VariableSeq vs = qe.Dummies;

+        List<Variable> vs = qe.Dummies;

         foreach (Variable/*!*/ x in vs) {

           Contract.Assert(x != null);

           string name = x.Name;

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

 

   public class HavocCmd : Cmd {

-    public IdentifierExprSeq/*!*/ Vars;

+    public List<IdentifierExpr>/*!*/ Vars;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Vars != null);

     }

 

-    public HavocCmd(IToken/*!*/ tok, IdentifierExprSeq/*!*/ vars)

+    public HavocCmd(IToken/*!*/ tok, List<IdentifierExpr>/*!*/ vars)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(vars != null);

@@ -2617,7 +2617,7 @@ namespace Microsoft.Boogie {
         ide.Resolve(rc);

       }

     }

-    public override void AddAssignedVariables(VariableSeq vars) {

+    public override void AddAssignedVariables(List<Variable> vars) {

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

       foreach (IdentifierExpr/*!*/ e in this.Vars) {

         Contract.Assert(e != null);

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index e5d955d2..b3b2289b 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1801,12 +1801,12 @@ namespace Microsoft.Boogie {
       Contract.Assume(Func.OutParams.Count == 1);

 

       List<Type/*!*/>/*!*/ resultingTypeArgs;

-      TypeSeq actualResultType =

+      List<Type> actualResultType =

         Type.CheckArgumentTypes(Func.TypeParameters,

                                 out resultingTypeArgs,

-                                new TypeSeq(Func.InParams.Select(Item => Item.TypedIdent.Type).ToArray()),

+                                new List<Type>(Func.InParams.Select(Item => Item.TypedIdent.Type).ToArray()),

                                 actuals,

-                                new TypeSeq(Func.OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),

+                                new List<Type>(Func.OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),

                                 null,

         // we need some token to report a possibly wrong number of

         // arguments

@@ -2317,7 +2317,7 @@ namespace Microsoft.Boogie {
         return Type.Int;

       }

       MapType mapType = a0Type.AsMap;

-      TypeSeq actualArgTypes = new TypeSeq();

+      List<Type> actualArgTypes = new List<Type>();

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

         actualArgTypes.Add(cce.NonNull(args[i]).ShallowType);

       }

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

 

   public class CodeExpr : Expr {

-    public VariableSeq/*!*/ LocVars;

+    public List<Variable>/*!*/ LocVars;

     [Rep]

     public List<Block/*!*/>/*!*/ Blocks;

     [ContractInvariantMethod]

@@ -2563,7 +2563,7 @@ namespace Microsoft.Boogie {
       Contract.Invariant(cce.NonNullElements(Blocks));

     }

 

-    public CodeExpr(VariableSeq/*!*/ localVariables, List<Block/*!*/>/*!*/ blocks)

+    public CodeExpr(List<Variable>/*!*/ localVariables, List<Block/*!*/>/*!*/ blocks)

       : base(Token.NoToken) {

       Contract.Requires(localVariables != null);

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

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index e42df50f..5fdc3e68 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie {
   [ContractClass(typeof(BinderExprContracts))]

   public abstract class BinderExpr : Expr {

     public TypeVariableSeq/*!*/ TypeParameters;

-    public VariableSeq/*!*/ Dummies;

+    public List<Variable>/*!*/ Dummies;

     public QKeyValue Attributes;

     public Expr/*!*/ Body;

     [ContractInvariantMethod]

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

 

     public BinderExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,

-                      VariableSeq/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)

+                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)

       : base(tok)

       {

       Contract.Requires(tok != null);

@@ -160,7 +160,7 @@ namespace Microsoft.Boogie {
         rc.PopVarContext();

 

         // establish a canonical order of the type parameters

-        this.TypeParameters = Type.SortTypeParams(TypeParameters, new TypeSeq(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()), null);

+        this.TypeParameters = Type.SortTypeParams(TypeParameters, new List<Type>(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()), null);

 

       } finally {

         rc.TypeBinderState = previousTypeBinderState;

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

     protected TypeVariableSeq GetUnmentionedTypeParameters() {

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

-      TypeVariableSeq/*!*/ dummyParameters = Type.FreeVariablesIn(new TypeSeq(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()));

+      TypeVariableSeq/*!*/ dummyParameters = Type.FreeVariablesIn(new List<Type>(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()));

       Contract.Assert(dummyParameters != null);

       TypeVariableSeq/*!*/ unmentionedParameters = new TypeVariableSeq();

       foreach (TypeVariable/*!*/ var in TypeParameters) {

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

   public class ForallExpr : QuantifierExpr {

     public ForallExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParams,

-                      VariableSeq/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)

+                      List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)

       : base(tok, typeParams, dummies, kv, triggers, body) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParams != null);

@@ -430,21 +430,21 @@ namespace Microsoft.Boogie {
       Contract.Requires(body != null);

       Contract.Requires(dummies.Count + typeParams.Count > 0);

     }

-    public ForallExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)

+    public ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body)

       : base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

-    public ForallExpr(IToken tok, VariableSeq dummies, Expr body)

+    public ForallExpr(IToken tok, List<Variable> dummies, Expr body)

       : base(tok, new TypeVariableSeq(), dummies, null, null, body) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

-    public ForallExpr(IToken tok, TypeVariableSeq typeParams, VariableSeq dummies, Expr body)

+    public ForallExpr(IToken tok, TypeVariableSeq typeParams, List<Variable> dummies, Expr body)

       : base(tok, typeParams, dummies, null, null, body) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

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

 

   public class ExistsExpr : QuantifierExpr {

-    public ExistsExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ dummies,

+    public ExistsExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParams, List<Variable>/*!*/ dummies,

                       QKeyValue kv, Trigger triggers, Expr/*!*/ body)

       : base(tok, typeParams, dummies, kv, triggers, body) {

       Contract.Requires(tok != null);

@@ -476,14 +476,14 @@ namespace Microsoft.Boogie {
       Contract.Requires(body != null);

       Contract.Requires(dummies.Count + typeParams.Count > 0);

     }

-    public ExistsExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)

+    public ExistsExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body)

       : base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

-    public ExistsExpr(IToken tok, VariableSeq dummies, Expr body)

+    public ExistsExpr(IToken tok, List<Variable> dummies, Expr body)

       : base(tok, new TypeVariableSeq(), dummies, null, null, body) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

@@ -516,7 +516,7 @@ namespace Microsoft.Boogie {
     public readonly int SkolemId;

 

     public QuantifierExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,

-                          VariableSeq/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)

+                          List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)

       : base(tok, typeParameters, dummies, kv, body) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParameters != null);

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

   public class LambdaExpr : BinderExpr {

     public LambdaExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,

-                      VariableSeq/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)

+                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)

       : base(tok, typeParameters, dummies, kv, body) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParameters != null);

@@ -725,7 +725,7 @@ namespace Microsoft.Boogie {
       Body.Typecheck(tc);

       Contract.Assert(Body.Type != null);  // follows from postcondition of Expr.Typecheck

 

-      TypeSeq/*!*/ argTypes = new TypeSeq();

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

       foreach (Variable/*!*/ v in Dummies) {

         Contract.Assert(v != null);

         argTypes.Add(v.TypedIdent.Type);

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

 

         if (mapType == null) {

-          TypeSeq/*!*/ argTypes = new TypeSeq();

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

           foreach (Variable/*!*/ v in Dummies) {

             Contract.Assert(v != null);

             argTypes.Add(v.TypedIdent.Type);

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 3d02768e..e5fad05d 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -365,10 +365,10 @@ namespace Microsoft.Boogie {
 #if OLD_UNIFICATION

     public static IDictionary<TypeVariable!, Type!>!

                   MatchArgumentTypes(TypeVariableSeq! typeParams,

-                                     TypeSeq! formalArgs,

+                                     List<Type>! formalArgs,

                                      ExprSeq! actualArgs,

-                                     TypeSeq formalOuts,

-                                     IdentifierExprSeq actualOuts,

+                                     List<Type> formalOuts,

+                                     List<IdentifierExpr> actualOuts,

                                      string! opName,

                                      TypecheckingContext! tc)

       {

@@ -437,10 +437,10 @@ namespace Microsoft.Boogie {
 #else

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

                   MatchArgumentTypes(TypeVariableSeq/*!*/ typeParams,

-                                     TypeSeq/*!*/ formalArgs,

+                                     List<Type>/*!*/ formalArgs,

                                      ExprSeq/*!*/ actualArgs,

-                                     TypeSeq formalOuts,

-                                     IdentifierExprSeq actualOuts,

+                                     List<Type> formalOuts,

+                                     List<IdentifierExpr> actualOuts,

                                      string/*!*/ opName,

                                      TypecheckingContext/*!*/ tc) {

       Contract.Requires(typeParams != null);

@@ -505,12 +505,12 @@ namespace Microsoft.Boogie {
     //------------  on concrete types, substitute the result into the

     //------------  result type. Null is returned for type errors

 

-    public static TypeSeq CheckArgumentTypes(TypeVariableSeq/*!*/ typeParams,

+    public static List<Type> CheckArgumentTypes(TypeVariableSeq/*!*/ typeParams,

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

-                                             TypeSeq/*!*/ formalIns,

+                                             List<Type>/*!*/ formalIns,

                                              ExprSeq/*!*/ actualIns,

-                                             TypeSeq/*!*/ formalOuts,

-                                             IdentifierExprSeq actualOuts,

+                                             List<Type>/*!*/ formalOuts,

+                                             List<IdentifierExpr> actualOuts,

                                              IToken/*!*/ typeCheckingSubject,

                                              string/*!*/ opName,

                                              TypecheckingContext/*!*/ tc)

@@ -550,7 +550,7 @@ namespace Microsoft.Boogie {
         actualTypeParams.Add(subst[var]);

       }

 

-      TypeSeq/*!*/ actualResults = new TypeSeq();

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

       foreach (Type/*!*/ t in formalOuts) {

         Contract.Assert(t != null);

         actualResults.Add(t.Substitute(subst));

@@ -578,9 +578,9 @@ namespace Microsoft.Boogie {
     // about the same as Type.CheckArgumentTypes, but without

     // detailed error reports

     public static Type/*!*/ InferValueType(TypeVariableSeq/*!*/ typeParams,

-                                       TypeSeq/*!*/ formalArgs,

+                                       List<Type>/*!*/ formalArgs,

                                        Type/*!*/ formalResult,

-                                       TypeSeq/*!*/ actualArgs) {

+                                       List<Type>/*!*/ actualArgs) {

       Contract.Requires(typeParams != null);

       Contract.Requires(formalArgs != null);

       Contract.Requires(formalResult != null);

@@ -603,8 +603,8 @@ namespace Microsoft.Boogie {
 #if OLD_UNIFICATION

     public static IDictionary<TypeVariable!, Type!>!

                   InferTypeParameters(TypeVariableSeq! typeParams,

-                                      TypeSeq! formalArgs,

-                                      TypeSeq! actualArgs)

+                                      List<Type>! formalArgs,

+                                      List<Type>! actualArgs)

       {

  Contract.Requires(formalArgs.Length == actualArgs.Length);

       

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

     /// <summary>

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

-    /// (and only does arguments, not results; and takes actuals as TypeSeq, not ExprSeq)

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

     /// </summary>

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

                   InferTypeParameters(TypeVariableSeq/*!*/ typeParams,

-                                      TypeSeq/*!*/ formalArgs,

-                                      TypeSeq/*!*/ actualArgs) {

+                                      List<Type>/*!*/ formalArgs,

+                                      List<Type>/*!*/ actualArgs) {

       Contract.Requires(typeParams != null);

       Contract.Requires(formalArgs != null);

       Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Count == actualArgs.Count);

       Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));

 

       

-      TypeSeq proxies = new TypeSeq();

+      List<Type> proxies = new List<Type>();

       Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();

       foreach (TypeVariable/*!*/ tv in typeParams) {

         Contract.Assert(tv != null);

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

 

     // Sort the type parameters according to the order of occurrence in the argument types

-    public static TypeVariableSeq/*!*/ SortTypeParams(TypeVariableSeq/*!*/ typeParams, TypeSeq/*!*/ argumentTypes, Type resultType) {

+    public static TypeVariableSeq/*!*/ SortTypeParams(TypeVariableSeq/*!*/ typeParams, List<Type>/*!*/ argumentTypes, Type resultType) {

       Contract.Requires(typeParams != null);

       Contract.Requires(argumentTypes != null);

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

@@ -718,8 +718,8 @@ namespace Microsoft.Boogie {
     // not in "argumentTypes".

     [Pure]

     public static bool CheckBoundVariableOccurrences(TypeVariableSeq/*!*/ typeParams,

-                                                     TypeSeq/*!*/ argumentTypes,

-                                                     TypeSeq moreArgumentTypes,

+                                                     List<Type>/*!*/ argumentTypes,

+                                                     List<Type> moreArgumentTypes,

                                                      IToken/*!*/ resolutionSubject,

                                                      string/*!*/ subjectName,

                                                      ResolutionContext/*!*/ rc) {

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

 

     [Pure]

-    public static TypeVariableSeq FreeVariablesIn(TypeSeq arguments) {

+    public static TypeVariableSeq FreeVariablesIn(List<Type> arguments) {

       Contract.Requires(arguments != null);

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

       TypeVariableSeq/*!*/ res = new TypeVariableSeq();

@@ -1172,7 +1172,7 @@ Contract.Requires(that != null);
   // during the resolution phase

   public class UnresolvedTypeIdentifier : Type {

     public readonly string/*!*/ Name;

-    public readonly TypeSeq/*!*/ Arguments;

+    public readonly List<Type>/*!*/ Arguments;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Name != null);

@@ -1181,12 +1181,12 @@ Contract.Requires(that != null);
 

 

     public UnresolvedTypeIdentifier(IToken token, string name)

-      : this(token, name, new TypeSeq()) {

+      : this(token, name, new List<Type>()) {

       Contract.Requires(name != null);

       Contract.Requires(token != null);

     }

 

-    public UnresolvedTypeIdentifier(IToken token, string name, TypeSeq arguments)

+    public UnresolvedTypeIdentifier(IToken token, string name, List<Type> arguments)

       : base(token) {

       Contract.Requires(arguments != null);

       Contract.Requires(name != null);

@@ -1203,7 +1203,7 @@ Contract.Requires(that != null);
     public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {

       //Contract.Requires(cce.NonNullElements(varMap));

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

-      TypeSeq/*!*/ newArgs = new TypeSeq();

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

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         newArgs.Add(t.Clone(varMap));

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

     public override Type CloneUnresolved() {

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

-      TypeSeq/*!*/ newArgs = new TypeSeq();

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

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         newArgs.Add(t.CloneUnresolved());

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

           return this;

         }

-        TypeSeq/*!*/ resolvedArgs = ResolveArguments(rc);

+        List<Type>/*!*/ resolvedArgs = ResolveArguments(rc);

         Contract.Assert(resolvedArgs != null);

 

         return new TypeSynonymAnnotation(this.tok, synDecl, resolvedArgs);

@@ -1351,10 +1351,10 @@ Contract.Requires(that != null);
       return this;

     }

 

-    private TypeSeq ResolveArguments(ResolutionContext rc) {

+    private List<Type> ResolveArguments(ResolutionContext rc) {

       Contract.Requires(rc != null);

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

-      TypeSeq/*!*/ resolvedArgs = new TypeSeq();

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

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

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         resolvedArgs.Add(t.ResolveType(rc));

@@ -2271,7 +2271,7 @@ Contract.Requires(that != null);
     // each constraint specifies that the given combination of argument/result

     // types must be a possible instance of the formal map argument/result types

     private struct Constraint {

-      public readonly TypeSeq/*!*/ Arguments;

+      public readonly List<Type>/*!*/ Arguments;

       public readonly Type/*!*/ Result;

       [ContractInvariantMethod]

       void ObjectInvariant() {

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

 

 

-      public Constraint(TypeSeq arguments, Type result) {

+      public Constraint(List<Type> arguments, Type result) {

         Contract.Requires(result != null);

         Contract.Requires(arguments != null);

         Arguments = arguments;

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

       public Constraint Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {

         Contract.Requires(cce.NonNullDictionaryAndValues(varMap));

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

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

         foreach (Type/*!*/ t in Arguments) {

           Contract.Assert(t != null);

           args.Add(t.Clone(varMap));

@@ -2379,7 +2379,7 @@ Contract.Requires(that != null);
       Contract.Assert(f == null);  // no other types should occur as specialisations of this proxy

 

       // otherwise, we just record the constraints given by this usage of the map type

-      TypeSeq/*!*/ arguments = new TypeSeq();

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

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

         Contract.Assert(e != null);

         arguments.Add(e.Type);

@@ -2388,7 +2388,7 @@ Contract.Requires(that != null);
       Contract.Assert(result != null);

       AddConstraint(new Constraint(arguments, result));

 

-      TypeSeq/*!*/ argumentsResult = new TypeSeq();

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

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

         Contract.Assert(e != null);

         argumentsResult.Add(e.Type);

@@ -2551,7 +2551,7 @@ Contract.Requires(that != null);
   public class TypeSynonymAnnotation : Type {

     public Type/*!*/ ExpandedType;

 

-    public readonly TypeSeq/*!*/ Arguments;

+    public readonly List<Type>/*!*/ Arguments;

     // is set during resolution and determines whether the right number of arguments is given

     public readonly TypeSynonymDecl/*!*/ Decl;

     [ContractInvariantMethod]

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

 

 

-    public TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, TypeSeq/*!*/ arguments)

+    public TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, List<Type>/*!*/ arguments)

       : base(token) {

       Contract.Requires(token != null);

       Contract.Requires(decl != null);

@@ -2581,7 +2581,7 @@ Contract.Requires(that != null);
       ExpandedType = decl.Body.Substitute(subst);

     }

 

-    private TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, TypeSeq/*!*/ arguments,

+    private TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, List<Type>/*!*/ arguments,

                                   Type/*!*/ expandedType)

       : base(token) {

       Contract.Requires(token != null);

@@ -2602,7 +2602,7 @@ Contract.Requires(that != null);
     public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {

       //Contract.Requires(cce.NonNullElements(varMap));

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

-      TypeSeq/*!*/ newArgs = new TypeSeq();

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

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         newArgs.Add(t.Clone(varMap));

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

     public override Type CloneUnresolved() {

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

-      TypeSeq/*!*/ newArgs = new TypeSeq();

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

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         newArgs.Add(t.CloneUnresolved());

@@ -2672,7 +2672,7 @@ Contract.Requires(that != null);
       Contract.Ensures(Contract.Result<Type>() != null);

       if (subst.Count == 0)

         return this;

-      TypeSeq newArgs = new TypeSeq();

+      List<Type> newArgs = new List<Type>();

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         newArgs.Add(t.Substitute(subst));

@@ -2703,7 +2703,7 @@ Contract.Requires(that != null);
     public override Type ResolveType(ResolutionContext rc) {

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

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

-      TypeSeq resolvedArgs = new TypeSeq();

+      List<Type> resolvedArgs = new List<Type>();

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         resolvedArgs.Add(t.ResolveType(rc));

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

 

   public class CtorType : Type {

-    public readonly TypeSeq/*!*/ Arguments;

+    public readonly List<Type>/*!*/ Arguments;

     // is set during resolution and determines whether the right number of arguments is given

     public readonly TypeCtorDecl/*!*/ Decl;

     [ContractInvariantMethod]

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

 

 

-    public CtorType(IToken/*!*/ token, TypeCtorDecl/*!*/ decl, TypeSeq/*!*/ arguments)

+    public CtorType(IToken/*!*/ token, TypeCtorDecl/*!*/ decl, List<Type>/*!*/ arguments)

       : base(token) {

       Contract.Requires(token != null);

       Contract.Requires(decl != null);

@@ -2848,7 +2848,7 @@ Contract.Requires(that != null);
     public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {

       //Contract.Requires(cce.NonNullElements(varMap));

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

-      TypeSeq/*!*/ newArgs = new TypeSeq();

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

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         newArgs.Add(t.Clone(varMap));

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

     public override Type CloneUnresolved() {

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

-      TypeSeq/*!*/ newArgs = new TypeSeq();

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

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         newArgs.Add(t.CloneUnresolved());

@@ -2950,7 +2950,7 @@ Contract.Requires(that != null);
       Contract.Ensures(Contract.Result<Type>() != null);

       if (subst.Count == 0)

         return this;

-      TypeSeq newArgs = new TypeSeq();

+      List<Type> newArgs = new List<Type>();

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         newArgs.Add(t.Substitute(subst));

@@ -2979,7 +2979,7 @@ Contract.Requires(that != null);
       EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength);

     }

 

-    internal static void EmitCtorType(string name, TypeSeq args, TokenTextWriter stream, int contextBindingStrength) {

+    internal static void EmitCtorType(string name, List<Type> args, TokenTextWriter stream, int contextBindingStrength) {

       Contract.Requires(stream != null);

       Contract.Requires(args != null);

       Contract.Requires(name != null);

@@ -3007,7 +3007,7 @@ Contract.Requires(that != null);
     public override Type ResolveType(ResolutionContext rc) {

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

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

-      TypeSeq resolvedArgs = new TypeSeq();

+      List<Type> resolvedArgs = new List<Type>();

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         resolvedArgs.Add(t.ResolveType(rc));

@@ -3063,7 +3063,7 @@ Contract.Requires(that != null);
     // an invariant is that each of the type parameters has to occur as

     // free variable in at least one of the arguments

     public readonly TypeVariableSeq/*!*/ TypeParameters;

-    public readonly TypeSeq/*!*/ Arguments;

+    public readonly List<Type>/*!*/ Arguments;

     public Type/*!*/ Result;

     [ContractInvariantMethod]

     void ObjectInvariant() {

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

 

 

-    public MapType(IToken/*!*/ token, TypeVariableSeq/*!*/ typeParameters, TypeSeq/*!*/ arguments, Type/*!*/ result)

+    public MapType(IToken/*!*/ token, TypeVariableSeq/*!*/ typeParameters, List<Type>/*!*/ arguments, Type/*!*/ result)

       : base(token) {

       Contract.Requires(token != null);

       Contract.Requires(typeParameters != null);

@@ -3110,7 +3110,7 @@ Contract.Requires(that != null);
         newTypeParams.Add(newVar);

       }

 

-      TypeSeq/*!*/ newArgs = new TypeSeq();

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

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         newArgs.Add(t.Clone(newVarMap));

@@ -3131,7 +3131,7 @@ Contract.Requires(that != null);
         newTypeParams.Add(newVar);

       }

 

-      TypeSeq/*!*/ newArgs = new TypeSeq();

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

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         newArgs.Add(t.CloneUnresolved());

@@ -3342,7 +3342,7 @@ Contract.Assert(var != null);
         return newType.Substitute(subst);

       }

 

-      TypeSeq newArgs = new TypeSeq();

+      List<Type> newArgs = new List<Type>();

       foreach (Type/*!*/ t in Arguments) {

         Contract.Assert(t != null);

         newArgs.Add(t.Substitute(subst));

@@ -3410,7 +3410,7 @@ Contract.Assert(var != null);
           rc.AddTypeBinder(v);

         }

 

-        TypeSeq resolvedArgs = new TypeSeq();

+        List<Type> resolvedArgs = new List<Type>();

         foreach (Type/*!*/ ty in Arguments) {

           Contract.Assert(ty != null);

           resolvedArgs.Add(ty.ResolveType(rc));

@@ -3419,7 +3419,7 @@ Contract.Assert(var != null);
         Type resolvedResult = Result.ResolveType(rc);

 

         CheckBoundVariableOccurrences(TypeParameters,

-                                      resolvedArgs, new TypeSeq(resolvedResult),

+                                      resolvedArgs, new List<Type> { resolvedResult },

                                       this.tok, "map arguments",

                                       rc);

 

@@ -3492,9 +3492,9 @@ Contract.Assert(var != null);
       Contract.Requires(tc != null);

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

       List<Type/*!*/>/*!*/ actualTypeParams;

-      TypeSeq actualResult =

+      List<Type> actualResult =

         Type.CheckArgumentTypes(TypeParameters, out actualTypeParams, Arguments, actualArgs,

-                                new TypeSeq(Result), null, typeCheckingSubject, opName, tc);

+                                new List<Type> { Result }, null, typeCheckingSubject, opName, tc);

       if (actualResult == null) {

         tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

         return null;

@@ -3630,7 +3630,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
 

     // the argument and result type of this particular usage of the map

     // type. these are necessary to derive the values of the type parameters

-    private readonly TypeSeq/*!*/ ArgumentsResult;

+    private readonly List<Type>/*!*/ ArgumentsResult;

 

     // field that is initialised once all necessary information is available

     // (the MapTypeProxy is instantiated to an actual type) and the instantiation

@@ -3645,7 +3645,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
 

 

     public MapTypeProxyParamInstantiation(MapTypeProxy/*!*/ proxy,

-                                          TypeSeq/*!*/ argumentsResult) {

+                                          List<Type>/*!*/ argumentsResult) {

       Contract.Requires(proxy != null);

       Contract.Requires(argumentsResult != null);

       this.Proxy = proxy;

@@ -3672,7 +3672,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
         if (Instantiations == null) {

           MapType realType = Proxy.ProxyFor as MapType;

           Contract.Assert(realType != null);

-          TypeSeq/*!*/ formalArgs = new TypeSeq();

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

           foreach (Type/*!*/ t in realType.Arguments) {

             Contract.Assert(t != null);

             formalArgs.Add(t);

diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs
index 8b35ffcb..0bd3123b 100644
--- a/Source/Core/BitvectorAnalysis.cs
+++ b/Source/Core/BitvectorAnalysis.cs
@@ -125,7 +125,7 @@ namespace Microsoft.Boogie {
       else {

         MapDisjointSet mapDisjointSet = disjointSet as MapDisjointSet;

         Debug.Assert(mapDisjointSet != null);

-        TypeSeq newArguments = new TypeSeq();

+        List<Type> newArguments = new List<Type>();

         Type result = NewType(mapType.Result, mapDisjointSet.Result);

         bool newTypeNeeded = (result != mapType.Result);

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

@@ -528,7 +528,7 @@ namespace Microsoft.Boogie {
       DiscoverIntAndBv32Functions(program);

 

       BvType bv32Type = new BvType(32);

-      VariableSeq bv32In = new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv32Type), true));

+      List<Variable> bv32In = new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv32Type), true));

       Formal bv32Out = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out", bv32Type), false);

       bv32Id = new Function(Token.NoToken, "bv32Id", bv32In, bv32Out);

       bv32Id.Body = new IdentifierExpr(Token.NoToken, bv32In[0]);

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 219cb3e6..4b20e4a7 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -159,7 +159,7 @@ PRODUCTIONS
 

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

 BoogiePL

-= (. VariableSeq/*!*/ vs;

+= (. List<Variable>/*!*/ vs;

      List<Declaration>/*!*/ ds;

      Axiom/*!*/ ax;

      List<Declaration/*!*/>/*!*/ ts;

@@ -199,11 +199,11 @@ BoogiePL
   .

 

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

-GlobalVars<out VariableSeq/*!*/ ds>

+GlobalVars<out List<Variable>/*!*/ ds>

 = (.

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

     QKeyValue kv = null;

-    ds = new VariableSeq();

+    ds = new List<Variable>();

     var dsx = ds;

   .)

   "var"

@@ -211,7 +211,7 @@ GlobalVars<out VariableSeq/*!*/ ds>
   IdsTypeWheres<true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } > ";"

   .

 

-LocalVars<VariableSeq/*!*/ ds>

+LocalVars<List<Variable>/*!*/ ds>

 = (.

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

     QKeyValue kv = null;

@@ -221,9 +221,9 @@ LocalVars<VariableSeq/*!*/ ds>
   IdsTypeWheres<true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } > ";"

   .

 

-ProcFormals<bool incoming, bool allowWhereClauses, out VariableSeq/*!*/ ds>

+ProcFormals<bool incoming, bool allowWhereClauses, out List<Variable>/*!*/ ds>

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

-     ds = new VariableSeq();

+     ds = new List<Variable>();

      var dsx = ds;

      var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals";

   .)

@@ -233,12 +233,12 @@ ProcFormals<bool incoming, bool allowWhereClauses, out VariableSeq/*!*/ ds>
   ")"

   .

 

-BoundVars<IToken/*!*/ x, out VariableSeq/*!*/ ds>

+BoundVars<IToken/*!*/ x, out List<Variable>/*!*/ ds>

 = (.

     Contract.Requires(x != null);

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

     List<TypedIdent>/*!*/ tyds = new List<TypedIdent>();

-    ds = new VariableSeq();

+    ds = new List<Variable>();

     var dsx = ds;

   .)

   AttrsIdsTypeWheres<true, false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } >

@@ -305,20 +305,20 @@ Type<out Bpl.Type/*!*/ ty>
   (

     TypeAtom<out ty>

   |

-    Ident<out tok>       (. TypeSeq/*!*/ args = new TypeSeq (); .)

+    Ident<out tok>       (. List<Type>/*!*/ args = new List<Type> (); .)

     [ TypeArgs<args> ]   (. ty = new UnresolvedTypeIdentifier (tok, tok.val, args); .)

   |

     MapType<out ty>

   )

   .

 

-TypeArgs<TypeSeq/*!*/ ts>

+TypeArgs<List<Type>/*!*/ ts>

 = (.Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; .)

   (

     TypeAtom<out ty>     (. ts.Add(ty); .)

     [ TypeArgs<ts> ]

   |

-    Ident<out tok>       (. TypeSeq/*!*/ args = new TypeSeq ();

+    Ident<out tok>       (. List<Type>/*!*/ args = new List<Type> ();

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

     [ TypeArgs<ts> ]

   |

@@ -342,7 +342,7 @@ TypeAtom<out Bpl.Type/*!*/ ty>
 MapType<out Bpl.Type/*!*/ ty>

 = (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null;

      IToken/*!*/ nnTok;

-     TypeSeq/*!*/ arguments = new TypeSeq();

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

      Bpl.Type/*!*/ result;

      TypeVariableSeq/*!*/ typeParameters = new TypeVariableSeq();

    .)

@@ -369,7 +369,7 @@ TypeParams<out IToken/*!*/ tok, out Bpl.TypeVariableSeq/*!*/ typeParams>
    .)

   .

 

-Types<TypeSeq/*!*/ ts>

+Types<List<Type>/*!*/ ts>

 = (. Contract.Requires(ts != null); Bpl.Type/*!*/ ty; .)

   Type<out ty>                 (. ts.Add(ty); .)

   { "," Type<out ty>           (. ts.Add(ty); .)

@@ -378,9 +378,9 @@ Types<TypeSeq/*!*/ ts>
 

 

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

-Consts<out VariableSeq/*!*/ ds>

+Consts<out List<Variable>/*!*/ ds>

 = (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; List<TypedIdent>/*!*/ xs;

-     ds = new VariableSeq();

+     ds = new List<Variable>();

      bool u = false; QKeyValue kv = null;

      bool ChildrenComplete = false;

      List<ConstantParent/*!*/> Parents = null; .)

@@ -444,7 +444,7 @@ Function<out List<Declaration>/*!*/ ds>
      ds = new List<Declaration>(); IToken/*!*/ z;

      IToken/*!*/ typeParamTok;

      var typeParams = new TypeVariableSeq();

-     var arguments = new VariableSeq();

+     var arguments = new List<Variable>();

      TypedIdent/*!*/ tyd;

      TypedIdent retTyd = null;

      Bpl.Type/*!*/ retTy;

@@ -587,12 +587,12 @@ UserDefinedType<out Declaration/*!*/ decl, QKeyValue kv>
 Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>

 = (. Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;

      TypeVariableSeq/*!*/ typeParams;

-     VariableSeq/*!*/ ins, outs;

+     List<Variable>/*!*/ ins, outs;

      List<Requires>/*!*/ pre = new List<Requires>();

-     IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();

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

      List<Ensures>/*!*/ post = new List<Ensures>();

 

-     VariableSeq/*!*/ locals = new VariableSeq();

+     List<Variable>/*!*/ locals = new List<Variable>();

      StmtList/*!*/ stmtList;

      QKeyValue kv = null;

      impl = null;

@@ -616,8 +616,8 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>
 Implementation<out Implementation/*!*/ impl>

 = (. Contract.Ensures(Contract.ValueAtReturn(out impl) != null); IToken/*!*/ x;

      TypeVariableSeq/*!*/ typeParams;

-     VariableSeq/*!*/ ins, outs;

-     VariableSeq/*!*/ locals;

+     List<Variable>/*!*/ ins, outs;

+     List<Variable>/*!*/ locals;

      StmtList/*!*/ stmtList;

      QKeyValue kv;

   .)

@@ -630,10 +630,10 @@ Implementation<out Implementation/*!*/ impl>
 

 

 ProcSignature<bool allowWhereClausesOnFormals, out IToken/*!*/ name, out TypeVariableSeq/*!*/ typeParams,

-              out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv>

+              out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv>

 = (. Contract.Ensures(Contract.ValueAtReturn(out name) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ins) != null); Contract.Ensures(Contract.ValueAtReturn(out outs) != null);

      IToken/*!*/ typeParamTok; typeParams = new TypeVariableSeq();

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

+     outs = new List<Variable>(); kv = null; .)

   { Attribute<ref kv> }

   Ident<out name>

   [ TypeParams<out typeParamTok, out typeParams> ]

@@ -642,7 +642,7 @@ ProcSignature<bool allowWhereClausesOnFormals, out IToken/*!*/ name, out TypeVar
   .

 

 

-Spec<List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post>

+Spec<List<Requires>/*!*/ pre, List<IdentifierExpr>/*!*/ mods, List<Ensures>/*!*/ post>

 = (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List<IToken>/*!*/ ms; .)

   ( "modifies"

     [ Idents<out ms>        (. foreach(IToken/*!*/ m in ms){

@@ -669,8 +669,8 @@ SpecPrePost<bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post>
 

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

 

-ImplBody<out VariableSeq/*!*/ locals, out StmtList/*!*/ stmtList>

-= (. Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new VariableSeq(); .)

+ImplBody<out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList>

+= (. Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List<Variable>(); .)

   "{"

   { LocalVars<locals> }

   StmtList<out stmtList>

@@ -841,7 +841,7 @@ LabelOrCmd<out Cmd c, out IToken label>
 /* ensures (c == null) != (label != null) */

 = (. IToken/*!*/ x; Expr/*!*/ e;

      List<IToken>/*!*/ xs;

-     IdentifierExprSeq ids;

+     List<IdentifierExpr> ids;

      c = dummyCmd;  label = null;

      Cmd/*!*/ cn;

      QKeyValue kv = null;

@@ -856,7 +856,7 @@ LabelOrCmd<out Cmd c, out IToken label>
     Proposition<out e>    (. c = new AssumeCmd(x, e, kv); .)

     ";"

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

-    Idents<out xs> ";"    (. ids = new IdentifierExprSeq();

+    Idents<out xs> ";"    (. ids = new List<IdentifierExpr>();

                              foreach(IToken/*!*/ y in xs){

                                Contract.Assert(y != null);

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

@@ -1238,12 +1238,12 @@ 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;  VariableSeq/*!*/ ds;  Trigger trig;

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

      TypeVariableSeq/*!*/ typeParams;

      IdentifierExpr/*!*/ id;

      QKeyValue kv;

      e = dummyExpr;

-     VariableSeq/*!*/ locals;

+     List<Variable>/*!*/ locals;

      List<Block/*!*/>/*!*/ blocks;

   .)

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

@@ -1299,8 +1299,8 @@ AtomExpression<out Expr/*!*/ e>
   )

   .

 

-CodeExpression<.out VariableSeq/*!*/ locals, out List<Block/*!*/>/*!*/ blocks.>

-= (. Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new VariableSeq(); Block/*!*/ b;

+CodeExpression<.out List<Variable>/*!*/ locals, out List<Block/*!*/>/*!*/ blocks.>

+= (. Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List<Variable>(); Block/*!*/ b;

      blocks = new List<Block/*!*/>();

   .)

   "|{"

@@ -1412,13 +1412,13 @@ IfThenElseExpression<out Expr/*!*/ e>
   .

 

 

-QuantifierBody<IToken/*!*/ q, out TypeVariableSeq/*!*/ typeParams, out VariableSeq/*!*/ ds,

+QuantifierBody<IToken/*!*/ q, out TypeVariableSeq/*!*/ typeParams, out List<Variable>/*!*/ ds,

                out QKeyValue kv, out Trigger trig, out Expr/*!*/ body>

 = (. Contract.Requires(q != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ds) != null); Contract.Ensures(Contract.ValueAtReturn(out body) != null);

      trig = null; typeParams = new TypeVariableSeq ();

      IToken/*!*/ tok;

      kv = null;

-     ds = new VariableSeq ();

+     ds = new List<Variable> ();

   .)

   (

      TypeParams<out tok, out typeParams>

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index e1da4dd6..62dfa03f 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -25,7 +25,7 @@ namespace Microsoft.Boogie {
       Implementation/*!*/ impl = base.VisitImplementation(node);

       Contract.Assert(impl != null);

       //Console.WriteLine("Old number of local variables = {0}", impl.LocVars.Length);

-      Microsoft.Boogie.VariableSeq/*!*/ vars = new Microsoft.Boogie.VariableSeq();

+      List<Variable>/*!*/ vars = new List<Variable>();

       foreach (Variable/*!*/ var in impl.LocVars) {

         Contract.Assert(var != null);

         if (usedVars.Contains(var))

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

       foreach (Procedure x in modSets.Keys)

       {

-          x.Modifies = new IdentifierExprSeq();

+          x.Modifies = new List<IdentifierExpr>();

           foreach (Variable v in modSets[x])

           {

               x.Modifies.Add(new IdentifierExpr(v.tok, v));

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

       return base.VisitIdentifierExpr((IdentifierExpr)node.Clone());

     }

-    public override IdentifierExprSeq VisitIdentifierExprSeq(IdentifierExprSeq identifierExprSeq) {

+    public override List<IdentifierExpr> VisitIdentifierExprSeq(List<IdentifierExpr> identifierExprSeq) {

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

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

-      return base.VisitIdentifierExprSeq(new IdentifierExprSeq(identifierExprSeq));

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

+      return base.VisitIdentifierExprSeq(new List<IdentifierExpr>(identifierExprSeq));

     }

     public override Implementation VisitImplementation(Implementation node) {

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

@@ -318,10 +318,10 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Variable>() != null);

       return node;

     }

-    public override VariableSeq VisitVariableSeq(VariableSeq variableSeq) {

+    public override List<Variable> VisitVariableSeq(List<Variable> variableSeq) {

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

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

-      return base.VisitVariableSeq(new VariableSeq(variableSeq));

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

+      return base.VisitVariableSeq(new List<Variable>(variableSeq));

     }

     public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {

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

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 5263fd1f..07c44bac 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -79,13 +79,13 @@ namespace Microsoft.Boogie {
       Contract.Requires(program != null);

       Contract.Requires(impl.Proc != null);

 

-      VariableSeq/*!*/ newInParams = new VariableSeq(impl.InParams);

+      List<Variable>/*!*/ newInParams = new List<Variable>(impl.InParams);

       Contract.Assert(newInParams != null);

-      VariableSeq/*!*/ newOutParams = new VariableSeq(impl.OutParams);

+      List<Variable>/*!*/ newOutParams = new List<Variable>(impl.OutParams);

       Contract.Assert(newOutParams != null);

-      VariableSeq/*!*/ newLocalVars = new VariableSeq(impl.LocVars);

+      List<Variable>/*!*/ newLocalVars = new List<Variable>(impl.LocVars);

       Contract.Assert(newLocalVars != null);

-      IdentifierExprSeq/*!*/ newModifies = new IdentifierExprSeq(impl.Proc.Modifies);

+      List<IdentifierExpr>/*!*/ newModifies = new List<IdentifierExpr>(impl.Proc.Modifies);

       Contract.Assert(newModifies != null);

 

       bool inlined = false;

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

 

     protected virtual List<Block/*!*/>/*!*/ DoInlineBlocks(List<Block/*!*/>/*!*/ blocks, Program/*!*/ program,

-                                                 VariableSeq/*!*/ newLocalVars, IdentifierExprSeq/*!*/ newModifies, 

+                                                 List<Variable>/*!*/ newLocalVars, List<IdentifierExpr>/*!*/ newModifies, 

                                                  ref bool inlinedSomething) {

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

       Contract.Requires(program != null);

@@ -322,7 +322,7 @@ namespace Microsoft.Boogie {
       return newBlocks;

     }

 

-    protected void BeginInline(VariableSeq newLocalVars, IdentifierExprSeq newModifies, Implementation impl) {

+    protected void BeginInline(List<Variable> newLocalVars, List<IdentifierExpr> newModifies, Implementation impl) {

       Contract.Requires(impl != null);

       Contract.Requires(impl.Proc != null);

       Contract.Requires(newModifies != null);

@@ -458,10 +458,10 @@ namespace Microsoft.Boogie {
         inCmds.Add(InlinedRequires(callCmd, req));

       }

 

-      VariableSeq locVars = cce.NonNull(impl.OriginalLocVars);

+      List<Variable> locVars = cce.NonNull(impl.OriginalLocVars);

 

       // havoc locals and out parameters in case procedure is invoked in a loop

-      IdentifierExprSeq havocVars = new IdentifierExprSeq();

+      List<IdentifierExpr> havocVars = new List<IdentifierExpr>();

       foreach (Variable v in locVars)

       {

           havocVars.Add((IdentifierExpr)codeCopier.Subst(v));

diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
index 6874f1c9..ede25c0e 100644
--- a/Source/Core/LambdaHelper.cs
+++ b/Source/Core/LambdaHelper.cs
@@ -96,10 +96,10 @@ namespace Microsoft.Boogie {
           lambda.ComputeFreeVariables(freeVars);

           // this is ugly, the output will depend on hashing order

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

-          VariableSeq formals = new VariableSeq();

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

           ExprSeq callArgs = new ExprSeq();

           ExprSeq axCallArgs = new ExprSeq();

-          VariableSeq dummies = new VariableSeq(lambda.Dummies);

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

           TypeVariableSeq freeTypeVars = new TypeVariableSeq();

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

           TypeVariableSeq freshTypeVars = new TypeVariableSeq();  // these are only used in the lambda@n function's definition

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index a20d8ce9..8d0faf2b 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -400,7 +400,7 @@ namespace Microsoft.Boogie
                 foreach (string domainName in linearDomains.Keys)

                 {

                     var domain = linearDomains[domainName];

-                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(domain.elementType), Type.Bool)), true);

+                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);

                     impl.InParams.Add(f);

                     domainNameToInputVar[domainName] = f;

                 }

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

                     proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInputScope[domainName])));

                     var domain = linearDomains[domainName];

-                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(domain.elementType), Type.Bool)), true);

+                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);

                     proc.InParams.Add(f);

                     domainNameToOutputScope[domainName].Add(f);

                     proc.Ensures.Add(new Ensures(true, DisjointnessExpr(domainName, domainNameToOutputScope[domainName])));

@@ -568,7 +568,7 @@ namespace Microsoft.Boogie
         public Expr DisjointnessExpr(string domainName, HashSet<Variable> scope)

         {

             LinearDomain domain = linearDomains[domainName];

-            BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(domain.elementType), Microsoft.Boogie.Type.Int)));

+            BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Microsoft.Boogie.Type.Int)));

             Expr disjointExpr = Expr.True;

             int count = 0;

             foreach (Variable v in scope)

@@ -580,7 +580,7 @@ namespace Microsoft.Boogie
                 e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.True)));

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

             }

-            return new ExistsExpr(Token.NoToken, new VariableSeq(partition), disjointExpr);

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

         }

     }

 

@@ -599,10 +599,10 @@ namespace Microsoft.Boogie
             this.elementType = elementType;

             this.axioms = new List<Axiom>();

 

-            MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Bool);

-            MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Int);

+            MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(this.elementType), Type.Bool);

+            MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(this.elementType), Type.Int);

             this.mapOrBool = new Function(Token.NoToken, domainName + "_linear_MapOr",

-                                          new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),

+                                          new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),

                                                           new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),

                                           new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));

             if (CommandLineOptions.Clo.UseArrayTheory)

@@ -622,15 +622,15 @@ namespace Microsoft.Boogie
                 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)));

-                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new VariableSeq(a, b), null, 

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

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

-                                               new ForallExpr(Token.NoToken, new VariableSeq(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

+                                               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));

             }

 

             this.mapImpBool = new Function(Token.NoToken, domainName + "_linear_MapImp",

-                                              new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),

+                                              new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),

                                                               new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),

                                               new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));

             if (CommandLineOptions.Clo.UseArrayTheory)

@@ -650,15 +650,15 @@ namespace Microsoft.Boogie
                 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)));

-                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new VariableSeq(a, b), null,

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

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

-                                               new ForallExpr(Token.NoToken, new VariableSeq(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

+                                               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));

             }

 

             this.mapConstBool = new Function(Token.NoToken, domainName + "_linear_MapConstBool",

-                                              new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true)),

+                                              new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true)),

                                               new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));

             if (CommandLineOptions.Clo.UseArrayTheory)

             {

@@ -670,18 +670,18 @@ namespace Microsoft.Boogie
                 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));

-                var trueAxiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(x), trueTerm);

+                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)); 

-                var falseAxiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(x), Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm));

+                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));

             }

 

             this.mapEqInt = new Function(Token.NoToken, domainName + "_linear_MapEq",

-                                              new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true),

+                                              new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true),

                                                               new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt), true)),

                                               new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));

             if (CommandLineOptions.Clo.UseArrayTheory)

@@ -701,15 +701,15 @@ namespace Microsoft.Boogie
                 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)));

-                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new VariableSeq(a, b), null, 

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

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

-                                               new ForallExpr(Token.NoToken, new VariableSeq(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

+                                               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));

             }

 

             this.mapConstInt = new Function(Token.NoToken, domainName + "_linear_MapConstInt",

-                                          new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true)),

+                                          new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true)),

                                           new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeInt), false));

             if (CommandLineOptions.Clo.UseArrayTheory)

             {

@@ -722,7 +722,7 @@ namespace Microsoft.Boogie
                 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 axiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(a, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie));

+                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 bee34156..2df7b3ba 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -143,7 +143,7 @@ namespace Microsoft.Boogie
     public class OwickiGriesTransform

     {

         Dictionary<string, ProcedureInfo> procNameToInfo;

-        IdentifierExprSeq globalMods;

+        List<IdentifierExpr> globalMods;

         LinearTypechecker linearTypechecker;

         Dictionary<string, Procedure> asyncAndParallelCallDesugarings;

         List<Procedure> yieldCheckerProcs;

@@ -156,7 +156,7 @@ namespace Microsoft.Boogie
             Program program = linearTypechecker.program;

             procNameToInfo = AsyncAndYieldTraverser.Traverse(program);

             AtomicTraverser.Traverse(program, procNameToInfo);

-            globalMods = new IdentifierExprSeq();

+            globalMods = new List<IdentifierExpr>();

             foreach (Variable g in program.GlobalVariables())

             {

                 globalMods.Add(new IdentifierExpr(Token.NoToken, g));

@@ -164,11 +164,11 @@ namespace Microsoft.Boogie
             asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();

             yieldCheckerProcs = new List<Procedure>();

             yieldCheckerImpls = new List<Implementation>();

-            VariableSeq inputs = new VariableSeq();

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

             foreach (string domainName in linearTypechecker.linearDomains.Keys)

             {

                 var domain = linearTypechecker.linearDomains[domainName];

-                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(domain.elementType), Type.Bool)), true);

+                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);

                 inputs.Add(f);

             }

             foreach (IdentifierExpr ie in globalMods)

@@ -176,7 +176,7 @@ namespace Microsoft.Boogie
                 Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);

                 inputs.Add(f);

             }

-            yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new VariableSeq(), new List<Requires>(), new IdentifierExprSeq(), new List<Ensures>());

+            yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

             yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

         }

 

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

                 exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));

             } 

-            CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new IdentifierExprSeq());

+            CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());

             yieldCallCmd.Proc = yieldProc;

             newCmds.Add(yieldCallCmd);

         }

@@ -273,11 +273,11 @@ namespace Microsoft.Boogie
             if (asyncAndParallelCallDesugarings.ContainsKey(procName))

                 return asyncAndParallelCallDesugarings[procName];

 

-            VariableSeq inParams = new VariableSeq();

-            VariableSeq outParams = new VariableSeq();

+            List<Variable> inParams = new List<Variable>();

+            List<Variable> outParams = new List<Variable>();

             List<Requires> requiresSeq = new List<Requires>();

             List<Ensures> ensuresSeq = new List<Ensures>();

-            IdentifierExprSeq ieSeq = new IdentifierExprSeq();

+            List<IdentifierExpr> ieSeq = new List<IdentifierExpr>();

             int count = 0;

             while (callCmd != null)

             {

@@ -323,8 +323,8 @@ namespace Microsoft.Boogie
 

             Program program = linearTypechecker.program;

             ProcedureInfo info = procNameToInfo[decl.Name];

-            VariableSeq locals = new VariableSeq();

-            VariableSeq inputs = new VariableSeq();

+            List<Variable> locals = new List<Variable>();

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

             foreach (IdentifierExpr ie in map.Values)

             {

                 locals.Add(ie.Decl);

@@ -406,12 +406,12 @@ namespace Microsoft.Boogie
 

             // Create the yield checker procedure

             var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name);

-            var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), new List<Requires>(), new IdentifierExprSeq(), new List<Ensures>());

+            var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

             yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

             yieldCheckerProcs.Add(yieldCheckerProc);

 

             // Create the yield checker implementation

-            var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), locals, yieldCheckerBlocks);

+            var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new List<Variable>(), locals, yieldCheckerBlocks);

             yieldCheckerImpl.Proc = yieldCheckerProc;

             yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

             yieldCheckerImpls.Add(yieldCheckerImpl);

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

                             if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))

                             {

-                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new IdentifierExprSeq(), new List<Ensures>());

+                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());

                             }

                             var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];

                             CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);

@@ -723,11 +723,11 @@ namespace Microsoft.Boogie
         private void AddYieldProcAndImpl() 

         {

             Program program = linearTypechecker.program;

-            VariableSeq inputs = new VariableSeq();

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

             foreach (string domainName in linearTypechecker.linearDomains.Keys)

             {

                 var domain = linearTypechecker.linearDomains[domainName];

-                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(domain.elementType), Type.Bool)), true);

+                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);

                 inputs.Add(f);

             }

             foreach (IdentifierExpr ie in globalMods)

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

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

                     }

-                    CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new IdentifierExprSeq());

+                    CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List<IdentifierExpr>());

                     callCmd.Proc = proc;

                     string label = string.Format("L_{0}", labelCount++);

                     Block block = new Block(Token.NoToken, label, new CmdSeq(callCmd), new ReturnCmd(Token.NoToken));

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

             blocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), transferCmd));

             

-            var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new TypeVariableSeq(), inputs, new VariableSeq(), new VariableSeq(), blocks);

+            var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new TypeVariableSeq(), inputs, new List<Variable>(), new List<Variable>(), blocks);

             yieldImpl.Proc = yieldProc;

             yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

             program.TopLevelDeclarations.Add(yieldProc);

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 44d56045..b0ce346a 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -207,7 +207,7 @@ private class BvBounds : Expr {
 

 

 	void BoogiePL() {

-		VariableSeq/*!*/ vs;

+		List<Variable>/*!*/ vs;

 		List<Declaration>/*!*/ ds;

 		Axiom/*!*/ ax;

 		List<Declaration/*!*/>/*!*/ ts;

@@ -277,9 +277,9 @@ private class BvBounds : Expr {
 		Expect(0);

 	}

 

-	void Consts(out VariableSeq/*!*/ ds) {

+	void Consts(out List<Variable>/*!*/ ds) {

 		Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; List<TypedIdent>/*!*/ xs;

-		ds = new VariableSeq();

+		ds = new List<Variable>();

 		bool u = false; QKeyValue kv = null;

 		bool ChildrenComplete = false;

 		List<ConstantParent/*!*/> Parents = null; 

@@ -325,7 +325,7 @@ private class BvBounds : Expr {
 		ds = new List<Declaration>(); IToken/*!*/ z;

 		IToken/*!*/ typeParamTok;

 		var typeParams = new TypeVariableSeq();

-		var arguments = new VariableSeq();

+		var arguments = new List<Variable>();

 		TypedIdent/*!*/ tyd;

 		TypedIdent retTyd = null;

 		Bpl.Type/*!*/ retTy;

@@ -452,10 +452,10 @@ private class BvBounds : Expr {
 		Expect(8);

 	}

 

-	void GlobalVars(out VariableSeq/*!*/ ds) {

+	void GlobalVars(out List<Variable>/*!*/ ds) {

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

 		QKeyValue kv = null;

-		ds = new VariableSeq();

+		ds = new List<Variable>();

 		var dsx = ds;

 		

 		Expect(7);

@@ -469,12 +469,12 @@ private class BvBounds : Expr {
 	void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) {

 		Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;

 		TypeVariableSeq/*!*/ typeParams;

-		VariableSeq/*!*/ ins, outs;

+		List<Variable>/*!*/ ins, outs;

 		List<Requires>/*!*/ pre = new List<Requires>();

-		IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();

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

 		List<Ensures>/*!*/ post = new List<Ensures>();

 		

-		VariableSeq/*!*/ locals = new VariableSeq();

+		List<Variable>/*!*/ locals = new List<Variable>();

 		StmtList/*!*/ stmtList;

 		QKeyValue kv = null;

 		impl = null;

@@ -501,8 +501,8 @@ private class BvBounds : Expr {
 	void Implementation(out Implementation/*!*/ impl) {

 		Contract.Ensures(Contract.ValueAtReturn(out impl) != null); IToken/*!*/ x;

 		TypeVariableSeq/*!*/ typeParams;

-		VariableSeq/*!*/ ins, outs;

-		VariableSeq/*!*/ locals;

+		List<Variable>/*!*/ ins, outs;

+		List<Variable>/*!*/ locals;

 		StmtList/*!*/ stmtList;

 		QKeyValue kv;

 		

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

 	}

 

-	void LocalVars(VariableSeq/*!*/ ds) {

+	void LocalVars(List<Variable>/*!*/ ds) {

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

 		QKeyValue kv = null;

 		

@@ -538,9 +538,9 @@ private class BvBounds : Expr {
 		Expect(8);

 	}

 

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

+	void ProcFormals(bool incoming, bool allowWhereClauses, out List<Variable>/*!*/ ds) {

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

-		ds = new VariableSeq();

+		ds = new List<Variable>();

 		var dsx = ds;

 		var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals";

 		

@@ -559,11 +559,11 @@ private class BvBounds : Expr {
 		}

 	}

 

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

+	void BoundVars(IToken/*!*/ x, out List<Variable>/*!*/ ds) {

 		Contract.Requires(x != null);

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

 		List<TypedIdent>/*!*/ tyds = new List<TypedIdent>();

-		ds = new VariableSeq();

+		ds = new List<Variable>();

 		var dsx = ds;

 		

 		AttrsIdsTypeWheres(true, false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } );

@@ -599,7 +599,7 @@ private class BvBounds : Expr {
 			TypeAtom(out ty);

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

 			Ident(out tok);

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

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

 			if (StartOf(6)) {

 				TypeArgs(args);

 			}

@@ -682,7 +682,7 @@ private class BvBounds : Expr {
 		

 	}

 

-	void TypeArgs(TypeSeq/*!*/ ts) {

+	void TypeArgs(List<Type>/*!*/ ts) {

 		Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; 

 		if (StartOf(5)) {

 			TypeAtom(out ty);

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

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

 			Ident(out tok);

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

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

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

 			if (StartOf(6)) {

 				TypeArgs(ts);

@@ -706,7 +706,7 @@ private class BvBounds : Expr {
 	void MapType(out Bpl.Type/*!*/ ty) {

 		Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null;

 		IToken/*!*/ nnTok;

-		TypeSeq/*!*/ arguments = new TypeSeq();

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

 		Bpl.Type/*!*/ result;

 		TypeVariableSeq/*!*/ typeParameters = new TypeVariableSeq();

 		

@@ -738,7 +738,7 @@ private class BvBounds : Expr {
 		

 	}

 

-	void Types(TypeSeq/*!*/ ts) {

+	void Types(List<Type>/*!*/ ts) {

 		Contract.Requires(ts != null); Bpl.Type/*!*/ ty; 

 		Type(out ty);

 		ts.Add(ty); 

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

 

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

-out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {

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

 		Contract.Ensures(Contract.ValueAtReturn(out name) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ins) != null); Contract.Ensures(Contract.ValueAtReturn(out outs) != null);

 		IToken/*!*/ typeParamTok; typeParams = new TypeVariableSeq();

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

+		outs = new List<Variable>(); kv = null; 

 		while (la.kind == 27) {

 			Attribute(ref kv);

 		}

@@ -867,7 +867,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		}

 	}

 

-	void Spec(List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post) {

+	void Spec(List<Requires>/*!*/ pre, List<IdentifierExpr>/*!*/ mods, List<Ensures>/*!*/ post) {

 		Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List<IToken>/*!*/ ms; 

 		if (la.kind == 34) {

 			Get();

@@ -888,8 +888,8 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		} else SynErr(102);

 	}

 

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

-		Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new VariableSeq(); 

+	void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {

+		Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List<Variable>(); 

 		Expect(27);

 		while (la.kind == 7) {

 			LocalVars(locals);

@@ -992,7 +992,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 	void LabelOrCmd(out Cmd c, out IToken label) {

 		IToken/*!*/ x; Expr/*!*/ e;

 		List<IToken>/*!*/ xs;

-		IdentifierExprSeq ids;

+		List<IdentifierExpr> ids;

 		c = dummyCmd;  label = null;

 		Cmd/*!*/ cn;

 		QKeyValue kv = null;

@@ -1029,7 +1029,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 			x = t; 

 			Idents(out xs);

 			Expect(8);

-			ids = new IdentifierExprSeq();

+			ids = new List<IdentifierExpr>();

 			foreach(IToken/*!*/ y in xs){

 			 Contract.Assert(y != null);

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

@@ -1688,12 +1688,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ 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;  VariableSeq/*!*/ ds;  Trigger trig;

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

 		TypeVariableSeq/*!*/ typeParams;

 		IdentifierExpr/*!*/ id;

 		QKeyValue kv;

 		e = dummyExpr;

-		VariableSeq/*!*/ locals;

+		List<Variable>/*!*/ locals;

 		List<Block/*!*/>/*!*/ blocks;

 		

 		switch (la.kind) {

@@ -1850,13 +1850,13 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		} else SynErr(126);

 	}

 

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

+	void QuantifierBody(IToken/*!*/ q, out TypeVariableSeq/*!*/ typeParams, out List<Variable>/*!*/ ds,

 out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {

 		Contract.Requires(q != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ds) != null); Contract.Ensures(Contract.ValueAtReturn(out body) != null);

 		trig = null; typeParams = new TypeVariableSeq ();

 		IToken/*!*/ tok;

 		kv = null;

-		ds = new VariableSeq ();

+		ds = new List<Variable> ();

 		

 		if (la.kind == 19) {

 			TypeParams(out tok, out typeParams);

@@ -1904,8 +1904,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); 

 	}

 

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

-		Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new VariableSeq(); Block/*!*/ b;

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

+		Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List<Variable>(); Block/*!*/ b;

 		blocks = new List<Block/*!*/>();

 		

 		Expect(84);

diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 532093b1..f3a27517 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -556,7 +556,7 @@ namespace Microsoft.Boogie {
   }

 

   public class TypecheckingContext : CheckingContext {

-    public IdentifierExprSeq Frame;  // used in checking the assignment targets of implementation bodies

+    public List<IdentifierExpr> Frame;  // used in checking the assignment targets of implementation bodies

 

     public TypecheckingContext(IErrorSink errorSink)

       : base(errorSink) {

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 8a38d67a..8f5cf64b 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -318,9 +318,9 @@ namespace Microsoft.Boogie {
         node.Decl = this.VisitVariable(node.Decl);

       return node;

     }

-    public virtual IdentifierExprSeq VisitIdentifierExprSeq(IdentifierExprSeq identifierExprSeq) {

+    public virtual List<IdentifierExpr> VisitIdentifierExprSeq(List<IdentifierExpr> identifierExprSeq) {

       Contract.Requires(identifierExprSeq != null);

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

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

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

         identifierExprSeq[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(identifierExprSeq[i]));

       return identifierExprSeq;

@@ -546,9 +546,9 @@ namespace Microsoft.Boogie {
       node.TypedIdent = this.VisitTypedIdent(node.TypedIdent);

       return node;

     }

-    public virtual VariableSeq VisitVariableSeq(VariableSeq variableSeq) {

+    public virtual List<Variable> VisitVariableSeq(List<Variable> variableSeq) {

       Contract.Requires(variableSeq != null);

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

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

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

         variableSeq[i] = this.VisitVariable(cce.NonNull(variableSeq[i]));

       return variableSeq;

diff --git a/Source/Core/TypeAmbiguitySeeker.cs b/Source/Core/TypeAmbiguitySeeker.cs
index d878791b..1293dd1b 100644
--- a/Source/Core/TypeAmbiguitySeeker.cs
+++ b/Source/Core/TypeAmbiguitySeeker.cs
@@ -92,7 +92,7 @@ namespace Microsoft.Boogie {
         return base.VisitMapTypeProxy(node);

 

       TypeVariableSeq/*!*/ typeParams = new TypeVariableSeq();

-      TypeSeq/*!*/ arguments = new TypeSeq();

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

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

         TypeVariable/*!*/ param = new TypeVariable(Token.NoToken, "arg" + i);

         Contract.Assert(param != null);

diff --git a/Source/Doomed/DoomedLoopUnrolling.cs b/Source/Doomed/DoomedLoopUnrolling.cs
index d97d56d0..d7ba6025 100644
--- a/Source/Doomed/DoomedLoopUnrolling.cs
+++ b/Source/Doomed/DoomedLoopUnrolling.cs
@@ -99,7 +99,7 @@ namespace VC
             Contract.Requires(tok != null);

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

 

-            VariableSeq varsToHavoc = new VariableSeq();

+            List<Variable> varsToHavoc = new List<Variable>();

             foreach (Block b in bl)

             {

                 Contract.Assert(b != null);

@@ -109,7 +109,7 @@ namespace VC
                     c.AddAssignedVariables(varsToHavoc);

                 }

             }

-            IdentifierExprSeq havocExprs = new IdentifierExprSeq();

+            List<IdentifierExpr> havocExprs = new List<IdentifierExpr>();

             foreach (Variable v in varsToHavoc)

             {

                 Contract.Assert(v != null);

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 321d4072..192e9a68 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -174,7 +174,7 @@ namespace Microsoft.Boogie.Houdini {
 

                     if (controlVar.InParams.Count != 0)

                     {

-                        term = new ForallExpr(Token.NoToken, new VariableSeq(controlVar.InParams.ToArray()),

+                        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))),

                             term);

                     }

@@ -621,7 +621,7 @@ namespace Microsoft.Boogie.Houdini {
             //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr);

 

             // Create a macro so that the VC can sit with the theorem prover

-            Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false));

+            Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false));

             prover.DefineMacro(macro, vcexpr);

 

             // Store VC

@@ -871,7 +871,7 @@ namespace Microsoft.Boogie.Houdini {
                 collector.VisitExpr(node);

 

                 // Find the outermost bound variables

-                var bound = new VariableSeq();

+                var bound = new List<Variable>();

                 if(boundVars.Count > 0) 

                     bound.AddRange(collector.usedVars.Intersect(boundVars[0].Values));

 

@@ -2126,7 +2126,7 @@ namespace Microsoft.Boogie.Houdini {
                 foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())

                 {

                     var nimpl = new Implementation(Token.NoToken, impl.Name, impl.TypeParameters,

-                        impl.InParams, impl.OutParams, new VariableSeq(impl.LocVars), new List<Block>());

+                        impl.InParams, impl.OutParams, new List<Variable>(impl.LocVars), new List<Block>());

                     foreach (var blk in impl.Blocks)

                     {

                         var cd = new CodeCopier();

@@ -2738,7 +2738,7 @@ namespace Microsoft.Boogie.Houdini {
 

         private void attachEnsures(Implementation impl)

         {

-            VariableSeq functionInterfaceVars = new VariableSeq();

+            List<Variable> functionInterfaceVars = new List<Variable>();

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

             {

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

@@ -2839,7 +2839,7 @@ namespace Microsoft.Boogie.Houdini {
             vcexpr = visitor.Mutate(vcexpr, true);

 

             // Create a macro so that the VC can sit with the theorem prover

-            Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false));

+            Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false));

             prover.DefineMacro(macro, vcexpr);

 

             // Store VC

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index ce46f20b..170b5212 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -163,7 +163,7 @@ namespace Microsoft.Boogie.Houdini {
         conjecture = exprGen.Implies(eqExpr, conjecture);

       }

 

-      Macro macro = new Macro(Token.NoToken, descriptiveName, new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false));

+      Macro macro = new Macro(Token.NoToken, descriptiveName, new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false));

       proverInterface.DefineMacro(macro, conjecture);

       conjecture = exprGen.Function(macro);

 

diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs
index eac60511..c655175a 100644
--- a/Source/Predication/BlockPredicator.cs
+++ b/Source/Predication/BlockPredicator.cs
@@ -108,7 +108,7 @@ public class BlockPredicator {
             new IdentifierExpr(Token.NoToken, havocVar);

         }

         cmdSeq.Add(new HavocCmd(Token.NoToken,

-                                new IdentifierExprSeq(havocTempExpr)));

+                                new List<IdentifierExpr> { havocTempExpr }));

         cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,

                                     new NAryExpr(Token.NoToken,

                                       new IfThenElse(Token.NoToken),

@@ -145,7 +145,7 @@ public class BlockPredicator {
         PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0]));

       } else {

         PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken,

-                                          new IdentifierExprSeq(cur)));

+                                          new List<IdentifierExpr> { cur }));

         PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken,

                targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or)));

       }

@@ -305,7 +305,7 @@ public class BlockPredicator {
                                new TypedIdent(Token.NoToken, "_P",

                                               Microsoft.Boogie.Type.Bool),

                                /*incoming=*/true);

-        dwf.InParams = new VariableSeq(

+        dwf.InParams = new List<Variable>(

           (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))

             .ToArray());

 

diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 9dc10d02..484a866d 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -115,7 +115,7 @@ public class SmartBlockPredicator {
             new IdentifierExpr(Token.NoToken, havocVar);

         }

         cmdSeq.Add(new HavocCmd(Token.NoToken,

-                                new IdentifierExprSeq(havocTempExpr)));

+                                new List<IdentifierExpr>(havocTempExpr)));

         cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,

                                     new NAryExpr(Token.NoToken,

                                       new IfThenElse(Token.NoToken),

@@ -501,7 +501,7 @@ public class SmartBlockPredicator {
                                  new TypedIdent(Token.NoToken, "_P",

                                                 Microsoft.Boogie.Type.Bool),

                                  /*incoming=*/true);

-          dwf.InParams = new VariableSeq(

+          dwf.InParams = new List<Variable>(

             (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))

               .ToArray());

 

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 6509bc30..b3574b94 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -492,7 +492,7 @@ namespace Microsoft.Boogie.VCExprAST {
       return new VCQuantifierInfos(qid, node.SkolemId, false, node.Attributes);

     }

 

-    private string getQidNameFromQKeyValue(VariableSeq vars, QKeyValue attributes) {

+    private string getQidNameFromQKeyValue(List<Variable> vars, QKeyValue attributes) {

       Contract.Requires(vars != null);

       // Check for a 'qid, name' pair in keyvalues

       string qid = QKeyValue.FindStringAttribute(attributes, "qid");

@@ -872,9 +872,9 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

-    public override VariableSeq VisitVariableSeq(VariableSeq variableSeq) {

+    public override List<Variable> VisitVariableSeq(List<Variable> variableSeq) {

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

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

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index e6384e67..f7860169 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -31,7 +31,7 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Requires(Contract.ForAll(0, types.Length, i => types[i] != null));

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

 

-      VariableSeq args = new VariableSeq();

+      List<Variable> args = new List<Variable>();

       for (int i = 0; i < types.Length - 1; ++i)

         args.Add(new Formal(Token.NoToken,

                              new TypedIdent(Token.NoToken, "arg" + i, cce.NonNull(types[i])),

@@ -511,12 +511,12 @@ namespace Microsoft.Boogie.TypeErasure {
 

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

       UDecl = uDecl;

-      Type/*!*/ u = new CtorType(Token.NoToken, uDecl, new TypeSeq());

+      Type/*!*/ u = new CtorType(Token.NoToken, uDecl, new List<Type>());

       U = u;

 

       TypeCtorDecl/*!*/ tDecl = new TypeCtorDecl(Token.NoToken, "T", 0);

       TDecl = tDecl;

-      Type/*!*/ t = new CtorType(Token.NoToken, tDecl, new TypeSeq());

+      Type/*!*/ t = new CtorType(Token.NoToken, tDecl, new List<Type>());

       T = t;

 

       Ctor = HelperFuns.BoogieFunction("Ctor", t, Type.Int);

@@ -940,14 +940,14 @@ namespace Microsoft.Boogie.TypeErasure {
 

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

 

-    public Function Select(MapType rawType, out TypeSeq instantiations) {

+    public Function Select(MapType rawType, out List<Type> instantiations) {

       Contract.Requires((rawType != null));

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

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

       return AbstractAndGetRepresentation(rawType, out instantiations).Select;

     }

 

-    public Function Store(MapType rawType, out TypeSeq instantiations) {

+    public Function Store(MapType rawType, out List<Type> instantiations) {

       Contract.Requires((rawType != null));

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

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

@@ -955,10 +955,10 @@ namespace Microsoft.Boogie.TypeErasure {
     }

 

     private MapTypeClassRepresentation

-            AbstractAndGetRepresentation(MapType rawType, out TypeSeq instantiations) {

+            AbstractAndGetRepresentation(MapType rawType, out List<Type> instantiations) {

       Contract.Requires((rawType != null));

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

-      instantiations = new TypeSeq();

+      instantiations = new List<Type>();

       MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations);

       return GetClassRepresentation(abstraction);

     }

@@ -966,7 +966,7 @@ namespace Microsoft.Boogie.TypeErasure {
     public CtorType AbstractMapType(MapType rawType) {

       Contract.Requires(rawType != null);

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

-      TypeSeq/*!*/ instantiations = new TypeSeq();

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

       MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations);

 

       MapTypeClassRepresentation repr = GetClassRepresentation(abstraction);

@@ -975,11 +975,11 @@ namespace Microsoft.Boogie.TypeErasure {
     }

 

     // TODO: cache the result of this operation

-    protected MapType ThinOutMapType(MapType rawType, TypeSeq instantiations) {

+    protected MapType ThinOutMapType(MapType rawType, List<Type> instantiations) {

       Contract.Requires(instantiations != null);

       Contract.Requires(rawType != null);

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

-      TypeSeq/*!*/ newArguments = new TypeSeq();

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

       foreach (Type/*!*/ subtype in rawType.Arguments) {

         Contract.Assert(subtype != null);

         newArguments.Add(ThinOutType(subtype, rawType.TypeParameters,

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

 

     // the instantiations of inserted type variables, the order corresponds to the order in which "AbstractionVariable(int)" delivers variables

-    private Type/*!*/ ThinOutType(Type rawType, TypeVariableSeq boundTypeParams, TypeSeq instantiations) {

+    private Type/*!*/ ThinOutType(Type rawType, TypeVariableSeq boundTypeParams, List<Type> instantiations) {

       Contract.Requires(instantiations != null);

       Contract.Requires(boundTypeParams != null);

       Contract.Requires(rawType != null);

@@ -1027,7 +1027,7 @@ namespace Microsoft.Boogie.TypeErasure {
         //

         // traverse the subtypes

         CtorType/*!*/ rawCtorType = rawType.AsCtor;

-        TypeSeq/*!*/ newArguments = new TypeSeq();

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

         foreach (Type/*!*/ subtype in rawCtorType.Arguments) {

           Contract.Assert(subtype != null);

           newArguments.Add(ThinOutType(subtype, boundTypeParams,

diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index 8e4bc7ab..00259ecd 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -627,7 +627,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
       if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) {

         MapType/*!*/ rawType = node[0].Type.AsMap;

         Contract.Assert(rawType != null);

-        TypeSeq/*!*/ abstractionInstantiation;

+        List<Type>/*!*/ abstractionInstantiation;

         Function/*!*/ select =

           AxBuilder.MapTypeAbstracter.Select(rawType, out abstractionInstantiation);

         Contract.Assert(abstractionInstantiation != null);

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

       if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) {

         MapType/*!*/ rawType = node[0].Type.AsMap;

-        TypeSeq/*!*/ abstractionInstantiation;

+        List<Type>/*!*/ abstractionInstantiation;

         Function/*!*/ store =

           AxBuilder.MapTypeAbstracter.Store(rawType, out abstractionInstantiation);

 

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

     private OpTypesPair TypesPairForSelectStore(VCExprNAry/*!*/ node, Function/*!*/ untypedOp,

       // instantiation of the abstract map type parameters

-                                                TypeSeq/*!*/ abstractionInstantiation) {

+                                                List<Type>/*!*/ abstractionInstantiation) {

       Contract.Requires(node != null);

       Contract.Requires(untypedOp != null);

       Contract.Requires(abstractionInstantiation != null);

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index ec2d47bd..c78d7fba 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -646,7 +646,7 @@ namespace Microsoft.Boogie.TypeErasure
       typeParams.AddRange(abstractedType.FreeVariables.ToList());

 

       originalIndexTypes = new List<Type/*!*/>(abstractedType.Arguments.Count + 1);

-      TypeSeq/*!*/ mapTypeParams = new TypeSeq();

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

       foreach (TypeVariable/*!*/ var in abstractedType.FreeVariables) {

         Contract.Assert(var != null);

         mapTypeParams.Add(var);

@@ -1271,7 +1271,7 @@ namespace Microsoft.Boogie.TypeErasure
 

       MapType/*!*/ mapType = node[0].Type.AsMap;

       Contract.Assert(mapType != null);

-      TypeSeq/*!*/ instantiations; // not used

+      List<Type>/*!*/ instantiations; // not used

       Function/*!*/ select =

         AxBuilder.MapTypeAbstracter.Select(mapType, out instantiations);

       Contract.Assert(select != null);

@@ -1291,7 +1291,7 @@ namespace Microsoft.Boogie.TypeErasure
       Contract.Requires(bindings != null);

       Contract.Requires(node != null);

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

-      TypeSeq/*!*/ instantiations; // not used

+      List<Type>/*!*/ instantiations; // not used

       Function/*!*/ store =

         AxBuilder.MapTypeAbstracter.Store(node[0].Type.AsMap, out instantiations);

       Contract.Assert(store != null);

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 3961f096..41f1e207 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -31,7 +31,7 @@ namespace Microsoft.Boogie {
       if (ControlFlowFunction == null) {

         Formal/*!*/ first = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);

         Formal/*!*/ second = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);

-        VariableSeq inputs = new VariableSeq();

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

         inputs.Add(first);

         inputs.Add(second);

         Formal/*!*/ returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), false);

@@ -728,11 +728,11 @@ namespace Microsoft.Boogie.VCExprAST {
       return res;

     }

 

-    public static TypeSeq ToTypeSeq(VCExpr[] exprs, int startIndex) {

+    public static List<Type> ToTypeSeq(VCExpr[] exprs, int startIndex) {

       Contract.Requires(exprs != null);

       Contract.Requires((Contract.ForAll(0, exprs.Length, i => exprs[i] != null)));

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

-      TypeSeq/*!*/ res = new TypeSeq();

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

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

       for (int i = startIndex; i < exprs.Length; ++i)

         res.Add(cce.NonNull(exprs[i]).Type);

       return res;

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 01366633..6137678b 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -576,7 +576,7 @@ namespace VC {
 

     private bool _disposed;

 

-    protected VariableSeq CurrentLocalVariables = null;

+    protected List<Variable> CurrentLocalVariables = null;

 

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

     protected Dictionary<Variable, int> variable2SequenceNumber;

@@ -1323,7 +1323,7 @@ namespace VC {
       return r;

     }

 

-    protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) {

+    protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(List<Block> blocks, List<IdentifierExpr> modifies, ModelViewInfo mvInfo) {

       Contract.Requires(blocks != null);

       Contract.Requires(modifies != null);

       Contract.Requires(mvInfo != null);

@@ -1397,7 +1397,7 @@ namespace VC {
     /// <summary>

     /// Compute the substitution for old expressions.

     /// </summary>

-    protected static Substitution ComputeOldExpressionSubstitution(IdentifierExprSeq modifies)

+    protected static Substitution ComputeOldExpressionSubstitution(List<IdentifierExpr> modifies)

     {

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

       foreach (IdentifierExpr ie in modifies)

@@ -1523,7 +1523,7 @@ namespace VC {
 

         HavocCmd hc = (HavocCmd)c;

         Contract.Assert(c != null);

-        IdentifierExprSeq havocVars = hc.Vars;

+        List<IdentifierExpr> havocVars = hc.Vars;

         // First, compute the new incarnations

         foreach (IdentifierExpr ie in havocVars) {

           Contract.Assert(ie != null);

@@ -1703,8 +1703,8 @@ namespace VC {
     public readonly List<Variable> AllVariables = new List<Variable>();

     public readonly List<Mapping> CapturePoints = new List<Mapping>();

     public static readonly Function MVState_FunctionDef = new Function(Token.NoToken, "$mv_state",

-      new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true),

-                      new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true)),

+      new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true),

+                           new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true) },

       new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false));

     public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "$mv_state_const", Bpl.Type.Int));

 

diff --git a/Source/VCGeneration/ExprExtensions.cs b/Source/VCGeneration/ExprExtensions.cs
index 7ebba061..2bdb4af7 100644
--- a/Source/VCGeneration/ExprExtensions.cs
+++ b/Source/VCGeneration/ExprExtensions.cs
@@ -159,7 +159,7 @@ namespace Microsoft.Boogie.ExprExtensions
 

         public FuncDecl MkFuncDecl(string name, Sort rng)

         {

-            Function g = new Function(Token.NoToken, name, new VariableSeq(), new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "dummy",rng)));

+            Function g = new Function(Token.NoToken, name, new List<Variable>(), new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "dummy",rng)));

             return BoogieFunctionOp(g);

         }

 

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index b4080e2c..59e2ca9e 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -178,7 +178,7 @@ namespace Microsoft.Boogie
 

             // collect the variables needed in the invariant

             ExprSeq exprs = new ExprSeq();

-            VariableSeq vars = new VariableSeq();

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

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

 

             if (style == AnnotationStyle.Flat)

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

             // collect the variables needed in the invariant

             ExprSeq exprs = new ExprSeq();

-            VariableSeq vars = new VariableSeq();

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

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

 

                 foreach (Variable v in program.GlobalVariables())

@@ -465,7 +465,7 @@ namespace Microsoft.Boogie
 

                 this.interfaceVars = interfaceVars;

                 this.assertExpr = Expr.Not(assertExpr);

-                VariableSeq functionInterfaceVars = new VariableSeq();

+                List<Variable> functionInterfaceVars = new List<Variable>();

                 foreach (Variable v in interfaceVars)

                 {

                     Contract.Assert(v != null);

@@ -654,7 +654,7 @@ namespace Microsoft.Boogie
                 // Get record type

                 var argtype = proc.InParams[0].TypedIdent.Type;

 

-                var ins = new VariableSeq();

+                var ins = new List<Variable>();

                 ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));

 

                 var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

diff --git a/Source/VCGeneration/OrderingAxioms.cs b/Source/VCGeneration/OrderingAxioms.cs
index 4fbc80da..1e7615cb 100644
--- a/Source/VCGeneration/OrderingAxioms.cs
+++ b/Source/VCGeneration/OrderingAxioms.cs
@@ -91,7 +91,7 @@ namespace Microsoft.Boogie {
 

       Function res;

       if (!OneStepFuns.TryGetValue(t, out res)) {

-        VariableSeq args = new VariableSeq();

+        List<Variable> args = new List<Variable>();

         args.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "arg0", t), true));

         args.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "arg1", t), true));

         Formal result = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "res", t), false);

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 5848e63b..d1a83827 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -195,7 +195,7 @@ namespace VC {
       vcgen = stratifiedVcGen;

       impl = implementation;

 

-      VariableSeq functionInterfaceVars = new VariableSeq();

+      List<Variable> functionInterfaceVars = new List<Variable>();

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

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

       }

@@ -337,7 +337,7 @@ namespace VC {
         // Get record type

         var argtype = proc.InParams[0].TypedIdent.Type;

 

-        var ins = new VariableSeq();

+        var ins = new List<Variable>();

         ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));

 

         var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

@@ -430,7 +430,7 @@ namespace VC {
     public Macro CreateNewMacro() {

       string newName = "StratifiedInliningMacro@" + macroCountForStratifiedInlining.ToString();

       macroCountForStratifiedInlining++;

-      return new Macro(Token.NoToken, newName, new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool), false));

+      return new Macro(Token.NoToken, newName, new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool), false));

     }

     private int varCountForStratifiedInlining = 0;

     public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 19e28099..491c7eae 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1235,7 +1235,7 @@ namespace VC {
 

             ResetPredecessors(codeExpr.Blocks);

             vcgen.AddBlocksBetween(codeExpr.Blocks);

-            Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));

+            Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new List<IdentifierExpr>(), new ModelViewInfo(codeExpr));

             int ac;  // computed, but then ignored for this CodeExpr

             VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);

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

@@ -2031,7 +2031,7 @@ namespace VC {
         #endregion

 

         #region Collect all variables that are assigned to in all of the natural loops for which this is the header

-        VariableSeq varsToHavoc = new VariableSeq();

+        List<Variable> varsToHavoc = new List<Variable>();

         foreach (Block backEdgeNode in cce.NonNull( g.BackEdgeNodes(header)))

         {

           Contract.Assert(backEdgeNode != null);

@@ -2045,7 +2045,7 @@ namespace VC {
             }

           }

         }

-        IdentifierExprSeq havocExprs = new IdentifierExprSeq();

+        List<IdentifierExpr> havocExprs = new List<IdentifierExpr>();

         foreach ( Variable v in varsToHavoc )

         {

           Contract.Assert(v != null);