main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() br label %bb1 bb1: %.0 = phi i32 [%tmp, %bb], [%tmp2, %bb1] %tmp2 = add i32 %.0, 1 br label %bb1 } 2.1 18 18 main bb 0 19 main bb 1 tmp v1 20 main bb1 1 tmp v1 .0 v2 v2 v1 21 main bb1 2 tmp v1 .0 v2 tmp2 v3 v2 v1 v3 v2 1 22 main bb1 1 tmp v1 .0 v4 tmp2 v3 v2 v1 v3 v2 1 v4 v3 25 main bb1 1 tmp v7 .0 v8 tmp2 v9 v2 v7 v8 v9 v2 v7 v7 v2 v8 v9 v9 v8 26 main bb1 2 tmp v7 .0 v8 tmp2 v10 v2 v7 v8 v9 v10 v8 1 v2 v7 v7 v2 v8 v9 v9 v8 27 main bb1 1 tmp v7 .0 v11 tmp2 v10 v2 v7 v8 v9 v10 v8 1 v11 v10 v2 v7 v7 v2 v8 v9 v9 v8 18 19 v1 19
20 v2 v1
20 21 v3 21
22 v4 v3
22 25 v7 v1 v8 v4 v9 v3 25 26 v10 26
27 v11 v10
27 25 v7 v7 v8 v11 v9 v10 18 20 25 26 27 22 21 19 1 22 25 pp1 v4 pp2 v1 pp3 v3 pp1 v4 pp2 v1 pp3 v3 v3 v2 1 v4 v3 v2 v1 v4 v3 v4 v3 v3 v4 v2 v1 v2 v1 v1 v2 2 20 21 pp1 v2 pp2 v1 pp1 v2 pp2 v1 pp3 v3 v2 v1 v3 v2 1 v2 v1 3 26 27 pp1 v8 pp2 v7 pp3 v10 pp1 v11 pp2 v7 pp3 v10 v10 v8 1 v8 v9 v8 v9 v9 v8 v2 v7 v2 v7 v7 v2 v10 v8 1 v8 v9 v8 v9 v9 v8 v2 v7 v11 v10 v2 v7 v7 v2 4 27 25 pp1 v11 pp2 v7 pp3 v10 pp1 v11 pp2 v7 pp3 v10 v10 v8 1 v8 v9 v8 v9 v9 v8 v2 v7 v11 v10 v2 v7 v7 v2 v11 v10 v11 v10 v10 v11 v2 v7 v2 v7 v7 v2 5 19 20 pp1 v1 pp1 v2 pp2 v1 v2 v1 6 18 19 pp1 v1 7 25 26 pp1 v8 pp2 v7 pp3 v9 pp1 v8 pp2 v7 pp3 v10 v8 v9 v8 v9 v9 v8 v2 v7 v2 v7 v7 v2 v10 v8 1 v8 v9 v8 v9 v9 v8 v2 v7 v2 v7 v7 v2 8 21 22 pp1 v2 pp2 v1 pp3 v3 pp1 v4 pp2 v1 pp3 v3 v3 v2 1 v2 v1 v3 v2 1 v4 v3 v2 v1 18 19 pp1 v1 20 pp1 v2 pp2 v1 21 pp1 v2 pp2 v1 pp3 v3 22 pp1 v4 pp2 v1 pp3 v3 25 pp1 v8 pp2 v7 pp3 v9 26 pp1 v8 pp2 v7 pp3 v10 27 pp1 v11 pp2 v7 pp3 v10 AProVE AProVE Commit ID: unknown Statistics for single proof: 75,00 % (3 real / 0 unknown / 1 assumptions / 4 total proof steps) http://aprove.informatik.rwth-aachen.de John Doe