main define i32 @main() { bb: br label %bb1 bb1: %.0 = phi i32 [0, %bb], [%tmp4, %bb2] %tmp = icmp slt i32 %.0, 100 br i1 %tmp, label %bb2, label %bb5 bb2: %tmp3 = add i32 %.0, 1 %tmp4 = sub i32 %tmp3, 1 br label %bb1 bb5: ret i32 0 } 2.1 26 32 main bb1 1 .0 v5 tmp v2 tmp3 v3 tmp4 v4 v1 0 v2 1 v3 v1 1 v4 v3 -1 1 v5 v4 v1 100 38 main bb1 1 .0 v10 tmp v11 tmp3 v12 tmp4 v13 v1 0 v11 1 v13 v12 -1 1 v10 v13 v1 100 v1 0 0 v1 v11 1 1 v11 v13 v12 -1 1 v12 -1 1 v13 v10 v13 v13 v10 39 main bb1 1 .0 v10 tmp v11 tmp3 v12 tmp4 v13 v1 0 v11 1 v13 v12 -1 1 v10 v13 v1 100 v10 100 v1 0 0 v1 v11 1 1 v11 v13 v12 -1 1 v12 -1 1 v13 v10 v13 v13 v10 40 main bb1 1 .0 v10 tmp v11 tmp3 v12 tmp4 v13 v1 0 v11 1 v13 v12 -1 1 v10 v13 v1 100 v1 0 0 v1 v11 1 1 v11 v13 v12 -1 1 v12 -1 1 v13 v10 v13 v13 v10 v10 100 41 main bb1 2 .0 v10 tmp v14 tmp3 v12 tmp4 v13 v1 0 v11 1 v13 v12 -1 1 v10 v13 v14 1 v1 100 v10 100 v1 0 0 v1 v11 1 1 v11 v13 v12 -1 1 v12 -1 1 v13 v10 v13 v13 v10 42 main bb1 2 .0 v10 tmp v15 tmp3 v12 tmp4 v13 v1 0 v11 1 v13 v12 -1 1 v10 v13 v15 0 v1 100 v1 0 0 v1 v11 1 1 v11 v13 v12 -1 1 v12 -1 1 v13 v10 v13 v13 v10 v10 100 43 main bb2 0 .0 v10 tmp v14 tmp3 v12 tmp4 v13 v1 0 v11 1 v13 v12 -1 1 v10 v13 v14 1 v1 100 v10 100 v1 0 0 v1 v11 1 1 v11 v13 v12 -1 1 v12 -1 1 v13 v10 v13 v13 v10 44 main bb5 0 .0 v10 tmp v15 tmp3 v12 tmp4 v13 v1 0 v11 1 v13 v12 -1 1 v10 v13 v15 0 v1 100 v1 0 0 v1 v11 1 1 v11 v13 v12 -1 1 v12 -1 1 v13 v10 v13 v13 v10 v10 100 45 main bb2 1 .0 v10 tmp v14 tmp3 v16 tmp4 v13 v1 0 v11 1 v13 v12 -1 1 v10 v13 v14 1 v16 v10 1 v1 100 v10 100 v1 0 0 v1 v11 1 1 v11 v13 v12 -1 1 v12 -1 1 v13 v10 v13 v13 v10 46 main bb2 2 .0 v10 tmp v14 tmp3 v16 tmp4 v17 v1 0 v11 1 v13 v12 -1 1 v10 v13 v14 1 v16 v10 1 v17 v16 -1 1 v1 100 v10 100 v1 0 0 v1 v11 1 1 v11 v13 v12 -1 1 v12 -1 1 v13 v10 v13 v13 v10 47 main bb1 1 .0 v18 tmp v14 tmp3 v16 tmp4 v17 v1 0 v11 1 v13 v12 -1 1 v10 v13 v14 1 v16 v10 1 v17 v16 -1 1 v18 v17 v1 100 v10 100 v1 0 0 v1 v11 1 1 v11 v13 v12 -1 1 v12 -1 1 v13 v10 v13 v13 v10 26 main bb 0 27 main bb1 1 .0 v1 v1 0 28 main bb1 2 .0 v1 tmp v2 v1 0 v2 1 29 main bb2 0 .0 v1 tmp v2 v1 0 v2 1 v1 100 30 main bb2 1 .0 v1 tmp v2 tmp3 v3 v1 0 v2 1 v3 v1 1 v1 100 31 main bb2 2 .0 v1 tmp v2 tmp3 v3 tmp4 v4 v1 0 v2 1 v3 v1 1 v4 v3 -1 1 v1 100 32 38 v10 v5 v11 v2 v12 v3 v13 v4 38 39 40 v10 100 39 41 v14 40 42 v15 41 43 42 44 43 45 v16 44 45 46 v17 46
47 v18 v17
47 38 v10 v18 v11 v14 v12 v16 v13 v17 26
27 v1 0
27 28 v2 28 29 29 30 v3 30 31 v4 31
32 v5 v4
30 32 26 40 43 29 47 39 46 42 27 28 41 31 38 45 1 31 32 pp1 v1 pp2 v2 pp3 v3 pp4 v4 pp1 v5 pp2 v2 pp3 v3 pp4 v4 v1 100 v2 1 v4 v3 -1 1 v1 0 v3 v1 1 v5 v4 v1 100 v2 1 v4 v3 -1 1 v1 0 v3 v1 1 2 30 31 pp1 v1 pp2 v2 pp3 v3 pp1 v1 pp2 v2 pp3 v3 pp4 v4 v1 100 v2 1 v1 0 v3 v1 1 v1 100 v2 1 v4 v3 -1 1 v1 0 v3 v1 1 3 41 43 pp1 v10 pp2 v14 pp3 v12 pp4 v13 pp1 v10 pp2 v14 pp3 v12 pp4 v13 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v10 100 v14 1 v1 0 v13 v12 -1 1 v12 -1 1 v13 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v10 100 v14 1 v1 0 v13 v12 -1 1 v12 -1 1 v13 4 27 28 pp1 v1 pp1 v1 pp2 v2 v1 0 v1 100 v2 1 v1 0 5 40 42 pp1 v10 pp2 v11 pp3 v12 pp4 v13 pp1 v10 pp2 v15 pp3 v12 pp4 v13 v1 100 100 v10 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v1 0 v13 v12 -1 1 v12 -1 1 v13 v1 100 100 v10 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v15 0 v1 0 v13 v12 -1 1 v12 -1 1 v13 6 42 44 pp1 v10 pp2 v15 pp3 v12 pp4 v13 pp1 v10 pp2 v15 pp3 v12 pp4 v13 v1 100 100 v10 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v15 0 v1 0 v13 v12 -1 1 v12 -1 1 v13 v1 100 100 v10 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v15 0 v1 0 v13 v12 -1 1 v12 -1 1 v13 7 38 39 pp1 v10 pp2 v11 pp3 v12 pp4 v13 pp1 v10 pp2 v11 pp3 v12 pp4 v13 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v1 0 v13 v12 -1 1 v12 -1 1 v13 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v10 100 v1 0 v13 v12 -1 1 v12 -1 1 v13 8 32 38 pp1 v5 pp2 v2 pp3 v3 pp4 v4 pp1 v5 pp2 v2 pp3 v3 pp4 v4 v5 v4 v1 100 v2 1 v4 v3 -1 1 v1 0 v3 v1 1 v1 100 v2 1 v5 v4 v4 v5 v5 v4 v2 1 1 v2 v4 v3 -1 1 v1 0 0 v1 v1 0 v4 v3 -1 1 v3 -1 1 v4 9 39 41 pp1 v10 pp2 v11 pp3 v12 pp4 v13 pp1 v10 pp2 v14 pp3 v12 pp4 v13 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v10 100 v1 0 v13 v12 -1 1 v12 -1 1 v13 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v10 100 v14 1 v1 0 v13 v12 -1 1 v12 -1 1 v13 10 29 30 pp1 v1 pp2 v2 pp1 v1 pp2 v2 pp3 v3 v1 100 v2 1 v1 0 v1 100 v2 1 v1 0 v3 v1 1 11 47 38 pp1 v18 pp2 v14 pp3 v16 pp4 v17 pp1 v18 pp2 v14 pp3 v16 pp4 v17 v18 v17 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v16 v10 1 v11 1 1 v11 v13 v12 -1 1 v17 v16 -1 1 v1 0 0 v1 v10 100 v14 1 v1 0 v13 v12 -1 1 v12 -1 1 v13 v1 100 v14 1 v18 v17 v17 v18 v18 v17 v14 1 1 v14 v17 v16 -1 1 v1 0 0 v1 v1 0 v17 v16 -1 1 v16 -1 1 v17 12 26 27 pp1 v1 v1 0 13 46 47 pp1 v10 pp2 v14 pp3 v16 pp4 v17 pp1 v18 pp2 v14 pp3 v16 pp4 v17 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v16 v10 1 v11 1 1 v11 v13 v12 -1 1 v17 v16 -1 1 v1 0 0 v1 v10 100 v14 1 v1 0 v13 v12 -1 1 v12 -1 1 v13 v18 v17 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v16 v10 1 v11 1 1 v11 v13 v12 -1 1 v17 v16 -1 1 v1 0 0 v1 v10 100 v14 1 v1 0 v13 v12 -1 1 v12 -1 1 v13 14 38 40 pp1 v10 pp2 v11 pp3 v12 pp4 v13 pp1 v10 pp2 v11 pp3 v12 pp4 v13 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v1 0 v13 v12 -1 1 v12 -1 1 v13 v1 100 100 v10 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v1 0 v13 v12 -1 1 v12 -1 1 v13 15 43 45 pp1 v10 pp2 v14 pp3 v12 pp4 v13 pp1 v10 pp2 v14 pp3 v16 pp4 v13 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v10 100 v14 1 v1 0 v13 v12 -1 1 v12 -1 1 v13 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v16 v10 1 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v10 100 v14 1 v1 0 v13 v12 -1 1 v12 -1 1 v13 16 28 29 pp1 v1 pp2 v2 pp1 v1 pp2 v2 v1 100 v2 1 v1 0 v1 100 v2 1 v1 0 17 45 46 pp1 v10 pp2 v14 pp3 v16 pp4 v13 pp1 v10 pp2 v14 pp3 v16 pp4 v17 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v16 v10 1 v11 1 1 v11 v13 v12 -1 1 v1 0 0 v1 v10 100 v14 1 v1 0 v13 v12 -1 1 v12 -1 1 v13 v1 100 v11 1 v10 v13 v13 v10 v10 v13 v16 v10 1 v11 1 1 v11 v13 v12 -1 1 v17 v16 -1 1 v1 0 0 v1 v10 100 v14 1 v1 0 v13 v12 -1 1 v12 -1 1 v13 32 pp1 v5 pp2 v2 pp3 v3 pp4 v4 38 pp1 v10 pp2 v11 pp3 v12 pp4 v13 39 pp1 v10 pp2 v11 pp3 v12 pp4 v13 40 pp1 v10 pp2 v11 pp3 v12 pp4 v13 41 pp1 v10 pp2 v14 pp3 v12 pp4 v13 42 pp1 v10 pp2 v15 pp3 v12 pp4 v13 43 pp1 v10 pp2 v14 pp3 v12 pp4 v13 44 pp1 v10 pp2 v15 pp3 v12 pp4 v13 45 pp1 v10 pp2 v14 pp3 v16 pp4 v13 46 pp1 v10 pp2 v14 pp3 v16 pp4 v17 47 pp1 v18 pp2 v14 pp3 v16 pp4 v17 26 27 pp1 v1 28 pp1 v1 pp2 v2 29 pp1 v1 pp2 v2 30 pp1 v1 pp2 v2 pp3 v3 31 pp1 v1 pp2 v2 pp3 v3 pp4 v4 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