summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
authorGravatar Shuvendu Lahiri <shuvendu@microsoft.com>2015-10-27 17:40:33 -0700
committerGravatar Shuvendu Lahiri <shuvendu@microsoft.com>2015-10-27 17:40:33 -0700
commit02f5c060ca5ce6bff003034ed634c114d5592398 (patch)
tree272d491b09fc5606928de9325803b4345843c5d3 /Source/Core
parente037ca99cdc163ca43690aaef3c380ebc1ce1962 (diff)
fix for deterministicExtractLoops for nested loops
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/Absy.cs3
1 files changed, 2 insertions, 1 deletions
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