main define i32 @main() { bb: br label %bb1 bb1: %.0 = phi i32 [0, %bb], [%tmp3, %bb2] %tmp = icmp sge i32 %.0, 0 br i1 %tmp, label %bb2, label %bb4 bb2: %tmp3 = sub i32 %.0, 1 br label %bb1 bb4: ret i32 0 } 2.1 23 23 main bb 0 24 main bb1 1 .0 v1 v1 0 25 main bb1 2 .0 v1 tmp v2 v1 0 v2 1 26 main bb2 0 .0 v1 tmp v2 v1 0 v2 1 v1 0 27 main bb2 1 .0 v1 tmp v2 tmp3 v3 v1 0 v2 1 v3 v1 -1 1 v1 0 28 main bb1 1 .0 v4 tmp v2 tmp3 v3 v1 0 v2 1 v3 v1 -1 1 v4 v3 v1 0 29 main bb1 2 .0 v4 tmp v5 tmp3 v3 v1 0 v2 1 v3 v1 -1 1 v4 v3 v5 0 v1 0 30 main bb4 0 .0 v4 tmp v5 tmp3 v3 v1 0 v2 1 v3 v1 -1 1 v4 v3 v5 0 v4 0 v1 0 23
24 v1 0
24 25 v2 25 26 26 27 v3 27
28 v4 v3
28 29 v5 29 30 30 23 25 26 27 28 29 24 1 28 29 pp1 v4 pp2 v2 pp3 v3 pp1 v4 pp2 v5 pp3 v3 v4 v3 v3 v1 -1 1 0 v1 v1 0 v2 1 v4 v3 v4 0 v3 v1 -1 1 v5 0 0 v1 v1 0 v2 1 2 24 25 pp1 v1 pp1 v1 pp2 v2 v1 0 0 v1 v1 0 v2 1 3 29 30 pp1 v4 pp2 v5 pp3 v3 pp1 v4 pp2 v5 pp3 v3 v4 v3 v4 0 v3 v1 -1 1 v5 0 0 v1 v1 0 v2 1 v4 v3 v4 0 v3 v1 -1 1 v5 0 0 v1 v1 0 v2 1 4 25 26 pp1 v1 pp2 v2 pp1 v1 pp2 v2 0 v1 v1 0 v2 1 0 v1 v1 0 v2 1 5 26 27 pp1 v1 pp2 v2 pp1 v1 pp2 v2 pp3 v3 0 v1 v1 0 v2 1 v3 v1 -1 1 0 v1 v1 0 v2 1 6 23 24 pp1 v1 v1 0 7 27 28 pp1 v1 pp2 v2 pp3 v3 pp1 v4 pp2 v2 pp3 v3 v3 v1 -1 1 0 v1 v1 0 v2 1 v4 v3 v3 v1 -1 1 0 v1 v1 0 v2 1 23 24 pp1 v1 25 pp1 v1 pp2 v2 26 pp1 v1 pp2 v2 27 pp1 v1 pp2 v2 pp3 v3 28 pp1 v4 pp2 v2 pp3 v3 29 pp1 v4 pp2 v5 pp3 v3 30 pp1 v4 pp2 v5 pp3 v3 23 23 25 25 pp1 pp1 pp2 pp2 26 26 pp1 pp1 pp2 pp2 27 27 pp1 pp1 pp2 pp2 pp3 pp3 28 28 pp1 pp1 pp2 pp2 pp3 pp3 29 29 pp1 pp1 pp2 pp2 pp3 pp3 24 24 pp1 pp1 AProVE AProVE Commit ID: unknown Statistics for single proof: 100,00 % (5 real / 0 unknown / 0 assumptions / 5 total proof steps) http://aprove.informatik.rwth-aachen.de John Doe