From 0339351e985c455e7ecf290be54aa5361fe7ae8f Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sun, 9 Nov 2014 10:41:46 -0800
Subject: a fix to type checking

---
 Source/Concurrency/TypeCheck.cs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Source/Concurrency')

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 96b03ad9..657e3b06 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -466,13 +466,13 @@ namespace Microsoft.Boogie
                     numAtomicActions++;
                 }
             }
-            if (!isLeftMover && !isRightMover && node.CallCmds.Count > 1)
+            if (maxCalleePhaseNum < enclosingProcPhaseNum && !isLeftMover && !isRightMover && node.CallCmds.Count > 1)
             {
-                Error(node, "The procedures in the parallel call must be all right mover or all left mover");
+                Error(node, "The callees in the parallel call must be all right movers or all left movers");
             }
             if (maxCalleePhaseNum == enclosingProcPhaseNum && numAtomicActions > 0)
             {
-                Error(node, "At phase {0}, either no callee is an atomic action or no callee phase equals the phase of the enclosing procedure");
+                Error(node, "If some callee in the parallel call has the same phase as the enclosing procedure, then no callee can be an atomic action");
             }
             return base.VisitParCallCmd(node);
         }
-- 
cgit v1.2.3