From 6b1a07688a8996acd297b80afe3217aa11104f04 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Fri, 19 Apr 2013 15:04:05 +0530
Subject: Test case for OG --> Houdini

---
 Test/og/houd1.bpl | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 Test/og/houd1.bpl

(limited to 'Test/og')

diff --git a/Test/og/houd1.bpl b/Test/og/houd1.bpl
new file mode 100644
index 00000000..aff53a48
--- /dev/null
+++ b/Test/og/houd1.bpl
@@ -0,0 +1,21 @@
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true} b2: bool;
+
+var x:int;
+
+procedure A()
+{
+  x := x + 1;
+  yield;
+}
+
+procedure B()
+{
+  x := 5;
+  yield;
+  assert b0 ==> (x == 5);
+  assert b1 ==> (x >= 5);
+  assert b2 ==> (x >= 6);
+}
+
-- 
cgit v1.2.3