Benchmark Result Comparison

Loopus KoAT CoFloCo C4B Loopus14 Rank
All 110 110 110 110 110 103
Bounded 86 90 87 36 86 78
Success 78 % 82 % 79 % 33 % 78 % 76 %
Time Outs 0 3 1 0 0 0
Failed 24 17 22 74 24 25
Total Runtime
without Time Outs
4 sec 3 min 50 sec 1 min 40 sec 6 sec 4 sec 20 sec
O(1) O(log n) O(n) O(n log n) O(n2) O(n3) O(n>=4) EXP
Loopus 2 0 51 0 27 1 5 0
KoAT 3 0 43 0 36 3 5 0
CoFloCo 3 0 45 0 34 2 3 0
C4B 0 0 36 0 0 0 0 0
Loopus14 2 0 50 0 28 2 4 0
Rank 3 0 49 0 21 3 2 0
Show examples where
Source FileFunctionLoopusKoATCoFloCoC4BLoopus14Rank
BoundDegreeVariablesTime msBoundDegreeVariablesTime msBoundDegreeVariablesTime msBoundDegreeVariablesTime msBoundDegreeVariablesTime msBoundDegreeVariablesTime ms
ABC_ex01.c foo 1 + max(0, (b + 1 + -a)) O(n) 2 11 V_A + V_B + 4 O(n) 2 218 max([-1*V_a+1*V_b+4,3]) O(n) 2 272 FAILED 17 max(0, (b + 1 + -a)) O(n) 2 500 (1+1)+1+((1+1)+((1+b__o')+(... O(n) 2 7
ABC_ex02.c ex02 1 + max(n, 0) × max(0, (1 ... O(n2) 1 18 6*V_N + 4*V_N^2 + 3 O(n2) 1 1527 max([3, (1*V_n+2)* (1*V_n)+... O(n2) 1 353 FAILED 34 max(n, 0) + max(0, max(n, ... O(n2) 1 500 (((1+1)+(((1/2)*n__o')+((1/... O(n2) 1 12
ABC_ex03.c foo 1 + max(m, 0) × max(0, (1 ... O(n6) 1 31 48675*V_M + 127719*V_M^3 + ... O(n6) 1 4208 max([7, (1*V_m+ -1)*nat((1*... O(n4) 1 951 FAILED 175 max(m, 0) + max(0, max(m, ... O(n4) 1 500 (((1+1)+(((1/2)*m__o')+((1/... O(n4) 1 158
ABC_ex04.c ex04 1 + max(n, 0) × max(0, (( ... O(n8) 1 24 FAILED 15611 FAILED 619 FAILED 48 max(0, max(n, 0) × max(0, ... O(n5) 1 500 FAILED 24
ABC_ex05.c foo 1 + max(n, 0) × max(0, (1 ... O(n2) 1 19 16*V_N + 4*V_N^2 + 3 O(n2) 1 1549 max([3, (1*V_n+2)* (1*V_n)+... O(n2) 1 354 FAILED 30 max(n, 0) + max(0, max(n, ... O(n2) 1 500 (((1+1)+(((1/2)*n__o')+((1/... O(n2) 1 14
ABC_ex06.c foo 1 + max(n, 0) × max(n, 0) ... O(n2) 1 16 26*V_N + 6*V_N^2 + 3 O(n2) 1 1595 max([3, (1*V_n+2)* (1*V_n)+... O(n2) 1 326 FAILED 32 max(n, 0) + max(0, max(n, ... O(n2) 1 500 (1+1)+1+(((1+1)+(((1/2)*n__... O(n2) 1 11
ABC_ex07.c foo 1 + max(n, 0) × max(m, 0) ... O(n2) 2 16 20*V_M + 4*V_M*V_N + 3 O(n2) 2 1382 max([2*V_m+3,3, (1*V_n+2)* ... O(n2) 2 394 FAILED 38 max(m, 0) + max(0, max(n, ... O(n2) 2 500 FAILED 25
ABC_ex08.c foo 1 + max(m, 0) × max(n, 0) ... O(n2) 2 16 40*V_N + 4*V_M*V_N + 3*V_M ... O(n2) 2 1300 max([2*V_n+3,3, (1*V_m+2)* ... O(n2) 2 390 FAILED 46 max(n, 0) + max(0, max(m, ... O(n2) 2 500 ((1+1)+n__o')+1+(((1+1)+(n_... O(n2) 2 22
ABC_ex09.c foo 1 + max(m, 0) × max(n, 0) ... O(n2) 2 16 20*V_N + 4*V_M*V_N + 3 O(n2) 2 1382 max([2*V_n+3,3, (1*V_m+2)* ... O(n2) 2 393 FAILED 40 max(n, 0) + max(0, max(m, ... O(n2) 2 500 FAILED 25
ABC_ex10.c foo 1 + max(m, 0) × max(n, 0) ... O(n2) 2 16 20*V_N + 4*V_M*V_N + 3*V_M ... O(n2) 2 1433 max([2*V_n+3,3, (1*V_m+2)* ... O(n2) 2 396 FAILED 52 max(n, 0) + max(0, max(m, ... O(n2) 2 500 FAILED 25
ABC_ex11.c foo 1 + max(m, 0) × max(n, 0) ... O(n2) 2 12 40*V_N + 4*V_M*V_N + 3*V_M ... O(n2) 2 1302 max([2*V_n+3,3, (1*V_m+2)* ... O(n2) 2 388 FAILED 48 max(n, 0) + max(0, max(m, ... O(n2) 2 500 ((1+1)+n__o')+1+(((1+1)+(n_... O(n2) 2 22
ABC_ex12.c foo 1 + max(n, 0) + max(n, 0) O(n) 1 16 20*V_N + 28 O(n) 1 1234 max([3*V_n+3,3]) O(n) 1 317 FAILED 45 max(n, 0) + max(n, 0) O(n) 1 500 (1+1)+1+(((1+1)+n__o')+n__o... O(n) 1 14
ABC_ex13.c foo 1 + max(0, (d + 1 + -c)) ×... O(n4) 4 28 627672*V_A + 627672*V_B + 8... O(n3) 4 26074 max([-2*V_a+2*V_b+5,3, (-1*... O(n3) 4 1254 FAILED 139 max(0, (b + 1 + -a)) + max(... O(n3) 4 500 ((1+1)+((1+b__o')+(-1*a__o'... O(n3) 4 206
ABC_ex14.c ex14 1 + max(m, 0) × max(n, 0) ... O(n8) 2 33 112*V_N + 72*V_M*V_N + 1360... O(n8) 2 3993 max([2*V_n+3,3,1*V_n*nat(1*... O(n4) 2 989 FAILED 230 max(n, 0) + max(0, max(m, ... O(n4) 2 500 FAILED 279
ABC_ex15.c foo 1 + max(m, 0) × max(n, 0) ... O(n5) 4 30 2140*V_N + 3220*V_M*V_N + 1... O(n5) 4 3675 max([2*V_n+3,3,1*V_n*nat(1*... O(n4) 3 2052 FAILED 256 max(n, 0) + max(0, max(m, ... O(n4) 4 500 (((((1+1)+((((((3/4)+((-1/2... O(n4) 3 1287
C4B-2015_gcd.c gcd 1 + max(x, 0) + max(y, 0) O(n) 2 21 2*V_X + 2*V_Y + 4 O(n) 2 687 max([1*V_x+1*V_y+2,3]) O(n) 2 365 1.00*|[0, x]|+1.00*|[0, y]| O(n) 2 6 max(x, 0) + max(y, 0) O(n) 2 500 ((1+1)+y__o')+1+(((1+1)+(-1... O(n) 2 21
C4B-2015_knuth-morris-pratt.c srch 2 + max(n, 0) + max(n, 0) O(n) 1 27 332*V_N + 144*V_N^2 + 16*V_... O(n3) 1 1489 max([7,nat(min([-1*V_m+1*V_... O(n2) 1 11271 2.00*|[0, n]| O(n) 1 30 FAILED 500 not analyzed
C4B-2015_t07.c start 1 + 2 × max(x, 0) + 2 × m... O(n) 2 35 4*V_X + 3*V_Y + 5 O(n) 2 759 FAILED 492 3.00*|[0, x]|+1.00*|[0, y]| O(n) 2 13 max(x, 0) + max(0, (y + 2 ... O(n) 2 500 (((1+1)+-1)+x__o')+1+((1+1)... O(n) 1 10
C4B-2015_t08.c start 1 + max(0, (y + -2)) + max(... O(n) 2 21 3*V_Y + 3*V_Z + 4 O(n) 2 527 max([-1*V_y+2*V_z+2,1*V_y+2... O(n) 2 371 1.33*|[y, z]|+0.33*|[0, y]| O(n) 1 13 max(0, (max(0, (y + -2)) + ... O(n) 2 500 ((1+1)+-1)+1+(((1+1)+-1)+(z... O(n) 2 9
C4B-2015_t10.c start 1 + max(0, (x - y)) O(n) 2 8 3*V_X + 3*V_Y + 5 O(n) 2 1228 max([1*V_x+ -1*V_y+3,3]) O(n) 2 346 1.00*|[y, x]| O(n) 2 9 max(0, (x - y)) O(n) 2 500 (1+1)+1+(((1+1)+((-1*y__o')... O(n) 2 10
C4B-2015_t11.c start 1 + max(0, (n - x)) + max(0... O(n) 4 16 2*V_M + 2*V_N + 2*V_X + 2*V... O(n) 4 642 max([1*V_m+1*V_n+ -1*V_x+ -... O(n) 4 471 1.00*|[x, n]|+1.00*|[y, m]| O(n) 3 14 max(0, (n - x)) + max(0, (m... O(n) 4 500 ((1+1)+((-1*x__o')+n__o'))+... O(n) 4 27
C4B-2015_t13.c start 1 + max(x, 0) + max(x, 0) +... O(n) 2 19 6*V_X + 6*V_X^2 + 6*V_X*V_Y... O(n2) 2 3295 max([3,2*V_x+nat(1*V_x+1*V_... O(n) 2 465 2.00*|[0, x]|+1.00*|[0, y]| O(n) 2 13 max(x, 0) + max(0, (max(x, ... O(n) 2 500 ((((1+1)+-1)+(((((-1/2)*y__... O(n2) 2 22
C4B-2015_t15.c start FAILED 14 18*V_X + 10*V_Y + 9*V_X*V_Y... O(n2) 2 1615 FAILED 484 1.00*|[0, x]| O(n) 1 15 FAILED 500 ((1+1)+((-1*y__o')+x__o'))+... O(n) 2 28
C4B-2015_t16.c start FAILED 14 18*V_X + 10*V_Y + 9*V_X*V_Y... O(n2) 2 1616 FAILED 485 1.00*|[0, x]| O(n) 1 13 FAILED 500 ((1+1)+((-1*y__o')+x__o'))+... O(n) 2 28
C4B-2015_t19.c start 1 + max(0, (i + -100)) + ma... O(n) 2 20 V_I + V_K + 155 O(n) 2 755 max([1*V_i+1*V_k+55,4,1*V_i... O(n) 2 360 1.00*|[-1, i]|+1.00*|[0, k]| O(n) 2 16 max(0, (i + -100)) + max(0,... O(n) 2 500 ((1+1)+((51+k__o')+i__o'))+... O(n) 2 18
C4B-2015_t20.c start 1 + max(0, (y - x)) + max(0... O(n) 2 26 3*V_X + 4*V_Y + 4 O(n) 2 460 max([1*V_x+ -1*V_y+4,4,-1*V... O(n) 2 350 1.00*|[x, y]|+1.00*|[y, x]| O(n) 2 11 max(0, (max(0, (y - x)) + m... O(n) 2 500 not analyzed
C4B-2015_t27.c start 1 + 1000 × max(0, -n) + ma... O(n) 2 19 204*V_N + 10404102*V_N^2 + ... O(n2) 2 2478 max([-12*V_n+1/100*V_y+13,3... O(n) 2 757 11.00*|[n, 0]|+0.01*|[0, y]| O(n) 2 12 max(0, (1000 + 1000 × max(... O(n) 2 500 FAILED 45
C4B-2015_t28.c start 1 + 1000 × max(0, (x - y))... O(n) 2 38 1004*V_X + 1002*V_Y + 6 O(n) 2 1124 max([1001*V_x+ -1000*V_y+40... O(n) 2 609 1.00*|[x, 0]|+1002.00*|[y, ... O(n) 2 19 max(0, ( 1000 × max(0, (x -... O(n) 2 500 (((1+1)+-1)+((-1*y__o')+x__... O(n) 2 55
C4B-2015_t30.c start 1 + max(x, y, 0) O(n) 2 18 FAILED 5363 FAILED 289 1.00*|[0, x]|+1.00*|[0, y]| O(n) 2 10 max(0, (1 + max(x, y, 0))) O(n) 2 500 (1+1)+1+((1+1)+x__o')+1 O(n) 1 8
C4B-2015_t46.c start 1 + max(y, 0) + max(y, 0) +... O(n) 2 33 FAILED 8111 FAILED 553 2.00*|[0, x]|+3.00*|[0, y]| O(n) 2 12 max(y, 0) + max(y, 0) O(n) 1 500 ((((1+1)+(y__o'+x__o'))+-1)... O(n) 2 112
KoAT-2013_sect1-lin.c sect1lin 1 + max(n, 0) + max(n, 0) O(n) 1 23 2*V_N + 4 O(n) 1 623 max([2*V_n+4,4]) O(n) 1 345 2.00*|[0, n]| O(n) 1 18 max(n, 0) + max(n, 0) O(n) 1 500 (((1+1)+n__o')+n__o')+1+(1+... O(n) 1 12
KoAT-2013_sect1-quad.c sect1quad 1 + max(n, 0) × max(0, (n ... O(n2) 1 25 2*V_N + V_N^2 + 4 O(n2) 1 771 FAILED 347 FAILED 36 max(n, 0) + max(0, max(n, ... O(n2) 1 500 (1+1)+1+(((1+1)+-1)+n__o')+1 O(n) 1 12
KoAT-2013_sect2.c sect2 1 + max(n, 0) × max(0, (-1... O(n2) 1 29 161*V_N + 392*V_N^2 + 17 O(n2) 1 2018 max([7, (1*V_n+1)* (1*V_n+ ... O(n2) 1 497 FAILED 35 max(n, 0) + max(n, 0) + max... O(n2) 1 500 ((((1+1)+n__o')+(((-1/2)*n_... O(n2) 1 46
Loopus-2011_Example1.c Example1 1 + max(n, 0, min(n, (n + -... O(n) 1 42 22*V_N + 15 O(n) 1 2418 max([4*V_n+4,1*V_n+8,6]) O(n) 1 647 2.00*|[0, n]| O(n) 1 27 max(0, min(n, (n + -1))) + ... O(n) 1 500 ((((1+1)+n__o')+(-1+n__o'))... O(n) 1 84
Loopus-2011_Example2.c bin_search_StepSize2 FAILED 21 FAILED 31130 TIMEOUT FAILED 54 FAILED 500 not analyzed
Loopus-2011_Example3.c Example3 1 + max(x, 0) + max(0, (255... O(n) 1 19 4*V_X + 1015*V_B + 764 O(n) 2 851 max([1*V_x+3,3,-1*V_x+258]) O(n) 1 380 FAILED 8 max(x, 0) + max(0, (max(x, ... O(n) 1 500 FAILED 20
Loopus-2014_fig1.c fig1 FAILED 32 TIMEOUT FAILED 2798 FAILED 49 max(n, 0) + max(n, 0) + max... O(n2) 1 500 (((1+1)+-1)+n__o')+1+(1+1)+... O(n) 1 514
Loopus-2014_fig2.c fig2 1 + max(m, 0) + max(m, 0) O(n) 1 23 9*V_M + 12*V_M^2 + 3 O(n2) 1 1531 max([3*V_m+3,3]) O(n) 1 518 2.00*|[0, m]| O(n) 1 24 max(m, 0) + max(m, 0) O(n) 1 500 ((((1+1)+(1+(2*m__o')))+(-3... O(n) 1 92
Loopus-JAR_break.c foo 1 + max(n, 0) O(n) 1 10 V_N + 3 O(n) 1 259 max([1*V_n+3,3]) O(n) 1 260 1.00*|[0, n]| O(n) 1 8 max(n, 0) O(n) 1 500 ((1+1)+n__o')+1+(1+1)+1 O(n) 1 7
Loopus-JAR_twoCounters.c twoCounters 1 + max(n, 0) + max(n, 0) O(n) 1 15 11*V_N + 8 O(n) 1 852 max([4*V_n+1,3]) O(n) 1 339 2.00*|[0, n]| O(n) 1 21 max(n, 0) + max(n, 0) O(n) 1 500 (((1+1)+(-3+(2*n__o')))+(-2... O(n) 1 18
Loopus-JAR_twoSCCs.c twoSCCs 1 + 2 × max(n, 0) + max(n,... O(n) 3 39 4*V_N + 3*V_M1 + 3*V_M2 + 6 O(n) 3 890 FAILED 439 1.00*|[0, m1]|+1.00*|[0, m2... O(n) 3 38 max(n, 0) + max(0, ( 2 × ma... O(n) 3 500 FAILED 81
Loopus-JAR_xnu.c xnu 1 + max(len, 0) + max(len, ... O(n) 1 62 215*V_LEN + 84*V_LEN^2 + 33 O(n2) 1 19923 max([3,max([2*V_len, (1*V_l... O(n2) 1 744 FAILED 132 FAILED 500 FAILED 87
Loopus-JAR_xnusimple.c xnuSimple 1 + max(n, 0) + max(n, 0) +... O(n) 1 19 480*V_N + 28*V_N^2 + 4 O(n2) 1 2392 FAILED 417 2.00*|[0, n]| O(n) 1 31 max(n, 0) + max(0, (max(n, ... O(n) 1 500 (1+1)+1+((((1+1)+(-1+(2*n__... O(n) 1 57
Rank-2010_ex1.c ex1 FAILED 20 FAILED 6691 max([3,1*V_m+1+max([4*V_m+4... O(n2) 1 749 FAILED 27 1 + max(0, (m + 1)) + max(0... O(n) 1 500 (((1+1)+((6+(5*m__o'))+(m__... O(n2) 1 40
Rank-2010_ex2.c ex2 1 + max(0, (m + -1)) + max(... O(n) 1 28 25*V_M + 10 O(n) 1 2784 max([3*V_m+2,3]) O(n) 1 596 FAILED 25 max(0, (m + -1)) + max(0, (... O(n) 1 500 FAILED 31
Rank-2010_ex3.c ex3 FAILED 69 TIMEOUT max([3,nat(nat(min([3/4*V_m... O(n2) 1 7861 FAILED 60 FAILED 500 FAILED 144
SPEED_CAV09_ex1.c foo 101 + max(m, 0) O(n) 1 15 2*V_M + 201 O(n) 1 584 max([1*V_m+103,103]) O(n) 1 336 1.00*|[0, m]| O(n) 1 14 100 + max(m, 0) O(n) 1 500 ((1+1)+100)+1+(((1+1)+m__o'... O(n) 1 13
SPEED_CAV09_ex2.c foo 1 + max(n, 0) × max(m, 0) ... O(n2) 2 18 V_M*V_N + V_M + V_N + 3 O(n2) 2 586 max([3,1*V_n+nat(1*V_n* (1*... O(n2) 2 333 FAILED 14 max(n, 0) + max(0, ( max(n,... O(n2) 2 500 ((1+1)+n__o')+1+(1+1)+1+(((... O(n2) 2 26
SPEED_CAV09_ex3.c foo 1 + max(n, 0) + max(n, 0) O(n) 1 23 FAILED 29595 FAILED 706 FAILED 25 max(n, 0) + max(n, 0) O(n) 1 500 (1+1)+1+(((1+1)+(1+n__o'))+... O(n) 1 14
SPEED_PLDI09_cyclic.c cyclic FAILED 17 FAILED 5852 FAILED 520 FAILED 11 FAILED 500 not analyzed
SPEED_PLDI09_Example2.c Example2 FAILED 12 6*V_N + 7 O(n) 1 2437 max([2*V_n+3,4]) O(n) 1 458 FAILED 29 FAILED 500 (((1+1)+n__o')+(n__o'+(-1*m... O(n) 2 50
SPEED_PLDI09_Example3.c Example3 1 + max(n, 0) × max(m, 0) ... O(n2) 2 20 2*V_N + 4*V_M*V_N + 2*V_M +... O(n3) 2 2724 max([4,1*V_n+nat(1*V_n* (1*... O(n2) 2 452 FAILED 18 max(n, 0) + max(0, ( max(m,... O(n2) 2 500 not analyzed
SPEED_PLDI09_Example4.c Example4 FAILED 15 FAILED 19129 FAILED 520 FAILED 12 FAILED 500 not analyzed
SPEED_PLDI09_Example5.c Example5 1 + max(m, 0) + max(0, (n -... O(n) 2 19 3*V_M + V_N + 7 O(n) 2 1044 max([-1*V_m+1*V_n+4,3,1*V_m... O(n) 2 481 FAILED 13 max(m, 0) + max(0, (max(m, ... O(n) 2 500 FAILED 216
SPEED_PLDI09_Example6.c Example6 1 + max(m, 0) + max(m, 0) +... O(n) 2 27 12*V_N + 10*V_M + 9 O(n) 2 5305 max([3,nat(1*V_m+1*V_n)+max... O(n2) 1 828 FAILED 115 max(m, 0) + max(m, 0) + max... O(n) 2 500 (((((1+1)+-1)+-1)+-1)+-1)+1... O(1) 0 527
SPEED_PLDI09_NestedLoop.c nestedLoop 1 + max(m, 0) × max(n, 0) ... O(n2) 3 42 TIMEOUT max([3*V_n+4,4,nat(min([1*V... O(n2) 3 3162 FAILED 88 max(0, max(m, 0) × max(0, ... O(n2) 3 500 FAILED 193
SPEED_PLDI10_Ex1.c Ex1 1 + max(n, 0) × max(0, (n ... O(n2) 1 27 FAILED 9033 max([5,1*V_n+ -2+ (1*V_n+1)... O(n2) 1 573 FAILED 19 max(n, 0) + max(0, max(n, ... O(n2) 1 500 FAILED 17
SPEED_PLDI10_Ex2.c Ex2 FAILED 17 FAILED 16304 FAILED 604 FAILED 32 FAILED 500 FAILED 35
SPEED_PLDI10_Ex3.c Ex3 FAILED 16 FAILED 2342 FAILED 516 FAILED 16 FAILED 500 not analyzed
SPEED_PLDI10_Ex4.c foo FAILED 20 26*V_N + 12 O(n) 1 1884 max([3*V_n+5,1*V_n+7,5]) O(n) 1 685 FAILED 13 FAILED 500 FAILED 9
SPEED_PLDI10_Ex5.c Ex5 FAILED 23 FAILED 9201 FAILED 573 FAILED 50 FAILED 500 FAILED 144
SPEED_PLDI10_Ex6.c Ex6 1 + max(0, (x + 1 + -z)) + ... O(n) 3 16 4*V_N + 2*V_X + 2*V_Z + 3 O(n) 3 587 max([3,1*V_n+ -1*V_x+nat(1*... O(n) 2 364 1.00*|[x, n]|+1.00*|[z, n]| O(n) 3 9 max(0, (max(0, (x + 1 + -z)... O(n) 3 500 (1+1)+1+(((1+1)+((-1*x__o')... O(n) 3 32
SPEED_PLDI10_Ex7.c foo FAILED 18 10*V_M + 2*V_M^2 + 14 O(n2) 1 1440 max([1*V_m+5,3]) O(n) 1 407 FAILED 21 FAILED 500 FAILED 23
SPEED_POPL09_Dis1.c Dis1 1 + max(0, (n - x0)) + max(... O(n) 4 15 2*V_M + 2*V_N + 2*V_X0 + 2*... O(n) 4 658 max([1*V_m+1*V_n+ -1*V_x0+ ... O(n) 4 471 1.00*|[x0, n]|+1.00*|[y0, m]| O(n) 4 20 max(0, (n - x0)) + max(0, (... O(n) 4 500 ((1+1)+((-1*x0__o')+n__o'))... O(n) 4 42
SPEED_POPL09_Dis2.c Dis2 1 + max(0, (x0 + 1 + -z0)) ... O(n) 3 16 4*V_N + 2*V_X0 + 2*V_Z0 + 3 O(n) 3 586 max([3,1*V_n+ -1*V_x0+nat(1... O(n) 2 363 1.00*|[x0, n]|+1.00*|[z0, n]| O(n) 3 19 max(0, (max(0, (x0 + 1 + -z... O(n) 3 500 (((1+1)+((-1*x0__o')+n__o')... O(n) 3 36
SPEED_POPL09_NestedMultiple.c NestedMultiple 1 + max(0, (m - y0)) + max(... O(n) 4 24 21*V_N + 21*V_X0 + 15*V_M +... O(n) 4 970 max([1*V_m+3*V_n+ -3*V_x0+ ... O(n) 4 1148 1.00*|[x0, n]|+1.00*|[y0, m]| O(n) 4 33 max(0, (m - y0)) + max(0, (... O(n) 4 500 (1+1)+1+(((1+1)+((-1*x0__o'... O(n2) 4 34
SPEED_POPL09_NestedMultipleDep.c foo 1 + max(m, 0) × max(n, 0) ... O(n2) 2 16 8*V_N + 4*V_M*V_N + 4*V_M + 11 O(n2) 2 1626 max([2*V_n+3,3, (1*V_m+2)* ... O(n2) 2 433 FAILED 38 max(n, 0) + max(0, max(m, ... O(n2) 2 500 (((1+1)+(n__o'*m__o'))+n__o... O(n2) 2 23
SPEED_POPL09_NestedSingle.c NestedSingle 1 + max(n, 0) + max(n, 0) O(n) 1 22 FAILED 31045 FAILED 655 FAILED 10 max(n, 0) + max(n, 0) O(n) 1 500 FAILED 8
SPEED_POPL09_SequentialSingle.c SequentialSingle 1 + max(n, 0) + max(n, 0) O(n) 1 27 3*V_N + 5 O(n) 1 571 max([1*V_n+4,4]) O(n) 1 361 1.00*|[0, n]| O(n) 1 9 max(n, 0) + max(n, 0) O(n) 1 500 (((1+1)+n__o')+n__o')+1+(1+... O(n) 1 11
SPEED_POPL09_SimpleMultiple.c SimpleMultiple 1 + max(n, 0) + max(m, 0) O(n) 2 15 V_M + V_N + 3 O(n) 2 582 max([1*V_m+1*V_n+3,3,1*V_n+... O(n) 2 391 1.00*|[0, m]|+1.00*|[0, n]| O(n) 2 16 max(n, 0) + max(m, 0) O(n) 2 500 ((1+1)+n__o')+1+(((1+1)+m__... O(n) 2 27
SPEED_POPL09_SimpleMultipleDep.c foo 1 + max(n, 0) × max(m, 0) ... O(n2) 2 17 V_M*V_N + V_M + V_N + 3 O(n2) 2 587 max([3,1*V_n+nat(1*V_n* (1*... O(n2) 2 332 FAILED 16 max(n, 0) + max(0, ( max(n,... O(n2) 2 500 (1+1)+1+((1+1)+n__o')+1+(1+... O(n2) 2 39
SPEED_POPL09_SimpleSingle.c SimpleSingle 1 + max(n, 0) O(n) 1 11 V_N + 3 O(n) 1 189 max([1*V_n+3,3]) O(n) 1 257 1.00*|[0, n]| O(n) 1 10 max(n, 0) O(n) 1 500 (1+1)+1+(((1+1)+n__o')+n__o... O(n) 1 11
SPEED_POPL09_SimpleSingle2.c SimpleSingle2 1 + max(n, 0) + max(m, 0) O(n) 2 19 6*V_N + 6*V_M + 8 O(n) 2 1030 max([1*V_n+4,4,1*V_m+4]) O(n) 2 683 1.00*|[0, m]|+1.00*|[0, n]| O(n) 2 22 max(n, 0) + max(m, 0) O(n) 2 500 ((1+1)+n__o')+1+((1+1)+((-1... O(n) 2 108
WTC_aaron2.c aaron2 1 + max(0, (x + 1 + -y)) O(n) 2 19 3*V_X + 3*V_Y + 9 O(n) 2 1163 max([1*V_x+ -1*V_y+5,4]) O(n) 2 398 FAILED 15 max(0, (x + 1 + -y)) O(n) 2 500 (1+1)+1+(((1+1)+((1+(-1*y__... O(n) 2 25
WTC_ax.c ax 1 + max(0, (n + -2)) × max... O(n2) 1 16 12*V_N + 4*V_N^2 + 10 O(n2) 1 1516 max([8,2*V_n+ -2+ (2*V_n+1)... O(n2) 1 332 FAILED 40 max(0, (n + -2)) + max(0, (... O(n2) 1 500 ((1+1)+((1+(-2*n__o'))+(n__... O(n2) 1 17
WTC_complex.c complex 1 + 12 × max(0, (30 - a)) ... O(n) 2 28 FAILED 20149 max([3,max([-4*V_a+56+max([... O(n2) 2 9010 FAILED 56 max(0, ( 12 × max(0, (30 - ... O(n) 2 500 (((1+1)+-1)+-1)+1+(((1+1)+-... O(n) 2 42
WTC_counterex1.c counterex1b FAILED 27 FAILED 8477 FAILED 2227 FAILED 22 FAILED 500 ((((1+1)+-1)+-1)+(1+x__o'))+1 O(n) 1 58
WTC_cousot9.c cousot9 1 + max(N, 0) × max(N, 0) ... O(n2) 2 18 V_N^2 + V_J + V_N + 3 O(n2) 2 677 max([3,nat(1*V_N* (1*V_N)+1... O(n2) 2 344 FAILED 10 max(N, 0) + max(0, ( max(N,... O(n2) 2 500 (((1+1)+-1)+N__o')+1+(1+1)+1 O(n) 1 26
WTC_determinant.c determinant 1 + max(0, (-2 + min((a + ... O(n3) 1 27 969*V_A + 1992*V_A^2 + 1776... O(n4) 1 3054 max([3, (1*V_a+ -1)*nat((1*... O(n3) 1 1014 FAILED 1364 max(0, (-1 + min(a, (a + 1)... O(n3) 1 500 ((((1+1)+(-1+a__o'))+(((-1/... O(n3) 1 680
WTC_easy1.c easy1 41 O(1) 0 13 123 O(1) 0 692 43 O(1) 0 322 FAILED 18 40 O(1) 0 500 FAILED 19
WTC_easy2.c easy2 1 + max(z, 0) O(n) 1 10 V_Z + 3 O(n) 1 259 max([1*V_z+3,3]) O(n) 1 259 1.00*|[0, z]| O(n) 1 16 max(z, 0) O(n) 1 500 ((1+1)+z__o')+1+(1+1)+1 O(n) 1 7
WTC_exmini.c exmini 1 + max(0, (101 + max(-i, -... O(n) 2 21 V_I + V_J + V_K + 105 O(n) 3 430 max([-1/2*V_i+ -1/2*V_j+1/2... O(n) 3 473 FAILED 22 max(0, (101 + max(-i, -j))) O(n) 2 500 ((1+1)+(((101+k__o')+(-1*j_... O(n) 3 12
WTC_gcd.c gcd 1 + max(x, 0) + max(y, 0) O(n) 2 26 2*V_Y + 6*V_X + 8 O(n) 2 1452 max([1*V_x+1*V_y+2,4]) O(n) 2 399 1.00*|[0, x]|+1.00*|[0, y]| O(n) 2 10 max(y, 0) + max(x, 0) O(n) 2 500 ((1+1)+1)+1+(((1+1)+(-1+x__... O(n) 2 73
WTC_insertsort.c insertsort 1 + max(0, (length + -1)) ... O(n2) 1 22 20*V_LENGTH + 2*V_LENGTH^2 + 3 O(n2) 1 680 max([3,max([3*V_length+ -3,... O(n2) 1 446 FAILED 23 max(0, (length + -1)) + max... O(n2) 1 500 ((((1+1)+(((-1/2)*length__o... O(n2) 1 27
WTC_loops.c loops FAILED 17 60*V_N + 10*V_N^2 + 6 O(n2) 1 2130 max([8, (1*V_n+ -1)* (2*V_n... O(n2) 1 405 FAILED 341 FAILED 500 (((1+1)+(1+n__o'))+((-1*n__... O(n2) 1 15
WTC_maccarthy91.c sipma91 1 + 10 × max(0, (101 - x))... O(n) 1 33 1660*V_X + 3*V_X^2 + 144385 O(n2) 1 2747 max([67/11,-1/11*V_x+101/11... O(n) 1 636 FAILED 4 max(0, ( 9 × max(0, (101 - ... O(n) 1 500 FAILED 240
WTC_nd_loop.c nd_loop FAILED 17 14 O(1) 0 179 12 O(1) 0 278 FAILED 32 FAILED 500 (((1+1)+10)+9)+1 O(1) 0 6
WTC_ndecr.c ndecr 1 + max(0, (n + -2)) O(n) 1 11 V_N + 3 O(n) 1 289 max([1*V_n+1,3]) O(n) 1 258 1.00*|[0, n]| O(n) 1 9 max(0, (n + -2)) O(n) 1 500 ((1+1)+(-2+n__o'))+1+(1+1)+1 O(n) 1 7
WTC_nestedLoop.c nestedLoop 1 + max(m, 0) × max(n, 0) ... O(n2) 3 26 28*V_N + 4*V_N*V_M + 6*V_N ... O(n2) 2 85160 max([1*V_N+2*V_m+6,2*V_n+4,... O(n2) 3 1222 FAILED 47 max(0, max(m, 0) × max(0, ... O(n2) 3 500 FAILED 195
WTC_perfect.c perfect FAILED 14 8*V_X + 4*V_X^2 + 7 O(n2) 1 2713 max([3,max([ (1*V_x+1)* (1*... O(n2) 1 618 FAILED 70 FAILED 500 FAILED 36
WTC_random1d.c random1d 1 + max(max, 0) O(n) 1 7 3*V_MAX + 5 O(n) 1 493 max([1*V_max+4,3]) O(n) 1 264 FAILED 15 max(max, 0) O(n) 1 500 (1+1)+1+((1+1)+max__o')+1 O(n) 1 9
WTC_random2d.c random2d 1 + max(N, 0) O(n) 1 10 6*V_N + 3 O(n) 1 1667 max([1*V_N+3,3]) O(n) 1 281 1.00*|[0, N]| O(n) 1 39 max(N, 0) O(n) 1 500 (((((((1+1)+N__o')+N__o')+N... O(n) 1 167
WTC_realbubble.c realbubble 1 + max(0, (length + -2)) ... O(n2) 1 22 1185*V_LENGTH + 168*V_LENGT... O(n2) 1 861 max([2*V_length+3,4, (1*V_l... O(n2) 1 549 FAILED 33 max(0, (length + -1)) + max... O(n2) 1 500 ((((1+1)+(((-1/2)*length__o... O(n2) 1 63
WTC_realheapsort.c realheapsort FAILED 84 146*V_N^2 + 184*V_N + 63 O(n2) 1 71827 FAILED 1272 FAILED 425 FAILED 500 FAILED 112
WTC_realheapsort_step1.c realheapsort_step1 1 + max(0, (N + -1)) × max... O(n2) 1 27 146*V_N + 8*V_N^2 + 5 O(n2) 1 56858 max([3,max([3*V_N+ -3, (1*V... O(n2) 1 496 FAILED 26 max(0, (N + -1)) + max(0, ... O(n2) 1 500 FAILED 166
WTC_realheapsort_step2.c realheapsort_step2 FAILED 53 216*V_N^2 + 12*V_N + 5 O(n2) 1 11380 FAILED 675 FAILED 255 FAILED 500 (1+1)+1+((((1+1)+((-3+((1/2... O(n2) 1 695
WTC_realselect.c realselect 1 + max(0, (array_size + -... O(n2) 1 16 96*V_ARRAY_SIZE + 12*V_ARRA... O(n2) 1 1985 max([3, (1*V_array_size+1)*... O(n2) 1 330 FAILED 30 max(0, (array_size + -1)) +... O(n2) 1 500 ((((1+1)+(-1+array_size__o'... O(n) 1 47
WTC_realshellsort.c realshellsort FAILED 24 36*V_ARRAY_SIZE^2 + 144*V_A... O(n4) 1 5766 FAILED 1128 FAILED 75 FAILED 500 (((((((1+1)+-1)+-1)+(((-1/6... O(n3) 1 249
WTC_relation1.c relation1 1 O(1) 0 6 3 O(1) 0 39 3 O(1) 0 215 FAILED 27 1 O(1) 0 500 ((1+1)+1)+1 O(1) 0 4
WTC_rsd.c rsd 1 + max(0, ( r × 2 - r)) ×... O(n2) 1 20 FAILED 3354 max([3,1*V_r+1+nat(min([1*V... O(n2) 1 350 FAILED 40 max(0, ( max(0, ( r × 2 - r... O(n2) 1 500 (((1+1)+((1+((3/2)*r__o'))+... O(n2) 1 27
WTC_sipmabubble.c sipmabubble 1 + max(n, 0) × max(0, (n ... O(n2) 1 18 1308*V_N + 544*V_N^2 + 43 O(n2) 1 1419 max([6, (2*V_n+2)* (1*V_n)+... O(n2) 1 356 FAILED 40 max(0, (n + 1)) + max(0, m... O(n2) 1 500 ((1+1)+(1+n__o'))+1+((((1+1... O(n2) 1 35
WTC_speedFails4.c speedFails4 FAILED 15 FAILED 6150 FAILED 401 FAILED 29 FAILED 500 ((1+1)+((1+(-1*x__o'))+n__o... O(n) 2 30
WTC_speedpldi2.c speedpldi2 FAILED 14 2*V_N + 6 O(n) 1 1168 max([2*V_n+3,4]) O(n) 1 370 FAILED 25 FAILED 500 (1+1)+1+(((1+1)+n__o')+(n__... O(n) 2 33
WTC_speedpldi3.c speedpldi3 1 + max(n, 0) × max(m, 0) ... O(n2) 2 18 V_M*V_N + V_M + V_N + 6 O(n2) 2 652 max([3,nat(min([1*V_n* (1*V... O(n2) 2 396 FAILED 20 max(n, 0) + max(0, ( max(m,... O(n2) 2 500 ((((1+1)+(n__o'*m__o'))+n__... O(n2) 2 49
WTC_speedpldi4.c speedpldi4 FAILED 13 2*V_N + 10*V_M + 6 O(n) 2 1127 max([-1*V_m+1*V_n+5,3,1*V_n... O(n) 2 400 1.00*|[0, n]| O(n) 1 14 FAILED 500 ((1+1)+1)+1+((((1+1)+(-1+m_... O(n) 2 56
WTC_terminate.c terminate 1 + max(0, (101 + max(-i, -... O(n) 2 22 V_I + V_J + V_K + 105 O(n) 3 427 max([-1/2*V_i+ -1/2*V_j+1/2... O(n) 3 472 FAILED 23 max(0, (101 + max(-i, -j))) O(n) 2 500 ((1+1)+(((101+k__o')+(-1*j_... O(n) 3 15
WTC_wcet1.c wcet1 1 + max(0, (n + -1)) O(n) 1 15 14*V_N + 10 O(n) 1 959 max([2*V_n+3,5]) O(n) 1 515 FAILED 25 max(0, (n + -1)) O(n) 1 500 ((1+1)+(-1+n__o'))+1+(1+1)+1 O(n) 1 48
WTC_wcet2.c wcet2 1 + 10 × max(0, (5 - i)) +... O(n) 1 19 375*V_I + 1803 O(n) 1 1798 max([-2*V_i+33,3,-12*V_i+63]) O(n) 1 376 FAILED 16 max(0, 10 × max(0, (3 - i)... O(n) 1 500 (((1+1)+(6+(-1*i__o')))+(54... O(n) 1 862
WTC_while2.c while2 1 + max(N, 0) × max(N, 0) ... O(n2) 1 16 8*V_N + 4*V_N^2 + 3 O(n2) 1 1132 max([3, (1*V_N+2)* (1*V_N)+... O(n2) 1 333 FAILED 36 max(N, 0) + max(0, max(N, ... O(n2) 1 500 (((1+1)+N__o')+(N__o'*N__o'... O(n2) 1 23
WTC_wise.c wise 1 + max(0, (x + -2 + -y)) +... O(n) 2 19 2*V_X + 2*V_Y + 7 O(n) 2 1158 max([1*V_x+ -1*V_y+2,4,-1*V... O(n) 2 396 FAILED 9 max(0, (max(0, (y + -2 + -x... O(n) 2 500 ((1+1)+((-2+(-1*y__o'))+x__... O(n) 2 18