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 [%tmp, %bb], [%tmp4, %bb3] %.0 = phi i32 [%tmp2, %bb], [%.01, %bb3] %tmp4 = sub i32 0, %.0 br label %bb3 } 2.1 24 32 main bb3 2 tmp v11 tmp2 v12 .01 v13 .0 v14 tmp4 v15 v3 v11 v4 v12 v13 v15 v3 v11 v11 v3 v4 v12 v12 v4 v13 v15 v15 v13 33 main bb3 3 tmp v11 tmp2 v12 .01 v13 .0 v14 tmp4 v16 v3 v11 v4 v12 v13 v15 v16 0 -1 v14 v3 v11 v11 v3 v4 v12 v12 v4 v13 v15 v15 v13 34 main bb3 2 tmp v11 tmp2 v12 .01 v17 .0 v18 tmp4 v16 v3 v11 v4 v12 v13 v15 v16 0 -1 v14 v17 v16 v18 v13 v3 v11 v11 v3 v4 v12 v12 v4 v13 v15 v15 v13 24 main bb 0 25 main bb 1 tmp v1 26 main bb 2 tmp v1 tmp2 v2 27 main bb3 2 tmp v1 tmp2 v2 .01 v3 .0 v4 v3 v1 v4 v2 28 main bb3 3 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 v3 v1 v4 v2 v5 0 -1 v4 29 main bb3 2 tmp v1 tmp2 v2 .01 v6 .0 v7 tmp4 v5 v3 v1 v4 v2 v5 0 -1 v4 v6 v5 v7 v3 32 33 v16 33
34 v17 v16 v18 v13
34 32 v11 v11 v12 v12 v13 v17 v14 v18 v15 v16 24 25 v1 25 26 v2 26
27 v3 v1 v4 v2
27 28 v5 28
29 v6 v5 v7 v3
29 32 v11 v1 v12 v2 v13 v6 v14 v7 v15 v5 34 33 32 25 26 27 29 28 24 1 33 34 pp1 v14 pp2 v13 pp3 v11 pp4 v12 pp5 v16 pp1 v18 pp2 v17 pp3 v11 pp4 v12 pp5 v16 v4 v12 v4 v12 v12 v4 v13 v15 v15 v13 v13 v15 v3 v11 v16 0 -1 v14 v3 v11 v11 v3 v17 v16 v4 v12 v4 v12 v12 v4 v13 v15 v15 v13 v13 v15 v3 v11 v18 v13 v16 0 -1 v14 v3 v11 v11 v3 2 32 33 pp1 v14 pp2 v13 pp3 v11 pp4 v12 pp5 v15 pp1 v14 pp2 v13 pp3 v11 pp4 v12 pp5 v16 v4 v12 v4 v12 v12 v4 v13 v15 v15 v13 v13 v15 v3 v11 v3 v11 v11 v3 v4 v12 v4 v12 v12 v4 v13 v15 v15 v13 v13 v15 v3 v11 v16 0 -1 v14 v3 v11 v11 v3 3 24 25 pp1 v1 4 26 27 pp1 v1 pp2 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 v3 v1 v4 v2 5 29 32 pp1 v7 pp2 v6 pp3 v1 pp4 v2 pp5 v5 pp1 v7 pp2 v6 pp3 v1 pp4 v2 pp5 v5 v3 v1 v5 0 -1 v4 v7 v3 v6 v5 v4 v2 v4 v2 v4 v2 v2 v4 v6 v5 v5 v6 v6 v5 v3 v1 v3 v1 v1 v3 6 34 32 pp1 v18 pp2 v17 pp3 v11 pp4 v12 pp5 v16 pp1 v18 pp2 v17 pp3 v11 pp4 v12 pp5 v16 v17 v16 v4 v12 v4 v12 v12 v4 v13 v15 v15 v13 v13 v15 v3 v11 v18 v13 v16 0 -1 v14 v3 v11 v11 v3 v4 v12 v4 v12 v12 v4 v17 v16 v16 v17 v17 v16 v3 v11 v3 v11 v11 v3 7 27 28 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 v3 v1 v4 v2 v3 v1 v5 0 -1 v4 v4 v2 8 25 26 pp1 v1 pp1 v1 pp2 v2 9 28 29 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp1 v7 pp2 v6 pp3 v1 pp4 v2 pp5 v5 v3 v1 v5 0 -1 v4 v4 v2 v3 v1 v5 0 -1 v4 v7 v3 v6 v5 v4 v2 32 pp1 v14 pp2 v13 pp3 v11 pp4 v12 pp5 v15 33 pp1 v14 pp2 v13 pp3 v11 pp4 v12 pp5 v16 34 pp1 v18 pp2 v17 pp3 v11 pp4 v12 pp5 v16 24 25 pp1 v1 26 pp1 v1 pp2 v2 27 pp1 v4 pp2 v3 pp3 v1 pp4 v2 28 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 29 pp1 v7 pp2 v6 pp3 v1 pp4 v2 pp5 v5 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