More refactoring towards replacing PureCollections.Sequence with List

2 files changed, 5 insertions, 5 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index c024a62a..0e095c44 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -658,7 +658,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
       public override Expr VisitNAryExpr(NAryExpr node) {

         if (node.Fun is UnaryOperator) {

           var op = (UnaryOperator)node.Fun;

-          Contract.Assert(node.Args.Length == 1);

+          Contract.Assert(node.Args.Count == 1);

           if (op.Op == UnaryOperator.Opcode.Neg) {

             BigInteger? lo, hi;

             VisitExpr(node.Args[0]);

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

         } else if (node.Fun is BinaryOperator) {

           var op = (BinaryOperator)node.Fun;

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

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

           BigInteger? lo0, hi0, lo1, hi1;

           VisitExpr(node.Args[0]);

           lo0 = Lo; hi0 = Hi;

@@ -837,7 +837,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
           }

         } else if (node.Fun is IfThenElse) {

           var op = (IfThenElse)node.Fun;

-          Contract.Assert(node.Args.Length == 3);

+          Contract.Assert(node.Args.Count == 3);

           BigInteger? guardLo, guardHi, lo0, hi0, lo1, hi1;

           VisitExpr(node.Args[0]);

           guardLo = Lo; guardHi = Hi;

@@ -1037,7 +1037,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
     public override Expr VisitNAryExpr(NAryExpr node) {

       if (node.Fun is BinaryOperator) {

         var op = (BinaryOperator)node.Fun;

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

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

         var arg0 = node.Args[0];

         var arg1 = node.Args[1];

         BigInteger? k;

diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs
index a1e88656..633ad86e 100644
--- a/Source/AbsInt/Traverse.cs
+++ b/Source/AbsInt/Traverse.cs
@@ -88,7 +88,7 @@ namespace Microsoft.Boogie {
 

         //PM: The folowing assumption is needed because we cannot prove that a simple field update

         //PM: leaves the value of a property unchanged.

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

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

         cce.EndExpose();

       } else {

         Contract.Assert(b.TransferCmd == null || b.TransferCmd is ReturnCmd);        // It must be a returnCmd;