AbsHoudini: Added support for quantifiers

1 files changed, 24 insertions, 0 deletions

diff --git a/Test/AbsHoudini/quant2.bpl b/Test/AbsHoudini/quant2.bpl
new file mode 100644
index 00000000..5a491877
--- /dev/null
+++ b/Test/AbsHoudini/quant2.bpl
@@ -0,0 +1,24 @@
+function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;

+

+procedure main() 

+{

+   var i: int;

+   var x: int;

+   var arr: [int] int;

+

+   i := 0;

+

+   while(*) 

+     invariant (i >= 0) && (forall j: int :: (0 <= j && j < i) ==> b1(arr[j]));

+   {

+       havoc x;

+       assume x == 0 || x == 1;

+

+       arr[i] := x;

+       i := i + 1;

+   }

+

+   havoc x;

+   assume x >= 0 && x < i;

+   assert arr[x] == 0 || arr[x] == 1;

+}