main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp1 = call i32 @__VERIFIER_nondet_int() %tmp2 = icmp sgt i32 %tmp, 0 br i1 %tmp2, label %bb3, label %bb9 bb3: br label %bb4 bb4: %.0 = phi i32 [%tmp1, %bb3], [%tmp7, %bb6] %tmp5 = icmp sgt i32 %tmp, %.0 br i1 %tmp5, label %bb6, label %bb8 bb6: %tmp7 = add i32 %.0, %tmp br label %bb4 bb8: br label %bb9 bb9: ret i32 0 } 2.1 39 67 main bb4 1 tmp v14 tmp1 v15 tmp2 v16 .0 v17 tmp5 v18 tmp7 v19 v16 1 v5 v15 v18 1 v17 v19 v14 0 v14 v5 v16 1 1 v16 v5 v15 v15 v5 v18 1 1 v18 v17 v19 v19 v17 68 main bb4 1 tmp v14 tmp1 v15 tmp2 v16 .0 v17 tmp5 v18 tmp7 v19 v16 1 v5 v15 v18 1 v17 v19 v14 0 v14 v5 v14 v17 v16 1 1 v16 v5 v15 v15 v5 v18 1 1 v18 v17 v19 v19 v17 69 main bb4 1 tmp v14 tmp1 v15 tmp2 v16 .0 v17 tmp5 v18 tmp7 v19 v16 1 v5 v15 v18 1 v17 v19 v14 0 v14 v5 v16 1 1 v16 v5 v15 v15 v5 v18 1 1 v18 v17 v19 v19 v17 v14 v17 70 main bb4 2 tmp v14 tmp1 v15 tmp2 v16 .0 v17 tmp5 v20 tmp7 v19 v16 1 v5 v15 v18 1 v17 v19 v20 1 v14 0 v14 v5 v14 v17 v16 1 1 v16 v5 v15 v15 v5 v18 1 1 v18 v17 v19 v19 v17 71 main bb4 2 tmp v14 tmp1 v15 tmp2 v16 .0 v17 tmp5 v21 tmp7 v19 v16 1 v5 v15 v18 1 v17 v19 v21 0 v14 0 v14 v5 v16 1 1 v16 v5 v15 v15 v5 v18 1 1 v18 v17 v19 v19 v17 v14 v17 72 main bb6 0 tmp v14 tmp1 v15 tmp2 v16 .0 v17 tmp5 v20 tmp7 v19 v16 1 v5 v15 v18 1 v17 v19 v20 1 v14 0 v14 v5 v14 v17 v16 1 1 v16 v5 v15 v15 v5 v18 1 1 v18 v17 v19 v19 v17 73 main bb8 0 tmp v14 tmp1 v15 tmp2 v16 .0 v17 tmp5 v21 tmp7 v19 v16 1 v5 v15 v18 1 v17 v19 v21 0 v14 0 v14 v5 v16 1 1 v16 v5 v15 v15 v5 v18 1 1 v18 v17 v19 v19 v17 v14 v17 74 main bb6 1 tmp v14 tmp1 v15 tmp2 v16 .0 v17 tmp5 v20 tmp7 v22 v16 1 v5 v15 v18 1 v17 v19 v20 1 v22 v17 v14 v14 0 v14 v5 v14 v17 v16 1 1 v16 v5 v15 v15 v5 v18 1 1 v18 v17 v19 v19 v17 75 main bb9 0 tmp v14 tmp1 v15 tmp2 v16 .0 v17 tmp5 v21 tmp7 v19 v16 1 v5 v15 v18 1 v17 v19 v21 0 v14 0 v14 v5 v16 1 1 v16 v5 v15 v15 v5 v18 1 1 v18 v17 v19 v19 v17 v14 v17 76 main bb4 1 tmp v14 tmp1 v15 tmp2 v16 .0 v23 tmp5 v20 tmp7 v22 v16 1 v5 v15 v18 1 v17 v19 v20 1 v22 v17 v14 v23 v22 v14 0 v14 v5 v14 v17 v16 1 1 v16 v5 v15 v15 v5 v18 1 1 v18 v17 v19 v19 v17 39 main bb 0 40 main bb 1 tmp v1 41 main bb 2 tmp v1 tmp1 v2 42 main bb 2 tmp v1 tmp1 v2 v1 0 43 main bb 2 tmp v1 tmp1 v2 v1 0 44 main bb 3 tmp v1 tmp1 v2 tmp2 v3 v3 1 v1 0 45 main bb 3 tmp v1 tmp1 v2 tmp2 v4 v4 0 v1 0 46 main bb3 0 tmp v1 tmp1 v2 tmp2 v3 v3 1 v1 0 47 main bb9 0 tmp v1 tmp1 v2 tmp2 v4 v4 0 v1 0 48 main bb4 1 tmp v1 tmp1 v2 tmp2 v3 .0 v5 v3 1 v5 v2 v1 0 49 main bb4 1 tmp v1 tmp1 v2 tmp2 v3 .0 v5 v3 1 v5 v2 v1 0 v1 v5 50 main bb4 1 tmp v1 tmp1 v2 tmp2 v3 .0 v5 v3 1 v5 v2 v1 0 v1 v5 51 main bb4 2 tmp v1 tmp1 v2 tmp2 v3 .0 v5 tmp5 v6 v3 1 v5 v2 v6 1 v1 0 v1 v5 52 main bb4 2 tmp v1 tmp1 v2 tmp2 v3 .0 v5 tmp5 v7 v3 1 v5 v2 v7 0 v1 0 v1 v5 53 main bb6 0 tmp v1 tmp1 v2 tmp2 v3 .0 v5 tmp5 v6 v3 1 v5 v2 v6 1 v1 0 v1 v5 54 main bb8 0 tmp v1 tmp1 v2 tmp2 v3 .0 v5 tmp5 v7 v3 1 v5 v2 v7 0 v1 0 v1 v5 55 main bb6 1 tmp v1 tmp1 v2 tmp2 v3 .0 v5 tmp5 v6 tmp7 v8 v3 1 v5 v2 v6 1 v8 v5 v1 v1 0 v1 v5 56 main bb9 0 tmp v1 tmp1 v2 tmp2 v3 .0 v5 tmp5 v7 v3 1 v5 v2 v7 0 v1 0 v1 v5 57 main bb4 1 tmp v1 tmp1 v2 tmp2 v3 .0 v9 tmp5 v6 tmp7 v8 v3 1 v5 v2 v6 1 v8 v5 v1 v9 v8 v1 0 v1 v5 67 68 69 v14 v17 68 70 v20 69 71 v21 70 72 71 73 72 74 v22 73
75
74
76 v23 v22
75 76 67 v14 v14 v15 v15 v16 v16 v17 v23 v18 v20 v19 v22 39 40 v1 40 41 v2 41 42 43 v1 0 42 44 v3 43 45 v4 44 46 45 47 46
48 v5 v2
47 48 49 50 v1 v5 49 51 v6 50 52 v7 51 53 52 54 53 55 v8 54
56
55
57 v9 v8
56 57 67 v14 v1 v15 v2 v16 v3 v17 v9 v18 v6 v19 v8 68 72 51 43 67 39 46 44 73 52 45 49 70 53 40 74 54 57 71 50 69 48 42 76 55 41 1 42 44 pp1 v1 pp2 v2 pp1 v1 pp2 v2 pp3 v3 0 v1 v3 1 0 v1 2 52 54 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v7 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v7 v1 v5 v7 0 v3 1 v5 v2 0 v1 v1 v5 v7 0 v3 1 v5 v2 0 v1 3 39 40 pp1 v1 4 53 55 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v6 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v6 pp6 v8 v6 1 v5 v1 v3 1 v5 v2 0 v1 v6 1 v5 v1 v8 v5 v1 v3 1 v5 v2 0 v1 5 49 51 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v6 v5 v1 v3 1 v5 v2 0 v1 v6 1 v5 v1 v3 1 v5 v2 0 v1 6 57 67 pp1 v9 pp2 v1 pp3 v2 pp4 v3 pp5 v6 pp6 v8 pp1 v9 pp2 v1 pp3 v2 pp4 v3 pp5 v6 pp6 v8 v6 1 v5 v1 v8 v5 v1 v3 1 v9 v8 v5 v2 0 v1 v3 1 1 v3 v5 v2 v3 1 v5 v1 v9 v8 0 v1 v5 v2 v2 v5 v9 v8 v8 v9 v6 1 1 v6 v6 1 7 55 57 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v6 pp6 v8 pp1 v9 pp2 v1 pp3 v2 pp4 v3 pp5 v6 pp6 v8 v6 1 v5 v1 v8 v5 v1 v3 1 v5 v2 0 v1 v6 1 v5 v1 v8 v5 v1 v3 1 v9 v8 v5 v2 0 v1 8 54 56 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v7 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v7 v1 v5 v7 0 v3 1 v5 v2 0 v1 v1 v5 v7 0 v3 1 v5 v2 0 v1 9 50 52 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v7 v1 v5 v3 1 v5 v2 0 v1 v1 v5 v7 0 v3 1 v5 v2 0 v1 10 43 45 pp1 v1 pp2 v2 pp1 v1 pp2 v2 pp3 v4 v1 0 v1 0 v4 0 11 67 69 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v18 pp6 v19 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v18 pp6 v19 v16 1 1 v16 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v16 1 1 v16 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v14 v17 12 44 46 pp1 v1 pp2 v2 pp3 v3 pp1 v1 pp2 v2 pp3 v3 v3 1 0 v1 v3 1 0 v1 13 68 70 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v18 pp6 v19 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v19 v16 1 1 v16 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v17 v14 v16 1 1 v16 v20 1 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v17 v14 14 72 74 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v19 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v22 v16 1 1 v16 v20 1 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v17 v14 v16 1 1 v16 v20 1 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v22 v17 v14 v17 v14 15 40 41 pp1 v1 pp1 v1 pp2 v2 16 46 48 pp1 v1 pp2 v2 pp3 v3 pp1 v5 pp2 v1 pp3 v2 pp4 v3 v3 1 0 v1 v3 1 v5 v2 0 v1 17 48 49 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp1 v5 pp2 v1 pp3 v2 pp4 v3 v3 1 v5 v2 0 v1 v5 v1 v3 1 v5 v2 0 v1 18 69 71 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v18 pp6 v19 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v21 pp6 v19 v16 1 1 v16 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v14 v17 v16 1 1 v16 v21 0 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v14 v17 19 41 42 pp1 v1 pp2 v2 pp1 v1 pp2 v2 0 v1 20 74 76 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v22 pp1 v23 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v22 v16 1 1 v16 v20 1 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v22 v17 v14 v17 v14 v16 1 1 v16 v20 1 v5 v15 v16 1 v5 v14 v17 v19 v23 v22 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v22 v17 v14 v17 v14 21 45 47 pp1 v1 pp2 v2 pp3 v4 pp1 v1 pp2 v2 pp3 v4 v1 0 v4 0 v1 0 v4 0 22 51 53 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v6 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v6 v6 1 v5 v1 v3 1 v5 v2 0 v1 v6 1 v5 v1 v3 1 v5 v2 0 v1 23 71 73 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v21 pp6 v19 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v21 pp6 v19 v16 1 1 v16 v21 0 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v14 v17 v16 1 1 v16 v21 0 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v14 v17 24 48 50 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp1 v5 pp2 v1 pp3 v2 pp4 v3 v3 1 v5 v2 0 v1 v1 v5 v3 1 v5 v2 0 v1 25 70 72 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v19 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v19 v16 1 1 v16 v20 1 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v17 v14 v16 1 1 v16 v20 1 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v17 v14 26 76 67 pp1 v23 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v22 pp1 v23 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v22 v16 1 1 v16 v20 1 v5 v15 v16 1 v5 v14 v17 v19 v23 v22 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v22 v17 v14 v17 v14 v16 1 1 v16 v5 v15 v16 1 v5 v14 v23 v22 0 v14 v5 v15 v15 v5 v23 v22 v22 v23 v20 1 1 v20 v20 1 27 41 43 pp1 v1 pp2 v2 pp1 v1 pp2 v2 v1 0 28 73 75 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v21 pp6 v19 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v21 pp6 v19 v16 1 1 v16 v21 0 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v14 v17 v16 1 1 v16 v21 0 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v14 v17 29 67 68 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v18 pp6 v19 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v18 pp6 v19 v16 1 1 v16 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v16 1 1 v16 v5 v15 v16 1 v5 v14 v17 v19 0 v14 v5 v15 v15 v5 v17 v19 v19 v17 v18 1 1 v18 v18 1 v17 v14 67 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v18 pp6 v19 68 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v18 pp6 v19 69 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v18 pp6 v19 70 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v19 71 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v21 pp6 v19 72 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v19 73 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v21 pp6 v19 74 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v22 75 pp1 v17 pp2 v14 pp3 v15 pp4 v16 pp5 v21 pp6 v19 76 pp1 v23 pp2 v14 pp3 v15 pp4 v16 pp5 v20 pp6 v22 39 40 pp1 v1 41 pp1 v1 pp2 v2 42 pp1 v1 pp2 v2 43 pp1 v1 pp2 v2 44 pp1 v1 pp2 v2 pp3 v3 45 pp1 v1 pp2 v2 pp3 v4 46 pp1 v1 pp2 v2 pp3 v3 47 pp1 v1 pp2 v2 pp3 v4 48 pp1 v5 pp2 v1 pp3 v2 pp4 v3 49 pp1 v5 pp2 v1 pp3 v2 pp4 v3 50 pp1 v5 pp2 v1 pp3 v2 pp4 v3 51 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v6 52 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v7 53 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v6 54 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v7 55 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v6 pp6 v8 56 pp1 v5 pp2 v1 pp3 v2 pp4 v3 pp5 v7 57 pp1 v9 pp2 v1 pp3 v2 pp4 v3 pp5 v6 pp6 v8 68 68 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 pp6 pp6 72 72 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 pp6 pp6 51 51 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 43 43 pp1 pp1 pp2 pp2 67 67 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 pp6 pp6 39 39 46 46 pp1 pp1 pp2 pp2 pp3 pp3 44 44 pp1 pp1 pp2 pp2 pp3 pp3 73 73 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 pp6 pp6 52 52 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 45 45 pp1 pp1 pp2 pp2 pp3 pp3 49 49 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 70 70 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 pp6 pp6 53 53 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 40 40 pp1 pp1 74 74 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 pp6 pp6 54 54 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 57 57 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 pp6 pp6 71 71 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 pp6 pp6 50 50 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 69 69 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 pp6 pp6 48 48 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 42 42 pp1 pp1 pp2 pp2 76 76 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 pp6 pp6 55 55 pp1 pp1 pp2 pp2 pp3 pp3 pp4 pp4 pp5 pp5 pp6 pp6 41 41 pp1 pp1 pp2 pp2 67 68 70 72 76 74 67 -1 pp1 1 pp2 68 -1 pp1 1 pp2 76 1 pp2 -1 pp6 74 -1 pp1 1 pp2 72 -1 pp1 1 pp2 70 -1 pp1 1 pp2 0 20 AProVE AProVE Commit ID: unknown Statistics for single proof: 100,00 % (7 real / 0 unknown / 0 assumptions / 7 total proof steps) http://aprove.informatik.rwth-aachen.de John Doe