various fixes

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 92ec7e1c..c6979fc7 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -154,12 +154,12 @@ namespace Microsoft.Boogie
             }

         }

 

-        private static bool IsTerminatingLoopHeader(Block block)

+        private bool IsTerminatingLoopHeader(Block block)

         {

             foreach (Cmd cmd in block.Cmds)

             {

                 AssertCmd assertCmd = cmd as AssertCmd;

-                if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates"))

+                if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && moverTypeChecker.absyToPhaseNums[assertCmd].Contains(currPhaseNum))

                 {

                     return true;

                 }