4 files changed, 20 insertions, 9 deletions
diff --git a/Test/og/Answer b/Test/og/Answer
index 154b0193..5264da4a 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -3,7 +3,7 @@
 foo.bpl(13,3): Error BP5001: This assertion might not hold.
 Execution trace:
     foo.bpl(5,5): anon0
-    (0,0): inline$YieldChecker_PC$0$L1
+    (0,0): inline$Impl_YieldChecker_PC$0$L0
 
 Boogie program verifier finished with 3 verified, 1 error
 
@@ -11,11 +11,11 @@ Boogie program verifier finished with 3 verified, 1 error
 bar.bpl(12,3): Error BP5001: This assertion might not hold.
 Execution trace:
     bar.bpl(5,5): anon0
-    (0,0): inline$YieldChecker_PC$0$L1
+    (0,0): inline$Impl_YieldChecker_PC$0$L0
 bar.bpl(12,3): Error BP5001: This assertion might not hold.
 Execution trace:
     bar.bpl(17,5): anon0
-    (0,0): inline$YieldChecker_PC$0$L1
+    (0,0): inline$Impl_YieldChecker_PC$0$L0
 
 Boogie program verifier finished with 2 verified, 2 errors
 
@@ -27,11 +27,11 @@ Boogie program verifier finished with 2 verified, 0 errors
 parallel1.bpl(9,3): Error BP5001: This assertion might not hold.
 Execution trace:
     parallel1.bpl(5,5): anon0
-    (0,0): inline$YieldChecker_PC$0$L1
+    (0,0): inline$Proc_YieldChecker_PC$0$L0
 parallel1.bpl(13,3): Error BP5001: This assertion might not hold.
 Execution trace:
     parallel1.bpl(5,5): anon0
-    (0,0): inline$YieldChecker_PC$0$L2
+    (0,0): inline$Impl_YieldChecker_PC$0$L0
 
 Boogie program verifier finished with 3 verified, 2 errors
 
@@ -63,12 +63,18 @@ Boogie program verifier finished with 4 verified, 0 errors
 parallel4.bpl(14,3): Error BP5001: This assertion might not hold.
 Execution trace:
     parallel4.bpl(12,3): anon0
-    (0,0): inline$YieldChecker_t$0$enter
-    (0,0): inline$YieldChecker_t$0$exit
-    parallel4.bpl(12,3): anon0$2
+    parallel4.bpl(12,3): anon0$1
 
 Boogie program verifier finished with 2 verified, 1 error
 
 -------------------- parallel5.bpl --------------------
 
 Boogie program verifier finished with 4 verified, 0 errors
+
+-------------------- parallel6.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- parallel7.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/og/parallel6.bpl b/Test/og/parallel6.bpl
new file mode 100644
index 00000000..dba3eb2b
--- /dev/null
+++ b/Test/og/parallel6.bpl
@@ -0,0 +1,2 @@
+procedure A();
+procedure C() { async call A(); }
diff --git a/Test/og/parallel7.bpl b/Test/og/parallel7.bpl
new file mode 100644
index 00000000..79c92196
--- /dev/null
+++ b/Test/og/parallel7.bpl
@@ -0,0 +1,3 @@
+procedure A();
+procedure B();
+procedure C() { call A() | B(); }
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 64c21618..4009b62f 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do (
   %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
 )
 
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl) do (
   echo.
   echo -------------------- %%f --------------------
   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis  /OwickiGries:OwickiGriesDesugared.bpl %%f