diff options
| author |  Shuvendu Lahiri <shuvendu@microsoft.com> | 2015-10-27 17:40:33 -0700 |
|---|---|---|
| committer | Shuvendu Lahiri <shuvendu@microsoft.com> | 2015-10-27 17:40:33 -0700 |
| commit | 02f5c060ca5ce6bff003034ed634c114d5592398 (patch) | |
| tree | 272d491b09fc5606928de9325803b4345843c5d3 /Source/Core | |
| parent | e037ca99cdc163ca43690aaef3c380ebc1ce1962 (diff) | |
fix for deterministicExtractLoops for nested loops
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.cs | 3 |
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 |