-------------------- 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