From f67d7393fd8294e8e9b36f44e16ec207732f8e3b Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 6 Oct 2014 11:21:11 +0100
Subject: Improved on my fix to the Duplicator bug fixed in ca82591ab1f8.
 Instead of the Duplicator maintaining state the VisitImplementation() method
 computes the mapping between old and new Blocks.

---
 Source/Core/Duplicator.cs | 21 +++++++++------------
 1 file changed, 9 insertions(+), 12 deletions(-)

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index a351e205..9843a2c6 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -14,8 +14,6 @@ using System.Linq;
 
 namespace Microsoft.Boogie {
   public class Duplicator : StandardVisitor {
-    // Used to resolve GotoCmd labelTargets by VisitImplementation after duplication
-    private Dictionary<Block,Block> BlockDuplicationMapping = null;
 
     public override Absy Visit(Absy node) {
       //Contract.Requires(node != null);
@@ -73,12 +71,7 @@ namespace Microsoft.Boogie {
     public override Block VisitBlock(Block node) {
       //Contract.Requires(node != null);
       Contract.Ensures(Contract.Result<Block>() != null);
-      var newBlock = base.VisitBlock((Block) node.Clone());
-
-      if (BlockDuplicationMapping != null)
-        BlockDuplicationMapping[node] = newBlock;
-
-      return newBlock;
+      return base.VisitBlock((Block) node.Clone());
     }
     public override BvConcatExpr VisitBvConcatExpr (BvConcatExpr node) {
       Contract.Ensures(Contract.Result<BvConcatExpr>() != null);
@@ -251,9 +244,14 @@ namespace Microsoft.Boogie {
     public override Implementation VisitImplementation(Implementation node) {
       //Contract.Requires(node != null);
       Contract.Ensures(Contract.Result<Implementation>() != null);
-      BlockDuplicationMapping = new Dictionary<Block, Block>();
-
       var impl = base.VisitImplementation((Implementation)node.Clone());
+      var blockDuplicationMapping = new Dictionary<Block, Block>();
+
+      // Compute the mapping between the blocks of the old implementation (node)
+      // and the new implementation (impl).
+      foreach (var blockPair in node.Blocks.Zip(impl.Blocks)) {
+        blockDuplicationMapping.Add(blockPair.Item1, blockPair.Item2);
+      }
 
       // The GotoCmds and blocks have now been duplicated.
       // Resolve GotoCmd targets to the duplicated blocks
@@ -261,14 +259,13 @@ namespace Microsoft.Boogie {
         var newLabelTargets = new List<Block>();
         var newLabelNames = new List<string>();
         for (int index = 0; index < gotoCmd.labelTargets.Count; ++index) {
-          var newBlock = BlockDuplicationMapping[gotoCmd.labelTargets[index]];
+          var newBlock = blockDuplicationMapping[gotoCmd.labelTargets[index]];
           newLabelTargets.Add(newBlock);
           newLabelNames.Add(newBlock.Label);
         }
         gotoCmd.labelTargets = newLabelTargets;
         gotoCmd.labelNames = newLabelNames;
       }
-      BlockDuplicationMapping.Clear();
 
       return impl;
     }
-- 
cgit v1.2.3