added test example

boogie-org · Jan 2, 2024 · 4ade00f · 4ade00f
1 parent 9ddf3b1
commit 4ade00f
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 0 deletions.
diff --git a/Test/civl/regression-tests/qelim1.bpl 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;
+}
diff --git a/Test/civl/regression-tests/qelim1.bpl.expect b/Test/civl/regression-tests/qelim1.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@

		Boogie program verifier finished with 1 verified, 0 errors