From 02f5c060ca5ce6bff003034ed634c114d5592398 Mon Sep 17 00:00:00 2001
From: Shuvendu Lahiri <shuvendu@microsoft.com>
Date: Tue, 27 Oct 2015 17:40:33 -0700
Subject: fix for deterministicExtractLoops for nested loops

---
 Source/Core/Absy.cs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Source')

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 8c04007b..d2243085 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -991,7 +991,8 @@ namespace Microsoft.Boogie {
                 //BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode
                 var loopNodes = GetBlocksInAllNaturalLoops(header, g); //var loopNodes = g.NaturalLoops(header, source); 
                 foreach(var bl in auxGotoCmd.labelTargets) {
-                    if (!loopNodes.Contains(bl)) {
+                    if (g.Nodes.Contains(bl) && //newly created blocks are not present in NaturalLoop(header, xx, g)
+                        !loopNodes.Contains(bl)) {
                         Block auxNewBlock = new Block();
                         auxNewBlock.Label = ((Block)bl).Label;
                         //these blocks may have read/write locals that are not present in naturalLoops
-- 
cgit v1.2.3