More refactoring

24 files changed, 164 insertions, 186 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 6b0fcdb3..347e3db7 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -11,6 +11,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
   using System.Diagnostics.Contracts;

   using System.Collections;

   using System.Collections.Generic;

+  using System.Linq;

 

   public class CallSite {

     public readonly Implementation/*!*/ Impl;

@@ -71,6 +72,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 

 namespace Microsoft.Boogie {

   using System;

+  using System.Linq;

   using System.Collections;

   using System.Diagnostics;

   using System.Collections.Generic;

@@ -210,7 +212,7 @@ namespace Microsoft.Boogie {
       TopLevelDeclarations = prunedTopLevelDeclarations;

     

       foreach (DatatypeConstructor f in constructors.Values) {

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

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

           DatatypeSelector selector = new DatatypeSelector(f, i);

           f.selectors.Add(selector);

           TopLevelDeclarations.Add(selector);

@@ -1843,10 +1845,10 @@ namespace Microsoft.Boogie {
       stream.Write(")");

 

       if (shortRet) {

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

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

         stream.Write(" : ");

         cce.NonNull(OutParams[0]).TypedIdent.Type.Emit(stream);

-      } else if (OutParams.Length > 0) {

+      } else if (OutParams.Count > 0) {

         stream.Write(" returns (");

         OutParams.Emit(stream, true);

         stream.Write(")");

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

 

     protected void SortTypeParams() {

-      TypeSeq/*!*/ allTypes = InParams.ToTypeSeq;

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

       Contract.Assert(allTypes != null);

-      allTypes.AddRange(OutParams.ToTypeSeq);

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

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

     }

 

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

         rc.PopVarContext();

         Type.CheckBoundVariableOccurrences(TypeParameters,

-                                           InParams.ToTypeSeq, OutParams.ToTypeSeq,

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

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

                                            this.tok, "function arguments",

                                            rc);

       } finally {

@@ -2151,7 +2154,7 @@ namespace Microsoft.Boogie {
       // type parameters only occur in the output type

       call = Expr.CoerceType(tok, call, (Type)OutParams[0].TypedIdent.Type.Clone());

       Expr def = Expr.Eq(call, definition);

-      if (quantifiedTypeVars.Count != 0 || dummies.Length != 0) {

+      if (quantifiedTypeVars.Count != 0 || dummies.Count != 0) {

         def = new ForallExpr(tok, quantifiedTypeVars, dummies,

                              kv,

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

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

 

         Type.CheckBoundVariableOccurrences(TypeParameters,

-                                           InParams.ToTypeSeq, OutParams.ToTypeSeq,

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

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

                                            this.tok, "procedure arguments",

                                            rc);

 

@@ -2750,7 +2754,7 @@ namespace Microsoft.Boogie {
       }

 

       if (this.StructuredStmts != null && !CommandLineOptions.Clo.PrintInstrumented && !CommandLineOptions.Clo.PrintInlined) {

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

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

           stream.WriteLine();

         }

         if (CommandLineOptions.Clo.PrintUnstructured < 2) {

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

 

         Type.CheckBoundVariableOccurrences(TypeParameters,

-                                           InParams.ToTypeSeq, OutParams.ToTypeSeq,

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

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

                                            this.tok, "implementation arguments",

                                            rc);

       } finally {

@@ -2870,7 +2875,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(procFormals != null);

       Contract.Requires(inout != null);

       Contract.Requires(tc != null);

-      if (implFormals.Length != procFormals.Length) {

+      if (implFormals.Count != procFormals.Count) {

         tc.Error(this, "mismatched number of {0}-parameters in procedure implementation: {1}",

                  inout, this.Name);

       } else {

@@ -2891,7 +2896,7 @@ namespace Microsoft.Boogie {
           subst2.Add(this.TypeParameters[i], newVar);

         }

 

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

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

           // the names of the formals are allowed to change from the proc to the impl

 

           // but types must be identical

@@ -2924,11 +2929,11 @@ namespace Microsoft.Boogie {
       if (this.formalMap != null)

         return this.formalMap;

       else {

-        Dictionary<Variable, Expr>/*!*/ map = new Dictionary<Variable, Expr> (InParams.Length + OutParams.Length);

+        Dictionary<Variable, Expr>/*!*/ map = new Dictionary<Variable, Expr> (InParams.Count + OutParams.Count);

 

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

-        Contract.Assume(InParams.Length == Proc.InParams.Length);

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

+        Contract.Assume(InParams.Count == Proc.InParams.Count);

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

           Variable/*!*/ v = InParams[i];

           Contract.Assert(v != null);

           IdentifierExpr ie = new IdentifierExpr(v.tok, v);

@@ -2936,8 +2941,8 @@ namespace Microsoft.Boogie {
           Contract.Assert(pv != null);

           map.Add(pv, ie);

         }

-        System.Diagnostics.Debug.Assert(OutParams.Length == Proc.OutParams.Length);

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

+        System.Diagnostics.Debug.Assert(OutParams.Count == Proc.OutParams.Count);

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

           Variable/*!*/ v = cce.NonNull(OutParams[i]);

           IdentifierExpr ie = new IdentifierExpr(v.tok, v);

           Variable pv = cce.NonNull(Proc.OutParams[i]);

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

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

 

-  public static class ListFactory {

-    public static List<T> MakeList<T>(params T[]/*!*/ args) {

-      return new List<T>(args);

-    }

-  }

-

   public sealed class VariableSeq : List<Variable> {

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

       : base(args) {

@@ -3224,33 +3223,6 @@ namespace Microsoft.Boogie {
       : base(varSeq) {

       Contract.Requires(varSeq != null);

     }

-    public void Emit(TokenTextWriter stream, bool emitAttributes) {

-      Contract.Requires(stream != null);

-      string sep = "";

-      foreach (Variable/*!*/ v in this) {

-        Contract.Assert(v != null);

-        stream.Write(sep);

-        sep = ", ";

-        v.EmitVitals(stream, 0, emitAttributes);

-      }

-    }

-    public TypeSeq/*!*/ ToTypeSeq {

-      get {

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

-

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

-        foreach (Variable/*!*/ v in this) {

-          Contract.Assert(v != null);

-          res.Add(v.TypedIdent.Type);

-        }

-        return res;

-      }

-    }

-    public int Length {

-      get {

-        return Count;

-      }

-    }

   }

 

   public sealed class TypeSeq : List<Type> {

@@ -3262,17 +3234,6 @@ namespace Microsoft.Boogie {
       : base(varSeq) {

       Contract.Requires(varSeq != null);

     }

-    public void Emit(TokenTextWriter stream, string separator) {

-      Contract.Requires(separator != null);

-      Contract.Requires(stream != null);

-      string sep = "";

-      foreach (Type/*!*/ v in this) {

-        Contract.Assert(v != null);

-        stream.Write(sep);

-        sep = separator;

-        v.Emit(stream);

-      }

-    }

   }

 

   public sealed class TypeVariableSeq : List<TypeVariable> {

@@ -3296,17 +3257,6 @@ namespace Microsoft.Boogie {
           this.Add(next);

       }

     }

-    public void Emit(TokenTextWriter stream, string separator) {

-      Contract.Requires(separator != null);

-      Contract.Requires(stream != null);

-      string sep = "";

-      foreach (TypeVariable/*!*/ v in this) {

-        Contract.Assert(v != null);

-        stream.Write(sep);

-        sep = separator;

-        v.Emit(stream);

-      }

-    }

   }

 

   public sealed class IdentifierExprSeq : List<IdentifierExpr> {

@@ -3318,33 +3268,7 @@ namespace Microsoft.Boogie {
       : base(ideSeq) {

       Contract.Requires(ideSeq != null);

     }

-    public new IdentifierExpr/*!*/ this[int index] {

-      get {

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

-

-        return cce.NonNull((IdentifierExpr)base[index]);

-      }

-      set {

-        base[index] = value;

-      }

-    }

-

-    public void Emit(TokenTextWriter stream, bool printWhereComments) {

-      Contract.Requires(stream != null);

-      string sep = "";

-      foreach (IdentifierExpr/*!*/ e in this) {

-        Contract.Assert(e != null);

-        stream.Write(sep);

-        sep = ", ";

-        e.Emit(stream);

 

-        if (printWhereComments && e.Decl != null && e.Decl.TypedIdent.WhereExpr != null) {

-          stream.Write(" /* where ");

-          e.Decl.TypedIdent.WhereExpr.Emit(stream);

-          stream.Write(" */");

-        }

-      }

-    }

   }

 

 

@@ -3464,6 +3388,58 @@ namespace Microsoft.Boogie {
       }

     }

 

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

+      Contract.Requires(stream != null);

+      string sep = "";

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

+        Contract.Assert(e != null);

+        stream.Write(sep);

+        sep = ", ";

+        e.Emit(stream);

+

+        if (printWhereComments && e.Decl != null && e.Decl.TypedIdent.WhereExpr != null) {

+          stream.Write(" /* where ");

+          e.Decl.TypedIdent.WhereExpr.Emit(stream);

+          stream.Write(" */");

+        }

+      }

+    }

+

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

+      Contract.Requires(stream != null);

+      string sep = "";

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

+        Contract.Assert(v != null);

+        stream.Write(sep);

+        sep = ", ";

+        v.EmitVitals(stream, 0, emitAttributes);

+      }

+    }

+

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

+      Contract.Requires(separator != null);

+      Contract.Requires(stream != null);

+      string sep = "";

+      foreach (Type/*!*/ v in tys) {

+        Contract.Assert(v != null);

+        stream.Write(sep);

+        sep = separator;

+        v.Emit(stream);

+      }

+    }

+

+    public static void Emit(this TypeVariableSeq tvs, TokenTextWriter stream, string separator) {

+      Contract.Requires(separator != null);

+      Contract.Requires(stream != null);

+      string sep = "";

+      foreach (TypeVariable/*!*/ v in tvs) {

+        Contract.Assert(v != null);

+        stream.Write(sep);

+        sep = separator;

+        v.Emit(stream);

+      }

+    }

+

   }

   #endregion

 

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index e4390634..1eb2ccc8 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1902,20 +1902,20 @@ namespace Microsoft.Boogie {
       // (a similar check is in CheckArgumentTypes, but we are not

       // able to call this method because it cannot cope with Ins/Outs

       // that are null)

-      if (Ins.Count != Proc.InParams.Length) {

+      if (Ins.Count != Proc.InParams.Count) {

         rc.Error(this.tok,

                  "wrong number of arguments in call to {0}: {1}",

                  callee, Ins.Count);

         return;

       }

-      if (Outs.Count != Proc.OutParams.Length) {

+      if (Outs.Count != Proc.OutParams.Count) {

         rc.Error(this.tok,

                  "wrong number of result variables in call to {0}: {1}",

                  callee, Outs.Count);

         return;

       }

       if (IsAsync) {

-        if (Proc.OutParams.Length > 0) {

+        if (Proc.OutParams.Count > 0) {

           rc.Error(this.tok, "a procedure called asynchronously can have no output parameters");

           return;

         }

@@ -2060,7 +2060,7 @@ namespace Microsoft.Boogie {
       VariableSeq/*!*/ cins = new VariableSeq();

       VariableSeq wildcardVars = new VariableSeq();

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

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

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

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

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

 

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

       #region assert (exists wildcardVars :: Pre[ins := cins])

       Substitution s = Substituter.SubstitutionFromHashtable(substMapBound);

-      bool hasWildcard = (wildcardVars.Length != 0);

+      bool hasWildcard = (wildcardVars.Count != 0);

       Expr preConjunction = null;

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

         Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);

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

       #region Create couts

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

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

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

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

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

 

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index fd09cd20..e5d955d2 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -14,6 +14,7 @@ namespace Microsoft.Boogie {
   using System.Collections.Generic;

   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics.Contracts;

+  using System.Linq;

   using Microsoft.Basetypes;

 

   using Set = GSet<object>; // not that the set used is not a set of Variable only, as it also contains TypeVariables

@@ -1787,7 +1788,7 @@ namespace Microsoft.Boogie {
     public virtual int ArgumentCount {

       get {

         Contract.Assume(Func != null);  // ArgumentCount requires object to be properly resolved.

-        return Func.InParams.Length;

+        return Func.InParams.Count;

       }

     }

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

@@ -1796,16 +1797,16 @@ 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.Count == Func.InParams.Length);

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

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

+      Contract.Assume(Func.OutParams.Count == 1);

 

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

       TypeSeq actualResultType =

         Type.CheckArgumentTypes(Func.TypeParameters,

                                 out resultingTypeArgs,

-                                Func.InParams.ToTypeSeq,

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

                                 actuals,

-                                Func.OutParams.ToTypeSeq,

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

                                 null,

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

         // arguments

@@ -2581,7 +2582,7 @@ namespace Microsoft.Boogie {
       int level = 0;

       stream.WriteLine(level, "|{");

 

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

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

         stream.Write(level + 1, "var ");

         this.LocVars.Emit(stream, true);

         stream.WriteLine(";");

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index a6382eb4..e42df50f 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -12,6 +12,7 @@ namespace Microsoft.Boogie {
   using System.Collections;

   using System.Diagnostics;

   using System.Collections.Generic;

+  using System.Linq;

   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics.Contracts;

   using Microsoft.Basetypes;

@@ -65,7 +66,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(typeParameters != null);

       Contract.Requires(dummies != null);

       Contract.Requires(body != null);

-      Contract.Requires(dummies.Length + typeParameters.Count > 0);

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

       TypeParameters = typeParameters;

       Dummies = dummies;

       Attributes = kv;

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

 

         // establish a canonical order of the type parameters

-        this.TypeParameters = Type.SortTypeParams(TypeParameters, Dummies.ToTypeSeq, null);

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

 

       } finally {

         rc.TypeBinderState = previousTypeBinderState;

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

     protected TypeVariableSeq GetUnmentionedTypeParameters() {

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

-      TypeVariableSeq/*!*/ dummyParameters = Type.FreeVariablesIn(Dummies.ToTypeSeq);

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

       Contract.Assert(dummyParameters != null);

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

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

@@ -427,21 +428,21 @@ namespace Microsoft.Boogie {
       Contract.Requires(typeParams != null);

       Contract.Requires(dummies != null);

       Contract.Requires(body != null);

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

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

     }

     public ForallExpr(IToken tok, VariableSeq 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.Length > 0);

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

     }

     public ForallExpr(IToken tok, VariableSeq 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.Length > 0);

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

     }

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

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

@@ -449,7 +450,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(dummies != null);

       Contract.Requires(typeParams != null);

       Contract.Requires(tok != null);

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

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

     }

 

     public override Absy StdDispatch(StandardVisitor visitor) {

@@ -473,21 +474,21 @@ namespace Microsoft.Boogie {
       Contract.Requires(typeParams != null);

       Contract.Requires(dummies != null);

       Contract.Requires(body != null);

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

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

     }

     public ExistsExpr(IToken tok, VariableSeq 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.Length > 0);

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

     }

     public ExistsExpr(IToken tok, VariableSeq 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.Length > 0);

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

     }

 

     public override Absy StdDispatch(StandardVisitor visitor) {

@@ -521,7 +522,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(typeParameters != null);

       Contract.Requires(dummies != null);

       Contract.Requires(body != null);

-      Contract.Requires(dummies.Length + typeParameters.Count > 0);

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

 

       Contract.Assert((this is ForallExpr) || (this is ExistsExpr));

 

@@ -702,7 +703,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(typeParameters != null);

       Contract.Requires(dummies != null);

       Contract.Requires(body != null);

-      Contract.Requires(dummies.Length + typeParameters.Count > 0);

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

     }

 

     public override BinderKind Kind {

diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs
index fd258399..8b35ffcb 100644
--- a/Source/Core/BitvectorAnalysis.cs
+++ b/Source/Core/BitvectorAnalysis.cs
@@ -190,12 +190,12 @@ namespace Microsoft.Boogie {
     }

 

     public override Implementation VisitImplementation(Implementation node) {

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

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

         DisjointSet a = MakeDisjointSet(node.InParams[i]);

         DisjointSet b = MakeDisjointSet(node.Proc.InParams[i]);

         a.Union(b);

       }

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

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

         DisjointSet a = MakeDisjointSet(node.OutParams[i]);

         DisjointSet b = MakeDisjointSet(node.Proc.OutParams[i]);

         a.Union(b);

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 2996514f..5263fd1f 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -339,7 +339,7 @@ namespace Microsoft.Boogie {
         substMap.Add(locVar, ie);

       }

 

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

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

         Variable inVar = cce.NonNull(impl.InParams[i]);

         LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, inVar.Name), inVar.TypedIdent.Type, inVar.TypedIdent.WhereExpr));

         newLocalVars.Add(localVar);

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

       }

 

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

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

         Variable outVar = cce.NonNull(impl.OutParams[i]);

         LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, outVar.Name), outVar.TypedIdent.Type, outVar.TypedIdent.WhereExpr));

         newLocalVars.Add(localVar);

@@ -445,7 +445,7 @@ namespace Microsoft.Boogie {
       CmdSeq inCmds = new CmdSeq();

 

       // assign in parameters

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

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

         Cmd cmd = Cmd.SimpleAssign(impl.tok,

                                    (IdentifierExpr)cce.NonNull(codeCopier.Subst)(cce.NonNull(impl.InParams[i])),

                                    cce.NonNull(callCmd.Ins[i]));

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

 

       // add where clauses of local vars as assume

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

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

         Expr whereExpr = (cce.NonNull(locVars[i])).TypedIdent.WhereExpr;

         if (whereExpr != null) {

           whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr);

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

 

       // add where clauses of output params as assume

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

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

         Expr whereExpr = (cce.NonNull(impl.OutParams[i])).TypedIdent.WhereExpr;

         if (whereExpr != null) {

           whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr);

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

 

       // assign out params

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

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

         Expr/*!*/ cout_exp = (IdentifierExpr)cce.NonNull(codeCopier.Subst(cce.NonNull(impl.OutParams[i])));

         Cmd cmd = Cmd.SimpleAssign(impl.tok, cce.NonNull(callCmd.Outs[i]), cout_exp);

         outCmds.Add(cmd);

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index bed2626f..a20d8ce9 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -62,7 +62,7 @@ namespace Microsoft.Boogie
         public override Implementation VisitImplementation(Implementation node)

         {

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

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

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

             {

                 string domainName = FindDomainName(node.Proc.InParams[i]);

                 if (domainName != null)

@@ -71,7 +71,7 @@ namespace Microsoft.Boogie
                     start.Add(node.InParams[i]);

                 }

             }

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

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

             {

                 string domainName = FindDomainName(node.Proc.OutParams[i]);

                 if (domainName != null)

@@ -296,7 +296,7 @@ namespace Microsoft.Boogie
         public override Cmd VisitCallCmd(CallCmd node)

         {

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

-            for (int i = 0; i < node.Proc.InParams.Length; i++)

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

             {

                 Variable formal = node.Proc.InParams[i];

                 string domainName = FindDomainName(formal);

@@ -331,7 +331,7 @@ namespace Microsoft.Boogie
                 inVars.Add(actual.Decl);

                 parallelCallInvars.Add(actual.Decl);

             }

-            for (int i = 0; i < node.Proc.OutParams.Length; i++)

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

             {

                 IdentifierExpr actual = node.Outs[i];

                 string actualDomainName = FindDomainName(actual.Decl);

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index beed64c8..bee34156 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -329,7 +329,7 @@ namespace Microsoft.Boogie
             {

                 locals.Add(ie.Decl);

             }

-            for (int i = 0; i < decl.InParams.Length - linearTypechecker.linearDomains.Count; i++)

+            for (int i = 0; i < decl.InParams.Count - linearTypechecker.linearDomains.Count; i++)

             {

                 Variable inParam = decl.InParams[i];

                 Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));

@@ -337,7 +337,7 @@ namespace Microsoft.Boogie
                 map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);

             }

             {

-                int i = decl.InParams.Length - linearTypechecker.linearDomains.Count;

+                int i = decl.InParams.Count - linearTypechecker.linearDomains.Count;

                 foreach (string domainName in linearTypechecker.linearDomains.Keys)

                 {

                     Variable inParam = decl.InParams[i];

@@ -347,7 +347,7 @@ namespace Microsoft.Boogie
                     i++;

                 }

             }

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

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

             {

                 Variable outParam = decl.OutParams[i];

                 var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));

@@ -439,7 +439,7 @@ namespace Microsoft.Boogie
             Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();

             Dictionary<string, Variable> domainNameToLocalVar = new Dictionary<string, Variable>();

             {

-                int i = impl.InParams.Length - linearTypechecker.linearDomains.Count;

+                int i = impl.InParams.Count - linearTypechecker.linearDomains.Count;

                 foreach (string domainName in linearTypechecker.linearDomains.Keys)

                 {

                     Variable inParam = impl.InParams[i];

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

                     domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);

                 }

-                for (int i = 0; i < impl.InParams.Length - linearTypechecker.linearDomains.Count; i++)

+                for (int i = 0; i < impl.InParams.Count - linearTypechecker.linearDomains.Count; i++)

                 {

                     Variable v = impl.InParams[i];

                     var domainName = linearTypechecker.FindDomainName(v);

@@ -627,7 +627,7 @@ namespace Microsoft.Boogie
 

             Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();

             {

-                int i = proc.InParams.Length - linearTypechecker.linearDomains.Count;

+                int i = proc.InParams.Count - linearTypechecker.linearDomains.Count;

                 foreach (string domainName in linearTypechecker.linearDomains.Keys)

                 {

                     Variable inParam = proc.InParams[i];

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

                     domainNameToScope[domainName].Add(v);

                 }

-                for (int i = 0; i < proc.InParams.Length - linearTypechecker.linearDomains.Count; i++)

+                for (int i = 0; i < proc.InParams.Count - linearTypechecker.linearDomains.Count; i++)

                 {

                     Variable v = proc.InParams[i];

                     var domainName = linearTypechecker.FindDomainName(v);

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

                     domainNameToScope[domainName].Add(v);

                 }

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

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

                 {

                     Variable v = proc.OutParams[i];

                     var domainName = linearTypechecker.FindDomainName(v);

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index ed5b88ae..44d56045 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -390,7 +390,7 @@ private class BvBounds : Expr {
 		}

 		if (!allUnnamed) {

 		 Bpl.Type prevType = null;

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

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

 		   TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;

 		   if (curr.HasName) {

 		     // the argument was given as both an identifier and a type

@@ -1775,13 +1775,13 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				Forall();

 				x = t; 

 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

-				if (typeParams.Count + ds.Length > 0)

+				if (typeParams.Count + ds.Count > 0)

 				 e = new ForallExpr(x, typeParams, ds, kv, trig, e); 

 			} else if (la.kind == 89 || la.kind == 90) {

 				Exists();

 				x = t; 

 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

-				if (typeParams.Count + ds.Length > 0)

+				if (typeParams.Count + ds.Count > 0)

 				 e = new ExistsExpr(x, typeParams, ds, kv, trig, e); 

 			} else if (la.kind == 91 || la.kind == 92) {

 				Lambda();

@@ -1789,7 +1789,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

 				if (trig != null)

 				 SemErr("triggers not allowed in lambda expressions");

-				if (typeParams.Count + ds.Length > 0)

+				if (typeParams.Count + ds.Count > 0)

 				 e = new LambdaExpr(x, typeParams, ds, kv, e); 

 			} else SynErr(123);

 			Expect(10);

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 77d49f3e..8a38d67a 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -549,7 +549,7 @@ namespace Microsoft.Boogie {
     public virtual VariableSeq VisitVariableSeq(VariableSeq variableSeq) {

       Contract.Requires(variableSeq != null);

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

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

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

         variableSeq[i] = this.VisitVariable(cce.NonNull(variableSeq[i]));

       return variableSeq;

     }

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index ceef059e..321d4072 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -82,7 +82,7 @@ namespace Microsoft.Boogie.Houdini {
             // type check

             existentialFunctions.Values.Iter(func =>

                 {

-                    if (func.OutParams.Length != 1 || !func.OutParams[0].TypedIdent.Type.IsBool)

+                    if (func.OutParams.Count != 1 || !func.OutParams[0].TypedIdent.Type.IsBool)

                         throw new AbsHoudiniInternalError(string.Format("Existential function {0} must return bool", func.Name));

                     if(func.Body != null)

                         throw new AbsHoudiniInternalError(string.Format("Existential function {0} should not have a body", func.Name));

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index f896c27f..b4408f03 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -265,7 +265,7 @@ namespace Microsoft.Boogie.Houdini {
     }

     private CmdSeq InlineRequiresForCallCmd(CallCmd node) {

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

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

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

         substMap.Add(node.Proc.InParams[i], node.Ins[i]);

       }

       Substitution substitution = Substituter.SubstitutionFromHashtable(substMap);

diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs
index ca5a0df6..a6287db5 100644
--- a/Source/Predication/UniformityAnalyser.cs
+++ b/Source/Predication/UniformityAnalyser.cs
@@ -338,7 +338,7 @@ namespace Microsoft.Boogie
                             SetNonUniform(callCmd.callee);

                         }

                     }

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

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

                     {

                         if (IsUniform(callCmd.callee, Callee.InParams[i].Name)

                             && !IsUniform(impl.Name, callCmd.Ins[i]))

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

                     }

 

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

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

                     {

                         if (IsUniform(impl.Name, callCmd.Outs[i].Name)

                         && !IsUniform(callCmd.callee, Callee.OutParams[i].Name))

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 7fffd6fc..4e94c238 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -273,7 +273,7 @@ namespace Microsoft.Boogie.SMTLib
               foreach (Function f in ctx.KnownDatatypeConstructors[datatype])

               {

                 string quotedConstructorName = Namer.GetQuotedName(f, f.Name);

-                if (f.InParams.Length == 0)

+                if (f.InParams.Count == 0)

                 {

                   datatypeString += quotedConstructorName + " ";

                 }

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 2bbe4978..2bf8fa22 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -209,7 +209,7 @@ void ObjectInvariant()
             string printedName = Namer.GetQuotedName(f, f.Name);

             Contract.Assert(printedName != null);

 

-            Contract.Assert(f.OutParams.Length == 1);

+            Contract.Assert(f.OutParams.Count == 1);

             var argTypes = f.InParams.Cast<Variable>().MapConcat(p => TypeToStringReg(p.TypedIdent.Type), " ");

             string decl;

             if(RegisteredRelations.Contains(op.Func))

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index a110c817..6509bc30 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -496,7 +496,7 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Requires(vars != null);

       // Check for a 'qid, name' pair in keyvalues

       string qid = QKeyValue.FindStringAttribute(attributes, "qid");

-      if (qid == null && vars.Length != 0) {

+      if (qid == null && vars.Count != 0) {

         // generate default name (line:column position in .bpl file)

         Variable v = vars[0];

         Contract.Assert(v != null); // Rustan's claim!

@@ -1148,7 +1148,7 @@ namespace Microsoft.Boogie.VCExprAST {
           // first bind the formals to VCExpr variables, which are later

           // substituted with the actual parameters

           var inParams = app.Func.InParams;

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

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

             subst[BaseTranslator.BindVariable(inParams[i])] = args[i];

 

           // recursively translate the body of the expansion

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 48bb3354..e6384e67 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -65,7 +65,7 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Requires(gen != null);

       Contract.Requires(fun != null);

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

-      List<VCExprVar/*!*/>/*!*/ arguments = new List<VCExprVar/*!*/>(fun.InParams.Length);

+      List<VCExprVar/*!*/>/*!*/ arguments = new List<VCExprVar/*!*/>(fun.InParams.Count);

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

         Contract.Assert(f != null);

         VCExprVar/*!*/ var = gen.Variable(f.Name, f.TypedIdent.Type);

@@ -192,7 +192,7 @@ namespace Microsoft.Boogie.TypeErasure {
     public TypeCtorRepr(Function ctor, List<Function/*!*/>/*!*/ dtors) {

       Contract.Requires(ctor != null);

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

-      Contract.Requires(ctor.InParams.Length == dtors.Count);

+      Contract.Requires(ctor.InParams.Count == dtors.Count);

       this.Ctor = ctor;

       this.Dtors = dtors;

     }

@@ -283,7 +283,7 @@ namespace Microsoft.Boogie.TypeErasure {
         GenCtorAssignment(Gen.Function(typeRepr,

                                        HelperFuns.ToVCExprList(quantifiedVars)));

 

-      if (typeRepr.InParams.Length == 0)

+      if (typeRepr.InParams.Count == 0)

         return eq;

 

       return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(),

@@ -711,7 +711,7 @@ namespace Microsoft.Boogie.TypeErasure {
 

     public bool IsCast(Function fun) {

       Contract.Requires(fun != null);

-      if (fun.InParams.Length != 1)

+      if (fun.InParams.Count != 1)

         return false;

       Type/*!*/ inType = cce.NonNull(fun.InParams[0]).TypedIdent.Type;

       if (inType.Equals(U)) {

diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index 79a3286b..8e4bc7ab 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -104,15 +104,15 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Ensures(Contract.Result<Function>() != null);

       Function res;

       if (!Typed2UntypedFunctions.TryGetValue(fun, out res)) {

-        Contract.Assert(fun.OutParams.Length == 1);

+        Contract.Assert(fun.OutParams.Count == 1);

 

         // if all of the parameters are int or bool, the function does

         // not have to be changed

-        if (Contract.ForAll(0, fun.InParams.Length, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&

+        if (Contract.ForAll(0, fun.InParams.Count, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&

             UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type)) {

           res = fun;

         } else {

-          Type[]/*!*/ types = new Type[fun.TypeParameters.Count + fun.InParams.Length + 1];

+          Type[]/*!*/ types = new Type[fun.TypeParameters.Count + fun.InParams.Count + 1];

 

           int i = 0;

           // the first arguments are the explicit type parameters

@@ -285,13 +285,13 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
       Contract.Requires(store != null);

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

 

-      int arity = select.InParams.Length - 1 - mapTypeParamNum - mapAbstractionVarNum;

+      int arity = select.InParams.Count - 1 - mapTypeParamNum - mapAbstractionVarNum;

       List<VCExprVar/*!*/>/*!*/ types =

         HelperFuns.VarVector("t", mapTypeParamNum + mapAbstractionVarNum,

                              AxBuilder.T, Gen);

 

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

-      for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Length; i++) {

+      for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Count; i++) {

         indexTypes.Add(cce.NonNull(select.InParams[i]).TypedIdent.Type);

       }

       Contract.Assert(arity == indexTypes.Count);

@@ -330,7 +330,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
       Contract.Requires(store != null);

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

 

-      int arity = select.InParams.Length - 1 - mapTypeParamNum - mapAbstractionVarNum;

+      int arity = select.InParams.Count - 1 - mapTypeParamNum - mapAbstractionVarNum;

 

       List<VCExprVar/*!*/>/*!*/ freeTypeVars =

         HelperFuns.VarVector("u", mapAbstractionVarNum, AxBuilder.T, Gen);

@@ -346,7 +346,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
       types1.AddRange(freeTypeVars);

 

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

-      for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Length; i++) {

+      for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Count; i++) {

         indexTypes.Add(cce.NonNull(select.InParams[i]).TypedIdent.Type);

       }

       Contract.Assert(arity == indexTypes.Count);

@@ -673,7 +673,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
         Contract.Assert(t != null);

         inferredTypeArgs.Add(t);}

 

-      Contract.Assert(untypedOp.InParams.Length == inferredTypeArgs.Count + node.Arity);

+      Contract.Assert(untypedOp.InParams.Count == inferredTypeArgs.Count + node.Arity);

       return new OpTypesPair (Gen.BoogieFunctionOp(untypedOp), inferredTypeArgs);

     }

 

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index d887a70f..ec2d47bd 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -370,11 +370,11 @@ namespace Microsoft.Boogie.TypeErasure
       Contract.Requires(fun != null);

       UntypedFunction res;

       if (!Typed2UntypedFunctions.TryGetValue(fun, out res)) {

-        Contract.Assert(fun.OutParams.Length == 1);

+        Contract.Assert(fun.OutParams.Count == 1);

 

         // if all of the parameters are int or bool, the function does

         // not have to be changed

-        if (Contract.ForAll(0, fun.InParams.Length, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&

+        if (Contract.ForAll(0, fun.InParams.Count, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&

             UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type) &&

             fun.TypeParameters.Count == 0) {

           res = new UntypedFunction(fun, new List<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>());

@@ -388,13 +388,13 @@ namespace Microsoft.Boogie.TypeErasure
           List<TypeVariable/*!*/>/*!*/ implicitParams, explicitParams;

           SeparateTypeParams(argTypes, fun.TypeParameters, out implicitParams, out explicitParams);

 

-          Type[]/*!*/ types = new Type[explicitParams.Count + fun.InParams.Length + 1];

+          Type[]/*!*/ types = new Type[explicitParams.Count + fun.InParams.Count + 1];

           int i = 0;

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

             types[i] = T;

             i = i + 1;

           }

-          for (int j = 0; j < fun.InParams.Length; ++i, ++j)

+          for (int j = 0; j < fun.InParams.Count; ++i, ++j)

             types[i] = TypeAfterErasure(cce.NonNull(fun.InParams[j]).TypedIdent.Type);

           types[types.Length - 1] = TypeAfterErasure(cce.NonNull(fun.OutParams[0]).TypedIdent.Type);

 

@@ -414,7 +414,7 @@ namespace Microsoft.Boogie.TypeErasure
     private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun) {

       Contract.Requires(originalFun != null);

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

-      List<Type/*!*/>/*!*/ originalInTypes = new List<Type/*!*/>(originalFun.InParams.Length);

+      List<Type/*!*/>/*!*/ originalInTypes = new List<Type/*!*/>(originalFun.InParams.Count);

       foreach (Formal/*!*/ f in originalFun.InParams)

         originalInTypes.Add(f.TypedIdent.Type);

 

@@ -433,7 +433,7 @@ namespace Microsoft.Boogie.TypeErasure
       Contract.Requires(cce.NonNullElements(explicitTypeParams));

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

       Contract.Requires(originalResultType != null);

-      Contract.Requires(originalInTypes.Count + explicitTypeParams.Count == fun.InParams.Length);

+      Contract.Requires(originalInTypes.Count + explicitTypeParams.Count == fun.InParams.Count);

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

 

       if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) {

@@ -764,9 +764,9 @@ namespace Microsoft.Boogie.TypeErasure
       Contract.Requires(cce.NonNullElements(originalInTypes));

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

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

-      int arity = store.InParams.Length - 2;

+      int arity = store.InParams.Count - 2;

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

-      List<VCExprVar/*!*/> quantifiedVars = new List<VCExprVar/*!*/>(store.InParams.Length);

+      List<VCExprVar/*!*/> quantifiedVars = new List<VCExprVar/*!*/>(store.InParams.Count);

       VariableBindings bindings = new VariableBindings();

 

       // bound variable:  m

@@ -779,7 +779,7 @@ namespace Microsoft.Boogie.TypeErasure
       // bound variables:  indexes

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

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

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

+      for (int i = 1; i < store.InParams.Count - 1; i++) {

         origIndexTypes.Add(originalInTypes[i]);

         indexTypes.Add(cce.NonNull(store.InParams[i]).TypedIdent.Type);

       }

@@ -856,10 +856,10 @@ namespace Microsoft.Boogie.TypeErasure
       Contract.Requires(select != null);

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

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

-      int arity = store.InParams.Length - 2;

+      int arity = store.InParams.Count - 2;

 

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

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

+      for (int i = 1; i < store.InParams.Count - 1; i++) {

         indexTypes.Add(cce.NonNull(store.InParams[i]).TypedIdent.Type);

       }

       Contract.Assert(indexTypes.Count == arity);

@@ -1279,7 +1279,7 @@ namespace Microsoft.Boogie.TypeErasure
       List<int>/*!*/ explicitTypeParams =

         AxBuilderPremisses.MapTypeAbstracterPremisses

                           .ExplicitSelectTypeParams(mapType);

-      Contract.Assert(select.InParams.Length == explicitTypeParams.Count + node.Arity);

+      Contract.Assert(select.InParams.Count == explicitTypeParams.Count + node.Arity);

 

       List<Type/*!*/>/*!*/ typeArgs = new List<Type/*!*/>(explicitTypeParams.Count);

       foreach (int i in explicitTypeParams)

@@ -1309,7 +1309,7 @@ namespace Microsoft.Boogie.TypeErasure
       Function/*!*/ oriFun = ((VCExprBoogieFunctionOp)node.Op).Func;

       Contract.Assert(oriFun != null);

       UntypedFunction untypedFun = AxBuilderPremisses.Typed2Untyped(oriFun);

-      Contract.Assert(untypedFun.Fun.InParams.Length ==

+      Contract.Assert(untypedFun.Fun.InParams.Count ==

              untypedFun.ExplicitTypeParams.Count + node.Arity);

 

       List<Type/*!*/>/*!*/ typeArgs =

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 90dcb2de..3961f096 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -1785,7 +1785,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

     public override int Arity {

       get {

-        return Func.InParams.Length;

+        return Func.InParams.Count;

       }

     }

     public override int TypeParamArity {

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index fe8d67f5..01366633 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -938,8 +938,8 @@ namespace VC {
       }

 

       // where clauses of out-parameters

-      Contract.Assert(impl.OutParams.Length == impl.Proc.OutParams.Length);

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

+      Contract.Assert(impl.OutParams.Count == impl.Proc.OutParams.Count);

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

         Variable f = cce.NonNull(impl.Proc.OutParams[i]);

         if (f.TypedIdent.WhereExpr != null) {

           Expr e = Substituter.Apply(formalProcImplSubst, f.TypedIdent.WhereExpr);

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index ac7ee9be..b4080e2c 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -643,7 +643,7 @@ namespace Microsoft.Boogie
                 var proc = decl as Procedure;

                 if (proc == null) continue;

                 if (!proc.Name.StartsWith(recordProcName)) continue;

-                Contract.Assert(proc.InParams.Length == 1);

+                Contract.Assert(proc.InParams.Count == 1);

 

                 // Make a new function

                 TypedIdent ti = new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool);

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index c5d88c5c..5848e63b 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -326,7 +326,7 @@ namespace VC {
         var proc = decl as Procedure;

         if (proc == null) continue;

         if (!proc.Name.StartsWith(recordProcName)) continue;

-        Contract.Assert(proc.InParams.Length == 1);

+        Contract.Assert(proc.InParams.Count == 1);

 

         // Make a new function

         TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 873a5589..eff8c2e2 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1240,7 +1240,7 @@ namespace VC {
             VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);

             VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);

 

-            if (vcgen.CurrentLocalVariables.Length != 0)

+            if (vcgen.CurrentLocalVariables.Count != 0)

             {

               Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;

               List<VCExprVar> boundVars = new List<VCExprVar>();