summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Shaz Qadeer <qadeer@microsoft.com>2015-09-26 21:19:33 -0700
committerGravatar Shaz Qadeer <qadeer@microsoft.com>2015-09-26 21:19:33 -0700
commit67ae2df042134ab49c5d9e055213b2c052033962 (patch)
treef3f8bd00c1628137dfde1fbe9de0f5a966cf425f /Source
parent5927744da636063556118f469cc8f9354b1cabe6 (diff)
removed a warning
Diffstat (limited to 'Source')
-rw-r--r--Source/Concurrency/TypeCheck.cs6
1 files changed, 1 insertions, 5 deletions
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 10127d33..e5c5999d 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -1083,11 +1083,7 @@ namespace Microsoft.Boogie
absyToLayerNums[node] = new HashSet<int>();
foreach (int layerNum in attrs)
{
- if (!AllImplementedLayerNums.Contains(layerNum))
- {
- Error(node, "Illegal layer number");
- }
- else if (layerNum > enclosingProcLayerNum)
+ if (layerNum > enclosingProcLayerNum)
{
Error(node, "The layer cannot be greater than the layer of enclosing procedure");
}