From f4fa1a77026cf5c2809ff09000985efe120d76dd Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <shaz.qadeer@gmail.com>
Date: Sat, 26 Oct 2024 09:07:03 -0700
Subject: [PATCH] first commit

---
 .../mover-proc-in-parcall.bpl                 | 67 +++++++++++++++++++
 .../mover-proc-in-parcall.bpl.expect          |  2 +
 2 files changed, 69 insertions(+)
 create mode 100644 Test/civl/regression-tests/mover-proc-in-parcall.bpl
 create mode 100644 Test/civl/regression-tests/mover-proc-in-parcall.bpl.expect

diff --git a/Test/civl/regression-tests/mover-proc-in-parcall.bpl b/Test/civl/regression-tests/mover-proc-in-parcall.bpl
new file mode 100644
index 000000000..822dac093
--- /dev/null
+++ b/Test/civl/regression-tests/mover-proc-in-parcall.bpl
@@ -0,0 +1,67 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var {:layer 0,1} x: int;
+
+yield procedure {:layer 0} Incr();
+refines both action {:layer 1} _ {
+    x := x + 1;
+}
+
+yield right procedure {:layer 1} A()
+modifies x;
+ensures {:layer 1} x == old(x) + 2;
+{
+    par Incr() | Incr();
+}
+
+yield right procedure {:layer 1} B()
+modifies x;
+ensures {:layer 1} x == old(x) + 4;
+{
+    par A() | A();
+}
+
+yield right procedure {:layer 1} R1(i: int)
+modifies x;
+requires {:layer 1} 0 <= i;
+ensures {:layer 1} x == old(x) + i;
+{
+    if (i == 0) {
+        return;
+    }
+    par Incr() | R1(i-1);
+}
+
+yield right procedure {:layer 1} R2(i: int)
+modifies x;
+requires {:layer 1} 0 <= i;
+ensures {:layer 1} x == old(x) + i;
+{
+    if (i == 0) {
+        return;
+    }
+    par R2(i-1) | Incr();
+}
+
+yield right procedure {:layer 1} M1(i: int)
+modifies x;
+requires {:layer 1} 0 <= i;
+ensures {:layer 1} x == old(x) + i;
+{
+    if (i == 0) {
+        return;
+    }
+    par Incr() | M2(i-1);
+}
+
+yield right procedure {:layer 1} M2(i: int)
+modifies x;
+requires {:layer 1} 0 <= i;
+ensures {:layer 1} x == old(x) + i;
+{
+    if (i == 0) {
+        return;
+    }
+    par M1(i-1) | Incr();
+}
\ No newline at end of file
diff --git a/Test/civl/regression-tests/mover-proc-in-parcall.bpl.expect b/Test/civl/regression-tests/mover-proc-in-parcall.bpl.expect
new file mode 100644
index 000000000..9823d44a8
--- /dev/null
+++ b/Test/civl/regression-tests/mover-proc-in-parcall.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 6 verified, 0 errors