main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp3 = call i32 @__VERIFIER_nondet_int() br label %bb4 bb4: %.02 = phi i32 [%tmp3, %bb], [%tmp12, %bb11] %.01 = phi i32 [%tmp, %bb], [%.02, %bb11] %.0 = phi i32 [LLVMUndefLiteral, %bb], [%.02, %bb11] %tmp5 = icmp sgt i32 %.01, 0 br i1 %tmp5, label %bb6, label %bb9 bb6: %tmp7 = sub i32 0, %.0 %tmp8 = icmp sle i32 %.02, %tmp7 br label %bb9 bb9: %tmp10 = phi i1 [0, %bb4], [%tmp8, %bb6] br i1 %tmp10, label %bb11, label %bb13 bb11: %tmp12 = call i32 @__VERIFIER_nondet_int() br label %bb4 bb13: ret i32 0 } 2.1 main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp3 = call i32 @__VERIFIER_nondet_int() br label %bb4 bb4: %.02 = phi i32 [%tmp3, %bb], [%tmp12, %bb11] %.01 = phi i32 [%tmp, %bb], [%.02, %bb11] %.0 = phi i32 [LLVMUndefLiteral, %bb], [%.02, %bb11] %tmp5 = icmp sgt i32 %.01, 0 br i1 %tmp5, label %bb6, label %bb9 bb6: %tmp7 = sub i32 0, %.0 %tmp8 = icmp sle i32 %.02, %tmp7 br label %bb9 bb9: %tmp10 = phi i1 [0, %bb4], [%tmp8, %bb6] br i1 %tmp10, label %bb11, label %bb13 bb11: %tmp12 = call i32 @__VERIFIER_nondet_int() br label %bb4 bb13: ret i32 0 } AProVE AProVE Commit ID: unknown Statistics for single proof: 0,00 % (0 real / 0 unknown / 1 assumptions / 1 total proof steps) http://aprove.informatik.rwth-aachen.de John Doe