1 files changed, 489 insertions, 489 deletions
diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer
index f0136d80..2ab37f22 100644
--- a/Test/AbsHoudini/Answer
+++ b/Test/AbsHoudini/Answer
@@ -1,489 +1,489 @@
-
--------------------- houd1.bpl --------------------
-function {:existential true} {:inline} b1(x: bool) : bool
-{
-  true
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd2.bpl --------------------
-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
-
--------------------- houd3.bpl --------------------
-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
-
--------------------- houd4.bpl --------------------
-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
-
--------------------- houd5.bpl --------------------
-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
-
--------------------- houd6.bpl --------------------
-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
-
--------------------- houd7.bpl --------------------
-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
-
--------------------- houd8.bpl --------------------
-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
-
--------------------- houd10.bpl --------------------
-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
-
--------------------- houd11.bpl --------------------
-function {:existential true} {:inline} Assert() : bool
-{
-  true
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd12.bpl --------------------
-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
-
--------------------- fail1.bpl --------------------
-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
-.
--------------------- test1.bpl --------------------
-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
-.
--------------------- test2.bpl --------------------
-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
-.
--------------------- test7.bpl --------------------
-function {:existential true} {:inline} Assert() : bool
-{
-  false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- test8.bpl --------------------
-function {:existential true} {:inline} Assert() : bool
-{
-  false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- test9.bpl --------------------
-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
-.
--------------------- test10.bpl --------------------
-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
-.
--------------------- pred1.bpl --------------------
-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
-.
--------------------- pred2.bpl --------------------
-function {:existential true} {:inline} b0(x: bool) : bool
-{
-  x
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- pred3.bpl --------------------
-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
-.
--------------------- pred4.bpl --------------------
-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
-.
--------------------- pred5.bpl --------------------
-function {:existential true} {:inline} b1(x: bool) : bool
-{
-  x
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- quant1.bpl --------------------
-function {:existential true} {:absdomain "IA[Intervals]"} {:inline} b1(x: int) : bool
-{
-  x >= 0 && x <= 2
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- quant2.bpl --------------------
-function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
-{
-  x >= 0 && x <= 1
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- quant3.bpl --------------------
-function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
-{
-  x >= 0 && x <= 0
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- quant4.bpl --------------------
-function {:existential true} {:absdomain "IA[HoudiniConst]"} {:inline} b1() : bool
-{
-  true
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- quant5.bpl --------------------
-function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
-{
-  x >= 5 && x <= 5
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- houd1.bpl --------------------
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- houd2.bpl --------------------
+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
+
+-------------------- houd3.bpl --------------------
+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
+
+-------------------- houd4.bpl --------------------
+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
+
+-------------------- houd5.bpl --------------------
+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
+
+-------------------- houd6.bpl --------------------
+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
+
+-------------------- houd7.bpl --------------------
+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
+
+-------------------- houd8.bpl --------------------
+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
+
+-------------------- houd10.bpl --------------------
+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
+
+-------------------- houd11.bpl --------------------
+function {:existential true} {:inline} Assert() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- houd12.bpl --------------------
+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
+
+-------------------- fail1.bpl --------------------
+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
+.
+-------------------- test1.bpl --------------------
+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
+.
+-------------------- test2.bpl --------------------
+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
+.
+-------------------- test7.bpl --------------------
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- test8.bpl --------------------
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- test9.bpl --------------------
+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
+.
+-------------------- test10.bpl --------------------
+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
+.
+-------------------- pred1.bpl --------------------
+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
+.
+-------------------- pred2.bpl --------------------
+function {:existential true} {:inline} b0(x: bool) : bool
+{
+  x
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- pred3.bpl --------------------
+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
+.
+-------------------- pred4.bpl --------------------
+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
+.
+-------------------- pred5.bpl --------------------
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  x
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant1.bpl --------------------
+function {:existential true} {:absdomain "IA[Intervals]"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 2
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant2.bpl --------------------
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 1
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant3.bpl --------------------
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 0
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant4.bpl --------------------
+function {:existential true} {:absdomain "IA[HoudiniConst]"} {:inline} b1() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant5.bpl --------------------
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 5 && x <= 5
+}
+
+Boogie program verifier finished with 1 verified, 0 errors