fixed a bug in block coalescer. previously, an unreachable block could have as a target a block that was coalesced. this caused a contract to fail downstream (under checked build). in the new behavior, the new blocks after coalescing only contain reachable blocks.

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index c1270eab..3c2b9a42 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -332,7 +332,7 @@ namespace Microsoft.Boogie {
       List<Block/*!*/> newBlocks = new List<Block/*!*/>();

       foreach (Block/*!*/ b in impl.Blocks) {

         Contract.Assert(b != null);

-        if (!removedBlocks.Contains(b)) {

+        if (visitedBlocks.Contains(b) && !removedBlocks.Contains(b)) {

           newBlocks.Add(b);

         }

       }