a fix to type checking

1 files changed, 3 insertions, 3 deletions

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);

         }