added another sample

1 files changed, 17 insertions, 0 deletions

diff --git a/Test/og/termination.bpl b/Test/og/termination.bpl
new file mode 100644
index 00000000..80109bf4
--- /dev/null
+++ b/Test/og/termination.bpl
@@ -0,0 +1,17 @@
+procedure {:yields} X();

+ensures {:atomic 0} |{ A: return true; }|;

+

+procedure {:yields} Y();

+ensures {:left 0} |{ A: return true; }|;

+

+procedure {:yields} main() {

+  yield;

+  call X();

+  while (*)

+//  invariant {:terminates} true;

+  {

+    call Y();

+  }

+  yield;

+  assert {:phase 1} true;

+}
\ No newline at end of file