-------------------- houd1.bpl --------------------
Assignment computed by Houdini:
b1 = False

Boogie program verifier finished with 1 verified, 0 errors

-------------------- houd2.bpl --------------------
Assignment computed by Houdini:
b1 = False
b2 = True
houd2.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
houd2.bpl(9,1): Related location: This is the postcondition that might not hold.
Execution trace:
    houd2.bpl(11,3): anon0

Boogie program verifier finished with 1 verified, 1 error

-------------------- houd3.bpl --------------------
Assignment computed by Houdini:
b1 = False
b2 = False

Boogie program verifier finished with 2 verified, 0 errors

-------------------- houd4.bpl --------------------
Assignment computed by Houdini:
b1 = True
b2 = True
b3 = True
b4 = True

Boogie program verifier finished with 2 verified, 0 errors

-------------------- houd5.bpl --------------------
Assignment computed by Houdini:
b1 = False
b2 = True
b3 = False
b4 = True
b5 = True

Boogie program verifier finished with 2 verified, 0 errors

-------------------- houd6.bpl --------------------
Assignment computed by Houdini:
b1 = False
b2 = False
b3 = False
b4 = False
b5 = False
b6 = False
b7 = False
b8 = False

Boogie program verifier finished with 3 verified, 0 errors

-------------------- houd7.bpl --------------------
Assignment computed by Houdini:
b1 = True
b2 = False
b3 = False

Boogie program verifier finished with 2 verified, 0 errors

-------------------- houd8.bpl --------------------
Assignment computed by Houdini:
b1 = True
b2 = False
b3 = False

Boogie program verifier finished with 1 verified, 0 errors

-------------------- houd9.bpl --------------------
Assignment computed by Houdini:
b1 = True
b2 = True
b3 = True
houd9.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
    houd9.bpl(18,9): anon0

Boogie program verifier finished with 0 verified, 1 error

-------------------- houd10.bpl --------------------
Assignment computed by Houdini:
b1 = True
b2 = True
b3 = True
houd10.bpl(15,3): Error BP5002: A precondition for this call might not hold.
houd10.bpl(20,1): Related location: This is the precondition that might not hold.
Execution trace:
    houd10.bpl(14,9): anon0

Boogie program verifier finished with 0 verified, 1 error

-------------------- houd11.bpl --------------------
Assignment computed by Houdini:
houd11.bpl(8,3): Error BP5001: This assertion might not hold.
Execution trace:
    houd11.bpl(7,9): anon0

Boogie program verifier finished with 0 verified, 1 error

-------------------- houd12.bpl --------------------
Assignment computed by Houdini:
b1 = False
b2 = True
b3 = True
b4 = True
b5 = True
b6 = False
b7 = False

Boogie program verifier finished with 1 verified, 0 errors
.
-------------------- test1.bpl --------------------
Assignment computed by Houdini:
b0 = True
b1 = False
b2 = False

Boogie program verifier finished with 4 verified, 0 errors
.
-------------------- test2.bpl --------------------
Assignment computed by Houdini:
b0 = True
b1 = False
b2 = False

Boogie program verifier finished with 4 verified, 0 errors
.
-------------------- test7.bpl --------------------
Assignment computed by Houdini:

Boogie program verifier finished with 2 verified, 0 errors
.
-------------------- test8.bpl --------------------
Assignment computed by Houdini:

Boogie program verifier finished with 2 verified, 0 errors
.
-------------------- test9.bpl --------------------
Assignment computed by Houdini:
b1 = False
b2 = False
b3 = False
b4 = True
b5 = False
b6 = True
b7 = False
b8 = False
b9 = False
b10 = True
b11 = False
b12 = True
b13 = False
b14 = False
b15 = False
b16 = False

Boogie program verifier finished with 5 verified, 0 errors
.
-------------------- test10.bpl --------------------
Assignment computed by Houdini:
b1 = True
b2 = True
b3 = True
b4 = True

Boogie program verifier finished with 5 verified, 0 errors