main define i32 @main() { bb: br label %bb1 bb1: %.0 = phi i32 [LLVMUndefLiteral, %bb], [%.3, %bb17] %tmp = icmp ne i32 %.0, 0 br i1 %tmp, label %bb2, label %bb18 bb2: %tmp3 = icmp sle i32 -5, %.0 br i1 %tmp3, label %bb4, label %bb16 bb4: %tmp5 = icmp sle i32 %.0, 35 br i1 %tmp5, label %bb6, label %bb16 bb6: %tmp7 = icmp slt i32 %.0, 0 br i1 %tmp7, label %bb8, label %bb9 bb8: br label %bb15 bb9: %tmp10 = icmp sgt i32 %.0, 30 br i1 %tmp10, label %bb11, label %bb12 bb11: br label %bb14 bb12: %tmp13 = sub i32 %.0, 1 br label %bb14 bb14: %.1 = phi i32 [35, %bb11], [%tmp13, %bb12] br label %bb15 bb15: %.2 = phi i32 [-5, %bb8], [%.1, %bb14] br label %bb17 bb16: br label %bb17 bb17: %.3 = phi i32 [%.2, %bb15], [0, %bb16] br label %bb1 bb18: ret i32 0 } 2.1 main define i32 @main() { bb: br label %bb1 bb1: %.0 = phi i32 [LLVMUndefLiteral, %bb], [%.3, %bb17] %tmp = icmp ne i32 %.0, 0 br i1 %tmp, label %bb2, label %bb18 bb2: %tmp3 = icmp sle i32 -5, %.0 br i1 %tmp3, label %bb4, label %bb16 bb4: %tmp5 = icmp sle i32 %.0, 35 br i1 %tmp5, label %bb6, label %bb16 bb6: %tmp7 = icmp slt i32 %.0, 0 br i1 %tmp7, label %bb8, label %bb9 bb8: br label %bb15 bb9: %tmp10 = icmp sgt i32 %.0, 30 br i1 %tmp10, label %bb11, label %bb12 bb11: br label %bb14 bb12: %tmp13 = sub i32 %.0, 1 br label %bb14 bb14: %.1 = phi i32 [35, %bb11], [%tmp13, %bb12] br label %bb15 bb15: %.2 = phi i32 [-5, %bb8], [%.1, %bb14] br label %bb17 bb16: br label %bb17 bb17: %.3 = phi i32 [%.2, %bb15], [0, %bb16] br label %bb1 bb18: 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