BlockSeq: farewell

19 files changed, 91 insertions, 102 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 1d6e6a30..fa601737 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -625,7 +625,7 @@ namespace Microsoft.Boogie {
           GotoCmd gotoCmd = source.TransferCmd as GotoCmd;

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

           List<String>/*!*/ newLabels = new List<String>();

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

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

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

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

               continue;

@@ -642,12 +642,12 @@ namespace Microsoft.Boogie {
         Block exit = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));

         GotoCmd cmd = new GotoCmd(Token.NoToken,

                                     new List<String> { cce.NonNull(blockMap[header]).Label, exit.Label },

-                                    new BlockSeq(blockMap[header], exit));

+                                    new List<Block> { blockMap[header], exit });

 

         if (detLoopExtract) //cutting the non-determinism

             cmd = new GotoCmd(Token.NoToken,

                                     new List<String> { cce.NonNull(blockMap[header]).Label },

-                                    new BlockSeq(blockMap[header]));

+                                    new List<Block> { blockMap[header] });

 

         Block entry;

         List<Cmd> initCmds = new List<Cmd>();

@@ -668,7 +668,7 @@ namespace Microsoft.Boogie {
           } else {

             Contract.Assume(gotoCmd.labelNames != null && gotoCmd.labelTargets != null);

             List<String> newLabels = new List<String>();

-            BlockSeq newTargets = new BlockSeq();

+            List<Block> newTargets = new List<Block>();

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

               Block target = gotoCmd.labelTargets[i];

               if (blockMap.ContainsKey(target)) {

@@ -701,7 +701,7 @@ namespace Microsoft.Boogie {
         Block lastIterBlock = new Block(Token.NoToken, lastIterBlockName, header.Cmds, header.TransferCmd);

         newBlocksCreated[header] = lastIterBlock;

         header.Cmds = new List<Cmd> { loopHeaderToCallCmd1[header] };

-        header.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { lastIterBlockName }, new BlockSeq(lastIterBlock));

+        header.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { lastIterBlockName }, new List<Block> { lastIterBlock });

         impl.Blocks.Add(lastIterBlock);

         blockMap[origHeader] = blockMap[header];

         blockMap.Remove(header);

@@ -830,7 +830,7 @@ namespace Microsoft.Boogie {
           else {

             List<String> newLabelNames = new List<String>();

             newLabelNames.AddRange(splitGotoCmd.labelNames);

-            BlockSeq newLabelTargets = new BlockSeq();

+            List<Block> newLabelTargets = new List<Block>();

             newLabelTargets.AddRange(splitGotoCmd.labelTargets);

             newTransferCmd = new GotoCmd(splitCandidate.tok, newLabelNames, newLabelTargets);

           }

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

       foreach (Block/*!*/ block in this.Blocks) {

         Contract.Assert(block != null);

-        block.Predecessors = new BlockSeq();

+        block.Predecessors = new List<Block>();

       }

 

     }

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

     public void ComputePredecessorsForBlocks() {

       foreach (Block b in this.Blocks) {

-        b.Predecessors = new BlockSeq();

+        b.Predecessors = new List<Block>();

       }

       foreach (Block b in this.Blocks) {

         GotoCmd gtc = b.TransferCmd as GotoCmd;

@@ -3264,17 +3264,6 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class BlockSeq : List<Block> {

-    public BlockSeq(params Block[]/*!*/ args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public BlockSeq(BlockSeq blockSeq)

-      : base(blockSeq) {

-      Contract.Requires(blockSeq != null);

-    }

-  }

-

   public static class Emitter {

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

       Contract.Requires(stream != null);

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 635b82f2..d1f3a845 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -816,7 +816,7 @@ namespace Microsoft.Boogie {
     public int iterations;         // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not

 

     // VC generation and SCC computation

-    public BlockSeq/*!*/ Predecessors;

+    public List<Block>/*!*/ Predecessors;

 

     // This field is used during passification to null-out entries in block2Incartion hashtable early

     public int succCount;

@@ -849,7 +849,7 @@ namespace Microsoft.Boogie {
       this.Label = label;

       this.Cmds = cmds;

       this.TransferCmd = transferCmd;

-      this.Predecessors = new BlockSeq();

+      this.Predecessors = new List<Block>();

       this.liveVarsBefore = null;

       this.TraversingStatus = VisitState.ToVisit;

       this.iterations = 0;

@@ -2690,7 +2690,7 @@ namespace Microsoft.Boogie {
     [Rep]

     public List<String> labelNames;

     [Rep]

-    public BlockSeq labelTargets;

+    public List<Block> labelTargets;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

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

       this.labelNames = labelSeq;

     }

-    public GotoCmd(IToken/*!*/ tok, List<String>/*!*/ labelSeq, BlockSeq/*!*/ blockSeq)

+    public GotoCmd(IToken/*!*/ tok, List<String>/*!*/ labelSeq, List<Block>/*!*/ blockSeq)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(labelSeq != null);

@@ -2717,7 +2717,7 @@ namespace Microsoft.Boogie {
       this.labelNames = labelSeq;

       this.labelTargets = blockSeq;

     }

-    public GotoCmd(IToken/*!*/ tok, BlockSeq/*!*/ blockSeq)

+    public GotoCmd(IToken/*!*/ tok, List<Block>/*!*/ blockSeq)

       : base(tok) { //requires (blockSeq[i] != null ==> blockSeq[i].Label != null);

       Contract.Requires(tok != null);

       Contract.Requires(blockSeq != null);

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

       }

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

-      labelTargets = new BlockSeq();

+      labelTargets = new List<Block>();

       foreach (string/*!*/ lbl in labelNames) {

         Contract.Assert(lbl != null);

         Block b = rc.LookUpBlock(lbl);

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index e59dd27e..3355c9a0 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -73,7 +73,7 @@ namespace Microsoft.Boogie {
         Contract.Assert(b != null);

         GotoCmd g = b.TransferCmd as GotoCmd;

         if (g != null) {

-          BlockSeq targets = new BlockSeq();

+          List<Block> targets = new List<Block>();

           foreach (Block t in cce.NonNull(g.labelTargets)) {

             Block nt = subst[t];

             targets.Add(nt);

@@ -83,10 +83,10 @@ namespace Microsoft.Boogie {
       }

       return clone;

     }

-    public override BlockSeq VisitBlockSeq(BlockSeq blockSeq) {

+    public override List<Block> VisitBlockSeq(List<Block> blockSeq) {

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

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

-      return base.VisitBlockSeq(new BlockSeq(blockSeq));

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

+      return base.VisitBlockSeq(new List<Block>(blockSeq));

     }

     public override List<Block/*!*/>/*!*/ VisitBlockList(List<Block/*!*/>/*!*/ blocks) {

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

diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs
index c8941bbf..63084d99 100644
--- a/Source/Core/InterProceduralReachabilityGraph.cs
+++ b/Source/Core/InterProceduralReachabilityGraph.cs
@@ -82,7 +82,7 @@ namespace Microsoft.Boogie
             (newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelTargets.Add(gotoCmd.labelTargets[i]);

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

           }

-          gotoCmd.labelTargets = new BlockSeq { newProcedureEntryNodes[proc] };

+          gotoCmd.labelTargets = new List<Block> { newProcedureEntryNodes[proc] };

           gotoCmd.labelNames = new List<String> { newProcedureEntryNodes[proc].Label };

         }

       }

@@ -97,7 +97,7 @@ namespace Microsoft.Boogie
         var gotoCmd = n.TransferCmd as GotoCmd;

         if (gotoCmd != null)

         {

-          BlockSeq newTargets = new BlockSeq();

+          List<Block> newTargets = new List<Block>();

           foreach (Block t in gotoCmd.labelTargets)

           {

             if (originalToNew.ContainsKey(t))

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

         if (!newProcedureEntryNodes.ContainsKey(proc.Name))

         {

-          Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new List<Cmd>(), new GotoCmd(Token.NoToken, new BlockSeq()));

+          Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<Block>()));

           nodes.Add(newBlock);

           newProcedureEntryNodes[proc.Name] = newBlock;

           newProcedureExitNodes[proc.Name] = newBlock;

@@ -137,7 +137,7 @@ namespace Microsoft.Boogie
       foreach (var impl in prog.TopLevelDeclarations.OfType<Implementation>())

       {

         string exitLabel = "__" + impl.Name + "_newExit";

-        Block newExit = new Block(Token.NoToken, exitLabel, new List<Cmd>(), new GotoCmd(Token.NoToken, new BlockSeq()));

+        Block newExit = new Block(Token.NoToken, exitLabel, new List<Cmd>(), new GotoCmd(Token.NoToken, new List<Block>()));

         nodes.Add(newExit);

         newProcedureExitNodes[impl.Name] = newExit;

         foreach (Block b in impl.Blocks)

@@ -164,7 +164,7 @@ namespace Microsoft.Boogie
               newBlock = new Block(b.tok, label, new List<Cmd>(cmds.ToArray()), null);

               nodes.Add(newBlock);

               originalToNew[newBlock] = newBlock;

-              prev.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { label }, new BlockSeq { newBlock });

+              prev.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { label }, new List<Block> { newBlock });

             }

             prev = newBlock;

             i++;

@@ -173,7 +173,7 @@ namespace Microsoft.Boogie
           if (b.TransferCmd is ReturnCmd || (b.TransferCmd is GotoCmd &&

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

           {

-            prev.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { exitLabel }, new BlockSeq { newExit });

+            prev.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { exitLabel }, new List<Block> { newExit });

           }

           else

           {

diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs
index a67f23f7..df1be84c 100644
--- a/Source/Core/LoopUnroll.cs
+++ b/Source/Core/LoopUnroll.cs
@@ -248,7 +248,7 @@ namespace Microsoft.Boogie {
 

         } else {

           body = node.Body;

-          BlockSeq newSuccs = new BlockSeq();

+          List<Block> newSuccs = new List<Block>();

 

           foreach (GraphNode succ in node.ForwardEdges) {

             Block s;

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index eaecf887..4815c781 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -372,7 +372,7 @@ namespace Microsoft.Boogie
             Substitution subst = Substituter.SubstitutionFromHashtable(map);

             List<Block> yieldCheckerBlocks = new List<Block>();

             List<String> labels = new List<String>();

-            BlockSeq labelTargets = new BlockSeq();

+            List<Block> labelTargets = new List<Block>();

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

             labels.Add(yieldCheckerBlock.Label);

             labelTargets.Add(yieldCheckerBlock);

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

                 if (lhss.Count > 0)

                 {

-                    Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new BlockSeq(impl.Blocks[0])));

+                    Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] }));

                     impl.Blocks.Insert(0, initBlock);

                 }

             }

@@ -739,7 +739,7 @@ namespace Microsoft.Boogie
             TransferCmd transferCmd = new ReturnCmd(Token.NoToken);

             if (yieldCheckerProcs.Count > 0)

             {

-                BlockSeq blockTargets = new BlockSeq();

+                List<Block> blockTargets = new List<Block>();

                 List<String> labelTargets = new List<String>();

                 int labelCount = 0;

                 foreach (Procedure proc in yieldCheckerProcs)

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 987eadb8..cf33e23e 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -136,9 +136,9 @@ namespace Microsoft.Boogie {
       node.Blocks = this.VisitBlockList(node.Blocks);

       return node;

     }

-    public virtual BlockSeq VisitBlockSeq(BlockSeq blockSeq) {

+    public virtual List<Block> VisitBlockSeq(List<Block> blockSeq) {

       Contract.Requires(blockSeq != null);

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

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

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

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

       return blockSeq;

diff --git a/Source/Core/Xml.cs b/Source/Core/Xml.cs
index b4783d28..dcc19b34 100644
--- a/Source/Core/Xml.cs
+++ b/Source/Core/Xml.cs
@@ -103,7 +103,7 @@ namespace Microsoft.Boogie {
       cce.EndExpose();

     }

 

-    public void WriteError(string message, IToken errorToken, IToken relatedToken, BlockSeq trace) {

+    public void WriteError(string message, IToken errorToken, IToken relatedToken, List<Block> trace) {

       Contract.Requires(errorToken != null);

       Contract.Requires(message != null);

       Contract.Requires(IsOpen && (trace == null || cce.Owner.Different(this, trace)));

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

 

 #if CCI

-    public void WriteError(string message, Cci.Node offendingNode, BlockSeq trace) {

+    public void WriteError(string message, Cci.Node offendingNode, List<Block> trace) {

       Contract.Requires(offendingNode != null);

       Contract.Requires(message != null);

       Contract.Requires(IsOpen && cce.Owner.Different(this, offendingNode));

diff --git a/Source/Doomed/DoomedLoopUnrolling.cs b/Source/Doomed/DoomedLoopUnrolling.cs
index 2b83da37..38fa99ac 100644
--- a/Source/Doomed/DoomedLoopUnrolling.cs
+++ b/Source/Doomed/DoomedLoopUnrolling.cs
@@ -338,11 +338,11 @@ namespace VC
                 Block b = kvp.Key;

                 if (UncheckableNodes.Contains(GraphMap[b])) uncheckables.Add(b);

                 blocks.Add(b);

-                b.Predecessors = new BlockSeq();

+                b.Predecessors = new List<Block>();

                 foreach (GraphNode p in kvp.Value.Pre) b.Predecessors.Add(p.Label);

                 if (kvp.Value.Suc.Count > 0)

                 {

-                    BlockSeq bs = new BlockSeq();                    

+                    List<Block> bs = new List<Block>();                    

                     foreach (GraphNode s in kvp.Value.Suc) bs.Add(s.Label);                    

                     b.TransferCmd = new GotoCmd(b.tok, bs);

                 }

diff --git a/Source/Doomed/HasseDiagram.cs b/Source/Doomed/HasseDiagram.cs
index b2ece2df..ad3d487e 100644
--- a/Source/Doomed/HasseDiagram.cs
+++ b/Source/Doomed/HasseDiagram.cs
@@ -335,7 +335,7 @@ namespace VC
             {

                 current = todo[0];

                 todo.Remove(current);

-                BlockSeq pre = m_Predecessors(current, forward);

+                List<Block> pre = m_Predecessors(current, forward);

                 bool ready = true;

                 if (pre != null)

                 {

@@ -356,7 +356,7 @@ namespace VC
                 done.Add(current);

                 unavoidableBlocks[current].Add(current);

 

-                BlockSeq suc = m_Succecessors(current, forward);

+                List<Block> suc = m_Succecessors(current, forward);

                 if (suc == null) continue;

                 foreach (Block bsuc in suc)

                 {

@@ -402,7 +402,7 @@ namespace VC
             return ret;

         }

 

-        private BlockSeq m_Predecessors(Block b, bool forward)

+        private List<Block> m_Predecessors(Block b, bool forward)

         {

             if (forward) return b.Predecessors;

             GotoCmd gc = b.TransferCmd as GotoCmd;

@@ -413,7 +413,7 @@ namespace VC
             return null;

         }

 

-        private BlockSeq m_Succecessors(Block b, bool forward)

+        private List<Block> m_Succecessors(Block b, bool forward)

         {

             return m_Predecessors(b, !forward);

         }

diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs
index ca282b0a..9f1d8290 100644
--- a/Source/Doomed/VCDoomed.cs
+++ b/Source/Doomed/VCDoomed.cs
@@ -791,7 +791,7 @@ namespace VC {
         // update the successors and predecessors

         foreach (Block b in lb)

         {

-            BlockSeq newpreds = new BlockSeq();

+            List<Block> newpreds = new List<Block>();

             foreach (Block b_ in b.Predecessors)

             {

                 newpreds.Add(clonemap[b_]);

@@ -802,7 +802,7 @@ namespace VC {
             if (gc != null)

             {

                 List<String> lseq = new List<String>();

-                BlockSeq bseq = new BlockSeq();

+                List<Block> bseq = new List<Block>();

                 foreach (string s in gc.labelNames) lseq.Add(s);

                 foreach (Block b_ in gc.labelTargets) bseq.Add(clonemap[b_]);

                 GotoCmd tcmd = new GotoCmd(gc.tok, lseq, bseq);

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index e988c638..f81150b1 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1499,7 +1499,7 @@ namespace Microsoft.Boogie
     }

 

 

-    private static void WriteErrorInformationToXmlSink(ErrorInformation errorInfo, BlockSeq trace)

+    private static void WriteErrorInformationToXmlSink(ErrorInformation errorInfo, List<Block> trace)

     {

       var msg = "assertion violation";

       switch (errorInfo.Kind)

diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs
index 771d403b..2174c150 100644
--- a/Source/Predication/BlockPredicator.cs
+++ b/Source/Predication/BlockPredicator.cs
@@ -51,9 +51,9 @@ public class BlockPredicator {
       contBlock.Label = block.Label + ".call.cont";

 

       block.TransferCmd =

-        new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));

+        new GotoCmd(Token.NoToken, new List<Block> { trueBlock, falseBlock });

       trueBlock.TransferCmd = falseBlock.TransferCmd =

-        new GotoCmd(Token.NoToken, new BlockSeq(contBlock));

+        new GotoCmd(Token.NoToken, new List<Block> { contBlock });

       nextBlock = contBlock;

     } else {

       PredicateCmd(block.Cmds, cmd);

@@ -217,7 +217,7 @@ public class BlockPredicator {
           Expr.Eq(cur, blockIds[n.Item1]),

           new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)) };

         backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,

-                                                new BlockSeq(n.Item1));

+                                                new List<Block> { n.Item1 });

 

         var tailBlock = new Block();

         newBlocks.Add(tailBlock);

@@ -227,7 +227,7 @@ public class BlockPredicator {
                                              Expr.Neq(cur, blockIds[n.Item1])) };

 

         prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

-                                        new BlockSeq(backedgeBlock, tailBlock));

+                                        new List<Block> { backedgeBlock, tailBlock });

         prevBlock = tailBlock;

       } else {

         var runBlock = n.Item1;

@@ -235,7 +235,7 @@ public class BlockPredicator {
         runBlock.Cmds = new List<Cmd>();

         newBlocks.Add(runBlock);

         prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

-                                            new BlockSeq(runBlock));

+                                            new List<Block> { runBlock });

 

         pExpr = Expr.Eq(cur, blockIds[runBlock]);

         if (createCandidateInvariants && blockGraph.Headers.Contains(runBlock)) {

diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 94b47f5e..8e1b960b 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -62,9 +62,9 @@ public class SmartBlockPredicator {
       contBlock.Label = block.Label + ".call.cont";

 

       block.TransferCmd =

-        new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));

+        new GotoCmd(Token.NoToken, new List<Block> { trueBlock, falseBlock });

       trueBlock.TransferCmd = falseBlock.TransferCmd =

-        new GotoCmd(Token.NoToken, new BlockSeq(contBlock));

+        new GotoCmd(Token.NoToken, new List<Block> { contBlock });

       nextBlock = contBlock;

     } else {

       PredicateCmd(p, block.Cmds, cmd);

@@ -389,7 +389,7 @@ public class SmartBlockPredicator {
           backedgeBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken, pExpr,

             new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)) };

           backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,

-                                                  new BlockSeq(n.Item1));

+                                                  new List<Block> { n.Item1 });

 

           var tailBlock = new Block();

           newBlocks.Add(tailBlock);

@@ -405,7 +405,7 @@ public class SmartBlockPredicator {
 

           if (prevBlock != null)

             prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

-                                          new BlockSeq(backedgeBlock, tailBlock));

+                                          new List<Block> { backedgeBlock, tailBlock });

           prevBlock = tailBlock;

         } else {

           PredicateBlock(pExpr, n.Item1, newBlocks, ref prevBlock);

@@ -430,7 +430,7 @@ public class SmartBlockPredicator {
     block.Cmds = new List<Cmd>();

     newBlocks.Add(block);

     if (prevBlock != null) {

-      prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(block));

+      prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new List<Block> { block });

     }

 

     if (parentMap.ContainsKey(block)) {

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 11efecdc..c6cf5221 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -626,9 +626,9 @@ namespace Microsoft.Boogie.VCExprAST {
       Push(e);

       return codeExpr;

     }

-    public override BlockSeq VisitBlockSeq(BlockSeq blockSeq) {

+    public override List<Block> VisitBlockSeq(List<Block> blockSeq) {

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

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

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

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index b094f209..93de935d 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -75,7 +75,7 @@ namespace Microsoft.Boogie {
     }

 

     [Peer]

-    public BlockSeq Trace;

+    public List<Block> Trace;

     public Model Model;

     public VC.ModelViewInfo MvInfo;

     public ProverContext Context;

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

     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;

 

-    internal Counterexample(BlockSeq trace, Model model, VC.ModelViewInfo mvInfo, ProverContext context) {

+    internal Counterexample(List<Block> trace, Model model, VC.ModelViewInfo mvInfo, ProverContext context) {

       Contract.Requires(trace != null);

       Contract.Requires(context != null);

       this.Trace = trace;

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

   public class CounterexampleComparer : IComparer<Counterexample> {

 

-    private int Compare(BlockSeq bs1, BlockSeq bs2)

+    private int Compare(List<Block> bs1, List<Block> bs2)

     {

       if (bs1.Count < bs2.Count)

       {

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

 

 

-    public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public AssertCounterexample(List<Block> trace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

       : base(trace, model, mvInfo, context) {

       Contract.Requires(trace != null);

       Contract.Requires(failingAssert != null);

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

 

 

-    public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public CallCounterexample(List<Block> trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

       : base(trace, model, mvInfo, context) {

       Contract.Requires(!failingRequires.Free);

       Contract.Requires(trace != null);

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

 

 

-    public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public ReturnCounterexample(List<Block> trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

       : base(trace, model, mvInfo, context) {

       Contract.Requires(trace != null);

       Contract.Requires(context != null);

@@ -679,7 +679,7 @@ namespace VC {
           }

           b.TransferCmd = new GotoCmd(Token.NoToken,

             new List<String> { targetBlock.Label },

-            new BlockSeq(targetBlock));

+            new List<Block> { targetBlock });

           targetBlock.Predecessors.Add(b);

         }

         impl.Blocks.Add(b);

@@ -724,7 +724,7 @@ namespace VC {
       Block origStartBlock = impl.Blocks[0];

       Block insertionPoint = new Block(

         new Token(-17, -4), blockLabel, startCmds,

-        new GotoCmd(Token.NoToken, new List<String> { origStartBlock.Label }, new BlockSeq(origStartBlock)));

+        new GotoCmd(Token.NoToken, new List<String> { origStartBlock.Label }, new List<Block> { origStartBlock }));

 

       impl.Blocks[0] = insertionPoint;  // make insertionPoint the start block

       impl.Blocks.Add(origStartBlock);  // and put the previous start block at the end of the list

@@ -808,7 +808,7 @@ namespace VC {
             ThreadInCodeExpr(impl, nextIP, be, true, debugWriter);

             // Third, make the old insertion-point block goto the entry block of the CodeExpr

             Block beEntry = cce.NonNull(be.Blocks[0]);

-            insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { beEntry.Label }, new BlockSeq(beEntry));

+            insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { beEntry.Label }, new List<Block> { beEntry });

             beEntry.Predecessors.Add(insertionPoint);

             // Fourth, update the insertion point

             insertionPoint = nextIP;

@@ -1110,7 +1110,7 @@ namespace VC {
             if (b.TransferCmd is ReturnCmd) {

               List<String> labels = new List<String>();

               labels.Add(unifiedExitLabel);

-              BlockSeq bs = new BlockSeq();

+              List<Block> bs = new List<Block>();

               bs.Add(unifiedExit);

               GotoCmd go = new GotoCmd(Token.NoToken, labels, bs);

               gotoCmdOrigins[go] = (ReturnCmd)b.TransferCmd;

@@ -1132,7 +1132,7 @@ namespace VC {
       Contract.Requires(blocks != null);

       foreach (Block b in blocks) {

         Contract.Assert(b != null);

-        b.Predecessors = new BlockSeq();

+        b.Predecessors = new List<Block>();

       }

       foreach (Block b in blocks) {

         Contract.Assert(b != null);

@@ -1621,7 +1621,7 @@ namespace VC {
       // successor of newBlock list

       List<String> ls = new List<String>();

       ls.Add(succ.Label);

-      BlockSeq bs = new BlockSeq();

+      List<Block> bs = new List<Block>();

       bs.Add(succ);

 

       Block newBlock = new Block(

@@ -1632,7 +1632,7 @@ namespace VC {
           );

 

       // predecessors of newBlock

-      BlockSeq ps = new BlockSeq();

+      List<Block> ps = new List<Block>();

       ps.Add(pred);

       newBlock.Predecessors = ps;

 

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 5a6ae6d3..3fe3910e 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -1585,7 +1585,7 @@ namespace Microsoft.Boogie
             Block entryBlock = cce.NonNull(procImpl.Blocks[0]);

             Contract.Assert(entryBlock != null);

            

-            BlockSeq trace = new BlockSeq(); 

+            List<Block> trace = new List<Block>(); 

             trace.Add(entryBlock);

 

             var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

@@ -1621,7 +1621,7 @@ namespace Microsoft.Boogie
         private Counterexample GenerateTraceRec(

                               RPFP rpfp, RPFP.Node root,

                               List<StateId> orderedStateIds,

-                              Block/*!*/ b, BlockSeq/*!*/ trace,

+                              Block/*!*/ b, List<Block>/*!*/ trace,

                               Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples,

                               StratifiedInliningInfo info,

                               bool toplevel)

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index f29a1b80..ef2cd1d1 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2558,7 +2558,7 @@ namespace VC {
             traceNodes.Add(absy, null);

         }

 

-        BlockSeq trace = new BlockSeq();

+        List<Block> trace = new List<Block>();

         Block entryBlock = cce.NonNull(procImpl.Blocks[0]);

         Contract.Assert(entryBlock != null);

         Contract.Assert(traceNodes.Contains(entryBlock));

@@ -2573,7 +2573,7 @@ namespace VC {
       private Counterexample GenerateTraceRec(

                             IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo,

                             int candidateId,

-                            Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace,

+                            Block/*!*/ b, Hashtable/*!*/ traceNodes, List<Block>/*!*/ trace,

                             Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples) {

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

         Contract.Requires(b != null);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 6599515d..92d1fd14 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -194,7 +194,7 @@ namespace VC {
             res.Add(kv.Value);

           }

           if (go != null) {

-            GotoCmd copy = new GotoCmd(go.tok, new List<String>(), new BlockSeq());

+            GotoCmd copy = new GotoCmd(go.tok, new List<String>(), new List<Block>());

             kv.Value.TransferCmd = copy;

             foreach (Block b in cce.NonNull(go.labelTargets)) {

               Contract.Assert(b != null);

@@ -744,7 +744,7 @@ namespace VC {
           GotoCmd gt = b.TransferCmd as GotoCmd;

           if (gt == null)

             continue;

-          BlockSeq targ = cce.NonNull(gt.labelTargets);

+          List<Block> targ = cce.NonNull(gt.labelTargets);

           if (targ.Count < 2)

             continue;

           // caution, we only consider two first exits

@@ -950,7 +950,7 @@ namespace VC {
         GotoCmd gt = b.TransferCmd as GotoCmd;

         copies[b] = res;

         if (gt != null) {

-          GotoCmd newGoto = new GotoCmd(gt.tok, new List<String>(), new BlockSeq());

+          GotoCmd newGoto = new GotoCmd(gt.tok, new List<String>(), new List<Block>());

           res.TransferCmd = newGoto;

           int pos = 0;

           foreach (Block ch in cce.NonNull(gt.labelTargets)) {

@@ -1038,7 +1038,7 @@ namespace VC {
         Contract.Requires(context != null);

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

 

-        BlockSeq trace = new BlockSeq();

+        List<Block> trace = new List<Block>();

         foreach (Block b in blocks) {

           Contract.Assert(b != null);

           trace.Add(b);

@@ -1735,7 +1735,7 @@ namespace VC {
             traceNodes.Add(absy, null);

         }

 

-        BlockSeq trace = new BlockSeq();

+        List<Block> trace = new List<Block>();

         Block entryBlock = cce.NonNull(this.blocks[0]);

         Contract.Assert(traceNodes.Contains(entryBlock));

         trace.Add(entryBlock);

@@ -1831,7 +1831,7 @@ namespace VC {
           // find the corresponding Block (assertNodes.Count is likely to be 1, or small in any case, so just do a linear search here)

           foreach (Block b in traceNodes) {

             if (b.Cmds.Contains(a)) {

-              BlockSeq trace = new BlockSeq();

+              List<Block> trace = new List<Block>();

               trace.Add(b);

               Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, model, MvInfo, context);

               callback.OnCounterexample(newCounterexample, null);

@@ -1882,7 +1882,7 @@ namespace VC {
 

       // Recompute the predecessors, but first insert a dummy start node that is sure not to be the target of any goto (because the cutting of back edges

       // below assumes that the start node has no predecessor)

-      impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new BlockSeq(impl.Blocks[0]))));

+      impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] })));

       ResetPredecessors(impl.Blocks);

       

       #region Convert program CFG into a DAG

@@ -1991,7 +1991,7 @@ namespace VC {
           if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Count > 1 )

           {

             // then remove the backedge by removing the target block from the list of gotos

-            BlockSeq remainingTargets = new BlockSeq();

+            List<Block> remainingTargets = new List<Block>();

             List<String> remainingLabels = new List<String>();

             Contract.Assume( gtc.labelNames != null);

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

@@ -2019,7 +2019,7 @@ namespace VC {
                 RecordCutEdge(edgesCut, backEdgeNode, gtc.labelTargets[0]);

           }

           #region Remove the backedge node from the list of predecessor nodes in the header

-          BlockSeq newPreds = new BlockSeq();

+          List<Block> newPreds = new List<Block>();

           foreach ( Block p in header.Predecessors )

           {

             if ( p != backEdgeNode )

@@ -2328,7 +2328,7 @@ namespace VC {
         var cex = cexInfo.counterexample;

         // Go through all blocks in the trace, map them back to blocks in the original program (if there is one)

         var ret = cex.Clone();

-        ret.Trace = new BlockSeq();

+        ret.Trace = new List<Block>();

         ret.calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

 

         for (int numBlock = 0; numBlock < cex.Trace.Count; numBlock ++ )

@@ -2448,7 +2448,7 @@ namespace VC {
     }

 

     static Counterexample TraceCounterexample(

-                          Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, Model errModel, ModelViewInfo mvInfo,

+                          Block/*!*/ b, Hashtable/*!*/ traceNodes, List<Block>/*!*/ trace, Model errModel, ModelViewInfo mvInfo,

                           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

                           ProverContext/*!*/ context,

                           Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples)

@@ -2493,7 +2493,7 @@ namespace VC {
       return null;

     }

 

-    public static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, Model errModel, ModelViewInfo mvInfo, ProverContext context) 

+    public static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, List<Block> trace, Model errModel, ModelViewInfo mvInfo, ProverContext context) 

     {

       Contract.Requires(cmd != null);

       Contract.Requires(transferCmd != null);

@@ -3024,13 +3024,13 @@ namespace VC {
     /// Remove the empty blocks reachable from the block.

     /// It changes the visiting state of the blocks, so that if you want to visit again the blocks, you have to reset them...

     /// </summary>

-    static BlockSeq RemoveEmptyBlocks(Block b) {

+    static List<Block> RemoveEmptyBlocks(Block b) {

       Contract.Requires(b != null);

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

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

 

       Contract.Assert(b.TraversingStatus == Block.VisitState.ToVisit);

       Block renameInfo;

-      BlockSeq retVal = removeEmptyBlocksWorker(b, true, out renameInfo);

+      List<Block> retVal = removeEmptyBlocksWorker(b, true, out renameInfo);

       if (renameInfo != null && !b.tok.IsValid) {

         bool onlyAssumes = true;

         foreach (Cmd c in b.Cmds) {

@@ -3054,14 +3054,14 @@ namespace VC {
     /// If renameInfoForStartBlock is non-null, it denotes an empty block with location information, and that

     /// information would be appropriate to display

     /// </summary>

-    private static BlockSeq removeEmptyBlocksWorker(Block b, bool startNode, out Block renameInfoForStartBlock)

+    private static List<Block> removeEmptyBlocksWorker(Block b, bool startNode, out Block renameInfoForStartBlock)

   {

       Contract.Requires(b != null);

       Contract.Ensures(Contract.ValueAtReturn(out renameInfoForStartBlock) == null || Contract.ValueAtReturn(out renameInfoForStartBlock).tok.IsValid);

       // ensures: b in result ==> renameInfoForStartBlock == null;

     

       renameInfoForStartBlock = null;

-      BlockSeq bs = new BlockSeq();

+      List<Block> bs = new List<Block>();

       GotoCmd gtc = b.TransferCmd as GotoCmd;

 

       // b has no successors

@@ -3103,7 +3103,7 @@ namespace VC {
         int m = 0;  // in the following loop, set renameInfoForStartBlock to the value that all recursive calls agree on, if possible; otherwise, null

         foreach (Block dest in gtc.labelTargets){Contract.Assert(dest != null);

           Block renameInfo;

-          BlockSeq ys = removeEmptyBlocksWorker(dest, false, out renameInfo);

+          List<Block> ys = removeEmptyBlocksWorker(dest, false, out renameInfo);

           Contract.Assert(ys != null);

           if (m == 0) {

             renameInfoForStartBlock = renameInfo;

@@ -3118,7 +3118,7 @@ namespace VC {
         }

         b.TraversingStatus = Block.VisitState.AlreadyVisited;

 

-        BlockSeq setOfSuccessors = new BlockSeq();

+        List<Block> setOfSuccessors = new List<Block>();

         foreach (Block d in mergedSuccessors)

           setOfSuccessors.Add(d);

         if (b.Cmds.Count == 0 && !startNode) {

@@ -3137,11 +3137,11 @@ namespace VC {
         if (!startNode) {

           renameInfoForStartBlock = null;

         }

-        return new BlockSeq(b);

+        return new List<Block> { b };

       }

       else // b has some successors, but we are already visiting it, or we have already visited it...

       {

-        return new BlockSeq(b);

+        return new List<Block> { b };

       }

     }