fixed loop bug

Author: shazqadeer

Source/Concurrency/YieldingProcChecker.cs

@@ -30,7 +30,8 @@ public static void AddCheckers(CivlTypeChecker civlTypeChecker, List<Declaration
         foreach (Implementation impl in program.Implementations.Where(impl => impl.Proc is YieldProcedureDecl).ToList())
         {
           var yieldProcedureDecl = (YieldProcedureDecl)impl.Proc;
-          if (yieldProcedureDecl.Layer > layerNum || yieldProcedureDecl.Layer == layerNum && !yieldProcedureDecl.HasMoverType)
+          if (yieldProcedureDecl.Layer > layerNum ||
+              yieldProcedureDecl.Layer == layerNum && !yieldProcedureDecl.HasMoverType)
           {
             duplicator.VisitImplementation(impl);
           }

Source/Concurrency/YieldingProcDuplicator.cs

@@ -194,7 +194,6 @@ public override Block VisitBlock(Block node)
     public override Cmd VisitAssertCmd(AssertCmd node)
     {
       var assertCmd = (AssertCmd)base.VisitAssertCmd(node);
-      bool insideLoopInvariantOfYieldingLoop = enclosingYieldingProc.YieldingLoops.ContainsKey(enclosingBlock) && inPredicatePhase;
       if (!node.Layers.Contains(layerNum))
       {
         assertCmd.Expr = Expr.True;
@@ -204,6 +203,7 @@ public override Cmd VisitAssertCmd(AssertCmd node)
       {
         return assertCmd;
       }
+      bool insideLoopInvariantOfYieldingLoop = enclosingYieldingProc.IsYieldingLoopHeaderAtProcedureLayer(enclosingBlock) && inPredicatePhase;
       if (insideLoopInvariantOfYieldingLoop)
       {
         return doRefinementCheck ? new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes) : assertCmd;

Source/Core/AST/Absy.cs

@@ -3432,7 +3432,7 @@ public List<CallCmd> DesugaredYieldEnsures
         return desugaredYieldEnsures;
       }
     }
-    
+
     public bool IsYieldingLoopHeader(Block block, int layerNum)
     {
       if (!YieldingLoops.ContainsKey(block))
@@ -3441,6 +3441,11 @@ public bool IsYieldingLoopHeader(Block block, int layerNum)
       }
       return layerNum <= YieldingLoops[block].Layer;
     }
+
+    public bool IsYieldingLoopHeaderAtProcedureLayer(Block block)
+    {
+      return IsYieldingLoopHeader(block, Layer);
+    }
   }
 
   public class LoopProcedure : Procedure