main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp5 = call i32 @__VERIFIER_nondet_int() %tmp6 = call i32 @__VERIFIER_nondet_int() br label %bb7 bb7: %.02 = phi i32 [1, %bb], [%.24, %bb28] %.01 = phi i32 [0, %bb], [%tmp29, %bb28] %.0 = phi i32 [%tmp5, %bb], [%.2, %bb28] %tmp8 = icmp slt i32 %.0, %tmp6 br i1 %tmp8, label %bb9, label %bb11 bb9: %tmp10 = icmp sgt i32 %.02, 0 br label %bb11 bb11: %tmp12 = phi i1 [0, %bb7], [%tmp10, %bb9] br i1 %tmp12, label %bb13, label %bb30 bb13: %tmp14 = icmp sgt i32 %.0, 0 br i1 %tmp14, label %bb15, label %bb19 bb15: %tmp16 = icmp sgt i32 %tmp, 1 br i1 %tmp16, label %bb17, label %bb19 bb17: %tmp18 = mul i32 %tmp, %.0 br label %bb28 bb19: %tmp20 = icmp sgt i32 %.0, 0 br i1 %tmp20, label %bb21, label %bb26 bb21: %tmp22 = icmp slt i32 %tmp, -1 br i1 %tmp22, label %bb23, label %bb26 bb23: %tmp24 = sub i32 0, %tmp %tmp25 = mul i32 %tmp24, %.0 br label %bb27 bb26: br label %bb27 bb27: %.13 = phi i32 [%.02, %bb23], [0, %bb26] %.1 = phi i32 [%tmp25, %bb23], [%.0, %bb26] br label %bb28 bb28: %.24 = phi i32 [%.02, %bb17], [%.13, %bb27] %.2 = phi i32 [%tmp18, %bb17], [%.1, %bb27] %tmp29 = add i32 %.01, 1 br label %bb7 bb30: ret i32 0 } 2.1 main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp5 = call i32 @__VERIFIER_nondet_int() %tmp6 = call i32 @__VERIFIER_nondet_int() br label %bb7 bb7: %.02 = phi i32 [1, %bb], [%.24, %bb28] %.01 = phi i32 [0, %bb], [%tmp29, %bb28] %.0 = phi i32 [%tmp5, %bb], [%.2, %bb28] %tmp8 = icmp slt i32 %.0, %tmp6 br i1 %tmp8, label %bb9, label %bb11 bb9: %tmp10 = icmp sgt i32 %.02, 0 br label %bb11 bb11: %tmp12 = phi i1 [0, %bb7], [%tmp10, %bb9] br i1 %tmp12, label %bb13, label %bb30 bb13: %tmp14 = icmp sgt i32 %.0, 0 br i1 %tmp14, label %bb15, label %bb19 bb15: %tmp16 = icmp sgt i32 %tmp, 1 br i1 %tmp16, label %bb17, label %bb19 bb17: %tmp18 = mul i32 %tmp, %.0 br label %bb28 bb19: %tmp20 = icmp sgt i32 %.0, 0 br i1 %tmp20, label %bb21, label %bb26 bb21: %tmp22 = icmp slt i32 %tmp, -1 br i1 %tmp22, label %bb23, label %bb26 bb23: %tmp24 = sub i32 0, %tmp %tmp25 = mul i32 %tmp24, %.0 br label %bb27 bb26: br label %bb27 bb27: %.13 = phi i32 [%.02, %bb23], [0, %bb26] %.1 = phi i32 [%tmp25, %bb23], [%.0, %bb26] br label %bb28 bb28: %.24 = phi i32 [%.02, %bb17], [%.13, %bb27] %.2 = phi i32 [%tmp18, %bb17], [%.1, %bb27] %tmp29 = add i32 %.01, 1 br label %bb7 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