diff options
| author |  akashlal <unknown> | 2013-04-19 15:04:05 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2013-04-19 15:04:05 +0530 |
| commit | 6b1a07688a8996acd297b80afe3217aa11104f04 (patch) | |
| tree | aed6cf25b65dc6d5a604492ecc8f0bc32f2430c3 /Test/og | |
| parent | 442ebdbbe6a473cd4f8c325609308346722e4fc8 (diff) | |
Test case for OG --> Houdini
Diffstat (limited to 'Test/og')
| -rw-r--r-- | Test/og/houd1.bpl | 21 |
1 files changed, 21 insertions, 0 deletions
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);
+}
+
|