main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() br label %bb1 bb1: %.0 = phi i32 [%tmp, %bb], [%tmp4, %bb3] %tmp2 = icmp sge i32 %.0, 0 br i1 %tmp2, label %bb3, label %bb5 bb3: %tmp4 = sub i32 %.0, 1 br label %bb1 bb5: ret i32 0 } 2.1 27 32 main bb1 2 tmp v1 .0 v2 tmp2 v3 v2 v1 v3 1 v2 0 33 main bb1 2 tmp v1 .0 v2 tmp2 v4 v2 v1 v4 0 v2 0 34 main bb3 0 tmp v1 .0 v2 tmp2 v3 v2 v1 v3 1 v2 0 35 main bb5 0 tmp v1 .0 v2 tmp2 v4 v2 v1 v4 0 v2 0 36 main bb3 1 tmp v1 .0 v2 tmp2 v3 tmp4 v5 v2 v1 v3 1 v5 v2 -1 1 v2 0 37 main bb1 1 tmp v1 .0 v6 tmp2 v3 tmp4 v5 v2 v1 v3 1 v5 v2 -1 1 v6 v5 v2 0 46 main bb1 1 tmp v11 .0 v12 tmp2 v13 tmp4 v14 v2 v11 v13 1 v12 v14 v2 0 v2 v11 v11 v2 v13 1 1 v13 v12 v14 v14 v12 47 main bb1 1 tmp v11 .0 v12 tmp2 v13 tmp4 v14 v2 v11 v13 1 v12 v14 v2 0 v2 v11 v11 v2 v13 1 1 v13 v12 v14 v14 v12 v12 0 48 main bb1 1 tmp v11 .0 v12 tmp2 v13 tmp4 v14 v2 v11 v13 1 v12 v14 v12 0 v2 0 v2 v11 v11 v2 v13 1 1 v13 v12 v14 v14 v12 49 main bb1 2 tmp v11 .0 v12 tmp2 v15 tmp4 v14 v2 v11 v13 1 v12 v14 v15 1 v2 0 v2 v11 v11 v2 v13 1 1 v13 v12 v14 v14 v12 v12 0 50 main bb1 2 tmp v11 .0 v12 tmp2 v16 tmp4 v14 v2 v11 v13 1 v12 v14 v16 0 v12 0 v2 0 v2 v11 v11 v2 v13 1 1 v13 v12 v14 v14 v12 51 main bb3 0 tmp v11 .0 v12 tmp2 v15 tmp4 v14 v2 v11 v13 1 v12 v14 v15 1 v2 0 v2 v11 v11 v2 v13 1 1 v13 v12 v14 v14 v12 v12 0 52 main bb5 0 tmp v11 .0 v12 tmp2 v16 tmp4 v14 v2 v11 v13 1 v12 v14 v16 0 v12 0 v2 0 v2 v11 v11 v2 v13 1 1 v13 v12 v14 v14 v12 53 main bb3 1 tmp v11 .0 v12 tmp2 v15 tmp4 v17 v2 v11 v13 1 v12 v14 v15 1 v17 v12 -1 1 v2 0 v2 v11 v11 v2 v13 1 1 v13 v12 v14 v14 v12 v12 0 54 main bb1 1 tmp v11 .0 v18 tmp2 v15 tmp4 v17 v2 v11 v13 1 v12 v14 v15 1 v17 v12 -1 1 v18 v17 v2 0 v2 v11 v11 v2 v13 1 1 v13 v12 v14 v14 v12 v12 0 27 main bb 0 28 main bb 1 tmp v1 29 main bb1 1 tmp v1 .0 v2 v2 v1 30 main bb1 1 tmp v1 .0 v2 v2 v1 v2 0 31 main bb1 1 tmp v1 .0 v2 v2 v1 v2 0 32 34 33 35 34 36 v5 35 36
37 v6 v5
37 46 v11 v1 v12 v6 v13 v3 v14 v5 46 47 48 v12 0 47 49 v15 48 50 v16 49 51 50 52 51 53 v17 52 53
54 v18 v17
54 46 v11 v11 v12 v18 v13 v15 v14 v17 27 28 v1 28
29 v2 v1
29 30 31 v2 0 30 32 v3 31 33 v4 34 49 36 53 30 32 51 29 54 47 50 33 48 46 37 27 28 31 1 31 33 pp1 v2 pp2 v1 pp1 v2 pp2 v1 pp3 v4 v2 0 v2 v1 v2 0 v2 v1 v4 0 2 51 53 pp1 v12 pp2 v11 pp3 v15 pp4 v14 pp1 v12 pp2 v11 pp3 v15 pp4 v17 v13 1 1 v13 0 v12 v2 v11 v15 1 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 0 v12 v17 v12 -1 1 v2 v11 v13 1 v2 v11 v11 v2 v13 1 1 v13 v15 1 v12 v14 v14 v12 0 v2 v12 v14 3 54 46 pp1 v18 pp2 v11 pp3 v15 pp4 v17 pp1 v18 pp2 v11 pp3 v15 pp4 v17 v18 v17 0 v12 v17 v12 -1 1 v2 v11 v13 1 v2 v11 v11 v2 v13 1 1 v13 v15 1 v12 v14 v14 v12 0 v2 v12 v14 v15 1 1 v15 v2 v11 v18 v17 v17 v18 0 v2 v15 1 v18 v17 v2 v11 v11 v2 4 37 46 pp1 v6 pp2 v1 pp3 v3 pp4 v5 pp1 v6 pp2 v1 pp3 v3 pp4 v5 v2 v1 v5 v2 -1 1 v3 1 0 v2 v6 v5 v3 1 1 v3 v2 v1 v6 v5 v5 v6 0 v2 v3 1 v6 v5 v2 v1 v1 v2 5 46 47 pp1 v12 pp2 v11 pp3 v13 pp4 v14 pp1 v12 pp2 v11 pp3 v13 pp4 v14 v13 1 1 v13 v2 v11 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 v13 1 1 v13 0 v12 v2 v11 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 6 46 48 pp1 v12 pp2 v11 pp3 v13 pp4 v14 pp1 v12 pp2 v11 pp3 v13 pp4 v14 v13 1 1 v13 v2 v11 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 v13 1 1 v13 v2 v11 v12 0 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 7 49 51 pp1 v12 pp2 v11 pp3 v15 pp4 v14 pp1 v12 pp2 v11 pp3 v15 pp4 v14 v13 1 1 v13 0 v12 v2 v11 v15 1 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 v13 1 1 v13 0 v12 v2 v11 v15 1 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 8 29 31 pp1 v2 pp2 v1 pp1 v2 pp2 v1 v2 v1 v2 0 v2 v1 9 36 37 pp1 v2 pp2 v1 pp3 v3 pp4 v5 pp1 v6 pp2 v1 pp3 v3 pp4 v5 v2 v1 v5 v2 -1 1 v3 1 0 v2 v2 v1 v5 v2 -1 1 v3 1 0 v2 v6 v5 10 53 54 pp1 v12 pp2 v11 pp3 v15 pp4 v17 pp1 v18 pp2 v11 pp3 v15 pp4 v17 0 v12 v17 v12 -1 1 v2 v11 v13 1 v2 v11 v11 v2 v13 1 1 v13 v15 1 v12 v14 v14 v12 0 v2 v12 v14 v18 v17 0 v12 v17 v12 -1 1 v2 v11 v13 1 v2 v11 v11 v2 v13 1 1 v13 v15 1 v12 v14 v14 v12 0 v2 v12 v14 11 48 50 pp1 v12 pp2 v11 pp3 v13 pp4 v14 pp1 v12 pp2 v11 pp3 v16 pp4 v14 v13 1 1 v13 v2 v11 v12 0 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 v13 1 1 v13 v2 v11 v16 0 v12 0 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 12 33 35 pp1 v2 pp2 v1 pp3 v4 pp1 v2 pp2 v1 pp3 v4 v2 0 v2 v1 v4 0 v2 0 v2 v1 v4 0 13 28 29 pp1 v1 pp1 v2 pp2 v1 v2 v1 14 32 34 pp1 v2 pp2 v1 pp3 v3 pp1 v2 pp2 v1 pp3 v3 v2 v1 v3 1 0 v2 v2 v1 v3 1 0 v2 15 47 49 pp1 v12 pp2 v11 pp3 v13 pp4 v14 pp1 v12 pp2 v11 pp3 v15 pp4 v14 v13 1 1 v13 0 v12 v2 v11 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 v13 1 1 v13 0 v12 v2 v11 v15 1 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 16 50 52 pp1 v12 pp2 v11 pp3 v16 pp4 v14 pp1 v12 pp2 v11 pp3 v16 pp4 v14 v13 1 1 v13 v2 v11 v16 0 v12 0 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 v13 1 1 v13 v2 v11 v16 0 v12 0 v12 v14 v14 v12 0 v2 v13 1 v12 v14 v2 v11 v11 v2 17 29 30 pp1 v2 pp2 v1 pp1 v2 pp2 v1 v2 v1 v2 v1 0 v2 18 27 28 pp1 v1 19 30 32 pp1 v2 pp2 v1 pp1 v2 pp2 v1 pp3 v3 v2 v1 0 v2 v2 v1 v3 1 0 v2 20 34 36 pp1 v2 pp2 v1 pp3 v3 pp1 v2 pp2 v1 pp3 v3 pp4 v5 v2 v1 v3 1 0 v2 v2 v1 v5 v2 -1 1 v3 1 0 v2 32 pp1 v2 pp2 v1 pp3 v3 33 pp1 v2 pp2 v1 pp3 v4 34 pp1 v2 pp2 v1 pp3 v3 35 pp1 v2 pp2 v1 pp3 v4 36 pp1 v2 pp2 v1 pp3 v3 pp4 v5 37 pp1 v6 pp2 v1 pp3 v3 pp4 v5 46 pp1 v12 pp2 v11 pp3 v13 pp4 v14 47 pp1 v12 pp2 v11 pp3 v13 pp4 v14 48 pp1 v12 pp2 v11 pp3 v13 pp4 v14 49 pp1 v12 pp2 v11 pp3 v15 pp4 v14 50 pp1 v12 pp2 v11 pp3 v16 pp4 v14 51 pp1 v12 pp2 v11 pp3 v15 pp4 v14 52 pp1 v12 pp2 v11 pp3 v16 pp4 v14 53 pp1 v12 pp2 v11 pp3 v15 pp4 v17 54 pp1 v18 pp2 v11 pp3 v15 pp4 v17 27 28 pp1 v1 29 pp1 v2 pp2 v1 30 pp1 v2 pp2 v1 31 pp1 v2 pp2 v1 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