-------------------- boog0.bpl -------------------- boog0.bpl(49,1): Error BP5003: A postcondition might not hold on this return path. boog0.bpl(43,3): Related location: This is the postcondition that might not hold. Execution trace: boog0.bpl(46,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(24,1): Error BP5003: A postcondition might not hold on this return path. boog2.bpl(20,3): Related location: This is the postcondition that might not hold. Execution trace: boog2.bpl(23,8): anon0 Boogie program verifier finished with 1 verified, 1 error -------------------- boog3.bpl -------------------- boog3.bpl(7,3): Error BP5001: This assertion might not hold. Execution trace: boog3.bpl(7,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(37,3): Error BP5003: A postcondition might not hold on this return path. boog5.bpl(30,3): Related location: This is the postcondition that might not hold. Execution trace: boog5.bpl(33,3): anon0 boog5.bpl(36,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(18,1): Error BP5003: A postcondition might not hold on this return path. boog7.bpl(14,3): Related location: This is the postcondition that might not hold. Execution trace: boog7.bpl(17,11): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog8.bpl -------------------- boog8.bpl(23,1): Error BP5003: A postcondition might not hold on this return path. boog8.bpl(19,3): Related location: This is the postcondition that might not hold. Execution trace: boog8.bpl(22,11): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog9.bpl -------------------- boog9.bpl(20,1): Error BP5003: A postcondition might not hold on this return path. boog9.bpl(16,3): Related location: This is the postcondition that might not hold. Execution trace: boog9.bpl(19,11): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog10.bpl -------------------- boog10.bpl(19,3): Error BP5001: This assertion might not hold. Execution trace: boog10.bpl(19,3): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog11.bpl -------------------- boog11.bpl(15,1): Error BP5003: A postcondition might not hold on this return path. boog11.bpl(11,3): Related location: This is the postcondition that might not hold. Execution trace: boog11.bpl(14,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog12.bpl -------------------- boog12.bpl(19,1): Error BP5003: A postcondition might not hold on this return path. boog12.bpl(14,3): Related location: This is the postcondition that might not hold. Execution trace: boog12.bpl(17,16): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog13.bpl -------------------- boog13.bpl(10,18): Error: more than one declaration of variable name: v 1 name resolution errors detected in boog13.bpl -------------------- boog14.bpl -------------------- boog14.bpl(12,1): Error BP5003: A postcondition might not hold on this return path. boog14.bpl(9,1): Related location: This is the postcondition that might not hold. Execution trace: boog14.bpl(11,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog15.bpl -------------------- boog15.bpl(11,1): Error BP5003: A postcondition might not hold on this return path. boog15.bpl(8,1): Related location: This is the postcondition that might not hold. Execution trace: boog15.bpl(10,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog16.bpl -------------------- boog16.bpl(12,1): Error BP5003: A postcondition might not hold on this return path. boog16.bpl(9,1): Related location: This is the postcondition that might not hold. Execution trace: boog16.bpl(11,8): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog17.bpl -------------------- boog17.bpl(26,3): Error BP5001: This assertion might not hold. Execution trace: boog17.bpl(17,1): start Boogie program verifier finished with 0 verified, 1 error -------------------- boog18.bpl -------------------- boog18.bpl(16,1): Error BP5003: A postcondition might not hold on this return path. boog18.bpl(13,1): Related location: This is the postcondition that might not hold. Execution trace: boog18.bpl(15,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(16,1): Error BP5001: This assertion might not hold. Execution trace: boog20.bpl(16,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(5,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(13,1): Error BP5001: This assertion might not hold. Execution trace: boog31.bpl(13,1): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- boog34.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- boog35.bpl -------------------- boog35.bpl(16,3): Error BP5001: This assertion might not hold. Execution trace: boog35.bpl(14,11): anon0 Boogie program verifier finished with 1 verified, 1 error -------------------- bar1.bpl -------------------- bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path. bar1.bpl(21,1): Related location: This is the postcondition that might not hold. Execution trace: bar1.bpl(24,3): anon0 Inlined call to procedure foo begins bar1.bpl(13,5): anon0 Inlined call to procedure bar begins bar1.bpl(7,5): anon0 Inlined call to procedure bar ends Inlined call to procedure bar begins bar1.bpl(7,5): anon0 Inlined call to procedure bar ends Inlined call to procedure foo ends Boogie program verifier finished with 0 verified, 1 error -------------------- bar2.bpl -------------------- bar2.bpl(21,3): Error BP5001: This assertion might not hold. Execution trace: bar2.bpl(19,3): anon0 Inlined call to procedure foo begins bar2.bpl(5,3): anon0 bar2.bpl(9,7): anon3_Else Inlined call to procedure foo ends Inlined call to procedure foo begins bar2.bpl(5,3): anon0 bar2.bpl(6,7): anon3_Then Inlined call to procedure foo ends Boogie program verifier finished with 0 verified, 1 error -------------------- bar3.bpl -------------------- bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path. bar3.bpl(34,1): Related location: This is the postcondition that might not hold. Execution trace: bar3.bpl(38,3): anon0 Inlined call to procedure foo begins bar3.bpl(18,3): anon0 bar3.bpl(24,7): anon3_Else Inlined call to procedure bar begins bar3.bpl(7,3): anon0 bar3.bpl(10,7): anon3_Else Inlined call to procedure bar ends Inlined call to procedure bar begins bar3.bpl(7,3): anon0 bar3.bpl(10,7): anon3_Else Inlined call to procedure bar ends Inlined call to procedure foo ends Inlined call to procedure bar begins bar3.bpl(7,3): anon0 bar3.bpl(10,7): anon3_Else Inlined call to procedure bar ends Boogie program verifier finished with 0 verified, 1 error -------------------- bar4.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- bar6.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors