fixed bugs in both parallel calls and linear stuff (reported by Chris)

also added improved error reporting suggested by Chris

1 files changed, 21 insertions, 0 deletions

diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
new file mode 100644
index 00000000..a5b2768f
--- /dev/null
+++ b/Test/og/parallel4.bpl
@@ -0,0 +1,21 @@
+var a:int;

+

+procedure {:entrypoint} main() 

+{

+  var {:linear "tid"} i: int;

+  var {:linear "tid"} j: int;

+  call i := t(i) | j := t(j);

+}

+

+procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+{

+  assume i == i';

+  call Yield();

+  assert a == old(a);

+  a := a + 1;

+}

+

+procedure Yield()

+{

+  yield;

+}