Complexity: C Integer
benchmark
CoFloCo 2018
AProVE
score
lower
upper
time
score
lower
upper
time
Flores-Montoya_2017/
examples_from_literature/
Other/
exclusive_phases.c
2
1
n
1
0.18/0.26
1
1
n
2
2.57/1.59
Flores-Montoya_2017/
examples_from_literature/
Other/
ex_paper1.c
2
1
n
2
0.39/0.46
2
1
n
2
13.91/12.72
Flores-Montoya_2017/
examples_from_literature/
Other/
ex_paper3.c
2
1
n
2
0.36/0.43
2
1
n
2
6.82/5.48
Flores-Montoya_2017/
examples_from_literature/
Other/
ex_paper2.c
2
1
n
2
0.18/0.34
2
1
n
2
2.20/1.23
Flores-Montoya_2017/
examples_from_literature/
Loopus/
Loopus2015_ex2.c
2
1
n
1
0.26/0.34
2
1
n
1
2.75/1.61
Flores-Montoya_2017/
examples_from_literature/
Loopus/
Loopus2011_ex1.c
2
1
n
1
0.30/0.38
2
1
n
1
3.05/1.93
Flores-Montoya_2017/
examples_from_literature/
Loopus/
Loopus2011_ex2.c
2
1
n
1
2.44/2.50
0
1
∞
48.76/46.89
Flores-Montoya_2017/
examples_from_literature/
Loopus/
Loopus2014_ex1.c
2
1
n
2
0.97/1.04
2
1
n
2
6.73/5.32
Flores-Montoya_2017/
examples_from_literature/
Loopus/
Loopus2015_original.c
2
1
n
1
0.55/0.63
2
1
n
1
4.42/3.08
Flores-Montoya_2017/
examples_from_literature/
Loopus/
Loopus2015_big.c
2
1
n
1
0.74/0.82
2
1
n
1
7.32/5.84
Flores-Montoya_2017/
examples_from_literature/
Loopus/
Loopus2014_ex2.c
2
1
n
1
0.31/0.39
2
1
n
1
3.55/2.52
Flores-Montoya_2017/
examples_from_literature/
Loopus/
Loopus2015_ex1.c
2
1
n
1
0.24/0.34
1
1
n
2
3.32/2.16
Flores-Montoya_2017/
examples_from_literature/
Loopus/
Loopus2011_ex3.c
2
1
n
1
0.20/0.28
2
1
n
1
2.67/1.79
Sinn_2016/
CPU2006_ParseFile.c
StarExec error
0
1
∞
302.77/297.60
Sinn_2016/
CPU2006_Configure.c
2
1
n
1
0.58/0.66
2
1
n
1
8.19/6.64
Sinn_2016/
CPU2006_local_alloc.c
2
1
n
1
0.27/0.35
1
1
n
2
2.39/1.34
Sinn_2016/
cBench_cf_decode_eol.c
2
1
n
1
0.75/0.82
1
1
n
2
9.68/8.11
Sinn_2016/
CPU2006_load_mems.c
2
1
n
2
0.64/0.72
1
1
n
3
6.81/5.38
Sinn_2016/
cBench_hc_compute.c
2
1
n
2
0.39/0.47
1
1
n
3
5.54/4.20
Sinn_2016/
cBench_cryptRandWriteFile.c
2
1
n
1
0.20/0.28
2
1
n
1
2.64/1.62
Sinn_2016/
cBench_inflated_stored.c
2
1
n
1
0.59/0.67
1
1
n
2
11.34/9.89
Sinn_2016/
cBench_bin_search_StepSize2.c
0
1
∞
142.59/142.66
0
1
∞
25.29/25.06
Sinn_2016/
cBench_s_SFD_process.c
2
1
n
1
0.38/0.46
1
1
n
3
15.53/13.82
Sinn_2016/
CPU2006_xdr3dfcoord.c
2
1
n
1
1.42/1.50
1
1
n
2
13.13/11.63
Sinn_2016/
cBench_subsetdump.c
2
1
n
1
0.38/0.46
1
1
n
2
5.57/4.19
Sinn_2016/
CPU2006_asctoeg.c
2
1
n
2
0.44/0.51
2
1
n
2
4.22/3.01
Sinn_2016/
cBench_noiseTickSize.c
2
1
n
1
0.21/0.29
1
1
n
2
4.53/3.12
Sinn_2016/
cBench_PackBitsEncode.c
0
1
∞
14.18/14.23
0
1
∞
179.94/177.36
Sinn_2016/
cBench_render_ht.c
2
1
n
1
0.14/0.22
2
1
n
1
2.73/1.63
Sinn_2016/
cBench_send_tree.c
2
1
n
1
0.82/0.90
2
1
n
1
6.08/4.63
Sinn_2016/
CPU2006_XNU.c
2
1
n
1
0.74/0.82
2
1
n
1
7.42/5.97
Sinn_2016/
cBench_set_color_ht.c
2
1
n
2
0.39/0.47
2
1
n
2
3.10/1.83
Sinn_2016/
CPU2006_ApplyBndRobin.c
2
1
n
4
2.54/2.60
0
1
∞
114.79/112.27
Sinn_2016/
cBench_sendMTFValues.c
2
1
n
1
2.34/2.41
1
1
n
2
11.62/9.83
Sinn_2016/
cBench_encode_mcu_AC_refine.c
2
1
n
1
0.36/0.44
2
1
n
1
5.26/3.83
Sinn_2016/
CPU2006_analyse_other.c
2
1
n
3
1.92/1.99
0
1
∞
299.16/296.37
Sinn_2016/
cBench_zwritehexstring_at.c
2
1
n
1
0.21/0.29
2
1
n
1
2.71/1.66
Sinn_2016/
CPU2006_Perl_scan_vstring.c
2
1
n
2
4.34/4.39
2
1
n
2
35.45/33.46
Sinn_2016/
CPU2006_SingleLinkCluster.c
2
1
n
2
0.98/1.05
2
1
n
2
7.11/5.73
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
wcet2.c
2
1
n
1
0.19/0.27
2
1
n
1
2.35/1.30
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedNestedMultipleDep.c
2
1
n
2
0.22/0.30
2
1
n
2
2.22/1.26
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
nestedLoop.c
2
1
n
2
0.56/0.64
1
1
n
3
48.64/46.86
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
heapsort.c
2
1
n
1
0.39/0.46
2
1
n
1
5.64/4.16
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
terminate.c
2
1
n
1
0.17/0.25
2
1
n
1
2.23/1.22
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
random2d.c
2
1
n
1
0.21/0.30
2
1
n
1
4.73/3.24
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
loops.c
2
1
n
2
0.20/0.28
2
1
n
2
2.64/1.53
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
perfect1.c
2
1
n
2
0.30/0.38
2
1
n
2
3.09/1.92
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedFails4.c
0
1
∞
0.20/0.28
0
1
∞
4.19/3.13
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedpldi2.c
2
1
n
1
0.22/0.30
2
1
n
1
2.52/1.43
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedpldi4.c
2
1
n
1
0.19/0.27
2
1
n
1
2.50/1.45
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
realselect.c
2
1
n
2
0.20/0.28
2
1
n
2
2.63/1.58
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
rank1.c
2
1
n
2
0.52/0.60
2
1
n
2
11.41/10.15
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedSingleSingle.c
2
1
n
1
0.13/0.21
2
1
n
1
2.28/1.35
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
nested_loop.c
2
1
n
2
1.39/1.47
1
1
n
3
12.66/11.08
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
rsd.c
2
1
n
1
0.35/0.46
2
1
n
1
2.99/2.46
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
exmini.c
2
1
n
1
0.17/0.25
2
1
n
1
2.29/1.35
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
easy1.c
0
1
∞
0.17/0.25
0
1
∞
2.32/1.30
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedSimpleMultipleDep.c
2
1
n
2
0.22/0.30
2
1
n
2
2.38/1.40
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
rank3.c
0
1
∞
3.67/3.75
0
1
∞
21.17/20.67
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
cousot9.c
2
1
n
2
0.18/0.27
2
1
n
2
2.51/2.13
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedFails3.c
0
1
∞
0.24/0.32
0
1
∞
3.16/2.14
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
insertsort.c
2
1
n
2
0.23/0.31
2
1
n
2
3.03/2.06
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
realheapsort_step1.c
2
1
n
2
0.24/0.32
2
1
n
2
3.64/2.50
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
realshellsort.c
2
1
n
3
0.48/0.56
2
1
n
3
4.67/3.32
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedFails1.c
0
1
∞
0.14/0.22
0
1
∞
4.17/3.03
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
aaron2.c
2
1
n
1
0.19/0.27
2
1
n
1
2.94/1.92
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
terminatorbubble.c
2
1
n
2
0.47/0.54
2
1
n
2
3.64/2.31
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
random1d.c
2
1
n
1
0.14/0.22
2
1
n
1
2.56/1.51
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
wise.c
2
1
n
1
0.18/0.26
2
1
n
1
2.49/1.47
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedSingleSingle2.c
2
1
n
1
0.27/0.35
2
1
n
1
4.88/3.79
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
catmouse.c
0
1
∞
0.16/0.25
0
1
∞
2.61/1.62
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
ndecr.c
2
1
n
1
0.12/0.20
2
1
n
1
2.11/1.18
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
serpent.c
StarExec error
0
1
∞
11.87/10.45
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
ax.c
2
1
n
2
0.20/0.28
2
1
n
2
2.43/1.33
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
realheapsort_step2.c
2
1
n
2
0.67/0.75
2
1
n
2
7.41/6.00
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedSimpleMultiple.c
2
1
n
1
0.20/0.28
2
1
n
1
2.39/1.40
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
easy2.c
2
1
n
1
0.12/0.20
2
1
n
1
2.08/1.25
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
sipma91.c
2
1
n
1
0.26/0.37
2
1
n
1
4.44/3.35
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
sipmamergesort.c
2
1
n
2
3.77/3.84
0
1
∞
34.86/32.63
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedDis2.c
2
1
n
1
0.17/0.25
2
1
n
1
2.42/1.39
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
counterex1c.c
0
1
∞
0.42/0.50
0
1
∞
19.28/17.66
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
gcd.c
2
1
n
1
0.26/0.36
0
1
∞
3.06/1.92
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
alain.c
2
1
n
2
0.38/0.46
1
1
n
3
3.48/2.12
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
unperfect.c
2
1
n
2
0.33/0.42
2
1
n
2
3.13/1.95
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedpldi3.c
2
1
n
2
0.26/0.35
2
1
n
2
2.56/1.54
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
sipmabubble.c
2
1
n
2
0.18/0.26
2
1
n
2
2.63/1.92
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedNestedMultiple.c
2
1
n
1
0.36/0.44
2
1
n
1
3.18/2.00
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
realbubble.c
2
1
n
2
0.28/0.36
2
1
n
2
4.36/3.17
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
realheapsort.c
0
1
∞
0.73/0.80
0
1
∞
102.20/99.85
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
while2.c
2
1
n
2
0.17/0.25
2
1
n
2
2.34/1.24
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedDis1.c
2
1
n
1
0.19/0.27
2
1
n
1
2.46/1.43
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
speedFails2.c
0
1
∞
0.15/0.24
0
1
∞
2.50/1.43
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
aaron3.c
0
1
∞
0.21/0.29
0
1
∞
6.92/5.49
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
relation1.c
0
1
∞
0.09/0.07
0
1
∞
2.13/1.13
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
perfect.c
2
1
n
2
0.29/0.45
2
1
n
2
2.84/1.84
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
wcet0.c
2
1
n
1
0.29/0.37
2
1
n
1
2.82/1.88
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
counterex1b.c
0
1
∞
4.77/4.85
0
1
∞
13.91/12.47
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
aaron12.c
0
1
∞
0.16/0.24
0
1
∞
0.56/0.38
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
complex.c
2
1
n
1
0.75/0.83
2
1
n
1
2.72/1.63
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
nd_loop.c
0
1
∞
0.12/0.21
0
1
∞
2.50/1.51
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
sipmamergesort2.c
2
1
n
2
18.83/18.88
0
1
∞
250.90/247.97
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
perfect2.c
2
1
n
2
0.34/0.41
2
1
n
2
3.24/2.02
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
rank2.c
2
1
n
1
0.26/0.34
2
1
n
1
3.13/2.17
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
counterex1a.c
0
1
∞
0.68/0.76
0
1
∞
17.89/21.57
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
wcet1.c
2
1
n
1
0.31/0.39
2
1
n
1
3.11/1.97
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
perfectg.c
2
1
n
2
0.33/0.41
2
1
n
2
3.00/1.92
Flores-Montoya_2017/
examples_from_literature/
WTC_V2/
real2.c
0
1
∞
0.27/0.35
0
1
∞
8.27/7.08
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Hanoi_3vars_false-termination.c
0
1
∞
0.13/0.22
0
1
∞
6.61/5.54
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
2Nested_false-termination.c
0
1
∞
0.13/0.21
0
1
∞
3.89/2.85
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Cairo_nondet_false-termination.c
0
1
∞
0.15/0.23
0
1
∞
2.92/1.76
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Bangalore_false-termination.c
0
1
∞
0.13/0.25
0
1
∞
3.68/2.63
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Singapore_plus_false-termination.c
0
1
∞
0.13/0.21
0
1
∞
3.83/2.82
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Singapore_v2_false-termination.c
0
1
∞
0.13/0.22
0
1
∞
3.64/2.65
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
McCarthy91_Iteration_true-termination.c
0
1
∞
0.15/0.23
2
1
n
2
2.48/1.44
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Cairo_step2_false-termination.c
0
1
∞
0.14/0.22
0
1
∞
2.55/1.48
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Copenhagen_disj_true-termination.c
0
1
∞
0.14/0.22
0
1
∞
2.76/1.63
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Gothenburg_v2_true-termination.c
2
1
n
1
0.18/0.26
0
1
∞
4.47/3.36
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Hanoi_2vars_false-termination.c
0
1
∞
0.12/0.21
0
1
∞
4.10/3.03
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Mysore_false-termination.c
0
1
∞
0.13/0.22
0
1
∞
5.73/4.63
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Benghazi_nondet_true-termination.c
0
1
∞
0.14/0.26
0
1
∞
4.52/3.45
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Singapore_v1_false-termination.c
0
1
∞
0.13/0.21
0
1
∞
3.89/2.76
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Bangalore_v3_false-termination.c
0
1
∞
0.14/0.22
0
1
∞
3.55/2.54
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Bangalore_v2_false-termination.c
0
1
∞
0.14/0.22
0
1
∞
3.56/2.54
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Hanoi_plus_false-termination.c
0
1
∞
0.14/0.22
0
1
∞
5.82/4.68
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Singapore_true-termination.c
0
1
∞
0.15/0.23
0
1
∞
4.51/3.30
Flores-Montoya_2017/
Adapted_from_Ton_Chanh_15/
Bangalore_v4_true-termination.c
0
1
∞
0.13/0.24
0
1
∞
2.29/1.29
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
knuth_morris_pratt.c
StarExec error
2
1
n
1
3.86/2.56
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t15.c
2
1
n
1
0.21/0.29
2
1
n
1
2.54/1.52
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_pldi09_fig4_4.c
2
1
n
1
0.19/0.27
2
1
n
1
2.42/1.35
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_popl10_simple_multiple.c
2
1
n
1
0.20/0.28
2
1
n
1
2.39/1.37
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t19.c
2
1
n
1
0.17/0.25
2
1
n
1
2.41/1.28
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_popl10_nested_single.c
2
1
n
1
0.27/0.35
2
1
n
1
2.85/1.70
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_pldi10_ex1.c
2
1
n
2
0.29/0.37
2
1
n
2
4.00/2.78
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t30.c
0
1
∞
0.12/0.21
0
1
∞
3.56/2.40
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t20.c
2
1
n
1
0.18/0.26
2
1
n
1
2.26/1.27
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t13.c
2
1
n
1
0.24/0.32
1
1
n
2
3.30/2.12
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_popl10_simple_single.c
2
1
n
1
0.13/0.21
2
1
n
1
2.28/1.30
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t10.c
2
1
n
1
0.15/0.23
2
1
n
1
2.58/1.62
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_popl10_simple_single_2.c
2
1
n
1
0.23/0.31
2
1
n
1
2.29/1.31
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t62.c
2
1
n
1
0.55/0.63
2
1
n
1
5.15/3.70
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t08.c
2
1
n
1
0.18/0.26
2
1
n
1
2.47/1.34
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_popl10_nested_multiple.c
2
1
n
1
0.36/0.44
2
1
n
1
3.30/2.02
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t28.c
2
1
n
1
0.26/0.34
2
1
n
1
2.44/1.46
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t07.c
2
1
n
1
0.21/0.29
2
1
n
1
2.53/1.37
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t27.c
2
1
n
1
0.24/0.32
2
1
n
1
2.53/1.54
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
gcd.c
2
1
n
1
0.24/0.34
2
1
n
1
2.47/1.46
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_pldi09_fig4_2.c
2
1
n
1
0.21/0.29
2
1
n
1
2.44/1.41
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_popl10_fig2_2.c
2
1
n
1
0.17/0.25
2
1
n
1
2.53/1.44
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_pldi09_fig4_5.c
2
1
n
1
0.24/0.32
1
1
n
2
3.09/2.02
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_pldi09_fig1.c
2
1
n
1
0.18/0.32
1
1
n
2
2.67/1.59
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_popl10_fig2_1.c
2
1
n
1
0.19/0.27
2
1
n
1
2.42/1.44
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t11.c
2
1
n
1
0.19/0.35
2
1
n
1
2.55/1.49
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t47.c
2
1
n
1
0.14/0.22
2
1
n
1
2.25/1.23
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_pldi10_ex3.c
2
1
n
1
0.23/0.31
2
1
n
1
2.67/1.72
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_pldi10_ex4.c
2
1
n
1
0.18/0.27
2
1
n
1
2.39/1.31
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
speed_popl10_sequential_single.c
2
1
n
1
0.20/0.29
2
1
n
1
2.82/1.68
Flores-Montoya_2017/
examples_from_literature/
C4B_examples/
t16.c
2
1
n
1
0.19/0.28
1
1
n
2
2.74/1.76
Flores-Montoya_2017/
examples_from_literature/
ABC/
jama_ex5.c
2
1
n
2
0.18/0.27
2
1
n
2
2.28/1.22
Flores-Montoya_2017/
examples_from_literature/
ABC/
jama_ex7.c
2
1
n
2
0.19/0.86
2
1
n
2
2.45/1.33
Flores-Montoya_2017/
examples_from_literature/
ABC/
jama_ex4.c
2
1
n
2
0.23/3.42
2
1
n
2
2.57/1.37
Flores-Montoya_2017/
examples_from_literature/
ABC/
jama_ex1.c
2
1
n
2
0.18/0.26
2
1
n
2
2.40/1.28
Flores-Montoya_2017/
examples_from_literature/
ABC/
textbook_ex2.c
2
1
n
2
0.18/0.26
2
1
n
2
2.32/1.24
Flores-Montoya_2017/
examples_from_literature/
ABC/
textbook_ex1.c
2
1
n
1
0.13/0.21
2
1
n
1
2.26/1.24
Flores-Montoya_2017/
examples_from_literature/
ABC/
jama_ex6.c
2
1
n
3
0.50/0.62
1
1
n
4
2.47/1.50
Flores-Montoya_2017/
examples_from_literature/
ABC/
textbook_ex3.c
2
1
n
4
0.39/1.23
1
1
n
6
2.46/1.47
Flores-Montoya_2017/
examples_from_literature/
ABC/
jama_ex2.c
2
1
n
2
0.18/0.27
2
1
n
2
2.09/1.26
Flores-Montoya_2017/
examples_from_literature/
ABC/
jama_ex3.c
2
1
n
2
0.18/0.26
2
1
n
2
2.40/1.26
Flores-Montoya_2017/
examples_from_literature/
ABC/
textbook_ex4.c
2
1
n
2
0.22/0.33
2
1
n
2
2.36/1.27
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Bangalore_true-termination.c
2
1
n
1
0.13/0.22
2
1
n
1
2.48/1.36
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-counterex1a_true-termination.c
0
1
∞
0.69/0.77
0
1
∞
20.90/19.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.02.c
2
1
n
1
0.13/0.21
2
1
n
1
2.31/1.22
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
LogMult.c
0
1
∞
0.13/0.21
0
1
∞
0.51/0.35
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Ex03.c
0
1
∞
0.16/0.24
0
1
∞
2.52/1.56
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Mysore_true-termination.c
2
1
n
1
0.14/0.23
2
1
n
1
2.50/1.36
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Ex07.c
0
1
∞
0.13/0.21
0
1
∞
2.23/1.27
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.05.c
2
1
n
1
0.16/0.24
2
1
n
1
2.79/1.63
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NonTermination1_false-termination.c
0
1
∞
0.11/0.19
0
1
∞
3.25/2.24
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
easy2_true-termination.c
2
1
n
1
0.12/0.20
2
1
n
1
2.15/1.19
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ConvLower.c
0
1
∞
0.16/0.24
0
1
∞
2.55/1.57
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaB3.c
2
1
n
1
0.14/0.22
2
1
n
1
2.27/3.32
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex3.05_true-termination.c
0
1
∞
0.16/0.24
0
1
∞
2.73/1.88
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination.c
0
1
∞
0.13/0.21
0
1
∞
2.80/1.82
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Urban-WST2013-Fig2-modified1000_true-termination.c
2
1
n
1
0.15/0.27
2
1
n
1
2.25/1.26
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
TelAviv-Amir-Minimum_true-termination.c
0
1
∞
0.20/0.29
0
1
∞
5.78/4.45
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination.c
2
1
n
1
0.16/0.24
1
1
n
2
2.28/1.28
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-counterex1b_true-termination.c
0
1
∞
4.77/4.84
0
1
∞
14.94/13.47
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Factorial.c
0
1
∞
0.14/0.22
0
1
∞
2.44/1.45
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
DivMinus.c
2
1
n
1
0.14/0.22
2
1
n
1
2.32/1.30
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-termination.c
0
1
∞
0.13/0.22
0
1
∞
3.63/2.47
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Masse-VMCAI2014-Fig1a_true-termination.c
2
1
n
2
0.35/0.44
1
1
n
3
2.60/1.48
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_a.05.c
2
1
n
1
0.13/0.21
2
1
n
1
2.06/1.18
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
LeikeHeizmann-WST2014-Ex5_false-termination.c
0
1
∞
0.13/0.21
0
1
∞
2.82/1.72
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_true-termination.c
0
1
∞
0.17/0.28
0
1
∞
0.57/0.46
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Ex04.c
0
1
∞
0.08/0.08
0
1
∞
2.10/1.16
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
GopanReps-CAV2006-Fig1a_true-termination.c.c
0
1
∞
0.16/0.25
0
1
∞
2.47/1.35
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-wise_true-termination.c
2
1
n
1
0.19/0.27
2
1
n
1
2.32/1.37
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ComplxStruc.c
0
1
∞
0.26/0.39
0
1
∞
5.33/4.22
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Fibonacci.c
0
1
∞
0.15/0.26
0
1
∞
2.77/1.61
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
LeikeHeizmann-TACAS2014-Ex9_true-termination.c
2
1
n
1
0.18/0.28
2
1
n
1
2.59/1.65
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
WhileNestedOffset.c
0
1
∞
0.17/0.25
0
1
∞
3.25/2.23
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaB16.c
2
1
n
1
0.19/0.32
2
1
n
1
2.24/1.33
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NonTerminationSimple5_false-termination.c
0
1
∞
0.14/0.22
0
1
∞
3.58/3.25
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
GulavaniGulwani-CAV2008-Fig1c_true-termination.c
2
1
n
1
0.13/0.21
2
1
n
1
2.33/1.34
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
GCD4.c
2
1
n
1
0.22/0.32
0
1
∞
2.29/1.33
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
BrockschmidtCookFuhs-CAV2013-Fig1_true-termination.c
2
1
n
2
0.22/0.30
2
1
n
2
2.27/1.32
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.19_true-termination.c
0
1
∞
0.13/0.26
0
1
∞
4.72/3.70
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaB14.c
2
1
n
1
0.20/0.28
2
1
n
1
2.28/1.35
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-Fig2b_true-termination.c
0
1
∞
4.66/4.74
0
1
∞
21.63/20.19
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
GulavaniGulwani-CAV2008-Fig1a_true-termination.c
2
1
n
1
0.17/0.25
2
1
n
1
2.45/1.43
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaB1.c
2
1
n
1
0.13/0.21
2
1
n
1
2.35/1.26
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaC7.c
2
1
n
1
0.16/0.24
2
1
n
1
2.39/1.23
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.04.c
0
1
∞
0.12/0.20
0
1
∞
2.14/1.20
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
UpAndDown.c
0
1
∞
0.23/0.31
0
1
∞
4.47/3.20
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
McCarthyIterative.c
0
1
∞
0.15/0.23
2
1
n
2
2.44/1.42
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
MenloPark_true-termination.c
2
1
n
1
0.15/0.24
0
1
∞
3.31/2.28
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Lcm.c
0
1
∞
0.16/0.24
0
1
∞
2.76/1.76
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_a.08.c
2
1
n
1
0.13/0.21
2
1
n
1
2.15/1.21
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
UrbanMine-ESOP2014-Fig3_true-termination.c
0
1
∞
0.30/0.38
0
1
∞
14.46/12.86
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ColonSipma-TACAS2001-Fig1_true-termination.c
2
1
n
1
0.16/0.25
2
1
n
1
2.27/1.29
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_01.c
0
1
∞
0.11/0.19
0
1
∞
2.11/1.24
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
LeikeHeizmann-TACAS2014-Ex8_true-termination.c
0
1
∞
0.16/0.24
0
1
∞
4.20/4.76
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NonTermination4_false-termination.c
0
1
∞
0.11/0.19
0
1
∞
2.90/1.80
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_a.07.c
2
1
n
1
0.17/0.25
2
1
n
1
2.19/2.23
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
CookSeeZuleger-TACAS2013-Fig1_true-termination.c
0
1
∞
0.17/0.25
0
1
∞
6.90/5.81
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NoriSharma-FSE2013-Fig8_true-termination.c
2
1
n
2
0.23/0.31
1
1
n
3
3.22/2.74
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_java_Continue1.c
0
1
∞
0.13/0.22
0
1
∞
2.21/1.20
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex3.07_true-termination.c
0
1
∞
0.14/0.22
0
1
∞
3.86/2.84
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AlternKonv.c
0
1
∞
0.38/0.46
0
1
∞
3.97/2.81
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-termination.c
0
1
∞
0.13/0.21
0
1
∞
4.25/3.12
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
UpAndDownIneq.c
0
1
∞
0.21/0.29
0
1
∞
3.92/3.35
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_java_Nested.c
0
1
∞
0.15/0.23
0
1
∞
2.37/1.21
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-termination.c
0
1
∞
0.13/0.22
0
1
∞
10.25/9.02
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_flag.c
2
1
n
1
0.17/0.25
2
1
n
1
2.23/1.25
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_c.01-no-inv.c
2
1
n
2
0.19/0.27
2
1
n
2
2.51/1.40
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_13.c
0
1
∞
0.15/0.23
0
1
∞
3.07/1.92
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Nyala-2lex_true-termination.c
0
1
∞
0.16/0.24
0
1
∞
7.18/7.18
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Toulouse-BranchesToLoop_true-termination.c
0
1
∞
0.21/0.30
0
1
∞
3.41/2.38
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
WhileNested.c
0
1
∞
0.16/0.24
0
1
∞
3.26/2.18
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_a.09_assume.c
2
1
n
1
0.15/0.23
2
1
n
1
2.39/1.23
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
min_rf_true-termination.c
0
1
∞
3.69/3.77
2
1
n
1
4.87/3.63
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaC9.c
0
1
∞
0.17/0.25
0
1
∞
6.68/5.43
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Middle.c
0
1
∞
0.16/0.25
0
1
∞
2.47/1.55
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c
0
1
∞
0.13/0.22
0
1
∞
6.26/5.04
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.16.c
2
1
n
1
0.18/0.27
2
1
n
1
2.31/1.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
BradleyMannaSipma-CAV2005-Fig1_true-termination.c
2
1
n
1
0.26/0.34
0
1
∞
2.83/1.87
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NonTerminationSimple6_false-termination.c
0
1
∞
0.11/0.19
0
1
∞
2.59/1.71
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
MirrorIntervSim.c
0
1
∞
0.19/0.27
0
1
∞
2.92/1.87
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
LeikeHeizmann-TACAS2014-Ex7_true-termination.c
0
1
∞
0.13/0.21
0
1
∞
3.50/2.52
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Overflow.c
2
1
n
1
0.12/0.20
2
1
n
1
2.09/1.16
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-termination.c
0
1
∞
0.13/0.21
0
1
∞
3.08/2.05
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_21.c
0
1
∞
0.11/0.19
0
1
∞
2.33/1.28
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaA5.c
2
1
n
1
0.13/0.21
2
1
n
1
2.29/1.21
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NonTerminationSimple4_false-termination.c
0
1
∞
0.12/0.20
0
1
∞
2.39/1.98
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_java_AG313.c
2
1
n
1
0.15/0.23
2
1
n
1
2.38/1.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_true-termination.c
0
1
∞
0.17/0.25
0
1
∞
2.87/1.72
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NonTerminationSimple8_false-termination.c
0
1
∞
0.21/0.29
0
1
∞
20.08/18.45
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.09_assume.c
StarExec error
2
1
n
2
2.22/1.29
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
aaron3_true-termination.c
0
1
∞
0.27/0.34
0
1
∞
9.84/9.56
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
easy1_true-termination.c
0
1
∞
0.18/0.26
0
1
∞
2.29/1.21
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NarrowKonv.c
0
1
∞
0.22/0.30
0
1
∞
3.33/2.14
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaB15.c
2
1
n
1
0.22/0.31
2
1
n
1
2.54/1.39
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ComplInterv2.c
0
1
∞
0.18/0.26
0
1
∞
3.05/1.98
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-speedFails4_true-termination.c
0
1
∞
0.22/0.92
0
1
∞
3.99/2.90
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Flip.c
0
1
∞
0.30/0.38
0
1
∞
2.57/1.55
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_true-termination.c
0
1
∞
0.14/0.22
2
1
n
1
2.41/1.41
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex1.02_true-termination.c
2
1
n
1
0.17/0.25
2
1
n
1
2.60/1.64
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaA4.c
2
1
n
1
0.12/0.21
2
1
n
1
2.12/1.20
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Ex06.c
0
1
∞
0.17/0.25
0
1
∞
2.60/1.58
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
BrockschmidtCookFuhs-CAV2013-Introduction_true-termination.c
2
1
n
1
0.13/0.21
2
1
n
1
2.15/1.48
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaA1.c
2
1
n
2
0.17/0.25
2
1
n
2
2.38/1.30
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NonTerminationSimple3_false-termination.c
0
1
∞
0.13/0.21
0
1
∞
3.42/2.72
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaC2.c
2
1
n
2
0.17/0.29
2
1
n
2
2.29/1.25
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination.c
StarExec error
0
1
∞
3.34/2.33
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.11.c
2
1
n
1
0.25/0.32
2
1
n
1
2.54/1.34
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_c.01_assume.c
2
1
n
2
0.22/0.30
2
1
n
2
2.43/1.35
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.13.c
StarExec error
2
1
n
1
2.94/1.96
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_c.03.c
2
1
n
1
0.17/0.25
2
1
n
1
2.52/1.39
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Madrid_false-termination.c
0
1
∞
0.09/0.08
0
1
∞
2.09/1.18
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_12.c
0
1
∞
0.14/0.22
0
1
∞
2.68/1.74
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Rotation180_false-termination.c
0
1
∞
0.09/0.07
0
1
∞
2.07/1.21
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Choose.c
StarExec error
0
1
∞
2.72/1.67
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.16_true-termination.c
0
1
∞
0.12/0.21
0
1
∞
3.54/2.40
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaC1.c
2
1
n
2
0.19/0.27
2
1
n
2
2.56/1.41
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-rsd_true-termination.c
2
1
n
2
0.33/0.41
0
1
∞
4.85/3.59
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaB2.c
2
1
n
1
0.13/0.22
2
1
n
1
2.25/1.20
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
BradleyMannaSipma-CAV2005-Fig1-modified_false-termination.c
0
1
∞
0.17/0.25
0
1
∞
2.79/1.78
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
MinusBuiltIn.c
0
1
∞
0.12/0.20
0
1
∞
2.16/1.22
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_a.10.c
2
1
n
1
0.16/0.24
1
1
n
2
2.45/1.34
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Sunset.c
0
1
∞
0.17/0.26
0
1
∞
2.99/1.88
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-loops_true-termination.c
2
1
n
2
0.20/0.28
2
1
n
2
2.61/1.48
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AlternDiv.c
0
1
∞
0.24/0.33
0
1
∞
2.80/1.87
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.17.c
2
1
n
1
0.21/0.30
2
1
n
1
2.35/1.33
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.08_true-termination.c
0
1
∞
0.13/0.22
0
1
∞
4.43/3.35
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaB6.c
2
1
n
1
0.15/0.23
2
1
n
1
2.08/1.21
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-termination.c
0
1
∞
0.13/0.21
0
1
∞
4.28/3.28
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_ex1.c
2
1
n
1
0.12/0.20
2
1
n
1
2.29/1.22
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_24.c
0
1
∞
0.11/0.20
0
1
∞
2.47/1.48
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaC3.c
2
1
n
1
0.17/0.25
2
1
n
1
2.42/1.42
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Masse-VMCAI2014-Fig1b_true-termination.c
0
1
∞
0.14/0.22
0
1
∞
4.24/3.24
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Ex08.c
0
1
∞
0.28/0.37
0
1
∞
4.12/3.11
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.22_true-termination.c
0
1
∞
0.15/0.24
0
1
∞
3.23/2.19
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Et4.c
0
1
∞
0.16/0.24
0
1
∞
4.00/2.99
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination.c
0
1
∞
0.31/0.39
0
1
∞
7.96/6.68
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
WhileTrue.c
0
1
∞
0.09/0.08
0
1
∞
2.10/1.21
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NonTermination2_false-termination.c
0
1
∞
0.14/0.23
0
1
∞
3.15/2.18
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex3.04_true-termination.c
0
1
∞
0.16/0.24
0
1
∞
2.65/1.64
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Velroyen_false-termination.c
0
1
∞
0.19/0.27
0
1
∞
2.98/1.95
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.15.c
2
1
n
1
0.22/0.30
2
1
n
1
2.32/1.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ComplInterv3.c
0
1
∞
0.16/0.24
0
1
∞
2.88/1.76
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PodelskiRybalchenko-LICS2004-Fig1_true-termination.c
2
1
n
2
0.19/0.27
2
1
n
2
2.63/1.47
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
collatz.c
0
1
∞
0.26/0.34
0
1
∞
5.14/3.90
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination.c
2
1
n
2
0.49/0.57
StarExec error
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Waldkirch_true-termination.c
StarExec error
0
1
∞
2.21/1.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
MinusUserDefined.c
2
1
n
1
0.50/0.58
2
1
n
1
4.34/3.35
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-termination.c
0
1
∞
0.13/0.22
0
1
∞
5.65/4.68
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
CookSeeZuleger-TACAS2013-Fig8b_true-termination.c
2
1
n
1
0.16/0.24
2
1
n
1
2.49/1.46
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex3.10_true-termination.c
2
1
n
1
0.16/0.24
2
1
n
1
2.44/1.41
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Narrowing.c
0
1
∞
0.78/0.85
0
1
∞
7.64/5.12
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
WhileFalse_true-termination.c
0
1
∞
0.08/0.09
0
1
∞
2.20/1.34
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.13_true-termination.c
0
1
∞
0.13/0.21
0
1
∞
3.90/2.93
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex3.09_true-termination.c
0
1
∞
0.19/0.29
0
1
∞
4.03/2.80
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination.c
2
1
n
2
0.27/0.36
2
1
n
2
2.67/1.57
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
4NestedWith3Variables_true-termination.c
0
1
∞
0.14/0.22
0
1
∞
297.83/296.06
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination.c
2
1
n
1
0.19/0.30
2
1
n
1
2.47/1.51
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PodelskiRybalchenko-VMCAI2004-Ex1_true-termination.c
2
1
n
1
0.17/2.57
2
1
n
1
3.49/2.30
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
DivMinus2.c
2
1
n
1
0.22/0.30
2
1
n
1
2.71/1.66
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Et1.c
0
1
∞
0.13/2.98
0
1
∞
4.75/3.82
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex1.04_true-termination.c
2
1
n
1
0.14/0.22
2
1
n
1
2.52/1.67
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination.c
2
1
n
2
0.21/0.32
2
1
n
2
2.51/1.49
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
WhilePart.c
0
1
∞
0.14/0.22
0
1
∞
2.44/1.86
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination.c
2
1
n
1
0.14/0.25
2
1
n
1
2.58/1.60
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.09_true-termination.c
0
1
∞
0.17/0.25
0
1
∞
2.65/1.79
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaA9.c
2
1
n
1
0.14/0.23
2
1
n
1
2.61/1.46
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
GCD.c
0
1
∞
0.37/0.53
0
1
∞
4.97/3.93
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
CookSeeZuleger-TACAS2013-Fig8a_true-termination.c
2
1
n
1
0.14/0.22
1
1
n
2
2.25/1.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Swingers.c
0
1
∞
0.12/0.20
0
1
∞
2.54/1.53
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.06.c
2
1
n
1
0.15/0.26
2
1
n
1
2.19/1.38
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-complex_true-termination.c
2
1
n
1
0.76/0.87
2
1
n
1
2.69/1.79
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-terminate_true-termination.c
2
1
n
1
0.17/0.26
2
1
n
1
2.30/1.35
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_00.c
0
1
∞
0.10/0.20
0
1
∞
2.32/1.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination.c
2
1
n
1
0.16/0.27
2
1
n
1
2.81/1.87
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-termination.c
0
1
∞
0.14/0.22
0
1
∞
2.70/1.61
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
MinusMin.c
2
1
n
1
0.18/0.29
2
1
n
1
2.39/1.29
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_10.c
0
1
∞
0.11/0.20
0
1
∞
3.16/2.19
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
IntPath.c
0
1
∞
0.13/0.21
0
1
∞
2.22/1.28
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_a.06.c
2
1
n
1
0.14/0.30
2
1
n
1
2.33/1.45
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_c.02.c
2
1
n
2
0.18/0.26
2
1
n
2
2.29/1.34
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex4.01_true-termination.c
0
1
∞
0.18/0.26
0
1
∞
2.77/1.93
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaB7.c
2
1
n
1
0.16/0.25
2
1
n
1
2.26/1.40
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Avery-FLOPS2006-Table1_true-termination.c
2
1
n
1
0.17/0.25
2
1
n
1
2.26/1.42
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Marbie2.c
0
1
∞
0.09/0.12
0
1
∞
2.09/1.33
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
LogAG.c
2
1
n
1
0.18/0.29
2
1
n
1
2.24/1.41
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Marbie1.c
0
1
∞
0.11/0.23
0
1
∞
2.79/1.72
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Copenhagen_true-termination.c
2
1
n
1
0.14/0.22
2
1
n
1
2.30/1.25
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Parallel_true-termination.c
2
1
n
1
0.18/0.26
2
1
n
1
2.70/1.90
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
WhileIncr.c
0
1
∞
0.11/0.20
0
1
∞
2.89/1.78
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PodelskiRybalchenko-TACAS2011-Fig1_true-termination.c
2
1
n
1
0.12/0.20
2
1
n
1
2.25/1.24
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_ex2.c
0
1
∞
0.31/0.39
0
1
∞
5.42/4.39
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChooseLife.c
0
1
∞
0.13/0.21
0
1
∞
2.70/1.68
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
GCD3.c
2
1
n
1
0.27/0.37
2
1
n
1
3.09/1.90
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Ex05.c
0
1
∞
0.09/0.29
0
1
∞
2.22/1.46
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_04.c
0
1
∞
0.53/0.64
0
1
∞
6.83/5.41
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination.c
2
1
n
1
0.22/0.30
2
1
n
1
2.50/1.70
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_22.c
0
1
∞
0.12/0.25
0
1
∞
2.52/1.63
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex3.03_true-termination.c
0
1
∞
0.13/0.22
0
1
∞
6.83/5.80
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaC10.c
0
1
∞
0.13/0.31
0
1
∞
4.20/3.22
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Thun_true-termination.c
0
1
∞
0.13/0.21
0
1
∞
4.94/3.90
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_true-termination.c
2
1
n
1
0.37/0.44
2
1
n
1
5.72/4.50
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Toulouse-MultiBranchesToLoop_true-termination.c
0
1
∞
0.54/0.61
0
1
∞
4.02/2.71
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
2Nested_true-termination.c
0
1
∞
0.13/0.21
0
1
∞
4.06/3.07
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_true-termination.c
0
1
∞
0.66/0.73
0
1
∞
44.73/42.95
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Log.c
2
1
n
1
0.14/0.23
2
1
n
1
2.40/1.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Sequence.c
0
1
∞
0.15/0.25
0
1
∞
2.35/1.25
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Lobnya-Boolean-Reordered_true-termination.c
2
1
n
1
0.21/0.30
2
1
n
1
2.73/1.76
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaB11.c
2
1
n
1
0.24/0.32
2
1
n
1
2.47/2.72
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.18.c
2
1
n
1
0.23/0.31
2
1
n
1
2.62/1.44
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_03.c
0
1
∞
0.13/0.21
0
1
∞
2.56/1.58
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination.c
2
1
n
2
0.18/0.26
2
1
n
2
2.47/1.60
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
DivWithoutMinus.c
0
1
∞
0.23/0.31
0
1
∞
3.58/2.69
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination.c
2
1
n
1
0.14/0.24
2
1
n
1
2.62/1.83
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Ben-Amram-LMCS2010-Ex2.3_true-termination.c
2
1
n
1
0.36/0.53
0
1
∞
6.98/6.11
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Fig1_true-termination.c
0
1
∞
0.13/0.25
0
1
∞
4.20/3.16
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Ex02.c
0
1
∞
0.16/0.25
0
1
∞
2.73/1.86
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PodelskiRybalchenko-VMCAI2004-Ex2_true-termination.c
0
1
∞
0.12/0.21
0
1
∞
2.72/1.80
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NonTerminationSimple7_false-termination.c
0
1
∞
0.13/0.25
0
1
∞
3.82/2.87
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_c.07.c
2
1
n
1
0.17/0.27
2
1
n
1
2.31/1.44
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
LeikeHeizmann-WST2014-Ex6_false-termination.c
0
1
∞
0.13/0.26
0
1
∞
5.12/4.28
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaA7.c
2
1
n
1
0.17/3.52
2
1
n
1
2.21/1.37
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Benghazi_true-termination.c
2
1
n
1
0.15/0.25
2
1
n
1
2.45/1.58
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-termination.c
0
1
∞
0.13/0.36
0
1
∞
3.67/2.59
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
DoubleNeg.c
0
1
∞
0.12/0.23
0
1
∞
3.14/2.16
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.03-no-inv_assume.c
2
1
n
1
0.14/0.22
2
1
n
1
2.46/1.46
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_java_Sequence.c
0
1
∞
0.15/0.27
0
1
∞
2.22/1.38
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Pure2Phase_true-termination.c
0
1
∞
0.19/0.30
0
1
∞
5.79/4.81
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Loop.c
0
1
∞
0.11/0.24
0
1
∞
2.26/1.44
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
LeikeHeizmann-TACAS2014-Fig1_true-termination.c
0
1
∞
0.13/0.22
0
1
∞
4.24/3.21
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination.c
0
1
∞
0.19/0.28
0
1
∞
5.53/4.65
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.09-no-inv_assume.c
2
1
n
1
0.19/0.34
0
1
∞
3.36/2.38
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination.c
0
1
∞
0.19/0.32
0
1
∞
5.59/4.20
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
gcd1_true-termination.c
2
1
n
1
0.30/0.42
1
1
n
2
2.63/1.73
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.03_assume.c
2
1
n
1
0.14/0.22
2
1
n
1
2.41/1.27
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Masse-VMCAI2014-Ex6_true-termination.c
2
1
n
2
0.20/0.29
1
1
n
3
2.38/1.44
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Urban-WST2013-Fig1_false-termination.c
StarExec error
0
1
∞
2.51/1.47
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
MirrorInterv.c
0
1
∞
0.27/0.42
0
1
∞
3.43/2.41
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.01.c
2
1
n
1
0.13/0.21
2
1
n
1
2.16/1.20
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-ndecr_true-termination.c
2
1
n
1
0.11/0.20
2
1
n
1
2.14/1.17
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Piecewise_true-termination.c
0
1
∞
0.19/0.27
0
1
∞
7.73/6.39
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaB17.c
2
1
n
1
0.21/0.29
2
1
n
1
2.41/1.29
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Cairo_true-termination.c
2
1
n
1
0.12/0.21
2
1
n
1
2.35/1.77
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex1.01_true-termination.c
0
1
∞
0.12/0.20
0
1
∞
2.63/1.61
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_true-termination.c
2
1
n
1
0.39/0.47
2
1
n
1
10.08/8.59
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaB4.c
0
1
∞
0.11/0.20
0
1
∞
2.28/1.22
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
GulwaniJainKoskinen-PLDI2009-Fig1_true-termination.c
2
1
n
1
0.35/0.43
0
1
∞
4.56/3.43
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_a.04.c
2
1
n
1
0.12/0.21
2
1
n
1
2.15/1.18
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Even.c
0
1
∞
0.15/0.23
0
1
∞
2.52/1.49
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NoriSharma-FSE2013-Fig7_true-termination.c
2
1
n
1
0.17/0.25
2
1
n
1
2.28/1.25
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.14.c
2
1
n
1
0.20/0.28
2
1
n
1
2.34/1.35
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
BradleyMannaSipma-ICALP2005-Fig1_true-termination.c
0
1
∞
0.26/0.34
0
1
∞
14.87/13.54
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PlusSwap.c
0
1
∞
0.12/0.21
0
1
∞
3.55/2.44
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination.c
StarExec error
2
1
n
1
2.61/1.58
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Gauss.c
0
1
∞
0.14/0.26
0
1
∞
2.44/1.43
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_ex3a.c
0
1
∞
0.13/0.21
0
1
∞
0.54/0.38
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
WhileSingle.c
0
1
∞
0.16/0.25
0
1
∞
2.68/1.60
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaA8.c
2
1
n
1
0.13/0.21
2
1
n
1
2.34/1.25
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
WhileTrue_false-termination.c
0
1
∞
0.09/0.08
0
1
∞
2.30/1.23
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex1.03_true-termination.c
0
1
∞
0.15/0.23
StarExec error
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Stockholm_true-termination.c
StarExec error
2
1
n
1
2.44/1.41
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
CookSeeZuleger-TACAS2013-Fig7b_true-termination.c
0
1
∞
0.26/0.36
0
1
∞
34.86/33.14
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.10_true-termination.c
StarExec error
StarExec error
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination.c
2
1
n
1
0.12/0.20
2
1
n
1
2.05/1.16
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex3.08_true-termination.c
0
1
∞
0.14/0.23
0
1
∞
4.44/3.39
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaA10.c
2
1
n
1
0.16/0.24
1
1
n
2
2.37/1.30
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Ex01.c
0
1
∞
0.11/0.19
0
1
∞
2.82/1.72
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AlternDivWide.c
0
1
∞
0.33/0.41
0
1
∞
3.08/1.98
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex1.05_true-termination.c
2
1
n
1
0.14/0.22
2
1
n
1
2.51/1.49
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Nested.c
0
1
∞
0.16/0.25
0
1
∞
2.35/1.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
aaron2_true-termination.c
2
1
n
1
0.18/0.27
2
1
n
1
3.18/2.03
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.12.c
2
1
n
1
0.18/0.26
2
1
n
1
2.98/1.89
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ComplInterv.c
0
1
∞
0.14/0.22
0
1
∞
0.50/0.35
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination.c
2
1
n
1
0.19/0.28
2
1
n
1
2.26/1.25
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
GCD2.c
0
1
∞
0.28/0.36
0
1
∞
4.57/3.33
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_c.08.c
2
1
n
2
0.18/0.26
2
1
n
2
2.31/1.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.21_true-termination.c
0
1
∞
0.13/0.21
0
1
∞
3.46/3.26
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-while2_true-termination.c
2
1
n
2
0.17/0.25
2
1
n
2
2.36/1.24
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NonTerminationSimple9_false-termination.c
0
1
∞
0.12/0.20
StarExec error
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Flip2.c
StarExec error
0
1
∞
3.10/2.01
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-termination.c
0
1
∞
0.13/0.21
0
1
∞
4.80/3.73
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination.c
2
1
n
2
0.53/0.61
0
1
∞
11.36/9.92
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Et2.c
0
1
∞
0.13/0.21
0
1
∞
3.39/2.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.18_true-termination.c
0
1
∞
0.13/0.21
0
1
∞
5.14/4.12
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
TrueDiv.c
0
1
∞
0.11/0.19
0
1
∞
2.60/1.53
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-exmini_true-termination.c
StarExec error
2
1
n
1
2.39/1.30
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Cousot.c
0
1
∞
0.13/0.21
0
1
∞
3.48/2.53
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AlternDivWidening.c
0
1
∞
144.44/144.50
0
1
∞
4.35/3.12
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_java_Break.c
0
1
∞
0.11/0.20
0
1
∞
2.08/1.22
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PodelskiRybalchenko-TACAS2011-Fig2_true-termination.c
2
1
n
2
0.19/0.27
2
1
n
2
2.33/1.30
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
TwoFloatInterv.c
0
1
∞
0.23/0.31
0
1
∞
3.73/2.49
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination.c
2
1
n
1
0.13/0.21
2
1
n
1
2.18/1.31
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Gothenburg_true-termination.c
2
1
n
1
0.19/0.27
1
1
n
2
2.74/1.73
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_fermat.c
0
1
∞
0.27/0.34
0
1
∞
0.78/0.44
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.07_true-termination.c
StarExec error
0
1
∞
2.61/1.64
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_true-termination.c
StarExec error
0
1
∞
4.96/3.75
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
GulavaniGulwani-CAV2008-Fig1b_true-termination.c
2
1
n
1
0.20/0.28
2
1
n
1
2.32/1.32
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_ex3b.c
0
1
∞
0.14/0.22
0
1
∞
0.52/0.36
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-Fig2a_true-termination.c
2
1
n
1
0.31/0.39
2
1
n
1
3.54/2.35
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
CookSeeZuleger-TACAS2013-Fig7a_true-termination.c
0
1
∞
0.21/0.29
0
1
∞
14.25/12.77
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_02.c
0
1
∞
0.13/0.22
0
1
∞
2.36/1.37
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
genady_true-termination.c
0
1
∞
0.13/0.21
0
1
∞
2.17/1.37
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination.c
2
1
n
1
0.14/0.22
2
1
n
1
2.50/1.50
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
WhileIncrPart.c
0
1
∞
0.14/0.22
0
1
∞
2.51/1.47
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Pure3Phase_true-termination.c
0
1
∞
0.16/0.24
0
1
∞
5.29/4.22
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.10.c
2
1
n
1
0.19/0.27
2
1
n
1
2.44/1.42
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NO_23.c
0
1
∞
0.12/0.20
0
1
∞
2.33/1.34
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.01_true-termination.c
0
1
∞
0.13/0.21
0
1
∞
4.21/3.13
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PodelskiRybalchenko-TACAS2011-Fig4_true-termination.c
0
1
∞
0.17/0.25
0
1
∞
7.30/6.06
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_easySum.c
2
1
n
1
0.13/0.21
2
1
n
1
2.22/1.19
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_a.01.c
2
1
n
2
0.17/0.26
2
1
n
2
2.26/1.24
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
WhileDecr.c
2
1
n
1
0.12/0.20
2
1
n
1
2.25/1.16
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
LeikeHeizmann-TACAS2014-Ex1_true-termination.c
2
1
n
1
0.15/0.24
2
1
n
1
2.31/3.97
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
NonTerminationSimple2_false-termination.c
0
1
∞
0.11/0.20
0
1
∞
2.62/1.62
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
PastaA6.c
2
1
n
1
0.14/0.22
2
1
n
1
2.38/1.25
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
Urban-WST2013-Fig2_true-termination.c
2
1
n
1
0.15/0.23
2
1
n
1
2.15/1.22
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
svcomp_b.07.c
2
1
n
1
0.17/0.25
2
1
n
1
2.34/1.23
Flores-Montoya_2017/
Adapted_from_Stroeder_15/
ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-termination.c
0
1
∞
0.13/0.21
0
1
∞
4.90/3.87
518
476