main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() br label %bb2 bb2: %.01 = phi i32 [%tmp, %bb], [%tmp10, %bb9] %.0 = phi i32 [LLVMUndefLiteral, %bb], [%.01, %bb9] %tmp3 = icmp sgt i32 %.01, 1 br i1 %tmp3, label %bb4, label %bb7 bb4: %tmp5 = mul i32 -2, %.01 %tmp6 = icmp eq i32 %tmp5, %.0 br label %bb7 bb7: %tmp8 = phi i1 [0, %bb2], [%tmp6, %bb4] br i1 %tmp8, label %bb9, label %bb11 bb9: %tmp10 = call i32 @__VERIFIER_nondet_int() br label %bb2 bb11: ret i32 0 } 2.1 main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() br label %bb2 bb2: %.01 = phi i32 [%tmp, %bb], [%tmp10, %bb9] %.0 = phi i32 [LLVMUndefLiteral, %bb], [%.01, %bb9] %tmp3 = icmp sgt i32 %.01, 1 br i1 %tmp3, label %bb4, label %bb7 bb4: %tmp5 = mul i32 -2, %.01 %tmp6 = icmp eq i32 %tmp5, %.0 br label %bb7 bb7: %tmp8 = phi i1 [0, %bb2], [%tmp6, %bb4] br i1 %tmp8, label %bb9, label %bb11 bb9: %tmp10 = call i32 @__VERIFIER_nondet_int() br label %bb2 bb11: 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