main define i32 @main() { bb: br label %bb1 bb1: %.0 = phi i32 [0, %bb], [%.1, %bb6] %tmp = icmp slt i32 %.0, 100 br i1 %tmp, label %bb2, label %bb7 bb2: %tmp3 = icmp slt i32 %.0, 50 br i1 %tmp3, label %bb4, label %bb5 bb4: br label %bb6 bb5: br label %bb6 bb6: %.1 = phi i32 [51, %bb4], [49, %bb5] br label %bb1 bb7: ret i32 0 } 2.1 35 65 main bb1 1 .0 v25 tmp v26 tmp3 v27 .1 v28 v1 0 v26 1 v25 v28 v1 100 v1 50 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 66 main bb1 1 .0 v25 tmp v26 tmp3 v27 .1 v28 v1 0 v26 1 v25 v28 v1 100 v1 50 v25 100 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 67 main bb1 1 .0 v25 tmp v26 tmp3 v27 .1 v28 v1 0 v26 1 v25 v28 v1 100 v1 50 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 v25 100 68 main bb1 2 .0 v25 tmp v29 tmp3 v27 .1 v28 v1 0 v26 1 v25 v28 v29 1 v1 100 v1 50 v25 100 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 69 main bb1 2 .0 v25 tmp v30 tmp3 v27 .1 v28 v1 0 v26 1 v25 v28 v30 0 v1 100 v1 50 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 v25 100 70 main bb2 0 .0 v25 tmp v29 tmp3 v27 .1 v28 v1 0 v26 1 v25 v28 v29 1 v1 100 v1 50 v25 100 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 71 main bb7 0 .0 v25 tmp v30 tmp3 v27 .1 v28 v1 0 v26 1 v25 v28 v30 0 v1 100 v1 50 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 v25 100 72 main bb2 0 .0 v25 tmp v29 tmp3 v27 .1 v28 v1 0 v26 1 v25 v28 v29 1 v1 100 v1 50 v25 100 v25 50 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 73 main bb2 0 .0 v25 tmp v29 tmp3 v27 .1 v28 v1 0 v26 1 v25 v28 v29 1 v1 100 v1 50 v25 100 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 v25 50 74 main bb2 1 .0 v25 tmp v29 tmp3 v31 .1 v28 v1 0 v26 1 v25 v28 v29 1 v31 1 v1 100 v1 50 v25 100 v25 50 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 75 main bb2 1 .0 v25 tmp v29 tmp3 v32 .1 v28 v1 0 v26 1 v25 v28 v29 1 v32 0 v1 100 v1 50 v25 100 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 v25 50 76 main bb4 0 .0 v25 tmp v29 tmp3 v31 .1 v28 v1 0 v26 1 v25 v28 v29 1 v31 1 v1 100 v1 50 v25 100 v25 50 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 77 main bb5 0 .0 v25 tmp v29 tmp3 v32 .1 v28 v1 0 v26 1 v25 v28 v29 1 v32 0 v1 100 v1 50 v25 100 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 v25 50 78 main bb6 1 .0 v25 tmp v29 tmp3 v31 .1 v33 v1 0 v26 1 v25 v28 v29 1 v31 1 v33 51 v1 100 v1 50 v25 100 v25 50 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 79 main bb6 1 .0 v25 tmp v29 tmp3 v32 .1 v34 v1 0 v26 1 v25 v28 v29 1 v32 0 v34 49 v1 100 v1 50 v25 100 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 v25 50 80 main bb1 1 .0 v39 tmp v29 tmp3 v31 .1 v33 v1 0 v26 1 v25 v28 v29 1 v31 1 v33 51 v39 v33 v1 100 v1 50 v25 100 v25 50 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 81 main bb1 1 .0 v44 tmp v29 tmp3 v32 .1 v34 v1 0 v26 1 v25 v28 v29 1 v32 0 v34 49 v44 v34 v1 100 v1 50 v25 100 v1 0 0 v1 v26 1 1 v26 v25 v28 v28 v25 v25 50 35 main bb 0 36 main bb1 1 .0 v1 v1 0 37 main bb1 2 .0 v1 tmp v2 v1 0 v2 1 38 main bb2 0 .0 v1 tmp v2 v1 0 v2 1 v1 100 39 main bb2 1 .0 v1 tmp v2 tmp3 v3 v1 0 v2 1 v3 1 v1 100 40 main bb4 0 .0 v1 tmp v2 tmp3 v3 v1 0 v2 1 v3 1 v1 100 v1 50 41 main bb6 1 .0 v1 tmp v2 tmp3 v3 .1 v4 v1 0 v2 1 v3 1 v4 51 v1 100 v1 50 42 main bb1 1 .0 v5 tmp v2 tmp3 v3 .1 v4 v1 0 v2 1 v3 1 v4 51 v5 v4 v1 100 v1 50 49 main bb1 1 .0 v10 tmp v11 tmp3 v12 .1 v13 v1 0 v11 1 v10 v13 v1 100 v1 50 v1 0 0 v1 v11 1 1 v11 0 v12 49 v13 v10 v13 v13 v10 65 66 67 v25 100 66 68 v29 67 69 v30 68 70 69 71 70 72 73 v25 50 71 72 74 v31 73 75 v32 74 76 75 77 76
78 v33 51
77
79 v34 49
78
80 v39 v33
79
81 v44 v34
80 65 v25 v39 v26 v29 v27 v31 v28 v33 81 65 v25 v44 v26 v29 v27 v32 v28 v34 35
36 v1 0
36 37 v2 37 38 38 39 v3 39 40 40
41 v4 51
41
42 v5 v4
42 49 v10 v5 v11 v2 v12 v3 v13 v4 49 65 v25 v10 v26 v11 v27 v12 v28 v13 68 81 77 72 67 80 39 37 65 73 38 66 49 36 70 79 75 40 74 78 69 35 42 76 41 1 69 71 pp1 v25 pp2 v28 pp3 v30 pp4 v27 pp1 v25 pp2 v28 pp3 v30 pp4 v27 100 v25 v25 v28 v25 v28 v28 v25 v1 50 v1 0 v30 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 100 v25 v25 v28 v25 v28 v28 v25 v1 50 v1 0 v30 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 2 49 65 pp1 v10 pp2 v13 pp3 v11 pp4 v12 pp1 v10 pp2 v13 pp3 v11 pp4 v12 v11 1 49 v13 v10 v13 v10 v13 v13 v10 v11 1 1 v11 0 v12 v1 50 v1 0 v1 0 0 v1 v1 100 v1 50 v1 0 v1 0 0 v1 v11 1 1 v11 v1 100 v11 1 v10 v13 v10 v13 v13 v10 3 35 36 pp1 v1 v1 0 4 76 78 pp1 v25 pp2 v28 pp3 v29 pp4 v31 pp1 v25 pp2 v33 pp3 v29 pp4 v31 v25 50 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v31 1 v1 100 v26 1 v33 51 v25 50 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v31 1 v1 100 v26 1 5 78 80 pp1 v25 pp2 v33 pp3 v29 pp4 v31 pp1 v39 pp2 v33 pp3 v29 pp4 v31 v33 51 v25 50 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v31 1 v1 100 v26 1 v33 51 v25 50 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v31 1 v1 100 v26 1 v39 v33 6 65 67 pp1 v25 pp2 v28 pp3 v26 pp4 v27 pp1 v25 pp2 v28 pp3 v26 pp4 v27 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 v25 v28 v25 v28 v28 v25 v1 50 100 v25 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 v25 v28 v25 v28 v28 v25 7 39 40 pp1 v1 pp2 v2 pp3 v3 pp1 v1 pp2 v2 pp3 v3 v1 50 v3 1 v1 0 v1 100 v2 1 v1 50 v3 1 v1 0 v1 100 v2 1 8 68 70 pp1 v25 pp2 v28 pp3 v29 pp4 v27 pp1 v25 pp2 v28 pp3 v29 pp4 v27 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 9 81 65 pp1 v44 pp2 v34 pp3 v29 pp4 v32 pp1 v44 pp2 v34 pp3 v29 pp4 v32 v44 v34 50 v25 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v32 0 v34 49 v1 100 v26 1 v1 50 v1 0 v1 0 0 v1 v29 1 1 v29 v1 100 v29 1 v44 v34 v44 v34 v34 v44 10 36 37 pp1 v1 pp1 v1 pp2 v2 v1 0 v1 0 v1 100 v2 1 11 37 38 pp1 v1 pp2 v2 pp1 v1 pp2 v2 v1 0 v1 100 v2 1 v1 0 v1 100 v2 1 12 38 39 pp1 v1 pp2 v2 pp1 v1 pp2 v2 pp3 v3 v1 0 v1 100 v2 1 v1 50 v3 1 v1 0 v1 100 v2 1 13 66 68 pp1 v25 pp2 v28 pp3 v26 pp4 v27 pp1 v25 pp2 v28 pp3 v29 pp4 v27 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 v25 v28 v25 100 v25 v28 v28 v25 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 14 74 76 pp1 v25 pp2 v28 pp3 v29 pp4 v31 pp1 v25 pp2 v28 pp3 v29 pp4 v31 v25 50 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v31 1 v1 100 v26 1 v25 50 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v31 1 v1 100 v26 1 15 41 42 pp1 v1 pp2 v4 pp3 v2 pp4 v3 pp1 v5 pp2 v4 pp3 v2 pp4 v3 v4 51 v1 50 v3 1 v1 0 v1 100 v2 1 v4 51 v1 50 v3 1 v1 0 v5 v4 v1 100 v2 1 16 77 79 pp1 v25 pp2 v28 pp3 v29 pp4 v32 pp1 v25 pp2 v34 pp3 v29 pp4 v32 50 v25 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v32 0 v1 100 v26 1 50 v25 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v32 0 v34 49 v1 100 v26 1 17 72 74 pp1 v25 pp2 v28 pp3 v29 pp4 v27 pp1 v25 pp2 v28 pp3 v29 pp4 v31 v25 50 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 v25 50 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v31 1 v1 100 v26 1 18 75 77 pp1 v25 pp2 v28 pp3 v29 pp4 v32 pp1 v25 pp2 v28 pp3 v29 pp4 v32 50 v25 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v32 0 v1 100 v26 1 50 v25 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v32 0 v1 100 v26 1 19 79 81 pp1 v25 pp2 v34 pp3 v29 pp4 v32 pp1 v44 pp2 v34 pp3 v29 pp4 v32 50 v25 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v32 0 v34 49 v1 100 v26 1 v44 v34 50 v25 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v32 0 v34 49 v1 100 v26 1 20 80 65 pp1 v39 pp2 v33 pp3 v29 pp4 v31 pp1 v39 pp2 v33 pp3 v29 pp4 v31 v33 51 v25 50 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v31 1 v1 100 v26 1 v39 v33 v1 50 v1 0 v1 0 0 v1 v29 1 1 v29 v1 100 v29 1 v39 v33 v39 v33 v33 v39 21 65 66 pp1 v25 pp2 v28 pp3 v26 pp4 v27 pp1 v25 pp2 v28 pp3 v26 pp4 v27 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 v25 v28 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 v25 v28 v25 100 v25 v28 v28 v25 22 73 75 pp1 v25 pp2 v28 pp3 v29 pp4 v27 pp1 v25 pp2 v28 pp3 v29 pp4 v32 50 v25 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 50 v25 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v32 0 v1 100 v26 1 23 42 49 pp1 v5 pp2 v4 pp3 v2 pp4 v3 pp1 v5 pp2 v4 pp3 v2 pp4 v3 v4 51 v1 50 v3 1 v1 0 v5 v4 v1 100 v2 1 v2 1 49 v4 v5 v4 v5 v4 v4 v5 v2 1 1 v2 0 v3 v1 50 v1 0 v1 0 0 v1 v1 100 24 40 41 pp1 v1 pp2 v2 pp3 v3 pp1 v1 pp2 v4 pp3 v2 pp4 v3 v1 50 v3 1 v1 0 v1 100 v2 1 v4 51 v1 50 v3 1 v1 0 v1 100 v2 1 25 70 72 pp1 v25 pp2 v28 pp3 v29 pp4 v27 pp1 v25 pp2 v28 pp3 v29 pp4 v27 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 v25 50 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 26 67 69 pp1 v25 pp2 v28 pp3 v26 pp4 v27 pp1 v25 pp2 v28 pp3 v30 pp4 v27 v1 50 100 v25 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 v25 v28 v25 v28 v28 v25 100 v25 v25 v28 v25 v28 v28 v25 v1 50 v1 0 v30 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 27 70 73 pp1 v25 pp2 v28 pp3 v29 pp4 v27 pp1 v25 pp2 v28 pp3 v29 pp4 v27 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 50 v25 v25 v28 v29 1 v25 100 v25 v28 v28 v25 v1 50 v1 0 v1 0 0 v1 v26 1 1 v26 v1 100 v26 1 65 pp1 v25 pp2 v28 pp3 v26 pp4 v27 66 pp1 v25 pp2 v28 pp3 v26 pp4 v27 67 pp1 v25 pp2 v28 pp3 v26 pp4 v27 68 pp1 v25 pp2 v28 pp3 v29 pp4 v27 69 pp1 v25 pp2 v28 pp3 v30 pp4 v27 70 pp1 v25 pp2 v28 pp3 v29 pp4 v27 71 pp1 v25 pp2 v28 pp3 v30 pp4 v27 72 pp1 v25 pp2 v28 pp3 v29 pp4 v27 73 pp1 v25 pp2 v28 pp3 v29 pp4 v27 74 pp1 v25 pp2 v28 pp3 v29 pp4 v31 75 pp1 v25 pp2 v28 pp3 v29 pp4 v32 76 pp1 v25 pp2 v28 pp3 v29 pp4 v31 77 pp1 v25 pp2 v28 pp3 v29 pp4 v32 78 pp1 v25 pp2 v33 pp3 v29 pp4 v31 79 pp1 v25 pp2 v34 pp3 v29 pp4 v32 80 pp1 v39 pp2 v33 pp3 v29 pp4 v31 81 pp1 v44 pp2 v34 pp3 v29 pp4 v32 35 36 pp1 v1 37 pp1 v1 pp2 v2 38 pp1 v1 pp2 v2 39 pp1 v1 pp2 v2 pp3 v3 40 pp1 v1 pp2 v2 pp3 v3 41 pp1 v1 pp2 v4 pp3 v2 pp4 v3 42 pp1 v5 pp2 v4 pp3 v2 pp4 v3 49 pp1 v10 pp2 v13 pp3 v11 pp4 v12 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