diff options
Diffstat (limited to 'Test/AbsHoudini/houd10.bpl')
| -rw-r--r-- | Test/AbsHoudini/houd10.bpl | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/Test/AbsHoudini/houd10.bpl b/Test/AbsHoudini/houd10.bpl new file mode 100644 index 00000000..bb0c65e7 --- /dev/null +++ b/Test/AbsHoudini/houd10.bpl @@ -0,0 +1,22 @@ +function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} Assert(): bool;
+var fooVar: int;
+var xVar: int;
+
+procedure foo()
+modifies fooVar;
+modifies xVar;
+ensures b1() || fooVar==0;
+ensures b3() || xVar<0;
+{
+ fooVar:=5;
+ call bar();
+}
+
+procedure bar();
+modifies xVar;
+requires Assert() || fooVar!=5;
+
+// expected assigment: Assert->true,b1->True,b2->false,b3->True
|