main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: br label %bb3 bb3: %.01 = phi i32 [LLVMUndefLiteral, %bb], [%.12, %bb14] %.0 = phi i32 [LLVMUndefLiteral, %bb], [%.1, %bb14] %tmp = icmp sge i32 %.01, 0 br i1 %tmp, label %bb4, label %bb6 bb4: %tmp5 = icmp sge i32 %.0, 0 br label %bb6 bb6: %tmp7 = phi i1 [0, %bb3], [%tmp5, %bb4] br i1 %tmp7, label %bb8, label %bb15 bb8: %tmp9 = sub i32 %.0, 1 %tmp10 = icmp slt i32 %tmp9, 0 br i1 %tmp10, label %bb11, label %bb14 bb11: %tmp12 = sub i32 %.01, 1 %tmp13 = call i32 @__VERIFIER_nondet_int() br label %bb14 bb14: %.12 = phi i32 [%tmp12, %bb11], [%.01, %bb8] %.1 = phi i32 [%tmp13, %bb11], [%tmp9, %bb8] br label %bb3 bb15: ret i32 0 } 2.1 main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: br label %bb3 bb3: %.01 = phi i32 [LLVMUndefLiteral, %bb], [%.12, %bb14] %.0 = phi i32 [LLVMUndefLiteral, %bb], [%.1, %bb14] %tmp = icmp sge i32 %.01, 0 br i1 %tmp, label %bb4, label %bb6 bb4: %tmp5 = icmp sge i32 %.0, 0 br label %bb6 bb6: %tmp7 = phi i1 [0, %bb3], [%tmp5, %bb4] br i1 %tmp7, label %bb8, label %bb15 bb8: %tmp9 = sub i32 %.0, 1 %tmp10 = icmp slt i32 %tmp9, 0 br i1 %tmp10, label %bb11, label %bb14 bb11: %tmp12 = sub i32 %.01, 1 %tmp13 = call i32 @__VERIFIER_nondet_int() br label %bb14 bb14: %.12 = phi i32 [%tmp12, %bb11], [%.01, %bb8] %.1 = phi i32 [%tmp13, %bb11], [%tmp9, %bb8] br label %bb3 bb15: 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