From 4ade00fc1ee2e21244b11106eab9ec3fe7c5aa7c Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <shaz.qadeer@gmail.com>
Date: Tue, 2 Jan 2024 13:58:54 -0800
Subject: [PATCH] added test example

---
 Test/civl/regression-tests/qelim1.bpl        | 14 ++++++++++++++
 Test/civl/regression-tests/qelim1.bpl.expect |  2 ++
 2 files changed, 16 insertions(+)
 create mode 100644 Test/civl/regression-tests/qelim1.bpl
 create mode 100644 Test/civl/regression-tests/qelim1.bpl.expect

diff --git a/Test/civl/regression-tests/qelim1.bpl b/Test/civl/regression-tests/qelim1.bpl
new file mode 100644
index 000000000..739dc5c19
--- /dev/null
+++ b/Test/civl/regression-tests/qelim1.bpl
@@ -0,0 +1,14 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+atomic action {:layer 2} AtomicFoo() returns (o: int)
+{
+    var y: int;
+    o := y;
+}
+yield procedure {:layer 1} Foo() returns (o: int) 
+refines AtomicFoo;
+{
+    var x: int;
+    o := x;
+}
\ No newline at end of file
diff --git a/Test/civl/regression-tests/qelim1.bpl.expect b/Test/civl/regression-tests/qelim1.bpl.expect
new file mode 100644
index 000000000..37fad75c9
--- /dev/null
+++ b/Test/civl/regression-tests/qelim1.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors