Convert the AbsHoudini tests to lit tests. They weren't being run by the old

infrastructure so I have not bothered to update the Answer file. These tests
are still disabled by the lit.local.cfg file in the AbsHoudini folder because
the following tests fail or weren't even being run previously (these are left
unresolved because I do not know how these tests are meant to be run)

UNRESOLVED: Boogie :: AbsHoudini/f1.bpl (1 of 32)
UNRESOLVED: Boogie :: AbsHoudini/imp1.bpl (7 of 32)
UNRESOLVED: Boogie :: AbsHoudini/int1.bpl (8 of 32)
UNRESOLVED: Boogie :: AbsHoudini/multi.bpl (9 of 32)
FAIL: Boogie :: AbsHoudini/quant3.bpl (22 of 32)
FAIL: Boogie :: AbsHoudini/quant5.bpl (28 of 32)

56 files changed, 489 insertions, 0 deletions

diff --git a/Test/AbsHoudini/fail1.bpl b/Test/AbsHoudini/fail1.bpl
index abbd015b..5e15340c 100644
--- a/Test/AbsHoudini/fail1.bpl
+++ b/Test/AbsHoudini/fail1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1(x: bool) : bool;

 

 var myVar: int;

diff --git a/Test/AbsHoudini/fail1.bpl.expect b/Test/AbsHoudini/fail1.bpl.expect
new file mode 100644
index 00000000..e987f773
--- /dev/null
+++ b/Test/AbsHoudini/fail1.bpl.expect
@@ -0,0 +1,11 @@
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  false
+}
+fail1.bpl(16,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    fail1.bpl(11,3): anon0
+    fail1.bpl(12,11): anon4_Then
+    fail1.bpl(16,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/AbsHoudini/houd1.bpl b/Test/AbsHoudini/houd1.bpl
index fc3d5713..0a8ebeb3 100644
--- a/Test/AbsHoudini/houd1.bpl
+++ b/Test/AbsHoudini/houd1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1(x: bool) : bool;

 

 var myVar: int;

diff --git a/Test/AbsHoudini/houd1.bpl.expect b/Test/AbsHoudini/houd1.bpl.expect
new file mode 100644
index 00000000..0b023466
--- /dev/null
+++ b/Test/AbsHoudini/houd1.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd10.bpl b/Test/AbsHoudini/houd10.bpl
index bb0c65e7..6ee73b9a 100644
--- a/Test/AbsHoudini/houd10.bpl
+++ b/Test/AbsHoudini/houd10.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1():bool;

 function {:existential true} b2():bool;

 function {:existential true} b3():bool;

diff --git a/Test/AbsHoudini/houd10.bpl.expect b/Test/AbsHoudini/houd10.bpl.expect
new file mode 100644
index 00000000..d427a9f2
--- /dev/null
+++ b/Test/AbsHoudini/houd10.bpl.expect
@@ -0,0 +1,18 @@
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  false
+}
+function {:existential true} {:inline} b3() : bool
+{
+  true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd11.bpl b/Test/AbsHoudini/houd11.bpl
index 78087744..dbde4f37 100644
--- a/Test/AbsHoudini/houd11.bpl
+++ b/Test/AbsHoudini/houd11.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert() : bool;

 

 var fooVar: int;

diff --git a/Test/AbsHoudini/houd11.bpl.expect b/Test/AbsHoudini/houd11.bpl.expect
new file mode 100644
index 00000000..13aff08c
--- /dev/null
+++ b/Test/AbsHoudini/houd11.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} Assert() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd12.bpl b/Test/AbsHoudini/houd12.bpl
index b3a1a6db..ac46ef62 100644
--- a/Test/AbsHoudini/houd12.bpl
+++ b/Test/AbsHoudini/houd12.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 // Example to test candidate annotations on loops

 

 function {:existential true} Assert(): bool;

diff --git a/Test/AbsHoudini/houd12.bpl.expect b/Test/AbsHoudini/houd12.bpl.expect
new file mode 100644
index 00000000..aefaac93
--- /dev/null
+++ b/Test/AbsHoudini/houd12.bpl.expect
@@ -0,0 +1,34 @@
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  false
+}
+function {:existential true} {:inline} b3() : bool
+{
+  false
+}
+function {:existential true} {:inline} b4() : bool
+{
+  false
+}
+function {:existential true} {:inline} b5() : bool
+{
+  false
+}
+function {:existential true} {:inline} b6() : bool
+{
+  true
+}
+function {:existential true} {:inline} b7() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd2.bpl b/Test/AbsHoudini/houd2.bpl
index fd2611e2..c4d8e4e0 100644
--- a/Test/AbsHoudini/houd2.bpl
+++ b/Test/AbsHoudini/houd2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert(x:bool) : bool;

 function {:existential true} b1 (x:bool):bool;

 function {:existential true} b2 (x:bool):bool;

diff --git a/Test/AbsHoudini/houd2.bpl.expect b/Test/AbsHoudini/houd2.bpl.expect
new file mode 100644
index 00000000..6fe401ad
--- /dev/null
+++ b/Test/AbsHoudini/houd2.bpl.expect
@@ -0,0 +1,14 @@
+function {:existential true} {:inline} Assert(x: bool) : bool
+{
+  true
+}
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  true
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd3.bpl b/Test/AbsHoudini/houd3.bpl
index 81f11018..a37b5874 100644
--- a/Test/AbsHoudini/houd3.bpl
+++ b/Test/AbsHoudini/houd3.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert(x: bool) : bool;

 function {:existential true} b1(x: bool) : bool;

 function {:existential true} b2(x: bool) : bool;

diff --git a/Test/AbsHoudini/houd3.bpl.expect b/Test/AbsHoudini/houd3.bpl.expect
new file mode 100644
index 00000000..780edc91
--- /dev/null
+++ b/Test/AbsHoudini/houd3.bpl.expect
@@ -0,0 +1,14 @@
+function {:existential true} {:inline} Assert(x: bool) : bool
+{
+  x
+}
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  true
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd4.bpl b/Test/AbsHoudini/houd4.bpl
index 01ee6707..2fc339d9 100644
--- a/Test/AbsHoudini/houd4.bpl
+++ b/Test/AbsHoudini/houd4.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert() : bool;

 function {:existential true} b1():bool;

 function {:existential true} b2(x:bool):bool;

diff --git a/Test/AbsHoudini/houd4.bpl.expect b/Test/AbsHoudini/houd4.bpl.expect
new file mode 100644
index 00000000..a6756239
--- /dev/null
+++ b/Test/AbsHoudini/houd4.bpl.expect
@@ -0,0 +1,22 @@
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+function {:existential true} {:inline} b1() : bool
+{
+  false
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+  false
+}
+function {:existential true} {:inline} b3(x: bool) : bool
+{
+  false
+}
+function {:existential true} {:inline} b4(x: bool) : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd5.bpl b/Test/AbsHoudini/houd5.bpl
index afbaa81c..8a08b5cf 100644
--- a/Test/AbsHoudini/houd5.bpl
+++ b/Test/AbsHoudini/houd5.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1(x:bool):bool;

 function {:existential true} b2(x:bool):bool;

 function {:existential true} b3(x:bool):bool;

diff --git a/Test/AbsHoudini/houd5.bpl.expect b/Test/AbsHoudini/houd5.bpl.expect
new file mode 100644
index 00000000..12144524
--- /dev/null
+++ b/Test/AbsHoudini/houd5.bpl.expect
@@ -0,0 +1,26 @@
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  !x
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+  x
+}
+function {:existential true} {:inline} b3(x: bool) : bool
+{
+  !x
+}
+function {:existential true} {:inline} b4(x: bool) : bool
+{
+  x
+}
+function {:existential true} {:inline} b5() : bool
+{
+  false
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd6.bpl b/Test/AbsHoudini/houd6.bpl
index e4927901..209e2f01 100644
--- a/Test/AbsHoudini/houd6.bpl
+++ b/Test/AbsHoudini/houd6.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1():bool;

 function {:existential true} b2():bool;

 function {:existential true} b3():bool;

diff --git a/Test/AbsHoudini/houd6.bpl.expect b/Test/AbsHoudini/houd6.bpl.expect
new file mode 100644
index 00000000..f5c02d70
--- /dev/null
+++ b/Test/AbsHoudini/houd6.bpl.expect
@@ -0,0 +1,38 @@
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} b3() : bool
+{
+  true
+}
+function {:existential true} {:inline} b4() : bool
+{
+  true
+}
+function {:existential true} {:inline} b5() : bool
+{
+  true
+}
+function {:existential true} {:inline} b6() : bool
+{
+  true
+}
+function {:existential true} {:inline} b7() : bool
+{
+  true
+}
+function {:existential true} {:inline} b8() : bool
+{
+  true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd7.bpl b/Test/AbsHoudini/houd7.bpl
index ef3293db..6df7b428 100644
--- a/Test/AbsHoudini/houd7.bpl
+++ b/Test/AbsHoudini/houd7.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1():bool;

 function {:existential true} b2():bool;

 function {:existential true} b3():bool;

diff --git a/Test/AbsHoudini/houd7.bpl.expect b/Test/AbsHoudini/houd7.bpl.expect
new file mode 100644
index 00000000..ce1675e4
--- /dev/null
+++ b/Test/AbsHoudini/houd7.bpl.expect
@@ -0,0 +1,18 @@
+function {:existential true} {:inline} b1() : bool
+{
+  false
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} b3() : bool
+{
+  true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd8.bpl b/Test/AbsHoudini/houd8.bpl
index 8be7f3db..e5b88466 100644
--- a/Test/AbsHoudini/houd8.bpl
+++ b/Test/AbsHoudini/houd8.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1():bool;

 function {:existential true} b2():bool;

 function {:existential true} b3():bool;

diff --git a/Test/AbsHoudini/houd8.bpl.expect b/Test/AbsHoudini/houd8.bpl.expect
new file mode 100644
index 00000000..605ec988
--- /dev/null
+++ b/Test/AbsHoudini/houd8.bpl.expect
@@ -0,0 +1,14 @@
+function {:existential true} {:inline} b1() : bool
+{
+  false
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} b3() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred1.bpl b/Test/AbsHoudini/pred1.bpl
index fc37a15b..0c2d7f10 100644
--- a/Test/AbsHoudini/pred1.bpl
+++ b/Test/AbsHoudini/pred1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b0(x:bool, y:bool): bool;

 function {:existential true} b1(x:bool, y:bool): bool;

 function {:existential true} b2(x:bool, y:bool): bool;

diff --git a/Test/AbsHoudini/pred1.bpl.expect b/Test/AbsHoudini/pred1.bpl.expect
new file mode 100644
index 00000000..0e3d3333
--- /dev/null
+++ b/Test/AbsHoudini/pred1.bpl.expect
@@ -0,0 +1,14 @@
+function {:existential true} {:inline} b0(x: bool, y: bool) : bool
+{
+  x && !y
+}
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+  (y || x) && (!x || !y)
+}
+function {:existential true} {:inline} b2(x: bool, y: bool) : bool
+{
+  x && !y
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred2.bpl b/Test/AbsHoudini/pred2.bpl
index 3ce948ce..9e93495f 100644
--- a/Test/AbsHoudini/pred2.bpl
+++ b/Test/AbsHoudini/pred2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b0(x:bool): bool;

 

 var g: int;

diff --git a/Test/AbsHoudini/pred2.bpl.expect b/Test/AbsHoudini/pred2.bpl.expect
new file mode 100644
index 00000000..55e46035
--- /dev/null
+++ b/Test/AbsHoudini/pred2.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} b0(x: bool) : bool
+{
+  x
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred3.bpl b/Test/AbsHoudini/pred3.bpl
index 450efde4..1cb36798 100644
--- a/Test/AbsHoudini/pred3.bpl
+++ b/Test/AbsHoudini/pred3.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b0(x:bool, y:bool): bool;

 function {:existential true} b1(x:bool, y:bool): bool;

 function {:existential true} b2(x:bool, y:bool): bool;

diff --git a/Test/AbsHoudini/pred3.bpl.expect b/Test/AbsHoudini/pred3.bpl.expect
new file mode 100644
index 00000000..0e3d3333
--- /dev/null
+++ b/Test/AbsHoudini/pred3.bpl.expect
@@ -0,0 +1,14 @@
+function {:existential true} {:inline} b0(x: bool, y: bool) : bool
+{
+  x && !y
+}
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+  (y || x) && (!x || !y)
+}
+function {:existential true} {:inline} b2(x: bool, y: bool) : bool
+{
+  x && !y
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred4.bpl b/Test/AbsHoudini/pred4.bpl
index d4741720..9c814e3b 100644
--- a/Test/AbsHoudini/pred4.bpl
+++ b/Test/AbsHoudini/pred4.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1(x:bool, y:bool): bool;

 function {:existential true} {:absdomain "Intervals"} b3(x:int): bool;

 

diff --git a/Test/AbsHoudini/pred4.bpl.expect b/Test/AbsHoudini/pred4.bpl.expect
new file mode 100644
index 00000000..ec1d9517
--- /dev/null
+++ b/Test/AbsHoudini/pred4.bpl.expect
@@ -0,0 +1,10 @@
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+  (y || x) && (!x || !y)
+}
+function {:existential true} {:absdomain "Intervals"} {:inline} b3(x: int) : bool
+{
+  x >= 0 && x <= 0
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred5.bpl b/Test/AbsHoudini/pred5.bpl
index 6940e820..762a354f 100644
--- a/Test/AbsHoudini/pred5.bpl
+++ b/Test/AbsHoudini/pred5.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1(x: bool) : bool;

 

 procedure main() 

diff --git a/Test/AbsHoudini/pred5.bpl.expect b/Test/AbsHoudini/pred5.bpl.expect
new file mode 100644
index 00000000..a5e1c73d
--- /dev/null
+++ b/Test/AbsHoudini/pred5.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  x
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/quant1.bpl b/Test/AbsHoudini/quant1.bpl
index e12525b6..a5709736 100644
--- a/Test/AbsHoudini/quant1.bpl
+++ b/Test/AbsHoudini/quant1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} {:absdomain "IA[Intervals]"} b1(x: int) : bool;

 

 procedure foo ()

diff --git a/Test/AbsHoudini/quant1.bpl.expect b/Test/AbsHoudini/quant1.bpl.expect
new file mode 100644
index 00000000..7d06cb21
--- /dev/null
+++ b/Test/AbsHoudini/quant1.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:absdomain "IA[Intervals]"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 2
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/quant2.bpl b/Test/AbsHoudini/quant2.bpl
index 5a491877..2f291fca 100644
--- a/Test/AbsHoudini/quant2.bpl
+++ b/Test/AbsHoudini/quant2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;

 

 procedure main() 

diff --git a/Test/AbsHoudini/quant2.bpl.expect b/Test/AbsHoudini/quant2.bpl.expect
new file mode 100644
index 00000000..0610db26
--- /dev/null
+++ b/Test/AbsHoudini/quant2.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 1
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/quant3.bpl b/Test/AbsHoudini/quant3.bpl
index cc0ef79e..10fb72c7 100644
--- a/Test/AbsHoudini/quant3.bpl
+++ b/Test/AbsHoudini/quant3.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;

 

 procedure foo ()

diff --git a/Test/AbsHoudini/quant3.bpl.expect b/Test/AbsHoudini/quant3.bpl.expect
new file mode 100644
index 00000000..d43073ab
--- /dev/null
+++ b/Test/AbsHoudini/quant3.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 0
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/quant4.bpl b/Test/AbsHoudini/quant4.bpl
index 55947f1f..99c37572 100644
--- a/Test/AbsHoudini/quant4.bpl
+++ b/Test/AbsHoudini/quant4.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} {:absdomain "IA[HoudiniConst]"} b1() : bool;

 

 procedure foo ()

diff --git a/Test/AbsHoudini/quant4.bpl.expect b/Test/AbsHoudini/quant4.bpl.expect
new file mode 100644
index 00000000..07f98295
--- /dev/null
+++ b/Test/AbsHoudini/quant4.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:absdomain "IA[HoudiniConst]"} {:inline} b1() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/quant5.bpl b/Test/AbsHoudini/quant5.bpl
index dfc44e47..83e6e68a 100644
--- a/Test/AbsHoudini/quant5.bpl
+++ b/Test/AbsHoudini/quant5.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;

 

 procedure foo ()

diff --git a/Test/AbsHoudini/quant5.bpl.expect b/Test/AbsHoudini/quant5.bpl.expect
new file mode 100644
index 00000000..b74f5abc
--- /dev/null
+++ b/Test/AbsHoudini/quant5.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 5 && x <= 5
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test1.bpl b/Test/AbsHoudini/test1.bpl
index 5884cf7b..ba18cf15 100644
--- a/Test/AbsHoudini/test1.bpl
+++ b/Test/AbsHoudini/test1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 var g: bool;

 

 procedure foo() 

diff --git a/Test/AbsHoudini/test1.bpl.expect b/Test/AbsHoudini/test1.bpl.expect
new file mode 100644
index 00000000..ecc2a8fd
--- /dev/null
+++ b/Test/AbsHoudini/test1.bpl.expect
@@ -0,0 +1,18 @@
+function {:existential true} {:inline} b0() : bool
+{
+  false
+}
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl
index a30c3159..76a02e23 100644
--- a/Test/AbsHoudini/test10.bpl
+++ b/Test/AbsHoudini/test10.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 var sdv_7: int;

 var sdv_21: int;

 function {:existential true} b1(): bool;

diff --git a/Test/AbsHoudini/test10.bpl.expect b/Test/AbsHoudini/test10.bpl.expect
new file mode 100644
index 00000000..c9e99b13
--- /dev/null
+++ b/Test/AbsHoudini/test10.bpl.expect
@@ -0,0 +1,18 @@
+function {:existential true} {:inline} b1() : bool
+{
+  false
+}
+function {:existential true} {:inline} b2() : bool
+{
+  false
+}
+function {:existential true} {:inline} b3() : bool
+{
+  false
+}
+function {:existential true} {:inline} b4() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test2.bpl b/Test/AbsHoudini/test2.bpl
index bfd78363..8c1717bf 100644
--- a/Test/AbsHoudini/test2.bpl
+++ b/Test/AbsHoudini/test2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 var g: int;

 var h: int;

 

diff --git a/Test/AbsHoudini/test2.bpl.expect b/Test/AbsHoudini/test2.bpl.expect
new file mode 100644
index 00000000..ecc2a8fd
--- /dev/null
+++ b/Test/AbsHoudini/test2.bpl.expect
@@ -0,0 +1,18 @@
+function {:existential true} {:inline} b0() : bool
+{
+  false
+}
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test7.bpl b/Test/AbsHoudini/test7.bpl
index bfe8a32d..d9500308 100644
--- a/Test/AbsHoudini/test7.bpl
+++ b/Test/AbsHoudini/test7.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert() : bool;

 

 var g: int;

diff --git a/Test/AbsHoudini/test7.bpl.expect b/Test/AbsHoudini/test7.bpl.expect
new file mode 100644
index 00000000..82afc94e
--- /dev/null
+++ b/Test/AbsHoudini/test7.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test8.bpl b/Test/AbsHoudini/test8.bpl
index 6c55016a..0b00bc19 100644
--- a/Test/AbsHoudini/test8.bpl
+++ b/Test/AbsHoudini/test8.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert(): bool;

 

 var g: int;

diff --git a/Test/AbsHoudini/test8.bpl.expect b/Test/AbsHoudini/test8.bpl.expect
new file mode 100644
index 00000000..82afc94e
--- /dev/null
+++ b/Test/AbsHoudini/test8.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl
index c08edf6b..221234e5 100644
--- a/Test/AbsHoudini/test9.bpl
+++ b/Test/AbsHoudini/test9.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 var v1: int;

 var v2: int;

 var v3: int;

diff --git a/Test/AbsHoudini/test9.bpl.expect b/Test/AbsHoudini/test9.bpl.expect
new file mode 100644
index 00000000..ae5e9286
--- /dev/null
+++ b/Test/AbsHoudini/test9.bpl.expect
@@ -0,0 +1,66 @@
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} b3() : bool
+{
+  true
+}
+function {:existential true} {:inline} b4() : bool
+{
+  false
+}
+function {:existential true} {:inline} b5() : bool
+{
+  true
+}
+function {:existential true} {:inline} b6() : bool
+{
+  false
+}
+function {:existential true} {:inline} b7() : bool
+{
+  true
+}
+function {:existential true} {:inline} b8() : bool
+{
+  true
+}
+function {:existential true} {:inline} b9() : bool
+{
+  true
+}
+function {:existential true} {:inline} b10() : bool
+{
+  false
+}
+function {:existential true} {:inline} b11() : bool
+{
+  true
+}
+function {:existential true} {:inline} b12() : bool
+{
+  false
+}
+function {:existential true} {:inline} b13() : bool
+{
+  true
+}
+function {:existential true} {:inline} b14() : bool
+{
+  true
+}
+function {:existential true} {:inline} b15() : bool
+{
+  true
+}
+function {:existential true} {:inline} b16() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors