alloca/svcomp_Avery-2006FLOPS-Tabel1_true-alloca.c |
91.3 /
81.4 s
|
432.1 /
300.0 s
|
7.9 /
7.4 s
|
loca/svcomp_Ben-Amram-2010LMCS-Ex2.3_true-alloca.c |
11.9 /
4.2 s
|
143.8 /
113.8 s
|
6.0 /
5.8 s
|
nnaSipma-2005CAV-Fig1-modified_false-termination.c |
31.5 /
9.9 s
|
44.9 /
21.3 s
|
6.0 /
5.8 s
|
vcomp_BradleyMannaSipma-2005CAV-Fig1_true-alloca.c |
683.3 /
300.1 s
|
321.4 /
225.3 s
|
6.9 /
6.6 s
|
omp_BradleyMannaSipma-2005ICALP-Fig1_true-alloca.c |
30.4 /
9.8 s
|
67.7 /
34.0 s
|
6.3 /
6.1 s
|
mp_BrockschmidtCookFuhs-2013CAV-Fig1_true-alloca.c |
29.0 /
10.7 s
|
100.7 /
74.5 s
|
1.2 /
1.2 s
|
schmidtCookFuhs-2013CAV-Introduction_true-alloca.c |
9.7 /
3.6 s
|
26.1 /
15.7 s
|
1.5 /
1.4 s
|
mp_ChenFlurMukhopadhyay-2012SAS-Fig1_true-alloca.c |
8.7 /
3.2 s
|
127.4 /
85.6 s
|
1.7 /
1.6 s
|
svcomp_CookSeeZuleger-2013TACAS-Fig3_true-alloca.c |
8.4 /
3.1 s
|
51.9 /
34.6 s
|
6.3 /
6.1 s
|
vcomp_CookSeeZuleger-2013TACAS-Fig7a_true-alloca.c |
15.3 /
5.2 s
|
297.3 /
249.0 s
|
6.7 /
6.4 s
|
vcomp_CookSeeZuleger-2013TACAS-Fig7b_true-alloca.c |
67.4 /
23.1 s
|
266.6 /
217.4 s
|
7.1 /
6.8 s
|
mp_GulwaniJainKoskinen-2009PLDI-Fig1_true-alloca.c |
11.8 /
4.6 s
|
342.7 /
300.0 s
|
6.7 /
6.4 s
|
p_HarrisLalNoriRajamani-2010SAS-Fig1_true-alloca.c |
3.3 /
1.6 s
|
491.0 /
300.1 s
|
8.9 /
8.2 s
|
0SAS-Fig2_false-unreach-label-termination-alloca.c |
122.8 /
55.6 s
|
238.7 /
224.2 s
|
3.0 /
2.6 s
|
p_HarrisLalNoriRajamani-2010SAS-Fig3_true-alloca.c |
11.8 /
4.1 s
|
14.5 /
8.6 s
|
6.6 /
6.4 s
|
aTsitovichWintersteiger-2010CAV-Fig1_true-alloca.c |
304.7 /
300.0 s
|
39.0 /
25.0 s
|
5.9 /
5.7 s
|
riguez-CarbonellRubio-2013FMCAD-Fig1_true-alloca.c |
983.3 /
300.1 s
|
348.5 /
300.0 s
|
1.3 /
1.2 s
|
C/AProVE_memory_alloca/svcomp_Masse_true-alloca.c |
52.7 /
24.4 s
|
18.4 /
8.6 s
|
6.1 /
6.0 s
|
lloca/svcomp_NoriSharma-2013FSE-Fig7_true-alloca.c |
230.1 /
217.4 s
|
305.1 /
300.0 s
|
6.6 /
6.3 s
|
lloca/svcomp_NoriSharma-2013FSE-Fig8_true-alloca.c |
80.2 /
65.6 s
|
315.4 /
300.0 s
|
2.5 /
2.2 s
|
mp_PodelskiRybalchenko-2004VMCAI-Ex2_true-alloca.c |
115.6 /
40.0 s
|
17.8 /
8.6 s
|
1.4 /
1.3 s
|
y_alloca/svcomp_TelAviv-Amir-Minimum_true-alloca.c |
968.3 /
300.0 s
|
350.6 /
300.0 s
|
6.8 /
6.5 s
|
lloca/svcomp_Toulouse-BranchesToLoop_true-alloca.c |
7.1 /
2.7 s
|
500.3 /
300.0 s
|
1.8 /
1.7 s
|
/svcomp_Toulouse-MultiBranchesToLoop_true-alloca.c |
8.8 /
3.5 s
|
313.5 /
284.7 s
|
6.0 /
5.8 s
|
3WST-Fig1_false-unreach-label-termination-alloca.c |
3.4 /
1.6 s
|
15.3 /
7.7 s
|
5.7 /
5.6 s
|
comp_Urban-2013WST-Fig2-modified1000_true-alloca.c |
8.1 /
3.0 s
|
323.6 /
300.0 s
|
1.2 /
1.1 s
|
ory_alloca/svcomp_Urban-2013WST-Fig2_true-alloca.c |
5.8 /
2.2 s
|
325.8 /
300.0 s
|
1.2 /
1.1 s
|
C/AProVE_memory_alloca/svcomp_Urban_true-alloca.c |
36.2 /
11.9 s
|
153.5 /
117.2 s
|
6.6 /
6.4 s
|
_Velroyen_false-unreach-label-termination-alloca.c |
10.1 /
3.4 s
|
24.8 /
11.9 s
|
5.9 /
5.8 s
|
C/AProVE_memory_alloca/svcomp_a.01-alloca.c |
58.2 /
44.8 s
|
173.8 /
147.2 s
|
1.3 /
1.3 s
|
C/AProVE_memory_alloca/svcomp_a.04-alloca.c |
19.7 /
12.0 s
|
52.7 /
33.5 s
|
2.0 /
1.8 s
|
C/AProVE_memory_alloca/svcomp_a.05-alloca.c |
21.3 /
13.5 s
|
55.4 /
34.1 s
|
6.2 /
6.0 s
|
C/AProVE_memory_alloca/svcomp_a.06-alloca.c |
52.7 /
43.3 s
|
399.6 /
296.2 s
|
6.5 /
6.2 s
|
C/AProVE_memory_alloca/svcomp_a.07-alloca.c |
102.6 /
92.3 s
|
415.4 /
300.0 s
|
6.5 /
6.2 s
|
C/AProVE_memory_alloca/svcomp_a.08-alloca.c |
26.3 /
18.2 s
|
78.4 /
55.1 s
|
6.1 /
5.9 s
|
C/AProVE_memory_alloca/svcomp_a.09_assume-alloca.c |
7.7 /
2.9 s
|
57.7 /
36.0 s
|
6.4 /
6.1 s
|
C/AProVE_memory_alloca/svcomp_a.10-alloca.c |
30.8 /
20.8 s
|
174.7 /
130.8 s
|
6.3 /
6.1 s
|
C/AProVE_memory_alloca/svcomp_add_last_alloca.c |
1.5 /
0.9 s
|
318.6 /
300.0 s
|
6.0 /
5.8 s
|
C/AProVE_memory_alloca/svcomp_array01_alloca.c |
24.6 /
10.7 s
|
22.2 /
12.6 s
|
6.7 /
6.4 s
|
C/AProVE_memory_alloca/svcomp_array02_alloca.c |
72.9 /
42.7 s
|
40.2 /
26.7 s
|
8.4 /
7.8 s
|
C/AProVE_memory_alloca/svcomp_array03_alloca.c |
78.2 /
47.9 s
|
4.7 /
3.7 s
|
6.5 /
6.3 s
|
C/AProVE_memory_alloca/svcomp_aviad_true-alloca.c |
19.6 /
9.7 s
|
353.2 /
300.0 s
|
6.2 /
6.0 s
|
C/AProVE_memory_alloca/svcomp_b.01-alloca.c |
21.0 /
13.2 s
|
71.5 /
50.1 s
|
6.2 /
6.0 s
|
C/AProVE_memory_alloca/svcomp_b.02-alloca.c |
54.8 /
44.0 s
|
74.1 /
52.4 s
|
2.0 /
1.8 s
|
E_memory_alloca/svcomp_b.03-no-inv_assume-alloca.c |
5.7 /
2.3 s
|
26.2 /
15.4 s
|
6.1 /
5.9 s
|
C/AProVE_memory_alloca/svcomp_b.03_assume-alloca.c |
5.7 /
2.3 s
|
24.8 /
14.3 s
|
6.0 /
5.9 s
|
C/AProVE_memory_alloca/svcomp_b.04-alloca.c |
2.7 /
1.3 s
|
74.3 /
47.0 s
|
6.3 /
6.1 s
|
C/AProVE_memory_alloca/svcomp_b.05-alloca.c |
7.2 /
2.8 s
|
15.8 /
10.7 s
|
6.0 /
5.8 s
|
C/AProVE_memory_alloca/svcomp_b.06-alloca.c |
30.2 /
21.7 s
|
57.8 /
36.3 s
|
6.2 /
6.0 s
|
C/AProVE_memory_alloca/svcomp_b.07-alloca.c |
112.0 /
99.9 s
|
463.6 /
300.0 s
|
2.3 /
2.1 s
|
E_memory_alloca/svcomp_b.09-no-inv_assume-alloca.c |
19.5 /
11.8 s
|
155.5 /
118.0 s
|
6.3 /
6.1 s
|
C/AProVE_memory_alloca/svcomp_b.09_assume-alloca.c |
21.7 /
12.8 s
|
200.4 /
152.4 s
|
6.3 /
6.1 s
|
C/AProVE_memory_alloca/svcomp_b.10-alloca.c |
47.1 /
29.6 s
|
78.7 /
53.8 s
|
6.4 /
6.1 s
|
C/AProVE_memory_alloca/svcomp_b.11-alloca.c |
61.6 /
47.4 s
|
185.2 /
149.5 s
|
6.3 /
6.1 s
|
C/AProVE_memory_alloca/svcomp_b.12-alloca.c |
25.2 /
13.6 s
|
326.8 /
300.0 s
|
6.3 /
6.1 s
|
C/AProVE_memory_alloca/svcomp_b.13-alloca.c |
76.4 /
62.2 s
|
395.4 /
300.0 s
|
2.4 /
2.2 s
|
C/AProVE_memory_alloca/svcomp_b.14-alloca.c |
16.0 /
9.6 s
|
63.9 /
44.6 s
|
6.2 /
6.0 s
|
C/AProVE_memory_alloca/svcomp_b.15-alloca.c |
32.1 /
25.3 s
|
389.1 /
300.0 s
|
6.5 /
6.2 s
|
C/AProVE_memory_alloca/svcomp_b.16-alloca.c |
30.6 /
14.5 s
|
76.7 /
51.5 s
|
1.4 /
1.3 s
|
C/AProVE_memory_alloca/svcomp_b.17-alloca.c |
73.6 /
58.9 s
|
387.5 /
300.0 s
|
1.5 /
1.4 s
|
C/AProVE_memory_alloca/svcomp_b.18-alloca.c |
7.5 /
2.8 s
|
61.2 /
46.9 s
|
2.6 /
2.3 s
|
C/AProVE_memory_alloca/svcomp_bubblesort_alloca.c |
101.7 /
68.0 s
|
23.2 /
13.3 s
|
0.8 /
0.8 s
|
C/AProVE_memory_alloca/svcomp_c.01-no-inv-alloca.c |
26.8 /
10.9 s
|
59.1 /
36.9 s
|
1.3 /
1.3 s
|
C/AProVE_memory_alloca/svcomp_c.01_assume-alloca.c |
15.7 /
5.5 s
|
51.6 /
36.1 s
|
1.3 /
1.2 s
|
C/AProVE_memory_alloca/svcomp_c.02-alloca.c |
33.5 /
15.5 s
|
333.3 /
300.0 s
|
1.4 /
1.3 s
|
C/AProVE_memory_alloca/svcomp_c.03-alloca.c |
97.3 /
80.4 s
|
393.3 /
300.0 s
|
6.6 /
6.3 s
|
C/AProVE_memory_alloca/svcomp_c.07-alloca.c |
86.7 /
76.9 s
|
446.0 /
300.0 s
|
2.7 /
2.4 s
|
C/AProVE_memory_alloca/svcomp_c.08-alloca.c |
101.9 /
88.2 s
|
333.2 /
300.0 s
|
1.3 /
1.3 s
|
C/AProVE_memory_alloca/svcomp_count_down_alloca.c |
66.5 /
28.2 s
|
25.9 /
16.0 s
|
6.9 /
6.6 s
|
C/AProVE_memory_alloca/svcomp_cstrcat_alloca.c |
6.3 /
2.6 s
|
189.0 /
184.5 s
|
9.1 /
8.4 s
|
/AProVE_memory_alloca/svcomp_cstrchr_true_alloca.c |
8.9 /
3.4 s
|
30.1 /
15.1 s
|
6.2 /
6.0 s
|
/AProVE_memory_alloca/svcomp_cstrcmp_true_alloca.c |
14.2 /
5.7 s
|
99.0 /
85.1 s
|
0.3 /
0.3 s
|
C/AProVE_memory_alloca/svcomp_cstrcpy_alloca.c |
12.7 /
5.8 s
|
305.2 /
300.0 s
|
7.4 /
6.9 s
|
AProVE_memory_alloca/svcomp_cstrcspn_true_alloca.c |
49.0 /
23.5 s
|
24.5 /
21.2 s
|
3.0 /
2.7 s
|
/AProVE_memory_alloca/svcomp_cstrlen_true_alloca.c |
6.7 /
2.6 s
|
23.5 /
11.6 s
|
6.2 /
6.0 s
|
C/AProVE_memory_alloca/svcomp_cstrncat_alloca.c |
6.5 /
2.7 s
|
45.4 /
41.4 s
|
8.2 /
7.7 s
|
AProVE_memory_alloca/svcomp_cstrncmp_true_alloca.c |
19.4 /
7.7 s
|
92.9 /
80.1 s
|
0.3 /
0.3 s
|
C/AProVE_memory_alloca/svcomp_cstrncpy_alloca.c |
30.4 /
14.1 s
|
306.3 /
300.0 s
|
11.9 /
10.7 s
|
AProVE_memory_alloca/svcomp_cstrpbrk_true_alloca.c |
29.6 /
13.8 s
|
25.5 /
22.1 s
|
3.0 /
2.7 s
|
/AProVE_memory_alloca/svcomp_cstrspn_true_alloca.c |
33.6 /
16.5 s
|
34.6 /
31.2 s
|
3.0 /
2.7 s
|
C/AProVE_memory_alloca/svcomp_diff_alloca.c |
315.8 /
300.0 s
|
321.7 /
300.0 s
|
5.3 /
5.3 s
|
C/AProVE_memory_alloca/svcomp_easySum-alloca.c |
49.3 /
42.9 s
|
54.9 /
35.3 s
|
6.0 /
5.9 s
|
C/AProVE_memory_alloca/svcomp_ex1-alloca.c |
5.5 /
2.3 s
|
5.0 /
3.7 s
|
6.4 /
6.2 s
|
C/AProVE_memory_alloca/svcomp_ex2-alloca.c |
40.1 /
26.4 s
|
5.2 /
4.0 s
|
3.1 /
2.7 s
|
C/AProVE_memory_alloca/svcomp_ex3a-alloca.c |
7.9 /
3.0 s
|
4.9 /
3.8 s
|
5.9 /
5.8 s
|
C/AProVE_memory_alloca/svcomp_ex3b-alloca.c |
17.5 /
7.0 s
|
5.0 /
3.8 s
|
2.0 /
1.9 s
|
C/AProVE_memory_alloca/svcomp_fermat-alloca.c |
122.3 /
73.8 s
|
5.0 /
4.0 s
|
6.2 /
6.0 s
|
C/AProVE_memory_alloca/svcomp_flag-alloca.c |
22.0 /
14.8 s
|
422.3 /
300.0 s
|
6.4 /
6.2 s
|
C/AProVE_memory_alloca/svcomp_gcd1_true-alloca.c |
29.9 /
11.5 s
|
116.7 /
86.5 s
|
1.4 /
1.3 s
|
C/AProVE_memory_alloca/svcomp_genady_true-alloca.c |
22.4 /
12.0 s
|
27.0 /
16.0 s
|
5.7 /
5.6 s
|
AProVE_memory_alloca/svcomp_insertionsort_alloca.c |
56.8 /
38.4 s
|
157.2 /
132.3 s
|
5.0 /
5.0 s
|
C/AProVE_memory_alloca/svcomp_java_AG313-alloca.c |
13.2 /
5.7 s
|
84.9 /
58.0 s
|
6.2 /
6.0 s
|
C/AProVE_memory_alloca/svcomp_java_Break-alloca.c |
6.9 /
2.7 s
|
30.3 /
15.9 s
|
1.6 /
1.5 s
|
roVE_memory_alloca/svcomp_java_BubbleSort_alloca.c |
48.9 /
37.5 s
|
35.4 /
22.9 s
|
0.8 /
0.8 s
|
ProVE_memory_alloca/svcomp_java_Continue1-alloca.c |
12.9 /
4.6 s
|
317.9 /
300.0 s
|
1.7 /
1.6 s
|
roVE_memory_alloca/svcomp_java_LogBuiltIn-alloca.c |
8.3 /
3.1 s
|
30.6 /
17.6 s
|
1.7 /
1.6 s
|
C/AProVE_memory_alloca/svcomp_java_Nested-alloca.c |
18.3 /
7.9 s
|
73.3 /
68.0 s
|
1.3 /
1.2 s
|
AProVE_memory_alloca/svcomp_java_Sequence-alloca.c |
12.4 /
4.5 s
|
331.8 /
300.0 s
|
6.9 /
6.6 s
|
C/AProVE_memory_alloca/svcomp_lis_alloca.c |
314.0 /
300.0 s
|
198.2 /
177.1 s
|
1.0 /
0.9 s
|
C/AProVE_memory_alloca/svcomp_min_rf_true-alloca.c |
57.6 /
31.4 s
|
345.9 /
300.0 s
|
6.7 /
6.4 s
|
C/AProVE_memory_alloca/svcomp_mult_array_alloca.c |
55.8 /
36.4 s
|
4.4 /
3.7 s
|
7.2 /
6.8 s
|
ProVE_memory_alloca/svcomp_openbsd_cbzero_alloca.c |
0.8 /
0.5 s
|
312.8 /
300.0 s
|
0.2 /
0.3 s
|
roVE_memory_alloca/svcomp_openbsd_cmemchr_alloca.c |
0.8 /
0.5 s
|
319.8 /
300.0 s
|
0.2 /
0.3 s
|
oVE_memory_alloca/svcomp_openbsd_cmemrchr_alloca.c |
0.8 /
0.5 s
|
21.1 /
11.0 s
|
0.2 /
0.3 s
|
roVE_memory_alloca/svcomp_openbsd_cmemset_alloca.c |
0.8 /
0.5 s
|
319.6 /
300.0 s
|
0.2 /
0.3 s
|
roVE_memory_alloca/svcomp_openbsd_cstpcpy_alloca.c |
12.9 /
5.1 s
|
304.8 /
300.0 s
|
7.8 /
7.3 s
|
oVE_memory_alloca/svcomp_openbsd_cstpncpy_alloca.c |
0.8 /
0.5 s
|
306.6 /
300.0 s
|
0.2 /
0.3 s
|
roVE_memory_alloca/svcomp_openbsd_cstrcat_alloca.c |
6.2 /
2.5 s
|
46.7 /
43.2 s
|
9.1 /
8.4 s
|
roVE_memory_alloca/svcomp_openbsd_cstrcmp_alloca.c |
12.7 /
4.8 s
|
47.3 /
43.4 s
|
7.0 /
6.7 s
|
roVE_memory_alloca/svcomp_openbsd_cstrcpy_alloca.c |
12.7 /
5.0 s
|
304.7 /
300.0 s
|
8.1 /
7.5 s
|
oVE_memory_alloca/svcomp_openbsd_cstrcspn_alloca.c |
0.8 /
0.5 s
|
304.9 /
300.0 s
|
0.2 /
0.3 s
|
oVE_memory_alloca/svcomp_openbsd_cstrlcpy_alloca.c |
0.8 /
0.5 s
|
305.7 /
300.0 s
|
0.2 /
0.3 s
|
roVE_memory_alloca/svcomp_openbsd_cstrlen_alloca.c |
0.8 /
0.5 s
|
21.8 /
10.8 s
|
0.2 /
0.3 s
|
oVE_memory_alloca/svcomp_openbsd_cstrncat_alloca.c |
0.8 /
0.5 s
|
21.3 /
17.6 s
|
0.2 /
0.3 s
|
oVE_memory_alloca/svcomp_openbsd_cstrncmp_alloca.c |
0.8 /
0.5 s
|
21.4 /
18.1 s
|
0.2 /
0.3 s
|
oVE_memory_alloca/svcomp_openbsd_cstrncpy_alloca.c |
0.8 /
0.5 s
|
306.4 /
300.0 s
|
0.2 /
0.3 s
|
oVE_memory_alloca/svcomp_openbsd_cstrnlen_alloca.c |
0.8 /
0.5 s
|
4.3 /
3.2 s
|
0.2 /
0.3 s
|
oVE_memory_alloca/svcomp_openbsd_cstrpbrk_alloca.c |
0.8 /
0.5 s
|
216.4 /
180.0 s
|
3.3 /
2.9 s
|
roVE_memory_alloca/svcomp_openbsd_cstrspn_alloca.c |
0.8 /
0.5 s
|
28.6 /
24.8 s
|
0.2 /
0.3 s
|
roVE_memory_alloca/svcomp_openbsd_cstrstr_alloca.c |
0.8 /
0.5 s
|
57.5 /
53.5 s
|
0.2 /
0.3 s
|
AProVE_memory_alloca/svcomp_selectionsort_alloca.c |
51.1 /
35.8 s
|
32.0 /
19.9 s
|
1.8 /
1.6 s
|
C/AProVE_memory_alloca/svcomp_stroeder1_alloca.c |
13.6 /
6.6 s
|
14.3 /
8.3 s
|
6.2 /
6.0 s
|
C/AProVE_memory_alloca/svcomp_stroeder2_alloca.c |
26.6 /
12.1 s
|
24.5 /
13.7 s
|
2.5 /
2.3 s
|
C/AProVE_memory_alloca/svcomp_strreplace_alloca.c |
22.8 /
9.4 s
|
304.8 /
300.0 s
|
6.9 /
6.5 s
|
C/AProVE_memory_alloca/svcomp_subseq_alloca.c |
18.9 /
7.6 s
|
83.8 /
80.4 s
|
7.2 /
6.8 s
|
C/AProVE_memory_alloca/svcomp_substring_alloca.c |
27.7 /
11.9 s
|
23.0 /
19.7 s
|
3.1 /
2.7 s
|
C/AProVE_memory_alloca/svcomp_twisted-alloca.c |
3.1 /
1.4 s
|
395.9 /
300.0 s
|
7.9 /
7.5 s
|
C/AProVE_memory_unsafe/svcomp_add_last_unsafe.c |
1.3 /
0.8 s
|
5.4 /
4.0 s
|
6.0 /
5.8 s
|
C/AProVE_memory_unsafe/svcomp_bubble_sort_unsafe.c |
1.6 /
0.9 s
|
5.2 /
4.1 s
|
0.8 /
0.8 s
|
C/AProVE_memory_unsafe/svcomp_bubblesort_unsafe.c |
1.8 /
1.1 s
|
5.1 /
4.0 s
|
4.8 /
4.9 s
|
C/AProVE_memory_unsafe/svcomp_count_down_unsafe.c |
1.7 /
1.0 s
|
5.5 /
4.2 s
|
6.9 /
6.6 s
|
C/AProVE_memory_unsafe/svcomp_cstrcat_unsafe.c |
1.2 /
0.7 s
|
5.0 /
4.0 s
|
7.4 /
7.1 s
|
C/AProVE_memory_unsafe/svcomp_cstrchr_unsafe.c |
1.6 /
0.9 s
|
9.1 /
6.6 s
|
6.2 /
6.0 s
|
C/AProVE_memory_unsafe/svcomp_cstrcpy_unsafe.c |
1.2 /
0.8 s
|
5.1 /
3.9 s
|
6.7 /
6.4 s
|
C/AProVE_memory_unsafe/svcomp_cstrlen_unsafe.c |
1.2 /
0.8 s
|
6.8 /
4.8 s
|
6.1 /
5.9 s
|
C/AProVE_memory_unsafe/svcomp_cstrncat_unsafe.c |
1.3 /
0.8 s
|
5.2 /
4.0 s
|
8.1 /
7.6 s
|
C/AProVE_memory_unsafe/svcomp_cstrncpy_unsafe.c |
2.2 /
1.2 s
|
5.3 /
4.1 s
|
11.1 /
10.0 s
|
C/AProVE_memory_unsafe/svcomp_cstrpbrk_unsafe.c |
1.4 /
0.9 s
|
59.9 /
57.1 s
|
2.6 /
2.4 s
|
AProVE_memory_unsafe/svcomp_delete_alloca_unsafe.c |
1.2 /
0.8 s
|
5.0 /
3.9 s
|
5.9 /
5.8 s
|
C/AProVE_memory_unsafe/svcomp_delete_unsafe.c |
1.2 /
0.7 s
|
5.1 /
4.0 s
|
5.8 /
5.7 s
|
C/AProVE_memory_unsafe/svcomp_diff_usafe.c |
2.5 /
1.2 s
|
5.2 /
4.0 s
|
5.4 /
5.3 s
|
ProVE_memory_unsafe/svcomp_insertion_sort_unsafe.c |
1.4 /
0.9 s
|
5.0 /
4.0 s
|
0.8 /
0.8 s
|
AProVE_memory_unsafe/svcomp_insertionsort_unsafe.c |
1.4 /
0.9 s
|
5.1 /
3.9 s
|
0.8 /
0.8 s
|
roVE_memory_unsafe/svcomp_java_BubbleSort_unsafe.c |
1.7 /
1.0 s
|
5.0 /
4.0 s
|
0.8 /
0.8 s
|
roVE_memory_unsafe/svcomp_knapsack_alloca_unsafe.c |
4.5 /
2.1 s
|
5.7 /
4.3 s
|
0.9 /
0.9 s
|
C/AProVE_memory_unsafe/svcomp_knapsack_unsafe.c |
2.4 /
1.2 s
|
5.5 /
4.2 s
|
0.9 /
0.9 s
|
C/AProVE_memory_unsafe/svcomp_lis_unsafe.c |
2.2 /
1.2 s
|
8.3 /
5.8 s
|
5.1 /
5.1 s
|
C/AProVE_memory_unsafe/svcomp_mult_array_unsafe.c |
2.5 /
1.3 s
|
4.4 /
3.7 s
|
7.2 /
6.8 s
|
memory_unsafe/svcomp_reverse_array_alloca_unsafe.c |
3.0 /
1.4 s
|
7.6 /
5.4 s
|
2.5 /
2.3 s
|
AProVE_memory_unsafe/svcomp_reverse_array_unsafe.c |
2.0 /
1.1 s
|
5.6 /
4.1 s
|
6.7 /
6.4 s
|
ProVE_memory_unsafe/svcomp_selection_sort_unsafe.c |
1.5 /
1.0 s
|
5.3 /
4.3 s
|
1.5 /
1.4 s
|
AProVE_memory_unsafe/svcomp_selectionsort_unsafe.c |
1.7 /
1.0 s
|
5.3 /
4.2 s
|
1.5 /
1.4 s
|
C/AProVE_memory_unsafe/svcomp_stroeder1_unsafe.c |
1.3 /
0.8 s
|
5.1 /
3.8 s
|
6.0 /
5.9 s
|
C/AProVE_memory_unsafe/svcomp_stroeder2_unsafe.c |
1.3 /
0.8 s
|
5.0 /
4.0 s
|
6.5 /
6.2 s
|
C/AProVE_numeric/Avg_true.c |
8.2 /
3.0 s
|
15.3 /
10.2 s
|
6.9 /
6.6 s
|
C/AProVE_numeric/Binomial_true.c |
201.4 /
101.0 s
|
4.4 /
3.5 s
|
0.9 /
0.9 s
|
C/AProVE_numeric/Et1_true.c |
8.3 /
3.3 s
|
7.3 /
5.3 s
|
5.3 /
5.3 s
|
C/AProVE_numeric/Et2_true.c |
15.0 /
5.5 s
|
8.2 /
6.2 s
|
6.9 /
6.6 s
|
C/AProVE_numeric/Et3_true.c |
20.6 /
6.4 s
|
7.4 /
5.3 s
|
5.3 /
5.3 s
|
C/AProVE_numeric/Et4_true.c |
24.7 /
8.2 s
|
23.1 /
14.4 s
|
7.4 /
7.1 s
|
C/AProVE_numeric/LeUserDefRec_true.c |
4.1 /
1.8 s
|
6.1 /
4.8 s
|
0.3 /
0.3 s
|
C/AProVE_numeric/LogRecursive_true.c |
31.4 /
8.9 s
|
5.1 /
4.0 s
|
6.3 /
6.1 s
|
C/AProVE_numeric/Parts_true.c |
41.8 /
21.5 s
|
383.0 /
300.0 s
|
0.9 /
0.9 s
|
C/AProVE_numeric/TerminatorRec02_true.c |
4.2 /
1.7 s
|
4.4 /
3.6 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/TwoWay_true.c |
3.6 /
1.6 s
|
4.4 /
3.7 s
|
5.3 /
5.2 s
|
C/AProVE_numeric/ex2.c |
3.4 /
1.5 s
|
6.6 /
4.8 s
|
6.3 /
6.1 s
|
C/AProVE_numeric/ex3.c |
2.9 /
1.4 s
|
13.3 /
8.2 s
|
21.9 /
18.8 s
|
C/AProVE_numeric/rec_counter1.c |
6.7 /
2.6 s
|
9.6 /
6.5 s
|
6.0 /
5.9 s
|
C/AProVE_numeric/rec_counter3.c |
6.4 /
2.5 s
|
335.8 /
300.0 s
|
6.8 /
6.6 s
|
C/AProVE_numeric/rec_strlen.c |
4.0 /
1.7 s
|
21.6 /
11.0 s
|
6.1 /
5.9 s
|
_Ackermann01_true-unreach-call_modified_modified.c |
6.6 /
2.6 s
|
453.0 /
300.0 s
|
380.8 /
300.0 s
|
on01_true-unreach-call_true-termination_modified.c |
3.3 /
1.5 s
|
8.7 /
5.7 s
|
1.2 /
1.2 s
|
dd01_true-unreach-call_true-termination_modified.c |
4.2 /
1.8 s
|
21.1 /
10.7 s
|
6.0 /
5.9 s
|
ic/svcomp_Fibonacci01_true-unreach-call_modified.c |
4.6 /
1.9 s
|
881.5 /
300.0 s
|
0.8 /
0.8 s
|
tive_true-unreach-call_true-termination_modified.c |
4.0 /
1.7 s
|
10.4 /
6.7 s
|
5.7 /
5.6 s
|
C/AProVE_numeric/svcomp_a.01.c |
27.5 /
13.9 s
|
8.5 /
5.8 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_a.04.c |
10.6 /
4.7 s
|
5.5 /
4.4 s
|
0.7 /
0.7 s
|
C/AProVE_numeric/svcomp_a.05.c |
10.9 /
5.4 s
|
5.5 /
4.4 s
|
0.7 /
0.7 s
|
C/AProVE_numeric/svcomp_a.06.c |
18.3 /
12.3 s
|
5.8 /
4.5 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_a.07.c |
29.3 /
18.8 s
|
5.7 /
4.5 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_a.08.c |
13.6 /
6.7 s
|
5.7 /
4.4 s
|
0.7 /
0.7 s
|
C/AProVE_numeric/svcomp_a.09_assume.c |
5.1 /
2.1 s
|
5.6 /
4.4 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_a.10.c |
14.0 /
6.9 s
|
10.2 /
6.2 s
|
16.2 /
13.7 s
|
C/AProVE_numeric/svcomp_b.01.c |
11.9 /
5.4 s
|
5.5 /
4.5 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_b.02.c |
19.6 /
11.9 s
|
5.7 /
4.6 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_b.03-no-inv_assume.c |
4.3 /
1.8 s
|
6.0 /
4.7 s
|
0.7 /
0.7 s
|
C/AProVE_numeric/svcomp_b.03_assume.c |
4.2 /
1.7 s
|
5.7 /
4.5 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_b.04.c |
1.4 /
0.9 s
|
5.5 /
4.5 s
|
0.7 /
0.7 s
|
C/AProVE_numeric/svcomp_b.05.c |
1.8 /
1.0 s
|
5.9 /
4.7 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_b.06.c |
15.7 /
8.0 s
|
5.6 /
4.5 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_b.07.c |
28.6 /
20.9 s
|
5.8 /
4.5 s
|
0.7 /
0.7 s
|
C/AProVE_numeric/svcomp_b.09-no-inv_assume.c |
14.6 /
6.1 s
|
14.2 /
8.0 s
|
6.4 /
6.2 s
|
C/AProVE_numeric/svcomp_b.09_assume.c |
14.4 /
6.3 s
|
8.6 /
5.5 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_b.10.c |
20.0 /
10.4 s
|
7.3 /
5.2 s
|
0.8 /
0.9 s
|
C/AProVE_numeric/svcomp_b.11.c |
29.8 /
17.2 s
|
9.0 /
6.0 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_b.12.c |
14.9 /
6.0 s
|
7.1 /
5.3 s
|
4.9 /
4.9 s
|
C/AProVE_numeric/svcomp_b.13.c |
19.1 /
11.8 s
|
10.7 /
7.5 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_b.14.c |
11.7 /
4.6 s
|
6.1 /
4.9 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_b.15.c |
12.2 /
6.7 s
|
7.5 /
5.4 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_b.16.c |
13.9 /
5.8 s
|
6.3 /
4.9 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_b.17.c |
25.4 /
14.7 s
|
8.5 /
5.8 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_b.18.c |
8.2 /
2.9 s
|
7.1 /
5.2 s
|
0.8 /
0.9 s
|
C/AProVE_numeric/svcomp_c.01-no-inv.c |
17.2 /
6.0 s
|
13.7 /
6.6 s
|
1.1 /
1.1 s
|
C/AProVE_numeric/svcomp_c.01_assume.c |
12.2 /
4.2 s
|
7.8 /
5.5 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_c.02.c |
15.9 /
5.6 s
|
8.4 /
5.5 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_c.03.c |
31.7 /
17.0 s
|
7.5 /
5.4 s
|
5.4 /
5.4 s
|
C/AProVE_numeric/svcomp_c.07.c |
23.0 /
15.3 s
|
6.6 /
4.8 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_c.08.c |
33.1 /
21.4 s
|
7.8 /
5.5 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_easySum.c |
17.2 /
7.8 s
|
5.6 /
4.6 s
|
0.7 /
0.7 s
|
C/AProVE_numeric/svcomp_ex1.c |
4.1 /
1.7 s
|
4.5 /
3.8 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_ex2.c |
16.3 /
8.0 s
|
4.4 /
3.7 s
|
8.5 /
7.9 s
|
C/AProVE_numeric/svcomp_ex3a.c |
21.9 /
6.4 s
|
4.4 /
3.7 s
|
5.9 /
5.8 s
|
C/AProVE_numeric/svcomp_ex3b.c |
11.1 /
4.0 s
|
4.5 /
3.5 s
|
6.1 /
5.9 s
|
C/AProVE_numeric/svcomp_fermat.c |
111.1 /
52.6 s
|
4.4 /
3.7 s
|
425.6 /
300.0 s
|
C/AProVE_numeric/svcomp_flag.c |
10.5 /
5.3 s
|
25.6 /
12.8 s
|
0.2 /
0.3 s
|
cd01_true-unreach-call_true-termination_modified.c |
5.1 /
2.1 s
|
12.9 /
7.2 s
|
0.8 /
0.8 s
|
C/AProVE_numeric/svcomp_java_AG313.c |
9.3 /
3.6 s
|
5.6 /
4.4 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_java_Break.c |
4.9 /
2.0 s
|
5.5 /
4.3 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_java_Continue1.c |
9.4 /
3.4 s
|
5.7 /
4.4 s
|
0.7 /
0.8 s
|
C/AProVE_numeric/svcomp_java_LogBuiltIn.c |
6.3 /
2.4 s
|
6.6 /
4.7 s
|
1.5 /
1.4 s
|
C/AProVE_numeric/svcomp_java_Nested.c |
16.1 /
6.3 s
|
9.3 /
6.5 s
|
5.8 /
5.7 s
|
C/AProVE_numeric/svcomp_java_Sequence.c |
8.4 /
3.2 s
|
6.0 /
4.7 s
|
0.7 /
0.8 s
|
oi02_true-unreach-call_true-termination_modified.c |
3.5 /
1.5 s
|
6.9 /
4.9 s
|
5.5 /
5.5 s
|
C/AProVE_numeric/svcomp_twisted.c |
41.8 /
21.4 s
|
13.4 /
6.6 s
|
0.9 /
0.9 s
|
teFeautrierGonnord-SAS2010-Fig1_true-termination.c |
32.5 /
11.5 s
|
15.9 /
9.3 s
|
0.9 /
0.9 s
|
eFeautrierGonnord-SAS2010-Fig2a_true-termination.c |
51.6 /
19.9 s
|
10.0 /
6.8 s
|
0.8 /
0.8 s
|
eFeautrierGonnord-SAS2010-Fig2b_true-termination.c |
323.8 /
300.0 s
|
315.8 /
300.0 s
|
331.6 /
162.9 s
|
FeautrierGonnord-SAS2010-aaron2_true-termination.c |
20.1 /
8.7 s
|
6.1 /
4.8 s
|
4.9 /
4.9 s
|
FeautrierGonnord-SAS2010-aaron3_true-termination.c |
711.6 /
300.0 s
|
11.7 /
7.8 s
|
7.6 /
6.7 s
|
eautrierGonnord-SAS2010-complex_true-termination.c |
68.1 /
28.8 s
|
15.9 /
10.8 s
|
0.9 /
0.9 s
|
rierGonnord-SAS2010-counterex1a_true-termination.c |
22.6 /
7.9 s
|
20.3 /
9.4 s
|
65.7 /
55.3 s
|
rierGonnord-SAS2010-counterex1b_true-termination.c |
103.1 /
36.4 s
|
17.5 /
9.7 s
|
5.1 /
5.1 s
|
eautrierGonnord-SAS2010-cousot9_true-termination.c |
6.5 /
2.5 s
|
8.6 /
6.2 s
|
0.7 /
0.8 s
|
eFeautrierGonnord-SAS2010-easy1_true-termination.c |
7.5 /
2.8 s
|
6.6 /
4.8 s
|
0.7 /
0.8 s
|
eFeautrierGonnord-SAS2010-easy2_true-termination.c |
6.2 /
2.4 s
|
5.5 /
4.4 s
|
0.7 /
0.8 s
|
FeautrierGonnord-SAS2010-exmini_true-termination.c |
6.6 /
2.6 s
|
6.0 /
4.7 s
|
0.7 /
0.8 s
|
eFeautrierGonnord-SAS2010-loops_true-termination.c |
16.3 /
5.6 s
|
11.4 /
5.9 s
|
1.2 /
1.2 s
|
eFeautrierGonnord-SAS2010-ndecr_true-termination.c |
3.5 /
1.5 s
|
5.3 /
4.3 s
|
0.7 /
0.7 s
|
trierGonnord-SAS2010-nestedLoop_true-termination.c |
31.8 /
14.7 s
|
19.8 /
10.7 s
|
5.0 /
5.0 s
|
autrierGonnord-SAS2010-random1d_true-termination.c |
15.8 /
6.8 s
|
5.8 /
4.7 s
|
0.8 /
0.8 s
|
autrierGonnord-SAS2010-random2d_true-termination.c |
706.7 /
300.0 s
|
5.9 /
4.6 s
|
0.9 /
0.9 s
|
rteFeautrierGonnord-SAS2010-rsd_true-termination.c |
303.4 /
300.0 s
|
10.4 /
6.6 s
|
6.4 /
6.2 s
|
rierGonnord-SAS2010-speedFails4_true-termination.c |
6.6 /
2.6 s
|
8.4 /
5.8 s
|
5.6 /
5.5 s
|
trierGonnord-SAS2010-speedpldi2_true-termination.c |
12.5 /
6.5 s
|
12.7 /
8.4 s
|
0.8 /
0.8 s
|
trierGonnord-SAS2010-speedpldi3_true-termination.c |
19.8 /
8.2 s
|
9.2 /
6.5 s
|
5.7 /
5.6 s
|
trierGonnord-SAS2010-speedpldi4_true-termination.c |
6.7 /
2.5 s
|
9.4 /
6.7 s
|
0.7 /
0.8 s
|
utrierGonnord-SAS2010-terminate_true-termination.c |
6.2 /
2.4 s
|
6.1 /
4.6 s
|
0.7 /
0.8 s
|
eFeautrierGonnord-SAS2010-wcet2_true-termination.c |
12.5 /
4.2 s
|
226.3 /
208.1 s
|
0.8 /
0.9 s
|
FeautrierGonnord-SAS2010-while2_true-termination.c |
9.2 /
3.3 s
|
7.3 /
5.1 s
|
0.7 /
0.8 s
|
teFeautrierGonnord-SAS2010-wise_true-termination.c |
32.9 /
10.4 s
|
8.1 /
5.6 s
|
6.2 /
6.0 s
|
C/SVComp/Avery-FLOPS2006-Table1_true-termination.c |
34.5 /
25.9 s
|
6.8 /
4.9 s
|
4.9 /
4.9 s
|
SVComp/Ben-Amram-LMCS2010-Ex2.3_true-termination.c |
12.5 /
4.3 s
|
8.7 /
5.9 s
|
17.8 /
15.9 s
|
nnaSipma-CAV2005-Fig1-modified_false-termination.c |
30.1 /
9.4 s
|
5.2 /
4.3 s
|
7.8 /
7.3 s
|
/BradleyMannaSipma-CAV2005-Fig1_true-termination.c |
28.7 /
8.9 s
|
13.4 /
8.9 s
|
7.1 /
6.8 s
|
radleyMannaSipma-ICALP2005-Fig1_true-termination.c |
764.0 /
300.1 s
|
18.4 /
8.9 s
|
1.0 /
1.0 s
|
ockschmidtCookFuhs-CAV2013-Fig1_true-termination.c |
11.3 /
4.3 s
|
8.7 /
6.1 s
|
0.7 /
0.8 s
|
ckschmidtCookFuhs-CAV2013-Fig9a_true-termination.c |
27.9 /
17.8 s
|
19.4 /
6.5 s
|
0.8 /
0.8 s
|
dtCookFuhs-CAV2013-Introduction_true-termination.c |
6.7 /
2.6 s
|
5.9 /
4.5 s
|
5.1 /
5.1 s
|
lwaniSagivYang-ESOP2008-aaron12_true-termination.c |
1110.7 /
300.1 s
|
4.4 /
3.8 s
|
6.3 /
6.1 s
|
ulwaniSagivYang-ESOP2008-aaron1_true-termination.c |
23.4 /
8.9 s
|
11.6 /
7.9 s
|
0.2 /
0.3 s
|
ulwaniSagivYang-ESOP2008-aaron2_true-termination.c |
21.1 /
9.0 s
|
6.1 /
4.7 s
|
0.8 /
0.8 s
|
ulwaniSagivYang-ESOP2008-aaron3_true-termination.c |
839.2 /
300.1 s
|
11.9 /
7.9 s
|
7.6 /
6.8 s
|
ulwaniSagivYang-ESOP2008-aaron4_true-termination.c |
900.6 /
300.0 s
|
11.3 /
7.5 s
|
0.2 /
0.3 s
|
ulwaniSagivYang-ESOP2008-aaron6_true-termination.c |
308.5 /
300.0 s
|
7.2 /
5.0 s
|
0.8 /
0.8 s
|
GulwaniSagivYang-ESOP2008-easy1_true-termination.c |
5.5 /
2.2 s
|
6.6 /
5.1 s
|
0.8 /
0.8 s
|
GulwaniSagivYang-ESOP2008-easy2_true-termination.c |
7.3 /
2.7 s
|
5.4 /
4.4 s
|
0.7 /
0.7 s
|
waniSagivYang-ESOP2008-random1d_true-termination.c |
18.3 /
7.5 s
|
5.8 /
4.7 s
|
0.8 /
0.8 s
|
waniSagivYang-ESOP2008-random2d_true-termination.c |
720.2 /
300.0 s
|
6.0 /
4.7 s
|
0.9 /
0.9 s
|
rOHearn-TACAS2014-Introduction_false-termination.c |
3.2 /
1.6 s
|
4.8 /
3.9 s
|
5.8 /
5.6 s
|
FlurMukhopadhyay-SAS2012-Ex1.01_true-termination.c |
3.6 /
1.6 s
|
11.3 /
5.9 s
|
5.8 /
5.7 s
|
FlurMukhopadhyay-SAS2012-Ex1.02_true-termination.c |
5.1 /
2.0 s
|
5.9 /
4.7 s
|
0.7 /
0.8 s
|
FlurMukhopadhyay-SAS2012-Ex1.03_true-termination.c |
1.5 /
0.9 s
|
5.8 /
4.6 s
|
0.7 /
0.8 s
|
FlurMukhopadhyay-SAS2012-Ex1.04_true-termination.c |
4.0 /
1.7 s
|
5.8 /
4.6 s
|
0.7 /
0.7 s
|
FlurMukhopadhyay-SAS2012-Ex1.05_true-termination.c |
4.9 /
2.0 s
|
5.8 /
4.6 s
|
0.7 /
0.7 s
|
FlurMukhopadhyay-SAS2012-Ex2.01_true-termination.c |
8.0 /
2.9 s
|
6.1 /
4.5 s
|
5.2 /
5.1 s
|
lurMukhopadhyay-SAS2012-Ex2.02_false-termination.c |
645.4 /
300.0 s
|
16.3 /
7.7 s
|
5.9 /
5.8 s
|
lurMukhopadhyay-SAS2012-Ex2.03_false-termination.c |
26.1 /
15.3 s
|
4.8 /
4.1 s
|
5.9 /
5.7 s
|
lurMukhopadhyay-SAS2012-Ex2.04_false-termination.c |
65.0 /
53.3 s
|
4.9 /
4.0 s
|
5.9 /
5.7 s
|
lurMukhopadhyay-SAS2012-Ex2.05_false-termination.c |
26.4 /
9.1 s
|
5.1 /
4.1 s
|
1.5 /
1.4 s
|
lurMukhopadhyay-SAS2012-Ex2.06_false-termination.c |
632.2 /
300.0 s
|
20.5 /
10.7 s
|
5.9 /
5.8 s
|
FlurMukhopadhyay-SAS2012-Ex2.07_true-termination.c |
5.5 /
2.2 s
|
6.9 /
4.9 s
|
1.0 /
1.0 s
|
FlurMukhopadhyay-SAS2012-Ex2.08_true-termination.c |
10.7 /
3.7 s
|
6.2 /
4.7 s
|
5.2 /
5.1 s
|
FlurMukhopadhyay-SAS2012-Ex2.09_true-termination.c |
406.1 /
105.7 s
|
7.8 /
4.8 s
|
6.9 /
6.6 s
|
FlurMukhopadhyay-SAS2012-Ex2.10_true-termination.c |
4.7 /
1.9 s
|
5.5 /
4.3 s
|
0.7 /
0.8 s
|
lurMukhopadhyay-SAS2012-Ex2.11_false-termination.c |
30.6 /
12.3 s
|
60.7 /
46.4 s
|
5.8 /
5.7 s
|
lurMukhopadhyay-SAS2012-Ex2.12_false-termination.c |
15.0 /
5.4 s
|
4.8 /
3.9 s
|
5.9 /
5.8 s
|
FlurMukhopadhyay-SAS2012-Ex2.13_true-termination.c |
9.1 /
3.3 s
|
6.2 /
4.5 s
|
1.0 /
1.0 s
|
lurMukhopadhyay-SAS2012-Ex2.14_false-termination.c |
32.1 /
21.3 s
|
4.8 /
4.0 s
|
5.8 /
5.8 s
|
lurMukhopadhyay-SAS2012-Ex2.15_false-termination.c |
44.1 /
14.4 s
|
4.8 /
4.0 s
|
5.8 /
5.7 s
|
FlurMukhopadhyay-SAS2012-Ex2.16_true-termination.c |
5.0 /
1.9 s
|
6.0 /
4.6 s
|
1.0 /
1.0 s
|
lurMukhopadhyay-SAS2012-Ex2.17_false-termination.c |
1135.3 /
300.0 s
|
4.8 /
4.0 s
|
5.9 /
5.8 s
|
FlurMukhopadhyay-SAS2012-Ex2.18_true-termination.c |
9.7 /
3.3 s
|
6.0 /
4.5 s
|
5.9 /
5.8 s
|
FlurMukhopadhyay-SAS2012-Ex2.19_true-termination.c |
5.8 /
2.3 s
|
6.1 /
4.7 s
|
1.0 /
1.0 s
|
FlurMukhopadhyay-SAS2012-Ex2.20_true-termination.c |
4.5 /
1.8 s
|
5.7 /
4.6 s
|
0.7 /
0.8 s
|
FlurMukhopadhyay-SAS2012-Ex2.21_true-termination.c |
6.7 /
2.5 s
|
6.0 /
4.7 s
|
1.0 /
1.0 s
|
FlurMukhopadhyay-SAS2012-Ex2.22_true-termination.c |
2.1 /
1.1 s
|
6.7 /
4.9 s
|
0.7 /
0.7 s
|
FlurMukhopadhyay-SAS2012-Ex3.01_true-termination.c |
3.6 /
1.7 s
|
6.3 /
4.7 s
|
5.2 /
5.1 s
|
lurMukhopadhyay-SAS2012-Ex3.02_false-termination.c |
75.7 /
21.7 s
|
4.9 /
4.0 s
|
6.1 /
5.9 s
|
FlurMukhopadhyay-SAS2012-Ex3.03_true-termination.c |
75.2 /
21.5 s
|
7.5 /
5.1 s
|
1.1 /
1.2 s
|
FlurMukhopadhyay-SAS2012-Ex3.04_true-termination.c |
13.1 /
5.5 s
|
6.3 /
4.7 s
|
1.1 /
1.1 s
|
FlurMukhopadhyay-SAS2012-Ex3.05_true-termination.c |
12.9 /
5.3 s
|
6.2 /
4.8 s
|
1.0 /
1.0 s
|
lurMukhopadhyay-SAS2012-Ex3.06_false-termination.c |
916.8 /
300.1 s
|
15.3 /
7.7 s
|
6.1 /
6.0 s
|
FlurMukhopadhyay-SAS2012-Ex3.07_true-termination.c |
7.7 /
2.8 s
|
7.5 /
5.0 s
|
5.3 /
5.2 s
|
lurMukhopadhyay-SAS2012-Ex3.08_false-termination.c |
49.1 /
40.7 s
|
5.0 /
4.2 s
|
6.4 /
6.1 s
|
FlurMukhopadhyay-SAS2012-Ex3.09_true-termination.c |
7.2 /
2.8 s
|
7.7 /
5.2 s
|
0.7 /
0.7 s
|
FlurMukhopadhyay-SAS2012-Ex3.10_true-termination.c |
87.5 /
300.0 s
|
5.5 /
4.3 s
|
0.7 /
0.7 s
|
lurMukhopadhyay-SAS2012-Ex4.01_false-termination.c |
1066.8 /
300.0 s
|
5.1 /
4.1 s
|
6.6 /
6.3 s
|
enFlurMukhopadhyay-SAS2012-Fig1_true-termination.c |
8.0 /
2.9 s
|
7.4 /
5.0 s
|
5.2 /
5.2 s
|
VComp/ColonSipma-TACAS2001-Fig1_true-termination.c |
6.2 /
2.4 s
|
5.9 /
4.6 s
|
0.7 /
0.8 s
|
p/CookSeeZuleger-TACAS2013-Fig1_true-termination.c |
11.1 /
3.8 s
|
9.3 /
6.4 s
|
0.8 /
0.8 s
|
/CookSeeZuleger-TACAS2013-Fig7a_true-termination.c |
13.9 /
5.0 s
|
15.2 /
8.7 s
|
0.8 /
0.8 s
|
/CookSeeZuleger-TACAS2013-Fig7b_true-termination.c |
45.8 /
16.1 s
|
14.2 /
8.3 s
|
0.8 /
0.8 s
|
uleger-TACAS2013-Fig8a-modified_true-termination.c |
5.3 /
2.1 s
|
8.1 /
5.9 s
|
24.8 /
21.6 s
|
/CookSeeZuleger-TACAS2013-Fig8a_true-termination.c |
5.2 /
2.0 s
|
7.9 /
5.6 s
|
25.5 /
22.0 s
|
/CookSeeZuleger-TACAS2013-Fig8b_true-termination.c |
3.5 /
1.5 s
|
10.6 /
6.7 s
|
15.6 /
13.9 s
|
VComp/GopanReps-CAV2006-Fig1a_true-termination.c.c |
7.8 /
2.9 s
|
8.8 /
6.2 s
|
0.8 /
0.8 s
|
p/GulavaniGulwani-CAV2008-Fig1a_true-termination.c |
9.6 /
3.5 s
|
9.5 /
6.8 s
|
5.3 /
5.3 s
|
p/GulavaniGulwani-CAV2008-Fig1b_true-termination.c |
9.8 /
3.6 s
|
6.2 /
4.7 s
|
0.7 /
0.8 s
|
p/GulavaniGulwani-CAV2008-Fig1c_true-termination.c |
4.8 /
2.0 s
|
5.6 /
4.5 s
|
0.7 /
0.7 s
|
lwaniJainKoskinen-PLDI2009-Fig1_true-termination.c |
881.7 /
300.0 s
|
339.6 /
300.0 s
|
51.8 /
43.6 s
|
risLalNoriRajamani-SAS2010-Fig1_true-termination.c |
66.3 /
27.1 s
|
11.3 /
5.7 s
|
0.9 /
1.0 s
|
isLalNoriRajamani-SAS2010-Fig2_false-termination.c |
89.8 /
37.0 s
|
7.6 /
5.5 s
|
71.8 /
57.6 s
|
risLalNoriRajamani-SAS2010-Fig3_true-termination.c |
5.0 /
2.0 s
|
5.8 /
4.6 s
|
6.4 /
6.2 s
|
ickeLeikePodelski-ATVA2013-Fig1_true-termination.c |
5.0 /
2.0 s
|
5.7 /
4.5 s
|
1.0 /
1.0 s
|
ickeLeikePodelski-ATVA2013-Fig2_true-termination.c |
14.1 /
5.0 s
|
13.5 /
6.4 s
|
5.6 /
5.6 s
|
ickeLeikePodelski-ATVA2013-Fig4_true-termination.c |
2.9 /
1.4 s
|
5.4 /
4.3 s
|
0.7 /
0.8 s
|
ickeLeikePodelski-ATVA2013-Fig5_true-termination.c |
4.3 /
1.8 s
|
12.6 /
6.0 s
|
5.6 /
5.5 s
|
ickeLeikePodelski-ATVA2013-Fig6_true-termination.c |
3.8 /
1.6 s
|
6.6 /
4.9 s
|
0.7 /
0.8 s
|
ickeLeikePodelski-ATVA2013-Fig7_true-termination.c |
9.3 /
3.5 s
|
6.2 /
4.7 s
|
6.3 /
6.1 s
|
ickeLeikePodelski-ATVA2013-Fig8_true-termination.c |
626.5 /
300.0 s
|
9.3 /
5.1 s
|
0.9 /
0.9 s
|
ickeLeikePodelski-ATVA2013-Fig9_true-termination.c |
625.4 /
300.0 s
|
10.3 /
5.4 s
|
6.2 /
6.0 s
|
rSutre-POPL2002-LockingExample_false-termination.c |
29.6 /
10.4 s
|
5.2 /
4.1 s
|
11.3 /
10.2 s
|
itovichWintersteiger-CAV2010-Ex_true-termination.c |
8.6 /
3.1 s
|
5.7 /
4.6 s
|
4.9 /
4.9 s
|
ovichWintersteiger-CAV2010-Fig1_true-termination.c |
304.7 /
300.0 s
|
23.6 /
10.8 s
|
6.2 /
6.0 s
|
C/SVComp/LICENSE.txt |
0.8 /
0.5 s
|
3.9 /
3.1 s
|
0.0 /
0.0 s
|
z-CarbonellRubio-FMCAD2013-Fig1_true-termination.c |
959.3 /
300.0 s
|
14.3 /
8.7 s
|
5.4 /
5.4 s
|
/LeeJonesBen-Amram-POPL2001-Ex1_true-termination.c |
3.8 /
1.6 s
|
21.5 /
9.5 s
|
1.4 /
1.4 s
|
/LeeJonesBen-Amram-POPL2001-Ex2_true-termination.c |
4.3 /
1.8 s
|
22.4 /
10.2 s
|
5.8 /
5.7 s
|
/LeeJonesBen-Amram-POPL2001-Ex3_true-termination.c |
4.9 /
2.0 s
|
663.1 /
255.9 s
|
0.9 /
0.9 s
|
/LeeJonesBen-Amram-POPL2001-Ex4_true-termination.c |
6.9 /
2.7 s
|
21.0 /
10.6 s
|
0.8 /
0.8 s
|
/LeeJonesBen-Amram-POPL2001-Ex5_true-termination.c |
434.6 /
300.0 s
|
32.1 /
17.8 s
|
7.7 /
7.3 s
|
/LeeJonesBen-Amram-POPL2001-Ex6_true-termination.c |
6.2 /
2.3 s
|
10.4 /
6.3 s
|
6.3 /
6.2 s
|
omp/LeikeHeizmann-TACAS2014-Ex1_true-termination.c |
6.0 /
2.3 s
|
5.9 /
4.7 s
|
0.7 /
0.7 s
|
omp/LeikeHeizmann-TACAS2014-Ex7_true-termination.c |
11.1 /
3.6 s
|
5.9 /
4.5 s
|
1.0 /
1.0 s
|
omp/LeikeHeizmann-TACAS2014-Ex8_true-termination.c |
7.6 /
2.8 s
|
8.2 /
5.7 s
|
0.7 /
0.8 s
|
omp/LeikeHeizmann-TACAS2014-Ex9_true-termination.c |
6.5 /
2.4 s
|
6.9 /
5.1 s
|
0.7 /
0.8 s
|
mp/LeikeHeizmann-TACAS2014-Fig1_true-termination.c |
8.2 /
2.9 s
|
5.9 /
4.4 s
|
1.0 /
1.0 s
|
Comp/LeikeHeizmann-WST2014-Ex5_false-termination.c |
1104.1 /
300.0 s
|
16.3 /
7.3 s
|
5.9 /
5.8 s
|
Comp/LeikeHeizmann-WST2014-Ex6_false-termination.c |
1184.6 /
300.1 s
|
18.5 /
8.4 s
|
6.1 /
6.0 s
|
VComp/LeikeHeizmann-WST2014-Ex9_true-termination.c |
3.1 /
1.4 s
|
6.0 /
4.6 s
|
5.5 /
5.5 s
|
C/SVComp/Masse-VMCAI2014-Ex6_true-termination.c |
9.5 /
3.4 s
|
9.3 /
6.9 s
|
0.7 /
0.8 s
|
C/SVComp/Masse-VMCAI2014-Fig1a_true-termination.c |
8.1 /
3.0 s
|
7.4 /
5.4 s
|
5.2 /
5.2 s
|
C/SVComp/Masse-VMCAI2014-Fig1b_true-termination.c |
45.3 /
20.0 s
|
13.0 /
7.2 s
|
6.1 /
6.0 s
|
/SVComp/NoriSharma-FSE2013-Fig7_true-termination.c |
64.4 /
52.3 s
|
15.7 /
7.7 s
|
0.8 /
0.8 s
|
/SVComp/NoriSharma-FSE2013-Fig8_true-termination.c |
28.3 /
16.6 s
|
10.4 /
7.0 s
|
4.9 /
4.9 s
|
delskiRybalchenko-LICS2004-Fig1_true-termination.c |
9.2 /
3.3 s
|
10.6 /
5.8 s
|
1.1 /
1.1 s
|
delskiRybalchenko-LICS2004-Fig2_true-termination.c |
1117.9 /
300.0 s
|
647.1 /
300.0 s
|
32.6 /
28.1 s
|
elskiRybalchenko-TACAS2011-Fig1_true-termination.c |
2.7 /
1.3 s
|
5.3 /
4.2 s
|
0.7 /
0.7 s
|
elskiRybalchenko-TACAS2011-Fig2_true-termination.c |
11.8 /
4.1 s
|
7.4 /
5.3 s
|
0.7 /
0.8 s
|
elskiRybalchenko-TACAS2011-Fig3_true-termination.c |
1111.2 /
300.0 s
|
645.8 /
300.1 s
|
20.5 /
18.0 s
|
elskiRybalchenko-TACAS2011-Fig4_true-termination.c |
8.3 /
3.0 s
|
8.6 /
6.0 s
|
0.8 /
0.8 s
|
delskiRybalchenko-VMCAI2004-Ex1_true-termination.c |
16.3 /
6.1 s
|
10.4 /
7.6 s
|
6.9 /
6.6 s
|
delskiRybalchenko-VMCAI2004-Ex2_true-termination.c |
3.6 /
1.6 s
|
11.8 /
6.1 s
|
1.6 /
1.5 s
|
C/SVComp/README.txt |
0.8 /
0.5 s
|
3.9 /
3.4 s
|
0.0 /
0.0 s
|
C/SVComp/TelAviv-Amir-Minimum_true-termination.c |
1024.8 /
300.0 s
|
21.9 /
14.0 s
|
0.8 /
0.8 s
|
/SVComp/Toulouse-BranchesToLoop_true-termination.c |
8.1 /
2.9 s
|
7.7 /
5.1 s
|
374.9 /
300.0 s
|
mp/Toulouse-MultiBranchesToLoop_true-termination.c |
7.1 /
2.8 s
|
10.9 /
7.3 s
|
376.6 /
300.0 s
|
C/SVComp/Urban-WST2013-Fig1_false-termination.c |
3.1 /
1.5 s
|
5.8 /
4.4 s
|
14.3 /
12.8 s
|
Urban-WST2013-Fig2-modified1000_true-termination.c |
6.7 /
2.5 s
|
332.2 /
300.0 s
|
0.8 /
0.8 s
|
C/SVComp/Urban-WST2013-Fig2_true-termination.c |
6.7 /
2.5 s
|
8.9 /
6.4 s
|
4.9 /
4.9 s
|
/SVComp/UrbanMine-ESOP2014-Fig3_true-termination.c |
45.9 /
16.2 s
|
21.7 /
10.0 s
|
98.3 /
83.2 s
|
C/SVComp/Velroyen_false-termination.c |
10.7 /
3.5 s
|
5.0 /
4.1 s
|
36.3 /
31.4 s
|
C/SVComp/aviad_true-termination.c |
17.4 /
6.8 s
|
12.1 /
6.6 s
|
6.2 /
6.0 s
|
C/SVComp/gcd1_true-termination.c |
50.7 /
15.6 s
|
19.1 /
13.4 s
|
0.8 /
0.8 s
|
C/SVComp/genady_true-termination.c |
15.0 /
6.6 s
|
5.5 /
4.2 s
|
0.7 /
0.7 s
|
C/SVComp/joey_false-termination.c |
10.3 /
4.2 s
|
23.0 /
10.6 s
|
6.4 /
6.3 s
|
C/SVComp/min_rf_true-termination.c |
53.8 /
29.3 s
|
24.2 /
13.7 s
|
52.8 /
45.1 s
|
C/SVComp/svcomp_cstrcmp_true-termination.c |
7.2 /
2.8 s
|
258.2 /
254.0 s
|
0.3 /
0.3 s
|
C/SVComp/svcomp_cstrcspn_true-termination.c |
22.4 /
9.3 s
|
277.1 /
272.6 s
|
2.5 /
2.3 s
|
C/SVComp/svcomp_cstrlen_true-termination.c |
3.2 /
1.5 s
|
23.2 /
11.9 s
|
6.1 /
5.9 s
|
C/SVComp/svcomp_cstrncmp_true-termination.c |
8.7 /
3.3 s
|
228.5 /
214.7 s
|
0.3 /
0.3 s
|
C/SVComp/svcomp_cstrpbrk_true-termination.c |
16.7 /
6.3 s
|
200.9 /
196.7 s
|
2.5 /
2.2 s
|
C/SVComp/svcomp_cstrspn_true-termination.c |
21.7 /
8.3 s
|
214.3 /
210.3 s
|
2.5 /
2.2 s
|
C/SVComp/svcomp_strchr_true-termination.c |
4.3 /
1.8 s
|
30.9 /
16.7 s
|
6.1 /
5.9 s
|
C/Ultimate/2Nested_true-termination.c |
11.6 /
3.8 s
|
5.8 /
4.5 s
|
5.2 /
5.2 s
|
C/Ultimate/4BitCounterPointer_true-termination.c |
2.5 /
1.2 s
|
296.8 /
243.0 s
|
6.2 /
6.0 s
|
/Ultimate/4NestedWith3Variables_true-termination.c |
100.3 /
28.0 s
|
11.1 /
5.8 s
|
6.1 /
5.9 s
|
ays01-EquivalentConstantIndices_true-termination.c |
2.3 /
1.2 s
|
10.7 /
4.3 s
|
5.4 /
5.4 s
|
ys02-EquivalentConstantIndices_false-termination.c |
3.7 /
1.9 s
|
6.8 /
4.6 s
|
5.4 /
5.4 s
|
ate/Arrays03-ValueRestictsIndex_true-termination.c |
1.0 /
0.6 s
|
7.0 /
5.2 s
|
0.8 /
0.8 s
|
C/Ultimate/Bangalore_true-termination.c |
5.1 /
2.1 s
|
5.6 /
4.9 s
|
0.7 /
0.7 s
|
C/Ultimate/Benghazi_true-termination.c |
11.3 /
3.9 s
|
7.9 /
5.2 s
|
5.4 /
5.4 s
|
C/Ultimate/Cairo_true-termination.c |
3.5 /
1.6 s
|
6.5 /
4.8 s
|
5.4 /
5.3 s
|
C/Ultimate/Collatz_unknown-termination.c |
101.5 /
28.3 s
|
25.8 /
12.0 s
|
5.6 /
5.6 s
|
C/Ultimate/Copenhagen_true-termination.c |
4.2 /
1.7 s
|
5.6 /
4.5 s
|
6.0 /
5.9 s
|
C/Ultimate/Division_false-termination.c |
7.1 /
2.8 s
|
5.0 /
4.1 s
|
5.6 /
5.5 s
|
C/Ultimate/Gothenburg_true-termination.c |
17.7 /
8.3 s
|
16.1 /
7.9 s
|
5.7 /
5.6 s
|
C/Ultimate/LICENSE.txt |
0.8 /
0.5 s
|
3.9 /
3.1 s
|
0.0 /
0.0 s
|
C/Ultimate/LexIndexValue-Array_true-termination.c |
1.0 /
0.6 s
|
10.9 /
6.9 s
|
6.0 /
5.9 s
|
/Ultimate/LexIndexValue-Pointer_true-termination.c |
1.1 /
0.7 s
|
323.7 /
300.0 s
|
6.1 /
5.9 s
|
timate/Lobnya-Boolean-Reordered_true-termination.c |
3.5 /
1.5 s
|
26.6 /
11.7 s
|
0.2 /
0.3 s
|
C/Ultimate/Madrid_false-termination.c |
2.3 /
1.2 s
|
4.7 /
3.8 s
|
300.1 /
300.0 s
|
C/Ultimate/MenloPark_true-termination.c |
7.8 /
2.9 s
|
7.3 /
5.0 s
|
6.0 /
5.8 s
|
C/Ultimate/Mysore_true-termination.c |
8.7 /
3.2 s
|
6.0 /
4.6 s
|
5.1 /
5.1 s
|
C/Ultimate/NonTermination1_false-termination.c |
32.9 /
12.4 s
|
4.9 /
3.9 s
|
1.5 /
1.4 s
|
C/Ultimate/NonTermination2_false-termination.c |
817.8 /
300.0 s
|
4.9 /
4.1 s
|
0.7 /
0.7 s
|
C/Ultimate/NonTermination3_false-termination.c |
1.0 /
0.6 s
|
8.7 /
4.9 s
|
5.9 /
5.7 s
|
C/Ultimate/NonTermination4_false-termination.c |
1181.7 /
300.1 s
|
13.8 /
6.9 s
|
5.7 /
5.6 s
|
Ultimate/NonTerminationSimple2_false-termination.c |
11.0 /
4.1 s
|
4.8 /
4.1 s
|
5.6 /
5.5 s
|
Ultimate/NonTerminationSimple3_false-termination.c |
45.4 /
15.0 s
|
4.8 /
3.9 s
|
5.8 /
5.7 s
|
Ultimate/NonTerminationSimple4_false-termination.c |
1119.5 /
300.0 s
|
4.9 /
3.8 s
|
1.7 /
1.6 s
|
Ultimate/NonTerminationSimple5_false-termination.c |
31.6 /
10.0 s
|
6.9 /
5.1 s
|
6.0 /
5.8 s
|
Ultimate/NonTerminationSimple6_false-termination.c |
17.1 /
5.9 s
|
4.8 /
4.1 s
|
5.9 /
5.8 s
|
Ultimate/NonTerminationSimple7_false-termination.c |
3.0 /
1.5 s
|
4.8 /
4.1 s
|
5.9 /
5.8 s
|
Ultimate/NonTerminationSimple8_false-termination.c |
325.3 /
91.9 s
|
5.0 /
3.9 s
|
7.3 /
7.0 s
|
Ultimate/NonTerminationSimple9_false-termination.c |
9.9 /
3.9 s
|
4.9 /
4.0 s
|
5.7 /
5.6 s
|
C/Ultimate/Nyala-2lex_true-termination.c |
9.4 /
3.2 s
|
7.7 /
5.5 s
|
0.7 /
0.7 s
|
C/Ultimate/Parallel_true-termination.c |
6.5 /
2.4 s
|
8.3 /
5.9 s
|
4.9 /
4.9 s
|
C/Ultimate/Piecewise_true-termination.c |
20.8 /
7.2 s
|
11.8 /
8.1 s
|
0.7 /
0.8 s
|
C/Ultimate/Pure2Phase_true-termination.c |
9.3 /
3.3 s
|
8.2 /
5.9 s
|
0.7 /
0.8 s
|
C/Ultimate/Pure3Phase_true-termination.c |
1136.6 /
300.0 s
|
8.2 /
5.8 s
|
7.6 /
7.3 s
|
C/Ultimate/README.txt |
0.8 /
0.5 s
|
3.9 /
3.0 s
|
0.0 /
0.0 s
|
ltimate/RecursiveMultiplication_true-termination.c |
3.6 /
1.6 s
|
8.9 /
6.0 s
|
24.1 /
21.0 s
|
timate/RecursiveNonterminating_false-termination.c |
19.7 /
9.2 s
|
5.2 /
4.1 s
|
6.2 /
6.0 s
|
C/Ultimate/Rotation180_false-termination.c |
4.8 /
2.2 s
|
5.0 /
4.1 s
|
300.1 /
300.0 s
|
C/Ultimate/Stockholm_true-termination.c |
5.8 /
2.3 s
|
5.8 /
4.5 s
|
1.0 /
1.0 s
|
Ultimate/SyntaxSupportPointer01_true-termination.c |
1.1 /
0.7 s
|
11.8 /
7.1 s
|
5.5 /
5.5 s
|
C/Ultimate/Thun_true-termination.c |
5.5 /
2.1 s
|
5.9 /
4.6 s
|
1.0 /
1.0 s
|
C/Ultimate/Waldkirch_true-termination.c |
1.1 /
0.7 s
|
5.3 /
4.0 s
|
0.7 /
0.7 s
|
C/Ultimate/WhileFalse_true-termination.c |
1.0 /
0.7 s
|
4.6 /
3.8 s
|
0.5 /
0.5 s
|
C/Ultimate/WhileTrue_false-termination.c |
2.2 /
1.2 s
|
4.7 /
3.8 s
|
0.2 /
0.3 s
|