Merge

1 files changed, 21 insertions, 0 deletions

diff --git a/Test/AbsHoudini/imp1.bpl b/Test/AbsHoudini/imp1.bpl
new file mode 100644
index 00000000..29cbf567
--- /dev/null
+++ b/Test/AbsHoudini/imp1.bpl
@@ -0,0 +1,21 @@
+function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool;

+function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool;

+

+var x: int;

+var flag: bool;

+

+procedure foo ()

+  modifies x, flag;

+  ensures b1(flag, x == 0);

+{

+   flag := true;

+   x := 0;

+}

+

+procedure bar()

+  modifies x, flag;

+  ensures b2(flag, x == 0);

+{

+   flag := false;

+   x := 0;

+}