1 files changed, 10 insertions, 1 deletions
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 402ea7dc..056a47f9 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -107,12 +107,21 @@ namespace Microsoft.Boogie {
     public override Cmd VisitCallCmd(CallCmd node) {
       //Contract.Requires(node != null);
       Contract.Ensures(Contract.Result<Cmd>() != null);
-      CallCmd/*!*/ clone = (CallCmd)node.Clone();
+      CallCmd clone = (CallCmd)node.Clone();
       Contract.Assert(clone != null);
       clone.Ins = new List<Expr>(clone.Ins);
       clone.Outs = new List<IdentifierExpr>(clone.Outs);
       return base.VisitCallCmd(clone);
     }
+    public override Cmd VisitParCallCmd(ParCallCmd node)
+    {
+        //Contract.Requires(node != null);
+        Contract.Ensures(Contract.Result<Cmd>() != null);
+        ParCallCmd clone = (ParCallCmd)node.Clone();
+        Contract.Assert(clone != null);
+        clone.CallCmds = new List<CallCmd>(node.CallCmds);
+        return base.VisitParCallCmd(clone);
+    }
     public override Choice VisitChoice(Choice node) {
       //Contract.Requires(node != null);
       Contract.Ensures(Contract.Result<Choice>() != null);