1 2 3 4 5
Assignment computed by Houdini: b1 = False b2 = False Boogie program verifier finished with 2 verified, 0 errors