Benchmark Result Comparison

PUBS Loopus
All 669 658
Bounded 279 386
Timeouts 58 6
Failed 332 266
Runtime without Timeouts 998 sec 226 sec
O(1) O(log n) O(n) O(n log n) O(n2) O(n3) O(n>=4) EXP
PUBS 116 5 129 5 15 4 0 5
Loopus 134 0 152 0 81 15 4 0
Show examples where
Source File PUBS Loopus
Bound Degree Time ms Bound Degree Time ms
1.t2.c FAILED 403 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 FAILED 394 FAILED 500
232.t2.c FAILED 70 -2 + (-2 + max(call_to_non... O(n2) 500
241.t2.c FAILED 71 -2 + (-2 + max(call_to_non... O(n2) 500
3.t2.c FAILED 61 FAILED 500
5.t2.c FAILED 275 1 (no loops) O(1) 500
6.t2.c FAILED 62 FAILED 500
7.t2.c FAILED 70 FAILED 500
ABC_ex01.c (4 + (2 * max(0, ((A + B) +... O(n) 78 a - b O(n) 500
ABC_ex02.c (5 + (3 * max(0, B))) O(n) 89 b + -1 + b × (b + -1) O(n2) 500
ABC_ex03.c (4 + (max(0, B) * ((5 + (ma... O(n3) 174 b + -1 + (b + -1) × (-1 + ... O(n4) 500
ABC_ex04.c FAILED 78 -1 + (n + -1) × (-1 + (( n... O(n5) 500
ABC_ex05.c (5 + (3 * max(0, B))) O(n) 109 b + -1 + (b + -1) × (-1 + ... O(n2) 500
ABC_ex06.c (5 + (3 * max(0, B))) O(n) 90 b + -1 + (b + -2) × (b + -1) O(n2) 500
ABC_ex07.c (5 + (3 * max(0, B))) O(n) 99 b + -1 + (b + -1) × (d + -1) O(n2) 500
ABC_ex08.c (5 + (3 * max(0, A))) O(n) 89 a + -1 + (a + -1) × (b + -1) O(n2) 500
ABC_ex09.c (5 + (3 * max(0, B))) O(n) 99 b + -1 + (d + -1) × (b + -1) O(n2) 500
ABC_ex10.c (5 + (3 * max(0, A))) O(n) 91 b + -1 + (a + -1) × (b + -1) O(n2) 500
ABC_ex11.c (5 + (3 * max(0, A))) O(n) 85 a + -1 + (a + -1) × (b + -1) O(n2) 500
ABC_ex12.c (5 + (3 * max(0, A))) O(n) 90 0 O(1) 500
ABC_ex13.c (10 + (3 * max(0, ((A + B) ... O(n) 145 b + (b - a) × (d - c) + (... O(n3) 500
ABC_ex14.c (4 + (max(0, A) * ((6 + (ma... O(n3) 175 b + -1 + (a + -1) × (b + -... O(n4) 500
ABC_ex15.c (4 + (max(0, A) * ((6 + (ma... O(n3) 254 n + -1 + (n + -1) × (m + -... O(n4) 500
FGPSF09-Beerendonk_01.c (1 + max(0, (A - B))) O(n) 73 a + -1 + -b O(n) 500
FGPSF09-Beerendonk_02.c (1 + max(0, (((A / 2) - (B ... O(n) 75 a + -1 + -b O(n) 500
FGPSF09-Beerendonk_03.c (1 + max(0, (A - B))) O(n) 76 a + -1 + -b O(n) 500
FGPSF09-Beerendonk_04.c 1+log(4,3+nat(A/2-B/2+1/2)) O(log n) 69 a + -1 + -b O(n) 500
FGPSF09-Beerendonk_05.c (1 + max(0, A)) O(n) 66 1 O(1) 500
FGPSF09-Beerendonk_06.c (1 + max(0, A)) O(n) 66 1 O(1) 500
FGPSF09-Beerendonk_07.c (1 + max(0, ((A / 3) + (2 /... O(n) 71 1 O(1) 1000
FGPSF09-Beerendonk_08.c (1 + max(0, B)) O(n) 73 b + -1 O(n) 500
FGPSF09-Beerendonk_09.c (1 + max(0, (B + C))) O(n) 81 a + -1 + -b O(n) 500
FGPSF09-Beerendonk_10.c (1 + max(0, A)) O(n) 79 FAILED 500
FGPSF09-Beerendonk_11.c (1 + max(0, B)) O(n) 113 b + b + 1 + max(-1, min(-1,... O(n) 500
FGPSF09-Beerendonk_13.c (1 + max(0, A)) O(n) 78 a + max(-1, min(-1, (-1 - b))) O(n) 500
FGPSF09-Beerendonk_15.c (1 + max(0, (A + B))) O(n) 86 b + a + -1 O(n) 500
FGPSF09-Beerendonk_16.c (1 + max(0, (A + B))) O(n) 108 a + b + -1 + -c O(n) 500
FGPSF09-Beerendonk_17.c (1 + max(0, (A + B))) O(n) 101 b + a + -2 + a × 2 O(n) 500
FGPSF09-Beerendonk_18.c FAILED 77 a + b + -2 O(n) 500
FGPSF09-Beerendonk_19.c FAILED 87 c + a + -2 + -b + -b O(n) 500
FGPSF09-Beerendonk_20.c 1+log(4,3+nat(A))* (2+nat(A)) O(n log n) 78 a + a + -2 O(n) 500
FGPSF09-Beerendonk_21.c 1+log(4,3+nat(A-B))* (2+nat... O(n log n) 87 a + a + -2 + -b + -b O(n) 500
FGPSF09-Beerendonk_22.c FAILED 85 FAILED 500
FGPSF09-Beerendonk_23.c FAILED 94 FAILED 500
FGPSF09-Beerendonk_24.c 1+log(4,3+nat(A/2+B-1/2))*m... O(n log n) 103 a + a + b + b + -4 O(n) 500
FGPSF09-CAV02_practical1.c (1 + (max(0, (A + 1)) * (2 ... O(n2) 83 a + a × (a + -1) O(n2) 500
FGPSF09-CAV02_practical2.c FAILED 531 309 + 9 × (99 - b) + -b + ... O(n) 500
FGPSF09-CAV05_c.05.c (1 + max(0, ((A + B) - 1))) O(n) 98 a + -2 O(n) 1000
FGPSF09-ESOP08_abstractions.c FAILED 82 a + -1 O(n) 500
FGPSF09-LICS04_c.01.c 1+nat(A+1)* (2+log(2,1+nat(... O(n log n) 84 a + a × (a + -2) O(n2) 500
FGPSF09-LICS04_choice.c FAILED 73 a + -1 O(n) 500
FGPSF09-PLDI06_c.03.c FAILED 81 a + -1 + max(b, a) + -b + -c O(n) 500
FGPSF09-PLDI06_c.04.c (1 + max(0, ((B + C) - 1))) O(n) 111 a + -1 + -b O(n) 500
FGPSF09-RTA08_round.c FAILED 48 not analyzed
FGPSF09-SAS05_c.02.c (1 + (max(0, (A + 1)) * (2 ... O(n2) 97 a + a × (a + -1) O(n2) 500
FGPSF09-TACAS01_terminate.c (1 + max(0, ((((A / 2) + (B... O(n) 103 100 - a O(n) 500
FGPSF09-VMCAI04_complete1.c (1 + max(0, (A - B))) O(n) 78 a + -1 + -b O(n) 500
FGPSF09-VMCAI04_complete2.c FAILED 74 FAILED 500
FGPSF09-VMCAI04_complete3.c (1 + (max(0, (A + 1)) * (2 ... O(n2) 84 a + a × (a + -1) O(n2) 500
FGPSF09-VMCAI04_complete4.c FAILED 74 b + a + a × max(call_to_no... O(n2) 500
FGPSF09-VMCAI05_poly1.c FAILED 78 FAILED 500
FGPSF09-VMCAI05_poly2.c FAILED 78 FAILED 500
FGPSF09-VMCAI05_poly3.c FAILED 86 FAILED 1000
FGPSF09-VMCAI05_poly4.c FAILED 123 c + a + -2 + -b + -d O(n) 500
FGPSF09-new_randomFullUpDown.c FAILED 61 not analyzed
FGPSF09-new_unsatCond2.c FAILED 87 FAILED 500
FGPSF09-patrs-pasta_a.01.c (1 + (max(0, A) * (2 + max(... O(n2) 80 a + -1 + (a + -2) × (a + -1) O(n2) 500
FGPSF09-patrs-pasta_a.02.c FAILED 206 FAILED 500
FGPSF09-patrs-pasta_a.03.c max((1 + (max(0, ((A + B) -... O(n2) 429 b + b + a + a + -8 O(n) 500
FGPSF09-patrs-pasta_a.04.c (1 + max(0, (A - B))) O(n) 72 a + -1 + -b O(n) 500
FGPSF09-patrs-pasta_a.05.c (1 + max(0, (A - B))) O(n) 85 a + -1 + -b O(n) 500
FGPSF09-patrs-pasta_a.06.c (1 + max(0, ((((A / 2) - (B... O(n) 85 a + -1 + -c + -b O(n) 500
FGPSF09-patrs-pasta_a.07.c (1 + max(0, (A - C))) O(n) 85 a + -1 + -b O(n) 500
FGPSF09-patrs-pasta_a.08.c (1 + max(0, (A - B))) O(n) 77 a + -1 + -b O(n) 500
FGPSF09-patrs-pasta_a.09.c (1 + max(0, ((A - B) + 1))) O(n) 84 a - b O(n) 500
FGPSF09-patrs-pasta_a.10.c FAILED 74 FAILED 500
FGPSF09-patrs-pasta_a.11.c FAILED 92 a + -1 + -b O(n) 500
FGPSF09-patrs_div.c (2 + max(0, (B - 1))) O(n) 75 b + -1 + -a O(n) 500
FGPSF09-patrs_increase1.c (1 + max(0, (A - B))) O(n) 77 a + -1 + -b O(n) 500
FGPSF09-patrs_increase2.c (1 + max(0, ((A - B) - C))) O(n) 97 a + -1 + -b + -c O(n) 500
FGPSF09-patrs_increase3.c (1 + max(0, ((((2 * A) - B)... O(n) 93 a + -1 + -b O(n) 500
FGPSF09-patrs_increase4.c (1 + max(0, (A - B))) O(n) 89 a + -1 + -b O(n) 500
FGPSF09-patrs_random_full_no_wrap.c FAILED 63 not analyzed
FGPSF09-patrs_random_no_wrap.c (2 + (4 * max(0, A))) O(n) 62 not analyzed
FGPSF09-patrs_sqrt.c (2 + max(0, ((D / 2) + (1 /... O(n) 99 d + -1 O(n) 500
FGPSF09-patrs_sumto_no_if.c (2 + max(0, ((A + B) + 1))) O(n) 75 b - a O(n) 500
KoAT-2013_sect1-lin.c FAILED 80 b + a + a + -3 O(n) 500
KoAT-2013_sect1-quad.c FAILED 61 a + b + -2 + a × (a + -1) O(n2) 500
KoAT-2013_sect2.c FAILED 131 b + b + -3 + (b + -3) × (b... O(n2) 500
KoAT-2013_sect4-facSum.c (2 + (max(0, (B + 1)) * (6 ... O(n2) 69 not analyzed
KoAT-2013_sect5-len.c (2 + max(0, B)) O(n) 74 b + -1 O(n) 500
KoAT-2013_sect5-sumSum.c (1 + (max(0, B) * (2 + max(... O(n2) 103 b + -1 + (b + -2) × (b + -1) O(n2) 500
Loop.t2.c TIMEOUT 1 (no loops) O(1) 500
Loopus_Example1.c FAILED 108 max((b + -1), min((b + -2),... O(n) 500
Loopus_Example2.c TIMEOUT FAILED 1000
Loopus_Example3.c FAILED 83 507 + 254 × (254 - a) + -a O(n) 500
Rank_ex1.c FAILED 424 b + b × b O(n2) 500
Rank_ex2.c (6 + (4 * max(0, (B / 2)))) O(n) 123 b + b + -2 + (b + -2) × (b... O(n3) 500
Rank_ex3.c FAILED 129 b + b + -3 + (b + -2) × (b... O(n2) 500
SAS10_aaron2.c FAILED 92 x - y O(n) 500
SAS10_ackermann.c (5 + (4 * max(0, A))) O(n) 103 a + -1 O(n) 500
SAS10_ax.c FAILED 128 n + n + -3 + (n + -2) × (n... O(n2) 500
SAS10_complex.c FAILED 88 30 + (30 - a) × ((29 - b) ... O(n2) 500
SAS10_counterex1.c FAILED 100 FAILED 500
SAS10_cousot9.c FAILED 79 j + N + N × N O(n2) 500
SAS10_determinant.c ((5 + (2 * max(0, (A - 1)))... O(n) 281 -1 + (-2 + min(a, (a + 1))... O(n3) 1000
SAS10_easy1.c FAILED 88 40 O(1) 500
SAS10_easy2.c (3 + max(0, (A - 1))) O(n) 143 z O(n) 500
SAS10_exmini.c (3 + max(0, ((A - G) + 201))) O(n) 252 100 - i O(n) 500
SAS10_gcd.c FAILED 85 y + x + -2 O(n) 500
SAS10_insertsort.c ((5 + (max(0, (A - 2)) * (3... O(n2) 619 length + -1 + (length + -2... O(n2) 500
SAS10_loops.c FAILED 79 n + n × (n + -1) O(n2) 500
SAS10_maccarthy91.c FAILED 219 310 + 9 × (100 - x) + -x +... O(n) 500
SAS10_nd_loop.c 21 O(1) 98 FAILED 500
SAS10_ndecr.c (3 + max(0, (A - 2))) O(n) 101 n + -2 O(n) 500
SAS10_nestedLoop.c FAILED 153 m × min(n, N) + min(n, N) ... O(n2) 500
SAS10_perfect.c FAILED 215 FAILED 500
SAS10_random1d.c (3 + max(0, (A - 1))) O(n) 266 max + -1 O(n) 500
SAS10_random2d.c (4 + (2 * max(0, (A - 1)))) O(n) 5932 N O(n) 500
SAS10_realbubble.c FAILED 467 length + length + -2 + (le... O(n2) 500
SAS10_realheapsort.c FAILED 598 FAILED 500
SAS10_realselect.c (5 + max(0, (A - 2))) O(n) 6607 array_size + -1 + (array_s... O(n2) 500
SAS10_realshellsort.c FAILED 1369 FAILED 500
SAS10_relation1.c 3 O(1) 70 1 O(1) 500
SAS10_rsd.c FAILED 92 -1 + r × 2 + r × 2 + (-1... O(n2) 500
SAS10_sipmabubble.c FAILED 95 n + n × (n + -1) O(n2) 500
SAS10_speedFails4.c FAILED 111 FAILED 500
SAS10_speedpldi2.c (3 + (2 * max(0, (G - 1)))) O(n) 458 FAILED 500
SAS10_speedpldi3.c FAILED 185 m + n + m × n O(n2) 500
SAS10_speedpldi4.c ((6 + max(0, (A + C))) + ma... O(n) 238 FAILED 500
SAS10_terminate.c (3 + max(0, ((A - E) + 201))) O(n) 254 100 - i O(n) 500
SAS10_wcet1.c (3 + max(0, (A - 2))) O(n) 906 n + -1 O(n) 500
SAS10_wcet2.c FAILED 91 2 + 9 × (2 - i) + -i O(n) 500
SAS10_while2.c FAILED 129 N + N × N O(n2) 500
SAS10_wise.c FAILED 82 FAILED 500
SPEED-CAV09_ex1.c FAILED 81 c + 98 O(n) 500
SPEED-CAV09_ex2.c FAILED 93 d + c + -2 + (d + -1) × (c... O(n2) 500
SPEED-CAV09_ex3.c FAILED 97 b + b + -2 O(n) 500
SPEED-PLDI09_Example2.c FAILED 108 FAILED 500
SPEED-PLDI09_Example3.c FAILED 132 b + a + -2 + (b + -1) × (a... O(n2) 500
SPEED-PLDI09_Example4.c FAILED 94 FAILED 1000
SPEED-PLDI09_Example5.c FAILED 86 b + -2 + (b + -1) × (a + -1) O(n2) 500
SPEED-PLDI09_Example6.c FAILED 445 d + g + g + -3 O(n) 500
SPEED-PLDI09_NestedLoop.c FAILED 250 (b + -1) × max((c + -1), (... O(n2) 500
SPEED-PLDI09_cyclic.c FAILED 152 FAILED 500
SPEED-PLDI10_Ex1.c FAILED 89 a + -1 + (a + -2) × (a + -1) O(n2) 500
SPEED-PLDI10_Ex2.c FAILED 85 FAILED 500
SPEED-PLDI10_Ex3.c FAILED 84 FAILED 500
SPEED-PLDI10_Ex4.c FAILED 84 FAILED 500
SPEED-PLDI10_Ex5.c FAILED 118 FAILED 500
SPEED-PLDI10_Ex6.c FAILED 87 c + -1 + max(c, b) + -a + -b O(n) 500
SPEED-PLDI10_Ex7.c FAILED 97 FAILED 500
SPEED-POPL09_Dis1.c FAILED 92 c + a + -2 + -d + -b O(n) 500
SPEED-POPL09_Dis2.c FAILED 83 a + -1 + max(c, a) + -b + -c O(n) 500
SPEED-POPL09_NestedMultiple.c (6 + (3 * max(0, (A + B)))) O(n) 145 FAILED 500
SPEED-POPL09_NestedMultipleDep.c (5 + (3 * max(0, B))) O(n) 113 b + -1 + (b + -1) × (e + -1) O(n2) 500
SPEED-POPL09_NestedSingle.c FAILED 85 b + b + -2 O(n) 500
SPEED-POPL09_SequentialSingle.c ((6 + (3 * max(0, B))) + (2... O(n) 110 b + b + b + -3 O(n) 500
SPEED-POPL09_SimpleMultiple.c FAILED 90 c + d + -2 O(n) 500
SPEED-POPL09_SimpleMultipleDep.c FAILED 90 d + c + -2 + (d + -1) × (c... O(n2) 500
SPEED-POPL09_SimpleSingle.c (4 + (2 * max(0, B))) O(n) 81 b + -1 O(n) 500
SPEED-POPL09_SimpleSingle2.c FAILED 115 d + c + -2 O(n) 500
WTC_aaron2.c (4 + (3 * max(0, ((B - C) +... O(n) 134 b - c O(n) 500
WTC_ax.c (7 + (3 * max(0, (C - 2)))) O(n) 92 c + c + -5 + (c + -3) × (c... O(n2) 500
WTC_complex.c FAILED 96 FAILED 500
WTC_counterex1b.c FAILED 197 FAILED 500
WTC_cousot9.c FAILED 91 c + d + -2 + (c + -1) × (c... O(n2) 500
WTC_easy1.c 124 O(1) 96 39 O(1) 500
WTC_easy2.c (4 + (2 * max(0, A))) O(n) 73 a + -1 O(n) 500
WTC_exmini.c (4 + (2 * max(0, ((((A / 2)... O(n) 95 b - c O(n) 500
WTC_gcd.c FAILED 82 FAILED 500
WTC_insertsort.c (6 + (4 * max(0, (B - 1)))) O(n) 111 b + -2 + (b + -2) × (b + -2) O(n2) 500
WTC_loops.c (5 + (4 * max(0, (A + 1)))) O(n) 88 a + -2 + (a + -3) × (a + -2) O(n2) 500
WTC_nd_loop.c 13 O(1) 74 FAILED 500
WTC_ndecr.c (4 + (2 * max(0, (A - 2)))) O(n) 71 a + -3 O(n) 500
WTC_nestedLoop.c FAILED 140 (b + -1) × max((c + -1), (... O(n2) 500
WTC_perfect.c (6 + (3 * max(0, (A - 1)))) O(n) 174 a + -2 + a × (a + -2) O(n2) 500
WTC_random1d.c (4 + (2 * max(0, A))) O(n) 92 a + -1 O(n) 500
WTC_random2d.c (4 + (7 * max(0, B))) O(n) 392 b + -1 O(n) 500
WTC_realbubble.c (9 + (4 * max(0, (A - 1)))) O(n) 115 a + a + -4 + (a + -3) × (a... O(n2) 500
WTC_realheapsort.c ((11 + (3 * max(0, (A - 1))... O(n) 275 FAILED 1000
WTC_realheapsort_step1.c (6 + (3 * max(0, (A - 1)))) O(n) 173 N + -2 + (N + -2) × (N + -1) O(n2) 500
WTC_realheapsort_step2.c (10 + (4 * max(0, (A - 1)))) O(n) 115 FAILED 500
WTC_realselect.c (5 + (4 * max(0, (B - 1)))) O(n) 93 b + -2 + (b + -3) × (b + -2) O(n2) 500
WTC_realshellsort.c 1+max([10+3*log(2,1+nat(A))... O(log n) 134 FAILED 500
WTC_rsd.c FAILED 95 -1 + a × 2 + a × 2 + (-1... O(n2) 500
WTC_sipma91.c FAILED 152 309 + 9 × (99 - a) + -a + ... O(n) 500
WTC_sipmabubble.c (7 + (3 * max(0, (A + 1)))) O(n) 82 a + a × (a + -1) O(n2) 500
WTC_speedFails4.c FAILED 91 FAILED 500
WTC_speedpldi2.c FAILED 85 FAILED 500
WTC_speedpldi3.c FAILED 92 a + b + -2 + (a + -1) × (b... O(n2) 500
WTC_speedpldi4.c FAILED 80 FAILED 500
WTC_terminate.c (4 + (2 * max(0, ((((A / 2)... O(n) 97 100 - a O(n) 500
WTC_wcet1.c (7 + (4 * max(0, (A - 1)))) O(n) 420 a + -2 O(n) 500
WTC_wcet2.c (5 + (3 * max(0, (A + 5)))) O(n) 88 4 + 8 × (4 - a) + -a O(n) 500
WTC_while2.c (5 + (3 * max(0, B))) O(n) 88 b + -1 + (b + -1) × (b + -1) O(n2) 500
WTC_wise.c TIMEOUT FAILED 500
a.10.c.t2.c FAILED (Irreducible Control Flow) 189 1 (no loops) O(1) 500
acqrel-fail.t2.c FAILED 92 FAILED 500
afagp-fail.t2.c FAILED 47840 FAILED 1000
afagx1.t2.c FAILED 68 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) 40 1 (no loops) O(1) 500
array1.t2.c 1 O(1) 66 1 (no loops) O(1) 500
array2.t2.c 52 O(1) 76 49 O(1) 500
array3.t2.c 103 O(1) 93 98 O(1) 500
array_free.t2.c 44 O(1) 69 41 O(1) 500
array_init.t2.c 12 O(1) 71 9 O(1) 500
array_init_assign.t2.c 7 O(1) 78 2 O(1) 500
ase_example.t2.c 23 O(1) 150 27 O(1) 500
bf10.t2.c 68 O(1) 466 22 O(1) 500
bf11.t2.c 73 O(1) 441 24 O(1) 500
bf12.t2.c 78 O(1) 464 26 O(1) 500
bf13.t2.c 83 O(1) 464 28 O(1) 1000
bf14.t2.c 88 O(1) 463 30 O(1) 500
bf15.t2.c 93 O(1) 461 32 O(1) 500
bf16.t2.c 98 O(1) 466 34 O(1) 500
bf17.t2.c 103 O(1) 462 36 O(1) 500
bf18.t2.c 108 O(1) 457 38 O(1) 500
bf19.t2.c 113 O(1) 465 40 O(1) 500
bf20.t2.c 118 O(1) 465 42 O(1) 1000
bf5.t2.c 43 O(1) 468 12 O(1) 500
bf6.t2.c 48 O(1) 466 14 O(1) 500
bf7.t2.c 53 O(1) 463 16 O(1) 500
bf8.t2.c 58 O(1) 461 18 O(1) 500
bf9.t2.c 63 O(1) 464 20 O(1) 500
bio.t2.c TIMEOUT FAILED 1000
bitcount16.t2.c 18 O(1) 383 15 O(1) 500
bitcount32.t2.c 34 O(1) 377 31 O(1) 500
broydn.c.i.broydn.pl.t2.fixed.t2.c FAILED 123 TIMEOUT
broydn.c.i.broydn.pl.t2.nor.t2.rlgfixed.t2.c (3 + max(0, ((A - B) + 1))) O(n) 23206 TIMEOUT
broydn.t2.c (3 + max(0, ((A - B) + 1))) O(n) 23167 TIMEOUT
brp.t2.c FAILED 7580 1 (no loops) O(1) 500
brp_withassume.t2.c FAILED 8101 FAILED 1000
bs.t2.c FAILED 153 FAILED 500
bsort100.t2.c 10302 O(1) 396 198 O(1) 500
bubbleSort.t2.c ((3 + max(0, C)) + (max(0, ... O(n2) 293 -4 + max(call_to_nondet_lin... O(n) 1000
bubblesort_inner_loop.t2.c 6 O(1) 107 3 O(1) 500
buggyNonTermLoop.t2.c TIMEOUT 1 (no loops) O(1) 500
byron-1.t2.c FAILED 77 FAILED 500
byron-2.t2.c FAILED 98 -4 + (-3 + max(call_to_non... O(n2) 500
byron-3.t2.c FAILED 71 FAILED 500
byron-4.t2.c FAILED 98 FAILED 500
cfg.t2.c FAILED (Irreducible Control Flow) 69 1 (no loops) O(1) 500
cnt.t2.c 243 O(1) 2057 20 O(1) 500
collatz.t2.c FAILED 109 FAILED 500
complex_guard.t2.c 10 O(1) 74 2 O(1) 500
constants.t2.c 402 O(1) 110 399 O(1) 1000
consts1.t2.c FAILED 68 FAILED 500
consts1nt.t2.c FAILED 64 FAILED 500
consts2.t2.c (1 + max(0, ((A / 1000) - (... O(n) 67 -1001 + max(call_to_nondet_... O(n) 500
consts2nt.t2.c FAILED 62 FAILED 500
consts3.t2.c (1 + max(0, (A - 201))) O(n) 129 -202 + max(call_to_nondet_l... O(n) 500
consts3nt.t2.c FAILED 68 FAILED 500
consts4.t2.c (1 + max(0, ((A / 1000) - (... O(n) 67 -1201 + max(call_to_nondet_... O(n) 500
consts4nt.t2.c FAILED 69 FAILED 500
consts5.t2.c FAILED 64 1 (no loops) O(1) 500
consts5nt.t2.c FAILED 71 FAILED 500
costa-jvm-cost_ArrayReverse.c (5 + (3 * max(0, A))) O(n) 58 length O(n) 500
costa-jvm-cost_BST.c -27+52*pow(2,nat(A-1)) EXP 359 not analyzed
costa-jvm-cost_Concat.c ((10 + (3 * max(0, B))) + (... O(n) 78 lengthB + lengthA O(n) 500
costa-jvm-cost_Cons.c (20 + (16 * max(0, (A - 1)))) O(n) 89 Depth(Set(Select(1, _), c)) O(n) 500
costa-jvm-cost_Delete.c (5 + (max(0, D) * max(((21 ... O(n2) 807 la × Depth(Set(Select(1, _... O(n2) 500
costa-jvm-cost_DetEval.c (7 + (3 * max(0, A))) O(n) 1242 la + la + la + la + la + -1... O(n3) 500
costa-jvm-cost_DivByTwo.c 5+3*log(2,1+nat(2*A-1)) O(log n) 54 n O(n) 500
costa-jvm-cost_EvenDigits.c 5+nat(A)* (10+3*log(3,2+nat... O(n log n) 95 n + n × (n + -1) O(n2) 500
costa-jvm-cost_EvenDigitsNew.c 15 O(1) 115 not analyzed
costa-jvm-cost_FactSum.c (5 + (max(0, (A + 1)) * (10... O(n2) 76 n + n × (n + -2) O(n2) 500
costa-jvm-cost_FactSumNew.c (10 + (5 * max(0, B))) O(n) 103 not analyzed
costa-jvm-cost_Factorial.c (6 + (5 * max(0, A))) O(n) 51 n + -2 O(n) 500
costa-jvm-cost_Fibonacci.c -7+13*pow(2,nat(A-1)) EXP 69 not analyzed
costa-jvm-cost_FibonacciNew.c FAILED 64 not analyzed
costa-jvm-cost_Hanoi.c -8+15*pow(2,nat(A)) EXP 71 not analyzed
costa-jvm-cost_Incr.c (5 + (11 * max(0, (A + 1)))) O(n) 178 n O(n) 500
costa-jvm-cost_LinEqSolve.c (9 + (3 * max(0, B))) O(n) 1271 la + la + la + la + la + la... O(n3) 1000
costa-jvm-cost_ListInter.c (11 + (max(0, B) * (25 + (5... O(n2) 223 Depth(Set(Select(1, _), l1)... O(n2) 500
costa-jvm-cost_ListReverse.c (5 + (3 * max(0, B))) O(n) 61 Depth(Set(Select(1, _), x)) O(n) 500
costa-jvm-cost_MatMult.c (5 + (max(0, B) * (7 + (max... O(n3) 177 la + la × lb + la × lb × lb O(n3) 500
costa-jvm-cost_MatrixInverse.c (6 + (3 * max(0, A))) O(n) 1326 la + la + la + la + la + la... O(n3) 500
costa-jvm-cost_MergeList.c (15 + (15 * max(0, (A + B)))) O(n) 177 Depth(Set(Select(1, _), oth... O(n2) 500
costa-jvm-cost_Polynomial.c 71 O(1) 104 min(Select(0, this), 10) O(n) 500
costa-jvm-cost_Power.c (6 + (5 * max(0, A))) O(n) 53 n + -1 O(n) 500
costa-jvm-cost_SelectOrd.c (5 + (max(0, (A - 2)) * (7 ... O(n2) 168 lv + -2 + (lv + -2) × (lv ... O(n2) 500
costa-jvm-cost_ms.c 3+5*log(2,1+nat(-2*C+2*E-1)) O(log n) 251 not analyzed
costa-misc_ack.c FAILED 68 a + -1 O(n) 500
costa-misc_direct_n_log_n.c 1+log(2,1+nat(A-1)) O(log n) 73 a + -2 O(n) 500
costa-misc_divide_and_conquer.c 1+3* (pow(2,nat(2*A+1))-1) EXP 60 not analyzed
costa-misc_exponential.c 1+ (pow(2,nat(1*A))-1) EXP 55 not analyzed
costa-misc_linear.c max(101, (1 + max(0, A))) O(n) 71 FAILED 500
costa-misc_logarithmic.c FAILED 79 1 O(1) 500
costa-misc_merge.c (1 + max(0, ((A + B) - 1))) O(n) 88 a + -1 O(n) 500
costa-misc_ms.c (1 + (3 * max(0, (A - 1)))) O(n) 65 not analyzed
costa-misc_mspe.c (1 + max(0, ((A + B) + 1))) O(n) 571 FAILED 1000
costa-misc_n_log_n.c FAILED 56 not analyzed
costa-misc_no_cover_point.c FAILED 47 not analyzed
costa-misc_quadratic.c (1 + (max(0, A) * (3 + max(... O(n2) 55 n + -1 + (n + -1) × (n + -1) O(n2) 500
cover.t2.c TIMEOUT 177 O(1) 500
crc.t2.c 5210 O(1) 25587 96 O(1) 500
create.t2.c FAILED 265 call_to_nondet_line_66 + -3 O(n) 1000
create_seg.t2.c FAILED 358 call_to_nondet_line_69 + -3 O(n) 500
create_via_tmps.t2.c ((3 + max(0, (A - 2))) + ma... O(n) 16789 -3 + max(call_to_nondet_lin... O(n) 500
ctl.t2.c FAILED 106 FAILED 500
curious.t2.c FAILED 51 FAILED 500
curious2.t2.c not analyzed 1 (no loops) O(1) 500
curious4.t2.c TIMEOUT FAILED 500
d.t2.c FAILED 68 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 87 FAILED 500
destroy.t2.c FAILED 21364 call_to_nondet_line_150 + -... O(n) 500
destroy_seg.t2.c FAILED 46319 call_to_nondet_line_234 + -... O(n) 500
destroy_seg_leak.t2.c FAILED 27064 FAILED 500
disj_nightmare.t2.c not analyzed FAILED 500
disj_nightmare_abi.t2.c FAILED 69 1 O(1) 500
dropbuf-live.t2.c 1 O(1) 67 1 (no loops) O(1) 500
dropbuf.t2.c FAILED 28863 FAILED 1000
dsa_test.t2.c 1 O(1) 68 1 (no loops) O(1) 500
dsa_test1.t2.c 1 O(1) 66 1 (no loops) O(1) 500
dsa_test10.t2.c 23 O(1) 125 18 O(1) 500
dsa_test11.t2.c 1 O(1) 64 1 (no loops) O(1) 500
dsa_test12.t2.c 1 O(1) 64 1 (no loops) O(1) 500
dsa_test13.t2.c 1 O(1) 53 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) 92 18 O(1) 500
dsa_test2.t2.c not analyzed 1 (no loops) O(1) 500
dsa_test4.t2.c 1 O(1) 64 1 (no loops) O(1) 500
dsa_test5.t2.c 1 O(1) 66 1 (no loops) O(1) 500
dsa_test6.t2.c 12 O(1) 74 9 O(1) 500
dsa_test7.t2.c not analyzed 1 (no loops) O(1) 500
dsa_test8.t2.c 1 O(1) 53 1 (no loops) O(1) 500
dsa_test9.t2.c 1 O(1) 63 1 (no loops) O(1) 500
dummy.t2.c FAILED 68 FAILED 500
e-1394complete-succeed.t2.c TIMEOUT FAILED 1000
e-acqrel-fail.t2.c FAILED 79 FAILED 500
e-acqrel-succeed.t2.c FAILED 83 FAILED 500
e-pgarch-fail.t2.c FAILED 203 FAILED 500
e-pgarch-succeed.t2.c FAILED 238 FAILED 500
e-popl07-fail.t2.c FAILED 1052 FAILED 1000
edn.t2.c 2753 O(1) 13287 398 O(1) 500
efegp.t2.c FAILED 18458 FAILED 1000
elmhes.c.i.elmhes.pl.t2.fixed.t2.c FAILED 89 -1 + (max(call_to_nondet_l... O(n2) 1000
elmhes.c.i.elmhes.pl.t2.nor.t2.rlgfixed.t2.c FAILED 859 -1 + (max(call_to_nondet_l... O(n2) 500
elmhes.t2.c FAILED 860 -1 + (max(call_to_nondet_l... O(n2) 1000
eric.t2.c FAILED 101 -4 + max(call_to_nondet_lin... O(n) 1000
eric1.t2.c FAILED 73 FAILED 500
eric2.t2.c FAILED 1626 FAILED 1000
eric3.t2.c FAILED 92 FAILED 500
ex1.t2.c FAILED 79 FAILED 500
ex10.t2.c FAILED 148 FAILED 500
ex11.t2.c FAILED 83 FAILED 500
ex12.t2.c (23 / 2) O(1) 72 17 O(1) 500
ex13.t2.c 1 O(1) 66 1 (no loops) O(1) 500
ex14.t2.c 12 O(1) 79 9 O(1) 500
ex15.t2.c 1 O(1) 70 1 (no loops) O(1) 500
ex16.t2.c FAILED 454 FAILED 500
ex17.t2.c 102 O(1) 179 FAILED 1000
ex18.t2.c FAILED 137 FAILED 500
ex19.t2.c FAILED 87 FAILED 1000
ex2.t2.c FAILED 75 FAILED 500
ex20.t2.c 1026 O(1) 114 1023 O(1) 500
ex21.t2.c 203 O(1) 120 198 O(1) 500
ex22.t2.c 390 O(1) 5420 366 O(1) 500
ex23.t2.c 38 O(1) 79 35 O(1) 500
ex26.t2.c 203 O(1) 127 198 O(1) 500
ex27.t2.c 595 O(1) 15104 565 O(1) 500
ex29.t2.c 4 O(1) 175 1 (no loops) O(1) 500
ex3.t2.c 12 O(1) 84 9 O(1) 500
ex30.t2.c FAILED 168 call_to_nondet_line_56 + ca... O(n) 500
ex31.t2.c FAILED 68 FAILED 1000
ex32.t2.c 2003 O(1) 108 1998 O(1) 500
ex33.t2.c 1 O(1) 71 1 (no loops) O(1) 500
ex34.t2.c 1 O(1) 281 1 (no loops) O(1) 500
ex36.t2.c FAILED 24757 FAILED 11000
ex37.t2.c 1 O(1) 64 1 (no loops) O(1) 500
ex4.t2.c 34 O(1) 318 18 O(1) 500
ex40.t2.c FAILED 51 FAILED 500
ex6.t2.c 1 O(1) 61 1 (no loops) O(1) 500
ex7.t2.c 12 O(1) 94 9 O(1) 500
ex8.t2.c FAILED 111 FAILED 500
ex9.t2.c FAILED 121 FAILED 500
example.t2.c (1 + max(0, ((A + B) - 2))) O(n) 84 -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) 502 14 O(1) 500
fermat.t2.c 9 O(1) 953 6 O(1) 500
fibcall.t2.c 31 O(1) 185 28 O(1) 500
fir.t2.c FAILED 997 7 + 9 × (-2 + max(call_to_... O(n) 1000
firewire.t2.c FAILED 45033 FAILED 3000
flipflop.t2.c FAILED 62 FAILED 500
fourn.c.i.fourn.pl.t2.fixed.t2.c FAILED 88 FAILED 1000
fourn.c.i.fourn.pl.t2.nor.t2.rlgfixed.t2.c FAILED 4317 FAILED 2000
fourn.t2.c FAILED 4291 FAILED 1000
fuhs-inflasso.t2.c FAILED 74 -2 + (-1 + max(call_to_non... O(n2) 500
fun1.t2.c TIMEOUT FAILED 1000
fun10.t2.c FAILED (Irreducible Control Flow) 57663 FAILED (Irreducible Control Flow) 500
fun10b.t2.c FAILED (Irreducible Control Flow) 50929 FAILED (Irreducible Control Flow) 500
fun11.t2.c FAILED 105 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 FAILED 80 FAILED 500
fun4.t2.c FAILED 87 FAILED 500
fun5.t2.c TIMEOUT FAILED 2000
fun6.t2.c FAILED (Irreducible Control Flow) 444 FAILED (Irreducible Control Flow) 500
fun7.t2.c FAILED (Irreducible Control Flow) 873 FAILED (Irreducible Control Flow) 500
fun8.t2.c FAILED 25106 27 O(1) 500
fun9.t2.c TIMEOUT FAILED 500
graycode.t2.c 39 O(1) 9856 43 O(1) 500
heidy1.t2.c FAILED 68 FAILED 500
heidy10.t2.c FAILED 73 call_to_nondet_line_27 + -2... O(n2) 500
heidy2.t2.c FAILED 70 FAILED 500
heidy3.t2.c FAILED 80 FAILED 1000
heidy5.t2.c (2 + max(0, B)) O(n) 83 -1 + max(call_to_nondet_lin... O(n) 500
heidy6.t2.c FAILED 88 FAILED 500
heidy7-simple.t2.c FAILED 77 FAILED 500
heidy7.t2.c FAILED 93 FAILED 500
heidy8.t2.c FAILED 138 FAILED 500
heidy9.t2.c (2 + max(0, A)) O(n) 74 -1 + max(call_to_nondet_lin... O(n) 500
hongyi1.t2.c (11 + (3 * max(0, D))) O(n) 16934 FAILED 1000
hqr.c.i.hqr.pl.t2.fixed.t2.c FAILED 213 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 FAILED 821 27 + max(call_to_nondet_lin... O(n) 500
iecs.t2.c FAILED 46 FAILED 500
insertsort.t2.c FAILED 58 FAILED 500
intSqRoot.t2.c FAILED 73 FAILED 500
invgen.t2.c (1 + max(0, (B + 1))) O(n) 74 max(call_to_nondet_line_5, ... O(n) 500
jacobi.c.i.jacobi.pl.t2.fixed.t2.c FAILED 108 -12 + (-1 + max((call_to_n... O(n3) 10000
jacobi.c.i.jacobi.pl.t2.nor.t2.rlgfixed.t2.c FAILED 3825