LoAT | |||||||||
---|---|---|---|---|---|---|---|---|---|
Best UB | Ω(1) | Ω(n) | Ω(n2) | Ω(n3) | Ω(n4) | EXP | INF | no result | |
O(1) | 132 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | |
O(n) | 45 | 125 | 0 | 0 | 0 | 0 | 0 | 0 | |
O(n2) | 9 | 18 | 33 | 0 | 0 | 0 | 0 | 0 | |
O(n3) | 2 | 0 | 0 | 3 | 0 | 0 | 0 | 0 | |
O(n4) | 1 | 0 | 0 | 0 | 2 | 0 | 0 | 0 | |
EXP | 0 | 0 | 0 | 0 | 0 | 5 | 0 | 0 | |
INF | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | |
no result | 50 | 31 | 3 | 0 | 0 | 0 | 173 | 7 |
O(1) | O(n) | O(n2) | O(n3) | O(n4) | O(n6) | O(n8) | EXP | INF | no result | any result | Avg. time | Avg. time (incl. no res.) | |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
LoAT | 239 | 174 | 36 | 3 | 2 | 0 | 0 | 5 | 173 | 7 | 632 | 1761ms | 2399ms |
Best UB | 132 | 170 | 60 | 5 | 3 | 0 | 0 | 5 | 0 | 264 | 375 | - | - |
KoAT | 125 | 154 | 67 | 4 | 2 | 1 | 1 | 5 | 0 | 280 | 359 | 1002ms | 5513ms |
CoFloCo | 118 | 141 | 51 | 2 | 2 | 0 | 0 | 0 | 0 | 325 | 314 | 805ms | 8646ms |
Loopus | 77 | 103 | 45 | 6 | 5 | 0 | 0 | 0 | 0 | 403 | 236 | 115ms | 922ms |
Rank | 90 | 18 | 8 | 1 | 0 | 0 | 0 | 0 | 0 | 522 | 117 | 485ms | 1557ms |
Example | LoAT | KoAT | CoFloCo | Loopus | Rank |
---|---|---|---|---|---|
FGPSF09/Beerendonk/01 | 1 - B + A 83ms, Ω(n), #vars: 2, input, output | A + B + 1 57ms, O(n), #vars: 2, input, output | max(A + -1 * B + 1, 1) 236ms, O(n), #vars: 2, input, output | max(0, A - B) 55ms, O(n), #vars: 2, input, output | 97ms, input, aspic, output, errors |
FGPSF09/Beerendonk/02 | 1 + meter 63ms, Ω(n), #vars: 1, input, output | A + B + 1 75ms, O(n), #vars: 2, input, output | max(1 / 2 * A + -1 / 2... 224ms, O(n), #vars: 2, input, output | max(0, A - B) 55ms, O(n), #vars: 2, input, output | 89ms, input, aspic, output, errors |
FGPSF09/Beerendonk/03 | 1 81ms, Ω(1), #vars: 0, input, output | A + B + 1 106ms, O(n), #vars: 2, input, output | max(A + -1 * B + 1, 1) 220ms, O(n), #vars: 2, input, output | max(0, A - B) 51ms, O(n), #vars: 2, input, output | 83ms, input, aspic |
FGPSF09/Beerendonk/04 | 1 61ms, Ω(1), #vars: 0, input, output | 2 23ms, O(1), #vars: 0, input, output | 2 224ms, O(1), #vars: 0, input, output | max(0, A - B) 57ms, O(n), #vars: 2, input, output | 97ms, input, aspic, output, errors |
FGPSF09/Beerendonk/05 | 1 197ms, Ω(1), #vars: 0, input, output | 2 24ms, O(1), #vars: 0, input, output | max(A + 1, 1) 182ms, O(n), #vars: 1, input, output | 1 59ms, O(1), #vars: 0, input, output | 4 87ms, O(1), #vars: 0, input, aspic, output |
FGPSF09/Beerendonk/06 | 1 80ms, Ω(1), #vars: 0, input, output | 2 25ms, O(1), #vars: 0, input, output | max(A + 1, 1) 240ms, O(n), #vars: 1, input, output | 1 46ms, O(1), #vars: 0, input, output | 4 102ms, O(1), #vars: 0, input, aspic, output |
FGPSF09/Beerendonk/07 | 1 81ms, Ω(1), #vars: 0, input, output | 2 22ms, O(1), #vars: 0, input, output | max(1 / 3 * A + 1, 1) 205ms, O(n), #vars: 1, input, output | 1 46ms, O(1), #vars: 0, input, output | 6 84ms, O(1), #vars: 0, input, aspic, output |
FGPSF09/Beerendonk/08 | 1 + B 261ms, Ω(n), #vars: 1, input, output | B + 1 117ms, O(n), #vars: 1, input, output | max(1, max(0, min(B, A... 235ms, O(n), #vars: 2, input, output | max(B, 0) 61ms, O(n), #vars: 1, input, output | 85ms, input, aspic, output, errors |
FGPSF09/Beerendonk/09 | 1 - B + C 310ms, Ω(n), #vars: 2, input, output | A + B + 1 81ms, O(n), #vars: 2, input, output | max(1, max(0, min(A + ... 217ms, O(n), #vars: 3, input, output | max(0, C - B) 55ms, O(n), #vars: 2, input, output | 84ms, input, aspic, output, errors |
FGPSF09/Beerendonk/10 | 1 1903ms, Ω(1), #vars: 0, input, output | 2 * A + 2 111ms, O(n), #vars: 1, input, output | max(A + 1, 2) 264ms, O(n), #vars: 1, input, output | 777ms, input, output | 143ms, input, aspic, output, errors |
FGPSF09/Beerendonk/11 | 1 + B 376ms, Ω(n), #vars: 1, input, output | B + 4 149ms, O(n), #vars: 1, input, output | max(B + 1, 3, A + 2) 465ms, O(n), #vars: 2, input, output | max(0, B + max(0, min(... 88ms, O(n), #vars: 1, input, output | 110ms, input, aspic, output, errors |
FGPSF09/Beerendonk/13 | 1 + A 156ms, Ω(n), #vars: 1, input, output | A + 2 101ms, O(n), #vars: 1, input, output | max(B + 2, 2, A + 1) 254ms, O(n), #vars: 2, input, output | max(0, A + max(0, min(... 72ms, O(n), #vars: 1, input, output | 99ms, input, aspic, output, errors |
FGPSF09/Beerendonk/15 | 1 267ms, Ω(1), #vars: 0, input, output | 2 * A + 2 * B + 1 160ms, O(n), #vars: 2, input, output | max(A + B + 1, 1, max(... 315ms, O(n), #vars: 2, input, output | 1 + max(A, 0) + max(0,... 109ms, O(n), #vars: 2, input, output | 76ms, input, aspic, aspic (errors) |
FGPSF09/Beerendonk/16 | 1 418ms, Ω(1), #vars: 0, input, output | 2 * A + 2 * B + 2 * C + 1 172ms, O(n), #vars: 3, input, output | max(A + B + -1 * C + 1... 326ms, O(n), #vars: 3, input, output | 1 + max(A, 0) + max(0,... 62ms, O(n), #vars: 3, input, output | 76ms, input, aspic, aspic (errors) |
FGPSF09/Beerendonk/17 | 1 323ms, Ω(1), #vars: 0, input, output | 3 * A + 3 * B + 1 231ms, O(n), #vars: 2, input, output | max(A + B + 1, 1, max(... 411ms, O(n), #vars: 2, input, output | max(0, A + B) + max(0,... 119ms, O(n2), #vars: 1, input, output | 78ms, input, aspic, output, errors |
FGPSF09/Beerendonk/18 | 1 + A 456ms, Ω(n), #vars: 1, input, output | 2 * A + B + 2 309ms, O(n), #vars: 2, input, output | max(A + B + 1, A + 1, ... 308ms, O(n), #vars: 2, input, output | 1 + max(B, 0) + max(A,... 91ms, O(n), #vars: 1, input, output | 91ms, input, aspic, aspic (errors) |
FGPSF09/Beerendonk/19 | 1 - B + A 500ms, Ω(n), #vars: 2, input, output | 2 * A + 3 * B + C + 2 256ms, O(n), #vars: 3, input, output | max(A + -2 * B + C + 1... 359ms, O(n), #vars: 3, input, output | 1 + max(0, A - B) + ma... 97ms, O(n), #vars: 2, input, output | 71ms, input, aspic, aspic (errors) |
FGPSF09/Beerendonk/20 | 3 + A 110ms, Ω(n), #vars: 1, input, output | A + 3 114ms, O(n), #vars: 1, input, output | max(A + 3, 1) 247ms, O(n), #vars: 1, input, output | max(A, 0) + max(A, 0) ... 65ms, O(n), #vars: 1, input, output | 97ms, input, aspic, output, errors |
FGPSF09/Beerendonk/21 | 3 - B + A 134ms, Ω(n), #vars: 2, input, output | A + B + 3 98ms, O(n), #vars: 2, input, output | max(-1 * B + C + 3, 1) 284ms, O(n), #vars: 2, input, output | max(0, A - B) + max(0,... 65ms, O(n), #vars: 2, input, output | 85ms, input, aspic, output, errors |
FGPSF09/Beerendonk/22 | 3 + B 138ms, Ω(n), #vars: 1, input, output | 4 * A + B + 1 163ms, O(n), #vars: 2, input, output | max(2 * A + B + 1, 2 *... 301ms, O(n), #vars: 2, input, output | max(A, 0) + max(B, 0) ... 71ms, O(n), #vars: 1, input, output | 92ms, input, aspic, output, errors |
FGPSF09/Beerendonk/23 | 3 - B + C 211ms, Ω(n), #vars: 2, input, output | 4 * A + 5 * B + C + 1 578ms, O(n), #vars: 3, input, output | max(2 * A + -3 * B + C... 491ms, O(n), #vars: 3, input, output | max(0, A - B) + max(0,... 71ms, O(n), #vars: 2, input, output | 106ms, input, aspic, output, errors |
FGPSF09/Beerendonk/24 | 3 + A 284ms, Ω(n), #vars: 1, input, output | 2 * A + 2 * B + 7 189ms, O(n), #vars: 2, input, output | max(B + 3, 1, A + 3) 261ms, O(n), #vars: 2, input, output | max(A, 0) + max(A, 0) ... 86ms, O(n), #vars: 1, input, output | 92ms, input, aspic, output, errors |
FGPSF09/CAV02/practical1 | 1 + 1 / 2 * A^2 + 5 / ... 101ms, Ω(n2), #vars: 1, input, output | 16 * A + 4 * A^2 + 13 383ms, O(n2), #vars: 1, input, output | max(3, (A + 2) * A + 1... 324ms, O(n2), #vars: 1, input, output | max(0, A + 1) + max(0,... 63ms, O(n2), #vars: 1, input, output | 97ms, input, aspic, output, errors |
FGPSF09/CAV02/practical2 | 2 + meter 97ms, Ω(n), #vars: 1, input, output | 49927 * B + 5038821 1062ms, O(n), #vars: 1, input, output | max(56 / 11, -1 / 11 *... 829ms, O(n), #vars: 1, input, output | max(0, 9 * max(0, 101 ... 129ms, O(n), #vars: 1, input, output | 144ms, input, aspic, output |
FGPSF09/CAV05/c.05 | 1 462ms, Ω(1), #vars: 0, input, output | 2 * A + 2 * B + 3 187ms, O(n), #vars: 2, input, output | max(A + B + -1, 1) 224ms, O(n), #vars: 2, input, output | max(A, 0) + max(A, 0) ... 125ms, O(n), #vars: 1, input, output | 92ms, input, aspic |
FGPSF09/ESOP08/abstractions | 1 + B 131ms, Ω(n), #vars: 1, input, output | 2394ms, input, output | 257ms, input, output | 72ms, input, output | 89ms, input, aspic, output, errors |
FGPSF09/LICS04/c.01 | 4 305ms, Ω(1), #vars: 0, input, output | 10 * A + 2 * A^2 + 9 192ms, O(n2), #vars: 1, input, output | max(2 * A + 3, 4, A + ... 459ms, O(n2), #vars: 1, input, output | max(0, A + 1) + max(0,... 86ms, O(n2), #vars: 1, input, output | 94ms, input, aspic |
FGPSF09/LICS04/choice | 1 + A 146ms, Ω(n), #vars: 1, input, output | 3519ms, input, output | 276ms, input, output | max(B, A, 0) 81ms, O(n), #vars: 2, input, output | 99ms, input, aspic, output, errors |
FGPSF09/PLDI06/c.03 | 2 + B - C 212ms, Ω(n), #vars: 2, input, output | 5 * A + 2 * B + 3 * C + 4 121ms, O(n), #vars: 3, input, output | max(1, A + -1 * B + ma... 313ms, O(n), #vars: 2, input, output | max(0, max(0, B + 1 + ... 113ms, O(n2), #vars: 2, input, output | 100ms, input, aspic, output, errors |
FGPSF09/PLDI06/c.04 | 1 200ms, Ω(1), #vars: 0, input, output | A + B + 2 137ms, O(n), #vars: 2, input, output | max(A + -1 * B + 1, 2) 341ms, O(n), #vars: 2, input, output | max(0, A - B) + max(0,... 85ms, O(n), #vars: 2, input, output | 84ms, input, aspic |
FGPSF09/SAS05/c.02 | 9 / 2 - 1 / 2 * (1 + A... 173ms, Ω(n2), #vars: 1, input, output | 149 * A + 6 * A^2 + 336 152ms, O(n2), #vars: 1, input, output | max(A + 3, 2, max(A + ... 365ms, O(n2), #vars: 1, input, output | max(0, A + 1) + max(0,... 80ms, O(n2), #vars: 1, input, output | 90ms, input, aspic, output, errors |
FGPSF09/TACAS01/terminate | 1 84ms, Ω(1), #vars: 0, input, output | A + B + C + 102 99ms, O(n), #vars: 3, input, output | max(-1 / 2 * A + 1 / 2... 262ms, O(n), #vars: 3, input, output | max(0, B + 1 + 0 - C) 62ms, O(n), #vars: 2, input, output | 73ms, input, aspic, output, errors |
FGPSF09/VMCAI04/complete1 | 1 - B + A 153ms, Ω(n), #vars: 2, input, output | A + B + 1 104ms, O(n), #vars: 2, input, output | max(A + -1 * B + 1, 1) 301ms, O(n), #vars: 2, input, output | max(0, A - B) 208ms, O(n), #vars: 2, input, output | 158ms, input, aspic |
FGPSF09/VMCAI04/complete2 | 1 96ms, Ω(1), #vars: 0, input, output | 5 261ms, O(1), #vars: 0, input, output | 237ms, input, output | 1 63ms, O(1), #vars: 0, input, output | 143ms, input, aspic, output, errors |
FGPSF09/VMCAI04/complete3 | 1 + 1 / 2 * A^2 + 5 / ... 97ms, Ω(n2), #vars: 1, input, output | 16 * A + 4 * A^2 + 13 384ms, O(n2), #vars: 1, input, output | max(3, (A + 2) * A + 1... 333ms, O(n2), #vars: 1, input, output | max(0, A + 1) + max(0,... 68ms, O(n2), #vars: 1, input, output | 88ms, input, aspic, output, errors |
FGPSF09/VMCAI04/complete4 | 3 + (1 + A) * free + 2... 151ms, INF, #vars: 2, input, output | 2373ms, input, output | 257ms, input, output | 66ms, input, output | 108ms, input, aspic, output, errors |
FGPSF09/VMCAI05/poly1 nonlinear | 1 75ms, Ω(1), #vars: 0, input, output | 5610ms, input, output | 306ms, input, output | 56ms, input, output | Non-linear example not handled by prover. |
FGPSF09/VMCAI05/poly2 | 1 77ms, Ω(1), #vars: 0, input, output | 6182ms, input, output | 273ms, input, output | 56ms, input, output | 93ms, input, aspic |
FGPSF09/VMCAI05/poly3 nonlinear | 2 + A 125ms, Ω(n), #vars: 1, input, output | 5749ms, input, output | 216ms, input, output | 102ms, input, output | Non-linear example not handled by prover. |
FGPSF09/VMCAI05/poly4 | 1 - B + A 574ms, Ω(n), #vars: 2, input, output | 2 * A + 2 * B + 2 * C ... 299ms, O(n), #vars: 4, input, output | max(A + -1 * B + C + -... 683ms, O(n), #vars: 4, input, output | max(0, C - D) + max(0,... 73ms, O(n), #vars: 2, input, output | 100ms, input, aspic, output, errors |
FGPSF09/new/unsatCond2 nonlinear | 1 65ms, Ω(1), #vars: 0, input, output | 100ms, input, output | 232ms, input, output | 44ms, input, output | Non-linear example not handled by prover. |
FGPSF09/patrs/div | 1 83ms, Ω(1), #vars: 0, input, output | A + B + 3 97ms, O(n), #vars: 2, input, output | 2 211ms, O(1), #vars: 0, input, output | max(0, B - A) 82ms, O(n), #vars: 2, input, output | 75ms, input, aspic |
FGPSF09/patrs/increase1 | 1 - B + A 86ms, Ω(n), #vars: 2, input, output | A + B + 1 59ms, O(n), #vars: 2, input, output | max(A + -1 * B + 1, 1) 209ms, O(n), #vars: 2, input, output | max(0, A - B) 53ms, O(n), #vars: 2, input, output | 81ms, input, aspic, output, errors |
FGPSF09/patrs/increase2 | 1 - B - C + A 115ms, Ω(n), #vars: 3, input, output | 2 * A + 2 * B + 2 * C + 1 107ms, O(n), #vars: 3, input, output | max(A + -1 * B + -1 * ... 283ms, O(n), #vars: 3, input, output | max(0, max(0, A - C - ... 84ms, O(n2), #vars: 3, input, output | 79ms, input, aspic, output, errors |
FGPSF09/patrs/increase3 | 1 - B + A 235ms, Ω(n), #vars: 2, input, output | 4 * A + 2 * B + 2 * C + 3 106ms, O(n), #vars: 3, input, output | max(2 * A + -1 * B + -... 257ms, O(n), #vars: 3, input, output | max(0, A - C) + max(0,... 86ms, O(n), #vars: 2, input, output | 85ms, input, aspic, output, errors |
FGPSF09/patrs/increase4 | 1 - B + A 84ms, Ω(n), #vars: 2, input, output | A + B + 1 69ms, O(n), #vars: 2, input, output | max(A + -1 * B + 1, 1) 252ms, O(n), #vars: 2, input, output | max(0, A - B) 49ms, O(n), #vars: 2, input, output | 88ms, input, aspic, output, errors |
FGPSF09/patrs/pasta/a.01 | 1 + 1 / 2 * A^2 + 5 / ... 193ms, Ω(n2), #vars: 1, input, output | 4 * A + 2 * A^2 + 1 169ms, O(n2), #vars: 1, input, output | max(A + 2, 2, max(A, (... 376ms, O(n2), #vars: 1, input, output | max(A, 0) + max(0, max... 78ms, O(n2), #vars: 1, input, output | 91ms, input, aspic, output, errors |
FGPSF09/patrs/pasta/a.02 | 1 1563ms, Ω(1), #vars: 0, input, output | 3067ms, input, output | 319ms, input, output | 113ms, input, output | 107ms, input, aspic, output, errors |
FGPSF09/patrs/pasta/a.03 | -7 + 4 * A 1797ms, Ω(n), #vars: 1, input, output | 174 * A + 162 * B + 36... 664ms, O(n2), #vars: 2, input, output | max(-2 * A + B + 5, 17... 5224ms, O(n2), #vars: 2, input, output | 141ms, input, output | 82ms, input, aspic |
FGPSF09/patrs/pasta/a.04 | 1 - B + A 86ms, Ω(n), #vars: 2, input, output | A + B + 1 57ms, O(n), #vars: 2, input, output | max(A + -1 * B + 1, 1) 248ms, O(n), #vars: 2, input, output | max(0, A - B) 48ms, O(n), #vars: 2, input, output | 72ms, input, aspic, output, errors |
FGPSF09/patrs/pasta/a.05 | 1 - B + A 88ms, Ω(n), #vars: 2, input, output | A + B + 1 56ms, O(n), #vars: 2, input, output | max(A + -1 * B + 1, 1) 253ms, O(n), #vars: 2, input, output | max(0, A - B) 56ms, O(n), #vars: 2, input, output | 77ms, input, aspic, output, errors |
FGPSF09/patrs/pasta/a.06 | 1 + meter 66ms, Ω(n), #vars: 1, input, output | A + B + C + 1 81ms, O(n), #vars: 3, input, output | max(1 / 2 * A + -1 / 2... 264ms, O(n), #vars: 3, input, output | max(0, A - C - B) 53ms, O(n), #vars: 3, input, output | 93ms, input, aspic, output, errors |
FGPSF09/patrs/pasta/a.07 | 1 - B + A 301ms, Ω(n), #vars: 2, input, output | A + B + 1 83ms, O(n), #vars: 2, input, output | max(1, max(0, min(A + ... 321ms, O(n), #vars: 3, input, output | max(0, A - C) 57ms, O(n), #vars: 2, input, output | 75ms, input, aspic, output, errors |
FGPSF09/patrs/pasta/a.08 | 1 - B + A 93ms, Ω(n), #vars: 2, input, output | A + B + 1 74ms, O(n), #vars: 2, input, output | max(A + -1 * B + 1, 1) 215ms, O(n), #vars: 2, input, output | max(0, A - B) 52ms, O(n), #vars: 2, input, output | 83ms, input, aspic, output, errors |
FGPSF09/patrs/pasta/a.09 | 1 85ms, Ω(1), #vars: 0, input, output | A + B + 2 117ms, O(n), #vars: 2, input, output | max(A + -1 * B + 2, 1) 267ms, O(n), #vars: 2, input, output | max(0, A + 1 + 0 - B) 53ms, O(n), #vars: 2, input, output | 84ms, input, aspic |
FGPSF09/patrs/pasta/a.10 | 1 - B + A 195ms, Ω(n), #vars: 2, input, output | 2 * A + 2 * B + 2 162ms, O(n), #vars: 2, input, output | max(A + -1 * B + 1, 1,... 274ms, O(n), #vars: 2, input, output | 139ms, input, output | 85ms, input, aspic, output, errors |
FGPSF09/patrs/pasta/a.11 | 1 - 2 * B + 2 * A 316ms, Ω(n), #vars: 2, input, output | 16 * A + 6 * B + 10 * ... 311ms, O(n), #vars: 3, input, output | max(6 * A + -4 * B + -... 549ms, O(n), #vars: 3, input, output | max(0, max(0, A - C) *... 138ms, O(n3), #vars: 2, input, output | 86ms, input, aspic, output, errors |
FGPSF09/patrs/sqrt | 1 83ms, Ω(1), #vars: 0, input, output | D + 2 151ms, O(n), #vars: 1, input, output | max(1 / 2 * D + 2, 2) 306ms, O(n), #vars: 1, input, output | max(D, 0) 50ms, O(n), #vars: 1, input, output | 90ms, input, aspic |
FGPSF09/patrs/sumto_no_if | 2 + B - A 83ms, Ω(n), #vars: 2, input, output | A + B + 3 66ms, O(n), #vars: 2, input, output | max(-1 * A + B + 3, 2) 201ms, O(n), #vars: 2, input, output | max(0, B + 1 + 0 - A) 60ms, O(n), #vars: 2, input, output | 100ms, input, aspic, output, errors |
KoAT-2013/sect1-lin | 2 + B + 2 * A 76ms, Ω(n), #vars: 2, input, output | 2 * A + B + 2 183ms, O(n), #vars: 2, input, output | 216ms, input, output | max(A, 0) + max(0, max... 59ms, O(n), #vars: 1, input, output | 91ms, input, aspic, output, errors |
KoAT-2013/sect1-quad | 3 + 1 / 2 * A^2 + B + ... 79ms, Ω(n2), #vars: 2, input, output | 2 * A + B + A^2 + 2 232ms, O(n2), #vars: 2, input, output | 221ms, input, output | max(A, 0) + max(0, max... 58ms, O(n2), #vars: 1, input, output | 66ms, input, aspic |
KoAT-2013/sect2 | 2 + 7 / 2 * B + 1 / 2 ... 133ms, Ω(n2), #vars: 1, input, output | 5 * B + 2 * B^2 + 2 312ms, O(n2), #vars: 1, input, output | max(2 * B + 3, 2, B + ... 379ms, O(n2), #vars: 1, input, output | max(B, 0) + max(B, 0) ... 90ms, O(n2), #vars: 1, input, output | 95ms, input, aspic, output, errors |
KoAT-2013/sect5-len | 1 + B 56ms, Ω(n), #vars: 1, input, output | B + 2 96ms, O(n), #vars: 1, input, output | max(B + 2, 2) 187ms, O(n), #vars: 1, input, output | max(B, 0) 42ms, O(n), #vars: 1, input, output | 79ms, input, aspic, output, errors |
KoAT-2013/sect5-sumSum | 1 + 5 / 2 * B + 1 / 2 ... 92ms, Ω(n2), #vars: 1, input, output | 11 * B + 4 * B^2 + 7 825ms, O(n2), #vars: 1, input, output | max(1, (B + 2) * B + 1) 254ms, O(n2), #vars: 1, input, output | max(B, 0) + max(0, max... 61ms, O(n2), #vars: 1, input, output | 77ms, input, aspic |
KoAT-2014/adding-exp-growth1 | 2 + pow(2, A) + A 95ms, EXP, #vars: 1, input, output | pow(2, A) + A + 2 251ms, EXP, #vars: 1, input, output | 264ms, input, output | 65ms, input, output | 19ms, input |
KoAT-2014/adding-exp-growth2 | 2 + C + pow(2, C) 97ms, EXP, #vars: 1, input, output | pow(2, 2 * C) + C + 3 302ms, EXP, #vars: 1, input, output | 286ms, input, output | 69ms, input, output | 21ms, input |
KoAT-2014/adding-exp-growth3 | 2 + pow(2, A) + 2 * A 96ms, EXP, #vars: 1, input, output | pow(2, 2 * A + 1) + 4 ... 258ms, EXP, #vars: 1, input, output | 252ms, input, output | 69ms, input, output | 13ms, input |
KoAT-2014/nesting-ex1 | 3 + 4 / 3 * B + 1 / 2 ... 114ms, Ω(n3), #vars: 1, input, output | 15 * B + 12 * B^2 + 4 ... 927ms, O(n3), #vars: 1, input, output | 506ms, input, output | max(B, 0) + max(0, max... 104ms, O(n3), #vars: 1, input, output | 16ms, input |
KoAT-2014/scaling-doubly-exp-growth | 3 + pow(2, A) + pow(2,... 122ms, EXP, #vars: 1, input, output | 2 * pow(2, A) * 2 + po... 452ms, EXP, #vars: 1, input, output | 444ms, input, output | 113ms, input, output | 19ms, input |
KoAT-2014/scaling-exp-growth | 2 + B + pow(2, B) * A 100ms, EXP, #vars: 2, input, output | pow(2, B) * A + B + A + 2 247ms, EXP, #vars: 2, input, output | 248ms, input, output | 73ms, input, output | 21ms, input |
SAS10/aaron2 | 1 1049ms, Ω(1), #vars: 0, input, output | 4 * A + 4 * C + 4 * E + 7 841ms, O(n), #vars: 3, input, output | 169ms, input, output, errors | 42ms, input, output | 88ms, input, aspic |
SAS10/ackermann | 1 693ms, Ω(1), #vars: 0, input, output | 16 * A + 4 217ms, O(n), #vars: 1, input, output | max(4 * A + 2, 5) 286ms, O(n), #vars: 1, input, output | max(A, 0) 76ms, O(n), #vars: 1, input, output | max(1 + A__o' + 1 + A_... 112ms, O(n), #vars: 1, input, aspic, output |
SAS10/ax | 1 + A 671ms, Ω(n), #vars: 1, input, output | 2 * A^2 + 10 * A + 14 297ms, O(n2), #vars: 1, input, output | max(3, 2 * A + -6 + ma... 469ms, O(n2), #vars: 1, input, output | 81ms, input, output | max(1 + 1 + -2 * A__o'... 138ms, O(n2), #vars: 1, input, aspic, output |
SAS10/complex | 6 5354ms, Ω(1), #vars: 0, input, output | 248 * A + 45 * C + 8960 1211ms, O(n), #vars: 2, input, output | 164ms, input, output, errors | 42ms, input, output | 60002ms, input, aspic, output, errors |
SAS10/counterex1 | 2 + A 1220ms, Ω(n), #vars: 1, input, output | 29234ms, input, output | 169ms, input, output, errors | 40ms, input, output | 1 + 1 + A__o' + -1 + 1... 285ms, O(n), #vars: 1, input, aspic, output, errors |
SAS10/cousot9 | 2 + C 704ms, Ω(n), #vars: 1, input, output | 2 * A^2 + 8 * A + C + 12 419ms, O(n2), #vars: 2, input, output | 161ms, input, output, errors | 40ms, input, output | max(4, 1 + A__o' + 1 + 1) 148ms, O(n), #vars: 1, input, aspic, output, errors |
SAS10/determinant | 11 / 6 - (-1 + A)^2 * ... 1276ms, Ω(n3), #vars: 1, input, output | 28 * A + 44 * A^2 + 16... 495ms, O(n3), #vars: 1, input, output | max(A + 4, 5, max((A +... 1674ms, O(n3), #vars: 1, input, output | max(0, -1 + min(A, A +... 124ms, O(n3), #vars: 1, input, output | max(2 + A__o' + -1 + 1... 173ms, O(n3), #vars: 1, input, aspic, output |
SAS10/easy1 | 1 1042ms, Ω(1), #vars: 0, input, output | 126 634ms, O(1), #vars: 0, input, output | 159ms, input, output, errors | 120ms, input, output | max(44, 84) 137ms, O(1), #vars: 0, input, aspic, output |
SAS10/easy2 | 1 + A 241ms, Ω(n), #vars: 1, input, output | A + 4 293ms, O(n), #vars: 1, input, output | max(A + 2, 3) 293ms, O(n), #vars: 1, input, output | max(0, D + -1 + max(mi... 56ms, O(n), #vars: 2, input, output | max(2 + A__o' + 1 + 1, 4) 97ms, O(n), #vars: 1, input, aspic, output |
SAS10/exmini | 1 842ms, Ω(1), #vars: 0, input, output | A + E + G + 107 285ms, O(n), #vars: 3, input, output | max(3, max(0, min(-1 /... 858ms, O(n), #vars: 3, input, output | 178ms, input, output | 99ms, input, aspic |
SAS10/gcd | 1 683ms, Ω(1), #vars: 0, input, output | 4 * A + 4 * C + 18 463ms, O(n), #vars: 2, input, output | 163ms, input, output, errors | 38ms, input, output | 115ms, input, aspic |
SAS10/insertsort | -2 + 2 * A 890ms, Ω(n), #vars: 1, input, output | 3 * A^2 + 22 * A + 28 553ms, O(n2), #vars: 1, input, output | max(4, max(3 * A + -6,... 1555ms, O(n2), #vars: 1, input, output | max(0, -1 + min(A, A +... 302ms, O(n2), #vars: 1, input, output | max(2 + -1 + A__o' + -... 252ms, O(n2), #vars: 1, input, aspic, output |
SAS10/loops | 3 953ms, Ω(1), #vars: 0, input, output | 13 * A + 2 * A^2 + 17 516ms, O(n2), #vars: 1, input, output | 163ms, input, output, errors | 38ms, input, output | 85ms, input, aspic |
SAS10/maccarthy91 | 2 + meter 2504ms, Ω(n), #vars: 1, input, output | 8 * A + 813 906ms, O(n), #vars: 1, input, output | 172ms, input, output, errors | 187ms, input, output | 154ms, input, aspic, output |
SAS10/nd_loop | 1 362ms, Ω(1), #vars: 0, input, output | 43 210ms, O(1), #vars: 0, input, output | 21 285ms, O(1), #vars: 0, input, output | 10 70ms, O(1), #vars: 0, input, output | 23 125ms, O(1), #vars: 0, input, aspic, output |
SAS10/ndecr | A 168ms, Ω(n), #vars: 1, input, output | A + 4 168ms, O(n), #vars: 1, input, output | max(A + 1, 3) 225ms, O(n), #vars: 1, input, output | max(0, A + -2) 44ms, O(n), #vars: 1, input, output | max(2 + -1 + A__o' + 1... 75ms, O(n), #vars: 1, input, aspic, output |
SAS10/nestedLoop | 1 + C 5310ms, Ω(n), #vars: 1, input, output | 12 * A + 12 * C + 6 * ... 1140ms, O(n2), #vars: 3, input, output | 186ms, input, output, errors | 45ms, input, output | 256ms, input, aspic, output |
SAS10/perfect | 1 2651ms, Ω(1), #vars: 0, input, output | 2 * A^2 + 10 * A + 15 665ms, O(n2), #vars: 1, input, output | 2 377ms, O(1), #vars: 0, input, output | 947ms, input, output | 109ms, input, aspic |
SAS10/random1d | 1 + A 609ms, Ω(n), #vars: 1, input, output | 2 * A + 7 304ms, O(n), #vars: 1, input, output | max(A + 2, 3) 336ms, O(n), #vars: 1, input, output | 136ms, input, output | max(2 + A__o' + 1 + 1, 4) 125ms, O(n), #vars: 1, input, aspic, output |
SAS10/random2d | 1 6484ms, Ω(1), #vars: 0, input, output | 22 * A + 19 1251ms, O(n), #vars: 1, input, output | max(2 * A + 2, 4) 1409ms, O(n), #vars: 1, input, output | 680ms, input, output | 218ms, input, aspic, output |
SAS10/realbubble | 4 2768ms, Ω(1), #vars: 0, input, output | 24 * A^2 + 60 * A + 27 875ms, O(n2), #vars: 1, input, output | max(5, max(max(0, min(... 927ms, O(n2), #vars: 1, input, output | 45ms, input, output | 223ms, input, aspic, output |
SAS10/realheapsort | 1 14632ms, Ω(1), #vars: 0, input, output | 1288422 * A + 714 * A^... 4644ms, O(n2), #vars: 1, input, output | 242ms, input, output, errors | 63ms, input, output | 1243ms, input, aspic |
SAS10/realselect | 1 3719ms, Ω(1), #vars: 0, input, output | 12 * A + 19 727ms, O(n), #vars: 1, input, output | 5 400ms, O(1), #vars: 0, input, output | 254ms, input, output | 220ms, input, aspic, output |
SAS10/realshellsort | 5 12763ms, Ω(1), #vars: 0, input, output | 264 * L + 105 * L^2 + ... 1069ms, O(n3), #vars: 1, input, output | 60001ms, input, output | 274ms, input, output | 351ms, input, aspic |
SAS10/relation1 | 1 16ms, Ω(1), #vars: 0, input, output | 3 24ms, O(1), #vars: 0, input, output | 3 167ms, O(1), #vars: 0, input, output | 43ms, input | 5 90ms, O(1), #vars: 0, input, aspic, output |
SAS10/rsd | 2 + A 864ms, Ω(n), #vars: 1, input, output | 6 * A^2 + 43 * A + 9 1152ms, O(n2), #vars: 1, input, output | 161ms, input, output, errors | 39ms, input, output | 107ms, input, aspic |
SAS10/sipmabubble | 1 + A 885ms, Ω(n), #vars: 1, input, output | 72 * A + 36 * A^2 + 40 541ms, O(n2), #vars: 1, input, output | 172ms, input, output, errors | 40ms, input, output | max(2 + 1 + A__o' + 1 ... 304ms, O(n2), #vars: 1, input, aspic, output |
SAS10/speedFails4 | 2 - B + C 1791ms, Ω(n), #vars: 2, input, output | 2 * B + 2 * C + 7 575ms, O(n), #vars: 2, input, output | 166ms, input, output, errors | 40ms, input, output | 112ms, input, aspic |
SAS10/speedpldi2 | 1 1210ms, Ω(1), #vars: 0, input, output | 6 * G + 9 435ms, O(n), #vars: 1, input, output | max(2 * G + 1, 3) 467ms, O(n), #vars: 1, input, output | 230ms, input, output | max(4, 2 + G__o' + G__... 217ms, O(n), #vars: 2, input, aspic, output |
SAS10/speedpldi3 | 2 + A 1745ms, Ω(n), #vars: 1, input, output | 2 * A * C + 8 * C + A + 9 396ms, O(n2), #vars: 2, input, output | max(3, 2 * C + -2 + ma... 1018ms, O(n2), #vars: 2, input, output | 393ms, input, output | max(5, 2 + C__o' * A__... 351ms, O(n2), #vars: 2, input, aspic, output |
SAS10/speedpldi4 | 2 1115ms, Ω(1), #vars: 0, input, output | 2 * A + 2 * C + 17 382ms, O(n), #vars: 2, input, output | max(-1 * A + C + 5, 6,... 3237ms, O(n), #vars: 2, input, output | 256ms, input, output | 93ms, input, aspic |
SAS10/terminate | 1 835ms, Ω(1), #vars: 0, input, output | A + E + 207 285ms, O(n), #vars: 2, input, output | max(3, max(0, min(-1 /... 755ms, O(n), #vars: 3, input, output | 155ms, input, output | 85ms, input, aspic |
SAS10/wcet1 | A 2158ms, Ω(n), #vars: 1, input, output | 3 * A + 13 658ms, O(n), #vars: 1, input, output | max(A + 1, 3) 645ms, O(n), #vars: 1, input, output | 169ms, input, output | 111ms, input, aspic |
SAS10/wcet2 | 4 1254ms, Ω(1), #vars: 0, input, output | 44 * A + 221 728ms, O(n), #vars: 1, input, output | 168ms, input, output, errors | 38ms, input, output | 60003ms, input, aspic, output |
SAS10/while2 | 2 + A 655ms, Ω(n), #vars: 1, input, output | 10 * A + 2 * A^2 + 14 390ms, O(n2), #vars: 1, input, output | max(4, max(0, min(A + ... 424ms, O(n2), #vars: 1, input, output | 155ms, input, output | max(4, 2 + A__o' * A__... 125ms, O(n2), #vars: 1, input, aspic, output |
SAS10/wise | -1 + C - A 621ms, Ω(n), #vars: 2, input, output | 2 * A + 2 * C + 12 364ms, O(n), #vars: 2, input, output | 162ms, input, output, errors | 40ms, input, output | max(2 + -2 + -1 * C__o... 126ms, O(n), #vars: 2, input, aspic, output |
T2/1 | F 235ms, Ω(n), #vars: 1, input, output | 4389ms, input, output | 737ms, input, output | 73ms, input, output | 302ms, input, aspic |
T2/1394-fail | INF 1973ms, INF, #vars: 1, input, output | 5560ms, input, output | 60001ms, input, output | 457ms, input, output | 70ms, input, aspic, aspic (errors) |
T2/1394-succeed | INF 1822ms, INF, #vars: 1, input, output | 5497ms, input, output | 51174ms, input, output | 523ms, input, output | 73ms, input, aspic, aspic (errors) |
T2/1394complete-fail | INF 1634ms, INF, #vars: 1, input, output | 4993ms, input, output | 57747ms, input, output | 436ms, input, output | 67ms, input, aspic, aspic (errors) |
T2/1394complete-succeed | INF 1798ms, INF, #vars: 1, input, output | 5584ms, input, output | 60004ms, input, output | 847ms, input, output | 73ms, input, aspic, aspic (errors) |
T2/2 | F 199ms, Ω(n), #vars: 1, input, output | 4024ms, input, output | 709ms, input, output | 83ms, input, output | 326ms, input, aspic |
T2/232 | -1 / 2 + (-1 + A) * A ... 299ms, Ω(n2), #vars: 1, input, output | A^2 + 3 * A + 2 204ms, O(n2), #vars: 1, input, output | max(1, max(0, (A + -1)... 250ms, O(n2), #vars: 1, input, output | max(0, A + -1) + max(0... 56ms, O(n2), #vars: 1, input, output | max(2, 1 + 3 / 2 * A__... 71ms, O(n2), #vars: 1, input, aspic, output |
T2/241 | -1 / 2 + (-1 + A) * A ... 312ms, Ω(n2), #vars: 1, input, output | A^2 + 3 * A + 2 202ms, O(n2), #vars: 1, input, output | max(1, max(0, (A + -1)... 198ms, O(n2), #vars: 1, input, output | max(0, A + -1) + max(0... 57ms, O(n2), #vars: 1, input, output | max(2, 1 + 3 / 2 * A__... 15216ms, O(n2), #vars: 1, input, aspic, output |
T2/3 | INF 31ms, INF, #vars: 1, input, output | 119ms, input, output | 176ms, input, output | 40ms, input, output | 71ms, input, aspic, output, errors |
T2/5 | INF 3876ms, INF, #vars: 1, input, output | 23448ms, input, output | 2047ms, input, output | 488ms, input, output | 1011ms, input, aspic, output, errors |
T2/6 | INF 34ms, INF, #vars: 1, input, output | 123ms, input, output | 164ms, input, output | 42ms, input, output | 69ms, input, aspic, output, errors |
T2/7 | INF 25ms, INF, #vars: 1, input, output | 683ms, input, output | 211ms, input, output | 50ms, input, output | 81ms, input, aspic |
T2/Loop | 1 10774ms, Ω(1), #vars: 0, input, output | 111 * C + 111 * E + 11... 1453ms, O(n), #vars: 4, input, output | 60002ms, input, output | 220ms, input, output | 723ms, input, aspic, output |
T2/a.10.c | 1 49ms, Ω(1), #vars: 0, input, output | 42136 * A + 42076 * B ... 345ms, O(n2), #vars: 4, input, output | max(2 * D + -2 * F + 2... 320ms, O(n), #vars: 4, input, output | 45ms, input | 377ms, input, aspic, output, errors |
T2/acqrel-fail | INF 106ms, INF, #vars: 1, input, output | 822ms, input, output | 454ms, input, output | 73ms, input, output | 77ms, input, aspic, output, errors |
T2/afagp-fail | INF 2129ms, INF, #vars: 1, input, output | 60019ms, input | 12584ms, input, output, errors | 765ms, input, output | 72ms, input, aspic, aspic (errors) |
T2/afagx1 | INF 92ms, INF, #vars: 1, input, output | 410ms, input, output | 315ms, input, output | 70ms, input, output | 82ms, input, aspic, output, errors |
T2/agafp | INF 5300ms, INF, #vars: 1, input, output | 60016ms, input | 60001ms, input, output | 2029ms, input, output | 75ms, input, aspic, aspic (errors) |
T2/apchild-accepted | 3 + free_30 2499ms, INF, #vars: 1, input, output | 23476ms, input, output | 60001ms, input, output | 1080ms, input, output | 71ms, input, aspic, aspic (errors) |
T2/apchild-accepted-fail | 3 + free_30 2715ms, INF, #vars: 1, input, output | 22900ms, input, output | 60001ms, input, output | 1023ms, input, output | 65ms, input, aspic, aspic (errors) |
T2/apchild-live | INF 2961ms, INF, #vars: 1, input, output | 26782ms, input, output | 60001ms, input, output | 561ms, input, output | 99ms, input, aspic, aspic (errors) |
T2/apchildlive-succeed | 2 + free_59 3422ms, INF, #vars: 1, input, output | 13024ms, input, output | 60003ms, input, output | 407ms, input, output | 64ms, input, aspic, aspic (errors) |
T2/array | 1 17ms, Ω(1), #vars: 0, input, output | 1 16ms, O(1), #vars: 0, input, output | 1 217ms, O(1), #vars: 0, input, output | 41ms, input | 3 76ms, O(1), #vars: 0, input, aspic, output |
T2/array1 | 1 16ms, Ω(1), #vars: 0, input, output | 1 17ms, O(1), #vars: 0, input, output | 1 144ms, O(1), #vars: 0, input, output | 40ms, input | 3 81ms, O(1), #vars: 0, input, aspic, output |
T2/array2 | 51 61ms, Ω(1), #vars: 0, input, output | 52 90ms, O(1), #vars: 0, input, output | 52 168ms, O(1), #vars: 0, input, output | 50 56ms, O(1), #vars: 0, input, output | 54 102ms, O(1), #vars: 0, input, aspic, output |
T2/array3 | 102 79ms, Ω(1), #vars: 0, input, output | 103 183ms, O(1), #vars: 0, input, output | 103 389ms, O(1), #vars: 0, input, output | 100 70ms, O(1), #vars: 0, input, output | 105 87ms, O(1), #vars: 0, input, aspic, output |
T2/array_free | 43 66ms, Ω(1), #vars: 0, input, output | 86 136ms, O(1), #vars: 0, input, output | 44 166ms, O(1), #vars: 0, input, output | 42 71ms, O(1), #vars: 0, input, output | 46 81ms, O(1), #vars: 0, input, aspic, output |
T2/array_init | 11 66ms, Ω(1), #vars: 0, input, output | 13 91ms, O(1), #vars: 0, input, output | 12 173ms, O(1), #vars: 0, input, output | 10 41ms, O(1), #vars: 0, input, output | 14 76ms, O(1), #vars: 0, input, aspic, output |
T2/array_init_assign | 6 76ms, Ω(1), #vars: 0, input, output | 8 182ms, O(1), #vars: 0, input, output | 7 206ms, O(1), #vars: 0, input, output | 4 62ms, O(1), #vars: 0, input, output | 9 92ms, O(1), #vars: 0, input, aspic, output |
T2/ase_example | 33 100ms, Ω(1), #vars: 0, input, output | 85 189ms, O(1), #vars: 0, input, output | 34 344ms, O(1), #vars: 0, input, output | 30 101ms, O(1), #vars: 0, input, output | 36 120ms, O(1), #vars: 0, input, aspic, output |
T2/bf10 | 1 327ms, Ω(1), #vars: 0, input, output | 658 3093ms, O(1), #vars: 0, input, output | 85 1079ms, O(1), #vars: 0, input, output | 80 138ms, O(1), #vars: 0, input, output | 91 213ms, O(1), #vars: 0, input, aspic, output |
T2/bf11 | 1 324ms, Ω(1), #vars: 0, input, output | 736 3214ms, O(1), #vars: 0, input, output | 91 827ms, O(1), #vars: 0, input, output | 87 133ms, O(1), #vars: 0, input, output | 97 172ms, O(1), #vars: 0, input, aspic, output |
T2/bf12 | 1 311ms, Ω(1), #vars: 0, input, output | 814 3063ms, O(1), #vars: 0, input, output | 97 785ms, O(1), #vars: 0, input, output | 94 126ms, O(1), #vars: 0, input, output | 103 202ms, O(1), #vars: 0, input, aspic, output |
T2/bf13 | 1 321ms, Ω(1), #vars: 0, input, output | 898 2931ms, O(1), #vars: 0, input, output | 103 822ms, O(1), #vars: 0, input, output | 101 129ms, O(1), #vars: 0, input, output | 109 221ms, O(1), #vars: 0, input, aspic, output |
T2/bf14 | 1 308ms, Ω(1), #vars: 0, input, output | 986 3111ms, O(1), #vars: 0, input, output | 109 818ms, O(1), #vars: 0, input, output | 108 130ms, O(1), #vars: 0, input, output | 115 221ms, O(1), #vars: 0, input, aspic, output |
T2/bf15 | 1 315ms, Ω(1), #vars: 0, input, output | 1078 3100ms, O(1), #vars: 0, input, output | 115 765ms, O(1), #vars: 0, input, output | 115 164ms, O(1), #vars: 0, input, output | 121 224ms, O(1), #vars: 0, input, aspic, output |
T2/bf16 | 1 318ms, Ω(1), #vars: 0, input, output | 1195 3452ms, O(1), #vars: 0, input, output | 121 778ms, O(1), #vars: 0, input, output | 122 131ms, O(1), #vars: 0, input, output | 127 190ms, O(1), #vars: 0, input, aspic, output |
T2/bf17 | 1 307ms, Ω(1), #vars: 0, input, output | 1274 3333ms, O(1), #vars: 0, input, output | 127 842ms, O(1), #vars: 0, input, output | 129 127ms, O(1), #vars: 0, input, output | 133 261ms, O(1), #vars: 0, input, aspic, output |
T2/bf18 | 1 317ms, Ω(1), #vars: 0, input, output | 1378 3096ms, O(1), #vars: 0, input, output | 133 803ms, O(1), #vars: 0, input, output | 136 130ms, O(1), #vars: 0, input, output | 139 226ms, O(1), #vars: 0, input, aspic, output |
T2/bf19 | 1 325ms, Ω(1), #vars: 0, input, output | 1486 3017ms, O(1), #vars: 0, input, output | 139 807ms, O(1), #vars: 0, input, output | 143 130ms, O(1), #vars: 0, input, output | 145 233ms, O(1), #vars: 0, input, aspic, output |
T2/bf20 | 1 331ms, Ω(1), #vars: 0, input, output | 1598 3161ms, O(1), #vars: 0, input, output | 145 1068ms, O(1), #vars: 0, input, output | 150 137ms, O(1), #vars: 0, input, output | 151 230ms, O(1), #vars: 0, input, aspic, output |
T2/bf5 | 1 325ms, Ω(1), #vars: 0, input, output | 342 3029ms, O(1), #vars: 0, input, output | 55 780ms, O(1), #vars: 0, input, output | 45 126ms, O(1), #vars: 0, input, output | 61 162ms, O(1), #vars: 0, input, aspic, output |
T2/bf6 | 1 325ms, Ω(1), #vars: 0, input, output | 394 3135ms, O(1), #vars: 0, input, output | 61 851ms, O(1), #vars: 0, input, output | 52 142ms, O(1), #vars: 0, input, output | 67 235ms, O(1), #vars: 0, input, aspic, output |
T2/bf7 | 1 331ms, Ω(1), #vars: 0, input, output | 454 3271ms, O(1), #vars: 0, input, output | 67 803ms, O(1), #vars: 0, input, output | 59 134ms, O(1), #vars: 0, input, output | 73 235ms, O(1), #vars: 0, input, aspic, output |
T2/bf8 | 1 318ms, Ω(1), #vars: 0, input, output | 518 3127ms, O(1), #vars: 0, input, output | 73 790ms, O(1), #vars: 0, input, output | 66 167ms, O(1), #vars: 0, input, output | 79 222ms, O(1), #vars: 0, input, aspic, output |
T2/bf9 | 1 333ms, Ω(1), #vars: 0, input, output | 589 3103ms, O(1), #vars: 0, input, output | 79 1041ms, O(1), #vars: 0, input, output | 73 141ms, O(1), #vars: 0, input, output | 85 325ms, O(1), #vars: 0, input, aspic, output |
T2/bio | 1 31531ms, Ω(1), #vars: 0, input, output | 60013ms, input | 60001ms, input | 2029ms, input, output | 69ms, input, aspic, aspic (errors) |
T2/bitcount16 | 1 104ms, Ω(1), #vars: 0, input, output | 34 141ms, O(1), #vars: 0, input, output | 18 318ms, O(1), #vars: 0, input, output | 48 53ms, O(1), #vars: 0, input, output | 20 121ms, O(1), #vars: 0, input, aspic, output |
T2/bitcount32 | 1 116ms, Ω(1), #vars: 0, input, output | 66 133ms, O(1), #vars: 0, input, output | 34 308ms, O(1), #vars: 0, input, output | 96 58ms, O(1), #vars: 0, input, output | 36 117ms, O(1), #vars: 0, input, aspic, output |
T2/broydn | 2 - B + A 1450ms, Ω(n), #vars: 2, input, output | 11682ms, input, output | 60001ms, input, output | 336ms, input, output | 4711ms, input, aspic |
T2/broydn.c.i.broydn.pl.t2.fixed nonlinear | 2 - B + A 1998ms, Ω(n), #vars: 2, input, output | 14084ms, input, output | 60001ms, input, output | 372ms, input, output | Non-linear example not handled by prover. |
T2/broydn.c.i.broydn.pl.t2.nor.t2.rlgfixed | 2 - B + A 1418ms, Ω(n), #vars: 2, input, output | 11672ms, input, output | 60012ms, input, output | 388ms, input, output | 5172ms, input, aspic |
T2/brp | 1 11112ms, Ω(1), #vars: 0, input, output | 60013ms, input | 60001ms, input, output | 1168ms, input, output | 60003ms, input, aspic |
T2/brp_withassume | 1 12079ms, Ω(1), #vars: 0, input, output | 60013ms, input | 60001ms, input, output | 1317ms, input, output | 30996ms, input, aspic, aspic (errors) |
T2/bs | 1 153ms, Ω(1), #vars: 0, input, output | 2036ms, input, output | 393ms, input, output | 226ms, input, output | 140ms, input, aspic, output, errors |
T2/bsort100 | 1 218ms, Ω(1), #vars: 0, input, output | 1413880 413ms, O(1), #vars: 0, input, output | 10201 2741ms, O(1), #vars: 0, input, output | 29899 127ms, O(1), #vars: 0, input, output | 212ms, input, aspic, output, errors |
T2/bubbleSort | 1 / 2 - 1 / 2 * (-1 + ... 245ms, Ω(n2), #vars: 1, input, output | 422 * C + 20 * C^2 + 591 396ms, O(n2), #vars: 1, input, output | max(5, (C + 1) * (C + ... 546ms, O(n2), #vars: 1, input, output | max(C, 0) + max(0, C +... 81ms, O(n2), #vars: 1, input, output | 134ms, input, aspic, output, errors |
T2/bubblesort_inner_loop | 1 111ms, Ω(1), #vars: 0, input, output | 11 227ms, O(1), #vars: 0, input, output | 6 210ms, O(1), #vars: 0, input, output | 4 48ms, O(1), #vars: 0, input, output | 8 84ms, O(1), #vars: 0, input, aspic, output |
T2/buggyNonTermLoop | INF 10520ms, INF, #vars: 1, input, output | 2903ms, input, output | 60008ms, input, output | 226ms, input, output | 798ms, input, aspic, output |
T2/byron-1 | 1 61ms, Ω(1), #vars: 0, input, output | A + 3 253ms, O(n), #vars: 1, input, output | max(A + 2, 2) 186ms, O(n), #vars: 1, input, output | 43ms, input, output | 90ms, input, aspic |
T2/byron-2 | -1 + C 645ms, Ω(n), #vars: 1, input, output | 347ms, input, output | 239ms, input, output | 104ms, input, output | 133ms, input, aspic, output, errors |
T2/byron-3 | 1 58ms, Ω(1), #vars: 0, input, output | 2780ms, input, output | 182ms, input, output | 68ms, input, output | 75ms, input, aspic |
T2/byron-4 | 1 + 2 * meter 213ms, Ω(n), #vars: 1, input, output | 2 * A + 3 280ms, O(n), #vars: 1, input, output | max(A + 2, 4) 221ms, O(n), #vars: 1, input, output | 208ms, input, output | 76ms, input, aspic, output, errors |
T2/cfg | INF 65ms, INF, #vars: 1, input, output | 1495ms, input, output | 190ms, input, output | 49ms, input, output | 82ms, input, aspic, output, errors |
T2/cnt | 1 248ms, Ω(1), #vars: 0, input, output | 1773 411ms, O(1), #vars: 0, input, output | 243 1396ms, O(1), #vars: 0, input, output | 450 87ms, O(1), #vars: 0, input, output | 431ms, input, aspic |
T2/collatz | 1 1784ms, Ω(1), #vars: 0, input, output | 2321ms, input, output | 218ms, input, output | 10722ms, input, output | 105ms, input, aspic |
T2/complex_guard | 7 61ms, Ω(1), #vars: 0, input, output | 25 130ms, O(1), #vars: 0, input, output | 10 235ms, O(1), #vars: 0, input, output | 3 80ms, O(1), #vars: 0, input, output | 12 86ms, O(1), #vars: 0, input, aspic, output |
T2/constants | 1 84ms, Ω(1), #vars: 0, input, output | 404 126ms, O(1), #vars: 0, input, output | 402 252ms, O(1), #vars: 0, input, output | 400 72ms, O(1), #vars: 0, input, output | 98ms, input, aspic, output |
T2/consts1 | 1 61ms, Ω(1), #vars: 0, input, output | 301 87ms, O(1), #vars: 0, input, output | 200 164ms, O(1), #vars: 0, input, output | 67ms, input, output | 202 79ms, O(1), #vars: 0, input, aspic, output |
T2/consts1nt | INF 70ms, INF, #vars: 1, input, output | 594ms, input, output | 170ms, input, output | 81ms, input, output | 71ms, input, aspic, output, errors |
T2/consts2 | 1 + meter 61ms, Ω(n), #vars: 1, input, output | A + 1000 87ms, O(n), #vars: 1, input, output | max(1 / 1000 * A, 1) 164ms, O(n), #vars: 1, input, output | max(0, A + -1000) 71ms, O(n), #vars: 1, input, output | 75ms, input, aspic, output, errors |
T2/consts2nt | INF 60ms, INF, #vars: 1, input, output | 1354ms, input, output | 163ms, input, output | 61ms, input, output | 80ms, input, aspic, output, errors |
T2/consts3 | -200 + A 64ms, Ω(n), #vars: 1, input, output | A + 1 77ms, O(n), #vars: 1, input, output | max(A + -200, 1) 218ms, O(n), #vars: 1, input, output | max(0, A + -201) 47ms, O(n), #vars: 1, input, output | 97ms, input, aspic, output, errors |
T2/consts3nt | INF 52ms, INF, #vars: 1, input, output | 784ms, input, output | 166ms, input, output | 42ms, input, output | 83ms, input, aspic, output, errors |
T2/consts4 | 1 + meter 57ms, Ω(n), #vars: 1, input, output | A + 1200 81ms, O(n), #vars: 1, input, output | max(1 / 1000 * A + -1 ... 161ms, O(n), #vars: 1, input, output | max(0, A + -1200) 42ms, O(n), #vars: 1, input, output | 71ms, input, aspic, output, errors |
T2/consts4nt | INF 57ms, INF, #vars: 1, input, output | 1294ms, input, output | 162ms, input, output | 54ms, input, output | 78ms, input, aspic, output, errors |
T2/consts5 | 1 79ms, Ω(1), #vars: 0, input, output | 1 28ms, O(1), #vars: 0, input, output | 1 172ms, O(1), #vars: 0, input, output | 46ms, input | 3 81ms, O(1), #vars: 0, input, aspic, output |
T2/consts5nt | INF 74ms, INF, #vars: 1, input, output | 1404ms, input, output | 218ms, input, output | 52ms, input, output | 86ms, input, aspic, output, errors |
T2/cover | 1 800ms, Ω(1), #vars: 0, input, output | 60012ms, input | 60001ms, input, output | 762ms, input, output | 60003ms, input, aspic, output |
T2/crc | 1 606ms, Ω(1), #vars: 0, input, output | 1008 * L + 346135 2678ms, O(n), #vars: 1, input, output | 2649 6922ms, O(1), #vars: 0, input, output | 4194 292ms, O(1), #vars: 0, input, output | 2266ms, input, aspic, output |
T2/create | -1 + free_26 119ms, INF, #vars: 1, input, output | 873ms, input, output | 312ms, input, output | 63ms, input, output | 511ms, input, aspic |
T2/create_seg | -1 + free_26 88ms, INF, #vars: 1, input, output | 884ms, input, output | 352ms, input, output | 67ms, input, output | 668ms, input, aspic |
T2/create_via_tmps | 1 + U + A 2014ms, Ω(n), #vars: 2, input, output | 4 * U + A + 15 893ms, O(n), #vars: 2, input, output | max(A + -1, 1) 1604ms, O(n), #vars: 1, input, output | 231ms, input, output | 2677ms, input, aspic |
T2/ctl | INF 74ms, INF, #vars: 1, input, output | 271ms, input, output | 369ms, input, output | 48ms, input, output | 132ms, input, aspic, output, errors |
T2/curious | INF 52ms, INF, #vars: 1, input, output | 126ms, input, output | 167ms, input, output | 40ms, input, output | 78ms, input, aspic, output, errors |
T2/curious4 | INF 3687ms, INF, #vars: 1, input, output | 60013ms, input | 11500ms, input, output, errors | 772ms, input, output | 85ms, input, aspic, aspic (errors) |
T2/d | 1 96ms, Ω(1), #vars: 0, input, output | 1227ms, input, output | 222ms, input, output | 53ms, input, output | 117ms, input, aspic |
T2/db2 | 34 + free_1 23118ms, INF, #vars: 1, input, output | 60015ms, input | 60001ms, input | 4030ms, input, output | 60ms, input, aspic, aspic (errors) |
T2/db3 | 34 + free_1 25052ms, INF, #vars: 1, input, output | 60022ms, input | 60001ms, input | 3839ms, input, output | 80ms, input, aspic, aspic (errors) |
T2/dead.neg-st88b-succeed | INF 425ms, INF, #vars: 1, input, output | 1886ms, input, output | 310ms, input, output | 162ms, input, output | 105ms, input, aspic, output, errors |
T2/destroy | 1 + R + free_74 2274ms, INF, #vars: 2, input, output | 1516ms, input, output | 1607ms, input, output | 203ms, input, output | 5834ms, input, aspic |
T2/destroy_seg | 1 + free_75 + T 2594ms, INF, #vars: 2, input, output | 1421ms, input, output | 2538ms, input, output | 185ms, input, output | 8552ms, input, aspic |
T2/destroy_seg_leak | 60016ms, input, output | 60014ms, input | 35180ms, input, output | 26547ms, input, output, errors | 155ms, input, aspic, aspic (errors) |
T2/disj_nightmare_abi | 1 109ms, Ω(1), #vars: 0, input, output | 3 53ms, O(1), #vars: 0, input, output | 2 173ms, O(1), #vars: 0, input, output | 1 103ms, O(1), #vars: 0, input, output | 80ms, input, aspic, output, errors |
T2/dropbuf | INF 1200ms, INF, #vars: 1, input, output | 1877ms, input, output | 5141ms, input, output | 434ms, input, output | 1234ms, input, aspic, output |
T2/dropbuf-live | 1 17ms, Ω(1), #vars: 0, input, output | 1 26ms, O(1), #vars: 0, input, output | 1 144ms, O(1), #vars: 0, input, output | 41ms, input | 3 97ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test | 1 16ms, Ω(1), #vars: 0, input, output | 1 18ms, O(1), #vars: 0, input, output | 1 195ms, O(1), #vars: 0, input, output | 44ms, input | 3 82ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test1 | 1 16ms, Ω(1), #vars: 0, input, output | 1 22ms, O(1), #vars: 0, input, output | 1 143ms, O(1), #vars: 0, input, output | 35ms, input | 3 81ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test10 | 22 81ms, Ω(1), #vars: 0, input, output | 31 211ms, O(1), #vars: 0, input, output | 23 244ms, O(1), #vars: 0, input, output | 20 66ms, O(1), #vars: 0, input, output | 25 106ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test11 | 1 18ms, Ω(1), #vars: 0, input, output | 1 17ms, O(1), #vars: 0, input, output | 1 185ms, O(1), #vars: 0, input, output | 66ms, input | 3 90ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test12 | 1 18ms, Ω(1), #vars: 0, input, output | 1 18ms, O(1), #vars: 0, input, output | 1 143ms, O(1), #vars: 0, input, output | 49ms, input | 3 76ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test13 | 1 17ms, Ω(1), #vars: 0, input, output | 1 16ms, O(1), #vars: 0, input, output | 1 144ms, O(1), #vars: 0, input, output | 53ms, input | 3 83ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test15 | 22 79ms, Ω(1), #vars: 0, input, output | 23 171ms, O(1), #vars: 0, input, output | 23 217ms, O(1), #vars: 0, input, output | 20 64ms, O(1), #vars: 0, input, output | 25 82ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test4 | 1 17ms, Ω(1), #vars: 0, input, output | 1 18ms, O(1), #vars: 0, input, output | 1 143ms, O(1), #vars: 0, input, output | 66ms, input | 3 76ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test5 | 1 17ms, Ω(1), #vars: 0, input, output | 1 20ms, O(1), #vars: 0, input, output | 1 145ms, O(1), #vars: 0, input, output | 102ms, input | 3 74ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test6 | 11 56ms, Ω(1), #vars: 0, input, output | 12 82ms, O(1), #vars: 0, input, output | 12 169ms, O(1), #vars: 0, input, output | 10 47ms, O(1), #vars: 0, input, output | 14 77ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test8 | 1 23ms, Ω(1), #vars: 0, input, output | 1 19ms, O(1), #vars: 0, input, output | 1 144ms, O(1), #vars: 0, input, output | 52ms, input | 3 79ms, O(1), #vars: 0, input, aspic, output |
T2/dsa_test9 | 1 17ms, Ω(1), #vars: 0, input, output | 1 20ms, O(1), #vars: 0, input, output | 1 148ms, O(1), #vars: 0, input, output | 36ms, input | 3 103ms, O(1), #vars: 0, input, aspic, output |
T2/dummy | INF 81ms, INF, #vars: 1, input, output | 2515ms, input, output | 187ms, input, output | 44ms, input, output | 68ms, input, aspic |
T2/e-1394complete-succeed | INF 1661ms, INF, #vars: 1, input, output | 5135ms, input, output | 50045ms, input, output | 353ms, input, output | 57ms, input, aspic, aspic (errors) |
T2/e-acqrel-fail | INF 93ms, INF, #vars: 1, input, output | 652ms, input, output | 248ms, input, output | 54ms, input, output | 94ms, input, aspic, output, errors |
T2/e-acqrel-succeed | INF 80ms, INF, #vars: 1, input, output | 803ms, input, output | 485ms, input, output | 61ms, input, output | 97ms, input, aspic, output, errors |
T2/e-pgarch-fail | INF 174ms, INF, #vars: 1, input, output | 368ms, input, output | 550ms, input, output | 48ms, input, output | 233ms, input, aspic, output, errors |
T2/e-pgarch-succeed | INF 169ms, INF, #vars: 1, input, output | 397ms, input, output | 785ms, input, output | 59ms, input, output | 282ms, input, aspic, output, errors |
T2/e-popl07-fail | INF 268ms, INF, #vars: 1, input, output | 975ms, input, output | 3041ms, input, output | 562ms, input, output | 693ms, input, aspic, output |
T2/edn | 1 363ms, Ω(1), #vars: 0, input, output | 1291579 2353ms, O(1), #vars: 0, input, output | 27161 / 7 10535ms, O(1), #vars: 0, input, output | 6297 210ms, O(1), #vars: 0, input, output | 6398ms, input, aspic, output |
T2/efegp | 3 - 2 * free_2 1632ms, INF, #vars: 1, input, output | 31773ms, input, output | 4258ms, input, output, errors | 677ms, input, output | 62ms, input, aspic, aspic (errors) |
T2/elmhes | 3 - E + A 876ms, Ω(n), #vars: 2, input, output | 13577382562501012 * A ... 1500ms, O(n2), #vars: 3, input, output | 6294ms, input, output | 464ms, input, output | 782ms, input, aspic, output, errors |
T2/elmhes.c.i.elmhes.pl.t2.fixed nonlinear | 3 - E + A 1525ms, Ω(n), #vars: 2, input, output | 2318416846246180 * A +... 1515ms, O(n2), #vars: 3, input, output | 7053ms, input, output | 475ms, input, output | Non-linear example not handled by prover. |
T2/elmhes.c.i.elmhes.pl.t2.nor.t2.rlgfixed | 3 - E + A 894ms, Ω(n), #vars: 2, input, output | 2318416846246180 * A +... 1488ms, O(n2), #vars: 3, input, output | 6583ms, input, output | 403ms, input, output | 754ms, input, aspic, output, errors |
T2/eric | 1 - 2 * B + 2 * A 561ms, Ω(n), #vars: 2, input, output | 1496ms, input, output | max(2 * A + -2 * B + 3... 470ms, O(n), #vars: 2, input, output | 80ms, input, output | 83ms, input, aspic, output, errors |
T2/eric1 | 1 + 2 * B 151ms, Ω(n), #vars: 1, input, output | 8490ms, input, output | max(2, max(0, min(B + ... 354ms, O(n2), #vars: 1, input, output | 109ms, input, output | max(3 / 2 * B__o' + 1 ... 87ms, O(n2), #vars: 1, input, aspic, output |
T2/eric2 | 3 + H 4545ms, Ω(n), #vars: 1, input, output | 60018ms, input | 5820ms, input, output | 251ms, input, output | 846ms, input, aspic, output |
T2/eric3 | INF 117ms, INF, #vars: 1, input, output | 1322ms, input, output | 205ms, input, output | 252ms, input, output | 91ms, input, aspic, output, errors |
T2/ex1 | INF 27ms, INF, #vars: 1, input, output | 736ms, input, output | 184ms, input, output | 38ms, input, output | 93ms, input, aspic, output, errors |
T2/ex10 | INF 85ms, INF, #vars: 1, input, output | 819ms, input, output | 373ms, input, output | 87ms, input, output | 158ms, input, aspic, output, errors |
T2/ex11 | 1 5783ms, Ω(1), #vars: 0, input, output | 2029ms, input, output | 241ms, input, output | 168ms, input, output | 76ms, input, aspic, output, errors |
T2/ex12 | 1 65ms, Ω(1), #vars: 0, input, output | 20 137ms, O(1), #vars: 0, input, output | 11 201ms, O(1), #vars: 0, input, output | 18 42ms, O(1), #vars: 0, input, output | 23 106ms, O(1), #vars: 0, input, aspic, output |
T2/ex13 | 1 16ms, Ω(1), #vars: 0, input, output | 1 18ms, O(1), #vars: 0, input, output | 1 202ms, O(1), #vars: 0, input, output | 48ms, input | 3 81ms, O(1), #vars: 0, input, aspic, output |
T2/ex14 | 11 58ms, Ω(1), #vars: 0, input, output | 12 128ms, O(1), #vars: 0, input, output | 12 178ms, O(1), #vars: 0, input, output | 10 46ms, O(1), #vars: 0, input, output | 14 78ms, O(1), #vars: 0, input, aspic, output |
T2/ex15 | 1 17ms, Ω(1), #vars: 0, input, output | 1 26ms, O(1), #vars: 0, input, output | 1 146ms, O(1), #vars: 0, input, output | 34ms, input | 3 107ms, O(1), #vars: 0, input, aspic, output |
T2/ex16 | 1 153ms, Ω(1), #vars: 0, input, output | 4115ms, input, output | 614ms, input, output | 66ms, input, output | 204ms, input, aspic |
T2/ex17 | 1 95ms, Ω(1), #vars: 0, input, output | 104 247ms, O(1), #vars: 0, input, output | 102 520ms, O(1), #vars: 0, input, output | 70ms, input, output | 133ms, input, aspic, output |
T2/ex18 | 1 153ms, Ω(1), #vars: 0, input, output | 2932ms, input, output | 302 396ms, O(1), #vars: 0, input, output | 195ms, input, output | 162ms, input, aspic, output, errors |
T2/ex19 | INF 69ms, INF, #vars: 1, input, output | 1738ms, input, output | 293ms, input, output | 55ms, input, output | 63ms, input, aspic, output, errors |
T2/ex2 | INF 77ms, INF, #vars: 1, input, output | 2256ms, input, output | 216ms, input, output | 112ms, input, output | 83ms, input, aspic, output, errors |
T2/ex20 | 1 71ms, Ω(1), #vars: 0, input, output | 1030 174ms, O(1), #vars: 0, input, output | 1026 293ms, O(1), #vars: 0, input, output | 1024 86ms, O(1), #vars: 0, input, output | 1028 103ms, O(1), #vars: 0, input, aspic, output |
T2/ex21 | 202 79ms, Ω(1), #vars: 0, input, output | 499 209ms, O(1), #vars: 0, input, output | 203 247ms, O(1), #vars: 0, input, output | 200 65ms, O(1), #vars: 0, input, output | 205 88ms, O(1), #vars: 0, input, aspic, output |
T2/ex22 | 1 361ms, Ω(1), #vars: 0, input, output | 11928 4268ms, O(1), #vars: 0, input, output | 390 3481ms, O(1), #vars: 0, input, output | 370 190ms, O(1), #vars: 0, input, output | 1570ms, input, aspic, output |
T2/ex23 | 37 66ms, Ω(1), #vars: 0, input, output | 39 115ms, O(1), #vars: 0, input, output | 38 247ms, O(1), #vars: 0, input, output | 36 56ms, O(1), #vars: 0, input, output | max(40, 3) 96ms, O(1), #vars: 0, input, aspic, output |
T2/ex26 | 202 78ms, Ω(1), #vars: 0, input, output | 499 219ms, O(1), #vars: 0, input, output | 203 327ms, O(1), #vars: 0, input, output | 200 58ms, O(1), #vars: 0, input, output | 205 99ms, O(1), #vars: 0, input, aspic, output |
T2/ex27 | 1 479ms, Ω(1), #vars: 0, input, output | 22853 10128ms, O(1), #vars: 0, input, output | 595 10627ms, O(1), #vars: 0, input, output | 570 400ms, O(1), #vars: 0, input, output | 4101ms, input, aspic, output |
T2/ex29 | 1 31ms, Ω(1), #vars: 0, input, output | 15 131ms, O(1), #vars: 0, input, output | 4 234ms, O(1), #vars: 0, input, output | 50ms, input | 255ms, input, aspic, output |
T2/ex3 | 11 68ms, Ω(1), #vars: 0, input, output | 13 86ms, O(1), #vars: 0, input, output | 23 / 2 188ms, O(1), #vars: 0, input, output | 10 48ms, O(1), #vars: 0, input, output | 25 82ms, O(1), #vars: 0, input, aspic, output |
T2/ex30 | 2 + free + free_2 76ms, INF, #vars: 2, input, output | 2348ms, input, output | 402ms, input, output | 61ms, input, output | 121ms, input, aspic, output, errors |
T2/ex31 | 1 95ms, Ω(1), #vars: 0, input, output | 1099ms, input, output | 257ms, input, output | 72ms, input, output | 88ms, input, aspic, output, errors |
T2/ex32 | 2002 76ms, Ω(1), #vars: 0, input, output | 2003 226ms, O(1), #vars: 0, input, output | 2003 234ms, O(1), #vars: 0, input, output | 2000 61ms, O(1), #vars: 0, input, output | 95ms, input, aspic, output |
T2/ex33 | 1 50ms, Ω(1), #vars: 0, input, output | 3 66ms, O(1), #vars: 0, input, output | 1 155ms, O(1), #vars: 0, input, output | 36ms, input | 3 86ms, O(1), #vars: 0, input, aspic, output |
T2/ex34 | 1 19ms, Ω(1), #vars: 0, input, output | 1 13ms, O(1), #vars: 0, input, output | 1 169ms, O(1), #vars: 0, input, output | 48ms, input | 65ms, input, aspic, aspic (errors) |
T2/ex36 | 12 + free_82 + free_64... 14866ms, INF, #vars: 5, input, output | 60018ms, input | 60001ms, input, output | 1088ms, input, output | 69ms, input, aspic, aspic (errors) |
T2/ex37 | 1 16ms, Ω(1), #vars: 0, input, output | 1 14ms, O(1), #vars: 0, input, output | 1 197ms, O(1), #vars: 0, input, output | 49ms, input | 3 78ms, O(1), #vars: 0, input, aspic, output |
T2/ex4 | 1 228ms, Ω(1), #vars: 0, input, output | 87 325ms, O(1), #vars: 0, input, output | 34 516ms, O(1), #vars: 0, input, output | 20 95ms, O(1), #vars: 0, input, output | 36 146ms, O(1), #vars: 0, input, aspic, output |
T2/ex40 | INF 33ms, INF, #vars: 1, input, output | 1438ms, input, output | 200ms, input, output | 50ms, input, output | 83ms, input, aspic, output, errors |
T2/ex6 | 1 48ms, Ω(1), #vars: 0, input, output | 3 19ms, O(1), #vars: 0, input, output | 1 147ms, O(1), #vars: 0, input, output | 35ms, input | 3 82ms, O(1), #vars: 0, input, aspic, output |
T2/ex7 | 11 56ms, Ω(1), #vars: 0, input, output | 12 92ms, O(1), #vars: 0, input, output | 12 197ms, O(1), #vars: 0, input, output | 10 48ms, O(1), #vars: 0, input, output | 14 83ms, O(1), #vars: 0, input, aspic, output |
T2/ex8 | INF 77ms, INF, #vars: 1, input, output | 2835ms, input, output | 417ms, input, output | 78ms, input, output | 82ms, input, aspic, aspic (errors) |
T2/ex9 | INF 88ms, INF, #vars: 1, input, output | 2693ms, input, output | 586ms, input, output | 88ms, input, output | 78ms, input, aspic, aspic (errors) |
T2/example | A 189ms, Ω(n), #vars: 1, input, output | 2 * A + 2 * B + 5 138ms, O(n), #vars: 2, input, output | max(A + B + -1, 1) 246ms, O(n), #vars: 2, input, output | max(0, B + -1) + max(0... 80ms, O(n), #vars: 1, input, output | max(2, 2, 1 + -1 + B__... 102ms, O(n), #vars: 2, input, aspic, output |
T2/fake-succeed | INF 7722ms, INF, #vars: 1, input, output | 60015ms, input | 60001ms, input, output | 486ms, input, output | 61ms, input, aspic, aspic (errors) |
T2/fast_poll | INF 2204ms, INF, #vars: 1, input, output | 10432ms, input, output | 60001ms, input, output | 185ms, input, output | 5872ms, input, aspic, output |
T2/fdct | 18 81ms, Ω(1), #vars: 0, input, output | 31 171ms, O(1), #vars: 0, input, output | 19 707ms, O(1), #vars: 0, input, output | 16 70ms, O(1), #vars: 0, input, output | 21 924ms, O(1), #vars: 0, input, aspic, output |
T2/fermat | 12 103ms, Ω(1), #vars: 0, input, output | 17 297ms, O(1), #vars: 0, input, output | 13 857ms, O(1), #vars: 0, input, output | 9 122ms, O(1), #vars: 0, input, output | 15 349ms, O(1), #vars: 0, input, aspic, output |
T2/fibcall | 1 60ms, Ω(1), #vars: 0, input, output | 31 191ms, O(1), #vars: 0, input, output | 31 247ms, O(1), #vars: 0, input, output | 29 43ms, O(1), #vars: 0, input, output | 87ms, input, aspic |
T2/fir | 21 + 10 * free 866ms, INF, #vars: 1, input, output | 3774ms, input, output | 1452ms, input, output | 125ms, input, output | 233ms, input, aspic, output, errors |
T2/firewire | 1 1823ms, Ω(1), #vars: 0, input, output | 4162ms, input, output | 4089ms, input, output | 388ms, input, output | 561ms, input, aspic, output, errors |
T2/flipflop | INF 72ms, INF, #vars: 1, input, output | 1030ms, input, output | 211ms, input, output | 49ms, input, output | 76ms, input, aspic, output, errors |
T2/fourn | 8 + 2 * meter - B + A 7661ms, Ω(n), #vars: 3, input, output | 22123ms, input, output | 60001ms, input, output | 565ms, input, output | 2604ms, input, aspic |
T2/fourn.c.i.fourn.pl.t2.fixed nonlinear | 3 - B + A 40190ms, Ω(n), #vars: 2, input, output | A + B + 4 436ms, O(n), #vars: 2, input, output | 60001ms, input, output | 1526ms, input, output | Non-linear example not handled by prover. |
T2/fourn.c.i.fourn.pl.t2.nor.t2.rlgfixed | 8 + 2 * meter - B + A 7287ms, Ω(n), #vars: 3, input, output | 21568ms, input, output | 60001ms, input, output | 647ms, input, output | 3151ms, input, aspic |
T2/fuhs-inflasso | -1 / 2 + 1 / 2 * (-1 +... 231ms, Ω(n2), #vars: 1, input, output | C^2 + 5 * C + 7 122ms, O(n2), #vars: 1, input, output | max(1, max(0, min(C + ... 351ms, O(n2), #vars: 1, input, output | max(0, C + -1) + max(0... 71ms, O(n2), #vars: 1, input, output | 82ms, input, aspic |
T2/fun1 | INF 9709ms, INF, #vars: 1, input, output | 2943ms, input, output | 60001ms, input, output | 239ms, input, output | 623ms, input, aspic, output |
T2/fun10 | INF 3387ms, INF, #vars: 1, input, output | 60017ms, input | 60001ms, input, output | 334ms, input, output | 61ms, input, aspic, aspic (errors) |
T2/fun10b | INF 3236ms, INF, #vars: 1, input, output | 60016ms, input | 60001ms, input, output | 287ms, input, output | 73ms, input, aspic, aspic (errors) |
T2/fun11 | INF 133ms, INF, #vars: 1, input, output | 1343ms, input, output | 257ms, input, output | 47ms, input, output | 113ms, input, aspic, output, errors |
T2/fun1b | INF 10131ms, INF, #vars: 1, input, output | 3303ms, input, output | 60001ms, input, output | 241ms, input, output | 757ms, input, aspic, output |
T2/fun2 | 1 11986ms, Ω(1), #vars: 0, input, output | 111 * C + 111 * E + 11... 1448ms, O(n), #vars: 4, input, output | 60001ms, input, output | 209ms, input, output | 801ms, input, aspic, output |
T2/fun2b | 1 10013ms, Ω(1), #vars: 0, input, output | 2857ms, input, output | 60001ms, input, output | 222ms, input, output | 968ms, input, aspic, output |
T2/fun3 | 1 10929ms, Ω(1), #vars: 0, input, output | 111 * C + 111 * E + 11... 1554ms, O(n), #vars: 4, input, output | 60001ms, input, output | 214ms, input, output | 766ms, input, aspic, output |
T2/fun4 | 2 245ms, Ω(1), #vars: 0, input, output | 24 351ms, O(1), #vars: 0, input, output | max(1 / 2 * A + -1 * B... 304ms, O(n), #vars: 2, input, output | 100ms, input, output | 97ms, input, aspic, output, errors |
T2/fun4-alt | 2 178ms, Ω(1), #vars: 0, input, output | 24 203ms, O(1), #vars: 0, input, output | max(1 / 2 * A + -1 * B... 254ms, O(n), #vars: 2, input, output | 95ms, input, output | 101ms, input, aspic, output, errors |
T2/fun5 | 1 1098ms, Ω(1), #vars: 0, input, output | 13901ms, input, output | 46627ms, input, output | 979ms, input, output | 60001ms, input, aspic |
T2/fun6 | 4 + free 369ms, INF, #vars: 1, input, output | 19559ms, input, output | 262ms, input, output, errors | 85ms, input, output | 7937ms, input, aspic, output |
T2/fun7 | 1 1065ms, Ω(1), #vars: 0, input, output | 762ms, input, output | 3221ms, input, output | 309ms, input, output | 3645ms, input, aspic, output |
T2/fun8 | 1 2390ms, Ω(1), #vars: 0, input, output | 1068 1970ms, O(1), #vars: 0, input, output | 32 3571ms, O(1), #vars: 0, input, output | 247ms, input, output | 3557ms, input, aspic |
T2/fun9 | 1 5493ms, Ω(1), #vars: 0, input, output | 6356ms, input, output | 60006ms, input, output | 273ms, input, output | 1583ms, input, aspic, output, errors |
T2/graycode | 1 276ms, Ω(1), #vars: 0, input, output | 583643 9159ms, O(1), #vars: 0, input, output | 60005ms, input, output | 178 743ms, O(1), #vars: 0, input, output | 676ms, input, aspic, output |
T2/heidy1 | INF 32ms, INF, #vars: 1, input, output | 638ms, input, output | 180ms, input, output | 40ms, input, output | 68ms, input, aspic, output, errors |
T2/heidy10 | 1 + free 175ms, INF, #vars: 1, input, output | 2609ms, input, output | 249ms, input, output | 68ms, input, output | 182ms, input, aspic, output, errors |
T2/heidy2 | INF 56ms, INF, #vars: 1, input, output | 1142ms, input, output | 174ms, input, output | 48ms, input, output | 107ms, input, aspic, output, errors |
T2/heidy3 | INF 76ms, INF, #vars: 1, input, output | 354ms, input, output | 252ms, input, output | 52ms, input, output | 75ms, input, aspic, output, errors |
T2/heidy5 | 1 + B 62ms, Ω(n), #vars: 1, input, output | B + 3 104ms, O(n), #vars: 1, input, output | max(B + 2, 2) 180ms, O(n), #vars: 1, input, output | max(B, 0) 77ms, O(n), #vars: 1, input, output | 73ms, input, aspic, output, errors |
T2/heidy6 | INF 77ms, INF, #vars: 1, input, output | 528ms, input, output | 279ms, input, output | 83ms, input, output | 87ms, input, aspic, output, errors |
T2/heidy7 | 1 + B 192ms, Ω(n), #vars: 1, input, output | 2406ms, input, output | 262ms, input, output | 111ms, input, output | 103ms, input, aspic, output, errors |
T2/heidy7-simple | INF 66ms, INF, #vars: 1, input, output | 1227ms, input, output | 251ms, input, output | 55ms, input, output | 82ms, input, aspic, output, errors |
T2/heidy8 | 1 + C 194ms, Ω(n), #vars: 1, input, output | 4632ms, input, output | 358ms, input, output | 85ms, input, output | 96ms, input, aspic, output, errors |
T2/heidy9 | 1 + A 61ms, Ω(n), #vars: 1, input, output | A + 2 101ms, O(n), #vars: 1, input, output | max(A + 2, 2) 170ms, O(n), #vars: 1, input, output | max(A, 0) 57ms, O(n), #vars: 1, input, output | 88ms, input, aspic, output, errors |
T2/hongyi1 | 3 + 2 * C 9809ms, Ω(n), #vars: 1, input, output | 188 * C + 627 * D + 23... 23166ms, O(n), #vars: 3, input, output | 60001ms, input, output | 1282ms, input, output | 30706ms, input, aspic, aspic (errors) |
T2/hqr | 5 + 2 * B - Q 30737ms, Ω(n), #vars: 2, input, output | 60012ms, input | 60001ms, input, output | 362ms, input, output | 72ms, input, aspic, aspic (errors) |
T2/hqr.c.i.hqr.pl.t2.fixed nonlinear | 6 - Q 52954ms, Ω(n), #vars: 1, input, output | 60013ms, input | 60001ms, input, output | 694ms, input, output | Non-linear example not handled by prover. |
T2/hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed | 5 + 2 * B - Q 27704ms, Ω(n), #vars: 2, input, output | 60013ms, input | 60001ms, input, output | 413ms, input, output | 74ms, input, aspic, aspic (errors) |
T2/huh | 32 + free_24 206ms, INF, #vars: 1, input, output | 3908ms, input, output | 738ms, input, output | 56ms, input, output | 695ms, input, aspic |
T2/iecs | 1 57ms, Ω(1), #vars: 0, input, output | B + 1 231ms, O(n), #vars: 1, input, output | max(B + 1, 1) 173ms, O(n), #vars: 1, input, output | 67ms, input, output | 76ms, input, aspic |
T2/insertsort | INF 54ms, INF, #vars: 1, input, output | 4212ms, input, output | 266ms, input, output | 55ms, input, output | 109ms, input, aspic, output, errors |
T2/intSqRoot nonlinear | 1 118ms, Ω(1), #vars: 0, input, output | 1561ms, input, output | 224ms, input, output | 87ms, input, output | Non-linear example not handled by prover. |
T2/invgen | 1 75ms, Ω(1), #vars: 0, input, output | B + 2 100ms, O(n), #vars: 1, input, output | max(B + 2, 1) 200ms, O(n), #vars: 1, input, output | max(0, B + 1) 46ms, O(n), #vars: 1, input, output | 63ms, input, aspic |
T2/jacobi | 4 - C + A 614ms, Ω(n), #vars: 2, input, output | 225 * A + 218 * B + 7 ... 4389ms, O(n), #vars: 3, input, output | 60001ms, input, output | 928ms, input, output | 2373ms, input, aspic, output |
T2/jacobi.c.i.jacobi.pl.t2.fixed nonlinear | 4 - C + A 8557ms, Ω(n), #vars: 2, input, output | 225 * A + 218 * B + 7 ... 5433ms, O(n), #vars: 3, input, output | 60001ms, input, output | 873ms, input, output | Non-linear example not handled by prover. |
T2/jacobi.c.i.jacobi.pl.t2.nor.t2.rlgfixed | 4 - C + A 637ms, Ω(n), #vars: 2, input, output | 225 * A + 218 * B + 7 ... 4391ms, O(n), #vars: 3, input, output | 60001ms, input, output | 924ms, input, output | 2027ms, input, aspic, output |
T2/janne_complex | 1 1132ms, Ω(1), #vars: 0, input, output | 1550ms, input, output | 581ms, input, output | 465ms, input, output | 106ms, input, aspic, output, errors |
T2/jfdctint | 83 104ms, Ω(1), #vars: 0, input, output | 94 282ms, O(1), #vars: 0, input, output | 84 827ms, O(1), #vars: 0, input, output | 80 109ms, O(1), #vars: 0, input, output | 86 1119ms, O(1), #vars: 0, input, aspic, output |
T2/loop3 | 1 2671ms, Ω(1), #vars: 0, input, output | 1873991 47348ms, O(1), #vars: 0, input, output | 53078ms, input, output | 494ms, input, output | 999ms, input, aspic |
T2/loop_on_input | 1 124ms, Ω(1), #vars: 0, input, output | 10 308ms, O(1), #vars: 0, input, output | 6 178ms, O(1), #vars: 0, input, output | 54ms, input, output | 54ms, input, aspic |
T2/ludcmp | 3 - D + A 4625ms, Ω(n), #vars: 2, input, output | 932 * A + 926 * D + 4 ... 2544ms, O(n), #vars: 4, input, output | 60004ms, input, output | max(0, max(0, max(0, A... 691ms, O(n4), #vars: 2, input, output | 403ms, input, aspic, output |
T2/ludcmp.c.i.ludcmp.pl.t2.fixed nonlinear | 3 - D + A 4613ms, Ω(n), #vars: 2, input, output | 602 * A + 596 * D + 4 ... 2619ms, O(n), #vars: 4, input, output | 60002ms, input, output | max(0, max(0, max(0, A... 736ms, O(n4), #vars: 2, input, output | Non-linear example not handled by prover. |
T2/ludcmp.c.i.ludcmp.pl.t2.nor.t2.rlgfixed | 3 - D + A 4418ms, Ω(n), #vars: 2, input, output | 568 * A + 562 * D + 4 ... 2793ms, O(n), #vars: 4, input, output | 60004ms, input, output | max(0, max(0, max(0, A... 693ms, O(n4), #vars: 2, input, output | 436ms, input, aspic, output |
T2/magic | 2 + free_2 581ms, INF, #vars: 1, input, output | 60013ms, input | 60001ms, input, output | 372ms, input, output | 9946ms, input, aspic |
T2/matmul | 222 136ms, Ω(1), #vars: 0, input, output | 6567 388ms, O(1), #vars: 0, input, output | 223 338ms, O(1), #vars: 0, input, output | 190 83ms, O(1), #vars: 0, input, output | 91ms, input, aspic, output, errors |
T2/matmult | 9723 178ms, Ω(1), #vars: 0, input, output | 163873 790ms, O(1), #vars: 0, input, output | 9724 829ms, O(1), #vars: 0, input, output | 9280 140ms, O(1), #vars: 0, input, output | 298ms, input, aspic, output, errors |
T2/matrixsqrt | 30 177ms, Ω(1), #vars: 0, input, output | 524 2996ms, O(1), #vars: 0, input, output | 31 913ms, O(1), #vars: 0, input, output | 22 88ms, O(1), #vars: 0, input, output | 275ms, input, aspic, output, errors |
T2/mc91 | 1 + meter 308ms, INF, #vars: 1, input, output | 1870ms, input, output | 230ms, input, output | 93ms, input, output | 83ms, input, aspic, output, errors |
T2/mc91test | 1 + meter 699ms, INF, #vars: 1, input, output | 3935ms, input, output | 281ms, input, output | 336ms, input, output | 117ms, input, aspic, output, errors |
T2/minmax | 1 19ms, Ω(1), #vars: 0, input, output | 5 44ms, O(1), #vars: 0, input, output | 3 188ms, O(1), #vars: 0, input, output | 36ms, input | 5 139ms, O(1), #vars: 0, input, aspic, output |
T2/n-1 | INF 58ms, INF, #vars: 1, input, output | 1408ms, input, output | 244ms, input, output | 45ms, input, output | 144ms, input, aspic, output, errors |
T2/n-10 | INF 104ms, INF, #vars: 1, input, output | 158ms, input, output | 349ms, input, output | 56ms, input, output | 225ms, input, aspic, output, errors |
T2/n-12 | INF 160ms, INF, #vars: 1, input, output | 278ms, input, output | 224ms, input, output | 90ms, input, output | 89ms, input, aspic, output, errors |
T2/n-12a | INF 53ms, INF, #vars: 1, input, output | 128ms, input, output | 169ms, input, output | 39ms, input, output | 82ms, input, aspic, output, errors |
T2/n-13 | INF 57ms, INF, #vars: 1, input, output | 935ms, input, output | 173ms, input, output | 40ms, input, output | 83ms, input, aspic, output, errors |
T2/n-14 | INF 159ms, INF, #vars: 1, input, output | 281ms, input, output | 224ms, input, output | 290ms, input, output | 119ms, input, aspic, output, errors |
T2/n-15 | INF 76ms, INF, #vars: 1, input, output | 895ms, input, output | 212ms, input, output | 50ms, input, output | 54ms, input, aspic, output, errors |
T2/n-15a | INF 400ms, INF, #vars: 1, input, output | 288ms, input, output | 247ms, input, output | 154ms, input, output | 100ms, input, aspic, output, errors |
T2/n-16 | INF 80ms, INF, #vars: 1, input, output | 991ms, input, output | 208ms, input, output | 48ms, input, output | 64ms, input, aspic, output, errors |
T2/n-16a | 1 65ms, Ω(1), #vars: 0, input, output | 2428ms, input, output | 228ms, input, output | 56ms, input, output | 83ms, input, aspic |
T2/n-17 | INF 73ms, INF, #vars: 1, input, output | 937ms, input, output | 201ms, input, output | 63ms, input, output | 79ms, input, aspic, output, errors |
T2/n-18 | INF 52ms, INF, #vars: 1, input, output | 889ms, input, output | 170ms, input, output | 55ms, input, output | 73ms, input, aspic, output, errors |
T2/n-18a | 1 58ms, Ω(1), #vars: 0, input, output | 2472ms, input, output | 191ms, input, output | 63ms, input, output | 133ms, input, aspic |
T2/n-1c | INF 110ms, INF, #vars: 1, input, output | 158ms, input, output | 277ms, input, output | 67ms, input, output | 183ms, input, aspic, output, errors |
T2/n-1d | INF 192ms, INF, #vars: 1, input, output | 215ms, input, output | 234ms, input, output | 86ms, input, output | 102ms, input, aspic, output, errors |
T2/n-20 | INF 73ms, INF, #vars: 1, input, output | 184ms, input, output | 269ms, input, output | 43ms, input, output | 191ms, input, aspic, output, errors |
T2/n-21 | INF 70ms, INF, #vars: 1, input, output | 1441ms, input, output | 208ms, input, output | 53ms, input, output | 88ms, input, aspic, output, errors |
T2/n-3 | INF 96ms, INF, #vars: 1, input, output | 1277ms, input, output | 211ms, input, output | 64ms, input, output | 79ms, input, aspic, output, errors |
T2/n-32 | 1 72ms, Ω(1), #vars: 0, input, output | 1143ms, input, output | 171ms, input, output | 50ms, input, output | 83ms, input, aspic, output, errors |
T2/n-33 | 1 307ms, Ω(1), #vars: 0, input, output | 366ms, input, output | 312ms, input, output | 559ms, input, output | 136ms, input, aspic, output, errors |
T2/n-36 | INF 250ms, INF, #vars: 1, input, output | 349ms, input, output | 1002ms, input, output | 348ms, input, output | 1386ms, input, aspic, output, errors |
T2/n-37 | INF 28ms, INF, #vars: 1, input, output | 1001ms, input, output | 210ms, input, output | 42ms, input, output | 68ms, input, aspic, output, errors |
T2/n-3a | INF 540ms, INF, #vars: 1, input, output | 404ms, input, output | 465ms, input, output | 332ms, input, output | 136ms, input, aspic, output, errors |
T2/n-4 | 1 - C + A 351ms, Ω(n), #vars: 2, input, output | 6727ms, input, output | 147ms, input, output, errors | 39ms, input, output | 212ms, input, aspic, output, errors |
T2/n-40 | INF 2017ms, INF, #vars: 1, input, output | 2323ms, input, output | 586ms, input, output | 169ms, input, output | 178ms, input, aspic, output, errors |
T2/n-46 | INF 101ms, INF, #vars: 1, input, output | 2191ms, input, output | 206ms, input, output | 61ms, input, output | 88ms, input, aspic, output, errors |
T2/n-48 | 1 65ms, Ω(1), #vars: 0, input, output | 3052ms, input, output | 220ms, input, output | 53ms, input, output | 111ms, input, aspic |
T2/n-5 | 1 + B - A 208ms, Ω(n), #vars: 2, input, output | 2711ms, input, output | 989ms, input, output | 149ms, input, output | 366ms, input, aspic, output, errors |
T2/n-6 | INF 179ms, INF, #vars: 1, input, output | 236ms, input, output | 233ms, input, output | 141ms, input, output | 89ms, input, aspic, output, errors |
T2/n-6a | INF 112ms, INF, #vars: 1, input, output | 281ms, input, output | 224ms, input, output | 55ms, input, output | 91ms, input, aspic, output, errors |
T2/n-7 | INF 76ms, INF, #vars: 1, input, output | 1537ms, input, output | 193ms, input, output | 151ms, input, output | 81ms, input, aspic, output, errors |
T2/n-8 | INF 111ms, INF, #vars: 1, input, output | 148ms, input, output | 368ms, input, output | 67ms, input, output | 166ms, input, aspic, output, errors |
T2/n-8a | INF 54ms, INF, #vars: 1, input, output | 1005ms, input, output | 196ms, input, output | 50ms, input, output | 83ms, input, aspic, output, errors |
T2/n-9 | 1 119ms, Ω(1), #vars: 0, input, output | 269ms, input, output | 277ms, input, output | 76ms, input, output | 137ms, input, aspic, output, errors |
T2/n_firewire_instrumented-PP | 1 4091ms, Ω(1), #vars: 0, input, output | 14958ms, input, output | 2347ms, input, output | 487ms, input, output | 16895ms, input, aspic, output, errors |
T2/nakata | 1 + 2 * free_1 5463ms, INF, #vars: 1, input, output | 23182ms, input, output | 60001ms, input, output | 622ms, input, output | 39863ms, input, aspic, aspic (errors) |
T2/nakata_withassume | 1 + 2 * free_1 7463ms, INF, #vars: 1, input, output | 50053ms, input, output | 60001ms, input, output | 228ms, input, output | 60002ms, input, aspic |
T2/ndes | 1 9087ms, Ω(1), #vars: 0, input, output | 59 * W1 + 59 * E2 + 73... 13535ms, O(n), #vars: 2, input, output | 60001ms, input, output | 1373ms, input, output | 77ms, input, aspic, aspic (errors) |
T2/neg-1394complete-fail | INF 1702ms, INF, #vars: 1, input, output | 5965ms, input, output | 55476ms, input, output | 1110ms, input, output | 67ms, input, aspic, aspic (errors) |
T2/neg-1394complete-succeed | INF 1689ms, INF, #vars: 1, input, output | 4954ms, input, output | 59316ms, input, output | 358ms, input, output | 72ms, input, aspic, aspic (errors) |
T2/neg-e-1394complete-fail | INF 1690ms, INF, #vars: 1, input, output | 5019ms, input, output | 50994ms, input, output | 333ms, input, output | 71ms, input, aspic, aspic (errors) |
T2/neg-e-1394complete-succeed | INF 1694ms, INF, #vars: 1, input, output | 4958ms, input, output | 55037ms, input, output | 339ms, input, output | 83ms, input, aspic, aspic (errors) |
T2/neg-e-acqrel-fail | INF 80ms, INF, #vars: 1, input, output | 300ms, input, output | 504ms, input, output | 55ms, input, output | 102ms, input, aspic, output, errors |
T2/neg-e-acqrel-succeed | INF 83ms, INF, #vars: 1, input, output | 678ms, input, output | 287ms, input, output | 67ms, input, output | 96ms, input, aspic, output, errors |
T2/neg-e-pgarch-fail | INF 168ms, INF, #vars: 1, input, output | 361ms, input, output | 386ms, input, output | 47ms, input, output | 212ms, input, aspic, output, errors |
T2/neg-e-pgarch-succeed | INF 165ms, INF, #vars: 1, input, output | 424ms, input, output | 418ms, input, output | 40ms, input, output | 129ms, input, aspic, output, errors |
T2/neg-e-popl07-succeed | INF 263ms, INF, #vars: 1, input, output | 1026ms, input, output | 2890ms, input, output | 487ms, input, output | 624ms, input, aspic, output, errors |
T2/neg-pgarch-succeed | INF 181ms, INF, #vars: 1, input, output | 360ms, input, output | 492ms, input, output | 43ms, input, output | 170ms, input, aspic, output, errors |
T2/neg-popl07-fail | INF 168ms, INF, #vars: 1, input, output | 474ms, input, output | 2498ms, input, output | 464ms, input, output | 607ms, input, aspic, output, errors |
T2/neg-popl07-succeed | INF 206ms, INF, #vars: 1, input, output | 742ms, input, output | 2717ms, input, output | 455ms, input, output | 622ms, input, aspic, output, errors |
T2/neg-smagilla-fail | INF 188ms, INF, #vars: 1, input, output | 977ms, input, output | 427ms, input, output | 224ms, input, output | 113ms, input, aspic, output, errors |
T2/neg-smagilla-succeed | INF 189ms, INF, #vars: 1, input, output | 970ms, input, output | 513ms, input, output | 212ms, input, output | 105ms, input, aspic, output, errors |
T2/nested | 1 + 3 * free_3 108ms, INF, #vars: 1, input, output | 1381ms, input, output | 278ms, input, output | 101ms, input, output | 123ms, input, aspic, output, errors |
T2/nested2 | 5001 + 5001 * meter_1 163ms, INF, #vars: 1, input, output | 1394ms, input, output | 253ms, input, output | 89ms, input, output | 92ms, input, aspic, output, errors |
T2/new_ex | 2 + free 562ms, INF, #vars: 1, input, output | 2714ms, input, output | 572ms, input, output | 147ms, input, output | 105ms, input, aspic, output, errors |
T2/non_term | 1 72ms, Ω(1), #vars: 0, input, output | 2712ms, input, output | 177ms, input, output | 45ms, input, output | 68ms, input, aspic |
T2/ns | 936 131ms, Ω(1), #vars: 0, input, output | 15265 459ms, O(1), #vars: 0, input, output | 937 617ms, O(1), #vars: 0, input, output | 810 179ms, O(1), #vars: 0, input, output | 155ms, input, aspic, output, errors |
T2/oct_vs_subpoly | INF 32ms, INF, #vars: 1, input, output | 719ms, input, output | 216ms, input, output | 55ms, input, output | 83ms, input, aspic, output, errors |
T2/p-1 | INF 57ms, INF, #vars: 1, input, output | 1249ms, input, output | 199ms, input, output | 39ms, input, output | 105ms, input, aspic, output, errors |
T2/p-10 | INF 52ms, INF, #vars: 1, input, output | 1342ms, input, output | 301ms, input, output | 47ms, input, output | 117ms, input, aspic, output, errors |
T2/p-12 | 2 + A 61ms, Ω(n), #vars: 1, input, output | A + 3 93ms, O(n), #vars: 1, input, output | max(A + 3, 2) 244ms, O(n), #vars: 1, input, output | max(0, A + 1) 56ms, O(n), #vars: 1, input, output | 90ms, input, aspic, output, errors |
T2/p-13 | 1 48ms, Ω(1), #vars: 0, input, output | 2 58ms, O(1), #vars: 0, input, output | 1 147ms, O(1), #vars: 0, input, output | 34ms, input | 3 66ms, O(1), #vars: 0, input, aspic, output |
T2/p-14 | A 60ms, Ω(n), #vars: 1, input, output | A + 2 91ms, O(n), #vars: 1, input, output | max(A + 1, 2) 166ms, O(n), #vars: 1, input, output | max(0, A + -1) 42ms, O(n), #vars: 1, input, output | 8156ms, input, aspic, output, errors |
T2/p-15 | 1 + A 58ms, Ω(n), #vars: 1, input, output | A + 2 89ms, O(n), #vars: 1, input, output | max(A + 2, 2) 348ms, O(n), #vars: 1, input, output | max(A, 0) 62ms, O(n), #vars: 1, input, output | 72ms, input, aspic, output, errors |
T2/p-16 | 1 + A 61ms, Ω(n), #vars: 1, input, output | A + 2 104ms, O(n), #vars: 1, input, output | max(A + 2, 2) 167ms, O(n), #vars: 1, input, output | max(A, 0) 49ms, O(n), #vars: 1, input, output | 60ms, input, aspic, output, errors |
T2/p-18 | 1 + A 56ms, Ω(n), #vars: 1, input, output | A + 2 96ms, O(n), #vars: 1, input, output | max(A + 2, 2) 183ms, O(n), #vars: 1, input, output | max(A, 0) 48ms, O(n), #vars: 1, input, output | 64ms, input, aspic, output, errors |
T2/p-19 | INF 53ms, INF, #vars: 1, input, output | 1098ms, input, output | 250ms, input, output | 46ms, input, output | 107ms, input, aspic, output, errors |
T2/p-19a | INF 55ms, INF, #vars: 1, input, output | 1251ms, input, output | 239ms, input, output | 49ms, input, output | 135ms, input, aspic, output, errors |
T2/p-1a | INF 53ms, INF, #vars: 1, input, output | 1350ms, input, output | 231ms, input, output | 54ms, input, output | 112ms, input, aspic, output, errors |
T2/p-1b | 1 + B - A 78ms, Ω(n), #vars: 2, input, output | A + B + 2 74ms, O(n), #vars: 2, input, output | max(-1 * A + B + 2, 2) 184ms, O(n), #vars: 2, input, output | max(0, B - A) 42ms, O(n), #vars: 2, input, output | 92ms, input, aspic, output, errors |
T2/p-1c | INF 64ms, INF, #vars: 1, input, output | 1304ms, input, output | 323ms, input, output | 49ms, input, output | 133ms, input, aspic, output, errors |
T2/p-1d | 1 + B - A 257ms, Ω(n), #vars: 2, input, output | 3 * A + 3 * B + 2 171ms, O(n), #vars: 2, input, output | max(-1 * A + B + 2, 2) 215ms, O(n), #vars: 2, input, output | max(0, max(0, B - A) *... 124ms, O(n2), #vars: 2, input, output | 76ms, input, aspic, output, errors |
T2/p-20 | INF 73ms, INF, #vars: 1, input, output | 146ms, input, output | 234ms, input, output | 50ms, input, output | 200ms, input, aspic, output, errors |
T2/p-21 | -27 + A 91ms, Ω(n), #vars: 1, input, output | A + 64 * B + 1314 172ms, O(n), #vars: 2, input, output | max(A + 2 * B + -68, A... 249ms, O(n), #vars: 2, input, output | max(0, B + -20) + max(... 94ms, O(n), #vars: 1, input, output | 84ms, input, aspic, output, errors |
T2/p-22 | A 62ms, Ω(n), #vars: 1, input, output | A + 3 131ms, O(n), #vars: 1, input, output | max(A + 1, 2) 168ms, O(n), #vars: 1, input, output | max(0, A + -1) 47ms, O(n), #vars: 1, input, output | max(3, A__o' + 1 + 1 + 1) 67ms, O(n), #vars: 1, input, aspic, output |
T2/p-3 | 1 + B - A 142ms, Ω(n), #vars: 2, input, output | A + B + 3 120ms, O(n), #vars: 2, input, output | max(-1 * A + B + 3, 3) 206ms, O(n), #vars: 2, input, output | 94ms, input, output | 93ms, input, aspic, output, errors |
T2/p-32 | 1 67ms, Ω(1), #vars: 0, input, output | 1149ms, input, output | 183ms, input, output | 50ms, input, output | 76ms, input, aspic, output, errors |
T2/p-33 | 1 141ms, Ω(1), #vars: 0, input, output | 248ms, input, output | 204ms, input, output | 112ms, input, output | 109ms, input, aspic, output, errors |
T2/p-34 | INF 155ms, INF, #vars: 1, input, output | 225ms, input, output | 1251ms, input, output | 204ms, input, output | 1870ms, input, aspic, output, errors |
T2/p-36 | INF 128ms, INF, #vars: 1, input, output | 1011ms, input, output | 526ms, input, output | 53ms, input, output | 568ms, input, aspic, output, errors |
T2/p-37 | 1 81ms, Ω(1), #vars: 0, input, output | 8 153ms, O(1), #vars: 0, input, output | 6 249ms, O(1), #vars: 0, input, output | 4 57ms, O(1), #vars: 0, input, output | 86ms, input, aspic, output |
T2/p-4 | 1 - B + A 171ms, Ω(n), #vars: 2, input, output | 107 * A + 108 * B + 3 ... 133ms, O(n2), #vars: 3, input, output | max(2 * A + -1 * B + -... 302ms, O(n), #vars: 3, input, output | max(0, max(0, B + -1 +... 82ms, O(n2), #vars: 2, input, output | 105ms, input, aspic, output, errors |
T2/p-40 | 500 - free_3 68ms, INF, #vars: 1, input, output | 918ms, input, output | 275ms, input, output | 66ms, input, output | 88ms, input, aspic, output, errors |
T2/p-41 | 1 17ms, Ω(1), #vars: 0, input, output | 1 14ms, O(1), #vars: 0, input, output | 1 149ms, O(1), #vars: 0, input, output | 35ms, input | 3 76ms, O(1), #vars: 0, input, aspic, output |
T2/p-42 | 3 - A 129ms, Ω(n), #vars: 1, input, output | A + B + 7 208ms, O(n), #vars: 2, input, output | max(-1 * A + -1 * B + ... 242ms, O(n), #vars: 2, input, output | max(0, 2 - A) + max(0,... 61ms, O(n), #vars: 1, input, output | 83ms, input, aspic, output, errors |
T2/p-43 | 1 351ms, Ω(1), #vars: 0, input, output | 536ms, input, output | 252ms, input, output | 72ms, input, output | 145ms, input, aspic, output, errors |
T2/p-43-terminate | 1 4431ms, Ω(1), #vars: 0, input, output | 6310ms, input, output | 201ms, input, output, errors | 73ms, input, output | 559ms, input, aspic, output |
T2/p-44 | 1 113ms, Ω(1), #vars: 0, input, output | A + 3 155ms, O(n), #vars: 1, input, output | max(A + 2, 2) 377ms, O(n), #vars: 1, input, output | max(A, 0) 55ms, O(n), #vars: 1, input, output | 88ms, input, aspic, output, errors |
T2/p-45 | 1 + B 274ms, Ω(n), #vars: 1, input, output | B + 3 201ms, O(n), #vars: 1, input, output | max(B + 2, 2, A + 2) 303ms, O(n), #vars: 2, input, output | max(B, 0) 54ms, O(n), #vars: 1, input, output | 109ms, input, aspic, output, errors |
T2/p-46 | 1 1459ms, Ω(1), #vars: 0, input, output | 451ms, input, output | 306ms, input, output | 174ms, input, output | 119ms, input, aspic |
T2/p-49 | 2 + A 56ms, Ω(n), #vars: 1, input, output | A + 3 92ms, O(n), #vars: 1, input, output | max(A + 3, 2) 170ms, O(n), #vars: 1, input, output | max(0, A + 1) 60ms, O(n), #vars: 1, input, output | 110ms, input, aspic, output, errors |
T2/p-5 | 1 + B - A 199ms, Ω(n), #vars: 2, input, output | 2602ms, input, output | 837ms, input, output | 170ms, input, output | 381ms, input, aspic, output, errors |
T2/p-52 | INF 52ms, INF, #vars: 1, input, output | 1387ms, input, output | 220ms, input, output | 53ms, input, output | 98ms, input, aspic, output, errors |
T2/p-53 | 1 43ms, Ω(1), #vars: 0, input, output | 2 32ms, O(1), #vars: 0, input, output | 1 149ms, O(1), #vars: 0, input, output | 53ms, input | 3 67ms, O(1), #vars: 0, input, aspic, output |
T2/p-55 | 1 - A 470ms, Ω(n), #vars: 1, input, output | 202 * B + 2 * A + 2 * ... 314ms, O(n2), #vars: 2, input, output | max(-1 * A + 102, 2, m... 297ms, O(n), #vars: 2, input, output | max(0, 1 + max(0, -1 -... 160ms, O(n), #vars: 1, input, output | 83ms, input, aspic |
T2/p-56 | 0 - D 329ms, Ω(n), #vars: 1, input, output | 2 * D + 5 239ms, O(n), #vars: 1, input, output | max(-1 * D + 1, 2) 404ms, O(n), #vars: 1, input, output | max(0, -1 - D) 87ms, O(n), #vars: 1, input, output | 97ms, input, aspic, output, errors |
T2/p-58 | 1 53ms, Ω(1), #vars: 0, input, output | 3 71ms, O(1), #vars: 0, input, output | 1 155ms, O(1), #vars: 0, input, output | 40ms, input, output | 86ms, input, aspic, output |
T2/p-6 | 1 + B - A 259ms, Ω(n), #vars: 2, input, output | 3 * A + 3 * B + 2 171ms, O(n), #vars: 2, input, output | max(-1 * A + B + 2, 2) 259ms, O(n), #vars: 2, input, output | max(0, max(0, B - A) *... 147ms, O(n2), #vars: 2, input, output | 87ms, input, aspic, output, errors |
T2/p-60 | 101 86ms, Ω(1), #vars: 0, input, output | 103 115ms, O(1), #vars: 0, input, output | 102 194ms, O(1), #vars: 0, input, output | 100 47ms, O(1), #vars: 0, input, output | max(104, 3) 92ms, O(1), #vars: 0, input, aspic, output |
T2/p-61 | 901 73ms, Ω(1), #vars: 0, input, output | 1003 122ms, O(1), #vars: 0, input, output | 902 200ms, O(1), #vars: 0, input, output | 900 44ms, O(1), #vars: 0, input, output | 904 100ms, O(1), #vars: 0, input, aspic, output |
T2/p-63 | 1 64ms, Ω(1), #vars: 0, input, output | A + 4 313ms, O(n), #vars: 1, input, output | max(A + 3, 2) 231ms, O(n), #vars: 1, input, output | 45ms, input, output | 78ms, input, aspic |
T2/p-7 | 1 + meter 83ms, Ω(n), #vars: 1, input, output | B + C + 3 111ms, O(n), #vars: 2, input, output | max(-1 / 2 * B + 1 / 2... 212ms, O(n), #vars: 2, input, output | max(0, C + -1 + 0 - B) 130ms, O(n), #vars: 2, input, output | 86ms, input, aspic, output, errors |
T2/p-7b | 1 + meter 97ms, Ω(n), #vars: 1, input, output | B + C + 4 107ms, O(n), #vars: 2, input, output | max(-1 / 2 * B + 1 / 2... 270ms, O(n), #vars: 2, input, output | max(0, C + -1 + 0 - B) 105ms, O(n), #vars: 2, input, output | 77ms, input, aspic, output, errors |
T2/p-8 | INF 51ms, INF, #vars: 1, input, output | 1069ms, input, output | 200ms, input, output | 39ms, input, output | 72ms, input, aspic, output, errors |
T2/p-9 | INF 52ms, INF, #vars: 1, input, output | 1063ms, input, output | 201ms, input, output | 50ms, input, output | 108ms, input, aspic, output, errors |
T2/pearl-necklace | 4 - B + 4 * A 154ms, Ω(n), #vars: 2, input, output | 157 * A + 145 * B + 29... 363ms, O(n), #vars: 2, input, output | max(4 * A + -1 * B + 4... 509ms, O(n), #vars: 2, input, output | max(0, max(B, 0) + max... 65ms, O(n), #vars: 2, input, output | 102ms, input, aspic, output, errors |
T2/pentagon | 1 117ms, Ω(1), #vars: 0, input, output | 1040ms, input, output | 392ms, input, output | 553ms, input, output | 242ms, input, aspic, output, errors |
T2/pgarch | 60013ms, input, output | 41916ms, input, output | 60001ms, input | 11949ms, input, output | 161ms, input, aspic, aspic (errors) |
T2/pldi | -1 / 2 - 1 / 2 * (-1 +... 392ms, Ω(n2), #vars: 1, input, output | 12 * B + 8 * B^2 + 5 630ms, O(n2), #vars: 1, input, output | max(4, (B + 1) * (B + ... 323ms, O(n2), #vars: 1, input, output | max(B, 0) + max(0, max... 208ms, O(n3), #vars: 1, input, output | 82ms, input, aspic, output, errors |
T2/polling | INF 636ms, INF, #vars: 1, input, output | 14470ms, input, output | 60001ms, input, output | 395ms, input, output | 5081ms, input, aspic |
T2/polling.bug | INF 1032ms, INF, #vars: 1, input, output | 15900ms, input, output | 60001ms, input, output | 551ms, input, output | 5888ms, input, aspic |
T2/polyrank1 | 1 59ms, Ω(1), #vars: 0, input, output | 2609ms, input, output | 179ms, input, output | 52ms, input, output | 81ms, input, aspic |
T2/polyrank2 | 1 57ms, Ω(1), #vars: 0, input, output | 5291ms, input, output | 259ms, input, output | 46ms, input, output | 75ms, input, aspic |
T2/polyrank3 | 1 78ms, Ω(1), #vars: 0, input, output | 5884ms, input, output | 198ms, input, output | 60ms, input, output | 92ms, input, aspic |
T2/polyrank4 | 1 73ms, Ω(1), #vars: 0, input, output | 10955ms, input, output | 198ms, input, output | 50ms, input, output | 65ms, input, aspic |
T2/polyrank5 | 1 + A 95ms, Ω(n), #vars: 1, input, output | 6397ms, input, output | 209ms, input, output | 60ms, input, output | 81ms, input, aspic |
T2/polyrank6 | 1 + A 175ms, Ω(n), #vars: 1, input, output | 5327ms, input, output | 215ms, input, output | 133ms, input, output | 67ms, input, aspic |
T2/polyrank7 | INF 47ms, INF, #vars: 1, input, output | 5887ms, input, output | 190ms, input, output | 54ms, input, output | 85ms, input, aspic |
T2/popl07-fail | INF 168ms, INF, #vars: 1, input, output | 466ms, input, output | 1712ms, input, output | 498ms, input, output | 538ms, input, aspic, output, errors |
T2/popl07-succeed | INF 181ms, INF, #vars: 1, input, output | 488ms, input, output | 2135ms, input, output | 470ms, input, output | 531ms, input, aspic, output, errors |
T2/print | 1 + Q + free_199 10296ms, INF, #vars: 2, input, output | 13373ms, input, output | 13921ms, input, output | 1442ms, input, output | 74ms, input, aspic, aspic (errors) |
T2/qrdcmp | 4 - D + A 607ms, Ω(n), #vars: 2, input, output | 162 * A + 12 * K + 5 *... 669ms, O(n), #vars: 4, input, output | 11707ms, input, output | max(0, A + 1 + 0 - K) ... 785ms, O(n), #vars: 2, input, output | 565ms, input, aspic |
T2/qrdcmp.c.i.qrdcmp.pl.t2.fixed nonlinear | 4 - D + A 914ms, Ω(n), #vars: 2, input, output | 162 * A + 12 * K + 5 *... 867ms, O(n), #vars: 4, input, output | 10193ms, input, output | max(0, A + 1 + 0 - K) ... 717ms, O(n), #vars: 2, input, output | Non-linear example not handled by prover. |
T2/qrdcmp.c.i.qrdcmp.pl.t2.nor.t2.rlgfixed | 4 - D + A 587ms, Ω(n), #vars: 2, input, output | 162 * A + 12 * K + 5 *... 692ms, O(n), #vars: 4, input, output | 11309ms, input, output | max(0, A + 1 + 0 - K) ... 716ms, O(n), #vars: 2, input, output | 692ms, input, aspic |
T2/queens | 1 2308ms, Ω(1), #vars: 0, input, output | 1157351968 5350ms, O(1), #vars: 0, input, output | 60001ms, input, output | 288 924ms, O(1), #vars: 0, input, output | 731ms, input, aspic, output |
T2/queue_1 | 1 120ms, Ω(1), #vars: 0, input, output | 17 424ms, O(1), #vars: 0, input, output | 7 227ms, O(1), #vars: 0, input, output | 2 72ms, O(1), #vars: 0, input, output | 9 124ms, O(1), #vars: 0, input, aspic, output |
T2/queue_10 | 1 116ms, Ω(1), #vars: 0, input, output | 276 453ms, O(1), #vars: 0, input, output | 43 236ms, O(1), #vars: 0, input, output | 20 66ms, O(1), #vars: 0, input, output | 45 155ms, O(1), #vars: 0, input, aspic, output |
T2/queue_100 | 1 122ms, Ω(1), #vars: 0, input, output | 2886 463ms, O(1), #vars: 0, input, output | 403 244ms, O(1), #vars: 0, input, output | 200 68ms, O(1), #vars: 0, input, output | 405 122ms, O(1), #vars: 0, input, aspic, output |
T2/queue_1000 | 1 119ms, Ω(1), #vars: 0, input, output | 28986 417ms, O(1), #vars: 0, input, output | 4003 232ms, O(1), #vars: 0, input, output | 2000 70ms, O(1), #vars: 0, input, output | 4005 129ms, O(1), #vars: 0, input, aspic, output |
T2/randomwalk | 1 2374ms, Ω(1), #vars: 0, input, output | 4892ms, input, output | 548ms, input, output | 228ms, input, output | 130ms, input, aspic, output, errors |
T2/randomwalk_withassume | 1 2937ms, Ω(1), #vars: 0, input, output | 5188ms, input, output | 1117ms, input, output | 134ms, input, output | 1 177ms, O(1), #vars: 0, input, aspic, output, errors |
T2/refine_disj_problem | INF 109ms, INF, #vars: 1, input, output | 1644ms, input, output | 196ms, input, output | 74ms, input, output | 82ms, input, aspic |
T2/rev_nt2 | INF 499ms, INF, #vars: 1, input, output | 1311ms, input, output | 4039ms, input, output | 167ms, input, output | 2288ms, input, aspic, output |
T2/rev_nt3 | INF 525ms, INF, #vars: 1, input, output | 1410ms, input, output | 3185ms, input, output | 197ms, input, output | 2348ms, input, aspic, output |
T2/rev_nt4 | 1 38ms, Ω(1), #vars: 0, input, output | 2 18ms, O(1), #vars: 0, input, output | 1 159ms, O(1), #vars: 0, input, output | 33ms, input | 79ms, input, aspic, output |
T2/reverse | 1 + free_347 + S 15315ms, INF, #vars: 2, input, output | 9800ms, input, output | 31045ms, input, output | 60001ms, input, output | 104ms, input, aspic, aspic (errors) |
T2/reverse_div4 | INF 890ms, INF, #vars: 1, input, output | 738ms, input, output | 3764ms, input, output | 112ms, input, output | 64ms, input, aspic, aspic (errors) |
T2/reverse_seg_cyclic | 1 + N + E1 11072ms, Ω(n), #vars: 2, input, output | 16 * J + 16 * K + 16 *... 6952ms, O(n), #vars: 6, input, output | max(N, 2) 19807ms, O(n), #vars: 1, input, output | 42934ms, input, output | 71ms, input, aspic, aspic (errors) |
T2/rewrite | INF 27ms, INF, #vars: 1, input, output | 533ms, input, output | 251ms, input, output | 43ms, input, output | 79ms, input, aspic, output, errors |
T2/rlft3 | 6 - 2 * K + 2 * J 5650ms, Ω(n), #vars: 2, input, output | 24 * H + 24 * I + 4 * ... 3119ms, O(n), #vars: 7, input, output | 60001ms, input, output | 1267ms, input, output | 2316ms, input, aspic, output |
T2/rlft3.c.i.rlft3.pl.t2.fixed nonlinear | 5 - K + J 3994ms, Ω(n), #vars: 2, input, output | 52 * H + 52 * I + 3 * ... 3073ms, O(n), #vars: 7, input, output | 60001ms, input, output | 1482ms, input, output | Non-linear example not handled by prover. |
T2/s1-saved | 1 + H + free_212 8377ms, INF, #vars: 2, input, output | 10711ms, input, output | 7666ms, input, output | 1335ms, input, output | 69ms, input, aspic, aspic (errors) |
T2/s3-work | 2 + B 52146ms, Ω(n), #vars: 1, input, output | 60025ms, input | 60001ms, input, output | 60001ms, input, output | 109ms, input, aspic, aspic (errors) |
T2/sas1 | 1 + B 386ms, Ω(n), #vars: 1, input, output | 19 * B + 7 819ms, O(n), #vars: 1, input, output | max(4 * B + 4, B + 7, 5) 513ms, O(n), #vars: 1, input, output | max(0, -2 + max(B, 0))... 154ms, O(n), #vars: 1, input, output | 118ms, input, aspic, output, errors |
T2/sas2 | 1 1183ms, Ω(1), #vars: 0, input, output | 6264ms, input, output | max(C + 11, -1 * C + 2... 3240ms, O(n), #vars: 1, input, output | 142ms, input, output | 390ms, input, aspic, output, errors |
T2/select | 1 333ms, Ω(1), #vars: 0, input, output | 16811ms, input, output | 19915ms, input, output | 1275ms, input, output | 790ms, input, aspic, output, errors |
T2/selectSort | 1 / 2 - 1 / 2 * (-1 + ... 265ms, Ω(n2), #vars: 1, input, output | 23 * C + 12 * C^2 + 4 1293ms, O(n2), #vars: 1, input, output | max(5, (C + 1) * (C + ... 756ms, O(n2), #vars: 1, input, output | max(C, 0) + max(0, C +... 71ms, O(n2), #vars: 1, input, output | 184ms, input, aspic, output, errors |
T2/send-more-money | 1 125ms, Ω(1), #vars: 0, input, output | 129 2142ms, O(1), #vars: 0, input, output | 60001ms, input, output | 103ms, input | 60001ms, input, aspic |
T2/seq | 2 + A 59ms, Ω(n), #vars: 1, input, output | A + 2 77ms, O(n), #vars: 1, input, output | max(A + 2, 1) 313ms, O(n), #vars: 1, input, output | max(0, A + 1) 52ms, O(n), #vars: 1, input, output | 87ms, input, aspic, output, errors |
T2/seq2 | 1 + A 59ms, Ω(n), #vars: 1, input, output | A + 1 78ms, O(n), #vars: 1, input, output | max(A + 1, 1) 168ms, O(n), #vars: 1, input, output | max(A, 0) 44ms, O(n), #vars: 1, input, output | 1 + 1 + A__o' + 1 79ms, O(n), #vars: 1, input, aspic, output |
T2/sequential_swap | 1 43ms, Ω(1), #vars: 0, input, output | 2 42ms, O(1), #vars: 0, input, output | 1 177ms, O(1), #vars: 0, input, output | 43ms, input | 3 98ms, O(1), #vars: 0, input, aspic, output |
T2/simple | INF 67ms, INF, #vars: 1, input, output | 1821ms, input, output | 171ms, input, output | 55ms, input, output | 72ms, input, aspic, output, errors |
T2/simpleWhile | 1 + C 113ms, Ω(n), #vars: 1, input, output | 2 * C + 7 190ms, O(n), #vars: 1, input, output | max(C + 3, 3) 376ms, O(n), #vars: 1, input, output | max(C, 0) + max(C, 0) ... 55ms, O(n), #vars: 1, input, output | 107ms, input, aspic, output, errors |
T2/simple_array_inversion | 3 56ms, Ω(1), #vars: 0, input, output | 5 84ms, O(1), #vars: 0, input, output | 4 214ms, O(1), #vars: 0, input, output | 2 48ms, O(1), #vars: 0, input, output | 6 92ms, O(1), #vars: 0, input, aspic, output |
T2/simple_control_on_input | 1 64ms, Ω(1), #vars: 0, input, output | 22 91ms, O(1), #vars: 0, input, output | 21 161ms, O(1), #vars: 0, input, output | 55ms, input, output | max(23, 3) 92ms, O(1), #vars: 0, input, aspic, output |
T2/simple_double_free | 1 16ms, Ω(1), #vars: 0, input, output | 1 21ms, O(1), #vars: 0, input, output | 1 140ms, O(1), #vars: 0, input, output | 42ms, input | 3 57ms, O(1), #vars: 0, input, aspic, output |
T2/simple_fail | 1 19ms, Ω(1), #vars: 0, input, output | 1 16ms, O(1), #vars: 0, input, output | 1 221ms, O(1), #vars: 0, input, output | 46ms, input | 3 81ms, O(1), #vars: 0, input, aspic, output |
T2/simple_pre | 1 19ms, Ω(1), #vars: 0, input, output | 1 16ms, O(1), #vars: 0, input, output | 1 162ms, O(1), #vars: 0, input, output | 46ms, input | 3 85ms, O(1), #vars: 0, input, aspic, output |
T2/simple_pre1 | 1 21ms, Ω(1), #vars: 0, input, output | 1 20ms, O(1), #vars: 0, input, output | 1 174ms, O(1), #vars: 0, input, output | 42ms, input | 3 85ms, O(1), #vars: 0, input, aspic, output |
T2/simple_pre2 | 1 17ms, Ω(1), #vars: 0, input, output | 1 20ms, O(1), #vars: 0, input, output | 1 142ms, O(1), #vars: 0, input, output | 35ms, input | 3 78ms, O(1), #vars: 0, input, aspic, output |
T2/simple_pre3 | 1 18ms, Ω(1), #vars: 0, input, output | 4 25ms, O(1), #vars: 0, input, output | 1 144ms, O(1), #vars: 0, input, output | 35ms, input | 90ms, input, aspic, output |
T2/simple_swap_call | 1 43ms, Ω(1), #vars: 0, input, output | 2 32ms, O(1), #vars: 0, input, output | 1 153ms, O(1), #vars: 0, input, output | 36ms, input | 3 78ms, O(1), #vars: 0, input, aspic, output |
T2/slayer-1-filtered | 1 + free_53 + G 615ms, INF, #vars: 2, input, output | 4930ms, input, output | 3220ms, input, output | 74ms, input, output | 73ms, input, aspic, aspic (errors) |
T2/slayer-1-rf | 3 1082ms, Ω(1), #vars: 0, input, output | 10662ms, input, output | 4652ms, input, output | 130ms, input, output | 64ms, input, aspic, aspic (errors) |
T2/slayer-2-filtered | 11 56ms, Ω(1), #vars: 0, input, output | 12 144ms, O(1), #vars: 0, input, output | 12 193ms, O(1), #vars: 0, input, output | 10 51ms, O(1), #vars: 0, input, output | 86ms, input, aspic, output |
T2/slayer-3 | 60014ms, input, output | 60021ms, input | 60001ms, input | 60001ms, input, output | 187ms, input, aspic, aspic (errors) |
T2/slayer-3-filtered | 1 + B 5633ms, Ω(n), #vars: 1, input, output | 49081ms, input, output | 60004ms, input, output | 686ms, input, output | 77ms, input, aspic, aspic (errors) |
T2/slayer-3-new | 60013ms, input, output | 60026ms, input | 60001ms, input | 60002ms, input, output, errors | 194ms, input, aspic, aspic (errors) |
T2/slayer-4-filtered | 60011ms, input, output | 60021ms, input | 60001ms, input | 21555ms, input, output | 108ms, input, aspic, aspic (errors) |
T2/slayer-n1 | INF 2860ms, INF, #vars: 1, input, output | 1649ms, input, output | 2834ms, input, output | 416ms, input, output | 9049ms, input, aspic |
T2/slayer-n1-filtered | INF 339ms, INF, #vars: 1, input, output | 1905ms, input, output | 1316ms, input, output | 66ms, input, output | 3467ms, input, aspic |
T2/slayer-n2 | INF 31ms, INF, #vars: 1, input, output | 936ms, input, output | 195ms, input, output | 48ms, input, output | 86ms, input, aspic, output, errors |
T2/slayer-n2-filtered | INF 31ms, INF, #vars: 1, input, output | 867ms, input, output | 177ms, input, output | 52ms, input, output | 80ms, input, aspic, output, errors |
T2/slayer-n3-filtered | 1 89ms, Ω(1), #vars: 0, input, output | 7 192ms, O(1), #vars: 0, input, output | 239ms, input, output, errors | 67ms, input | 1972ms, input, aspic, output |
T2/slayer-n5-filtered | 5 + free_53 - V + J1 2467ms, Ω(n), #vars: 3, input, output | 11792ms, input, output | 20548ms, input, output | 305ms, input, output | 73ms, input, aspic, aspic (errors) |
T2/smagilla-succeed | INF 196ms, INF, #vars: 1, input, output | 921ms, input, output | 404ms, input, output | 268ms, input, output | 97ms, input, aspic, output, errors |
T2/smagillb-succeed | INF 209ms, INF, #vars: 1, input, output | 459ms, input, output | 808ms, input, output | 250ms, input, output | 132ms, input, aspic, output, errors |
T2/smagillc-fail | INF 196ms, INF, #vars: 1, input, output | 879ms, input, output | 590ms, input, output | 239ms, input, output | 118ms, input, aspic, output, errors |
T2/smagillc-succeed | INF 189ms, INF, #vars: 1, input, output | 1027ms, input, output | 512ms, input, output | 221ms, input, output | 113ms, input, aspic, output, errors |
T2/sort | 1 1152ms, Ω(1), #vars: 0, input, output | 3977 1170ms, O(1), #vars: 0, input, output | 60003ms, input, output | 410ms, input, output | 748ms, input, aspic, output |
T2/spctrm | 4 - J + D 9855ms, Ω(n), #vars: 2, input, output | 186 * N + 186 * O + 16... 4268ms, O(n), #vars: 6, input, output | 60001ms, input, output | 903ms, input, output | 2343ms, input, aspic |
T2/spctrm.c.i.spctrm.pl.t2.fixed nonlinear | 4 - J 1212ms, Ω(n), #vars: 1, input, output | 186 * N + 186 * O + 16... 4289ms, O(n), #vars: 6, input, output | 60001ms, input, output | 724ms, input, output | Non-linear example not handled by prover. |
T2/spctrm.c.i.spctrm.pl.t2.nor.t2.rlgfixed | 4 - J + D 9829ms, Ω(n), #vars: 2, input, output | 186 * N + 186 * O + 16... 4354ms, O(n), #vars: 6, input, output | 60001ms, input, output | 783ms, input, output | 2596ms, input, aspic |
T2/spiral | B 3032ms, Ω(n), #vars: 1, input, output | 9 * A * B + B^2 + 25 *... 1587ms, O(n2), #vars: 2, input, output | max(2 * A + B + -1, -1... 672ms, O(n), #vars: 2, input, output | 34437ms, input, output | 96ms, input, aspic, output, errors |
T2/st88 | 19 - 2 * free_2 556ms, INF, #vars: 1, input, output | 2853ms, input, output | 223ms, input, output | 269ms, input, output | 87ms, input, aspic, output, errors |
T2/st88.bug | 13 - 2 * free_2 1235ms, INF, #vars: 1, input, output | 3398ms, input, output | 244ms, input, output | 119ms, input, output | 84ms, input, aspic, output, errors |
T2/statemate | 1 49097ms, Ω(1), #vars: 0, input, output | 60015ms, input | 60001ms, input | 4336ms, input, output | 98ms, input, aspic, aspic (errors) |
T2/stored | 1 149ms, Ω(1), #vars: 0, input, output | 1618ms, input, output | 288ms, input, output | 125ms, input, output | 83ms, input, aspic, output, errors |
T2/streamserver-succeed | INF 796ms, INF, #vars: 1, input, output | 14421ms, input, output | 60001ms, input, output | 791ms, input, output | 2413ms, input, aspic, output |
T2/streamserver.bug | INF 1077ms, INF, #vars: 1, input, output | 16418ms, input, output | 60001ms, input, output | 379ms, input, output | 2551ms, input, aspic, output |
T2/subpoly_crash | INF 50ms, INF, #vars: 1, input, output | 1223ms, input, output | 364ms, input, output | 46ms, input, output | 80ms, input, aspic, output, errors |
T2/sudoku nonlinear | 2 + free^2 + 2 * free 1088ms, INF, #vars: 1, input, output | 60013ms, input | 60001ms, input, output | 8725ms, input, output | Non-linear example not handled by prover. |
T2/sumit | 1 - 3 * B + 3 * C 605ms, Ω(n), #vars: 2, input, output | 2334ms, input, output | max(-3 * B + 3 * C + 6... 1455ms, O(n), #vars: 2, input, output | 255ms, input, output | 132ms, input, aspic, output, errors |
T2/svdcmp | 4 + H - A 24411ms, Ω(n), #vars: 2, input, output | 60013ms, input | 4966ms, input, output, errors | 535ms, input, output | 38511ms, input, aspic |
T2/svdcmp.c.i.svdcmp.pl.t2.fixed nonlinear | 60025ms, input, output | 60014ms, input | 5196ms, input, output, errors | 536ms, input, output | Non-linear example not handled by prover. |
T2/svdcmp.c.i.svdcmp.pl.t2.nor.t2.rlgfixed | 4 + H - A 21851ms, Ω(n), #vars: 2, input, output | 60012ms, input | 5242ms, input, output, errors | 489ms, input, output | 32830ms, input, aspic |
T2/toeplz | -14 + 3 / 2 * (-2 + A)... 1283ms, Ω(n2), #vars: 1, input, output | 5709ms, input, output | 13199ms, input, output | 262ms, input, output | 1131ms, input, aspic, output, errors |
T2/toeplz.c.i.toeplz.pl.t2.fixed nonlinear | 10 4356ms, Ω(1), #vars: 0, input, output | 522470403373181 * A + ... 1975ms, O(n2), #vars: 1, input, output | max(3, (7 / 2 * A + -3... 9803ms, O(n2), #vars: 1, input, output | 298ms, input, output | Non-linear example not handled by prover. |
T2/toeplz.c.i.toeplz.pl.t2.nor.t2.rlgfixed | -14 + 3 / 2 * (-2 + A)... 1303ms, Ω(n2), #vars: 1, input, output | 5988ms, input, output | 12993ms, input, output | 261ms, input, output | 1107ms, input, aspic, output, errors |
T2/tqli | 4 - B - D + 2 * A 9859ms, Ω(n), #vars: 3, input, output | 13352ms, input, output | 60001ms, input, output | 1240ms, input, output | 2752ms, input, aspic, output |
T2/tqli.c.i.tqli.pl.t2.fixed nonlinear | 60016ms, input, output | 17890ms, input, output | 60002ms, input, output | 1050ms, input, output | Non-linear example not handled by prover. |
T2/tqli.c.i.tqli.pl.t2.nor.t2.rlgfixed | 4 - B - D + 2 * A 9481ms, Ω(n), #vars: 3, input, output | 13698ms, input, output | 60001ms, input, output | 1290ms, input, output | 2640ms, input, aspic, output |
T2/traverse | 1 + free_195 + D 8405ms, INF, #vars: 2, input, output | 10061ms, input, output | 9326ms, input, output | 1715ms, input, output | 68ms, input, aspic, aspic (errors) |
T2/traverse2 | -1 + free_938 52182ms, INF, #vars: 1, input, output | 60016ms, input | 22970ms, input, output | 49052ms, input, output, errors | 96ms, input, aspic, aspic (errors) |
T2/traverse_seg | 1 + E + free_221 7957ms, INF, #vars: 2, input, output | 14218ms, input, output | 17553ms, input, output | 3432ms, input, output | 83ms, input, aspic, aspic (errors) |
T2/traverse_seg2 | 1 + R + free_207 8312ms, INF, #vars: 2, input, output | 15538ms, input, output | 11977ms, input, output | 2567ms, input, output | 83ms, input, aspic, aspic (errors) |
T2/traverse_twice | 1 + free_270 + D 11160ms, INF, #vars: 2, input, output | 27630ms, input, output | 16526ms, input, output | 2139ms, input, output | 87ms, input, aspic, aspic (errors) |
T2/two_arrays | 306 150ms, Ω(1), #vars: 0, input, output | 3043 669ms, O(1), #vars: 0, input, output | 307 575ms, O(1), #vars: 0, input, output | 300 89ms, O(1), #vars: 0, input, output | 309 208ms, O(1), #vars: 0, input, aspic, output |
T2/two_arrays1 | 408 195ms, Ω(1), #vars: 0, input, output | 3289 1027ms, O(1), #vars: 0, input, output | 409 872ms, O(1), #vars: 0, input, output | 400 130ms, O(1), #vars: 0, input, output | 244ms, input, aspic, output |
T2/two_arrays2 | 8 + 8 * E 192ms, Ω(n), #vars: 1, input, output | 18 * E + 55 1135ms, O(n), #vars: 1, input, output | max(8 * E + 9, 9) 1157ms, O(n), #vars: 1, input, output | max(E, 0) + max(E, 0) ... 131ms, O(n), #vars: 1, input, output | 281ms, input, aspic, output |
T2/two_arrays6 | 8 + 8 * E 199ms, Ω(n), #vars: 1, input, output | 20 * E + 51 1131ms, O(n), #vars: 1, input, output | max(8 * E + 9, 9) 1088ms, O(n), #vars: 1, input, output | max(E, 0) + max(E, 0) ... 176ms, O(n), #vars: 1, input, output | 282ms, input, aspic, output |
T2/ud | 1 752ms, Ω(1), #vars: 0, input, output | 76604 * F + 76604 * G ... 6770ms, O(n), #vars: 4, input, output | 381 5001ms, O(1), #vars: 0, input, output | 770 746ms, O(1), #vars: 0, input, output | 451ms, input, aspic |
T2/vmcai_bytes | 1 17ms, Ω(1), #vars: 0, input, output | 1 15ms, O(1), #vars: 0, input, output | 1 148ms, O(1), #vars: 0, input, output | 39ms, input | 3 84ms, O(1), #vars: 0, input, aspic, output |
T2/vmcai_struct | 1 19ms, Ω(1), #vars: 0, input, output | 1 14ms, O(1), #vars: 0, input, output | 1 143ms, O(1), #vars: 0, input, output | 35ms, input | 3 70ms, O(1), #vars: 0, input, aspic, output |
T2/w1 | INF 95ms, INF, #vars: 1, input, output | 1142ms, input, output | 163ms, input, output | 40ms, input, output | 92ms, input, aspic, output, errors |
T2/w2_nt | INF 478ms, INF, #vars: 1, input, output | 1285ms, input, output | 2289ms, input, output | 156ms, input, output | 1209ms, input, aspic, output |
T2/walk | 1 236ms, Ω(1), #vars: 0, input, output | 2957ms, input, output | 512ms, input, output | 65ms, input, output | 292ms, input, aspic, output, errors |
T2/wrong_loop | INF 434ms, INF, #vars: 1, input, output | 516ms, input, output | 303ms, input, output | 119ms, input, output | 85ms, input, aspic, output, errors |
T2/wtf | 1 10628ms, Ω(1), #vars: 0, input, output | 111 * C + 111 * E + 11... 1481ms, O(n), #vars: 4, input, output | 60001ms, input, output | 215ms, input, output | 758ms, input, aspic, output |
T2/zeroconf | 1 8128ms, Ω(1), #vars: 0, input, output | 53695ms, input, output | 4343ms, input, output | 220ms, input, output | 52192ms, input, aspic, aspic (errors) |
T2/zeroconf_withassume | 1 8929ms, Ω(1), #vars: 0, input, output | 55691ms, input, output | 5649ms, input, output | 285ms, input, output | 55314ms, input, aspic, aspic (errors) |
c-examples/ABC/ex01 | 4 + 2 * B - 2 * A 88ms, Ω(n), #vars: 2, input, output | 4 * A + 4 * B + 6 95ms, O(n), #vars: 2, input, output | max(-2 * A + 2 * B + 6... 192ms, O(n), #vars: 2, input, output | max(0, B + 1 + 0 - A) 44ms, O(n), #vars: 2, input, output | 102ms, input, aspic, output, errors |
c-examples/ABC/ex02 | 2 + 4 * B + B^2 104ms, Ω(n2), #vars: 1, input, output | 906 * B + 72 * B^2 + 298 204ms, O(n2), #vars: 1, input, output | max(4, (2 * B + 3) * B... 288ms, O(n2), #vars: 1, input, output | max(B, 0) + max(0, 1 +... 76ms, O(n2), #vars: 1, input, output | 91ms, input, aspic, output, errors |
c-examples/ABC/ex03 | -5 / 6 - 3 / 4 * (-1 +... 219ms, Ω(n4), #vars: 1, input, output | 159238928 * B + 242186... 494ms, O(n6), #vars: 1, input, output | max(9, (B + -1) * max(... 1179ms, O(n4), #vars: 1, input, output | max(B, 0) + max(0, 1 +... 141ms, O(n4), #vars: 1, input, output | 155ms, input, aspic, output, errors |
c-examples/ABC/ex04 nonlinear | 1 433ms, Ω(1), #vars: 0, input, output | 6191ms, input, output | 830ms, input, output | 206ms, input, output | Non-linear example not handled by prover. |
c-examples/ABC/ex05 | 2 + 4 * B + B^2 104ms, Ω(n2), #vars: 1, input, output | 2238 * B + 72 * B^2 + ... 206ms, O(n2), #vars: 1, input, output | max(4, (2 * B + 3) * B... 287ms, O(n2), #vars: 1, input, output | max(B, 0) + max(0, 1 +... 74ms, O(n2), #vars: 1, input, output | 103ms, input, aspic, output, errors |
c-examples/ABC/ex06 | 2 + 4 * B + B^2 98ms, Ω(n2), #vars: 1, input, output | 13106 * B + 84 * B^2 +... 206ms, O(n2), #vars: 1, input, output | max(4, (2 * B + 3) * B... 273ms, O(n2), #vars: 1, input, output | max(B, 0) + max(0, max... 68ms, O(n2), #vars: 1, input, output | 101ms, input, aspic, output, errors |
c-examples/ABC/ex07 | 2 + 3 * B + 2 * B * D 101ms, Ω(n2), #vars: 2, input, output | 30 * B + 12 * B * D + ... 232ms, O(n2), #vars: 2, input, output | max(3 * B + 4, 4, (2 *... 308ms, O(n2), #vars: 2, input, output | max(B, 0) + max(0, max... 67ms, O(n2), #vars: 1, input, output | 107ms, input, aspic, output, errors |
c-examples/ABC/ex08 | 2 + 2 * B * A + 3 * A 103ms, Ω(n2), #vars: 2, input, output | 15 * A + 12 * A * B + ... 196ms, O(n2), #vars: 2, input, output | max(3 * A + 4, 4, (2 *... 268ms, O(n2), #vars: 2, input, output | max(A, 0) + max(0, max... 67ms, O(n2), #vars: 1, input, output | 103ms, input, aspic, output, errors |
c-examples/ABC/ex09 | 2 + 3 * B + 2 * B * D 105ms, Ω(n2), #vars: 2, input, output | 30 * B + 12 * B * D + ... 226ms, O(n2), #vars: 2, input, output | max(3 * B + 4, 4, (2 *... 305ms, O(n2), #vars: 2, input, output | max(B, 0) + max(0, max... 69ms, O(n2), #vars: 1, input, output | 93ms, input, aspic, output, errors |
c-examples/ABC/ex10 | 2 + 2 * B * A + 3 * A 97ms, Ω(n2), #vars: 2, input, output | 30 * A + 12 * A * B + ... 204ms, O(n2), #vars: 2, input, output | max(3 * A + 4, 4, (2 *... 276ms, O(n2), #vars: 2, input, output | max(A, 0) + max(0, max... 66ms, O(n2), #vars: 1, input, output | 91ms, input, aspic, output, errors |
c-examples/ABC/ex11 | 2 + 2 * B * A + 3 * A 100ms, Ω(n2), #vars: 2, input, output | 15 * A + 12 * A * B + ... 196ms, O(n2), #vars: 2, input, output | max(3 * A + 4, 4, (2 *... 274ms, O(n2), #vars: 2, input, output | max(A, 0) + max(0, max... 66ms, O(n2), #vars: 1, input, output | 101ms, input, aspic, output, errors |
c-examples/ABC/ex12 | 2 + 5 * A 91ms, Ω(n), #vars: 1, input, output | 18 * A + 24 * A * B + ... 203ms, O(n2), #vars: 2, input, output | max(5 * A + 4, 4) 224ms, O(n), #vars: 1, input, output | 1 + max(A, 0) 68ms, O(n), #vars: 1, input, output | 90ms, input, aspic, output, errors |
c-examples/ABC/ex13 | -5 - 7 * B + 2 * (1 + ... 1147ms, Ω(n3), #vars: 3, input, output | 2537 * A + 2537 * B + ... 527ms, O(n4), #vars: 4, input, output | max(-3 * A + 3 * B + 7... 1279ms, O(n3), #vars: 4, input, output | max(0, max(0, max(0, D... 127ms, O(n3), #vars: 2, input, output | 195ms, input, aspic, output, errors |
c-examples/ABC/ex14 | 2 + 1 / 3 * B^3 * A + ... 200ms, Ω(n4), #vars: 2, input, output | 7871239044 * A + 11971... 521ms, O(n8), #vars: 2, input, output | max(3 * A + 4, 4, A * ... 1089ms, O(n4), #vars: 2, input, output | max(A, 0) + max(0, max... 174ms, O(n4), #vars: 1, input, output | 199ms, input, aspic, output, errors |
c-examples/ABC/ex15 | 6 + 6 * B 193ms, Ω(n), #vars: 1, input, output | 4045ms, input, output | 1198ms, input, output | 218ms, input, output | 269ms, input, aspic, output, errors |
c-examples/Loopus/Example1 | 1 + 3 * B 157ms, Ω(n), #vars: 1, input, output | 80 * B + 34 870ms, O(n), #vars: 1, input, output | max(8 * B + 1, 3 * B +... 768ms, O(n), #vars: 1, input, output | max(0, -2 + max(B, 0))... 147ms, O(n), #vars: 1, input, output | 150ms, input, aspic, output, errors |
c-examples/Loopus/Example2 | 1 2062ms, Ω(1), #vars: 0, input, output | 13381ms, input, output | max(3 / 2 * A + 25 / 2... 7854ms, O(n), #vars: 1, input, output | 302ms, input, output | 1226ms, input, aspic, output, errors |
c-examples/Loopus/Example3 | 677 156ms, Ω(1), #vars: 0, input, output | 18 * A * B + 4590 * B ... 770ms, O(n2), #vars: 2, input, output | max(3 * A + 4, 4, -3 *... 343ms, O(n), #vars: 1, input, output | max(0, max(A, 0) + max... 179ms, O(n), #vars: 1, input, output | 86ms, input, aspic, output, errors |
c-examples/Rank/ex1 | 10 + 8 * B 227ms, Ω(n), #vars: 1, input, output | 70944 * B + 36720 * B^... 4054ms, O(n2), #vars: 1, input, output | max(4, 6 * B + max(max... 730ms, O(n2), #vars: 1, input, output | 686ms, input, output | 184ms, input, aspic, output, errors |
c-examples/Rank/ex2 | 2 + 7 * meter 137ms, Ω(n), #vars: 1, input, output | 36 * B + 16 967ms, O(n), #vars: 1, input, output | max(4, 9 / 2 * B + 3 /... 435ms, O(n2), #vars: 1, input, output | max(0, B + -1) + max(0... 90ms, O(n), #vars: 1, input, output | 138ms, input, aspic, output, errors |
c-examples/Rank/ex3 | 4 + 5 * meter 186ms, Ω(n), #vars: 1, input, output | 52 * B + 30 1351ms, O(n), #vars: 1, input, output | max(25 / 4 * B + 11 / ... 520ms, O(n), #vars: 1, input, output | max(0, B + -1) + max(0... 92ms, O(n), #vars: 1, input, output | 248ms, input, aspic, output, errors |
c-examples/SPEED/CAV09/ex1 | 2 + 3 * C 160ms, Ω(n), #vars: 1, input, output | 6 * C + 602 514ms, O(n), #vars: 1, input, output | max(3 * C + 304, 304) 266ms, O(n), #vars: 1, input, output | 100 + max(C, 0) + max(... 74ms, O(n), #vars: 1, input, output | 101ms, input, aspic, output, errors |
c-examples/SPEED/CAV09/ex2 | -1 + 3 * C + 3 * (-1 +... 276ms, Ω(n2), #vars: 2, input, output | 12 * C + 18 * D + 18 *... 474ms, O(n2), #vars: 2, input, output | max(4, max(0, D * C + ... 263ms, O(n2), #vars: 2, input, output | max(C, 0) + max(0, max... 70ms, O(n2), #vars: 1, input, output | 101ms, input, aspic, output, errors |
c-examples/SPEED/CAV09/ex3 | 4 + 3 * B 124ms, Ω(n), #vars: 1, input, output | 90 * B + 5 3922ms, O(n), #vars: 1, input, output | max(8 * B + 5, 5, 3 * ... 644ms, O(n), #vars: 1, input, output | max(B, 0) + max(B, 0) ... 268ms, O(n), #vars: 1, input, output | 148ms, input, aspic, output, errors |
c-examples/SPEED/PLDI09/Example2 | 1 200ms, Ω(1), #vars: 0, input, output | 42 * A + 23 428ms, O(n), #vars: 1, input, output | max(8 * A, 5) 290ms, O(n), #vars: 1, input, output | 281ms, input, output | 110ms, input, aspic, output, errors |
c-examples/SPEED/PLDI09/Example3 | -2 + 4 * (-1 + B) * A ... 287ms, Ω(n2), #vars: 2, input, output | 500 * A + 300 * B + 50... 574ms, O(n2), #vars: 2, input, output | max(5, max(0, min(B * ... 503ms, O(n2), #vars: 2, input, output | max(B, 0) + max(0, max... 73ms, O(n2), #vars: 1, input, output | 163ms, input, aspic, output, errors |
c-examples/SPEED/PLDI09/Example4 | 1 155ms, Ω(1), #vars: 0, input, output | 32 * B^2 + 32 * A * B ... 1274ms, O(n2), #vars: 2, input, output | 247ms, input, output | 156ms, input, output | 126ms, input, aspic, output, errors |
c-examples/SPEED/PLDI09/Example5 | 2 + 3 * B - 3 * A 199ms, Ω(n), #vars: 2, input, output | 36 * B^2 + 54 * A * B ... 543ms, O(n2), #vars: 2, input, output | max(-3 * A + 3 * B + 4... 362ms, O(n), #vars: 2, input, output | max(A, 0) + max(A, 0) ... 103ms, O(n), #vars: 2, input, output | 122ms, input, aspic, output, errors |
c-examples/SPEED/PLDI09/Example6 | 5 + G 147ms, Ω(n), #vars: 1, input, output | 28 * D + 7 * G + 27 2435ms, O(n), #vars: 2, input, output | max(4, max(0, D + G) +... 664ms, O(n2), #vars: 1, input, output | max(G, 0) + max(G, 0) ... 147ms, O(n), #vars: 1, input, output | 182ms, input, aspic, output, errors |
c-examples/SPEED/PLDI09/NestedLoop | 7 + 3 * C 526ms, Ω(n), #vars: 1, input, output | 236 * A + 8 * C + 352 ... 1766ms, O(n2), #vars: 3, input, output | max(4 * A + 4, 5, max(... 4460ms, O(n2), #vars: 3, input, output | max(C, 0) + max(C, 0) ... 554ms, O(n2), #vars: 2, input, output | 192ms, input, aspic, output |
c-examples/SPEED/PLDI09/cyclic | 2 + 3 * B - 3 * A 368ms, Ω(n), #vars: 2, input, output | 2867ms, input, output | max(-3 * A + 3 * B + 8... 762ms, O(n), #vars: 2, input, output | 125ms, input, output | 135ms, input, aspic, output, errors |
c-examples/SPEED/PLDI10/Ex1 | -1 + 2 * (-1 + A) * A ... 242ms, Ω(n2), #vars: 1, input, output | 5565ms, input, output | max(8, 2 * A + -4 + (2... 427ms, O(n2), #vars: 1, input, output | max(A, 0) + max(0, max... 117ms, O(n3), #vars: 1, input, output | 126ms, input, aspic, output, errors |
c-examples/SPEED/PLDI10/Ex2 | INF 76ms, INF, #vars: 1, input, output | 5971ms, input, output | 483ms, input, output | 138ms, input, output | 131ms, input, aspic, output, errors |
c-examples/SPEED/PLDI10/Ex3 | 4 + 3 * A 127ms, Ω(n), #vars: 1, input, output | 3273ms, input, output | 458ms, input, output | 260ms, input, output | 84ms, input, aspic, output, errors |
c-examples/SPEED/PLDI10/Ex4 | 3 + 3 * A 122ms, Ω(n), #vars: 1, input, output | 90 * A + 69 736ms, O(n), #vars: 1, input, output | max(6 * A + 5, 7, 3 * ... 611ms, O(n), #vars: 1, input, output | 431ms, input, output | 109ms, input, aspic, output, errors |
c-examples/SPEED/PLDI10/Ex5 | INF 153ms, INF, #vars: 1, input, output | 5008ms, input, output | 499ms, input, output | 124ms, input, output | 148ms, input, aspic, output, errors |
c-examples/SPEED/PLDI10/Ex6 | 5 - 3 * B + 3 * A 202ms, Ω(n), #vars: 2, input, output | 15 * A + 12 * B + 27 *... 362ms, O(n), #vars: 3, input, output | max(4, -3 * A + 3 * C ... 227ms, O(n), #vars: 2, input, output | max(0, max(0, A + 1 + ... 114ms, O(n2), #vars: 2, input, output | 183ms, input, aspic, output, errors |
c-examples/SPEED/PLDI10/Ex7 | 2 + 2 * B - 2 * A 368ms, Ω(n), #vars: 2, input, output | 1464ms, input, output | max(-2 * A + 2 * B + 4... 513ms, O(n), #vars: 2, input, output | 165ms, input, output | 97ms, input, aspic, output, errors |
c-examples/SPEED/POPL09/Dis1 | 2 - 3 * C + 3 * D 311ms, Ω(n), #vars: 2, input, output | 6 * A + 6 * B + 6 * C ... 426ms, O(n), #vars: 4, input, output | max(-3 * A + 3 * B + -... 295ms, O(n), #vars: 4, input, output | max(0, D - C) + max(0,... 82ms, O(n), #vars: 2, input, output | 87ms, input, aspic, output, errors |
c-examples/SPEED/POPL09/Dis2 | 5 - 3 * C + 3 * A 206ms, Ω(n), #vars: 2, input, output | 18 * A + 34 * B + 16 *... 368ms, O(n), #vars: 3, input, output | max(4, -3 * A + 3 * B ... 234ms, O(n), #vars: 2, input, output | max(0, max(0, A + 1 + ... 116ms, O(n2), #vars: 2, input, output | 77ms, input, aspic, output, errors |
c-examples/SPEED/POPL09/NestedMultiple | 3 - 3 * C + 3 * D 283ms, Ω(n), #vars: 2, input, output | 3567ms, input, output | max(-3 * A + 3 * B + -... 759ms, O(n), #vars: 4, input, output | max(0, D - C) + max(0,... 77ms, O(n), #vars: 2, input, output | 153ms, input, aspic, output, errors |
c-examples/SPEED/POPL09/NestedMultipleDep | 2 + 2 * E * B + 3 * B 103ms, Ω(n2), #vars: 2, input, output | 25 * B + 20 * B * E + 4 662ms, O(n2), #vars: 2, input, output | max(3 * B + 4, 4, (2 *... 347ms, O(n2), #vars: 2, input, output | max(B, 0) + max(0, max... 66ms, O(n2), #vars: 1, input, output | 81ms, input, aspic, output, errors |
c-examples/SPEED/POPL09/NestedSingle | 3 + 3 * B 134ms, Ω(n), #vars: 1, input, output | 48 * B + 16 4200ms, O(n), #vars: 1, input, output | max(7 * B + 4, 3 * B +... 625ms, O(n), #vars: 1, input, output | max(B, 0) + max(B, 0) ... 89ms, O(n), #vars: 1, input, output | 106ms, input, aspic, output, errors |
c-examples/SPEED/POPL09/SequentialSingle | 2 + 3 * B 111ms, Ω(n), #vars: 1, input, output | 21 * B + 6 213ms, O(n), #vars: 1, input, output | max(3 * B + 6, 2 * B +... 258ms, O(n), #vars: 1, input, output | max(B, 0) + max(B, 0) 50ms, O(n), #vars: 1, input, output | 113ms, input, aspic, output, errors |
c-examples/SPEED/POPL09/SimpleMultiple | 2 + 3 * D 160ms, Ω(n), #vars: 1, input, output | 6 * C + 6 * D + 8 464ms, O(n), #vars: 2, input, output | max(3 * C + 3 * D + 4,... 321ms, O(n), #vars: 2, input, output | max(C, 0) + max(D, 0) ... 81ms, O(n), #vars: 1, input, output | 85ms, input, aspic, output, errors |
c-examples/SPEED/POPL09/SimpleMultipleDep | -1 + 3 * C + 3 * (-1 +... 262ms, Ω(n2), #vars: 2, input, output | 12 * C + 18 * D + 18 *... 495ms, O(n2), #vars: 2, input, output | max(4, max(0, D * C + ... 261ms, O(n2), #vars: 2, input, output | max(C, 0) + max(0, max... 72ms, O(n2), #vars: 1, input, output | 111ms, input, aspic, output, errors |
c-examples/SPEED/POPL09/SimpleSingle | 2 + 2 * B 72ms, Ω(n), #vars: 1, input, output | 4 * B + 6 99ms, O(n), #vars: 1, input, output | max(2 * B + 4, 4) 191ms, O(n), #vars: 1, input, output | max(B, 0) 46ms, O(n), #vars: 1, input, output | 83ms, input, aspic, output, errors |
c-examples/SPEED/POPL09/SimpleSingle2 | 2 + 3 * C 159ms, Ω(n), #vars: 1, input, output | 20 * D + 12 * C + 17 295ms, O(n), #vars: 2, input, output | max(-1 * C + 4 * D + 6... 1060ms, O(n), #vars: 2, input, output | max(D, 0) + max(C, 0) 51ms, O(n), #vars: 1, input, output | 113ms, input, aspic, output, errors |
c-examples/WTC/aaron2 | 1 117ms, Ω(1), #vars: 0, input, output | 35 * A + 28 * B + 28 *... 306ms, O(n), #vars: 3, input, output | max(3 * B + -3 * C + 7... 294ms, O(n), #vars: 2, input, output | max(0, max(0, B + 1 + ... 192ms, O(n2), #vars: 2, input, output | 110ms, input, aspic, output, errors |
c-examples/WTC/ax | 2 * C * (-2 + C) + C 108ms, Ω(n2), #vars: 1, input, output | 23 * C + 12 * C^2 + 14 201ms, O(n2), #vars: 1, input, output | max(2 * C + 2, 8, 2 * ... 416ms, O(n2), #vars: 1, input, output | max(0, C + -2) + max(0... 74ms, O(n2), #vars: 1, input, output | 117ms, input, aspic, output, errors |
c-examples/WTC/complex | 8 601ms, Ω(1), #vars: 0, input, output | 60011ms, input | max(4, max(0, min(-1 /... 37503ms, O(n2), #vars: 2, input, output | 171ms, input, output | 177ms, input, aspic, output, errors |
c-examples/WTC/counterex1b | 18 + 6 * (1 + A) * F +... 187ms, Ω(n2), #vars: 2, input, output | 5180ms, input, output | 1592ms, input, output | 404ms, input, output | 212ms, input, aspic, output, errors |
c-examples/WTC/cousot9 | 2 + 3 * free 243ms, INF, #vars: 1, input, output | 2661ms, input, output | 243ms, input, output | 66ms, input, output | 135ms, input, aspic, output, errors |
c-examples/WTC/easy1 | 1 97ms, Ω(1), #vars: 0, input, output | 830 207ms, O(1), #vars: 0, input, output | 124 250ms, O(1), #vars: 0, input, output | 40 76ms, O(1), #vars: 0, input, output | 93ms, input, aspic, output, errors |
c-examples/WTC/easy2 | 2 + 2 * A 67ms, Ω(n), #vars: 1, input, output | 4 * A + 6 94ms, O(n), #vars: 1, input, output | max(2 * A + 4, 4) 184ms, O(n), #vars: 1, input, output | max(A, 0) 44ms, O(n), #vars: 1, input, output | 78ms, input, aspic, output, errors |
c-examples/WTC/exmini | 1 90ms, Ω(1), #vars: 0, input, output | 2 * A + 2 * B + 2 * C ... 139ms, O(n), #vars: 3, input, output | max(-1 * A + B + -1 * ... 322ms, O(n), #vars: 3, input, output | max(0, B + 1 + 0 - C) 55ms, O(n), #vars: 2, input, output | 111ms, input, aspic, output, errors |
c-examples/WTC/gcd | 1 129ms, Ω(1), #vars: 0, input, output | 3385ms, input, output | max(3 * A + 3 * B + -2... 266ms, O(n), #vars: 2, input, output | 59ms, input, output | 121ms, input, aspic, output, errors |
c-examples/WTC/insertsort | -7 / 2 + 3 / 2 * (-1 +... 131ms, Ω(n2), #vars: 1, input, output | 172748 * B + 384 * B^2... 293ms, O(n2), #vars: 1, input, output | max(5, max(5 * B + -10... 464ms, O(n2), #vars: 1, input, output | max(0, B + -1) + max(0... 141ms, O(n2), #vars: 1, input, output | 125ms, input, aspic, output, errors |
c-examples/WTC/loops | 8 217ms, Ω(1), #vars: 0, input, output | 126 * A + 24 * A^2 + 107 752ms, O(n2), #vars: 1, input, output | max(3 * A + 7, 3, (2 *... 278ms, O(n2), #vars: 1, input, output | max(0, A + 1) + max(0,... 91ms, O(n2), #vars: 1, input, output | 106ms, input, aspic, output, errors |
c-examples/WTC/nd_loop | 1 130ms, Ω(1), #vars: 0, input, output | 15 85ms, O(1), #vars: 0, input, output | 13 239ms, O(1), #vars: 0, input, output | 1 45ms, O(1), #vars: 0, input, output | 8 84ms, O(1), #vars: 0, input, aspic, output |
c-examples/WTC/ndecr | -2 + 2 * A 69ms, Ω(n), #vars: 1, input, output | 4 * A + 6 87ms, O(n), #vars: 1, input, output | max(2 * A, 4) 181ms, O(n), #vars: 1, input, output | max(0, A + -2) 46ms, O(n), #vars: 1, input, output | 82ms, input, aspic, output, errors |
c-examples/WTC/nestedLoop | 8 + 2 * C 266ms, Ω(n), #vars: 1, input, output | 60014ms, input | max(6 * A + -4 * C + 4... 1239ms, O(n2), #vars: 3, input, output | max(C, 0) + max(C, 0) ... 110ms, O(n2), #vars: 2, input, output | 332ms, input, aspic, output, errors |
c-examples/WTC/perfect | 3 + 5 * meter 629ms, Ω(n), #vars: 1, input, output | 39 * A + 12 * A^2 + 36 1049ms, O(n2), #vars: 1, input, output | max(3, max((2 * A + 1)... 449ms, O(n2), #vars: 1, input, output | 274ms, input, output | 143ms, input, aspic, output, errors |
c-examples/WTC/random1d | 2 + 2 * A 67ms, Ω(n), #vars: 1, input, output | 12 * A + 13 155ms, O(n), #vars: 1, input, output | max(2 * A + 4, 3) 205ms, O(n), #vars: 1, input, output | max(A, 0) 55ms, O(n), #vars: 1, input, output | max(5, 2 + 1 + A__o' +... 102ms, O(n), #vars: 1, input, aspic, output |
c-examples/WTC/random2d | 2 + 2 * B 139ms, Ω(n), #vars: 1, input, output | 216 * B + 139 811ms, O(n), #vars: 1, input, output | max(7 * B + 4, 4) 317ms, O(n), #vars: 1, input, output | max(B, 0) 67ms, O(n), #vars: 1, input, output | 489ms, input, aspic, output, errors |
c-examples/WTC/realbubble | -4 + 2 * (-1 + A)^2 + ... 206ms, Ω(n2), #vars: 1, input, output | 212212 * A + 1248 * A^... 336ms, O(n2), #vars: 1, input, output | max(4 * A + 2, 4, (A +... 482ms, O(n2), #vars: 1, input, output | max(0, A + -1) + max(0... 101ms, O(n2), #vars: 1, input, output | 179ms, input, aspic, output, errors |
c-examples/WTC/realheapsort | 1 8504ms, Ω(1), #vars: 0, input, output | 891990781 * A + 759980... 2235ms, O(n4), #vars: 1, input, output | 1005ms, input, output | 685ms, input, output | 307ms, input, aspic, output |
c-examples/WTC/realheapsort_step1 | 1 8646ms, Ω(1), #vars: 0, input, output | 216 * A^2 + 86139 * A ... 755ms, O(n2), #vars: 1, input, output | max(4, max(4 * A + -8,... 469ms, O(n2), #vars: 1, input, output | 296ms, input, output | 681ms, input, aspic, output, errors |
c-examples/WTC/realheapsort_step2 | -24 + 9 * A 872ms, Ω(n), #vars: 1, input, output | 924 * A + 240 * A^2 + 888 1206ms, O(n2), #vars: 1, input, output | 589ms, input, output | 117ms, input, output | 326ms, input, aspic, output, errors |
c-examples/WTC/realselect | -1 - (-1 + B)^2 + 3 * ... 98ms, Ω(n2), #vars: 1, input, output | 132 * B + 72 * B^2 + 64 643ms, O(n2), #vars: 1, input, output | max(4, (2 * B + 2) * (... 269ms, O(n2), #vars: 1, input, output | max(0, B + -1) + max(0... 88ms, O(n2), #vars: 1, input, output | 112ms, input, aspic, output, errors |
c-examples/WTC/realshellsort | 1 988ms, Ω(1), #vars: 0, input, output | 78 * A + 330 * A^2 + 2... 1061ms, O(n3), #vars: 1, input, output | 1465ms, input, output | 234ms, input, output | 266ms, input, aspic, output, errors |
c-examples/WTC/rsd | 6 + 3 * A 127ms, Ω(n), #vars: 1, input, output | 81 * A + 72 * A^2 + 30 1011ms, O(n2), #vars: 1, input, output | max(3, 3 * A + 3 + max... 316ms, O(n2), #vars: 1, input, output | 144ms, input, output | 110ms, input, aspic, output, errors |
c-examples/WTC/sipma91 | 2 + 2 * meter 109ms, Ω(n), #vars: 1, input, output | 27608 * A + 135 * A^2 ... 1106ms, O(n2), #vars: 1, input, output | max(79 / 11, -2 / 11 *... 382ms, O(n), #vars: 1, input, output | max(0, 9 * max(0, 101 ... 152ms, O(n), #vars: 1, input, output | 201ms, input, aspic, output |
c-examples/WTC/sipmabubble | 2 + 3 / 2 * A^2 + 9 / ... 237ms, Ω(n2), #vars: 1, input, output | 255 * A + 120 * A^2 + 139 546ms, O(n2), #vars: 1, input, output | max(7, (4 * A + 3) * A... 264ms, O(n2), #vars: 1, input, output | max(0, A + 1) + max(0,... 98ms, O(n2), #vars: 1, input, output | 122ms, input, aspic, output, errors |
c-examples/WTC/speedFails4 | 1 131ms, Ω(1), #vars: 0, input, output | 3332ms, input, output | 297ms, input, output | 116ms, input, output | 121ms, input, aspic, output, errors |
c-examples/WTC/speedpldi2 | 1 192ms, Ω(1), #vars: 0, input, output | 28 * A + 10 386ms, O(n), #vars: 1, input, output | max(6 * A + 1, 4) 249ms, O(n), #vars: 1, input, output | 82ms, input, output | 114ms, input, aspic, output, errors |
c-examples/WTC/speedpldi3 | -1 + 3 * (-1 + B) * A ... 292ms, Ω(n2), #vars: 2, input, output | 6 * B + 225 * A + 30 *... 476ms, O(n2), #vars: 2, input, output | max(3, max(0, min(B * ... 349ms, O(n2), #vars: 2, input, output | max(B, 0) + max(0, max... 48ms, O(n2), #vars: 1, input, output | 120ms, input, aspic, output, errors |
c-examples/WTC/speedpldi4 | 1 143ms, Ω(1), #vars: 0, input, output | 15 * B + 6 399ms, O(n), #vars: 1, input, output | max(-3 * A + 3 * B + 7... 271ms, O(n), #vars: 2, input, output | 50ms, input, output | max(3 + 1 + B__o' + B_... 120ms, O(n), #vars: 2, input, aspic, output |
c-examples/WTC/terminate | 1 83ms, Ω(1), #vars: 0, input, output | 2 * A + 2 * B + 2 * C ... 132ms, O(n), #vars: 3, input, output | max(-1 * A + B + -1 * ... 310ms, O(n), #vars: 3, input, output | max(0, B + 1 + 0 - C) 54ms, O(n), #vars: 2, input, output | 90ms, input, aspic, output, errors |
c-examples/WTC/wcet1 | -2 + 4 * A 627ms, Ω(n), #vars: 1, input, output | 44 * A + 26 370ms, O(n), #vars: 1, input, output | max(4 * A + 3, 7) 406ms, O(n), #vars: 1, input, output | max(0, A + -1) 63ms, O(n), #vars: 1, input, output | max(2 + A__o' + 1 + A_... 146ms, O(n), #vars: 1, input, aspic, output |
c-examples/WTC/wcet2 | 1 126ms, Ω(1), #vars: 0, input, output | 123984 * A + 360 * A^2... 211ms, O(n2), #vars: 1, input, output | max(-3 * A + 59, 46, -... 450ms, O(n), #vars: 1, input, output | max(0, 10 + 10 * max(0... 119ms, O(n), #vars: 1, input, output | 92ms, input, aspic, output, errors |
c-examples/WTC/while2 | 2 + 3 * B + 2 * B^2 98ms, Ω(n2), #vars: 1, input, output | 19 * B + 12 * B^2 + 9 192ms, O(n2), #vars: 1, input, output | max(4, (2 * B + 3) * B... 263ms, O(n2), #vars: 1, input, output | max(B, 0) + max(0, max... 68ms, O(n2), #vars: 1, input, output | 96ms, input, aspic, output, errors |
c-examples/WTC/wise | -4 - 3 * B + 3 * A 165ms, Ω(n), #vars: 2, input, output | 18 * B + 18 * A + 15 455ms, O(n), #vars: 2, input, output | max(3 * A + -3 * B + -... 291ms, O(n), #vars: 2, input, output | 71ms, input, output | max(3 + 1 + B__o' + A_... 175ms, O(n), #vars: 2, input, aspic, output |
costa/RAML/rationalPotential | 1 117ms, Ω(1), #vars: 0, input, output | A + 1 169ms, O(n), #vars: 1, input, output | max(1, max(0, min(C, A... 201ms, O(n), #vars: 3, input, output | max(B, 0) 55ms, O(n), #vars: 1, input, output | 80ms, input, aspic, output, errors |
costa/misc/ack | 1 + B 137ms, Ω(n), #vars: 1, input, output | 2394ms, input, output | 205ms, input, output | 63ms, input, output | 79ms, input, aspic, output, errors |
costa/misc/direct_n_log_n | 1 150ms, Ω(1), #vars: 0, input, output | 4 * A + 9 81ms, O(n), #vars: 1, input, output | max(A, 1) 192ms, O(n), #vars: 1, input, output | 47ms, input, output | max(2, 1 + A__o' + 1) 69ms, O(n), #vars: 1, input, aspic, output |
costa/misc/linear | 1 + A 65ms, Ω(n), #vars: 1, input, output | A + 2 85ms, O(n), #vars: 1, input, output | max(A + 1, 101) 183ms, O(n), #vars: 1, input, output | max(A, 100) 50ms, O(n), #vars: 1, input, output | max(2, 1 + 1 + A__o' + 1) 79ms, O(n), #vars: 1, input, aspic, output |
costa/misc/logarithmic nonlinear | 1 145ms, Ω(1), #vars: 0, input, output | 3 44ms, O(1), #vars: 0, input, output | 1 168ms, O(1), #vars: 0, input, output | 1 56ms, O(1), #vars: 0, input, output | Non-linear example not handled by prover. |
costa/misc/merge | 1 + A 158ms, Ω(n), #vars: 1, input, output | 2 * A + 2 * B + 3 138ms, O(n), #vars: 2, input, output | max(A + B, 1) 208ms, O(n), #vars: 2, input, output | max(B, 0) + max(A, 0) ... 68ms, O(n), #vars: 1, input, output | 84ms, input, aspic, output, errors |
costa/misc/mspe | 1 2061ms, Ω(1), #vars: 0, input, output | 4 * B + 4 * F + 5 205ms, O(n), #vars: 2, input, output | max(-1 * A + B + 2, 1) 4269ms, O(n), #vars: 2, input, output | 502ms, input, output | max(2, 1 + 2 + -1 * F_... 25241ms, O(n), #vars: 2, input, aspic, output |