main define i32 @main() { bb: %tmp = icmp sle i32 864, 10 br i1 %tmp, label %bb1, label %bb7 bb1: br label %bb2 bb2: %.0 = phi i32 [0, %bb1], [%tmp5, %bb4] %tmp3 = icmp slt i32 %.0, 100 br i1 %tmp3, label %bb4, label %bb6 bb4: %tmp5 = add i32 %.0, 1 br label %bb2 bb6: br label %bb30 bb7: %tmp8 = icmp sle i32 864, 50 br i1 %tmp8, label %bb9, label %bb15 bb9: br label %bb10 bb10: %.1 = phi i32 [0, %bb9], [%tmp13, %bb12] %tmp11 = icmp slt i32 %.1, 101 br i1 %tmp11, label %bb12, label %bb14 bb12: %tmp13 = add i32 %.1, 1 br label %bb10 bb14: br label %bb15 bb15: %tmp16 = icmp sle i32 864, 100 br i1 %tmp16, label %bb17, label %bb23 bb17: br label %bb18 bb18: %.2 = phi i32 [0, %bb17], [%tmp21, %bb20] %tmp19 = icmp slt i32 %.2, 102 br i1 %tmp19, label %bb20, label %bb22 bb20: %tmp21 = add i32 %.2, 1 br label %bb18 bb22: br label %bb29 bb23: br label %bb24 bb24: %tmp25 = icmp slt i32 0, 103 br i1 %tmp25, label %bb26, label %bb28 bb26: %tmp27 = add i32 0, 0 br label %bb24 bb28: br label %bb29 bb29: br label %bb30 bb30: ret i32 0 } 2.1 main define i32 @main() { bb: %tmp = icmp sle i32 864, 10 br i1 %tmp, label %bb1, label %bb7 bb1: br label %bb2 bb2: %.0 = phi i32 [0, %bb1], [%tmp5, %bb4] %tmp3 = icmp slt i32 %.0, 100 br i1 %tmp3, label %bb4, label %bb6 bb4: %tmp5 = add i32 %.0, 1 br label %bb2 bb6: br label %bb30 bb7: %tmp8 = icmp sle i32 864, 50 br i1 %tmp8, label %bb9, label %bb15 bb9: br label %bb10 bb10: %.1 = phi i32 [0, %bb9], [%tmp13, %bb12] %tmp11 = icmp slt i32 %.1, 101 br i1 %tmp11, label %bb12, label %bb14 bb12: %tmp13 = add i32 %.1, 1 br label %bb10 bb14: br label %bb15 bb15: %tmp16 = icmp sle i32 864, 100 br i1 %tmp16, label %bb17, label %bb23 bb17: br label %bb18 bb18: %.2 = phi i32 [0, %bb17], [%tmp21, %bb20] %tmp19 = icmp slt i32 %.2, 102 br i1 %tmp19, label %bb20, label %bb22 bb20: %tmp21 = add i32 %.2, 1 br label %bb18 bb22: br label %bb29 bb23: br label %bb24 bb24: %tmp25 = icmp slt i32 0, 103 br i1 %tmp25, label %bb26, label %bb28 bb26: %tmp27 = add i32 0, 0 br label %bb24 bb28: br label %bb29 bb29: br label %bb30 bb30: 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