From 5dba06d46a3e8c044cd4cc2c254885da3ccc1bb2 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Wed, 21 Dec 2011 08:14:39 -0800
Subject: forgot to check it in

---
 Test/houdini/test10.bpl | 47 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 Test/houdini/test10.bpl

(limited to 'Test/houdini')

diff --git a/Test/houdini/test10.bpl b/Test/houdini/test10.bpl
new file mode 100644
index 00000000..abb993f7
--- /dev/null
+++ b/Test/houdini/test10.bpl
@@ -0,0 +1,47 @@
+var sdv_7: int;
+var sdv_21: int;
+const {:existential true} b1: bool;
+const{:existential true}  b2: bool;
+const{:existential true}  b3: bool;
+const{:existential true}  b4: bool;
+
+procedure push(a:int)
+modifies sdv_7, sdv_21;
+{
+   sdv_21 := sdv_7;
+   sdv_7 := a;
+}
+
+procedure pop()
+modifies sdv_7, sdv_21;
+{
+   sdv_7 := sdv_21;
+   havoc sdv_21;
+}
+
+procedure foo()
+modifies sdv_7, sdv_21;
+requires {:candidate} b1 ==> (sdv_7 == 0);
+ensures{:candidate}  b2 ==> (sdv_7 == old(sdv_7));
+{
+   call push(2);
+   call pop();
+   call bar();
+}
+
+procedure bar()
+requires{:candidate} b3 ==> (sdv_7 == 0);
+ensures{:candidate}  b4 ==> (sdv_7 == old(sdv_7));
+modifies sdv_7, sdv_21;
+{
+   call push(1);
+   call pop();
+}
+
+procedure main()
+modifies sdv_7, sdv_21;
+{
+   sdv_7 := 0;
+   call foo();
+}
+
-- 
cgit v1.2.3