main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp2 = icmp slt i32 %tmp, 0 br i1 %tmp2, label %bb5, label %bb3 bb3: %tmp4 = icmp slt i32 2, 1 br i1 %tmp4, label %bb5, label %bb6 bb5: br label %bb13 bb6: br label %bb7 bb7: %.01 = phi i32 [2, %bb6], [%tmp10, %bb9] %.0 = phi i32 [1, %bb6], [%tmp11, %bb9] %tmp8 = icmp sgt i32 %tmp, %.01 br i1 %tmp8, label %bb9, label %bb12 bb9: %tmp10 = mul i32 %.01, %.01 %tmp11 = mul i32 2, %.0 br label %bb7 bb12: br label %bb13 bb13: ret i32 0 } 2.1 main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp2 = icmp slt i32 %tmp, 0 br i1 %tmp2, label %bb5, label %bb3 bb3: %tmp4 = icmp slt i32 2, 1 br i1 %tmp4, label %bb5, label %bb6 bb5: br label %bb13 bb6: br label %bb7 bb7: %.01 = phi i32 [2, %bb6], [%tmp10, %bb9] %.0 = phi i32 [1, %bb6], [%tmp11, %bb9] %tmp8 = icmp sgt i32 %tmp, %.01 br i1 %tmp8, label %bb9, label %bb12 bb9: %tmp10 = mul i32 %.01, %.01 %tmp11 = mul i32 2, %.0 br label %bb7 bb12: br label %bb13 bb13: 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