From e7a15ef3363e69b24b70f0e5de5cecc56d501a2b Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <qadeer@microsoft.com>
Date: Sun, 27 Sep 2015 22:46:45 -0700
Subject: fixed a small bug

---
 Source/Concurrency/TypeCheck.cs |  2 +-
 Test/civl/chris5.bpl            | 19 +++++++++++++++++++
 Test/civl/chris5.bpl.expect     |  7 +++++++
 3 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 Test/civl/chris5.bpl
 create mode 100644 Test/civl/chris5.bpl.expect

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
-- 
cgit v1.2.3