More refactoring towards replacing PureCollections.Sequence with List

19 files changed, 109 insertions, 158 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 9d857e22..b29e050c 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -564,7 +564,7 @@ namespace Microsoft.Boogie {
             if (detLoopExtract) {

                 GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;

                 Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null && 

-                    auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Length >= 1);

+                    auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1);

                 foreach(var bl in auxGotoCmd.labelTargets) {

                     bool found = false;

                     foreach(var n in g.NaturalLoops(header, source)) { //very expensive, can we do a contains?

@@ -621,10 +621,10 @@ namespace Microsoft.Boogie {
           dummyBlocks.Add(block1.Label);

 

           GotoCmd gotoCmd = source.TransferCmd as GotoCmd;

-          Contract.Assert(gotoCmd != null && gotoCmd.labelNames != null && gotoCmd.labelTargets != null && gotoCmd.labelTargets.Length >= 1);

+          Contract.Assert(gotoCmd != null && gotoCmd.labelNames != null && gotoCmd.labelTargets != null && gotoCmd.labelTargets.Count >= 1);

           StringSeq/*!*/ newLabels = new StringSeq();

           BlockSeq/*!*/ newTargets = new BlockSeq();

-          for (int i = 0; i < gotoCmd.labelTargets.Length; i++) {

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

             if (gotoCmd.labelTargets[i] == header)

               continue;

             newTargets.Add(gotoCmd.labelTargets[i]);

@@ -667,14 +667,14 @@ namespace Microsoft.Boogie {
             Contract.Assume(gotoCmd.labelNames != null && gotoCmd.labelTargets != null);

             StringSeq newLabels = new StringSeq();

             BlockSeq newTargets = new BlockSeq();

-            for (int i = 0; i < gotoCmd.labelTargets.Length; i++) {

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

               Block target = gotoCmd.labelTargets[i];

               if (blockMap.ContainsKey(target)) {

                 newLabels.Add(gotoCmd.labelNames[i]);

                 newTargets.Add(blockMap[target]);

               }  

             }

-            if (newTargets.Length == 0) {

+            if (newTargets.Count == 0) {

                 if (!detLoopExtract)

                     newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False));

                 newBlock.TransferCmd = new ReturnCmd(Token.NoToken);

@@ -2423,7 +2423,7 @@ namespace Microsoft.Boogie {
         e.Emit(stream, level);

       }

 

-      if (this.Modifies.Length > 0) {

+      if (this.Modifies.Count > 0) {

         stream.Write(level, "modifies ");

         this.Modifies.Emit(stream, false);

         stream.WriteLine(";");

@@ -3209,21 +3209,6 @@ namespace Microsoft.Boogie {
   // Generic Sequences

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

 

-  public sealed class TypedIdentSeq : PureCollections.Sequence {

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

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public new TypedIdent this[int index] {

-      get {

-        return (TypedIdent)base[index];

-      }

-      set {

-        base[index] = value;

-      }

-    }

-  }

-

   public sealed class VariableSeq : List<Variable> {

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

       : base(args) {

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

 

 

-  public sealed class CmdSeq : PureCollections.Sequence {

+  public sealed class CmdSeq : List<Cmd> {

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

       : base(args) {

       Contract.Requires(args != null);

@@ -3712,7 +3697,7 @@ namespace Microsoft.Boogie {
         GotoCmd/*!*/ g = (GotoCmd)tc;

         Contract.Assert(g != null);

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

-        if (g.labelTargets.Length == 1) {

+        if (g.labelTargets.Count == 1) {

           return new Sequential(new AtomicRE(b), Transform(cce.NonNull(g.labelTargets[0])));

         } else {

           RESeq rs = new RESeq();

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 15a9fff7..bfa43a1c 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -128,7 +128,7 @@ namespace Microsoft.Boogie {
       Contract.Assume(PrefixCommands == null);  // prefix has not been used

 

       BigBlock bb0 = BigBlocks[0];

-      if (prefixCmds.Length == 0) {

+      if (prefixCmds.Count == 0) {

         // This is always a success, since there is nothing to insert.  Now, decide

         // which name to use for the first block.

         if (bb0.Anonymous) {

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

             } else if (bcmd.Label == bb.LabelName) {

               // a break statement with a label can break out of both if statements and while statements

-              if (bb.simpleCmds.Length == 0) {

+              if (bb.simpleCmds.Count == 0) {

                 // this is a good target:  the label refers to the if/while statement

                 bcmd.BreakEnclosure = bb;

               } else {

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

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(labelNames == null || labelTargets == null || labelNames.Length == labelTargets.Length);

+      Contract.Invariant(labelNames == null || labelTargets == null || labelNames.Count == labelTargets.Count);

     }

 

     [NotDelayed]

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

       Contract.Requires(labelSeq != null);

       Contract.Requires(blockSeq != null);

-      Debug.Assert(labelSeq.Length == blockSeq.Length);

-      for (int i = 0; i < labelSeq.Length; i++) {

+      Debug.Assert(labelSeq.Count == blockSeq.Count);

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

         Debug.Assert(Equals(labelSeq[i], cce.NonNull(blockSeq[i]).Label));

       }

 

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

       Contract.Requires(blockSeq != null);

       StringSeq labelSeq = new StringSeq();

-      for (int i = 0; i < blockSeq.Length; i++)

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

         labelSeq.Add(cce.NonNull(blockSeq[i]).Label);

       this.labelNames = labelSeq;

       this.labelTargets = blockSeq;

@@ -2783,7 +2783,7 @@ namespace Microsoft.Boogie {
           labelTargets.Add(b);

         }

       }

-      Debug.Assert(rc.ErrorCount > 0 || labelTargets.Length == labelNames.Length);

+      Debug.Assert(rc.ErrorCount > 0 || labelTargets.Count == labelNames.Count);

     }

 

     public override Absy StdDispatch(StandardVisitor visitor) {

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 24622d8b..8d81c025 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1013,7 +1013,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(tc != null);

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

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

-      Contract.Ensures(args.Length == Contract.OldValue(args.Length));

+      Contract.Ensures(args.Count == Contract.OldValue(args.Count));

       throw new NotImplementedException();

     }

 

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

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

       stream.SetToken(ref this.tok);

-      Contract.Assert(args.Length == 1);

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

       // determine if parens are needed

       int opBindingStrength = 0x70;

       bool parensNeeded = opBindingStrength < contextBindingStrength ||

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

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

 

-      Contract.Assume(args.Length == 1);

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

       tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

       Type arg0type = cce.NonNull(cce.NonNull(args[0]).Type);

       switch (this.op) {

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

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

       stream.SetToken(ref this.tok);

-      Contract.Assert(args.Length == 2);

+      Contract.Assert(args.Count == 2);

       // determine if parens are needed

       int opBindingStrength;

       bool fragileLeftContext = false;  // false means "allow same binding power on left without parens"

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

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

       Contract.Ensures(args != null);

-      Contract.Assert(args.Length == 2);

+      Contract.Assert(args.Count == 2);

       // the default; the only binary operator with a type parameter is equality, but right

       // we don't store this parameter because it does not appear necessary

       tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

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

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

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

-      Contract.Assume(actuals.Length == Func.InParams.Length);

+      Contract.Assume(actuals.Count == Func.InParams.Length);

       Contract.Assume(Func.OutParams.Length == 1);

 

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

@@ -1809,7 +1809,7 @@ namespace Microsoft.Boogie {
                                 null,

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

         // arguments

-                                actuals.Length > 0 ? cce.NonNull(actuals[0]).tok : Token.NoToken,

+                                actuals.Count > 0 ? cce.NonNull(actuals[0]).tok : Token.NoToken,

                                 "application of " + name.Name,

                                 tc);

 

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

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

       stream.SetToken(ref this.tok);

-      Contract.Assert(args.Length == 1);

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

       // determine if parens are needed

       int opBindingStrength = 0x80;

       bool parensNeeded = opBindingStrength < contextBindingStrength ||

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

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

 

-      Contract.Assume(args.Length == 1);

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

       tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

 

       if (!this.Type.Unify(cce.NonNull(cce.NonNull(args[0]).Type)))

@@ -2010,7 +2010,7 @@ namespace Microsoft.Boogie {
       Contract.Ensures(args != null);

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

 

-      Contract.Assert(args.Length == 1);

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

 

       tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

 

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

       Fun = fun;

       Args = args;

-      Contract.Assert(Contract.ForAll(0, args.Length, index => args[index] != null));

+      Contract.Assert(Contract.ForAll(0, args.Count, index => args[index] != null));

     }

     [Pure]

     [Reads(ReadsAttribute.Reads.Nothing)]

@@ -2113,9 +2113,9 @@ namespace Microsoft.Boogie {
         Contract.Assert(e != null);

         e.Typecheck(tc);

       }

-      if (Fun.ArgumentCount != Args.Length) {

+      if (Fun.ArgumentCount != Args.Count) {

         tc.Error(this, "wrong number of arguments to function: {0} ({1} instead of {2})",

-                 Fun.FunctionName, Args.Length, Fun.ArgumentCount);

+                 Fun.FunctionName, Args.Count, Fun.ArgumentCount);

       } else if (tc.ErrorCount == prevErrorCount &&

         // if the type parameters are set, this node has already been

         // typechecked and does not need to be checked again

@@ -2191,7 +2191,7 @@ namespace Microsoft.Boogie {
                      int contextBindingStrength, bool fragileContext) {

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

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

-      Contract.Assume(args.Length == Arity + 1);

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

       Emit(args, stream, contextBindingStrength, fragileContext, false);

     }

 

@@ -2211,7 +2211,7 @@ namespace Microsoft.Boogie {
       stream.Write("[");

 

       string sep = "";

-      int lastIndex = withRhs ? args.Length - 1 : args.Length;

+      int lastIndex = withRhs ? args.Count - 1 : args.Count;

       for (int i = 1; i < lastIndex; ++i) {

         stream.Write(sep);

         sep = ", ";

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

       

       mapType = mapType.Expanded;

-      if (mapType.IsMap && mapType.MapArity != indexes.Length) {

+      if (mapType.IsMap && mapType.MapArity != indexes.Count) {

         tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1} instead of {2}",

-                 opName, indexes.Length, mapType.MapArity);

+                 opName, indexes.Count, mapType.MapArity);

         tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

         return null;

-      } else if (!mapType.Unify(new MapTypeProxy(map.tok, "select", indexes.Length))) {

+      } else if (!mapType.Unify(new MapTypeProxy(map.tok, "select", indexes.Count))) {

         tc.Error(map.tok, "{0} applied to a non-map: {1}", opName, map);

         tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

         return null;

@@ -2293,10 +2293,10 @@ namespace Microsoft.Boogie {
       //Contract.Requires(tc != null);

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

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

-      Contract.Assume(args.Length == Arity + 1);

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

 

       ExprSeq actualArgs = new ExprSeq();

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

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

         actualArgs.Add(args[i]);

 

       return Typecheck(cce.NonNull(cce.NonNull(args[0]).Type), cce.NonNull(args[0]),

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

       MapType mapType = a0Type.AsMap;

       TypeSeq actualArgTypes = new TypeSeq();

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

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

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

       }

       return Type.InferValueType(mapType.TypeParameters, mapType.Arguments, mapType.Result, actualArgTypes);

@@ -2372,7 +2372,7 @@ namespace Microsoft.Boogie {
                      int contextBindingStrength, bool fragileContext) {

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

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

-      Contract.Assert(args.Length == Arity + 2);

+      Contract.Assert(args.Count == Arity + 2);

       MapSelect.Emit(args, stream, contextBindingStrength, fragileContext, true);

     }

 

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

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

       ExprSeq selectArgs = new ExprSeq();

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

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

         selectArgs.Add(args[i]);

       Type resultType =

         MapSelect.Typecheck(cce.NonNull(cce.NonNull(args[0]).Type), cce.NonNull(args[0]),

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

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

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

-      Contract.Assert(args.Length == Arity + 2);

+      Contract.Assert(args.Count == Arity + 2);

       return Typecheck(args, out tpInstantiation, tc, this.tok, "map store");

     }

 

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

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

       stream.SetToken(ref this.tok);

-      Contract.Assert(args.Length == 3);

+      Contract.Assert(args.Count == 3);

       stream.Write("(if ");

       cce.NonNull(args[0]).Emit(stream, 0x00, false);

       stream.Write(" then ");

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

       Contract.Ensures(args != null);

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

-      Contract.Assert(args.Length == 3);

+      Contract.Assert(args.Count == 3);

       // the default; the only binary operator with a type parameter is equality, but right

       // we don't store this parameter because it does not appear necessary

       tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 6e719e60..a6382eb4 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -329,8 +329,8 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Tr != null);

-      Contract.Invariant(1 <= Tr.Length);

-      Contract.Invariant(Pos || Tr.Length == 1);

+      Contract.Invariant(1 <= Tr.Count);

+      Contract.Invariant(Pos || Tr.Count == 1);

     }

 

     public Trigger Next;

@@ -339,16 +339,16 @@ namespace Microsoft.Boogie {
       : this(tok, pos, tr, null) {

       Contract.Requires(tr != null);

       Contract.Requires(tok != null);

-      Contract.Requires(1 <= tr.Length);

-      Contract.Requires(pos || tr.Length == 1);

+      Contract.Requires(1 <= tr.Count);

+      Contract.Requires(pos || tr.Count == 1);

     }

 

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

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(tr != null);

-      Contract.Requires(1 <= tr.Length);

-      Contract.Requires(pos || tr.Length == 1);

+      Contract.Requires(1 <= tr.Count);

+      Contract.Requires(pos || tr.Count == 1);

       this.Pos = pos;

       this.Tr = tr;

       this.Next = next;

@@ -357,7 +357,7 @@ namespace Microsoft.Boogie {
     public void Emit(TokenTextWriter stream) {

       Contract.Requires(stream != null);

       stream.SetToken(this);

-      Contract.Assert(this.Tr.Length >= 1);

+      Contract.Assert(this.Tr.Count >= 1);

       string/*!*/ sep = Pos ? "{ " : "{:nopats ";

       foreach (Expr/*!*/ e in this.Tr) {

         Contract.Assert(e != null);

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index dd558f94..944bbe08 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -447,9 +447,9 @@ namespace Microsoft.Boogie {
       Contract.Requires(actualArgs != null);

       Contract.Requires(opName != null);

       Contract.Requires(tc != null);

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

+      Contract.Requires(formalArgs.Count == actualArgs.Count);

       Contract.Requires((formalOuts == null) == (actualOuts == null));

-      Contract.Requires(formalOuts == null || formalOuts.Count == cce.NonNull(actualOuts).Length);

+      Contract.Requires(formalOuts == null || formalOuts.Count == cce.NonNull(actualOuts).Count);

       Contract.Requires(tc == null || opName != null);//Redundant

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

 

@@ -524,15 +524,15 @@ namespace Microsoft.Boogie {
       Contract.Requires(opName != null);Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out actualTypeParams)));

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

 

-      if (formalIns.Count != actualIns.Length) {

+      if (formalIns.Count != actualIns.Count) {

         tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1}",

-                 opName, actualIns.Length);

+                 opName, actualIns.Count);

         // if there are no type parameters, we can still return the result

         // type and hope that the type checking proceeds

         return typeParams.Count == 0 ? formalOuts : null;

-      } else if (actualOuts != null && formalOuts.Count != actualOuts.Length) {

+      } else if (actualOuts != null && formalOuts.Count != actualOuts.Count) {

         tc.Error(typeCheckingSubject, "wrong number of result variables in {0}: {1}",

-                 opName, actualOuts.Length);

+                 opName, actualOuts.Count);

         // if there are no type parameters, we can still return the result

         // type and hope that the type checking proceeds

         actualTypeParams = new List<Type>();

diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs
index cac5068a..fd258399 100644
--- a/Source/Core/BitvectorAnalysis.cs
+++ b/Source/Core/BitvectorAnalysis.cs
@@ -351,7 +351,7 @@ namespace Microsoft.Boogie {
     public override Expr VisitNAryExpr(NAryExpr node) {

       BinaryOperator op = node.Fun as BinaryOperator;

       if (op != null) {

-        Debug.Assert(node.Args.Length == 2);

+        Debug.Assert(node.Args.Count == 2);

         MakeDisjointSet(node.Args[0]).Union(MakeDisjointSet(node.Args[1]));

       }

 

@@ -365,7 +365,7 @@ namespace Microsoft.Boogie {
             x = MakeDisjointSet(node.Args[0]);

           else

             x = MakeDisjointSet(node);

-          for (int i = 0; i < node.Args.Length; i++) {

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

             DisjointSet actual = MakeDisjointSet(node.Args[i]);

             actual.Union(x);

           }

@@ -392,8 +392,8 @@ namespace Microsoft.Boogie {
         int i = 0;

         MapDisjointSet mapDisjointSet = (MapDisjointSet)MakeDisjointSet(node.Args[i]);

         i++;

-        DisjointSet[] args = new DisjointSet[node.Args.Length - 1];

-        for (; i < node.Args.Length; i++) {

+        DisjointSet[] args = new DisjointSet[node.Args.Count - 1];

+        for (; i < node.Args.Count; i++) {

           args[i - 1] = MakeDisjointSet(node.Args[i]);

         }

         mapDisjointSet.Union(new MapDisjointSet(args, MakeDisjointSet(node)));

@@ -404,8 +404,8 @@ namespace Microsoft.Boogie {
         int i = 0;

         MapDisjointSet mapDisjointSet = (MapDisjointSet)MakeDisjointSet(node.Args[i]);

         i++;

-        DisjointSet[] args = new DisjointSet[node.Args.Length - 2];

-        for (; i < node.Args.Length - 1; i++) {

+        DisjointSet[] args = new DisjointSet[node.Args.Count - 2];

+        for (; i < node.Args.Count - 1; i++) {

           args[i - 1] = MakeDisjointSet(node.Args[i]);

         }

         mapDisjointSet.Union(new MapDisjointSet(args, MakeDisjointSet(node.Args[i])));

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 9cd7d524..0d737dfe 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -237,7 +237,7 @@ BoundVars<IToken/*!*/ x, out VariableSeq/*!*/ ds>
 = (.

     Contract.Requires(x != null);

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

-    TypedIdentSeq/*!*/ tyds = new TypedIdentSeq();

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

     ds = new VariableSeq();

     var dsx = ds;

   .)

@@ -246,10 +246,10 @@ BoundVars<IToken/*!*/ x, out VariableSeq/*!*/ ds>
 

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

 /* IdsType is used with const declarations */

-IdsType<out TypedIdentSeq/*!*/ tyds>

+IdsType<out List<TypedIdent>/*!*/ tyds>

 = (. Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); TokenSeq/*!*/ ids;  Bpl.Type/*!*/ ty; .)

   Idents<out ids> ":" Type<out ty>

-  (. tyds = new TypedIdentSeq();

+  (. tyds = new List<TypedIdent>();

      foreach(Token/*!*/ id in ids){

        Contract.Assert(id != null);

        tyds.Add(new TypedIdent(id, id.val, ty, null));

@@ -379,7 +379,7 @@ Types<TypeSeq/*!*/ ts>
 

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

 Consts<out VariableSeq/*!*/ ds>

-= (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; TypedIdentSeq/*!*/ xs;

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

      ds = new VariableSeq();

      bool u = false; QKeyValue kv = null;

      bool ChildrenComplete = false;

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 8cd3a2ea..e1da4dd6 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -310,7 +310,7 @@ namespace Microsoft.Boogie {
         GotoCmd gotoCmd = (GotoCmd)b.TransferCmd;

         if (gotoCmd.labelTargets == null)

           continue;

-        if (gotoCmd.labelTargets.Length == 1) {

+        if (gotoCmd.labelTargets.Count == 1) {

           Block/*!*/ succ = cce.NonNull(gotoCmd.labelTargets[0]);

           if (!multiPredBlocks.Contains(succ)) {

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

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

 

         CmdSeq cmds = block.Cmds;

-        int len = cmds.Length;

+        int len = cmds.Count;

         for (int i = len - 1; i >= 0; i--) {

           if (cmds[i] is CallCmd) {

             Procedure/*!*/ proc = cce.NonNull(cce.NonNull((CallCmd/*!*/)cmds[i]).Proc);

@@ -470,7 +470,7 @@ namespace Microsoft.Boogie {
       } else if (cmd is StateCmd) {

         StateCmd/*!*/ stCmd = (StateCmd)cce.NonNull(cmd);

         CmdSeq/*!*/ cmds = cce.NonNull(stCmd.Cmds);

-        int len = cmds.Length;

+        int len = cmds.Count;

         for (int i = len - 1; i >= 0; i--) {

           Propagate(cmds[i], liveSet);

         }

@@ -1242,7 +1242,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       // Propagate backwards in the block

       HashSet<Variable/*!*/>/*!*/ prop = new HashSet<Variable/*!*/>();

       prop.UnionWith(lv);

-      for (int i = block.Cmds.Length - 1; i >= 0; i--) {

+      for (int i = block.Cmds.Count - 1; i >= 0; i--) {

         Cmd/*!*/ cmd = block.Cmds[i];

         Contract.Assert(cmd != null);

         if (cmd is CallCmd) {

@@ -1303,7 +1303,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       GenKillWeight/*!*/ w = wi.getWeightAfter();

       Contract.Assert(w != null);

 

-      for (int i = wi.block.Cmds.Length - 1; i >= 0; i--) {

+      for (int i = wi.block.Cmds.Count - 1; i >= 0; i--) {

         Cmd/*!*/ c = wi.block.Cmds[i];

         Contract.Assert(c != null);

         if (c is CallCmd && procICFG.ContainsKey(cce.NonNull(cce.NonNull((CallCmd)c).Proc).Name)) {

@@ -1463,7 +1463,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
         Contract.Assert(stCmd != null);

         CmdSeq/*!*/ cmds = stCmd.Cmds;

         Contract.Assert(cmds != null);

-        int len = cmds.Length;

+        int len = cmds.Count;

         ret = GenKillWeight.one();

         for (int i = len - 1; i >= 0; i--) {

           GenKillWeight/*!*/ w = getWeight(cmds[i], impl, prog);

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 47cf25d3..d2acca18 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -226,7 +226,7 @@ namespace Microsoft.Boogie {
         string label = block.Label;

         int lblCount = 0;

 

-        for (int i = 0; i < cmds.Length; ++i) {

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

           Cmd cmd = cmds[i];

           CallCmd callCmd = cmd as CallCmd;

 

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

     private CmdSeq RemoveAsserts(CmdSeq cmds) {

       CmdSeq newCmdSeq = new CmdSeq();

-      for (int i = 0; i < cmds.Length; i++) {

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

         Cmd cmd = cmds[i];

         if (cmd is AssertCmd) continue;

         newCmdSeq.Add(cmd);

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

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

       }

-      if (havocVars.Length > 0)

+      if (havocVars.Count > 0)

       {

           inCmds.Add(new HavocCmd(Token.NoToken, havocVars));

       }

diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs
index 0c026757..e103c628 100644
--- a/Source/Core/InterProceduralReachabilityGraph.cs
+++ b/Source/Core/InterProceduralReachabilityGraph.cs
@@ -71,13 +71,13 @@ namespace Microsoft.Boogie
       #region Add call and return edges

       foreach (var n in nodes)

       {

-        if (n.Cmds.Length == 1 && n.Cmds[0] is CallCmd)

+        if (n.Cmds.Count == 1 && n.Cmds[0] is CallCmd)

         {

           string proc = ((CallCmd)n.Cmds[0]).callee;

           GotoCmd gotoCmd = n.TransferCmd as GotoCmd;

           Debug.Assert(gotoCmd != null);

 

-          for (int i = 0; i < gotoCmd.labelTargets.Length; i++)

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

           {

             (newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelTargets.Add(gotoCmd.labelTargets[i]);

             (newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelNames.Add(gotoCmd.labelNames[i]);

@@ -171,7 +171,7 @@ namespace Microsoft.Boogie
           }

           Debug.Assert(prev != null);

           if (b.TransferCmd is ReturnCmd || (b.TransferCmd is GotoCmd &&

-              ((GotoCmd)b.TransferCmd).labelTargets.Length == 0))

+              ((GotoCmd)b.TransferCmd).labelTargets.Count == 0))

           {

             prev.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq { exitLabel }, new BlockSeq { newExit });

           }

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 1d541183..bed2626f 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -408,7 +408,7 @@ namespace Microsoft.Boogie
                 foreach (Block b in impl.Blocks)

                 {

                     CmdSeq newCmds = new CmdSeq();

-                    for (int i = 0; i < b.Cmds.Length; i++)

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

                     {

                         Cmd cmd = b.Cmds[i];

                         newCmds.Add(cmd);

diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs
index 403f6ff4..249e4249 100644
--- a/Source/Core/LoopUnroll.cs
+++ b/Source/Core/LoopUnroll.cs
@@ -268,7 +268,7 @@ namespace Microsoft.Boogie {
             newSuccs.Add(s);

           }

 

-          if (newSuccs.Length == 0) {

+          if (newSuccs.Count == 0) {

             tcmd = new ReturnCmd(orig.TransferCmd.tok);

           } else {

             tcmd = new GotoCmd(orig.TransferCmd.tok, newSuccs);

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 51381625..beed64c8 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -237,14 +237,14 @@ namespace Microsoft.Boogie
         {

             AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

 

-            if (globalMods.Length > 0)

+            if (globalMods.Count > 0)

             {

                 newCmds.Add(new HavocCmd(Token.NoToken, globalMods));

             }

             Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[yieldCmd], domainNameToInputVar);

             AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

 

-            for (int j = 0; j < cmds.Length; j++)

+            for (int j = 0; j < cmds.Count; j++)

             {

                 PredicateCmd predCmd = (PredicateCmd)cmds[j];

                 newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr));

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

                 YieldCmd yieldCmd = null;

                 CmdSeq newCmds = new CmdSeq();

-                for (int i = 0; i < b.Cmds.Length; i++)

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

                 {

                     Cmd cmd = b.Cmds[i];

                     if (cmd is YieldCmd)

@@ -472,7 +472,7 @@ namespace Microsoft.Boogie
                         if (pcmd == null)

                         {

                             DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);

-                            if (cmds.Length > 0)

+                            if (cmds.Count > 0)

                             {

                                 yields.Add(cmds);

                                 cmds = new CmdSeq();

@@ -535,7 +535,7 @@ namespace Microsoft.Boogie
                 if (yieldCmd != null)

                 {

                     DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);

-                    if (cmds.Length > 0)

+                    if (cmds.Count > 0)

                     {

                         yields.Add(cmds);

                         cmds = new CmdSeq();

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 7b172d30..c1a5efef 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -278,7 +278,7 @@ private class BvBounds : Expr {
 	}

 

 	void Consts(out VariableSeq/*!*/ ds) {

-		Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; TypedIdentSeq/*!*/ xs;

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

 		ds = new VariableSeq();

 		bool u = false; QKeyValue kv = null;

 		bool ChildrenComplete = false;

@@ -562,19 +562,19 @@ private class BvBounds : Expr {
 	void BoundVars(IToken/*!*/ x, out VariableSeq/*!*/ ds) {

 		Contract.Requires(x != null);

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

-		TypedIdentSeq/*!*/ tyds = new TypedIdentSeq();

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

 		ds = new VariableSeq();

 		var dsx = ds;

 		

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

 	}

 

-	void IdsType(out TypedIdentSeq/*!*/ tyds) {

+	void IdsType(out List<TypedIdent>/*!*/ tyds) {

 		Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); TokenSeq/*!*/ ids;  Bpl.Type/*!*/ ty; 

 		Idents(out ids);

 		Expect(11);

 		Type(out ty);

-		tyds = new TypedIdentSeq();

+		tyds = new List<TypedIdent>();

 		foreach(Token/*!*/ id in ids){

 		 Contract.Assert(id != null);

 		 tyds.Add(new TypedIdent(id, id.val, ty, null));

@@ -833,7 +833,7 @@ private class BvBounds : Expr {
 		   typeParams.Add(new TypeVariable(t, t.val));}

 		 decl = new TypeSynonymDecl(id, id.val, typeParams, body, kv);

 		} else {

-		 decl = new TypeCtorDecl(id, id.val, paramTokens.Length, kv);

+		 decl = new TypeCtorDecl(id, id.val, paramTokens.Count, kv);

 		}

 		

 	}

@@ -1664,13 +1664,13 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 			}

 			Expect(18);

 			if (store)

-			 e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs);

+			 e = new NAryExpr(x, new MapStore(x, allArgs.Count - 2), allArgs);

 			else if (bvExtract)

 			 e = new BvExtractExpr(x, e,

 			                       ((BvBounds)index0).Upper.ToIntSafe,

 			                       ((BvBounds)index0).Lower.ToIntSafe);

 			else

-			 e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);

+			 e = new NAryExpr(x, new MapSelect(x, allArgs.Count - 1), allArgs);

 			

 		}

 	}

diff --git a/Source/Core/PureCollections.cs b/Source/Core/PureCollections.cs
index 58b6e9c0..8eafd73f 100644
--- a/Source/Core/PureCollections.cs
+++ b/Source/Core/PureCollections.cs
@@ -520,7 +520,7 @@ namespace PureCollections {
     public bool MoveNext() {

       index++;

       //while (index < seq.elems.Length); // Sequences allow nils ... && seq.elems[index] == null);

-      return index < seq.Length;

+      return index < seq.Count;

     }

     public object Current {

       get {

@@ -594,7 +594,7 @@ namespace PureCollections {
     }

 

     //In place Update (and Remove) and Length - - - - - - - - - - - - - - - 

-    public int Length {

+    public int Count {

       get {

         return this.card;

       }

@@ -634,40 +634,6 @@ namespace PureCollections {
       }

     }

 

-    public void Remove() {

-      if (card == 0)

-        return;

-      card--;

-    }

-

-    // remove the first occurrence of o from this sequence

-    public void Remove(Object x) {

-      if (x == null)

-        throw new MissingCase();

-      Contract.Assert(this.elems != null);

-      for (int i = 0; i < card; i++) {

-        if (x.Equals(elems[i])) {

-          ++i;

-          while (i < card) {

-            elems[i - 1] = elems[i];

-            ++i;

-          }

-          card--;

-          elems[card] = null;

-          return;

-        }

-      }

-    }

-

-    public void Truncate(int newLen) {

-      Contract.Requires(0 <= newLen && newLen <= Length);

-      Contract.Assert(elems != null);

-      for (int i = newLen; i < card; i++) {

-        elems[i] = null;

-      }

-      card = newLen;

-    }

-

     //ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -

     [Pure]

     public override string ToString() {

diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 2f840a9b..532093b1 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -565,7 +565,7 @@ namespace Microsoft.Boogie {
     public bool InFrame(Variable v) {

       Contract.Requires(v != null);

       Contract.Requires(Frame != null);

-      return Contract.Exists(0, Frame.Length, ie => Frame[ie].Decl == v);

+      return Contract.Exists(0, Frame.Count, ie => Frame[ie].Decl == v);

     }

   }

 }

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 927b73fe..77d49f3e 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -32,7 +32,7 @@ namespace Microsoft.Boogie {
     public virtual ExprSeq VisitExprSeq(ExprSeq list) {

       Contract.Requires(list != null);

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

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

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

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

       return list;

     }

@@ -139,7 +139,7 @@ namespace Microsoft.Boogie {
     public virtual BlockSeq VisitBlockSeq(BlockSeq blockSeq) {

       Contract.Requires(blockSeq != null);

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

-      for (int i = 0, n = blockSeq.Length; i < n; i++)

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

         blockSeq[i] = this.VisitBlock(cce.NonNull(blockSeq[i]));

       return blockSeq;

     }

@@ -171,7 +171,7 @@ namespace Microsoft.Boogie {
     public virtual CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {

       Contract.Requires(cmdSeq != null);

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

-      for (int i = 0, n = cmdSeq.Length; i < n; i++)

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

         cmdSeq[i] = (Cmd)this.Visit(cce.NonNull(cmdSeq[i])); // call general Visit so subtypes of Cmd get visited by their particular visitor

       return cmdSeq;

     }

@@ -238,7 +238,7 @@ namespace Microsoft.Boogie {
     public override ExprSeq VisitExprSeq(ExprSeq exprSeq) {

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

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

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

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

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

       return exprSeq;

     }

@@ -321,7 +321,7 @@ namespace Microsoft.Boogie {
     public virtual IdentifierExprSeq VisitIdentifierExprSeq(IdentifierExprSeq identifierExprSeq) {

       Contract.Requires(identifierExprSeq != null);

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

-      for (int i = 0, n = identifierExprSeq.Length; i < n; i++)

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

         identifierExprSeq[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(identifierExprSeq[i]));

       return identifierExprSeq;

     }

@@ -430,7 +430,7 @@ namespace Microsoft.Boogie {
     public virtual RESeq VisitRESeq(RESeq reSeq) {

       Contract.Requires(reSeq != null);

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

-      for (int i = 0, n = reSeq.Length; i < n; i++)

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

         reSeq[i] = (RE)this.VisitRE(cce.NonNull(reSeq[i]));

       return reSeq;

     }

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index 2aaae096..09b6664e 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -371,21 +371,21 @@ namespace Microsoft.Boogie {
         IAppliable fun = ne.Fun;

         ExprSeq eSeq = ne.Args;

         if (fun != null) {

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

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

             Expr e0 = eSeq[0];

             if (e0 != null) {

               string s0 = PrettyPrintBplExpr(e0);

               return s0 + ".Length";

             }

             //unexpected, just fall outside to the default

-          } else if (fun.FunctionName == "$typeof" && eSeq.Length == 1) {

+          } else if (fun.FunctionName == "$typeof" && eSeq.Count == 1) {

             Expr e0 = eSeq[0];

             if (e0 != null) {

               string s0 = PrettyPrintBplExpr(e0);

               return "(the dynamic type of: " + s0 + ")";

             }

             //unexpected, just fall outside to the default

-          } else if (fun.FunctionName == "IntArrayGet" && eSeq.Length == 2) {

+          } else if (fun.FunctionName == "IntArrayGet" && eSeq.Count == 2) {

             Expr e0 = eSeq[0];

             Expr e1 = eSeq[1];

             if (e0 != null && e1 != null) {

@@ -394,7 +394,7 @@ namespace Microsoft.Boogie {
               return s0 + "[" + s1 + "]";

             }

             //unexpected, just fall outside to the default

-          } else if (fun.FunctionName == "$Is" && eSeq.Length == 2) {

+          } else if (fun.FunctionName == "$Is" && eSeq.Count == 2) {

             Expr e0 = eSeq[0];

             Expr e1 = eSeq[1];

             if (e0 != null && e1 != null) {

@@ -403,7 +403,7 @@ namespace Microsoft.Boogie {
               return "(" + s0 + " == null || (" + s0 + " is " + s1 + "))";

             }

             //unexpected, just fall outside to the default

-          } else if (fun.FunctionName == "$IsNotNull" && eSeq.Length == 2) {

+          } else if (fun.FunctionName == "$IsNotNull" && eSeq.Count == 2) {

             Expr e0 = eSeq[0];

             Expr e1 = eSeq[1];

             if (e0 != null && e1 != null) {

@@ -412,12 +412,12 @@ namespace Microsoft.Boogie {
               return "(" + s0 + " is " + s1 + ")";

             }

             //unexpected, just fall outside to the default

-          } else if (fun is MapSelect && eSeq.Length <= 3) {

+          } else if (fun is MapSelect && eSeq.Count <= 3) {

             // only maps with up to two arguments are supported right now (here)

             if (cce.NonNull(eSeq[0]).ToString() == "$Heap") {

               //print Index0.Index1, unless Index1 is "$elements", then just print Index0

               string s0 = PrettyPrintBplExpr(cce.NonNull(eSeq[1]));

-              if (eSeq.Length > 2) {

+              if (eSeq.Count > 2) {

                 string s1 = PrettyPrintBplExpr(cce.NonNull(eSeq[2]));

                 if (s1 == "$elements") {

                   return s0;

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

             }

             //unexpected, just fall outside to the default

-          } else if (fun is Microsoft.Boogie.BinaryOperator && eSeq.Length == 2) {

+          } else if (fun is Microsoft.Boogie.BinaryOperator && eSeq.Count == 2) {

             Microsoft.Boogie.BinaryOperator f = (Microsoft.Boogie.BinaryOperator)fun;

             Expr e0 = eSeq[0];

             Expr e1 = eSeq[1];

@@ -503,7 +503,7 @@ namespace Microsoft.Boogie {
             //unexpected, just fall outside to the default

           } else {

             string s = fun.FunctionName + "(";

-            for (int i = 0; i < eSeq.Length; i++) {

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

               Expr ex = eSeq[i];

               Contract.Assume(ex != null);

               if (i > 0) {

diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs
index fd69d911..476f1cac 100644
--- a/Source/Core/VariableDependenceAnalyser.cs
+++ b/Source/Core/VariableDependenceAnalyser.cs
@@ -360,7 +360,7 @@ namespace Microsoft.Boogie {
 

       HashSet<VariableDescriptor> result = new HashSet<VariableDescriptor>();

       var gotoCmd = b.TransferCmd as GotoCmd;

-      if (gotoCmd != null && gotoCmd.labelTargets.Length >= 2) {

+      if (gotoCmd != null && gotoCmd.labelTargets.Count >= 2) {

         foreach (Block succ in gotoCmd.labelTargets) {

           foreach (Cmd c in succ.Cmds) {

             AssumeCmd a = c as AssumeCmd;