main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp1 = icmp sgt i32 %tmp, 0 br i1 %tmp1, label %bb2, label %bb8 bb2: br label %bb3 bb3: %.0 = phi i32 [%tmp, %bb2], [%tmp6, %bb5] %tmp4 = icmp ne i32 %.0, 0 br i1 %tmp4, label %bb5, label %bb7 bb5: %tmp6 = sub i32 %.0, 1 br label %bb3 bb7: br label %bb8 bb8: ret i32 0 } 2.1 36 64 main bb7 0 tmp v12 tmp1 v13 .0 v14 tmp4 v18 tmp6 v16 v13 1 v4 v12 v15 1 v14 v16 v14 0 v18 0 v4 0 v12 0 0 v4 v13 1 1 v13 v4 v12 v12 v4 v15 1 1 v15 v14 v16 v16 v14 65 main bb5 1 tmp v12 tmp1 v13 .0 v14 tmp4 v17 tmp6 v19 v13 1 v4 v12 v15 1 v14 v16 v17 1 v19 v14 -1 1 v4 0 v14 0 v12 0 0 v4 v13 1 1 v13 v4 v12 v12 v4 v15 1 1 v15 v14 v16 v16 v14 66 main bb8 0 tmp v12 tmp1 v13 .0 v14 tmp4 v18 tmp6 v16 v13 1 v4 v12 v15 1 v14 v16 v14 0 v18 0 v4 0 v12 0 0 v4 v13 1 1 v13 v4 v12 v12 v4 v15 1 1 v15 v14 v16 v16 v14 67 main bb3 1 tmp v12 tmp1 v13 .0 v20 tmp4 v17 tmp6 v19 v13 1 v4 v12 v15 1 v14 v16 v17 1 v19 v14 -1 1 v20 v19 v4 0 v14 0 v12 0 0 v4 v13 1 1 v13 v4 v12 v12 v4 v15 1 1 v15 v14 v16 v16 v14 36 main bb 0 37 main bb 1 tmp v1 38 main bb 1 tmp v1 v1 0 39 main bb 1 tmp v1 v1 0 40 main bb 2 tmp v1 tmp1 v2 v2 1 v1 0 41 main bb 2 tmp v1 tmp1 v3 v3 0 v1 0 42 main bb2 0 tmp v1 tmp1 v2 v2 1 v1 0 43 main bb8 0 tmp v1 tmp1 v3 v3 0 v1 0 44 main bb3 1 tmp v1 tmp1 v2 .0 v4 v2 1 v4 v1 v1 0 45 main bb3 2 tmp v1 tmp1 v2 .0 v4 tmp4 v5 v2 1 v4 v1 v5 1 v1 0 46 main bb5 0 tmp v1 tmp1 v2 .0 v4 tmp4 v5 v2 1 v4 v1 v5 1 v4 0 v1 0 47 main bb5 1 tmp v1 tmp1 v2 .0 v4 tmp4 v5 tmp6 v6 v2 1 v4 v1 v5 1 v6 v4 -1 1 v4 0 v1 0 48 main bb3 1 tmp v1 tmp1 v2 .0 v7 tmp4 v5 tmp6 v6 v2 1 v4 v1 v5 1 v6 v4 -1 1 v7 v6 v4 0 v1 0 58 main bb3 1 tmp v12 tmp1 v13 .0 v14 tmp4 v15 tmp6 v16 v13 1 v4 v12 v15 1 v14 v16 v4 0 v12 0 0 v4 v13 1 1 v13 v4 v12 v12 v4 v15 1 1 v15 v14 v16 v16 v14 59 main bb3 1 tmp v12 tmp1 v13 .0 v14 tmp4 v15 tmp6 v16 v13 1 v4 v12 v15 1 v14 v16 v4 0 v14 0 v12 0 0 v4 v13 1 1 v13 v4 v12 v12 v4 v15 1 1 v15 v14 v16 v16 v14 60 main bb3 1 tmp v12 tmp1 v13 .0 v14 tmp4 v15 tmp6 v16 v13 1 v4 v12 v15 1 v14 v16 v14 0 v4 0 v12 0 0 v4 v13 1 1 v13 v4 v12 v12 v4 v15 1 1 v15 v14 v16 v16 v14 61 main bb3 2 tmp v12 tmp1 v13 .0 v14 tmp4 v17 tmp6 v16 v13 1 v4 v12 v15 1 v14 v16 v17 1 v4 0 v14 0 v12 0 0 v4 v13 1 1 v13 v4 v12 v12 v4 v15 1 1 v15 v14 v16 v16 v14 62 main bb3 2 tmp v12 tmp1 v13 .0 v14 tmp4 v18 tmp6 v16 v13 1 v4 v12 v15 1 v14 v16 v14 0 v18 0 v4 0 v12 0 0 v4 v13 1 1 v13 v4 v12 v12 v4 v15 1 1 v15 v14 v16 v16 v14 63 main bb5 0 tmp v12 tmp1 v13 .0 v14 tmp4 v17 tmp6 v16 v13 1 v4 v12 v15 1 v14 v16 v17 1 v4 0 v14 0 v12 0 0 v4 v13 1 1 v13 v4 v12 v12 v4 v15 1 1 v15 v14 v16 v16 v14 64
66
65
67 v20 v19
66 67 58 v12 v12 v13 v13 v14 v20 v15 v17 v16 v19 36 37 v1 37 38 39 v1 0 38 40 v2 39 41 v3 40 42 41 43 42
44 v4 v1
43 44 45 v5 45 46 46 47 v6 47
48 v7 v6
48 58 v12 v1 v13 v2 v14 v7 v15 v5 v16 v6 58 59 60 v14 0 59 61 v17 60 62 v18 61 63 62 64 63 65 v19 36 40 60 61 47 64 67 48 46 39 37 63 65 44 58 42 59 41 62 38 45 1 64 66 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 v18 0 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 v18 0 0 v12 v14 v16 0 v4 0 v4 2 65 67 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v19 pp1 v20 pp2 v12 pp3 v13 pp4 v17 pp5 v19 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v19 v14 -1 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v19 v14 -1 1 v15 1 1 v15 v17 1 v20 v19 0 v12 v14 v16 0 v4 0 v4 3 67 58 pp1 v20 pp2 v12 pp3 v13 pp4 v17 pp5 v19 pp1 v20 pp2 v12 pp3 v13 pp4 v17 pp5 v19 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v19 v14 -1 1 v15 1 1 v15 v17 1 v20 v19 0 v12 v14 v16 0 v4 0 v4 v20 v19 v19 v20 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 v17 1 v17 1 1 v17 0 v12 v20 v19 0 v4 0 v4 4 37 39 pp1 v1 pp1 v1 v1 0 5 41 43 pp1 v1 pp2 v3 pp1 v1 pp2 v3 v3 0 v1 0 v3 0 v1 0 6 47 48 pp1 v4 pp2 v1 pp3 v2 pp4 v5 pp5 v6 pp1 v7 pp2 v1 pp3 v2 pp4 v5 pp5 v6 v5 1 v2 1 v6 v4 -1 1 v4 v1 0 v4 0 v1 v5 1 v7 v6 v2 1 v6 v4 -1 1 v4 v1 0 v4 0 v1 7 42 44 pp1 v1 pp2 v2 pp1 v4 pp2 v1 pp3 v2 v2 1 0 v1 v2 1 v4 v1 0 v1 8 58 60 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 9 63 65 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v19 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v19 v14 -1 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 10 38 40 pp1 v1 pp1 v1 pp2 v2 0 v1 v2 1 0 v1 11 58 59 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 12 36 37 pp1 v1 13 40 42 pp1 v1 pp2 v2 pp1 v1 pp2 v2 v2 1 0 v1 v2 1 0 v1 14 45 46 pp1 v4 pp2 v1 pp3 v2 pp4 v5 pp1 v4 pp2 v1 pp3 v2 pp4 v5 v5 1 v2 1 v4 v1 0 v4 0 v1 v5 1 v2 1 v4 v1 0 v4 0 v1 15 37 38 pp1 v1 pp1 v1 0 v1 16 44 45 pp1 v4 pp2 v1 pp3 v2 pp1 v4 pp2 v1 pp3 v2 pp4 v5 v2 1 v4 v1 0 v1 v5 1 v2 1 v4 v1 0 v4 0 v1 17 46 47 pp1 v4 pp2 v1 pp3 v2 pp4 v5 pp1 v4 pp2 v1 pp3 v2 pp4 v5 pp5 v6 v5 1 v2 1 v4 v1 0 v4 0 v1 v5 1 v2 1 v6 v4 -1 1 v4 v1 0 v4 0 v1 18 39 41 pp1 v1 pp1 v1 pp2 v3 v1 0 v3 0 v1 0 19 59 61 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 20 62 64 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 v18 0 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 v18 0 0 v12 v14 v16 0 v4 0 v4 21 48 58 pp1 v7 pp2 v1 pp3 v2 pp4 v5 pp5 v6 pp1 v7 pp2 v1 pp3 v2 pp4 v5 pp5 v6 v5 1 v7 v6 v2 1 v6 v4 -1 1 v4 v1 0 v4 0 v1 v7 v6 v6 v7 v2 1 1 v2 v2 1 v4 v1 v1 v4 v4 v1 v5 1 v5 1 1 v5 0 v1 v7 v6 0 v4 0 v4 22 61 63 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 23 60 62 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 v18 0 0 v12 v14 v16 0 v4 0 v4 64 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 65 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v19 66 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 67 pp1 v20 pp2 v12 pp3 v13 pp4 v17 pp5 v19 36 37 pp1 v1 38 pp1 v1 39 pp1 v1 40 pp1 v1 pp2 v2 41 pp1 v1 pp2 v3 42 pp1 v1 pp2 v2 43 pp1 v1 pp2 v3 44 pp1 v4 pp2 v1 pp3 v2 45 pp1 v4 pp2 v1 pp3 v2 pp4 v5 46 pp1 v4 pp2 v1 pp3 v2 pp4 v5 47 pp1 v4 pp2 v1 pp3 v2 pp4 v5 pp5 v6 48 pp1 v7 pp2 v1 pp3 v2 pp4 v5 pp5 v6 58 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 59 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 60 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 61 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v16 62 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 63 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v16 36 40 60 61 47 64 67 48 46 39 37 63 65 44 58 42 59 41 62 38 45 1 64 66 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 v18 0 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 v18 0 0 v12 v14 v16 0 v4 0 v4 2 65 67 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v19 pp1 v20 pp2 v12 pp3 v13 pp4 v17 pp5 v19 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v19 v14 -1 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v19 v14 -1 1 v15 1 1 v15 v17 1 v20 v19 0 v12 v14 v16 0 v4 0 v4 3 67 58 pp1 v20 pp2 v12 pp3 v13 pp4 v17 pp5 v19 pp1 v20 pp2 v12 pp3 v13 pp4 v17 pp5 v19 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v19 v14 -1 1 v15 1 1 v15 v17 1 v20 v19 0 v12 v14 v16 0 v4 0 v4 v20 v19 v19 v20 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 v17 1 v17 1 1 v17 0 v12 v20 v19 0 v4 0 v4 4 37 39 pp1 v1 pp1 v1 v1 0 5 41 43 pp1 v1 pp2 v3 pp1 v1 pp2 v3 v3 0 v1 0 v3 0 v1 0 6 47 48 pp1 v4 pp2 v1 pp3 v2 pp4 v5 pp5 v6 pp1 v7 pp2 v1 pp3 v2 pp4 v5 pp5 v6 v5 1 v2 1 v6 v4 -1 1 v4 v1 0 v4 0 v1 v5 1 v7 v6 v2 1 v6 v4 -1 1 v4 v1 0 v4 0 v1 7 42 44 pp1 v1 pp2 v2 pp1 v4 pp2 v1 pp3 v2 v2 1 0 v1 v2 1 v4 v1 0 v1 8 58 60 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 9 63 65 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v19 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v19 v14 -1 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 10 38 40 pp1 v1 pp1 v1 pp2 v2 0 v1 v2 1 0 v1 11 58 59 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 12 36 37 pp1 v1 13 40 42 pp1 v1 pp2 v2 pp1 v1 pp2 v2 v2 1 0 v1 v2 1 0 v1 14 45 46 pp1 v4 pp2 v1 pp3 v2 pp4 v5 pp1 v4 pp2 v1 pp3 v2 pp4 v5 v5 1 v2 1 v4 v1 0 v4 0 v1 v5 1 v2 1 v4 v1 0 v4 0 v1 15 37 38 pp1 v1 pp1 v1 0 v1 16 44 45 pp1 v4 pp2 v1 pp3 v2 pp1 v4 pp2 v1 pp3 v2 pp4 v5 v2 1 v4 v1 0 v1 v5 1 v2 1 v4 v1 0 v4 0 v1 17 46 47 pp1 v4 pp2 v1 pp3 v2 pp4 v5 pp1 v4 pp2 v1 pp3 v2 pp4 v5 pp5 v6 v5 1 v2 1 v4 v1 0 v4 0 v1 v5 1 v2 1 v6 v4 -1 1 v4 v1 0 v4 0 v1 18 39 41 pp1 v1 pp1 v1 pp2 v3 v1 0 v3 0 v1 0 19 59 61 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 20 62 64 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 v18 0 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 v18 0 0 v12 v14 v16 0 v4 0 v4 21 48 58 pp1 v7 pp2 v1 pp3 v2 pp4 v5 pp5 v6 pp1 v7 pp2 v1 pp3 v2 pp4 v5 pp5 v6 v5 1 v7 v6 v2 1 v6 v4 -1 1 v4 v1 0 v4 0 v1 v7 v6 v6 v7 v2 1 1 v2 v2 1 v4 v1 v1 v4 v4 v1 v5 1 v5 1 1 v5 0 v1 v7 v6 0 v4 0 v4 22 61 63 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v17 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v4 v12 v12 v4 v4 v12 0 v14 v15 1 v15 1 1 v15 v17 1 0 v12 v14 v16 0 v4 0 v4 23 60 62 pp1 v14 pp2 v12 pp3 v13 pp4 v15 pp5 v16 pp1 v14 pp2 v12 pp3 v13 pp4 v18 pp5 v16 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 0 v12 v14 v16 0 v4 0 v4 v14 v16 v16 v14 v13 1 1 v13 v13 1 v14 0 v4 v12 v12 v4 v4 v12 v15 1 v15 1 1 v15 v18 0 0 v12 v14 v16 0 v4 0 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