CmdSeq: farewell

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 8f5cf64b..987eadb8 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -168,9 +168,9 @@ namespace Microsoft.Boogie {
           node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(node.Outs[i]));

       return node;

     }

-    public virtual CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {

+    public virtual List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {

       Contract.Requires(cmdSeq != null);

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

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

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

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

       return cmdSeq;