| alloca/svcomp_Avery-2006FLOPS-Tabel1_true-alloca.c
|
YES
195.2 /
217.1
|
YES
1.6 /
2.7
|
YES
58.4 /
48.9
|
| loca/svcomp_Ben-Amram-2010LMCS-Ex2.3_true-alloca.c
|
YES
23.0 /
9.1
|
YES
0.9 /
1.9
|
YES
54.0 /
41.0
|
| nnaSipma-2005CAV-Fig1-modified_false-termination.c
|
.
306.4 /
300.1
|
NO
0.8 /
1.6
|
.
33.9 /
17.5
|
| vcomp_BradleyMannaSipma-2005CAV-Fig1_true-alloca.c
|
.
488.2 /
300.0
|
YES
148.8 /
194.9
|
.
246.6 /
300.1
|
| omp_BradleyMannaSipma-2005ICALP-Fig1_true-alloca.c
|
.
310.6 /
300.1
|
NO
0.8 /
1.5
|
.
30.4 /
20.9
|
| mp_BrockschmidtCookFuhs-2013CAV-Fig1_true-alloca.c
|
YES
38.3 /
32.1
|
.
15.0 /
9.8
|
YES
97.1 /
129.2
|
| schmidtCookFuhs-2013CAV-Introduction_true-alloca.c
|
YES
16.5 /
7.2
|
YES
0.4 /
0.7
|
YES
16.3 /
9.4
|
| mp_ChenFlurMukhopadhyay-2012SAS-Fig1_true-alloca.c
|
YES
17.5 /
6.7
|
YES
7.9 /
16.7
|
YES
28.9 /
20.2
|
| svcomp_CookSeeZuleger-2013TACAS-Fig3_true-alloca.c
|
YES
15.5 /
8.2
|
YES
0.5 /
1.4
|
YES
25.9 /
33.8
|
| vcomp_CookSeeZuleger-2013TACAS-Fig7a_true-alloca.c
|
YES
24.4 /
9.2
|
YES
0.8 /
0.8
|
.
262.7 /
300.0
|
| vcomp_CookSeeZuleger-2013TACAS-Fig7b_true-alloca.c
|
YES
60.0 /
20.4
|
YES
1.1 /
2.1
|
.
265.8 /
300.0
|
| mp_GulwaniJainKoskinen-2009PLDI-Fig1_true-alloca.c
|
YES
22.3 /
8.7
|
.
72.2 /
132.5
|
.
326.6 /
300.0
|
| p_HarrisLalNoriRajamani-2010SAS-Fig1_true-alloca.c
|
YES
6.4 /
3.0
|
YES
15.2 /
24.1
|
.
158.3 /
300.0
|
| 0SAS-Fig2_false-unreach-label-termination-alloca.c
|
NO
120.1 /
52.4
|
NO
28.8 /
50.5
|
.
150.7 /
300.0
|
| p_HarrisLalNoriRajamani-2010SAS-Fig3_true-alloca.c
|
.
14.9 /
5.9
|
.
0.2 /
0.5
|
YES
13.2 /
7.2
|
| aTsitovichWintersteiger-2010CAV-Fig1_true-alloca.c
|
.
429.7 /
300.1
|
YES
5.3 /
9.7
|
YES
28.6 /
27.1
|
| riguez-CarbonellRubio-2013FMCAD-Fig1_true-alloca.c
|
.
422.1 /
300.1
|
.
9.7 /
9.8
|
.
174.0 /
300.1
|
| C/AProVE_memory_alloca/svcomp_Masse_true-alloca.c
|
.
341.8 /
300.1
|
.
20.9 /
21.1
|
.
21.7 /
14.4
|
| lloca/svcomp_NoriSharma-2013FSE-Fig7_true-alloca.c
|
.
429.7 /
300.0
|
YES
2.7 /
2.7
|
.
234.7 /
300.0
|
| lloca/svcomp_NoriSharma-2013FSE-Fig8_true-alloca.c
|
YES
180.8 /
199.6
|
YES
2.7 /
4.2
|
.
303.0 /
300.1
|
| mp_PodelskiRybalchenko-2004VMCAI-Ex2_true-alloca.c
|
NO
4.7 /
6.1
|
NO
0.2 /
0.2
|
.
29.2 /
14.7
|
| y_alloca/svcomp_TelAviv-Amir-Minimum_true-alloca.c
|
.
401.5 /
300.1
|
YES
1.0 /
1.5
|
.
355.8 /
300.1
|
| lloca/svcomp_Toulouse-BranchesToLoop_true-alloca.c
|
YES
14.1 /
7.2
|
YES
1.7 /
2.9
|
YES
44.4 /
64.2
|
| /svcomp_Toulouse-MultiBranchesToLoop_true-alloca.c
|
YES
15.7 /
15.6
|
YES
7.9 /
8.0
|
.
235.7 /
300.1
|
| 3WST-Fig1_false-unreach-label-termination-alloca.c
|
NO
3.9 /
3.1
|
.
0.5 /
0.6
|
.
23.1 /
10.2
|
| comp_Urban-2013WST-Fig2-modified1000_true-alloca.c
|
YES
16.9 /
6.7
|
YES
0.4 /
0.8
|
.
250.9 /
300.0
|
| ory_alloca/svcomp_Urban-2013WST-Fig2_true-alloca.c
|
YES
21.4 /
23.5
|
YES
0.4 /
0.7
|
.
315.5 /
300.0
|
| C/AProVE_memory_alloca/svcomp_Urban_true-alloca.c
|
YES
51.2 /
18.3
|
YES
0.8 /
1.5
|
YES
37.6 /
26.0
|
| _Velroyen_false-unreach-label-termination-alloca.c
|
NO
4.8 /
2.6
|
.
1.0 /
1.1
|
.
27.7 /
14.7
|
| C/AProVE_memory_alloca/svcomp_a.01-alloca.c
|
YES
119.7 /
54.6
|
.
6.0 /
11.1
|
.
251.6 /
300.1
|
| C/AProVE_memory_alloca/svcomp_a.04-alloca.c
|
YES
34.8 /
28.9
|
YES
0.5 /
0.6
|
YES
22.4 /
31.3
|
| C/AProVE_memory_alloca/svcomp_a.05-alloca.c
|
YES
40.4 /
37.2
|
YES
0.5 /
0.5
|
YES
22.0 /
32.9
|
| C/AProVE_memory_alloca/svcomp_a.06-alloca.c
|
YES
108.0 /
49.4
|
YES
1.0 /
1.2
|
YES
37.9 /
28.1
|
| C/AProVE_memory_alloca/svcomp_a.07-alloca.c
|
YES
202.9 /
121.0
|
YES
1.1 /
2.5
|
YES
38.8 /
29.0
|
| C/AProVE_memory_alloca/svcomp_a.08-alloca.c
|
YES
48.8 /
56.3
|
YES
0.5 /
1.2
|
YES
23.8 /
33.4
|
| C/AProVE_memory_alloca/svcomp_a.09_assume-alloca.c
|
YES
14.4 /
13.6
|
.
0.4 /
0.7
|
YES
21.6 /
13.9
|
| C/AProVE_memory_alloca/svcomp_a.10-alloca.c
|
YES
51.9 /
41.4
|
YES
0.9 /
0.9
|
YES
31.1 /
20.9
|
| C/AProVE_memory_alloca/svcomp_add_last_alloca.c
|
.
3.4 /
2.0
|
.
2.2 /
4.4
|
.
167.4 /
300.1
|
| C/AProVE_memory_alloca/svcomp_array01_alloca.c
|
YES
39.0 /
43.3
|
.
13.2 /
22.9
|
YES
18.8 /
11.1
|
| C/AProVE_memory_alloca/svcomp_array02_alloca.c
|
YES
169.0 /
105.0
|
.
12.7 /
22.5
|
YES
26.7 /
19.4
|
| C/AProVE_memory_alloca/svcomp_array03_alloca.c
|
YES
180.2 /
73.4
|
.
33.2 /
33.2
|
YES
26.7 /
64.2
|
| C/AProVE_memory_alloca/svcomp_aviad_true-alloca.c
|
.
40.1 /
19.8
|
YES
1.5 /
1.5
|
.
254.0 /
300.0
|
| C/AProVE_memory_alloca/svcomp_b.01-alloca.c
|
YES
33.9 /
25.3
|
YES
0.5 /
0.5
|
YES
20.9 /
14.3
|
| C/AProVE_memory_alloca/svcomp_b.02-alloca.c
|
YES
97.7 /
60.7
|
YES
0.5 /
1.1
|
YES
23.3 /
32.6
|
| E_memory_alloca/svcomp_b.03-no-inv_assume-alloca.c
|
YES
11.2 /
4.9
|
YES
0.6 /
1.4
|
YES
16.5 /
19.9
|
| C/AProVE_memory_alloca/svcomp_b.03_assume-alloca.c
|
YES
12.1 /
5.2
|
.
0.3 /
0.4
|
YES
16.7 /
13.3
|
| C/AProVE_memory_alloca/svcomp_b.04-alloca.c
|
YES
5.2 /
2.4
|
YES
0.5 /
0.5
|
YES
24.1 /
15.4
|
| C/AProVE_memory_alloca/svcomp_b.05-alloca.c
|
YES
15.0 /
14.0
|
YES
0.5 /
0.5
|
YES
16.2 /
9.2
|
| C/AProVE_memory_alloca/svcomp_b.06-alloca.c
|
YES
55.7 /
27.1
|
YES
0.7 /
0.8
|
YES
22.8 /
13.8
|
| C/AProVE_memory_alloca/svcomp_b.07-alloca.c
|
YES
223.0 /
241.5
|
YES
0.9 /
0.9
|
YES
35.6 /
51.3
|
| E_memory_alloca/svcomp_b.09-no-inv_assume-alloca.c
|
YES
39.7 /
51.0
|
YES
4.9 /
4.9
|
YES
44.0 /
44.5
|
| C/AProVE_memory_alloca/svcomp_b.09_assume-alloca.c
|
YES
42.0 /
34.9
|
.
0.7 /
1.7
|
YES
31.6 /
39.9
|
| C/AProVE_memory_alloca/svcomp_b.10-alloca.c
|
YES
73.0 /
63.7
|
YES
0.8 /
1.8
|
YES
29.1 /
46.2
|
| C/AProVE_memory_alloca/svcomp_b.11-alloca.c
|
YES
127.5 /
133.8
|
YES
1.0 /
1.0
|
YES
101.4 /
149.0
|
| C/AProVE_memory_alloca/svcomp_b.12-alloca.c
|
YES
44.5 /
30.1
|
YES
0.8 /
1.7
|
YES
34.8 /
23.8
|
| C/AProVE_memory_alloca/svcomp_b.13-alloca.c
|
YES
155.5 /
73.2
|
YES
1.2 /
1.3
|
YES
55.1 /
63.8
|
| C/AProVE_memory_alloca/svcomp_b.14-alloca.c
|
YES
32.1 /
13.3
|
.
6.3 /
6.5
|
YES
29.4 /
19.7
|
| C/AProVE_memory_alloca/svcomp_b.15-alloca.c
|
YES
65.8 /
71.3
|
.
11.9 /
18.0
|
YES
93.7 /
141.9
|
| C/AProVE_memory_alloca/svcomp_b.16-alloca.c
|
YES
37.8 /
38.7
|
YES
0.8 /
1.4
|
YES
32.8 /
23.0
|
| C/AProVE_memory_alloca/svcomp_b.17-alloca.c
|
YES
147.3 /
117.1
|
.
14.2 /
23.0
|
YES
60.8 /
47.7
|
| C/AProVE_memory_alloca/svcomp_b.18-alloca.c
|
YES
10.2 /
4.7
|
.
11.5 /
13.8
|
YES
30.7 /
21.0
|
| C/AProVE_memory_alloca/svcomp_bubblesort_alloca.c
|
YES
239.2 /
199.5
|
.
83.4 /
83.4
|
.
293.3 /
300.0
|
| C/AProVE_memory_alloca/svcomp_c.01-no-inv-alloca.c
|
YES
43.1 /
16.3
|
.
8.1 /
13.2
|
.
184.7 /
300.1
|
| C/AProVE_memory_alloca/svcomp_c.01_assume-alloca.c
|
YES
33.3 /
19.5
|
.
0.4 /
1.2
|
YES
37.0 /
25.9
|
| C/AProVE_memory_alloca/svcomp_c.02-alloca.c
|
YES
45.3 /
26.3
|
.
7.1 /
14.5
|
.
222.3 /
300.1
|
| C/AProVE_memory_alloca/svcomp_c.03-alloca.c
|
YES
194.8 /
158.4
|
YES
1.2 /
1.3
|
YES
130.9 /
278.0
|
| C/AProVE_memory_alloca/svcomp_c.07-alloca.c
|
YES
189.5 /
111.4
|
YES
1.6 /
2.5
|
.
148.8 /
300.0
|
| C/AProVE_memory_alloca/svcomp_c.08-alloca.c
|
YES
219.2 /
102.1
|
.
6.2 /
10.5
|
.
202.7 /
300.0
|
| C/AProVE_memory_alloca/svcomp_count_down_alloca.c
|
YES
86.2 /
41.2
|
.
2.0 /
2.0
|
.
223.2 /
300.0
|
| C/AProVE_memory_alloca/svcomp_cstrcat_alloca.c
|
.
10.6 /
4.4
|
.
1.7 /
1.7
|
.
223.2 /
300.0
|
| /AProVE_memory_alloca/svcomp_cstrchr_true_alloca.c
|
YES
17.5 /
8.0
|
.
41.8 /
41.7
|
YES
18.5 /
22.9
|
| /AProVE_memory_alloca/svcomp_cstrcmp_true_alloca.c
|
YES
24.4 /
11.3
|
.
22.4 /
25.1
|
.
308.3 /
300.0
|
| C/AProVE_memory_alloca/svcomp_cstrcpy_alloca.c
|
YES
23.3 /
23.0
|
.
1.7 /
3.5
|
.
220.3 /
300.1
|
| AProVE_memory_alloca/svcomp_cstrcspn_true_alloca.c
|
YES
84.0 /
47.9
|
.
0.3 /
1.0
|
.
237.1 /
300.0
|
| /AProVE_memory_alloca/svcomp_cstrlen_true_alloca.c
|
YES
11.8 /
5.2
|
.
0.2 /
0.6
|
YES
16.1 /
19.8
|
| C/AProVE_memory_alloca/svcomp_cstrncat_alloca.c
|
.
12.1 /
4.2
|
.
0.6 /
0.6
|
.
306.7 /
300.0
|
| AProVE_memory_alloca/svcomp_cstrncmp_true_alloca.c
|
YES
36.9 /
14.2
|
.
0.5 /
1.1
|
.
153.1 /
300.0
|
| C/AProVE_memory_alloca/svcomp_cstrncpy_alloca.c
|
YES
69.9 /
71.1
|
.
0.5 /
0.5
|
.
323.0 /
300.0
|
| AProVE_memory_alloca/svcomp_cstrpbrk_true_alloca.c
|
YES
56.0 /
27.1
|
.
42.1 /
42.0
|
.
153.7 /
300.0
|
| /AProVE_memory_alloca/svcomp_cstrspn_true_alloca.c
|
YES
70.4 /
26.6
|
.
0.3 /
0.6
|
.
213.2 /
300.1
|
| C/AProVE_memory_alloca/svcomp_diff_alloca.c
|
.
280.5 /
300.1
|
.
12.0 /
26.7
|
.
132.2 /
300.0
|
| C/AProVE_memory_alloca/svcomp_easySum-alloca.c
|
YES
103.4 /
48.6
|
YES
0.5 /
0.5
|
YES
20.6 /
32.4
|
| C/AProVE_memory_alloca/svcomp_ex1-alloca.c
|
YES
11.4 /
6.1
|
YES
1.0 /
1.0
|
YES
57.2 /
59.7
|
| C/AProVE_memory_alloca/svcomp_ex2-alloca.c
|
YES
89.3 /
37.3
|
YES
3.9 /
6.6
|
.
135.9 /
300.0
|
| C/AProVE_memory_alloca/svcomp_ex3a-alloca.c
|
YES
15.2 /
16.4
|
YES
0.5 /
1.4
|
.
33.3 /
46.4
|
| C/AProVE_memory_alloca/svcomp_ex3b-alloca.c
|
YES
23.9 /
23.1
|
YES
0.6 /
0.7
|
.
41.0 /
50.9
|
| C/AProVE_memory_alloca/svcomp_fermat-alloca.c
|
YES
291.6 /
131.0
|
.
43.6 /
48.7
|
.
243.8 /
300.1
|
| C/AProVE_memory_alloca/svcomp_flag-alloca.c
|
YES
40.8 /
21.1
|
YES
1.1 /
1.1
|
YES
49.2 /
32.2
|
| C/AProVE_memory_alloca/svcomp_gcd1_true-alloca.c
|
YES
55.6 /
55.6
|
.
9.6 /
11.8
|
.
41.3 /
54.0
|
| C/AProVE_memory_alloca/svcomp_genady_true-alloca.c
|
YES
86.7 /
50.5
|
YES
0.3 /
0.3
|
YES
14.9 /
25.1
|
| AProVE_memory_alloca/svcomp_insertionsort_alloca.c
|
YES
118.0 /
86.9
|
.
20.2 /
21.1
|
.
332.0 /
300.0
|
| C/AProVE_memory_alloca/svcomp_java_AG313-alloca.c
|
YES
23.8 /
21.0
|
YES
0.8 /
1.4
|
YES
22.3 /
26.9
|
| C/AProVE_memory_alloca/svcomp_java_Break-alloca.c
|
YES
10.6 /
13.3
|
YES
0.3 /
0.4
|
YES
14.5 /
16.4
|
| roVE_memory_alloca/svcomp_java_BubbleSort_alloca.c
|
.
125.1 /
55.0
|
.
83.3 /
83.3
|
.
208.0 /
300.1
|
| ProVE_memory_alloca/svcomp_java_Continue1-alloca.c
|
YES
14.8 /
8.0
|
YES
0.4 /
0.4
|
.
178.1 /
300.1
|
| roVE_memory_alloca/svcomp_java_LogBuiltIn-alloca.c
|
YES
14.5 /
6.0
|
YES
0.4 /
0.5
|
YES
15.6 /
9.1
|
| C/AProVE_memory_alloca/svcomp_java_Nested-alloca.c
|
YES
33.7 /
28.0
|
YES
0.6 /
0.6
|
.
75.1 /
124.9
|
| AProVE_memory_alloca/svcomp_java_Sequence-alloca.c
|
YES
16.2 /
7.0
|
YES
0.6 /
1.5
|
.
213.2 /
300.1
|
| C/AProVE_memory_alloca/svcomp_lis_alloca.c
|
.
279.1 /
300.0
|
.
11.4 /
22.6
|
.
166.2 /
300.0
|
| C/AProVE_memory_alloca/svcomp_min_rf_true-alloca.c
|
YES
113.5 /
108.8
|
YES
1.4 /
1.4
|
.
290.1 /
300.1
|
| C/AProVE_memory_alloca/svcomp_mult_array_alloca.c
|
YES
86.5 /
36.8
|
.
3.7 /
3.7
|
YES
70.7 /
129.5
|
| ProVE_memory_alloca/svcomp_openbsd_cbzero_alloca.c
|
.
2.2 /
1.5
|
.
0.4 /
0.5
|
.
166.1 /
300.1
|
| roVE_memory_alloca/svcomp_openbsd_cmemchr_alloca.c
|
.
2.3 /
3.4
|
.
4.2 /
5.1
|
.
188.3 /
300.1
|
| oVE_memory_alloca/svcomp_openbsd_cmemrchr_alloca.c
|
.
2.0 /
3.6
|
.
0.3 /
0.6
|
YES
14.9 /
17.3
|
| roVE_memory_alloca/svcomp_openbsd_cmemset_alloca.c
|
.
2.0 /
1.5
|
.
0.5 /
1.1
|
.
204.9 /
300.0
|
| roVE_memory_alloca/svcomp_openbsd_cstpcpy_alloca.c
|
YES
25.3 /
8.4
|
.
19.0 /
43.4
|
.
326.8 /
300.0
|
| oVE_memory_alloca/svcomp_openbsd_cstpncpy_alloca.c
|
.
2.0 /
1.4
|
.
0.3 /
0.3
|
.
312.9 /
300.0
|
| roVE_memory_alloca/svcomp_openbsd_cstrcat_alloca.c
|
.
10.5 /
8.8
|
.
6.5 /
12.8
|
.
156.9 /
300.0
|
| roVE_memory_alloca/svcomp_openbsd_cstrcmp_alloca.c
|
YES
23.4 /
9.0
|
.
0.5 /
0.5
|
.
154.3 /
300.0
|
| roVE_memory_alloca/svcomp_openbsd_cstrcpy_alloca.c
|
YES
24.0 /
26.6
|
.
19.5 /
43.9
|
.
329.3 /
300.0
|
| oVE_memory_alloca/svcomp_openbsd_cstrcspn_alloca.c
|
.
2.4 /
4.8
|
.
0.3 /
1.1
|
.
154.2 /
300.1
|
| oVE_memory_alloca/svcomp_openbsd_cstrlcpy_alloca.c
|
.
2.0 /
1.4
|
.
0.3 /
0.3
|
YES
67.7 /
100.8
|
| roVE_memory_alloca/svcomp_openbsd_cstrlen_alloca.c
|
.
2.0 /
1.4
|
.
0.2 /
0.3
|
YES
16.4 /
20.5
|
| oVE_memory_alloca/svcomp_openbsd_cstrncat_alloca.c
|
.
2.0 /
3.6
|
.
5.3 /
10.1
|
.
227.1 /
300.0
|
| oVE_memory_alloca/svcomp_openbsd_cstrncmp_alloca.c
|
.
2.0 /
1.4
|
.
0.8 /
1.8
|
.
212.4 /
300.1
|
| oVE_memory_alloca/svcomp_openbsd_cstrncpy_alloca.c
|
.
2.2 /
5.9
|
.
0.5 /
1.3
|
.
218.4 /
300.1
|
| oVE_memory_alloca/svcomp_openbsd_cstrnlen_alloca.c
|
.
2.0 /
1.4
|
.
0.3 /
0.4
|
.
9.0 /
4.7
|
| oVE_memory_alloca/svcomp_openbsd_cstrpbrk_alloca.c
|
.
2.1 /
3.0
|
.
0.5 /
1.6
|
.
161.2 /
300.1
|
| roVE_memory_alloca/svcomp_openbsd_cstrspn_alloca.c
|
.
2.0 /
3.9
|
.
0.1 /
0.3
|
YES
159.7 /
139.2
|
| roVE_memory_alloca/svcomp_openbsd_cstrstr_alloca.c
|
.
2.1 /
1.4
|
.
0.2 /
0.3
|
.
175.2 /
300.0
|
| AProVE_memory_alloca/svcomp_selectionsort_alloca.c
|
.
119.0 /
62.2
|
YES
3.6 /
11.5
|
YES
82.6 /
104.7
|
| C/AProVE_memory_alloca/svcomp_stroeder1_alloca.c
|
.
24.3 /
24.9
|
.
0.3 /
1.4
|
YES
14.4 /
8.1
|
| C/AProVE_memory_alloca/svcomp_stroeder2_alloca.c
|
.
54.2 /
26.2
|
.
0.7 /
2.0
|
YES
20.9 /
12.4
|
| C/AProVE_memory_alloca/svcomp_strreplace_alloca.c
|
YES
54.4 /
23.7
|
.
82.9 /
82.8
|
YES
19.7 /
13.8
|
| C/AProVE_memory_alloca/svcomp_subseq_alloca.c
|
YES
49.7 /
48.3
|
.
27.6 /
27.9
|
.
293.6 /
300.0
|
| C/AProVE_memory_alloca/svcomp_substring_alloca.c
|
YES
54.6 /
32.4
|
.
21.9 /
21.9
|
.
212.5 /
300.1
|
| C/AProVE_memory_alloca/svcomp_twisted-alloca.c
|
YES
6.2 /
10.6
|
.
0.1 /
0.2
|
YES
53.9 /
84.6
|
| C/AProVE_memory_unsafe/svcomp_add_last_unsafe.c
|
.
3.0 /
1.9
|
.
2.2 /
2.8
|
.
10.5 /
13.6
|
| C/AProVE_memory_unsafe/svcomp_bubble_sort_unsafe.c
|
.
3.7 /
2.3
|
.
39.7 /
85.5
|
.
10.4 /
14.9
|
| C/AProVE_memory_unsafe/svcomp_bubblesort_unsafe.c
|
.
4.5 /
4.7
|
.
37.7 /
84.4
|
.
9.4 /
4.8
|
| C/AProVE_memory_unsafe/svcomp_count_down_unsafe.c
|
.
4.0 /
2.2
|
.
2.2 /
4.9
|
.
9.5 /
11.4
|
| C/AProVE_memory_unsafe/svcomp_cstrcat_unsafe.c
|
.
2.5 /
4.4
|
.
6.2 /
6.2
|
.
9.5 /
6.2
|
| C/AProVE_memory_unsafe/svcomp_cstrchr_unsafe.c
|
.
3.9 /
5.4
|
.
43.2 /
65.6
|
.
17.7 /
22.4
|
| C/AProVE_memory_unsafe/svcomp_cstrcpy_unsafe.c
|
.
3.0 /
6.9
|
.
1.7 /
3.5
|
.
11.3 /
13.9
|
| C/AProVE_memory_unsafe/svcomp_cstrlen_unsafe.c
|
.
3.0 /
2.7
|
.
0.3 /
0.8
|
.
13.5 /
8.1
|
| C/AProVE_memory_unsafe/svcomp_cstrncat_unsafe.c
|
.
2.8 /
4.1
|
.
0.6 /
1.2
|
.
10.4 /
14.4
|
| C/AProVE_memory_unsafe/svcomp_cstrncpy_unsafe.c
|
.
4.7 /
6.7
|
.
0.4 /
0.6
|
.
9.3 /
5.4
|
| C/AProVE_memory_unsafe/svcomp_cstrpbrk_unsafe.c
|
.
3.4 /
5.4
|
.
45.4 /
88.0
|
.
124.4 /
118.7
|
| AProVE_memory_unsafe/svcomp_delete_alloca_unsafe.c
|
.
3.9 /
4.4
|
.
0.2 /
0.3
|
.
9.7 /
5.1
|
| C/AProVE_memory_unsafe/svcomp_delete_unsafe.c
|
.
2.5 /
1.7
|
.
0.2 /
0.2
|
.
9.9 /
16.7
|
| C/AProVE_memory_unsafe/svcomp_diff_usafe.c
|
.
5.4 /
2.5
|
.
23.3 /
23.3
|
.
10.7 /
13.4
|
| ProVE_memory_unsafe/svcomp_insertion_sort_unsafe.c
|
.
3.2 /
2.0
|
.
9.6 /
22.7
|
.
9.8 /
10.8
|
| AProVE_memory_unsafe/svcomp_insertionsort_unsafe.c
|
.
3.4 /
11.6
|
.
9.8 /
22.2
|
.
9.0 /
5.1
|
| roVE_memory_unsafe/svcomp_java_BubbleSort_unsafe.c
|
.
3.8 /
6.0
|
.
64.0 /
85.0
|
.
9.5 /
5.3
|
| roVE_memory_unsafe/svcomp_knapsack_alloca_unsafe.c
|
.
9.8 /
4.3
|
.
4.9 /
4.9
|
.
12.0 /
6.2
|
| C/AProVE_memory_unsafe/svcomp_knapsack_unsafe.c
|
.
5.3 /
2.6
|
.
5.3 /
8.5
|
.
21.5 /
16.4
|
| C/AProVE_memory_unsafe/svcomp_lis_unsafe.c
|
.
3.9 /
2.1
|
.
12.6 /
22.6
|
.
14.9 /
21.6
|
| C/AProVE_memory_unsafe/svcomp_mult_array_unsafe.c
|
.
5.0 /
8.5
|
.
4.0 /
7.4
|
.
9.5 /
4.9
|
| memory_unsafe/svcomp_reverse_array_alloca_unsafe.c
|
.
6.3 /
3.0
|
.
124.2 /
200.8
|
.
11.4 /
6.2
|
| AProVE_memory_unsafe/svcomp_reverse_array_unsafe.c
|
.
4.5 /
6.8
|
.
190.1 /
228.8
|
.
10.0 /
5.5
|
| ProVE_memory_unsafe/svcomp_selection_sort_unsafe.c
|
.
3.3 /
5.4
|
.
5.9 /
6.0
|
.
9.4 /
4.9
|
| AProVE_memory_unsafe/svcomp_selectionsort_unsafe.c
|
.
4.6 /
6.8
|
.
6.4 /
9.5
|
.
9.4 /
4.9
|
| C/AProVE_memory_unsafe/svcomp_stroeder1_unsafe.c
|
.
3.0 /
4.7
|
.
0.3 /
0.3
|
.
10.5 /
6.2
|
| C/AProVE_memory_unsafe/svcomp_stroeder2_unsafe.c
|
.
3.2 /
2.0
|
.
0.7 /
2.0
|
.
11.0 /
16.3
|
| C/AProVE_numeric/Avg_true.c
|
YES
12.4 /
12.4
|
YES
0.6 /
1.6
|
YES
15.7 /
8.8
|
| C/AProVE_numeric/Binomial_true.c
|
YES
198.2 /
78.8
|
.
3.6 /
6.6
|
.
204.1 /
300.0
|
| C/AProVE_numeric/Et1_true.c
|
.
20.3 /
16.6
|
YES
0.3 /
0.3
|
YES
10.4 /
5.7
|
| C/AProVE_numeric/Et2_true.c
|
YES
20.6 /
11.7
|
YES
0.4 /
1.3
|
YES
12.7 /
6.7
|
| C/AProVE_numeric/Et3_true.c
|
.
18.9 /
7.7
|
YES
0.3 /
0.3
|
YES
12.7 /
25.7
|
| C/AProVE_numeric/Et4_true.c
|
YES
22.9 /
14.5
|
YES
0.4 /
1.5
|
YES
13.3 /
7.1
|
| C/AProVE_numeric/LeUserDefRec_true.c
|
YES
6.2 /
8.2
|
YES
0.3 /
0.6
|
YES
11.5 /
6.9
|
| C/AProVE_numeric/LogRecursive_true.c
|
.
619.8 /
300.0
|
YES
0.3 /
0.6
|
.
18.0 /
20.5
|
| C/AProVE_numeric/Parts_true.c
|
YES
117.2 /
100.7
|
YES
0.8 /
1.7
|
YES
53.1 /
66.3
|
| C/AProVE_numeric/TerminatorRec02_true.c
|
YES
6.4 /
9.2
|
YES
0.2 /
0.4
|
YES
12.0 /
16.8
|
| C/AProVE_numeric/TwoWay_true.c
|
YES
7.2 /
3.5
|
YES
0.6 /
0.6
|
YES
11.9 /
10.9
|
| C/AProVE_numeric/ex2.c
|
YES
4.8 /
2.7
|
YES
0.2 /
0.5
|
YES
10.9 /
6.0
|
| C/AProVE_numeric/ex3.c
|
YES
6.8 /
10.2
|
YES
0.3 /
0.7
|
YES
33.0 /
68.1
|
| C/AProVE_numeric/rec_counter1.c
|
YES
12.4 /
5.4
|
YES
0.3 /
0.4
|
YES
13.1 /
7.0
|
| C/AProVE_numeric/rec_counter3.c
|
YES
11.0 /
10.9
|
YES
0.4 /
1.2
|
YES
14.9 /
7.8
|
| C/AProVE_numeric/rec_strlen.c
|
YES
7.6 /
3.7
|
.
5.2 /
5.2
|
YES
16.0 /
9.7
|
| _Ackermann01_true-unreach-call_modified_modified.c
|
YES
10.7 /
4.0
|
YES
0.9 /
0.9
|
YES
134.2 /
98.2
|
| on01_true-unreach-call_true-termination_modified.c
|
.
6.8 /
9.0
|
.
0.2 /
1.3
|
YES
12.9 /
14.7
|
| dd01_true-unreach-call_true-termination_modified.c
|
YES
7.6 /
11.3
|
YES
0.3 /
0.4
|
YES
14.4 /
19.5
|
| ic/svcomp_Fibonacci01_true-unreach-call_modified.c
|
YES
14.8 /
8.8
|
YES
0.3 /
0.3
|
YES
37.4 /
36.0
|
| tive_true-unreach-call_true-termination_modified.c
|
YES
7.3 /
8.2
|
YES
0.6 /
0.6
|
YES
15.0 /
9.1
|
| C/AProVE_numeric/svcomp_a.01.c
|
YES
43.4 /
45.6
|
YES
0.3 /
0.3
|
YES
12.1 /
14.8
|
| C/AProVE_numeric/svcomp_a.04.c
|
YES
18.1 /
7.3
|
YES
0.2 /
0.2
|
YES
10.5 /
6.6
|
| C/AProVE_numeric/svcomp_a.05.c
|
YES
19.7 /
8.1
|
YES
0.2 /
0.3
|
YES
10.9 /
33.9
|
| C/AProVE_numeric/svcomp_a.06.c
|
YES
38.7 /
24.6
|
YES
0.2 /
0.2
|
YES
10.8 /
12.2
|
| C/AProVE_numeric/svcomp_a.07.c
|
YES
50.0 /
75.2
|
YES
0.2 /
0.2
|
YES
10.5 /
12.6
|
| C/AProVE_numeric/svcomp_a.08.c
|
YES
22.9 /
8.9
|
YES
0.2 /
0.2
|
YES
10.2 /
13.6
|
| C/AProVE_numeric/svcomp_a.09_assume.c
|
YES
8.3 /
3.8
|
.
0.3 /
0.3
|
YES
10.4 /
5.7
|
| C/AProVE_numeric/svcomp_a.10.c
|
YES
24.5 /
23.6
|
YES
0.3 /
0.3
|
YES
14.5 /
12.0
|
| C/AProVE_numeric/svcomp_b.01.c
|
YES
17.6 /
16.3
|
YES
0.2 /
0.4
|
YES
10.8 /
10.9
|
| C/AProVE_numeric/svcomp_b.02.c
|
YES
33.5 /
15.0
|
YES
0.2 /
0.2
|
YES
11.9 /
20.8
|
| C/AProVE_numeric/svcomp_b.03-no-inv_assume.c
|
YES
7.5 /
5.2
|
YES
0.3 /
1.3
|
YES
11.7 /
13.9
|
| C/AProVE_numeric/svcomp_b.03_assume.c
|
YES
8.0 /
12.4
|
.
0.3 /
0.7
|
YES
9.8 /
5.4
|
| C/AProVE_numeric/svcomp_b.04.c
|
YES
3.2 /
1.9
|
YES
0.2 /
0.4
|
YES
10.7 /
5.8
|
| C/AProVE_numeric/svcomp_b.05.c
|
YES
3.7 /
2.1
|
YES
0.2 /
0.2
|
YES
11.0 /
6.9
|
| C/AProVE_numeric/svcomp_b.06.c
|
YES
24.3 /
10.4
|
YES
0.2 /
0.5
|
YES
10.0 /
5.4
|
| C/AProVE_numeric/svcomp_b.07.c
|
YES
52.8 /
28.0
|
YES
0.2 /
0.5
|
YES
10.5 /
5.7
|
| C/AProVE_numeric/svcomp_b.09-no-inv_assume.c
|
YES
21.2 /
18.7
|
YES
0.7 /
0.7
|
YES
15.5 /
7.6
|
| C/AProVE_numeric/svcomp_b.09_assume.c
|
YES
20.5 /
19.5
|
.
0.7 /
1.9
|
YES
12.3 /
24.7
|
| C/AProVE_numeric/svcomp_b.10.c
|
YES
27.2 /
27.1
|
YES
0.3 /
0.8
|
YES
10.9 /
14.0
|
| C/AProVE_numeric/svcomp_b.11.c
|
YES
50.9 /
41.3
|
YES
0.3 /
0.3
|
YES
12.7 /
16.4
|
| C/AProVE_numeric/svcomp_b.12.c
|
YES
21.1 /
20.1
|
YES
0.3 /
0.3
|
YES
11.0 /
14.3
|
| C/AProVE_numeric/svcomp_b.13.c
|
YES
37.1 /
21.5
|
YES
0.3 /
0.3
|
YES
12.1 /
6.6
|
| C/AProVE_numeric/svcomp_b.14.c
|
YES
18.3 /
7.4
|
YES
0.4 /
0.5
|
YES
11.3 /
5.9
|
| C/AProVE_numeric/svcomp_b.15.c
|
YES
21.9 /
8.5
|
YES
0.4 /
0.5
|
YES
11.4 /
14.3
|
| C/AProVE_numeric/svcomp_b.16.c
|
YES
21.6 /
27.4
|
YES
0.4 /
0.7
|
YES
12.3 /
13.4
|
| C/AProVE_numeric/svcomp_b.17.c
|
YES
40.4 /
17.2
|
YES
0.4 /
0.4
|
YES
11.3 /
6.3
|
| C/AProVE_numeric/svcomp_b.18.c
|
YES
8.7 /
6.1
|
YES
0.4 /
0.5
|
YES
11.4 /
15.1
|
| C/AProVE_numeric/svcomp_c.01-no-inv.c
|
YES
25.4 /
8.1
|
YES
0.6 /
0.6
|
YES
16.1 /
8.3
|
| C/AProVE_numeric/svcomp_c.01_assume.c
|
YES
20.7 /
13.3
|
.
0.6 /
0.6
|
YES
12.3 /
16.7
|
| C/AProVE_numeric/svcomp_c.02.c
|
YES
26.8 /
13.0
|
YES
0.3 /
0.7
|
YES
13.1 /
6.8
|
| C/AProVE_numeric/svcomp_c.03.c
|
YES
44.8 /
18.1
|
YES
0.2 /
0.3
|
YES
12.6 /
7.0
|
| C/AProVE_numeric/svcomp_c.07.c
|
YES
42.7 /
37.8
|
YES
0.2 /
0.5
|
YES
10.4 /
13.6
|
| C/AProVE_numeric/svcomp_c.08.c
|
YES
61.8 /
29.5
|
YES
0.4 /
0.4
|
YES
13.9 /
18.0
|
| C/AProVE_numeric/svcomp_easySum.c
|
YES
24.9 /
22.4
|
YES
0.2 /
0.3
|
YES
10.3 /
13.1
|
| C/AProVE_numeric/svcomp_ex1.c
|
YES
7.2 /
3.6
|
YES
0.4 /
0.5
|
YES
10.3 /
5.3
|
| C/AProVE_numeric/svcomp_ex2.c
|
YES
28.4 /
14.6
|
YES
0.5 /
0.6
|
.
22.6 /
10.1
|
| C/AProVE_numeric/svcomp_ex3a.c
|
YES
9.6 /
4.2
|
YES
0.2 /
0.7
|
.
18.6 /
8.2
|
| C/AProVE_numeric/svcomp_ex3b.c
|
YES
14.5 /
14.5
|
YES
0.2 /
0.3
|
.
21.4 /
22.4
|
| C/AProVE_numeric/svcomp_fermat.c
|
YES
181.7 /
87.9
|
.
30.5 /
36.7
|
.
142.2 /
300.0
|
| C/AProVE_numeric/svcomp_flag.c
|
YES
20.0 /
7.9
|
YES
0.4 /
0.4
|
YES
28.8 /
13.1
|
| cd01_true-unreach-call_true-termination_modified.c
|
YES
7.8 /
8.3
|
YES
0.6 /
1.0
|
YES
13.7 /
7.6
|
| C/AProVE_numeric/svcomp_java_AG313.c
|
YES
17.1 /
16.1
|
YES
0.3 /
0.8
|
YES
10.2 /
12.4
|
| C/AProVE_numeric/svcomp_java_Break.c
|
YES
6.7 /
3.4
|
YES
0.2 /
0.4
|
YES
10.2 /
5.4
|
| C/AProVE_numeric/svcomp_java_Continue1.c
|
YES
11.0 /
11.2
|
YES
0.2 /
0.2
|
YES
10.2 /
5.4
|
| C/AProVE_numeric/svcomp_java_LogBuiltIn.c
|
YES
8.4 /
3.9
|
YES
0.2 /
0.9
|
YES
10.5 /
5.7
|
| C/AProVE_numeric/svcomp_java_Nested.c
|
YES
25.8 /
21.5
|
YES
0.3 /
0.3
|
YES
15.8 /
21.0
|
| C/AProVE_numeric/svcomp_java_Sequence.c
|
YES
10.6 /
18.9
|
YES
0.4 /
1.1
|
YES
10.6 /
5.7
|
| oi02_true-unreach-call_true-termination_modified.c
|
YES
5.5 /
7.5
|
YES
0.3 /
0.6
|
YES
11.5 /
9.1
|
| C/AProVE_numeric/svcomp_twisted.c
|
.
57.4 /
22.3
|
.
0.1 /
0.5
|
YES
11.7 /
9.3
|
| Mixed_Categories/960521-1_1_true-valid-memsafety.c
|
.
6.3 /
7.5
|
.
0.1 /
0.7
|
.
241.0 /
300.1
|
| es/Addition01_true-unreach-call_true-termination.c
|
.
8.4 /
8.3
|
.
0.2 /
0.3
|
YES
12.7 /
7.0
|
| es/BallRajamani-SPIN2000-Fig1_false-unreach-call.c
|
.
3.6 /
2.3
|
.
0.2 /
0.2
|
YES
19.6 /
19.8
|
| ies/EvenOdd01_true-unreach-call_true-termination.c
|
.
5.8 /
6.6
|
YES
0.5 /
0.5
|
YES
14.2 /
15.7
|
| P_Mixed_Categories/Fibonacci01_true-unreach-call.c
|
.
5.1 /
2.6
|
YES
0.3 /
0.5
|
YES
37.8 /
22.1
|
| /McCarthy91_false-unreach-call_false-termination.c
|
.
3.9 /
5.2
|
.
0.1 /
0.1
|
YES
21.1 /
13.2
|
| V-COMP_Mixed_Categories/Primes_true-unreach-call.c
|
.
15.5 /
13.5
|
.
0.3 /
0.3
|
NO
24.1 /
29.3
|
| d_Categories/Problem01_label00_true-unreach-call.c
|
.
507.2 /
300.1
|
.
119.8 /
300.0
|
NO
33.6 /
20.6
|
| d_Categories/Problem02_label00_true-unreach-call.c
|
.
334.4 /
300.1
|
.
183.6 /
300.1
|
.
284.8 /
300.1
|
| d_Categories/Problem03_label00_true-unreach-call.c
|
.
295.9 /
300.0
|
.
132.6 /
300.0
|
.
223.8 /
300.0
|
| d_Categories/Problem04_label00_true-unreach-call.c
|
.
387.4 /
300.0
|
.
135.7 /
300.0
|
.
220.9 /
300.1
|
| _Categories/Problem05_label00_false-unreach-call.c
|
.
2.7 /
300.0
|
.
181.0 /
300.0
|
.
304.6 /
300.1
|
| _Categories/Problem06_label00_false-unreach-call.c
|
.
2.4 /
300.0
|
.
252.9 /
300.1
|
.
302.1 /
300.1
|
| d_Categories/Problem07_label00_true-unreach-call.c
|
.
346.9 /
300.1
|
.
298.1 /
300.0
|
.
330.0 /
300.1
|
| d_Categories/Problem08_label00_true-unreach-call.c
|
.
2.5 /
300.0
|
.
228.9 /
300.0
|
.
325.1 /
300.1
|
| d_Categories/Problem09_label00_true-unreach-call.c
|
.
3.2 /
300.1
|
.
142.5 /
300.0
|
.
353.9 /
300.0
|
| d_Categories/Problem10_label00_true-unreach-call.c
|
.
281.8 /
300.0
|
.
194.1 /
300.0
|
.
187.5 /
189.8
|
| _Categories/Problem11_label00_false-unreach-call.c
|
.
573.1 /
300.0
|
.
174.4 /
300.0
|
.
236.4 /
300.1
|
| _Categories/Problem12_label00_false-unreach-call.c
|
.
261.9 /
300.0
|
.
208.3 /
300.0
|
.
222.2 /
300.0
|
| d_Categories/Problem13_label00_true-unreach-call.c
|
.
374.1 /
300.0
|
.
231.9 /
300.0
|
.
229.6 /
300.0
|
| d_Categories/Problem14_label00_true-unreach-call.c
|
.
239.8 /
300.1
|
.
235.4 /
300.0
|
.
617.1 /
300.0
|
| _Categories/Problem15_label00_false-unreach-call.c
|
.
337.6 /
300.0
|
.
234.1 /
300.0
|
.
282.7 /
300.1
|
| _Categories/Problem16_label00_false-unreach-call.c
|
.
302.2 /
300.1
|
.
235.2 /
300.0
|
.
327.5 /
300.0
|
| d_Categories/Problem17_label00_true-unreach-call.c
|
.
415.7 /
300.0
|
.
220.2 /
300.0
|
.
280.5 /
300.0
|
| _Categories/Problem18_label00_false-unreach-call.c
|
.
480.9 /
300.1
|
.
217.5 /
300.0
|
.
345.0 /
300.0
|
| d_Categories/Problem19_label00_true-unreach-call.c
|
.
322.7 /
300.0
|
.
225.4 /
300.0
|
.
218.6 /
300.0
|
| ed_Categories/afterrec_2calls_false-unreach-call.c
|
.
3.9 /
6.2
|
YES
0.2 /
0.2
|
YES
10.3 /
13.2
|
| ist_cell_true-unreach-call_false-termination.cil.c
|
.
33.3 /
13.5
|
.
0.1 /
0.2
|
.
274.4 /
300.1
|
| d_Categories/bubble_sort_linux_true-unreach-call.c
|
.
2.2 /
1.6
|
.
0.1 /
0.2
|
.
228.4 /
300.1
|
| o_simpl1_false-unreach-call_true-termination.cil.c
|
.
276.8 /
300.0
|
.
0.1 /
0.1
|
YES
20.1 /
12.2
|
| OMP_Mixed_Categories/cs_dekker_true-unreach-call.c
|
.
23.9 /
17.0
|
.
0.1 /
0.4
|
.
24.0 /
37.0
|
| Mixed_Categories/cs_fib_longer_true-unreach-call.c
|
.
2.3 /
4.7
|
.
0.1 /
0.3
|
.
275.3 /
300.1
|
| MP_Mixed_Categories/cs_lamport_true-unreach-call.c
|
.
48.9 /
38.0
|
.
0.1 /
0.5
|
.
22.6 /
11.6
|
| P_Mixed_Categories/cs_peterson_true-unreach-call.c
|
.
16.3 /
21.2
|
.
0.1 /
0.5
|
.
23.0 /
32.5
|
| _Mixed_Categories/cs_stateful_false-unreach-call.c
|
.
11.3 /
11.4
|
.
0.1 /
0.1
|
.
224.9 /
300.0
|
| _Mixed_Categories/cs_szymanski_true-unreach-call.c
|
.
24.5 /
30.4
|
.
0.1 /
0.1
|
.
21.2 /
10.6
|
| d_Categories/cs_time_var_mutex_true-unreach-call.c
|
.
20.6 /
22.3
|
.
0.1 /
0.1
|
.
28.6 /
19.8
|
| uctures_set_multi_proc_false-unreach-call_ground.c
|
.
38.4 /
39.1
|
.
0.2 /
0.9
|
.
231.8 /
300.0
|
| rf_simpl1_true-unreach-call_true-termination.cil.c
|
.
268.0 /
300.0
|
.
0.1 /
0.3
|
YES
16.5 /
22.0
|
| egories/dll_extends_pointer_true-valid-memsafety.c
|
.
2.5 /
1.8
|
.
0.2 /
0.2
|
.
307.6 /
300.1
|
| MP_Mixed_Categories/dll_of_dll_true-unreach-call.c
|
.
2.2 /
1.6
|
.
0.1 /
0.1
|
.
263.5 /
300.1
|
| s/elevator_spec1_product01_true-unreach-call.cil.c
|
.
2.4 /
1.7
|
.
0.1 /
0.1
|
.
222.2 /
300.1
|
| ries/email_spec0_product05_true-unreach-call.cil.c
|
.
2.7 /
4.5
|
.
0.1 /
0.2
|
YES
30.0 /
31.6
|
| ixed_Categories/fibo_2calls_2_false-unreach-call.c
|
YES
3.3 /
2.0
|
YES
0.3 /
0.7
|
YES
11.5 /
14.9
|
| -COMP_Mixed_Categories/fibo_5_false-unreach-call.c
|
YES
10.6 /
4.2
|
YES
0.2 /
0.5
|
YES
16.6 /
21.1
|
| y_simpl3_false-unreach-call_true-termination.cil.c
|
.
307.8 /
300.0
|
.
0.1 /
0.2
|
YES
16.8 /
9.6
|
| egories/gcd01_true-unreach-call_true-termination.c
|
YES
8.9 /
3.8
|
YES
0.7 /
1.3
|
YES
14.0 /
7.5
|
| OMP_Mixed_Categories/id2_b2_o3_true-unreach-call.c
|
.
350.2 /
300.1
|
NO
0.4 /
1.1
|
NO
10.8 /
13.2
|
| P_Mixed_Categories/id_i10_o10_false-unreach-call.c
|
YES
6.2 /
6.3
|
YES
0.2 /
0.2
|
YES
11.4 /
13.3
|
| tr_simpl1_true-unreach-call_true-termination.cil.c
|
.
580.3 /
300.0
|
.
0.1 /
0.1
|
YES
13.1 /
17.8
|
| Mixed_Categories/list-ext_1_true-valid-memsafety.c
|
.
2.9 /
5.5
|
.
0.1 /
0.1
|
.
227.9 /
300.1
|
| /SV-COMP_Mixed_Categories/list_true-unreach-call.c
|
.
2.6 /
1.7
|
.
0.1 /
0.3
|
.
225.6 /
300.0
|
| xed_Categories/lockfree-3.0_true-valid-memsafety.c
|
.
2.2 /
1.6
|
.
0.1 /
0.2
|
.
223.8 /
300.0
|
| ve_tlm.1_true-unreach-call_false-termination.cil.c
|
.
296.5 /
300.1
|
.
0.1 /
0.3
|
NO
128.6 /
97.4
|
| MP_Mixed_Categories/merge_sort_true-unreach-call.c
|
.
2.3 /
1.6
|
.
0.1 /
0.2
|
.
191.0 /
300.0
|
| s/minepump_spec1_product01_true-unreach-call.cil.c
|
.
2.4 /
1.7
|
.
0.1 /
0.4
|
NO
13.7 /
7.3
|
| Standby_false-unreach-call.1.ufo.BOUNDED-10.pals.c
|
.
2.6 /
3.3
|
.
0.1 /
0.2
|
.
8.8 /
10.1
|
| licated_false-unreach-call.1.ufo.BOUNDED-10.pals.c
|
.
2.5 /
2.1
|
.
0.1 /
0.3
|
.
9.0 /
6.7
|
| oodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c
|
.
2.3 /
1.7
|
.
0.1 /
0.1
|
YES
16.4 /
20.1
|
| odmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c
|
.
2.5 /
4.2
|
.
0.2 /
0.2
|
.
344.2 /
300.0
|
| t-time.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c
|
.
2.3 /
1.6
|
.
0.1 /
0.2
|
.
9.5 /
5.8
|
| -time.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c
|
.
2.5 /
6.3
|
.
0.1 /
0.2
|
.
8.3 /
4.4
|
| ls_lcr.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c
|
.
2.2 /
3.8
|
.
0.1 /
0.4
|
.
8.3 /
4.4
|
| s_lcr.8_false-unreach-call.1.ufo.BOUNDED-16.pals.c
|
.
2.3 /
4.2
|
.
0.1 /
0.5
|
.
10.6 /
6.5
|
| oodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c
|
.
2.4 /
1.6
|
.
0.1 /
0.1
|
YES
50.8 /
33.4
|
| odmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c
|
.
2.8 /
5.1
|
.
0.1 /
0.1
|
YES
72.0 /
48.6
|
| sfifo_1_false-unreach-call_false-termination.cil.c
|
.
6.5 /
9.3
|
.
0.1 /
0.1
|
NO
19.8 /
29.6
|
| es/recHanoi01_true-unreach-call_true-termination.c
|
.
4.8 /
11.2
|
YES
0.6 /
1.2
|
YES
42.2 /
34.5
|
| ed_Categories/rekcba_aso_false-unreach-call.1.M1.c
|
.
2.3 /
4.3
|
.
0.2 /
0.4
|
.
12.0 /
17.8
|
| Mixed_Categories/rekcba_ctm_false-unreach-call.2.c
|
.
298.9 /
149.3
|
.
0.4 /
0.4
|
.
452.7 /
300.0
|
| ed_Categories/rekcba_nxt_false-unreach-call.1.M1.c
|
.
2.3 /
4.3
|
.
0.2 /
0.5
|
.
10.4 /
12.3
|
| ixed_Categories/s3_clnt_1_false-unreach-call.cil.c
|
.
375.2 /
300.1
|
.
0.1 /
0.1
|
YES
47.9 /
61.7
|
| xed_Categories/s3_srvr_14_false-unreach-call.cil.c
|
.
542.3 /
300.0
|
.
0.1 /
0.4
|
NO
53.4 /
36.8
|
| ixed_Categories/s3_srvr_1_false-unreach-call.cil.c
|
.
259.8 /
300.1
|
.
0.1 /
0.1
|
NO
39.5 /
25.6
|
| ategories/sanfoundry_02_true-unreach-call_ground.c
|
.
77.3 /
65.3
|
.
0.5 /
0.5
|
.
287.9 /
300.0
|
| xed_Categories/simple-ext_1_true-valid-memsafety.c
|
.
2.6 /
1.7
|
.
0.1 /
0.1
|
.
173.8 /
300.1
|
| ed_Categories/skiplist_3lvl_true-valid-memsafety.c
|
.
2.3 /
3.4
|
.
0.1 /
0.1
|
.
154.2 /
300.0
|
| ixed_Categories/sll_to_dll_rev_true-unreach-call.c
|
.
2.2 /
1.7
|
.
0.1 /
0.1
|
.
176.6 /
300.0
|
| ries/sorting_bubblesort_true-unreach-call_ground.c
|
.
33.9 /
21.9
|
.
0.4 /
0.4
|
.
215.4 /
300.1
|
| V-COMP_Mixed_Categories/splice_true-unreach-call.c
|
.
2.8 /
1.8
|
.
0.1 /
0.1
|
.
229.8 /
300.1
|
| gories/standard_compare_true-unreach-call_ground.c
|
.
31.7 /
28.6
|
.
240.9 /
300.0
|
.
315.8 /
300.0
|
| tegories/standard_copy7_true-unreach-call_ground.c
|
.
45.9 /
18.6
|
.
246.3 /
300.0
|
.
279.3 /
300.0
|
| ories/standard_password_true-unreach-call_ground.c
|
.
29.9 /
30.7
|
.
246.6 /
300.0
|
.
338.9 /
300.0
|
| xed_Categories/stateful_check_false-unreach-call.c
|
.
2.0 /
1.4
|
.
105.3 /
52.7
|
NO
11.9 /
12.5
|
| COMP_Mixed_Categories/sum_2x3_false-unreach-call.c
|
YES
5.4 /
3.0
|
YES
0.2 /
1.0
|
YES
10.5 /
5.7
|
| P_Mixed_Categories/sum_non_eq_false-unreach-call.c
|
.
788.9 /
300.0
|
.
0.5 /
0.5
|
NO
10.4 /
12.8
|
| _Mixed_Categories/test-0134_true-valid-memsafety.c
|
.
2.2 /
4.0
|
.
0.1 /
0.1
|
.
313.3 /
300.0
|
| _Mixed_Categories/test-0219_true-valid-memsafety.c
|
.
2.2 /
1.5
|
.
0.1 /
0.1
|
.
144.3 /
300.0
|
| _Mixed_Categories/test-0234_true-valid-memsafety.c
|
.
2.2 /
3.7
|
.
0.1 /
0.1
|
.
247.9 /
300.0
|
| ixed_Categories/test-0513_1_true-valid-memsafety.c
|
.
3.5 /
2.4
|
.
0.1 /
0.2
|
.
168.5 /
300.0
|
| _Mixed_Categories/test-0521_true-valid-memsafety.c
|
.
7.0 /
10.2
|
.
0.1 /
0.1
|
.
226.7 /
300.1
|
| est_locks_15_true-unreach-call_false-termination.c
|
.
610.1 /
300.0
|
.
0.1 /
0.1
|
NO
177.2 /
161.7
|
| ring.01_false-unreach-call_false-termination.cil.c
|
.
294.2 /
300.0
|
.
0.1 /
0.1
|
NO
216.0 /
214.5
|
| ring.05_false-unreach-call_false-termination.cil.c
|
.
447.7 /
300.1
|
.
0.1 /
0.8
|
.
155.5 /
300.0
|
| ring.10_false-unreach-call_false-termination.cil.c
|
.
263.0 /
300.0
|
.
0.1 /
0.1
|
.
336.4 /
300.0
|
| ring.15_false-unreach-call_false-termination.cil.c
|
.
532.3 /
300.1
|
.
0.1 /
1.0
|
.
238.3 /
300.0
|
| tter.01_false-unreach-call_false-termination.cil.c
|
.
314.3 /
300.0
|
.
0.1 /
0.4
|
NO
89.6 /
99.6
|
| tter.06_false-unreach-call_false-termination.cil.c
|
.
402.8 /
300.0
|
.
0.1 /
0.2
|
.
229.3 /
300.0
|
| tter.11_false-unreach-call_false-termination.cil.c
|
.
461.5 /
300.1
|
.
0.1 /
0.1
|
.
253.5 /
300.0
|
| tter.16_false-unreach-call_false-termination.cil.c
|
.
357.5 /
300.0
|
.
0.1 /
0.1
|
.
246.6 /
300.1
|
| Mixed_Categories/tree_stack_true-valid-memsafety.c
|
.
2.9 /
6.2
|
.
0.1 /
0.1
|
.
175.5 /
300.1
|
| teFeautrierGonnord-SAS2010-Fig1_true-termination.c
|
YES
57.8 /
35.7
|
YES
0.7 /
1.4
|
YES
14.6 /
17.0
|
| eFeautrierGonnord-SAS2010-Fig2a_true-termination.c
|
YES
48.8 /
55.6
|
YES
0.5 /
0.5
|
YES
12.3 /
6.4
|
| eFeautrierGonnord-SAS2010-Fig2b_true-termination.c
|
.
573.0 /
300.0
|
YES
1.5 /
1.9
|
YES
16.0 /
9.7
|
| rierGonnord-SAS2010-counterex1a_true-termination.c
|
YES
39.8 /
18.4
|
.
45.9 /
54.0
|
YES
18.2 /
27.2
|
| rierGonnord-SAS2010-counterex1b_true-termination.c
|
.
127.6 /
46.9
|
YES
0.8 /
0.9
|
YES
14.6 /
14.6
|
| eautrierGonnord-SAS2010-cousot9_true-termination.c
|
YES
11.6 /
4.4
|
YES
0.3 /
0.8
|
YES
13.4 /
14.1
|
| eFeautrierGonnord-SAS2010-ndecr_true-termination.c
|
YES
5.3 /
6.2
|
YES
0.2 /
0.5
|
YES
12.0 /
19.8
|
| trierGonnord-SAS2010-nestedLoop_true-termination.c
|
.
69.7 /
26.8
|
YES
1.0 /
2.0
|
YES
15.7 /
19.4
|
| autrierGonnord-SAS2010-random1d_true-termination.c
|
YES
36.3 /
11.9
|
YES
0.3 /
0.6
|
YES
10.8 /
14.6
|
| rteFeautrierGonnord-SAS2010-rsd_true-termination.c
|
.
376.9 /
300.0
|
YES
0.6 /
1.1
|
YES
13.6 /
19.6
|
| trierGonnord-SAS2010-speedpldi2_true-termination.c
|
YES
23.7 /
22.6
|
.
3.6 /
7.0
|
YES
14.0 /
8.0
|
| trierGonnord-SAS2010-speedpldi3_true-termination.c
|
YES
32.5 /
31.5
|
YES
0.3 /
0.3
|
YES
13.5 /
19.5
|
| trierGonnord-SAS2010-speedpldi4_true-termination.c
|
YES
12.4 /
5.3
|
YES
0.3 /
0.3
|
YES
11.7 /
14.0
|
| utrierGonnord-SAS2010-terminate_true-termination.c
|
YES
14.0 /
12.0
|
YES
0.2 /
0.2
|
YES
10.8 /
14.3
|
| eFeautrierGonnord-SAS2010-wcet2_true-termination.c
|
YES
11.9 /
5.3
|
YES
0.4 /
0.4
|
YES
12.4 /
15.9
|
| FeautrierGonnord-SAS2010-while2_true-termination.c
|
YES
10.3 /
10.0
|
YES
0.3 /
0.3
|
YES
11.9 /
6.3
|
| teFeautrierGonnord-SAS2010-wise_true-termination.c
|
YES
15.2 /
14.9
|
YES
0.3 /
0.3
|
YES
13.1 /
6.6
|
| Category/Avery-FLOPS2006-Table1_true-termination.c
|
YES
72.8 /
45.4
|
YES
0.3 /
0.4
|
YES
11.2 /
14.4
|
| nnaSipma-CAV2005-Fig1-modified_false-termination.c
|
.
261.5 /
300.1
|
NO
0.5 /
0.6
|
NO
10.3 /
5.4
|
| /BradleyMannaSipma-CAV2005-Fig1_true-termination.c
|
YES
31.1 /
9.9
|
YES
0.4 /
0.5
|
YES
17.4 /
10.9
|
| radleyMannaSipma-ICALP2005-Fig1_true-termination.c
|
.
329.6 /
300.0
|
YES
47.6 /
47.5
|
YES
15.4 /
8.4
|
| lwaniSagivYang-ESOP2008-aaron12_true-termination.c
|
.
524.6 /
300.0
|
YES
20.9 /
31.1
|
.
21.0 /
21.1
|
| ulwaniSagivYang-ESOP2008-aaron1_true-termination.c
|
YES
31.3 /
43.1
|
YES
0.6 /
0.6
|
YES
12.5 /
15.2
|
| ulwaniSagivYang-ESOP2008-aaron4_true-termination.c
|
.
98.6 /
75.3
|
YES
1.7 /
2.9
|
YES
14.9 /
21.9
|
| ulwaniSagivYang-ESOP2008-aaron6_true-termination.c
|
.
600.1 /
300.1
|
YES
0.6 /
1.0
|
YES
11.4 /
7.0
|
| waniSagivYang-ESOP2008-random1d_true-termination.c
|
YES
33.4 /
11.2
|
YES
0.3 /
0.5
|
YES
10.1 /
8.8
|
| FlurMukhopadhyay-SAS2012-Ex1.02_true-termination.c
|
YES
7.8 /
3.8
|
YES
0.3 /
1.1
|
YES
11.5 /
7.0
|
| FlurMukhopadhyay-SAS2012-Ex1.03_true-termination.c
|
.
3.1 /
5.2
|
YES
0.2 /
0.2
|
YES
11.5 /
6.9
|
| FlurMukhopadhyay-SAS2012-Ex1.04_true-termination.c
|
YES
6.3 /
7.5
|
YES
0.2 /
1.0
|
YES
11.2 /
6.9
|
| FlurMukhopadhyay-SAS2012-Ex1.05_true-termination.c
|
YES
5.7 /
6.7
|
YES
0.2 /
0.4
|
YES
11.6 /
17.2
|
| FlurMukhopadhyay-SAS2012-Ex2.01_true-termination.c
|
YES
11.6 /
4.6
|
YES
0.2 /
0.2
|
YES
10.0 /
5.5
|
| lurMukhopadhyay-SAS2012-Ex2.02_false-termination.c
|
.
460.9 /
300.1
|
NO
0.9 /
1.5
|
.
20.9 /
22.7
|
| lurMukhopadhyay-SAS2012-Ex2.05_false-termination.c
|
NO
6.9 /
9.2
|
NO
1.5 /
1.8
|
NO
11.6 /
14.5
|
| FlurMukhopadhyay-SAS2012-Ex2.07_true-termination.c
|
YES
9.3 /
3.8
|
YES
0.3 /
0.9
|
YES
10.9 /
17.1
|
| FlurMukhopadhyay-SAS2012-Ex2.08_true-termination.c
|
YES
15.0 /
6.4
|
YES
0.2 /
0.2
|
YES
11.7 /
19.0
|
| FlurMukhopadhyay-SAS2012-Ex2.10_true-termination.c
|
YES
6.8 /
5.8
|
YES
0.2 /
0.5
|
YES
11.1 /
5.7
|
| FlurMukhopadhyay-SAS2012-Ex2.13_true-termination.c
|
YES
14.1 /
6.0
|
YES
0.2 /
0.6
|
YES
9.8 /
9.3
|
| FlurMukhopadhyay-SAS2012-Ex2.16_true-termination.c
|
YES
5.0 /
2.7
|
YES
0.2 /
0.2
|
YES
10.2 /
15.2
|
| lurMukhopadhyay-SAS2012-Ex2.17_false-termination.c
|
.
535.7 /
300.1
|
NO
0.5 /
1.1
|
NO
9.5 /
12.4
|
| FlurMukhopadhyay-SAS2012-Ex2.20_true-termination.c
|
YES
7.2 /
11.7
|
YES
0.2 /
0.5
|
YES
10.0 /
9.1
|
| FlurMukhopadhyay-SAS2012-Ex2.22_true-termination.c
|
YES
4.2 /
5.3
|
YES
0.3 /
0.6
|
YES
10.4 /
5.5
|
| FlurMukhopadhyay-SAS2012-Ex3.01_true-termination.c
|
YES
7.4 /
6.2
|
YES
0.2 /
0.4
|
YES
12.3 /
7.8
|
| FlurMukhopadhyay-SAS2012-Ex3.03_true-termination.c
|
YES
33.6 /
12.9
|
YES
0.5 /
0.5
|
YES
11.6 /
7.2
|
| FlurMukhopadhyay-SAS2012-Ex3.04_true-termination.c
|
YES
21.9 /
8.9
|
YES
0.3 /
1.0
|
YES
10.6 /
5.6
|
| FlurMukhopadhyay-SAS2012-Ex3.05_true-termination.c
|
YES
21.3 /
7.7
|
YES
0.4 /
2.0
|
YES
10.0 /
5.9
|
| FlurMukhopadhyay-SAS2012-Ex3.08_true-termination.c
|
YES
15.5 /
15.2
|
YES
0.2 /
0.5
|
YES
10.5 /
13.7
|
| FlurMukhopadhyay-SAS2012-Ex3.09_true-termination.c
|
YES
11.4 /
5.0
|
YES
0.3 /
0.7
|
YES
10.5 /
11.6
|
| FlurMukhopadhyay-SAS2012-Ex4.01_true-termination.c
|
YES
22.3 /
21.3
|
YES
0.7 /
0.7
|
YES
11.0 /
5.7
|
| y/CookSeeZuleger-TACAS2013-Fig1_true-termination.c
|
YES
17.5 /
15.1
|
YES
0.3 /
0.3
|
YES
12.5 /
6.8
|
| /CookSeeZuleger-TACAS2013-Fig7a_true-termination.c
|
YES
33.8 /
11.1
|
YES
0.4 /
0.7
|
YES
14.0 /
20.3
|
| /CookSeeZuleger-TACAS2013-Fig7b_true-termination.c
|
YES
70.2 /
24.7
|
YES
0.5 /
1.0
|
YES
14.4 /
18.8
|
| egory/GopanReps-CAV2006-Fig1a_true-termination.c.c
|
YES
10.1 /
7.6
|
YES
0.3 /
0.3
|
YES
14.4 /
21.0
|
| lwaniJainKoskinen-PLDI2009-Fig1_true-termination.c
|
.
15.2 /
6.4
|
.
12.8 /
12.9
|
.
274.9 /
300.0
|
| risLalNoriRajamani-SAS2010-Fig1_true-termination.c
|
YES
84.0 /
32.9
|
YES
1.4 /
2.9
|
YES
19.4 /
29.7
|
| isLalNoriRajamani-SAS2010-Fig2_false-termination.c
|
NO
102.7 /
53.2
|
NO
9.1 /
9.0
|
NO
10.1 /
5.4
|
| risLalNoriRajamani-SAS2010-Fig3_true-termination.c
|
YES
9.1 /
3.9
|
YES
0.2 /
0.2
|
YES
11.2 /
5.9
|
| ickeLeikePodelski-ATVA2013-Fig2_true-termination.c
|
.
10.5 /
13.3
|
.
0.6 /
1.2
|
.
20.2 /
10.0
|
| ickeLeikePodelski-ATVA2013-Fig5_true-termination.c
|
YES
6.0 /
3.2
|
YES
0.3 /
0.7
|
.
26.3 /
12.4
|
| ickeLeikePodelski-ATVA2013-Fig6_true-termination.c
|
YES
6.4 /
9.7
|
YES
0.3 /
0.3
|
YES
12.1 /
7.4
|
| ickeLeikePodelski-ATVA2013-Fig7_true-termination.c
|
YES
18.9 /
7.6
|
.
0.1 /
0.1
|
.
8.8 /
4.9
|
| ickeLeikePodelski-ATVA2013-Fig8_true-termination.c
|
.
8.4 /
3.6
|
YES
0.3 /
0.5
|
.
15.5 /
9.0
|
| ickeLeikePodelski-ATVA2013-Fig9_true-termination.c
|
.
9.7 /
8.4
|
YES
0.3 /
0.7
|
.
15.5 /
7.3
|
| rSutre-POPL2002-LockingExample_false-termination.c
|
.
335.6 /
300.1
|
NO
1.9 /
3.6
|
NO
12.4 /
15.4
|
| itovichWintersteiger-CAV2010-Ex_true-termination.c
|
YES
16.7 /
5.7
|
YES
0.2 /
0.2
|
YES
11.2 /
19.5
|
| ovichWintersteiger-CAV2010-Fig1_true-termination.c
|
.
575.5 /
300.0
|
YES
5.5 /
2.8
|
YES
12.5 /
15.3
|
| C/SV-COMP_Termination_Category/LICENSE.txt
|
.
2.1 /
1.5
|
.
0.1 /
0.1
|
.
7.9 /
9.3
|
| z-CarbonellRubio-FMCAD2013-Fig1_true-termination.c
|
.
459.8 /
300.0
|
YES
6.4 /
11.2
|
YES
15.8 /
13.5
|
| /LeeJonesBen-Amram-POPL2001-Ex1_true-termination.c
|
YES
6.5 /
8.6
|
YES
0.2 /
0.4
|
YES
19.2 /
20.4
|
| /LeeJonesBen-Amram-POPL2001-Ex2_true-termination.c
|
YES
7.4 /
3.6
|
YES
0.3 /
1.2
|
YES
19.5 /
8.9
|
| /LeeJonesBen-Amram-POPL2001-Ex3_true-termination.c
|
YES
7.1 /
6.7
|
YES
0.6 /
0.6
|
YES
49.5 /
54.2
|
| /LeeJonesBen-Amram-POPL2001-Ex4_true-termination.c
|
YES
7.8 /
4.0
|
YES
0.8 /
0.8
|
YES
22.4 /
26.6
|
| /LeeJonesBen-Amram-POPL2001-Ex5_true-termination.c
|
YES
6.7 /
6.6
|
YES
0.4 /
0.4
|
.
106.3 /
94.8
|
| /LeeJonesBen-Amram-POPL2001-Ex6_true-termination.c
|
YES
9.1 /
6.1
|
YES
20.5 /
45.2
|
YES
14.4 /
8.1
|
| ory/LeikeHeizmann-TACAS2014-Ex9_true-termination.c
|
YES
9.3 /
5.3
|
YES
0.3 /
1.2
|
YES
12.6 /
7.9
|
| egory/LeikeHeizmann-WST2014-Ex9_true-termination.c
|
.
3.7 /
5.5
|
YES
0.2 /
0.3
|
YES
10.2 /
12.7
|
| _Category/Masse-VMCAI2014-Fig1b_true-termination.c
|
.
215.9 /
300.0
|
.
21.0 /
21.0
|
.
18.1 /
8.5
|
| delskiRybalchenko-LICS2004-Fig2_true-termination.c
|
.
475.6 /
300.1
|
.
33.7 /
45.9
|
.
370.4 /
300.1
|
| elskiRybalchenko-TACAS2011-Fig4_true-termination.c
|
YES
16.5 /
20.7
|
YES
0.3 /
0.3
|
YES
13.1 /
6.9
|
| delskiRybalchenko-VMCAI2004-Ex1_true-termination.c
|
YES
22.0 /
19.4
|
YES
0.4 /
0.9
|
YES
17.3 /
22.8
|
| C/SV-COMP_Termination_Category/README.txt
|
.
2.1 /
4.5
|
.
0.1 /
0.1
|
.
9.1 /
10.0
|
| n_Category/TelAviv-Amir-Minimum_true-termination.c
|
.
319.4 /
300.1
|
YES
0.5 /
1.3
|
YES
16.0 /
19.5
|
| ategory/Toulouse-BranchesToLoop_true-termination.c
|
YES
11.5 /
13.5
|
YES
0.3 /
0.7
|
YES
11.8 /
14.0
|
| ry/Toulouse-MultiBranchesToLoop_true-termination.c
|
YES
13.0 /
14.9
|
YES
1.0 /
2.1
|
YES
14.0 /
15.2
|
| ategory/UrbanMine-ESOP2014-Fig3_true-termination.c
|
YES
66.6 /
30.7
|
YES
0.5 /
0.9
|
YES
16.0 /
25.6
|
| OMP_Termination_Category/aaron2_true-termination.c
|
YES
30.3 /
14.7
|
YES
0.3 /
0.3
|
YES
10.7 /
6.6
|
| OMP_Termination_Category/aaron3_true-termination.c
|
.
367.1 /
300.1
|
.
19.3 /
21.0
|
YES
14.3 /
17.0
|
| COMP_Termination_Category/aviad_true-termination.c
|
.
23.6 /
47.1
|
YES
0.4 /
0.4
|
YES
12.9 /
35.4
|
| -COMP_Termination_Category/gcd1_true-termination.c
|
YES
48.9 /
24.7
|
YES
0.5 /
0.5
|
YES
13.4 /
17.5
|
| OMP_Termination_Category/genady_true-termination.c
|
YES
24.7 /
10.0
|
YES
0.2 /
0.4
|
YES
10.1 /
5.5
|
| COMP_Termination_Category/joey_false-termination.c
|
.
6.0 /
6.8
|
NO
0.7 /
1.4
|
NO
17.9 /
22.0
|
| OMP_Termination_Category/min_rf_true-termination.c
|
YES
111.1 /
46.5
|
YES
0.5 /
0.5
|
YES
15.2 /
18.9
|
| ination_Category/svcomp_cstrcmp_true-termination.c
|
.
13.3 /
4.9
|
.
23.1 /
24.0
|
.
156.4 /
300.0
|
| nation_Category/svcomp_cstrcspn_true-termination.c
|
.
56.8 /
22.2
|
.
0.3 /
0.3
|
.
146.8 /
300.1
|
| ination_Category/svcomp_cstrlen_true-termination.c
|
.
5.2 /
2.7
|
.
0.2 /
0.3
|
YES
16.1 /
9.4
|
| nation_Category/svcomp_cstrncmp_true-termination.c
|
.
18.2 /
7.0
|
.
1.1 /
1.1
|
.
96.8 /
300.0
|
| nation_Category/svcomp_cstrpbrk_true-termination.c
|
.
35.4 /
30.7
|
.
43.6 /
44.8
|
.
241.2 /
300.0
|
| ination_Category/svcomp_cstrspn_true-termination.c
|
.
36.6 /
14.1
|
.
0.3 /
0.5
|
.
291.7 /
300.0
|
| mination_Category/svcomp_strchr_true-termination.c
|
.
9.3 /
11.8
|
.
41.7 /
41.6
|
YES
18.0 /
12.4
|
| C/Ton_Chanh_15/Ackermann_false-termination.c
|
.
481.9 /
300.0
|
NO
0.7 /
0.9
|
NO
11.9 /
6.6
|
| C/Ton_Chanh_15/Ackermann_true-termination.c
|
YES
8.5 /
3.8
|
YES
0.7 /
1.3
|
.
249.2 /
300.1
|
| C/Ton_Chanh_15/Binary_Search_true-termination.c
|
.
8.9 /
3.8
|
YES
0.3 /
0.4
|
NO
14.3 /
13.1
|
| n_Chanh_15/McCarthy91_Recursion_true-termination.c
|
.
6.7 /
2.8
|
YES
0.4 /
0.4
|
YES
21.9 /
26.9
|
| on_Chanh_15/MutualRecursion_1a_false-termination.c
|
.
5.1 /
2.6
|
NO
0.3 /
1.0
|
NO
13.8 /
9.1
|
| Ton_Chanh_15/MutualRecursion_1b_true-termination.c
|
.
23.3 /
16.5
|
YES
0.2 /
0.2
|
YES
42.9 /
27.3
|
| on_Chanh_15/NestedRecursion_1a_false-termination.c
|
.
207.2 /
300.0
|
NO
0.3 /
0.4
|
NO
10.5 /
5.9
|
| Ton_Chanh_15/NestedRecursion_1b_true-termination.c
|
.
291.0 /
300.1
|
YES
0.3 /
0.3
|
YES
32.9 /
18.0
|
| Ton_Chanh_15/NestedRecursion_1c_true-termination.c
|
YES
5.5 /
8.3
|
YES
0.4 /
0.4
|
YES
13.5 /
16.2
|
| Ton_Chanh_15/NestedRecursion_1d_true-termination.c
|
YES
7.0 /
3.0
|
YES
0.3 /
0.8
|
YES
35.4 /
32.2
|
| on_Chanh_15/NestedRecursion_2a_false-termination.c
|
.
5.2 /
3.1
|
NO
0.2 /
0.3
|
NO
9.5 /
5.0
|
| on_Chanh_15/NestedRecursion_2b_false-termination.c
|
.
4.7 /
2.5
|
NO
0.3 /
2.0
|
NO
14.6 /
17.3
|
| Ton_Chanh_15/NestedRecursion_2c_true-termination.c
|
YES
5.4 /
10.6
|
YES
0.3 /
1.3
|
YES
23.2 /
12.1
|
| C/Ultimate/4BitCounterPointer_true-termination.c
|
YES
5.3 /
7.9
|
YES
1.6 /
1.6
|
YES
114.3 /
111.5
|
| ays01-EquivalentConstantIndices_true-termination.c
|
YES
3.9 /
2.4
|
.
243.9 /
300.0
|
YES
10.5 /
5.5
|
| ys02-EquivalentConstantIndices_false-termination.c
|
NO
3.5 /
2.2
|
.
228.1 /
300.0
|
.
11.6 /
5.9
|
| ate/Arrays03-ValueRestictsIndex_true-termination.c
|
.
8.2 /
11.1
|
.
170.1 /
300.1
|
.
18.9 /
26.5
|
| C/Ultimate/Bangalore_true-termination.c
|
YES
6.1 /
20.2
|
YES
0.2 /
0.4
|
YES
10.9 /
11.0
|
| C/Ultimate/Cairo_true-termination.c
|
YES
6.2 /
8.1
|
YES
0.2 /
0.5
|
YES
11.0 /
5.8
|
| C/Ultimate/Collatz_unknown-termination.c
|
.
358.7 /
300.0
|
.
149.1 /
300.0
|
.
24.6 /
35.0
|
| C/Ultimate/Division_false-termination.c
|
NO
4.7 /
6.4
|
NO
0.2 /
0.6
|
NO
10.5 /
12.7
|
| C/Ultimate/Gothenburg_true-termination.c
|
YES
33.9 /
35.6
|
.
5.0 /
6.2
|
YES
20.1 /
30.5
|
| C/Ultimate/LICENSE.txt
|
.
2.0 /
1.4
|
.
0.1 /
0.1
|
.
8.3 /
4.2
|
| C/Ultimate/LexIndexValue-Array_true-termination.c
|
.
7.4 /
2.9
|
.
277.4 /
300.0
|
.
275.3 /
300.1
|
| /Ultimate/LexIndexValue-Pointer_true-termination.c
|
.
8.3 /
3.9
|
.
0.3 /
1.2
|
.
292.7 /
300.1
|
| timate/Lobnya-Boolean-Reordered_true-termination.c
|
YES
5.7 /
3.1
|
YES
0.3 /
0.7
|
YES
30.0 /
30.1
|
| C/Ultimate/Madrid_false-termination.c
|
NO
2.9 /
5.5
|
NO
0.1 /
0.3
|
NO
10.6 /
8.3
|
| C/Ultimate/Mysore_true-termination.c
|
YES
15.1 /
5.4
|
YES
0.5 /
2.0
|
YES
10.5 /
13.4
|
| C/Ultimate/NonTermination2_false-termination.c
|
.
644.7 /
300.1
|
NO
0.2 /
0.2
|
NO
9.5 /
5.1
|
| C/Ultimate/NonTermination3_false-termination.c
|
.
3.0 /
5.3
|
.
300.0 /
300.0
|
.
9.4 /
4.9
|
| Ultimate/NonTerminationSimple2_false-termination.c
|
NO
3.3 /
6.0
|
NO
0.2 /
0.5
|
NO
9.7 /
6.3
|
| Ultimate/NonTerminationSimple3_false-termination.c
|
NO
4.6 /
3.0
|
NO
0.2 /
0.2
|
NO
11.2 /
19.0
|
| Ultimate/NonTerminationSimple4_false-termination.c
|
NO
6.0 /
6.5
|
NO
0.2 /
0.9
|
NO
9.8 /
5.3
|
| Ultimate/NonTerminationSimple5_false-termination.c
|
.
261.4 /
300.0
|
NO
0.2 /
0.3
|
NO
12.4 /
6.7
|
| Ultimate/NonTerminationSimple6_false-termination.c
|
NO
4.3 /
8.1
|
NO
0.2 /
0.4
|
NO
9.8 /
6.4
|
| Ultimate/NonTerminationSimple7_false-termination.c
|
NO
3.5 /
4.9
|
NO
0.2 /
0.2
|
NO
10.0 /
6.2
|
| Ultimate/NonTerminationSimple8_false-termination.c
|
.
325.8 /
300.1
|
NO
0.5 /
0.9
|
NO
9.8 /
12.2
|
| Ultimate/NonTerminationSimple9_false-termination.c
|
NO
3.5 /
2.3
|
NO
0.2 /
0.6
|
NO
9.4 /
4.9
|
| C/Ultimate/Nyala-2lex_true-termination.c
|
YES
20.7 /
10.7
|
YES
0.3 /
0.3
|
YES
12.8 /
6.9
|
| C/Ultimate/Parallel_true-termination.c
|
YES
9.1 /
4.3
|
YES
0.2 /
0.2
|
YES
10.4 /
8.7
|
| C/Ultimate/Pure3Phase_true-termination.c
|
.
372.3 /
300.1
|
YES
0.5 /
1.5
|
.
211.4 /
300.0
|
| C/Ultimate/README.txt
|
.
2.0 /
1.4
|
.
0.1 /
0.1
|
.
9.4 /
5.5
|
| ltimate/RecursiveMultiplication_true-termination.c
|
YES
7.2 /
8.3
|
YES
0.2 /
0.2
|
YES
12.3 /
15.0
|
| timate/RecursiveNonterminating_false-termination.c
|
.
6.0 /
3.2
|
.
10.8 /
18.3
|
NO
10.2 /
5.3
|
| C/Ultimate/Rotation180_false-termination.c
|
NO
3.9 /
5.5
|
NO
0.2 /
0.4
|
NO
11.0 /
5.5
|
| C/Ultimate/Stockholm_true-termination.c
|
YES
12.1 /
6.2
|
YES
0.3 /
1.2
|
YES
11.9 /
16.9
|
| Ultimate/SyntaxSupportPointer01_true-termination.c
|
.
4.0 /
2.5
|
YES
0.2 /
0.2
|
YES
11.9 /
14.4
|
| C/Ultimate/WhileFalse_true-termination.c
|
YES
2.3 /
1.7
|
YES
0.1 /
0.5
|
YES
10.2 /
6.3
|
| C/Ultimate/WhileTrue_false-termination.c
|
NO
2.8 /
6.8
|
NO
0.1 /
0.1
|
NO
10.3 /
13.4
|