fixed a small bug

3 files changed, 27 insertions, 1 deletions

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index e5c5999d..79424303 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -386,7 +386,7 @@ namespace Microsoft.Boogie
             else if (callCmd.Proc.Modifies.Count == 0)
             {
                 if (callCmd.Outs.Count == 0)
-                    return false;
+                    return true;
                 var outputVar = callCmd.Outs[0].Decl;
                 Debug.Assert(localVarToLocalVariableInfo.ContainsKey(outputVar));
                 if (localVarToLocalVariableInfo[outputVar].isGhost)
diff --git a/Test/civl/chris5.bpl b/Test/civl/chris5.bpl
new file mode 100644
index 00000000..23ebe424
--- /dev/null
+++ b/Test/civl/chris5.bpl
@@ -0,0 +1,19 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var{:layer 1,1} g:int;
+
+procedure{:layer 1} P(x:int)
+  requires {:layer 1} x == 0;
+{
+}
+
+procedure{:yields}{:layer 1,2} Y(x:int)
+  ensures{:atomic} |{ A: return true; }|;
+{
+  yield;
+  
+  call P(x);
+  assert{:layer 1} x == 0;
+
+  yield;
+}
diff --git a/Test/civl/chris5.bpl.expect b/Test/civl/chris5.bpl.expect
new file mode 100644
index 00000000..32b474f5
--- /dev/null
+++ b/Test/civl/chris5.bpl.expect
@@ -0,0 +1,7 @@
+chris5.bpl(15,3): Error BP5002: A precondition for this call might not hold.
+chris5.bpl(6,3): Related location: This is the precondition that might not hold.
+Execution trace:
+    chris5.bpl(13,3): anon0
+    (0,0): anon00
+
+Boogie program verifier finished with 1 verified, 1 error