| Example | AProVE |
|---|
| c/signed/juggernaut/loop4.c | 7996 + 288372 * |a| + 450 * (|a| * |b|) + 450 * (|a| * |a|) + 153 * |b| | 296.801 |
| c/signed/juggernaut/loop7.c | 122 + 11 * |b_smax_32| + 11 * |y| | 296.739 |
| c/signed/juggernaut/loop9.c | 143 + 144 * |b_smax_32| + 96 * |x| | 43.507 |
| c/signed/juggernaut/svcomp1.c | 161 + 10 * |x| + 11 * |y| | 27.953 |
| c/signed/juggernaut/svcomp2.c | 4414 + 1781 * |a| | 297.149 |
| c/signed/juggernaut/svcomp3.c | Ο(ω) | -- |
| c/signed/juggernaut/svcomp6.c | max(max(19 + nat(8 * (-1 / 2) + 8 * ((3 / 2) * nat(n))) * nat(-2 + n) + nat(8 + 8 * (n / 2)) + nat(-14 + -14 * i), 1 + nat(8 * n) * nat(-2 + n)) + max(19 + 22 * n, 63), 12 + -14 * i + 14 * n, 34 + -14 * i, 34 + nat(8 * n) * nat(-2 + -1 * i + n) + nat(8 + 8 * i) + nat(-44 + -22 * i + 22 * n) + max(22 + 8 * i, 22), 48) | 47.508 |
| c/signed/juggernaut/svcomp7.c | 41 + 11 * |x| | 11.614 |
| c/signed/juggernaut/svcomp8.c | 177 + 84 * |b_smax_32| | 296.900 |
| c/signed/juggernaut/svcomp9.c | 178 + 273 * |b_smax_32| + 45 * (|b_smax_32| * |b_smax_32|) | 296.881 |
| c/signed/juggernaut/svcomp10.c | 345 + 238 * |b_smax_32| + 40 * (|y| * |b_smax_32|) + 86 * |y| | 297.007 |
| c/signed/juggernaut/svcomp11.c | Ο(ω) | -- |
| c/signed/juggernaut/svcomp12.c | max(49, 54 + -9 * x + -18 * y, 58 + -9 * x + 18 * y, max(42 + -9 * y, 60) + max(nat(-30 + -15 * y) + max(22 + -9 * x + 18 * y, 13), 22 + -9 * x + 18 * y, 13, max(9, 18 + 9 * x + 18 * y) + nat(-24 + -24 * y)), 50 + 9 * x + -18 * y, 54 + 9 * x + 18 * y, max(35 + 9 * x + -18 * y, 39 + -9 * x + -18 * y, 26, 30) + max(-9 + 24 * y, 39)) | 190.203 |
| c/signed/juggernaut/svcomp13.c | Ο(ω) | 7.297 |
| c/signed/juggernaut/svcomp15.c | Ο(ω) | 58.191 |
| c/signed/juggernaut/svcomp16.c | max(51, 7 + 11 * x, max(-4 + 11 * x, 29) + max(nat(-33 + 11 * x) + max(-55 + 22 * x, -77 + 22 * x, 22, 11), -77 + 22 * x, 22, 11), 40 + 22 * x + -22 * (8 / 3), 40 + 22 * x + -22 * (11 / 3), -125 + 44 * x) | 25.913 |
| c/signed/juggernaut/svcomp18.c | Ο(ω) | -- |
| c/signed/juggernaut/svcomp19.c | Ο(ω) | 2.937 |
| c/signed/juggernaut/svcomp20.c | Ο(ω) | 3.704 |
| c/signed/juggernaut/svcomp21.c | Ο(ω) | 2.844 |
| c/signed/juggernaut/svcomp22.c | max(43, 43 + 18 * m + 18 * n + 18 * r) | 90.301 |
| c/signed/juggernaut/svcomp23.c | max(49, 11 + 30 * y, 11 + 15 * x + 15 * y, 4 + 15 * x + 15 * y, 4 + 30 * y) | 27.655 |
| c/signed/juggernaut/svcomp29.c | Ο(ω) | -- |
| c/signed/juggernaut/svcomp32.c | max(34 + 9 * length, 61) | 26.815 |
| c/signed/juggernaut/svcomp34.c | Ο(ω) | -- |
| c/signed/juggernaut/svcomp36.c | max(92, 20 + 18 * length, 30 + 18 * length) | 198.207 |
| c/signed/juggernaut/svcomp38.c | 480 + 96 * |y| + 32 * |z| | 36.769 |
| c/signed/juggernaut/svcomp39.c | 102462 + 512 * |y| + 512 * |z| | 64.907 |
| c/signed/juggernaut/svcomp40.c | max(7032, 196823 + -18981 * x1) | 22.464 |
| c/signed/juggernaut/svcomp41.c | max(102, 1793 + -171 * x1) | 10.320 |
| c/signed/juggernaut/svcomp42.c | Ο(ω) | -- |
| c/signed/wdk-signed-overflow/allocsup.c | max(16 + 18 * Fcb_Mcb_CurrentEntryCount, 52) | 59.601 |
| c/signed/wdk-signed-overflow/detect.c | Ο(ω) | 2.777 |
| c/signed/wdk-signed-overflow/testapp.c | Ο(ω) | 107.263 |