Benchmark Result Comparison

KoAT Loopus
All 669 658
Bounded 321 386
Timeouts 279 6
Failed 69 266
Runtime without Timeouts 621 sec 226 sec
O(1) O(log n) O(n) O(n log n) O(n2) O(n3) O(n>=4) EXP
KoAT 121 0 143 0 54 0 3 0
Loopus 134 0 152 0 81 15 4 0
Show examples where
Source File KoAT Loopus
Bound Degree Time ms Bound Degree Time ms
1.t2.c TIMEOUT FAILED 1000
1394-fail.t2.c TIMEOUT FAILED 1000
1394-succeed.t2.c TIMEOUT FAILED 1000
1394complete-fail.t2.c TIMEOUT FAILED 500
1394complete-succeed.t2.c TIMEOUT FAILED 1000
2.t2.c TIMEOUT FAILED 500
232.t2.c A^2 + 3*A + 2 O(n2) 207 -2 + (-2 + max(call_to_non... O(n2) 500
241.t2.c A^2 + 3*A + 2 O(n2) 208 -2 + (-2 + max(call_to_non... O(n2) 500
3.t2.c FAILED 121 FAILED 500
5.t2.c TIMEOUT 1 (no loops) O(1) 500
6.t2.c FAILED 130 FAILED 500
7.t2.c TIMEOUT FAILED 500
ABC_ex01.c 4*A + 4*B + 6 O(n) 138 a - b O(n) 500
ABC_ex02.c 69*B + 72*B^2 + 19 O(n2) 344 b + -1 + b × (b + -1) O(n2) 500
ABC_ex03.c 964348*B + 2666040*B^2 + 37... O(n6) 852 b + -1 + (b + -1) × (-1 + ... O(n4) 500
ABC_ex04.c TIMEOUT -1 + (n + -1) × (-1 + (( n... O(n5) 500
ABC_ex05.c 141*B + 72*B^2 + 66 O(n2) 365 b + -1 + (b + -1) × (-1 + ... O(n2) 500
ABC_ex06.c 137*B + 84*B^2 + 58 O(n2) 313 b + -1 + (b + -2) × (b + -1) O(n2) 500
ABC_ex07.c 33*B + 12*B*D + 8*D + 26 O(n2) 375 b + -1 + (b + -1) × (d + -1) O(n2) 500
ABC_ex08.c 21*A + 12*A*B + 4*B + 11 O(n2) 273 a + -1 + (a + -1) × (b + -1) O(n2) 500
ABC_ex09.c 33*B + 12*B*D + 8*D + 26 O(n2) 372 b + -1 + (d + -1) × (b + -1) O(n2) 500
ABC_ex10.c 33*A + 12*A*B + 4*B + 15 O(n2) 320 b + -1 + (a + -1) × (b + -1) O(n2) 500
ABC_ex11.c 21*A + 12*A*B + 4*B + 11 O(n2) 278 a + -1 + (a + -1) × (b + -1) O(n2) 500
ABC_ex12.c 21*A + 24*A*B + 8*B + 11 O(n2) 279 0 O(1) 500
ABC_ex13.c 239*A + 231*B + 1280*A*D + ... O(n4) 704 b + (b - a) × (d - c) + (... O(n3) 500
ABC_ex14.c 4249295*A + 10229904*A*B + ... O(n8) 809 b + -1 + (a + -1) × (b + -... O(n4) 500
ABC_ex15.c TIMEOUT n + -1 + (n + -1) × (m + -... O(n4) 500
FGPSF09-Beerendonk_01.c A + B + 1 O(n) 102 a + -1 + -b O(n) 500
FGPSF09-Beerendonk_02.c A + B + 1 O(n) 139 a + -1 + -b O(n) 500
FGPSF09-Beerendonk_03.c A + B + 1 O(n) 114 a + -1 + -b O(n) 500
FGPSF09-Beerendonk_04.c 2 O(1) 22 a + -1 + -b O(n) 500
FGPSF09-Beerendonk_05.c 2 O(1) 23 1 O(1) 500
FGPSF09-Beerendonk_06.c 2 O(1) 23 1 O(1) 500
FGPSF09-Beerendonk_07.c 2 O(1) 22 1 O(1) 1000
FGPSF09-Beerendonk_08.c A + 1 O(n) 124 b + -1 O(n) 500
FGPSF09-Beerendonk_09.c B + C + 1 O(n) 154 a + -1 + -b O(n) 500
FGPSF09-Beerendonk_10.c 2*A + 2 O(n) 121 FAILED 500
FGPSF09-Beerendonk_11.c B + 6 O(n) 160 b + b + 1 + max(-1, min(-1,... O(n) 500
FGPSF09-Beerendonk_13.c A + 2 O(n) 108 a + max(-1, min(-1, (-1 - b))) O(n) 500
FGPSF09-Beerendonk_15.c 2*A + 2*B + 1 O(n) 172 b + a + -1 O(n) 500
FGPSF09-Beerendonk_16.c 2*A + 2*B + 2*C + 1 O(n) 184 a + b + -1 + -c O(n) 500
FGPSF09-Beerendonk_17.c 3*A + 3*B + 1 O(n) 313 b + a + -2 + a × 2 O(n) 500
FGPSF09-Beerendonk_18.c 2*A + B + 2 O(n) 333 a + b + -2 O(n) 500
FGPSF09-Beerendonk_19.c 2*A + 3*B + C + 2 O(n) 378 c + a + -2 + -b + -b O(n) 500
FGPSF09-Beerendonk_20.c A + 3 O(n) 152 a + a + -2 O(n) 500
FGPSF09-Beerendonk_21.c A + B + 3 O(n) 170 a + a + -2 + -b + -b O(n) 500
FGPSF09-Beerendonk_22.c 4*A + B + 7 O(n) 169 FAILED 500
FGPSF09-Beerendonk_23.c 4*A + 5*B + C + 7 O(n) 208 FAILED 500
FGPSF09-Beerendonk_24.c 2*A + 2*B + 7 O(n) 201 a + a + b + b + -4 O(n) 500
FGPSF09-CAV02_practical1.c 13*A + 12*A^2 + 4 O(n2) 232 a + a × (a + -1) O(n2) 500
FGPSF09-CAV02_practical2.c 4137*B + 20*B^2 + 211282 O(n2) 2638 309 + 9 × (99 - b) + -b + ... O(n) 500
FGPSF09-CAV05_c.05.c 2*A + 2*B + 3 O(n) 276 a + -2 O(n) 1000
FGPSF09-ESOP08_abstractions.c TIMEOUT a + -1 O(n) 500
FGPSF09-LICS04_c.01.c 12*A + 2*A^2 + 17 O(n2) 191 a + a × (a + -2) O(n2) 500
FGPSF09-LICS04_choice.c TIMEOUT a + -1 O(n) 500
FGPSF09-PLDI06_c.03.c 5*A + 2*B + 3*C + 4 O(n) 210 a + -1 + max(b, a) + -b + -c O(n) 500
FGPSF09-PLDI06_c.04.c A + B + 2 O(n) 144 a + -1 + -b O(n) 500
FGPSF09-RTA08_round.c FAILED 192 not analyzed
FGPSF09-SAS05_c.02.c 32*A + 6*A^2 + 41 O(n2) 302 a + a × (a + -1) O(n2) 500
FGPSF09-TACAS01_terminate.c A + B + C + 102 O(n) 153 100 - a O(n) 500
FGPSF09-VMCAI04_complete1.c A + B + 1 O(n) 117 a + -1 + -b O(n) 500
FGPSF09-VMCAI04_complete2.c TIMEOUT FAILED 500
FGPSF09-VMCAI04_complete3.c 13*A + 12*A^2 + 4 O(n2) 234 a + a × (a + -1) O(n2) 500
FGPSF09-VMCAI04_complete4.c TIMEOUT b + a + a × max(call_to_no... O(n2) 500
FGPSF09-VMCAI05_poly1.c TIMEOUT FAILED 500
FGPSF09-VMCAI05_poly2.c TIMEOUT FAILED 500
FGPSF09-VMCAI05_poly3.c TIMEOUT FAILED 1000
FGPSF09-VMCAI05_poly4.c 2*A + 2*B + 2*C + 2*D + 1 O(n) 588 c + a + -2 + -b + -d O(n) 500
FGPSF09-new_randomFullUpDown.c FAILED 702 not analyzed
FGPSF09-new_unsatCond2.c FAILED 109 FAILED 500
FGPSF09-patrs-pasta_a.01.c 7*A + 2*A^2 + 7 O(n2) 221 a + -1 + (a + -2) × (a + -1) O(n2) 500
FGPSF09-patrs-pasta_a.02.c TIMEOUT FAILED 500
FGPSF09-patrs-pasta_a.03.c 120*A + 142*B + 22*A*B + 12... O(n2) 760 b + b + a + a + -8 O(n) 500
FGPSF09-patrs-pasta_a.04.c A + B + 1 O(n) 92 a + -1 + -b O(n) 500
FGPSF09-patrs-pasta_a.05.c A + B + 1 O(n) 111 a + -1 + -b O(n) 500
FGPSF09-patrs-pasta_a.06.c A + B + C + 1 O(n) 153 a + -1 + -c + -b O(n) 500
FGPSF09-patrs-pasta_a.07.c A + C + 1 O(n) 153 a + -1 + -b O(n) 500
FGPSF09-patrs-pasta_a.08.c A + B + 1 O(n) 135 a + -1 + -b O(n) 500
FGPSF09-patrs-pasta_a.09.c A + B + 2 O(n) 128 a - b O(n) 500
FGPSF09-patrs-pasta_a.10.c 2*A + 2*B + A^2 + 2*A*B + B... O(n2) 264 FAILED 500
FGPSF09-patrs-pasta_a.11.c 18*A + 8*B + 10*C + 12 O(n) 564 a + -1 + -b O(n) 500
FGPSF09-patrs_div.c A + B + 3 O(n) 127 b + -1 + -a O(n) 500
FGPSF09-patrs_increase1.c A + B + 1 O(n) 92 a + -1 + -b O(n) 500
FGPSF09-patrs_increase2.c 2*A + 2*B + 2*C + 1 O(n) 177 a + -1 + -b + -c O(n) 500
FGPSF09-patrs_increase3.c 4*A + 2*B + 2*C + 3 O(n) 179 a + -1 + -b O(n) 500
FGPSF09-patrs_increase4.c A + B + 1 O(n) 133 a + -1 + -b O(n) 500
FGPSF09-patrs_random_full_no_wrap.c FAILED 824 not analyzed
FGPSF09-patrs_random_no_wrap.c 24*A + 7 O(n) 62 not analyzed
FGPSF09-patrs_sqrt.c D + 2 O(n) 326 d + -1 O(n) 500
FGPSF09-patrs_sumto_no_if.c A + B + 3 O(n) 101 b - a O(n) 500
KoAT-2013_sect1-lin.c 2*A + B + 4 O(n) 221 b + a + a + -3 O(n) 500
KoAT-2013_sect1-quad.c 3*A + B + A^2 + 3 O(n2) 264 a + b + -2 + a × (a + -1) O(n2) 500
KoAT-2013_sect2.c 8*B + 2*B^2 + 8 O(n2) 405 b + b + -3 + (b + -3) × (b... O(n2) 500
KoAT-2013_sect4-facSum.c 105*B + 11*B^2 + 56 O(n2) 401 not analyzed
KoAT-2013_sect5-len.c B + 2 O(n) 170 b + -1 O(n) 500
KoAT-2013_sect5-sumSum.c 4*B + 6*B^2 + 1 O(n2) 470 b + -1 + (b + -2) × (b + -1) O(n2) 500
Loop.t2.c TIMEOUT 1 (no loops) O(1) 500
Loopus_Example1.c 804*B + 220*B^2 + 736 O(n2) 2953 max((b + -1), min((b + -2),... O(n) 500
Loopus_Example2.c TIMEOUT FAILED 1000
Loopus_Example3.c FAILED 1349 507 + 254 × (254 - a) + -a O(n) 500
Rank_ex1.c FAILED 7136 b + b × b O(n2) 500
Rank_ex2.c 41*B + 5*B^2 + 38 O(n2) 645 b + b + -2 + (b + -2) × (b... O(n3) 500
Rank_ex3.c 61*B + 9*B^2 + 84 O(n2) 965 b + b + -3 + (b + -2) × (b... O(n2) 500
SAS10_aaron2.c 4*C + 4*E + 7 O(n) 990 x - y O(n) 500
SAS10_ackermann.c 16*A + 4 O(n) 244 a + -1 O(n) 500
SAS10_ax.c TIMEOUT n + n + -3 + (n + -2) × (n... O(n2) 500
SAS10_complex.c 193*A + 32*C + 6550 O(n) 1436 30 + (30 - a) × ((29 - b) ... O(n2) 500
SAS10_counterex1.c TIMEOUT FAILED 500
SAS10_cousot9.c TIMEOUT j + N + N × N O(n2) 500
SAS10_determinant.c TIMEOUT -1 + (-2 + min(a, (a + 1))... O(n3) 1000
SAS10_easy1.c 126 O(1) 901 40 O(1) 500
SAS10_easy2.c A + 4 O(n) 480 z O(n) 500
SAS10_exmini.c 2*A + 2*E + G + 106 O(n) 426 100 - i O(n) 500
SAS10_gcd.c 4*A + 4*C + 14 O(n) 778 y + x + -2 O(n) 500
SAS10_insertsort.c TIMEOUT length + -1 + (length + -2... O(n2) 500
SAS10_loops.c TIMEOUT n + n × (n + -1) O(n2) 500
SAS10_maccarthy91.c 8*A + 1563 O(n) 1172 310 + 9 × (100 - x) + -x +... O(n) 500
SAS10_nd_loop.c 43 O(1) 274 FAILED 500
SAS10_ndecr.c A + 4 O(n) 185 n + -2 O(n) 500
SAS10_nestedLoop.c TIMEOUT m × min(n, N) + min(n, N) ... O(n2) 500
SAS10_perfect.c TIMEOUT FAILED 500
SAS10_random1d.c 2*A + 7 O(n) 568 max + -1 O(n) 500
SAS10_random2d.c 22*A + 8 O(n) 1608 N O(n) 500
SAS10_realbubble.c TIMEOUT length + length + -2 + (le... O(n2) 500
SAS10_realheapsort.c TIMEOUT FAILED 500
SAS10_realselect.c 12*A + 19 O(n) 1212 array_size + -1 + (array_s... O(n2) 500
SAS10_realshellsort.c TIMEOUT FAILED 500
SAS10_relation1.c 3 O(1) 26 1 O(1) 500
SAS10_rsd.c TIMEOUT -1 + r × 2 + r × 2 + (-1... O(n2) 500
SAS10_sipmabubble.c TIMEOUT n + n × (n + -1) O(n2) 500
SAS10_speedFails4.c 2*B + 2*C + 7 O(n) 975 FAILED 500
SAS10_speedpldi2.c 6*G + 9 O(n) 584 FAILED 500
SAS10_speedpldi3.c TIMEOUT m + n + m × n O(n2) 500
SAS10_speedpldi4.c 2*A + 2*C + 17 O(n) 552 FAILED 500
SAS10_terminate.c A + E + 207 O(n) 401 100 - i O(n) 500
SAS10_wcet1.c 3*A + 13 O(n) 932 n + -1 O(n) 500
SAS10_wcet2.c 44*A + 221 O(n) 1012 2 + 9 × (2 - i) + -i O(n) 500
SAS10_while2.c TIMEOUT N + N × N O(n2) 500
SAS10_wise.c 2*A + 2*C + 14 O(n) 430 FAILED 500
SPEED-CAV09_ex1.c 10*C + 898 O(n) 931 c + 98 O(n) 500
SPEED-CAV09_ex2.c 15*C + 3*D + 9*C*D + 9 O(n2) 1080 d + c + -2 + (d + -1) × (c... O(n2) 500
SPEED-CAV09_ex3.c 90*B + 5 O(n) 402 b + b + -2 O(n) 500
SPEED-PLDI09_Example2.c TIMEOUT FAILED 500
SPEED-PLDI09_Example3.c 136*B + 20*A + 30*A*B + 105... O(n2) 1235 b + a + -2 + (b + -1) × (a... O(n2) 500
SPEED-PLDI09_Example4.c TIMEOUT FAILED 1000
SPEED-PLDI09_Example5.c 9*B + 15*A + 27*C + 24*A*C ... O(n2) 792 b + -2 + (b + -1) × (a + -1) O(n2) 500
SPEED-PLDI09_Example6.c 28*D + 7*G + 27 O(n) 779 d + g + g + -3 O(n) 500
SPEED-PLDI09_NestedLoop.c TIMEOUT (b + -1) × max((c + -1), (... O(n2) 500
SPEED-PLDI09_cyclic.c TIMEOUT FAILED 500
SPEED-PLDI10_Ex1.c FAILED 7292 a + -1 + (a + -2) × (a + -1) O(n2) 500
SPEED-PLDI10_Ex2.c FAILED 1441 FAILED 500
SPEED-PLDI10_Ex3.c FAILED 1274 FAILED 500
SPEED-PLDI10_Ex4.c 110*A + 33 O(n) 519 FAILED 500
SPEED-PLDI10_Ex5.c FAILED 2371 FAILED 500
SPEED-PLDI10_Ex6.c 6*A + 9*C + 3*B + 5 O(n) 1042 c + -1 + max(c, b) + -a + -b O(n) 500
SPEED-PLDI10_Ex7.c TIMEOUT FAILED 500
SPEED-POPL09_Dis1.c 9*A + 9*B + 10*C + 10*D + 7 O(n) 805 c + a + -2 + -d + -b O(n) 500
SPEED-POPL09_Dis2.c 6*A + 9*B + 3*C + 5 O(n) 1015 a + -1 + max(c, a) + -b + -c O(n) 500
SPEED-POPL09_NestedMultiple.c TIMEOUT FAILED 500
SPEED-POPL09_NestedMultipleDep.c 15*B + 12*B*E + 4*E + 9 O(n2) 404 b + -1 + (b + -1) × (e + -1) O(n2) 500
SPEED-POPL09_NestedSingle.c 48*B + 16 O(n) 335 b + b + -2 O(n) 500
SPEED-POPL09_SequentialSingle.c 21*B + 6 O(n) 324 b + b + b + -3 O(n) 500
SPEED-POPL09_SimpleMultiple.c 9*C + 10*D + 7 O(n) 984 c + d + -2 O(n) 500
SPEED-POPL09_SimpleMultipleDep.c 15*C + 3*D + 9*C*D + 9 O(n2) 1082 d + c + -2 + (d + -1) × (c... O(n2) 500
SPEED-POPL09_SimpleSingle.c 4*B + 6 O(n) 160 b + -1 O(n) 500
SPEED-POPL09_SimpleSingle2.c 20*D + 12*C + 17 O(n) 513 d + c + -2 O(n) 500
WTC_aaron2.c 35*A + 28*B + 28*C + 13 O(n) 344 b - c O(n) 500
WTC_ax.c 23*C + 12*C^2 + 14 O(n2) 369 c + c + -5 + (c + -3) × (c... O(n2) 500
WTC_complex.c TIMEOUT FAILED 500
WTC_counterex1b.c TIMEOUT FAILED 500
WTC_cousot9.c TIMEOUT c + d + -2 + (c + -1) × (c... O(n2) 500
WTC_easy1.c 830 O(1) 298 39 O(1) 500
WTC_easy2.c 4*A + 6 O(n) 116 a + -1 O(n) 500
WTC_exmini.c 2*A + 2*B + 2*C + 207 O(n) 200 b - c O(n) 500
WTC_gcd.c TIMEOUT FAILED 500
WTC_insertsort.c 716*B + 384*B^2 + 325 O(n2) 469 b + -2 + (b + -2) × (b + -2) O(n2) 500
WTC_loops.c TIMEOUT a + -2 + (a + -3) × (a + -2) O(n2) 500
WTC_nd_loop.c 15 O(1) 120 FAILED 500
WTC_ndecr.c 4*A + 6 O(n) 158 a + -3 O(n) 500
WTC_nestedLoop.c TIMEOUT (b + -1) × max((c + -1), (... O(n2) 500
WTC_perfect.c TIMEOUT a + -2 + a × (a + -2) O(n2) 500
WTC_random1d.c 12*A + 13 O(n) 299 a + -1 O(n) 500
WTC_random2d.c 189*B + 139 O(n) 1023 b + -1 O(n) 500
WTC_realbubble.c 2548*A + 1248*A^2 + 1305 O(n2) 608 a + a + -4 + (a + -3) × (a... O(n2) 500
WTC_realheapsort.c TIMEOUT FAILED 1000
WTC_realheapsort_step1.c 795*A + 216*A^2 + 730 O(n2) 31460 N + -2 + (N + -2) × (N + -1) O(n2) 500
WTC_realheapsort_step2.c TIMEOUT FAILED 500
WTC_realselect.c 150*B + 216*B^2 + 28 O(n2) 458 b + -2 + (b + -3) × (b + -2) O(n2) 500
WTC_realshellsort.c TIMEOUT FAILED 500
WTC_rsd.c 18*A^2 + 21*A + 7 O(n2) 1424 -1 + a × 2 + a × 2 + (-1... O(n2) 500
WTC_sipma91.c 3218*A + 15*A^2 + 172966 O(n2) 2962 309 + 9 × (99 - a) + -a + ... O(n) 500
WTC_sipmabubble.c 428*A + 864*A^2 + 57 O(n2) 345 a + a × (a + -1) O(n2) 500
WTC_speedFails4.c TIMEOUT FAILED 500
WTC_speedpldi2.c TIMEOUT FAILED 500
WTC_speedpldi3.c 15*B + 3*A + 9*A*B + 17 O(n2) 1657 a + b + -2 + (a + -1) × (b... O(n2) 500
WTC_speedpldi4.c TIMEOUT FAILED 500
WTC_terminate.c 2*A + 2*B + 2*C + 207 O(n) 205 100 - a O(n) 500
WTC_wcet1.c 44*A + 26 O(n) 594 a + -2 O(n) 500
WTC_wcet2.c 2814*A + 360*A^2 + 5423 O(n2) 334 4 + 8 × (4 - a) + -a O(n) 500
WTC_while2.c 25*B + 12*B^2 + 11 O(n2) 275 b + -1 + (b + -1) × (b + -1) O(n2) 500
WTC_wise.c 78*A + 78*B + 66*A^2 + 132*... O(n2) 575 FAILED 500
a.10.c.t2.c TIMEOUT 1 (no loops) O(1) 500
acqrel-fail.t2.c TIMEOUT FAILED 500
afagp-fail.t2.c TIMEOUT FAILED 1000
afagx1.t2.c FAILED 238 FAILED 500
agafp.t2.c TIMEOUT FAILED 500
apchild-accepted-fail.t2.c TIMEOUT FAILED 500
apchild-accepted.t2.c TIMEOUT FAILED 500
apchild-live.t2.c TIMEOUT FAILED 500
apchildlive-succeed.t2.c TIMEOUT FAILED 1000
array.t2.c 1 O(1) 21 1 (no loops) O(1) 500
array1.t2.c 1 O(1) 17 1 (no loops) O(1) 500
array2.t2.c 52 O(1) 141 49 O(1) 500
array3.t2.c 103 O(1) 287 98 O(1) 500
array_free.t2.c 86 O(1) 198 41 O(1) 500
array_init.t2.c 13 O(1) 129 9 O(1) 500
array_init_assign.t2.c 8 O(1) 262 2 O(1) 500
ase_example.t2.c 85 O(1) 579 27 O(1) 500
bf10.t2.c 756 O(1) 1255 22 O(1) 500
bf11.t2.c 807 O(1) 1255 24 O(1) 500
bf12.t2.c 858 O(1) 1250 26 O(1) 500
bf13.t2.c 909 O(1) 1294 28 O(1) 1000
bf14.t2.c 960 O(1) 1253 30 O(1) 500
bf15.t2.c 1011 O(1) 1252 32 O(1) 500
bf16.t2.c 1062 O(1) 1271 34 O(1) 500
bf17.t2.c 1113 O(1) 1248 36 O(1) 500
bf18.t2.c 1164 O(1) 1235 38 O(1) 500
bf19.t2.c 1215 O(1) 1246 40 O(1) 500
bf20.t2.c 1266 O(1) 1249 42 O(1) 1000
bf5.t2.c 501 O(1) 1245 12 O(1) 500
bf6.t2.c 552 O(1) 1252 14 O(1) 500
bf7.t2.c 603 O(1) 1238 16 O(1) 500
bf8.t2.c 654 O(1) 1244 18 O(1) 500
bf9.t2.c 705 O(1) 1241 20 O(1) 500
bio.t2.c TIMEOUT FAILED 1000
bitcount16.t2.c 34 O(1) 412 15 O(1) 500
bitcount32.t2.c 66 O(1) 532 31 O(1) 500
broydn.c.i.broydn.pl.t2.fixed.t2.c TIMEOUT TIMEOUT
broydn.c.i.broydn.pl.t2.nor.t2.rlgfixed.t2.c TIMEOUT TIMEOUT
broydn.t2.c TIMEOUT TIMEOUT
brp.t2.c TIMEOUT 1 (no loops) O(1) 500
brp_withassume.t2.c TIMEOUT FAILED 1000
bs.t2.c TIMEOUT FAILED 500
bsort100.t2.c 4959205 O(1) 927 198 O(1) 500
bubbleSort.t2.c 127*C + 40*C^2 + 105 O(n2) 876 -4 + max(call_to_nondet_lin... O(n) 1000
bubblesort_inner_loop.t2.c 11 O(1) 269 3 O(1) 500
buggyNonTermLoop.t2.c TIMEOUT 1 (no loops) O(1) 500
byron-1.t2.c TIMEOUT FAILED 500
byron-2.t2.c FAILED 377 -4 + (-3 + max(call_to_non... O(n2) 500
byron-3.t2.c TIMEOUT FAILED 500
byron-4.t2.c 2*A + 3 O(n) 401 FAILED 500
cfg.t2.c TIMEOUT 1 (no loops) O(1) 500
cnt.t2.c 41596 O(1) 1564 20 O(1) 500
collatz.t2.c TIMEOUT FAILED 500
complex_guard.t2.c 25 O(1) 171 2 O(1) 500
constants.t2.c 404 O(1) 292 399 O(1) 1000
consts1.t2.c 301 O(1) 136 FAILED 500
consts1nt.t2.c TIMEOUT FAILED 500
consts2.t2.c A + 1000 O(n) 78 -1001 + max(call_to_nondet_... O(n) 500
consts2nt.t2.c TIMEOUT FAILED 500
consts3.t2.c A + 1 O(n) 90 -202 + max(call_to_nondet_l... O(n) 500
consts3nt.t2.c TIMEOUT FAILED 500
consts4.t2.c A + 1200 O(n) 84 -1201 + max(call_to_nondet_... O(n) 500
consts4nt.t2.c TIMEOUT FAILED 500
consts5.t2.c 1 O(1) 28 1 (no loops) O(1) 500
consts5nt.t2.c TIMEOUT FAILED 500
costa-jvm-cost_ArrayReverse.c TIMEOUT length O(n) 500
costa-jvm-cost_BST.c FAILED 10670 not analyzed
costa-jvm-cost_Concat.c 9*B + 9*A + 16 O(n) 139 lengthB + lengthA O(n) 500
costa-jvm-cost_Cons.c 368*A + 70 O(n) 200 Depth(Set(Select(1, _), c)) O(n) 500
costa-jvm-cost_Delete.c TIMEOUT la × Depth(Set(Select(1, _... O(n2) 500
costa-jvm-cost_DetEval.c 9*A + 7 O(n) 5186 la + la + la + la + la + -1... O(n3) 500
costa-jvm-cost_DivByTwo.c 18*A + 6 O(n) 63 n O(n) 500
costa-jvm-cost_EvenDigits.c 241*A + 27 O(n) 1572 n + n × (n + -1) O(n2) 500
costa-jvm-cost_EvenDigitsNew.c 28 O(1) 1166 not analyzed
costa-jvm-cost_FactSum.c FAILED 1664 n + n × (n + -2) O(n2) 500
costa-jvm-cost_FactSumNew.c 10*B + 35 O(n) 2622 not analyzed
costa-jvm-cost_Factorial.c 25*A + 9 O(n) 71 n + -2 O(n) 500
costa-jvm-cost_Fibonacci.c FAILED 1581 not analyzed
costa-jvm-cost_FibonacciNew.c FAILED 1508 not analyzed
costa-jvm-cost_Hanoi.c FAILED 1740 not analyzed
costa-jvm-cost_Incr.c 275*A + 831 O(n) 281 n O(n) 500
costa-jvm-cost_LinEqSolve.c 9*B + 9 O(n) 5218 la + la + la + la + la + la... O(n3) 1000
costa-jvm-cost_ListInter.c 600*A*B + 575*A + 1056*B + ... O(n2) 2370 Depth(Set(Select(1, _), l1)... O(n2) 500
costa-jvm-cost_ListReverse.c 9*B + 6 O(n) 227 Depth(Set(Select(1, _), x)) O(n) 500
costa-jvm-cost_MatMult.c TIMEOUT la + la × lb + la × lb × lb O(n3) 500
costa-jvm-cost_MatrixInverse.c 9*A + 6 O(n) 5857 la + la + la + la + la + la... O(n3) 500
costa-jvm-cost_MergeList.c 481*A + 555*B + 47 O(n) 300 Depth(Set(Select(1, _), oth... O(n2) 500
costa-jvm-cost_Polynomial.c 1066 O(1) 173 min(Select(0, this), 10) O(n) 500
costa-jvm-cost_Power.c 25*A + 9 O(n) 83 n + -1 O(n) 500
costa-jvm-cost_SelectOrd.c 113*A + 80*A^2 + 80*A*D + 6 O(n2) 2507 lv + -2 + (lv + -2) × (lv ... O(n2) 500
costa-jvm-cost_ms.c 10*C + 10*E + 15 O(n) 2882 not analyzed
costa-misc_ack.c TIMEOUT a + -1 O(n) 500
costa-misc_direct_n_log_n.c 4*A + 9 O(n) 86 a + -2 O(n) 500
costa-misc_divide_and_conquer.c 12*A + 4 O(n) 153 not analyzed
costa-misc_exponential.c FAILED 263 not analyzed
costa-misc_linear.c A + 2 O(n) 119 FAILED 500
costa-misc_logarithmic.c 3 O(1) 35 1 O(1) 500
costa-misc_merge.c 2*A + 2*B + 3 O(n) 148 a + -1 O(n) 500
costa-misc_ms.c 12*A + 3*B + 10 O(n) 44 not analyzed
costa-misc_mspe.c 4*B + 4*F + 5 O(n) 229 FAILED 1000
costa-misc_n_log_n.c 3 O(1) 51 not analyzed
costa-misc_no_cover_point.c FAILED 381 not analyzed
costa-misc_quadratic.c 16*A + 12*A^2 + 5 O(n2) 181 n + -1 + (n + -1) × (n + -1) O(n2) 500
cover.t2.c TIMEOUT 177 O(1) 500
crc.t2.c 17*M + 17*N + 17*O + 17*P +... O(n) 18168 96 O(1) 500
create.t2.c TIMEOUT call_to_nondet_line_66 + -3 O(n) 1000
create_seg.t2.c TIMEOUT call_to_nondet_line_69 + -3 O(n) 500
create_via_tmps.t2.c A + 4*U + 13 O(n) 3502 -3 + max(call_to_nondet_lin... O(n) 500
ctl.t2.c FAILED 494 FAILED 500
curious.t2.c FAILED 235 FAILED 500
curious2.t2.c not analyzed 1 (no loops) O(1) 500
curious4.t2.c TIMEOUT FAILED 500
d.t2.c TIMEOUT FAILED 500
db.t2.c not analyzed 1 (no loops) O(1) 500
db2.t2.c TIMEOUT FAILED 1000
db3.t2.c TIMEOUT FAILED 1000
dead.neg-st88b-succeed.t2.c FAILED 1473 FAILED 500
destroy.t2.c TIMEOUT call_to_nondet_line_150 + -... O(n) 500
destroy_seg.t2.c TIMEOUT call_to_nondet_line_234 + -... O(n) 500
destroy_seg_leak.t2.c TIMEOUT FAILED 500
disj_nightmare.t2.c not analyzed FAILED 500
disj_nightmare_abi.t2.c 3 O(1) 49 1 O(1) 500
dropbuf-live.t2.c 1 O(1) 23 1 (no loops) O(1) 500
dropbuf.t2.c TIMEOUT FAILED 1000
dsa_test.t2.c 1 O(1) 6 1 (no loops) O(1) 500
dsa_test1.t2.c 1 O(1) 22 1 (no loops) O(1) 500
dsa_test10.t2.c 31 O(1) 285 18 O(1) 500
dsa_test11.t2.c 1 O(1) 36 1 (no loops) O(1) 500
dsa_test12.t2.c 1 O(1) 18 1 (no loops) O(1) 500
dsa_test13.t2.c 1 O(1) 10 1 (no loops) O(1) 500
dsa_test14.t2.c not analyzed 1 (no loops) O(1) 500
dsa_test15.t2.c 23 O(1) 261 18 O(1) 500
dsa_test2.t2.c not analyzed 1 (no loops) O(1) 500
dsa_test4.t2.c 1 O(1) 13 1 (no loops) O(1) 500
dsa_test5.t2.c 1 O(1) 39 1 (no loops) O(1) 500
dsa_test6.t2.c 12 O(1) 142 9 O(1) 500
dsa_test7.t2.c not analyzed 1 (no loops) O(1) 500
dsa_test8.t2.c 1 O(1) 10 1 (no loops) O(1) 500
dsa_test9.t2.c 1 O(1) 18 1 (no loops) O(1) 500
dummy.t2.c TIMEOUT FAILED 500
e-1394complete-succeed.t2.c TIMEOUT FAILED 1000
e-acqrel-fail.t2.c FAILED 263 FAILED 500
e-acqrel-succeed.t2.c FAILED 624 FAILED 500
e-pgarch-fail.t2.c FAILED 1838 FAILED 500
e-pgarch-succeed.t2.c FAILED 2984 FAILED 500
e-popl07-fail.t2.c TIMEOUT FAILED 1000
edn.t2.c TIMEOUT 398 O(1) 500
efegp.t2.c TIMEOUT FAILED 1000
elmhes.c.i.elmhes.pl.t2.fixed.t2.c TIMEOUT -1 + (max(call_to_nondet_l... O(n2) 1000
elmhes.c.i.elmhes.pl.t2.nor.t2.rlgfixed.t2.c TIMEOUT -1 + (max(call_to_nondet_l... O(n2) 500
elmhes.t2.c TIMEOUT -1 + (max(call_to_nondet_l... O(n2) 1000
eric.t2.c TIMEOUT -4 + max(call_to_nondet_lin... O(n) 1000
eric1.t2.c TIMEOUT FAILED 500
eric2.t2.c TIMEOUT FAILED 1000
eric3.t2.c TIMEOUT FAILED 500
ex1.t2.c TIMEOUT FAILED 500
ex10.t2.c TIMEOUT FAILED 500
ex11.t2.c TIMEOUT FAILED 500
ex12.t2.c 20 O(1) 191 17 O(1) 500
ex13.t2.c 1 O(1) 20 1 (no loops) O(1) 500
ex14.t2.c 12 O(1) 169 9 O(1) 500
ex15.t2.c 1 O(1) 28 1 (no loops) O(1) 500
ex16.t2.c TIMEOUT FAILED 500
ex17.t2.c 104 O(1) 358 FAILED 1000
ex18.t2.c TIMEOUT FAILED 500
ex19.t2.c TIMEOUT FAILED 1000
ex2.t2.c TIMEOUT FAILED 500
ex20.t2.c 1030 O(1) 509 1023 O(1) 500
ex21.t2.c 203 O(1) 278 198 O(1) 500
ex22.t2.c 11928 O(1) 9037 366 O(1) 500
ex23.t2.c 39 O(1) 176 35 O(1) 500
ex26.t2.c 203 O(1) 283 198 O(1) 500
ex27.t2.c 22853 O(1) 19474 565 O(1) 500
ex29.t2.c 15 O(1) 183 1 (no loops) O(1) 500
ex3.t2.c 13 O(1) 251 9 O(1) 500
ex30.t2.c TIMEOUT call_to_nondet_line_56 + ca... O(n) 500
ex31.t2.c TIMEOUT FAILED 1000
ex32.t2.c 2003 O(1) 325 1998 O(1) 500
ex33.t2.c 3 O(1) 10 1 (no loops) O(1) 500
ex34.t2.c 1 O(1) 15 1 (no loops) O(1) 500
ex36.t2.c TIMEOUT FAILED 11000
ex37.t2.c 1 O(1) 19 1 (no loops) O(1) 500
ex4.t2.c 87 O(1) 729 18 O(1) 500
ex40.t2.c TIMEOUT FAILED 500
ex6.t2.c 3 O(1) 18 1 (no loops) O(1) 500
ex7.t2.c 12 O(1) 193 9 O(1) 500
ex8.t2.c TIMEOUT FAILED 500
ex9.t2.c TIMEOUT FAILED 500
example.t2.c 2*A + 2*B + 5 O(n) 165 -4 + max(call_to_nondet_lin... O(n) 500
fake-succeed.t2.c TIMEOUT FAILED 500
fast_poll.t2.c TIMEOUT FAILED 500
fdct.t2.c 19 O(1) 586 14 O(1) 500
fermat.t2.c 15 O(1) 984 6 O(1) 500
fibcall.t2.c 31 O(1) 395 28 O(1) 500
fir.t2.c TIMEOUT 7 + 9 × (-2 + max(call_to_... O(n) 1000
firewire.t2.c TIMEOUT FAILED 3000
flipflop.t2.c TIMEOUT FAILED 500
fourn.c.i.fourn.pl.t2.fixed.t2.c A + B + 4 O(n) 812 FAILED 1000
fourn.c.i.fourn.pl.t2.nor.t2.rlgfixed.t2.c TIMEOUT FAILED 2000
fourn.t2.c TIMEOUT FAILED 1000
fuhs-inflasso.t2.c C^2 + 5*C + 7 O(n2) 297 -2 + (-1 + max(call_to_non... O(n2) 500
fun1.t2.c TIMEOUT FAILED 1000
fun10.t2.c TIMEOUT FAILED (Irreducible Control Flow) 500
fun10b.t2.c TIMEOUT FAILED (Irreducible Control Flow) 500
fun11.t2.c TIMEOUT FAILED 500
fun1b.t2.c TIMEOUT FAILED 1000
fun2.t2.c TIMEOUT FAILED 500
fun2b.t2.c TIMEOUT FAILED 500
fun3.t2.c TIMEOUT FAILED 1000
fun4-alt.t2.c 5*A + 21*B + 3*A^2 + 8*A*B ... O(n2) 366 FAILED 500
fun4.t2.c 9*A + 18*B + 2*A^2 + 8*A*B ... O(n2) 620 FAILED 500
fun5.t2.c TIMEOUT FAILED 2000
fun6.t2.c TIMEOUT FAILED (Irreducible Control Flow) 500
fun7.t2.c TIMEOUT FAILED (Irreducible Control Flow) 500
fun8.t2.c 573 O(1) 6188 27 O(1) 500
fun9.t2.c TIMEOUT FAILED 500
graycode.t2.c 245854 O(1) 5954 43 O(1) 500
heidy1.t2.c TIMEOUT FAILED 500
heidy10.t2.c TIMEOUT call_to_nondet_line_27 + -2... O(n2) 500
heidy2.t2.c TIMEOUT FAILED 500
heidy3.t2.c FAILED 376 FAILED 1000
heidy5.t2.c B + 3 O(n) 147 -1 + max(call_to_nondet_lin... O(n) 500
heidy6.t2.c TIMEOUT FAILED 500
heidy7-simple.t2.c TIMEOUT FAILED 500
heidy7.t2.c TIMEOUT FAILED 500
heidy8.t2.c TIMEOUT FAILED 500
heidy9.t2.c A + 2 O(n) 139 -1 + max(call_to_nondet_lin... O(n) 500
hongyi1.t2.c TIMEOUT FAILED 1000
hqr.c.i.hqr.pl.t2.fixed.t2.c TIMEOUT FAILED 4000
hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2.c TIMEOUT FAILED 4000
hqr.t2.c TIMEOUT FAILED 4000
huh.t2.c TIMEOUT 27 + max(call_to_nondet_lin... O(n) 500
iecs.t2.c TIMEOUT FAILED 500
insertsort.t2.c TIMEOUT FAILED 500
intSqRoot.t2.c TIMEOUT FAILED 500
invgen.t2.c B + 2 O(n) 105 max(call_to_nondet_line_5, ... O(n) 500
jacobi.c.i.jacobi.pl.t2.fixed.t2.c TIMEOUT -12 + (-1 + max((call_to_n... O(n3) 10000
jacobi.c.i.jacobi.pl.t2.nor.t2.rlgfixed.t2.c TIMEOUT