main define i32 @main() { bb: br label %bb5 bb5: %.03 = phi i32 [1, %bb], [%.14, %bb26] %.01 = phi i32 [1, %bb], [%.2, %bb26] %.0 = phi i32 [1, %bb], [%.1, %bb26] %tmp = mul i32 %.03, %.03 %tmp6 = mul i32 %tmp, %.03 %tmp7 = mul i32 %.01, %.01 %tmp8 = mul i32 %tmp7, %.01 %tmp9 = mul i32 %.0, %.0 %tmp10 = mul i32 %tmp9, %.0 %tmp11 = add i32 %tmp8, %tmp10 %tmp12 = icmp ne i32 %tmp6, %tmp11 br i1 %tmp12, label %bb13, label %bb15 bb13: %tmp14 = icmp sle i32 %.0, 1000 br label %bb15 bb15: %tmp16 = phi i1 [0, %bb5], [%tmp14, %bb13] br i1 %tmp16, label %bb17, label %bb27 bb17: %tmp18 = add i32 %.03, 1 %tmp19 = icmp sgt i32 %tmp18, 1000 br i1 %tmp19, label %bb20, label %bb22 bb20: %tmp21 = add i32 %.01, 1 br label %bb22 bb22: %.14 = phi i32 [1, %bb20], [%tmp18, %bb17] %.12 = phi i32 [%tmp21, %bb20], [%.01, %bb17] %tmp23 = icmp sgt i32 %.12, 1000 br i1 %tmp23, label %bb24, label %bb26 bb24: %tmp25 = add i32 %.0, 1 br label %bb26 bb26: %.2 = phi i32 [1, %bb24], [%.12, %bb22] %.1 = phi i32 [%tmp25, %bb24], [%.0, %bb22] br label %bb5 bb27: ret i32 0 } 2.1 main define i32 @main() { bb: br label %bb5 bb5: %.03 = phi i32 [1, %bb], [%.14, %bb26] %.01 = phi i32 [1, %bb], [%.2, %bb26] %.0 = phi i32 [1, %bb], [%.1, %bb26] %tmp = mul i32 %.03, %.03 %tmp6 = mul i32 %tmp, %.03 %tmp7 = mul i32 %.01, %.01 %tmp8 = mul i32 %tmp7, %.01 %tmp9 = mul i32 %.0, %.0 %tmp10 = mul i32 %tmp9, %.0 %tmp11 = add i32 %tmp8, %tmp10 %tmp12 = icmp ne i32 %tmp6, %tmp11 br i1 %tmp12, label %bb13, label %bb15 bb13: %tmp14 = icmp sle i32 %.0, 1000 br label %bb15 bb15: %tmp16 = phi i1 [0, %bb5], [%tmp14, %bb13] br i1 %tmp16, label %bb17, label %bb27 bb17: %tmp18 = add i32 %.03, 1 %tmp19 = icmp sgt i32 %tmp18, 1000 br i1 %tmp19, label %bb20, label %bb22 bb20: %tmp21 = add i32 %.01, 1 br label %bb22 bb22: %.14 = phi i32 [1, %bb20], [%tmp18, %bb17] %.12 = phi i32 [%tmp21, %bb20], [%.01, %bb17] %tmp23 = icmp sgt i32 %.12, 1000 br i1 %tmp23, label %bb24, label %bb26 bb24: %tmp25 = add i32 %.0, 1 br label %bb26 bb26: %.2 = phi i32 [1, %bb24], [%.12, %bb22] %.1 = phi i32 [%tmp25, %bb24], [%.0, %bb22] br label %bb5 bb27: 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