another fix requested by Chris

verification is performed now for all created layers

3 files changed, 2 insertions, 22 deletions

diff --git a/Source/Concurrency/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs
index 43d0f60c..8fc27be9 100644
--- a/Source/Concurrency/CivlRefinement.cs
+++ b/Source/Concurrency/CivlRefinement.cs
@@ -1212,7 +1212,7 @@ namespace Microsoft.Boogie
         public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
             Program program = linearTypeChecker.program;
-            foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums)
+            foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums)
             {
                 if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;
 
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index dba7ab4b..5215bc52 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -486,26 +486,6 @@ namespace Microsoft.Boogie
             }
         }
 
-        private HashSet<int> allImplementedLayerNums;
-        public IEnumerable<int> AllImplementedLayerNums
-        {
-            get
-            {
-                if (allImplementedLayerNums == null)
-                {
-                    allImplementedLayerNums = new HashSet<int>();
-                    foreach (ActionInfo actionInfo in procToActionInfo.Values)
-                    {
-                        if (actionInfo.hasImplementation)
-                        {
-                            allImplementedLayerNums.Add(actionInfo.createdAtLayerNum);
-                        }
-                    }
-                }
-                return allImplementedLayerNums;
-            }
-        }
-
         private HashSet<int> allCreatedLayerNums;
         public IEnumerable<int> AllCreatedLayerNums
         {
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index a69f066d..027e7e83 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -141,7 +141,7 @@ namespace Microsoft.Boogie
                 Graph<Block> implGraph = Program.GraphFromImpl(impl);
                 implGraph.ComputeLoops();
                 int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
-                foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums)
+                foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums)
                 {
                     if (layerNum > specLayerNum) continue;
                     YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers);