main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp2 = call i32 @__VERIFIER_nondet_int() br label %bb3 bb3: %.01 = phi i32 [%tmp2, %bb], [%.0, %bb9] %.0 = phi i32 [%tmp, %bb], [%.01, %bb9] %tmp4 = icmp ne i32 %.0, 0 br i1 %tmp4, label %bb5, label %bb7 bb5: %tmp6 = icmp ne i32 %.01, 0 br label %bb7 bb7: %tmp8 = phi i1 [0, %bb3], [%tmp6, %bb5] br i1 %tmp8, label %bb9, label %bb10 bb9: br label %bb3 bb10: ret i32 0 } 2.1 42 66 main bb7 1 tmp v24 tmp2 v25 .01 v26 .0 v27 tmp4 v28 tmp6 v29 tmp8 v30 v28 1 v29 1 v30 v29 v27 0 v26 0 v28 1 1 v28 v29 1 1 v29 v30 v29 v29 v30 67 main bb9 0 tmp v24 tmp2 v25 .01 v26 .0 v27 tmp4 v28 tmp6 v29 tmp8 v30 v28 1 v29 1 v30 v29 v27 0 v26 0 v28 1 1 v28 v29 1 1 v29 v30 v29 v29 v30 68 main bb3 2 tmp v24 tmp2 v25 .01 v38 .0 v39 tmp4 v28 tmp6 v29 tmp8 v30 v28 1 v29 1 v30 v29 v30 1 v38 v27 v39 v26 v27 0 v26 0 v28 1 1 v28 v29 1 1 v29 v30 v29 v29 v30 69 main bb3 3 tmp v24 tmp2 v25 .01 v38 .0 v39 tmp4 v40 tmp6 v29 tmp8 v30 v28 1 v29 1 v30 v29 v30 1 v38 v27 v39 v26 v40 1 v27 0 v26 0 v28 1 1 v28 v29 1 1 v29 v30 v29 v29 v30 70 main bb5 0 tmp v24 tmp2 v25 .01 v38 .0 v39 tmp4 v40 tmp6 v29 tmp8 v30 v28 1 v29 1 v30 v29 v30 1 v38 v27 v39 v26 v40 1 v27 0 v26 0 v39 0 v28 1 1 v28 v29 1 1 v29 v30 v29 v29 v30 71 main bb5 1 tmp v24 tmp2 v25 .01 v38 .0 v39 tmp4 v40 tmp6 v41 tmp8 v30 v28 1 v29 1 v30 v29 v30 1 v38 v27 v39 v26 v40 1 v41 1 v27 0 v26 0 v39 0 v28 1 1 v28 v29 1 1 v29 v30 v29 v29 v30 72 main bb7 1 tmp v24 tmp2 v25 .01 v38 .0 v39 tmp4 v40 tmp6 v41 tmp8 v42 v28 1 v29 1 v30 v29 v30 1 v38 v27 v39 v26 v40 1 v41 1 v42 v41 v27 0 v26 0 v39 0 v38 0 v28 1 1 v28 v29 1 1 v29 v30 v29 v29 v30 42 main bb 0 43 main bb 1 tmp v1 44 main bb 2 tmp v1 tmp2 v2 45 main bb3 2 tmp v1 tmp2 v2 .01 v3 .0 v4 v3 v2 v4 v1 46 main bb3 2 tmp v1 tmp2 v2 .01 v3 .0 v4 v3 v2 v4 v1 v4 0 47 main bb3 2 tmp v1 tmp2 v2 .01 v3 .0 v4 v3 v2 v4 v1 v4 0 48 main bb3 3 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 v3 v2 v4 v1 v5 1 v4 0 49 main bb3 3 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v6 v3 v2 v4 v1 v4 0 v6 0 50 main bb5 0 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 v3 v2 v4 v1 v5 1 v4 0 51 main bb7 1 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v6 tmp8 v7 v3 v2 v4 v1 v4 0 v6 0 v7 0 52 main bb5 0 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 v3 v2 v4 v1 v5 1 v4 0 v3 0 53 main bb5 0 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 v3 v2 v4 v1 v5 1 v3 0 v4 0 54 main bb10 0 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v6 tmp8 v7 v3 v2 v4 v1 v4 0 v6 0 v7 0 55 main bb5 1 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 tmp6 v8 v3 v2 v4 v1 v5 1 v8 1 v4 0 v3 0 56 main bb5 1 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 tmp6 v9 v3 v2 v4 v1 v5 1 v3 0 v9 0 v4 0 57 main bb7 1 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 tmp6 v8 tmp8 v10 v3 v2 v4 v1 v5 1 v8 1 v10 v8 v4 0 v3 0 58 main bb7 1 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 tmp6 v9 tmp8 v11 v3 v2 v4 v1 v5 1 v3 0 v9 0 v11 v9 v4 0 60 main bb10 0 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 tmp6 v9 tmp8 v11 v3 v2 v4 v1 v5 1 v3 0 v9 0 v11 v9 v4 0 66 67 67
68 v38 v27 v39 v26
68 69 v40 69 70 70 71 v41 71
72 v42 v41
72 66 v24 v24 v25 v25 v26 v38 v27 v39 v28 v40 v29 v41 v30 v42 42 43 v1 43 44 v2 44
45 v3 v2 v4 v1
45 46 47 v4 0 46 48 v5 47 49 v6 48 50 49 51 v7 0 50 52 53 v3 0 51 54 52 55 v8 53 56 v9 54 55
57 v10 v8
56
58 v11 v9
57 66 v24 v1 v25 v2 v26 v3 v27 v4 v28 v5 v29 v8 v30 v10 58 60 60 66 49 68 70 53 72 51 43 47 57 71 50 67 69 48 46 56 44 58 42 55 52 45 1 72 66 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v41 pp7 v42 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v41 pp7 v42 v28 1 0 v39 v28 1 1 v28 v29 1 0 v27 0 v38 v30 v29 v29 v30 v30 v29 v30 1 v38 v27 v39 v26 v41 1 0 v26 v29 1 1 v29 v40 1 v42 v41 v40 1 v42 v41 v40 1 1 v40 v41 1 0 v38 v41 1 1 v41 0 v39 v42 v41 v41 v42 2 71 72 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v41 pp7 v30 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v41 pp7 v42 v28 1 0 v39 v28 1 1 v28 v29 1 0 v27 0 v38 v30 v29 v29 v30 v30 v29 v30 1 v38 v27 v39 v26 v41 1 0 v26 v29 1 1 v29 v40 1 v28 1 0 v39 v28 1 1 v28 v29 1 0 v27 0 v38 v30 v29 v29 v30 v30 v29 v30 1 v38 v27 v39 v26 v41 1 0 v26 v29 1 1 v29 v40 1 v42 v41 3 49 51 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 pp6 v7 v6 0 v4 0 v3 v2 v4 v1 v6 0 v4 0 v7 0 v3 v2 v4 v1 4 66 67 pp1 v27 pp2 v26 pp3 v24 pp4 v25 pp5 v28 pp6 v29 pp7 v30 pp1 v27 pp2 v26 pp3 v24 pp4 v25 pp5 v28 pp6 v29 pp7 v30 v28 1 v30 v29 v28 1 1 v28 v29 1 0 v26 v29 1 1 v29 0 v27 v30 v29 v29 v30 v28 1 v30 v29 v30 1 v28 1 1 v28 v29 1 0 v26 v29 1 1 v29 0 v27 v30 v29 v29 v30 5 57 66 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v8 pp7 v10 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v8 pp7 v10 v10 v8 v5 1 0 v3 0 v4 v3 v2 v4 v1 v8 1 v5 1 v10 v8 v5 1 1 v5 v8 1 0 v3 v8 1 1 v8 0 v4 v10 v8 v8 v10 6 55 57 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v8 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v8 pp7 v10 v5 1 0 v3 0 v4 v3 v2 v4 v1 v8 1 v10 v8 v5 1 0 v3 0 v4 v3 v2 v4 v1 v8 1 7 70 71 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v29 pp7 v30 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v41 pp7 v30 v28 1 0 v39 v28 1 1 v28 v29 1 0 v27 v30 v29 v29 v30 v30 v29 v30 1 v38 v27 v39 v26 0 v26 v29 1 1 v29 v40 1 v28 1 0 v39 v28 1 1 v28 v29 1 0 v27 0 v38 v30 v29 v29 v30 v30 v29 v30 1 v38 v27 v39 v26 v41 1 0 v26 v29 1 1 v29 v40 1 8 69 70 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v29 pp7 v30 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v29 pp7 v30 v28 1 0 v39 v28 1 1 v28 v29 1 0 v27 v30 v29 v29 v30 v30 v29 v30 1 v38 v27 v39 v26 0 v26 v29 1 1 v29 v40 1 v28 1 0 v39 v28 1 1 v28 v29 1 0 v27 v30 v29 v29 v30 v30 v29 v30 1 v38 v27 v39 v26 0 v26 v29 1 1 v29 v40 1 9 45 47 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 v3 v2 v4 v1 v4 0 v3 v2 v4 v1 10 53 56 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v9 v5 1 v3 0 0 v4 v3 v2 v4 v1 v5 1 v3 0 0 v4 v3 v2 v4 v1 v9 0 11 50 53 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 v5 1 0 v4 v3 v2 v4 v1 v5 1 v3 0 0 v4 v3 v2 v4 v1 12 45 46 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 v3 v2 v4 v1 0 v4 v3 v2 v4 v1 13 46 48 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 0 v4 v3 v2 v4 v1 v5 1 0 v4 v3 v2 v4 v1 14 51 54 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 pp6 v7 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 pp6 v7 v6 0 v4 0 v7 0 v3 v2 v4 v1 v6 0 v4 0 v7 0 v3 v2 v4 v1 15 42 43 pp1 v1 16 58 60 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v9 pp7 v11 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v9 pp7 v11 v5 1 v3 0 0 v4 v11 v9 v3 v2 v4 v1 v9 0 v5 1 v3 0 0 v4 v11 v9 v3 v2 v4 v1 v9 0 v11 0 17 47 49 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 v4 0 v3 v2 v4 v1 v6 0 v4 0 v3 v2 v4 v1 18 48 50 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 v5 1 0 v4 v3 v2 v4 v1 v5 1 0 v4 v3 v2 v4 v1 19 68 69 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v28 pp6 v29 pp7 v30 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v29 pp7 v30 v28 1 v28 1 1 v28 v29 1 0 v27 v30 v29 v29 v30 v30 v29 v30 1 v38 v27 v39 v26 0 v26 v29 1 1 v29 v28 1 0 v39 v28 1 1 v28 v29 1 0 v27 v30 v29 v29 v30 v30 v29 v30 1 v38 v27 v39 v26 0 v26 v29 1 1 v29 v40 1 20 56 58 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v9 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v9 pp7 v11 v5 1 v3 0 0 v4 v3 v2 v4 v1 v9 0 v5 1 v3 0 0 v4 v11 v9 v3 v2 v4 v1 v9 0 21 67 68 pp1 v27 pp2 v26 pp3 v24 pp4 v25 pp5 v28 pp6 v29 pp7 v30 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v28 pp6 v29 pp7 v30 v28 1 v30 v29 v30 1 v28 1 1 v28 v29 1 0 v26 v29 1 1 v29 0 v27 v30 v29 v29 v30 v28 1 v28 1 1 v28 v29 1 0 v27 v30 v29 v29 v30 v30 v29 v30 1 v38 v27 v39 v26 0 v26 v29 1 1 v29 22 52 55 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v8 v5 1 0 v3 0 v4 v3 v2 v4 v1 v5 1 0 v3 0 v4 v3 v2 v4 v1 v8 1 23 43 44 pp1 v1 pp1 v1 pp2 v2 24 44 45 pp1 v1 pp2 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 v3 v2 v4 v1 25 50 52 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 v5 1 0 v4 v3 v2 v4 v1 v5 1 0 v3 0 v4 v3 v2 v4 v1 66 pp1 v27 pp2 v26 pp3 v24 pp4 v25 pp5 v28 pp6 v29 pp7 v30 67 pp1 v27 pp2 v26 pp3 v24 pp4 v25 pp5 v28 pp6 v29 pp7 v30 68 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v28 pp6 v29 pp7 v30 69 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v29 pp7 v30 70 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v29 pp7 v30 71 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v41 pp7 v30 72 pp1 v39 pp2 v38 pp3 v24 pp4 v25 pp5 v40 pp6 v41 pp7 v42 42 43 pp1 v1 44 pp1 v1 pp2 v2 45 pp1 v4 pp2 v3 pp3 v1 pp4 v2 46 pp1 v4 pp2 v3 pp3 v1 pp4 v2 47 pp1 v4 pp2 v3 pp3 v1 pp4 v2 48 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 49 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 50 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 51 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 pp6 v7 52 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 53 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 54 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 pp6 v7 55 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v8 56 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v9 57 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v8 pp7 v10 58 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v9 pp7 v11 60 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v9 pp7 v11 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