-------------------- boog0.bpl -------------------- boog0.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement. boog0.bpl(45,3): Related location: This is the postcondition that might not hold. Execution trace: boog0.bpl(48,7): anon0 Boogie program verifier finished with 1 verified, 1 error -------------------- boog1.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog2.bpl -------------------- boog2.bpl(23,1): Error BP5003: A postcondition might not hold at this return statement. boog2.bpl(19,3): Related location: This is the postcondition that might not hold. Execution trace: boog2.bpl(22,8): anon0 Boogie program verifier finished with 1 verified, 1 error -------------------- boog3.bpl -------------------- boog3.bpl(6,3): Error BP5001: This assertion might not hold. Execution trace: boog3.bpl(6,3): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog4.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog5.bpl -------------------- boog5.bpl(36,3): Error BP5003: A postcondition might not hold at this return statement. boog5.bpl(29,3): Related location: This is the postcondition that might not hold. Execution trace: boog5.bpl(32,3): anon0 boog5.bpl(35,13): anon3_Else Boogie program verifier finished with 0 verified, 1 error -------------------- boog6.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog7.bpl -------------------- boog7.bpl(17,1): Error BP5003: A postcondition might not hold at this return statement. boog7.bpl(13,3): Related location: This is the postcondition that might not hold. Execution trace: boog7.bpl(16,11): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog8.bpl -------------------- boog8.bpl(7,12): Error: no bitvector handling specified, please use /bv:i or /bv:z flag boog8.bpl(7,18): Error: no bitvector handling specified, please use /bv:i or /bv:z flag 2 type checking errors detected in boog8.bpl -------------------- boog9.bpl -------------------- boog9.bpl(19,1): Error BP5003: A postcondition might not hold at this return statement. boog9.bpl(15,3): Related location: This is the postcondition that might not hold. Execution trace: boog9.bpl(18,11): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog10.bpl -------------------- boog10.bpl(18,3): Error BP5001: This assertion might not hold. Execution trace: boog10.bpl(18,3): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog11.bpl -------------------- boog11.bpl(14,1): Error BP5003: A postcondition might not hold at this return statement. boog11.bpl(10,3): Related location: This is the postcondition that might not hold. Execution trace: boog11.bpl(13,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog12.bpl -------------------- boog12.bpl(18,1): Error BP5003: A postcondition might not hold at this return statement. boog12.bpl(13,3): Related location: This is the postcondition that might not hold. Execution trace: boog12.bpl(16,16): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog13.bpl -------------------- boog13.bpl(9,11): Error: more than one declaration of variable name: v 1 name resolution errors detected in boog13.bpl -------------------- boog14.bpl -------------------- boog14.bpl(11,1): Error BP5003: A postcondition might not hold at this return statement. boog14.bpl(8,1): Related location: This is the postcondition that might not hold. Execution trace: boog14.bpl(10,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog15.bpl -------------------- boog15.bpl(10,1): Error BP5003: A postcondition might not hold at this return statement. boog15.bpl(7,1): Related location: This is the postcondition that might not hold. Execution trace: boog15.bpl(9,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog16.bpl -------------------- boog16.bpl(11,1): Error BP5003: A postcondition might not hold at this return statement. boog16.bpl(8,1): Related location: This is the postcondition that might not hold. Execution trace: boog16.bpl(10,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog17.bpl -------------------- boog17.bpl(24,3): Error BP5001: This assertion might not hold. Execution trace: boog17.bpl(15,1): start boog17.bpl(19,1): label_3 boog17.bpl(22,1): label_4 Boogie program verifier finished with 0 verified, 1 error -------------------- boog18.bpl -------------------- boog18.bpl(15,1): Error BP5003: A postcondition might not hold at this return statement. boog18.bpl(12,1): Related location: This is the postcondition that might not hold. Execution trace: boog18.bpl(14,4): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog19.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog20.bpl -------------------- boog20.bpl(15,1): Error BP5001: This assertion might not hold. Execution trace: boog20.bpl(15,1): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog21.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog22.bpl -------------------- boog22.bpl(4,9): Error: more than one declaration of function/procedure name: f1 1 name resolution errors detected in boog22.bpl -------------------- boog23.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog24.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog25.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog28.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog29.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog30.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog31.bpl -------------------- boog31.bpl(12,1): Error BP5001: This assertion might not hold. Execution trace: boog31.bpl(12,1): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog34.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors