Fix for the Duplicator.

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 1d221bb7..ef958fa6 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -121,7 +121,7 @@ namespace Microsoft.Boogie {
     public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {

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

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

-      return base.VisitCmdSeq(cmdSeq);

+      return base.VisitCmdSeq(new List<Cmd>(cmdSeq));

     }

     public override Constant VisitConstant(Constant node) {

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