1 files changed, 13 insertions, 18 deletions
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index 5215bc52..430c0d2c 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -486,20 +486,27 @@ namespace Microsoft.Boogie
             }
         }
 
-        private HashSet<int> allCreatedLayerNums;
-        public IEnumerable<int> AllCreatedLayerNums
+        private HashSet<int> allLayerNums;
+        public IEnumerable<int> AllLayerNums
         {
             get
             {
-                if (allCreatedLayerNums == null)
+                if (allLayerNums == null)
                 {
-                    allCreatedLayerNums = new HashSet<int>();
+                    allLayerNums = new HashSet<int>();
                     foreach (ActionInfo actionInfo in procToActionInfo.Values)
                     {
-                        allCreatedLayerNums.Add(actionInfo.createdAtLayerNum);
+                        allLayerNums.Add(actionInfo.createdAtLayerNum);
+                    }
+                    foreach (var layerNums in absyToLayerNums.Values)
+                    {
+                        foreach (var layer in layerNums)
+                        {
+                            allLayerNums.Add(layer);
+                        }
                     }
                 }
-                return allCreatedLayerNums;
+                return allLayerNums;
             }
         }
 
@@ -705,18 +712,6 @@ namespace Microsoft.Boogie
                     Error(impl.Proc, "Extern procedure cannot have an implementation");
                 }
             }
-            foreach (var g in this.globalVarToSharedVarInfo.Keys)
-            {
-                var info = globalVarToSharedVarInfo[g];
-                if (!this.AllCreatedLayerNums.Contains(info.introLayerNum))
-                {
-                    Error(g, "Variable must be introduced with creation of some atomic action");
-                }
-                if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum))
-                {
-                    Error(g, "Variable must be hidden with creation of some atomic action");
-                }
-            }
             if (errorCount > 0) return;
             this.VisitProgram(program);
             if (errorCount > 0) return;