| alloca/svcomp_Avery-2006FLOPS-Tabel1_true-alloca.c
|
YES
232.8 /
100.7
|
YES
46.4 /
27.8
|
| loca/svcomp_Ben-Amram-2010LMCS-Ex2.3_true-alloca.c
|
YES
52.3 /
32.1
|
YES
160.6 /
157.2
|
| nnaSipma-2005CAV-Fig1-modified_false-termination.c
|
.
764.3 /
300.1
|
not finished |
| vcomp_BradleyMannaSipma-2005CAV-Fig1_true-alloca.c
|
.
424.9 /
179.0
|
.
380.4 /
300.0
|
| omp_BradleyMannaSipma-2005ICALP-Fig1_true-alloca.c
|
.
1114.4 /
300.1
|
NO
31.4 /
11.6
|
| mp_BrockschmidtCookFuhs-2013CAV-Fig1_true-alloca.c
|
YES
66.8 /
34.5
|
YES
73.7 /
55.0
|
| schmidtCookFuhs-2013CAV-Introduction_true-alloca.c
|
YES
18.9 /
8.2
|
YES
17.3 /
7.7
|
| mp_ChenFlurMukhopadhyay-2012SAS-Fig1_true-alloca.c
|
YES
16.8 /
7.5
|
YES
27.9 /
16.3
|
| svcomp_CookSeeZuleger-2013TACAS-Fig3_true-alloca.c
|
YES
20.2 /
8.7
|
YES
28.0 /
13.8
|
| vcomp_CookSeeZuleger-2013TACAS-Fig7a_true-alloca.c
|
YES
87.3 /
39.0
|
YES
63.2 /
42.9
|
| vcomp_CookSeeZuleger-2013TACAS-Fig7b_true-alloca.c
|
YES
278.6 /
149.9
|
YES
189.4 /
155.8
|
| mp_GulwaniJainKoskinen-2009PLDI-Fig1_true-alloca.c
|
YES
43.5 /
28.7
|
.
301.4 /
300.1
|
| p_HarrisLalNoriRajamani-2010SAS-Fig1_true-alloca.c
|
YES
15.5 /
8.3
|
.
707.4 /
300.1
|
| 0SAS-Fig2_false-unreach-label-termination-alloca.c
|
NO
435.6 /
300.1
|
.
390.2 /
300.1
|
| p_HarrisLalNoriRajamani-2010SAS-Fig3_true-alloca.c
|
YES
45.0 /
15.5
|
YES
14.5 /
6.5
|
| aTsitovichWintersteiger-2010CAV-Fig1_true-alloca.c
|
.
606.5 /
300.1
|
YES
194.3 /
144.8
|
| riguez-CarbonellRubio-2013FMCAD-Fig1_true-alloca.c
|
.
1159.2 /
300.1
|
YES
98.7 /
70.1
|
| C/AProVE_memory_alloca/svcomp_Masse_true-alloca.c
|
.
986.3 /
300.1
|
.
31.0 /
10.9
|
| lloca/svcomp_NoriSharma-2013FSE-Fig7_true-alloca.c
|
YES
614.1 /
300.1
|
.
525.5 /
300.1
|
| lloca/svcomp_NoriSharma-2013FSE-Fig8_true-alloca.c
|
YES
219.0 /
119.1
|
YES
302.1 /
270.5
|
| mp_PodelskiRybalchenko-2004VMCAI-Ex2_true-alloca.c
|
NO
6.2 /
2.6
|
.
46.9 /
20.8
|
| y_alloca/svcomp_TelAviv-Amir-Minimum_true-alloca.c
|
.
1119.4 /
300.1
|
.
73.0 /
43.4
|
| lloca/svcomp_Toulouse-BranchesToLoop_true-alloca.c
|
YES
19.2 /
7.7
|
YES
68.3 /
33.8
|
| /svcomp_Toulouse-MultiBranchesToLoop_true-alloca.c
|
YES
30.3 /
21.8
|
YES
187.5 /
148.6
|
| 3WST-Fig1_false-unreach-label-termination-alloca.c
|
NO
6.5 /
3.1
|
NO
11.5 /
4.9
|
| comp_Urban-2013WST-Fig2-modified1000_true-alloca.c
|
YES
53.3 /
19.2
|
.
366.8 /
300.1
|
| ory_alloca/svcomp_Urban-2013WST-Fig2_true-alloca.c
|
YES
131.7 /
40.6
|
.
325.1 /
300.1
|
| C/AProVE_memory_alloca/svcomp_Urban_true-alloca.c
|
YES
287.2 /
186.1
|
YES
47.7 /
27.6
|
| _Velroyen_false-unreach-label-termination-alloca.c
|
NO
10.7 /
8.2
|
NO
26.1 /
11.7
|
| C/AProVE_memory_alloca/svcomp_a.01-alloca.c
|
YES
157.6 /
74.8
|
.
336.2 /
300.1
|
| C/AProVE_memory_alloca/svcomp_a.04-alloca.c
|
YES
61.6 /
19.0
|
.
667.8 /
300.1
|
| C/AProVE_memory_alloca/svcomp_a.05-alloca.c
|
YES
59.8 /
19.4
|
.
576.5 /
300.0
|
| C/AProVE_memory_alloca/svcomp_a.06-alloca.c
|
YES
117.3 /
48.9
|
.
995.5 /
300.1
|
| C/AProVE_memory_alloca/svcomp_a.07-alloca.c
|
YES
216.8 /
112.5
|
.
979.2 /
300.1
|
| C/AProVE_memory_alloca/svcomp_a.08-alloca.c
|
YES
65.1 /
23.3
|
.
886.5 /
300.0
|
| C/AProVE_memory_alloca/svcomp_a.09_assume-alloca.c
|
YES
14.6 /
5.8
|
YES
22.4 /
10.5
|
| C/AProVE_memory_alloca/svcomp_a.10-alloca.c
|
YES
99.6 /
41.5
|
.
778.2 /
300.1
|
| C/AProVE_memory_alloca/svcomp_add_last_alloca.c
|
.
4.6 /
5.6
|
.
312.7 /
300.1
|
| C/AProVE_memory_alloca/svcomp_array01_alloca.c
|
YES
127.2 /
84.9
|
YES
23.0 /
11.5
|
| C/AProVE_memory_alloca/svcomp_array02_alloca.c
|
YES
431.5 /
300.1
|
YES
42.4 /
27.5
|
| C/AProVE_memory_alloca/svcomp_array03_alloca.c
|
YES
490.9 /
300.1
|
.
356.4 /
300.0
|
| C/AProVE_memory_alloca/svcomp_aviad_true-alloca.c
|
YES
113.2 /
68.7
|
.
906.4 /
300.1
|
| C/AProVE_memory_alloca/svcomp_b.01-alloca.c
|
YES
57.3 /
34.1
|
.
785.3 /
300.1
|
| C/AProVE_memory_alloca/svcomp_b.02-alloca.c
|
YES
124.2 /
60.6
|
.
876.8 /
300.1
|
| E_memory_alloca/svcomp_b.03-no-inv_assume-alloca.c
|
YES
11.5 /
4.4
|
YES
22.2 /
11.1
|
| C/AProVE_memory_alloca/svcomp_b.03_assume-alloca.c
|
YES
12.2 /
4.9
|
YES
23.9 /
11.1
|
| C/AProVE_memory_alloca/svcomp_b.04-alloca.c
|
YES
7.5 /
2.7
|
YES
22.7 /
9.3
|
| C/AProVE_memory_alloca/svcomp_b.05-alloca.c
|
YES
15.0 /
7.8
|
YES
19.5 /
8.3
|
| C/AProVE_memory_alloca/svcomp_b.06-alloca.c
|
YES
83.3 /
37.6
|
.
1034.2 /
300.2
|
| C/AProVE_memory_alloca/svcomp_b.07-alloca.c
|
YES
238.1 /
120.8
|
.
917.6 /
300.1
|
| E_memory_alloca/svcomp_b.09-no-inv_assume-alloca.c
|
YES
95.6 /
71.0
|
.
333.2 /
300.1
|
| C/AProVE_memory_alloca/svcomp_b.09_assume-alloca.c
|
YES
100.4 /
56.5
|
.
798.2 /
300.1
|
| C/AProVE_memory_alloca/svcomp_b.10-alloca.c
|
YES
137.9 /
69.9
|
.
511.5 /
300.1
|
| C/AProVE_memory_alloca/svcomp_b.11-alloca.c
|
YES
301.0 /
196.3
|
.
916.8 /
300.1
|
| C/AProVE_memory_alloca/svcomp_b.12-alloca.c
|
YES
124.6 /
83.0
|
.
405.2 /
300.1
|
| C/AProVE_memory_alloca/svcomp_b.13-alloca.c
|
YES
256.6 /
148.2
|
.
833.4 /
300.1
|
| C/AProVE_memory_alloca/svcomp_b.14-alloca.c
|
YES
58.9 /
25.7
|
YES
53.4 /
37.1
|
| C/AProVE_memory_alloca/svcomp_b.15-alloca.c
|
YES
93.4 /
39.2
|
YES
112.3 /
87.5
|
| C/AProVE_memory_alloca/svcomp_b.16-alloca.c
|
YES
87.2 /
39.2
|
.
540.8 /
300.0
|
| C/AProVE_memory_alloca/svcomp_b.17-alloca.c
|
YES
169.8 /
87.1
|
YES
50.6 /
28.1
|
| C/AProVE_memory_alloca/svcomp_b.18-alloca.c
|
YES
16.6 /
7.7
|
YES
34.3 /
18.6
|
| C/AProVE_memory_alloca/svcomp_bubblesort_alloca.c
|
YES
493.6 /
300.1
|
YES
71.2 /
44.0
|
| C/AProVE_memory_alloca/svcomp_c.01-no-inv-alloca.c
|
YES
85.4 /
42.7
|
.
292.1 /
234.7
|
| C/AProVE_memory_alloca/svcomp_c.01_assume-alloca.c
|
YES
52.1 /
36.9
|
YES
36.6 /
22.1
|
| C/AProVE_memory_alloca/svcomp_c.02-alloca.c
|
YES
178.7 /
86.8
|
.
344.1 /
300.1
|
| C/AProVE_memory_alloca/svcomp_c.03-alloca.c
|
YES
242.9 /
229.1
|
.
351.6 /
300.1
|
| C/AProVE_memory_alloca/svcomp_c.07-alloca.c
|
YES
199.6 /
108.1
|
.
865.7 /
300.1
|
| C/AProVE_memory_alloca/svcomp_c.08-alloca.c
|
YES
281.6 /
135.6
|
.
332.8 /
300.1
|
| C/AProVE_memory_alloca/svcomp_count_down_alloca.c
|
.
94.1 /
34.4
|
YES
141.7 /
107.9
|
| C/AProVE_memory_alloca/svcomp_cstrcat_alloca.c
|
.
12.1 /
8.7
|
.
681.1 /
300.1
|
| /AProVE_memory_alloca/svcomp_cstrchr_true_alloca.c
|
YES
23.6 /
11.6
|
YES
27.7 /
15.9
|
| /AProVE_memory_alloca/svcomp_cstrcmp_true_alloca.c
|
YES
69.8 /
43.3
|
.
404.9 /
300.1
|
| C/AProVE_memory_alloca/svcomp_cstrcpy_alloca.c
|
YES
73.8 /
25.7
|
.
322.6 /
300.1
|
| AProVE_memory_alloca/svcomp_cstrcspn_true_alloca.c
|
YES
415.8 /
300.0
|
.
412.7 /
300.1
|
| /AProVE_memory_alloca/svcomp_cstrlen_true_alloca.c
|
YES
13.3 /
5.0
|
.
51.3 /
17.7
|
| C/AProVE_memory_alloca/svcomp_cstrncat_alloca.c
|
.
13.1 /
8.6
|
.
657.0 /
300.1
|
| AProVE_memory_alloca/svcomp_cstrncmp_true_alloca.c
|
YES
139.7 /
106.5
|
YES
59.6 /
49.0
|
| C/AProVE_memory_alloca/svcomp_cstrncpy_alloca.c
|
YES
147.5 /
78.3
|
.
344.5 /
300.1
|
| AProVE_memory_alloca/svcomp_cstrpbrk_true_alloca.c
|
YES
259.3 /
200.7
|
.
408.0 /
300.0
|
| /AProVE_memory_alloca/svcomp_cstrspn_true_alloca.c
|
YES
335.4 /
256.6
|
.
413.4 /
300.1
|
| C/AProVE_memory_alloca/svcomp_diff_alloca.c
|
.
678.4 /
300.1
|
.
338.9 /
300.1
|
| C/AProVE_memory_alloca/svcomp_easySum-alloca.c
|
YES
109.9 /
55.1
|
YES
24.8 /
11.5
|
| C/AProVE_memory_alloca/svcomp_ex1-alloca.c
|
YES
12.9 /
5.4
|
YES
20.2 /
9.0
|
| C/AProVE_memory_alloca/svcomp_ex2-alloca.c
|
YES
212.1 /
134.9
|
.
1004.5 /
300.1
|
| C/AProVE_memory_alloca/svcomp_ex3a-alloca.c
|
YES
22.2 /
10.3
|
.
386.4 /
246.9
|
| C/AProVE_memory_alloca/svcomp_ex3b-alloca.c
|
YES
48.6 /
17.5
|
.
798.3 /
300.1
|
| C/AProVE_memory_alloca/svcomp_fermat-alloca.c
|
YES
524.4 /
300.1
|
.
324.1 /
300.1
|
| C/AProVE_memory_alloca/svcomp_flag-alloca.c
|
YES
66.7 /
23.8
|
.
1021.2 /
300.1
|
| C/AProVE_memory_alloca/svcomp_gcd1_true-alloca.c
|
YES
226.4 /
172.0
|
YES
50.2 /
31.8
|
| C/AProVE_memory_alloca/svcomp_genady_true-alloca.c
|
YES
53.8 /
17.2
|
YES
19.7 /
9.1
|
| AProVE_memory_alloca/svcomp_insertionsort_alloca.c
|
YES
392.4 /
300.1
|
YES
237.8 /
172.9
|
| C/AProVE_memory_alloca/svcomp_java_AG313-alloca.c
|
YES
44.1 /
19.9
|
YES
24.3 /
12.4
|
| C/AProVE_memory_alloca/svcomp_java_Break-alloca.c
|
YES
11.0 /
5.5
|
.
362.1 /
300.0
|
| roVE_memory_alloca/svcomp_java_BubbleSort_alloca.c
|
.
144.4 /
47.6
|
.
307.8 /
300.1
|
| ProVE_memory_alloca/svcomp_java_Continue1-alloca.c
|
YES
23.6 /
13.9
|
.
318.6 /
300.1
|
| roVE_memory_alloca/svcomp_java_LogBuiltIn-alloca.c
|
YES
16.2 /
7.3
|
.
414.8 /
300.1
|
| C/AProVE_memory_alloca/svcomp_java_Nested-alloca.c
|
YES
70.6 /
40.5
|
.
68.8 /
54.8
|
| AProVE_memory_alloca/svcomp_java_Sequence-alloca.c
|
YES
21.9 /
10.1
|
.
321.1 /
300.1
|
| C/AProVE_memory_alloca/svcomp_lis_alloca.c
|
.
656.4 /
300.1
|
.
370.5 /
300.1
|
| C/AProVE_memory_alloca/svcomp_min_rf_true-alloca.c
|
YES
416.1 /
300.0
|
.
337.8 /
300.0
|
| C/AProVE_memory_alloca/svcomp_mult_array_alloca.c
|
YES
297.9 /
232.0
|
.
475.9 /
300.1
|
| ProVE_memory_alloca/svcomp_openbsd_cbzero_alloca.c
|
YES
21.6 /
14.4
|
.
339.3 /
300.0
|
| roVE_memory_alloca/svcomp_openbsd_cmemchr_alloca.c
|
YES
67.4 /
55.4
|
.
87.9 /
300.1
|
| oVE_memory_alloca/svcomp_openbsd_cmemrchr_alloca.c
|
.
7.1 /
2.6
|
YES
19.6 /
9.3
|
| roVE_memory_alloca/svcomp_openbsd_cmemset_alloca.c
|
YES
37.4 /
14.8
|
.
330.7 /
300.0
|
| roVE_memory_alloca/svcomp_openbsd_cstpcpy_alloca.c
|
YES
35.3 /
12.0
|
.
340.3 /
300.1
|
| oVE_memory_alloca/svcomp_openbsd_cstpncpy_alloca.c
|
.
82.3 /
25.7
|
.
337.4 /
300.0
|
| roVE_memory_alloca/svcomp_openbsd_cstrcat_alloca.c
|
.
12.6 /
4.9
|
.
672.8 /
300.1
|
| roVE_memory_alloca/svcomp_openbsd_cstrcmp_alloca.c
|
YES
41.0 /
19.7
|
YES
37.2 /
19.8
|
| roVE_memory_alloca/svcomp_openbsd_cstrcpy_alloca.c
|
YES
37.5 /
13.1
|
.
338.4 /
300.1
|
| oVE_memory_alloca/svcomp_openbsd_cstrcspn_alloca.c
|
.
10.7 /
3.6
|
.
419.2 /
300.0
|
| oVE_memory_alloca/svcomp_openbsd_cstrlcpy_alloca.c
|
YES
134.0 /
78.6
|
.
453.7 /
300.1
|
| roVE_memory_alloca/svcomp_openbsd_cstrlen_alloca.c
|
YES
12.1 /
14.0
|
.
46.5 /
26.2
|
| oVE_memory_alloca/svcomp_openbsd_cstrncat_alloca.c
|
.
13.1 /
5.1
|
.
431.2 /
300.1
|
| oVE_memory_alloca/svcomp_openbsd_cstrncmp_alloca.c
|
YES
68.7 /
36.0
|
YES
58.3 /
39.5
|
| oVE_memory_alloca/svcomp_openbsd_cstrncpy_alloca.c
|
.
70.8 /
33.6
|
.
331.2 /
300.1
|
| oVE_memory_alloca/svcomp_openbsd_cstrnlen_alloca.c
|
YES
33.9 /
17.8
|
.
7.1 /
3.2
|
| oVE_memory_alloca/svcomp_openbsd_cstrpbrk_alloca.c
|
YES
103.2 /
70.4
|
.
346.8 /
300.1
|
| roVE_memory_alloca/svcomp_openbsd_cstrspn_alloca.c
|
.
11.4 /
5.8
|
.
413.6 /
300.1
|
| roVE_memory_alloca/svcomp_openbsd_cstrstr_alloca.c
|
.
33.9 /
9.5
|
.
819.6 /
300.0
|
| AProVE_memory_alloca/svcomp_selectionsort_alloca.c
|
.
125.4 /
54.2
|
.
318.9 /
300.1
|
| C/AProVE_memory_alloca/svcomp_stroeder1_alloca.c
|
YES
48.0 /
21.5
|
YES
16.7 /
8.3
|
| C/AProVE_memory_alloca/svcomp_stroeder2_alloca.c
|
YES
180.8 /
132.4
|
YES
24.3 /
12.7
|
| C/AProVE_memory_alloca/svcomp_strreplace_alloca.c
|
YES
263.0 /
131.6
|
YES
26.2 /
11.9
|
| C/AProVE_memory_alloca/svcomp_subseq_alloca.c
|
YES
177.7 /
108.9
|
YES
83.7 /
54.8
|
| C/AProVE_memory_alloca/svcomp_substring_alloca.c
|
YES
268.8 /
190.3
|
.
331.1 /
300.0
|
| C/AProVE_memory_alloca/svcomp_twisted-alloca.c
|
YES
14.9 /
7.9
|
YES
52.2 /
31.4
|
| C/AProVE_memory_unsafe/svcomp_add_last_unsafe.c
|
.
4.6 /
2.6
|
.
9.9 /
5.1
|
| C/AProVE_memory_unsafe/svcomp_bubble_sort_unsafe.c
|
.
4.6 /
1.9
|
.
11.8 /
4.6
|
| C/AProVE_memory_unsafe/svcomp_bubblesort_unsafe.c
|
.
9.8 /
3.9
|
.
8.8 /
4.0
|
| C/AProVE_memory_unsafe/svcomp_count_down_unsafe.c
|
.
4.8 /
2.0
|
.
9.5 /
4.8
|
| C/AProVE_memory_unsafe/svcomp_cstrcat_unsafe.c
|
.
4.0 /
1.7
|
.
8.7 /
4.1
|
| C/AProVE_memory_unsafe/svcomp_cstrchr_unsafe.c
|
.
4.5 /
1.8
|
.
22.4 /
11.6
|
| C/AProVE_memory_unsafe/svcomp_cstrcpy_unsafe.c
|
.
4.2 /
1.7
|
.
8.3 /
3.8
|
| C/AProVE_memory_unsafe/svcomp_cstrlen_unsafe.c
|
.
3.6 /
1.7
|
.
11.0 /
5.0
|
| C/AProVE_memory_unsafe/svcomp_cstrncat_unsafe.c
|
.
4.1 /
1.8
|
.
9.5 /
4.3
|
| C/AProVE_memory_unsafe/svcomp_cstrncpy_unsafe.c
|
.
5.0 /
2.0
|
.
8.8 /
4.0
|
| C/AProVE_memory_unsafe/svcomp_cstrpbrk_unsafe.c
|
.
4.5 /
1.9
|
.
19.4 /
10.2
|
| AProVE_memory_unsafe/svcomp_delete_alloca_unsafe.c
|
.
4.8 /
2.0
|
.
8.6 /
4.0
|
| C/AProVE_memory_unsafe/svcomp_delete_unsafe.c
|
.
3.8 /
1.6
|
.
6.9 /
3.2
|
| C/AProVE_memory_unsafe/svcomp_diff_usafe.c
|
.
6.0 /
2.3
|
.
8.5 /
4.0
|
| ProVE_memory_unsafe/svcomp_insertion_sort_unsafe.c
|
.
4.9 /
2.3
|
.
8.9 /
4.1
|
| AProVE_memory_unsafe/svcomp_insertionsort_unsafe.c
|
.
4.7 /
1.9
|
.
9.0 /
4.1
|
| roVE_memory_unsafe/svcomp_java_BubbleSort_unsafe.c
|
.
5.1 /
2.3
|
.
9.1 /
6.5
|
| roVE_memory_unsafe/svcomp_knapsack_alloca_unsafe.c
|
.
9.4 /
4.0
|
.
12.1 /
5.3
|
| C/AProVE_memory_unsafe/svcomp_knapsack_unsafe.c
|
.
5.7 /
2.3
|
.
9.5 /
4.3
|
| C/AProVE_memory_unsafe/svcomp_lis_unsafe.c
|
.
4.8 /
2.0
|
.
15.8 /
6.4
|
| C/AProVE_memory_unsafe/svcomp_mult_array_unsafe.c
|
.
5.5 /
2.1
|
.
9.3 /
4.2
|
| memory_unsafe/svcomp_reverse_array_alloca_unsafe.c
|
.
7.3 /
3.2
|
.
14.1 /
5.8
|
| AProVE_memory_unsafe/svcomp_reverse_array_unsafe.c
|
.
5.7 /
3.4
|
.
13.2 /
8.8
|
| ProVE_memory_unsafe/svcomp_selection_sort_unsafe.c
|
.
4.3 /
1.9
|
.
9.6 /
4.3
|
| AProVE_memory_unsafe/svcomp_selectionsort_unsafe.c
|
.
5.0 /
2.0
|
.
9.6 /
4.5
|
| C/AProVE_memory_unsafe/svcomp_stroeder1_unsafe.c
|
.
4.5 /
1.9
|
.
8.1 /
3.7
|
| C/AProVE_memory_unsafe/svcomp_stroeder2_unsafe.c
|
.
4.4 /
1.8
|
.
9.1 /
4.2
|
| C/AProVE_numeric/Avg_true.c
|
YES
18.9 /
6.9
|
YES
28.0 /
16.9
|
| C/AProVE_numeric/Binomial_true.c
|
YES
445.3 /
277.4
|
.
376.7 /
300.0
|
| C/AProVE_numeric/Et1_true.c
|
YES
23.7 /
8.0
|
YES
21.5 /
16.4
|
| C/AProVE_numeric/Et2_true.c
|
YES
27.0 /
10.9
|
YES
12.3 /
5.2
|
| C/AProVE_numeric/Et3_true.c
|
YES
23.2 /
7.6
|
YES
10.3 /
5.1
|
| C/AProVE_numeric/Et4_true.c
|
YES
31.4 /
13.1
|
YES
40.7 /
30.6
|
| C/AProVE_numeric/LeUserDefRec_true.c
|
YES
9.1 /
3.5
|
YES
9.1 /
4.5
|
| C/AProVE_numeric/LogRecursive_true.c
|
.
665.2 /
300.1
|
.
37.9 /
29.1
|
| C/AProVE_numeric/Parts_true.c
|
YES
424.0 /
300.1
|
.
846.9 /
300.1
|
| C/AProVE_numeric/TerminatorRec02_true.c
|
YES
7.7 /
3.6
|
YES
10.0 /
5.2
|
| C/AProVE_numeric/TwoWay_true.c
|
YES
8.3 /
3.4
|
YES
23.0 /
16.4
|
| C/AProVE_numeric/ex2.c
|
YES
6.9 /
3.2
|
YES
11.2 /
5.0
|
| C/AProVE_numeric/ex3.c
|
YES
8.1 /
3.1
|
.
529.5 /
300.1
|
| C/AProVE_numeric/rec_counter1.c
|
YES
18.1 /
7.4
|
YES
13.3 /
6.7
|
| C/AProVE_numeric/rec_counter3.c
|
YES
15.7 /
6.6
|
YES
12.8 /
5.9
|
| C/AProVE_numeric/rec_strlen.c
|
YES
9.0 /
3.5
|
YES
21.7 /
10.5
|
| _Ackermann01_true-unreach-call_modified_modified.c
|
YES
18.7 /
9.5
|
.
657.0 /
300.1
|
| on01_true-unreach-call_true-termination_modified.c
|
YES
7.2 /
3.4
|
YES
22.7 /
15.9
|
| dd01_true-unreach-call_true-termination_modified.c
|
YES
9.1 /
4.4
|
YES
20.5 /
12.6
|
| ic/svcomp_Fibonacci01_true-unreach-call_modified.c
|
YES
17.2 /
7.7
|
.
475.8 /
300.0
|
| tive_true-unreach-call_true-termination_modified.c
|
YES
10.2 /
4.3
|
YES
20.7 /
12.7
|
| C/AProVE_numeric/svcomp_a.01.c
|
YES
114.8 /
40.7
|
YES
11.6 /
5.4
|
| C/AProVE_numeric/svcomp_a.04.c
|
YES
23.8 /
7.3
|
YES
9.3 /
8.2
|
| C/AProVE_numeric/svcomp_a.05.c
|
YES
22.9 /
7.2
|
YES
9.5 /
4.4
|
| C/AProVE_numeric/svcomp_a.06.c
|
YES
48.7 /
15.4
|
YES
12.3 /
7.0
|
| C/AProVE_numeric/svcomp_a.07.c
|
YES
65.1 /
24.5
|
YES
9.8 /
4.5
|
| C/AProVE_numeric/svcomp_a.08.c
|
YES
36.4 /
10.9
|
YES
8.9 /
4.1
|
| C/AProVE_numeric/svcomp_a.09_assume.c
|
YES
10.0 /
4.4
|
YES
9.6 /
4.7
|
| C/AProVE_numeric/svcomp_a.10.c
|
YES
75.1 /
15.6
|
YES
15.6 /
11.3
|
| C/AProVE_numeric/svcomp_b.01.c
|
YES
25.1 /
14.6
|
YES
11.5 /
17.6
|
| C/AProVE_numeric/svcomp_b.02.c
|
YES
51.6 /
15.1
|
YES
9.3 /
4.3
|
| C/AProVE_numeric/svcomp_b.03-no-inv_assume.c
|
YES
8.4 /
3.2
|
YES
10.6 /
5.0
|
| C/AProVE_numeric/svcomp_b.03_assume.c
|
YES
9.4 /
4.1
|
YES
9.4 /
4.3
|
| C/AProVE_numeric/svcomp_b.04.c
|
YES
5.2 /
2.5
|
YES
11.6 /
6.5
|
| C/AProVE_numeric/svcomp_b.05.c
|
YES
6.2 /
2.7
|
YES
10.0 /
5.2
|
| C/AProVE_numeric/svcomp_b.06.c
|
YES
38.9 /
15.8
|
YES
9.1 /
7.9
|
| C/AProVE_numeric/svcomp_b.07.c
|
YES
67.7 /
27.7
|
YES
9.8 /
4.7
|
| C/AProVE_numeric/svcomp_b.09-no-inv_assume.c
|
YES
38.4 /
17.5
|
YES
15.6 /
7.9
|
| C/AProVE_numeric/svcomp_b.09_assume.c
|
YES
38.7 /
16.1
|
YES
10.4 /
4.8
|
| C/AProVE_numeric/svcomp_b.10.c
|
YES
52.3 /
22.0
|
YES
12.9 /
8.0
|
| C/AProVE_numeric/svcomp_b.11.c
|
YES
101.1 /
52.8
|
YES
11.2 /
5.1
|
| C/AProVE_numeric/svcomp_b.12.c
|
YES
44.7 /
22.8
|
YES
10.9 /
6.1
|
| C/AProVE_numeric/svcomp_b.13.c
|
YES
71.5 /
37.3
|
YES
11.2 /
5.2
|
| C/AProVE_numeric/svcomp_b.14.c
|
YES
23.4 /
12.5
|
YES
10.8 /
5.8
|
| C/AProVE_numeric/svcomp_b.15.c
|
YES
43.9 /
16.7
|
YES
11.5 /
5.7
|
| C/AProVE_numeric/svcomp_b.16.c
|
YES
32.8 /
12.3
|
YES
9.6 /
4.4
|
| C/AProVE_numeric/svcomp_b.17.c
|
YES
57.7 /
40.7
|
YES
10.1 /
5.0
|
| C/AProVE_numeric/svcomp_b.18.c
|
YES
10.8 /
4.5
|
YES
11.1 /
4.8
|
| C/AProVE_numeric/svcomp_c.01-no-inv.c
|
YES
37.8 /
15.0
|
YES
15.5 /
7.1
|
| C/AProVE_numeric/svcomp_c.01_assume.c
|
YES
27.1 /
13.5
|
YES
11.6 /
5.1
|
| C/AProVE_numeric/svcomp_c.02.c
|
YES
32.9 /
14.2
|
YES
11.6 /
5.3
|
| C/AProVE_numeric/svcomp_c.03.c
|
YES
79.8 /
33.5
|
YES
15.1 /
10.0
|
| C/AProVE_numeric/svcomp_c.07.c
|
YES
60.1 /
21.7
|
YES
21.8 /
17.1
|
| C/AProVE_numeric/svcomp_c.08.c
|
YES
80.9 /
35.4
|
YES
12.7 /
6.6
|
| C/AProVE_numeric/svcomp_easySum.c
|
YES
35.1 /
10.6
|
YES
9.0 /
4.1
|
| C/AProVE_numeric/svcomp_ex1.c
|
YES
9.1 /
4.0
|
YES
9.4 /
4.9
|
| C/AProVE_numeric/svcomp_ex2.c
|
YES
71.0 /
38.6
|
.
23.3 /
9.9
|
| C/AProVE_numeric/svcomp_ex3a.c
|
YES
11.6 /
7.0
|
.
20.9 /
11.9
|
| C/AProVE_numeric/svcomp_ex3b.c
|
YES
18.5 /
8.4
|
.
22.8 /
9.8
|
| C/AProVE_numeric/svcomp_fermat.c
|
YES
333.6 /
300.1
|
YES
154.0 /
142.4
|
| C/AProVE_numeric/svcomp_flag.c
|
YES
29.3 /
9.3
|
YES
24.7 /
9.1
|
| cd01_true-unreach-call_true-termination_modified.c
|
YES
10.7 /
3.7
|
YES
13.9 /
6.9
|
| C/AProVE_numeric/svcomp_java_AG313.c
|
YES
19.6 /
8.2
|
YES
9.7 /
4.5
|
| C/AProVE_numeric/svcomp_java_Break.c
|
YES
9.7 /
4.3
|
YES
9.7 /
5.2
|
| C/AProVE_numeric/svcomp_java_Continue1.c
|
YES
12.8 /
5.1
|
YES
9.3 /
4.3
|
| C/AProVE_numeric/svcomp_java_LogBuiltIn.c
|
YES
10.1 /
4.6
|
YES
9.6 /
4.4
|
| C/AProVE_numeric/svcomp_java_Nested.c
|
YES
38.8 /
19.4
|
YES
16.2 /
7.9
|
| C/AProVE_numeric/svcomp_java_Sequence.c
|
YES
12.5 /
4.9
|
YES
9.4 /
4.2
|
| oi02_true-unreach-call_true-termination_modified.c
|
YES
7.9 /
3.1
|
YES
11.1 /
7.9
|
| C/AProVE_numeric/svcomp_twisted.c
|
YES
206.0 /
143.8
|
YES
14.2 /
9.2
|
| Mixed_Categories/960521-1_1_true-valid-memsafety.c
|
.
6.3 /
2.3
|
.
356.9 /
300.1
|
| es/Addition01_true-unreach-call_true-termination.c
|
.
7.2 /
2.6
|
YES
24.3 /
16.1
|
| es/BallRajamani-SPIN2000-Fig1_false-unreach-call.c
|
.
5.3 /
2.3
|
YES
18.5 /
8.5
|
| ies/EvenOdd01_true-unreach-call_true-termination.c
|
.
5.8 /
2.2
|
YES
18.9 /
11.5
|
| P_Mixed_Categories/Fibonacci01_true-unreach-call.c
|
.
6.0 /
2.4
|
.
434.4 /
300.1
|
| /McCarthy91_false-unreach-call_false-termination.c
|
.
4.9 /
2.3
|
YES
59.1 /
47.8
|
| V-COMP_Mixed_Categories/Primes_true-unreach-call.c
|
.
12.0 /
4.6
|
NO
27.5 /
15.7
|
| d_Categories/Problem01_label00_true-unreach-call.c
|
.
602.8 /
300.1
|
.
369.4 /
300.1
|
| d_Categories/Problem02_label00_true-unreach-call.c
|
.
602.9 /
300.1
|
NO
48.2 /
20.2
|
| d_Categories/Problem03_label00_true-unreach-call.c
|
.
603.5 /
300.0
|
.
548.8 /
300.1
|
| d_Categories/Problem04_label00_true-unreach-call.c
|
.
313.1 /
300.1
|
.
444.8 /
300.1
|
| _Categories/Problem05_label00_false-unreach-call.c
|
.
3.5 /
300.1
|
.
558.3 /
300.1
|
| _Categories/Problem06_label00_false-unreach-call.c
|
.
3.4 /
300.0
|
.
558.4 /
300.1
|
| d_Categories/Problem07_label00_true-unreach-call.c
|
.
616.6 /
300.1
|
.
101.7 /
51.7
|
| d_Categories/Problem08_label00_true-unreach-call.c
|
.
3.5 /
300.1
|
.
143.6 /
83.7
|
| d_Categories/Problem09_label00_true-unreach-call.c
|
.
4.1 /
300.1
|
.
154.8 /
91.7
|
| d_Categories/Problem10_label00_true-unreach-call.c
|
.
602.0 /
300.1
|
.
112.0 /
79.3
|
| _Categories/Problem11_label00_false-unreach-call.c
|
.
603.1 /
300.1
|
.
344.9 /
300.1
|
| _Categories/Problem12_label00_false-unreach-call.c
|
.
603.9 /
300.1
|
.
335.9 /
300.1
|
| d_Categories/Problem13_label00_true-unreach-call.c
|
.
604.9 /
300.1
|
.
447.9 /
300.1
|
| d_Categories/Problem14_label00_true-unreach-call.c
|
.
602.4 /
300.0
|
NO
52.7 /
26.7
|
| _Categories/Problem15_label00_false-unreach-call.c
|
.
603.3 /
300.1
|
NO
110.4 /
61.1
|
| _Categories/Problem16_label00_false-unreach-call.c
|
.
601.4 /
300.1
|
NO
109.2 /
53.5
|
| d_Categories/Problem17_label00_true-unreach-call.c
|
.
602.0 /
300.0
|
NO
119.2 /
79.1
|
| _Categories/Problem18_label00_false-unreach-call.c
|
.
603.8 /
300.0
|
NO
206.2 /
143.7
|
| d_Categories/Problem19_label00_true-unreach-call.c
|
.
604.0 /
300.1
|
.
409.0 /
300.1
|
| ed_Categories/afterrec_2calls_false-unreach-call.c
|
YES
5.7 /
2.9
|
YES
11.1 /
5.8
|
| ist_cell_true-unreach-call_false-termination.cil.c
|
NO
42.4 /
18.4
|
NO
27.4 /
11.0
|
| d_Categories/bubble_sort_linux_true-unreach-call.c
|
.
3.1 /
1.5
|
.
229.6 /
212.3
|
| o_simpl1_false-unreach-call_true-termination.cil.c
|
.
622.6 /
300.1
|
YES
28.7 /
13.5
|
| OMP_Mixed_Categories/cs_dekker_true-unreach-call.c
|
.
18.1 /
8.5
|
.
342.1 /
300.1
|
| Mixed_Categories/cs_fib_longer_true-unreach-call.c
|
.
3.8 /
1.6
|
.
7.6 /
3.3
|
| MP_Mixed_Categories/cs_lamport_true-unreach-call.c
|
.
33.6 /
17.7
|
.
326.5 /
300.1
|
| P_Mixed_Categories/cs_peterson_true-unreach-call.c
|
.
14.7 /
12.2
|
.
334.6 /
300.1
|
| _Mixed_Categories/cs_stateful_false-unreach-call.c
|
.
10.9 /
5.2
|
.
351.1 /
300.1
|
| _Mixed_Categories/cs_szymanski_true-unreach-call.c
|
.
18.9 /
8.9
|
.
337.4 /
300.0
|
| d_Categories/cs_time_var_mutex_true-unreach-call.c
|
.
17.4 /
8.1
|
.
338.1 /
300.1
|
| uctures_set_multi_proc_false-unreach-call_ground.c
|
.
45.2 /
17.1
|
.
352.9 /
300.1
|
| rf_simpl1_true-unreach-call_true-termination.cil.c
|
.
635.5 /
300.0
|
YES
17.9 /
7.5
|
| egories/dll_extends_pointer_true-valid-memsafety.c
|
.
3.6 /
1.7
|
.
356.5 /
300.0
|
| MP_Mixed_Categories/dll_of_dll_true-unreach-call.c
|
.
3.3 /
1.6
|
.
343.7 /
300.1
|
| s/elevator_spec1_product01_true-unreach-call.cil.c
|
.
4.0 /
2.0
|
.
455.2 /
300.1
|
| ries/email_spec0_product05_true-unreach-call.cil.c
|
.
3.3 /
1.6
|
YES
13.5 /
6.0
|
| ixed_Categories/fibo_2calls_2_false-unreach-call.c
|
YES
5.4 /
2.1
|
YES
11.1 /
5.5
|
| -COMP_Mixed_Categories/fibo_5_false-unreach-call.c
|
YES
24.3 /
11.6
|
YES
30.5 /
19.6
|
| y_simpl3_false-unreach-call_true-termination.cil.c
|
.
629.2 /
300.0
|
YES
19.3 /
9.2
|
| egories/gcd01_true-unreach-call_true-termination.c
|
YES
11.9 /
4.1
|
YES
14.6 /
8.2
|
| OMP_Mixed_Categories/id2_b2_o3_true-unreach-call.c
|
.
105.2 /
28.5
|
NO
9.8 /
4.7
|
| P_Mixed_Categories/id_i10_o10_false-unreach-call.c
|
YES
7.8 /
3.1
|
YES
11.1 /
7.5
|
| tr_simpl1_true-unreach-call_true-termination.cil.c
|
.
622.6 /
300.0
|
YES
10.8 /
5.4
|
| Mixed_Categories/list-ext_1_true-valid-memsafety.c
|
.
4.3 /
1.9
|
.
319.2 /
300.1
|
| /SV-COMP_Mixed_Categories/list_true-unreach-call.c
|
.
3.7 /
1.7
|
.
332.9 /
300.0
|
| xed_Categories/lockfree-3.0_true-valid-memsafety.c
|
.
3.4 /
1.6
|
.
365.3 /
300.1
|
| ve_tlm.1_true-unreach-call_false-termination.cil.c
|
.
519.6 /
229.8
|
NO
25.0 /
11.5
|
| MP_Mixed_Categories/merge_sort_true-unreach-call.c
|
.
3.6 /
1.8
|
.
329.8 /
300.0
|
| s/minepump_spec1_product01_true-unreach-call.cil.c
|
.
3.9 /
1.9
|
NO
10.7 /
4.5
|
| Standby_false-unreach-call.1.ufo.BOUNDED-10.pals.c
|
.
3.8 /
1.8
|
.
321.0 /
300.1
|
| licated_false-unreach-call.1.ufo.BOUNDED-10.pals.c
|
.
3.8 /
2.0
|
YES
94.9 /
66.0
|
| oodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c
|
.
3.7 /
1.6
|
YES
25.7 /
13.2
|
| odmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c
|
.
4.1 /
1.7
|
YES
94.3 /
64.6
|
| t-time.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c
|
.
3.7 /
1.6
|
YES
19.2 /
9.5
|
| -time.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c
|
.
3.9 /
1.6
|
YES
22.8 /
13.1
|
| ls_lcr.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c
|
.
3.8 /
1.6
|
YES
36.1 /
16.5
|
| s_lcr.8_false-unreach-call.1.ufo.BOUNDED-16.pals.c
|
.
3.9 /
1.7
|
.
348.2 /
300.0
|
| oodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c
|
.
3.8 /
1.9
|
YES
16.3 /
6.8
|
| odmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c
|
.
3.9 /
2.0
|
YES
111.6 /
74.1
|
| sfifo_1_false-unreach-call_false-termination.cil.c
|
.
6.4 /
2.5
|
NO
11.8 /
5.1
|
| es/recHanoi01_true-unreach-call_true-termination.c
|
.
5.9 /
2.3
|
.
599.0 /
300.0
|
| ed_Categories/rekcba_aso_false-unreach-call.1.M1.c
|
.
4.4 /
2.4
|
.
10.3 /
4.2
|
| Mixed_Categories/rekcba_ctm_false-unreach-call.2.c
|
.
214.2 /
106.3
|
.
351.7 /
300.1
|
| ed_Categories/rekcba_nxt_false-unreach-call.1.M1.c
|
.
3.5 /
1.6
|
.
9.1 /
3.8
|
| ixed_Categories/s3_clnt_1_false-unreach-call.cil.c
|
.
620.6 /
300.1
|
YES
95.5 /
63.3
|
| xed_Categories/s3_srvr_14_false-unreach-call.cil.c
|
.
617.5 /
300.1
|
.
179.9 /
300.1
|
| ixed_Categories/s3_srvr_1_false-unreach-call.cil.c
|
.
621.9 /
300.1
|
NO
41.2 /
18.6
|
| ategories/sanfoundry_02_true-unreach-call_ground.c
|
.
96.3 /
29.5
|
.
374.4 /
300.0
|
| xed_Categories/simple-ext_1_true-valid-memsafety.c
|
.
3.9 /
1.8
|
.
645.6 /
300.1
|
| ed_Categories/skiplist_3lvl_true-valid-memsafety.c
|
.
3.7 /
1.6
|
.
372.4 /
300.0
|
| ixed_Categories/sll_to_dll_rev_true-unreach-call.c
|
.
3.4 /
1.7
|
.
318.7 /
300.1
|
| ries/sorting_bubblesort_true-unreach-call_ground.c
|
.
39.0 /
11.2
|
.
366.6 /
300.1
|
| V-COMP_Mixed_Categories/splice_true-unreach-call.c
|
.
3.9 /
2.0
|
.
400.2 /
300.1
|
| gories/standard_compare_true-unreach-call_ground.c
|
.
37.0 /
10.9
|
.
367.5 /
300.0
|
| tegories/standard_copy7_true-unreach-call_ground.c
|
.
60.2 /
27.9
|
.
511.9 /
300.0
|
| ories/standard_password_true-unreach-call_ground.c
|
.
38.5 /
14.8
|
.
374.0 /
300.0
|
| xed_Categories/stateful_check_false-unreach-call.c
|
.
3.2 /
1.6
|
NO
9.8 /
5.2
|
| COMP_Mixed_Categories/sum_2x3_false-unreach-call.c
|
YES
7.8 /
4.5
|
YES
9.5 /
4.9
|
| P_Mixed_Categories/sum_non_eq_false-unreach-call.c
|
.
100.8 /
29.4
|
NO
9.4 /
4.9
|
| _Mixed_Categories/test-0134_true-valid-memsafety.c
|
.
3.8 /
1.6
|
.
318.1 /
300.0
|
| _Mixed_Categories/test-0219_true-valid-memsafety.c
|
.
3.2 /
1.5
|
.
311.1 /
300.0
|
| _Mixed_Categories/test-0234_true-valid-memsafety.c
|
.
3.8 /
2.0
|
.
317.2 /
300.1
|
| ixed_Categories/test-0513_1_true-valid-memsafety.c
|
.
3.7 /
1.8
|
.
334.6 /
300.1
|
| _Mixed_Categories/test-0521_true-valid-memsafety.c
|
.
6.0 /
2.7
|
.
811.9 /
300.1
|
| est_locks_15_true-unreach-call_false-termination.c
|
.
627.4 /
300.1
|
NO
12.7 /
8.5
|
| ring.01_false-unreach-call_false-termination.cil.c
|
.
634.4 /
300.1
|
NO
18.0 /
8.1
|
| ring.05_false-unreach-call_false-termination.cil.c
|
.
627.5 /
300.0
|
NO
84.0 /
46.4
|
| ring.10_false-unreach-call_false-termination.cil.c
|
.
626.1 /
300.1
|
.
637.2 /
300.1
|
| ring.15_false-unreach-call_false-termination.cil.c
|
.
629.0 /
300.1
|
.
709.7 /
300.1
|
| tter.01_false-unreach-call_false-termination.cil.c
|
.
629.7 /
294.4
|
NO
17.8 /
11.3
|
| tter.06_false-unreach-call_false-termination.cil.c
|
.
623.9 /
300.1
|
NO
218.4 /
141.2
|
| tter.11_false-unreach-call_false-termination.cil.c
|
.
623.0 /
300.1
|
.
621.7 /
300.5
|
| tter.16_false-unreach-call_false-termination.cil.c
|
.
624.1 /
300.1
|
.
640.9 /
300.1
|
| Mixed_Categories/tree_stack_true-valid-memsafety.c
|
.
4.4 /
1.9
|
.
322.5 /
300.0
|
| teFeautrierGonnord-SAS2010-Fig1_true-termination.c
|
YES
154.6 /
73.9
|
YES
15.5 /
7.0
|
| eFeautrierGonnord-SAS2010-Fig2a_true-termination.c
|
YES
116.9 /
60.8
|
YES
12.6 /
5.7
|
| eFeautrierGonnord-SAS2010-Fig2b_true-termination.c
|
.
629.6 /
300.1
|
YES
22.8 /
12.1
|
| rierGonnord-SAS2010-counterex1a_true-termination.c
|
YES
203.3 /
116.1
|
YES
20.3 /
8.6
|
| rierGonnord-SAS2010-counterex1b_true-termination.c
|
YES
425.8 /
300.0
|
YES
14.2 /
6.7
|
| eautrierGonnord-SAS2010-cousot9_true-termination.c
|
YES
12.9 /
5.6
|
YES
11.8 /
5.6
|
| eFeautrierGonnord-SAS2010-ndecr_true-termination.c
|
YES
7.0 /
2.8
|
YES
9.4 /
4.2
|
| trierGonnord-SAS2010-nestedLoop_true-termination.c
|
.
67.2 /
24.4
|
YES
30.3 /
21.2
|
| autrierGonnord-SAS2010-random1d_true-termination.c
|
YES
230.4 /
79.1
|
YES
9.3 /
4.5
|
| rteFeautrierGonnord-SAS2010-rsd_true-termination.c
|
.
613.1 /
300.0
|
YES
26.6 /
19.8
|
| trierGonnord-SAS2010-speedpldi2_true-termination.c
|
YES
41.2 /
13.3
|
YES
11.2 /
5.7
|
| trierGonnord-SAS2010-speedpldi3_true-termination.c
|
YES
51.3 /
22.7
|
YES
12.0 /
5.9
|
| trierGonnord-SAS2010-speedpldi4_true-termination.c
|
YES
11.2 /
4.5
|
YES
12.3 /
5.6
|
| utrierGonnord-SAS2010-terminate_true-termination.c
|
YES
13.9 /
9.8
|
YES
23.8 /
19.1
|
| eFeautrierGonnord-SAS2010-wcet2_true-termination.c
|
YES
21.7 /
13.0
|
YES
16.1 /
6.8
|
| FeautrierGonnord-SAS2010-while2_true-termination.c
|
YES
16.9 /
9.0
|
YES
11.9 /
5.1
|
| teFeautrierGonnord-SAS2010-wise_true-termination.c
|
YES
20.9 /
7.9
|
YES
12.8 /
5.8
|
| Category/Avery-FLOPS2006-Table1_true-termination.c
|
YES
92.5 /
46.7
|
YES
15.3 /
14.6
|
| nnaSipma-CAV2005-Fig1-modified_false-termination.c
|
.
1124.9 /
300.1
|
NO
8.5 /
3.9
|
| /BradleyMannaSipma-CAV2005-Fig1_true-termination.c
|
YES
74.3 /
24.7
|
YES
29.7 /
20.5
|
| radleyMannaSipma-ICALP2005-Fig1_true-termination.c
|
.
902.8 /
300.1
|
YES
29.7 /
19.3
|
| lwaniSagivYang-ESOP2008-aaron12_true-termination.c
|
.
1160.0 /
300.1
|
.
50.2 /
35.6
|
| ulwaniSagivYang-ESOP2008-aaron1_true-termination.c
|
YES
311.5 /
258.7
|
YES
13.0 /
5.9
|
| ulwaniSagivYang-ESOP2008-aaron4_true-termination.c
|
YES
389.9 /
300.1
|
YES
28.0 /
19.6
|
| ulwaniSagivYang-ESOP2008-aaron6_true-termination.c
|
.
622.2 /
300.1
|
YES
20.8 /
5.5
|
| waniSagivYang-ESOP2008-random1d_true-termination.c
|
YES
103.4 /
45.8
|
YES
18.9 /
4.6
|
| FlurMukhopadhyay-SAS2012-Ex1.02_true-termination.c
|
YES
10.3 /
6.1
|
YES
14.5 /
9.7
|
| FlurMukhopadhyay-SAS2012-Ex1.03_true-termination.c
|
YES
4.6 /
1.9
|
YES
9.9 /
4.5
|
| FlurMukhopadhyay-SAS2012-Ex1.04_true-termination.c
|
YES
8.6 /
3.2
|
YES
9.1 /
4.3
|
| FlurMukhopadhyay-SAS2012-Ex1.05_true-termination.c
|
YES
8.5 /
3.2
|
YES
9.2 /
4.5
|
| FlurMukhopadhyay-SAS2012-Ex2.01_true-termination.c
|
YES
12.3 /
5.6
|
YES
9.9 /
4.6
|
| lurMukhopadhyay-SAS2012-Ex2.02_false-termination.c
|
.
1175.3 /
300.1
|
NO
9.3 /
4.3
|
| lurMukhopadhyay-SAS2012-Ex2.05_false-termination.c
|
NO
8.2 /
3.7
|
NO
8.2 /
3.9
|
| FlurMukhopadhyay-SAS2012-Ex2.07_true-termination.c
|
YES
9.9 /
3.8
|
YES
10.3 /
5.5
|
| FlurMukhopadhyay-SAS2012-Ex2.08_true-termination.c
|
YES
12.8 /
4.4
|
YES
9.8 /
4.8
|
| FlurMukhopadhyay-SAS2012-Ex2.10_true-termination.c
|
YES
9.5 /
3.6
|
YES
10.2 /
5.4
|
| FlurMukhopadhyay-SAS2012-Ex2.13_true-termination.c
|
YES
13.7 /
4.7
|
YES
21.1 /
16.1
|
| FlurMukhopadhyay-SAS2012-Ex2.16_true-termination.c
|
YES
6.9 /
2.9
|
YES
9.0 /
4.2
|
| lurMukhopadhyay-SAS2012-Ex2.17_false-termination.c
|
.
120.1 /
34.2
|
NO
9.4 /
4.7
|
| FlurMukhopadhyay-SAS2012-Ex2.20_true-termination.c
|
YES
10.3 /
3.8
|
YES
9.6 /
5.3
|
| FlurMukhopadhyay-SAS2012-Ex2.22_true-termination.c
|
YES
7.0 /
2.5
|
YES
9.7 /
4.7
|
| FlurMukhopadhyay-SAS2012-Ex3.01_true-termination.c
|
YES
9.0 /
5.1
|
YES
21.8 /
16.9
|
| FlurMukhopadhyay-SAS2012-Ex3.03_true-termination.c
|
YES
30.9 /
9.0
|
YES
10.5 /
5.2
|
| FlurMukhopadhyay-SAS2012-Ex3.04_true-termination.c
|
YES
30.6 /
9.4
|
YES
21.4 /
16.2
|
| FlurMukhopadhyay-SAS2012-Ex3.05_true-termination.c
|
YES
25.5 /
9.0
|
YES
21.2 /
16.3
|
| FlurMukhopadhyay-SAS2012-Ex3.08_true-termination.c
|
YES
21.2 /
8.2
|
YES
21.1 /
22.9
|
| FlurMukhopadhyay-SAS2012-Ex3.09_true-termination.c
|
YES
13.3 /
7.4
|
YES
23.6 /
19.6
|
| FlurMukhopadhyay-SAS2012-Ex4.01_true-termination.c
|
YES
28.5 /
15.0
|
YES
17.8 /
12.5
|
| y/CookSeeZuleger-TACAS2013-Fig1_true-termination.c
|
YES
31.5 /
18.0
|
YES
15.0 /
9.5
|
| /CookSeeZuleger-TACAS2013-Fig7a_true-termination.c
|
YES
147.8 /
64.5
|
YES
12.8 /
5.7
|
| /CookSeeZuleger-TACAS2013-Fig7b_true-termination.c
|
YES
458.4 /
294.9
|
YES
14.5 /
6.6
|
| egory/GopanReps-CAV2006-Fig1a_true-termination.c.c
|
YES
16.6 /
6.3
|
YES
23.4 /
9.5
|
| lwaniJainKoskinen-PLDI2009-Fig1_true-termination.c
|
.
18.4 /
8.1
|
.
418.6 /
300.1
|
| risLalNoriRajamani-SAS2010-Fig1_true-termination.c
|
YES
453.1 /
300.1
|
YES
47.5 /
36.4
|
| isLalNoriRajamani-SAS2010-Fig2_false-termination.c
|
NO
401.3 /
300.1
|
NO
11.0 /
7.7
|
| risLalNoriRajamani-SAS2010-Fig3_true-termination.c
|
YES
12.9 /
4.3
|
YES
8.9 /
4.3
|
| ickeLeikePodelski-ATVA2013-Fig2_true-termination.c
|
.
9.3 /
3.4
|
.
21.4 /
11.3
|
| ickeLeikePodelski-ATVA2013-Fig5_true-termination.c
|
YES
8.6 /
4.8
|
.
32.5 /
14.2
|
| ickeLeikePodelski-ATVA2013-Fig6_true-termination.c
|
YES
9.4 /
3.5
|
YES
10.1 /
5.2
|
| ickeLeikePodelski-ATVA2013-Fig7_true-termination.c
|
YES
22.8 /
9.7
|
YES
14.8 /
9.5
|
| ickeLeikePodelski-ATVA2013-Fig8_true-termination.c
|
.
10.3 /
3.6
|
.
14.3 /
5.8
|
| ickeLeikePodelski-ATVA2013-Fig9_true-termination.c
|
.
10.8 /
5.0
|
.
31.4 /
6.5
|
| rSutre-POPL2002-LockingExample_false-termination.c
|
.
1118.0 /
300.0
|
NO
8.3 /
3.9
|
| itovichWintersteiger-CAV2010-Ex_true-termination.c
|
YES
98.1 /
29.3
|
YES
9.4 /
4.3
|
| ovichWintersteiger-CAV2010-Fig1_true-termination.c
|
.
607.0 /
300.0
|
YES
24.8 /
9.6
|
| C/SV-COMP_Termination_Category/LICENSE.txt
|
.
0.3 /
0.2
|
.
6.6 /
3.1
|
| z-CarbonellRubio-FMCAD2013-Fig1_true-termination.c
|
.
184.5 /
48.1
|
YES
33.8 /
24.6
|
| /LeeJonesBen-Amram-POPL2001-Ex1_true-termination.c
|
YES
8.8 /
5.0
|
YES
22.7 /
4.9
|
| /LeeJonesBen-Amram-POPL2001-Ex2_true-termination.c
|
YES
8.1 /
3.2
|
YES
22.4 /
15.4
|
| /LeeJonesBen-Amram-POPL2001-Ex3_true-termination.c
|
YES
9.6 /
3.3
|
.
444.3 /
300.0
|
| /LeeJonesBen-Amram-POPL2001-Ex4_true-termination.c
|
YES
11.2 /
4.3
|
YES
50.1 /
40.0
|
| /LeeJonesBen-Amram-POPL2001-Ex5_true-termination.c
|
YES
8.1 /
2.9
|
.
134.3 /
101.6
|
| /LeeJonesBen-Amram-POPL2001-Ex6_true-termination.c
|
YES
9.5 /
3.5
|
YES
12.5 /
5.6
|
| ory/LeikeHeizmann-TACAS2014-Ex9_true-termination.c
|
YES
25.6 /
5.6
|
YES
10.2 /
4.6
|
| egory/LeikeHeizmann-WST2014-Ex9_true-termination.c
|
.
5.8 /
2.6
|
YES
9.6 /
4.3
|
| _Category/Masse-VMCAI2014-Fig1b_true-termination.c
|
.
1119.5 /
300.1
|
.
17.1 /
6.5
|
| delskiRybalchenko-LICS2004-Fig2_true-termination.c
|
.
325.0 /
91.2
|
.
843.2 /
300.1
|
| elskiRybalchenko-TACAS2011-Fig4_true-termination.c
|
YES
49.2 /
17.7
|
YES
11.3 /
5.3
|
| delskiRybalchenko-VMCAI2004-Ex1_true-termination.c
|
YES
36.6 /
12.0
|
YES
23.6 /
16.8
|
| C/SV-COMP_Termination_Category/README.txt
|
.
0.3 /
0.3
|
.
6.4 /
2.9
|
| n_Category/TelAviv-Amir-Minimum_true-termination.c
|
.
1169.8 /
300.1
|
YES
26.5 /
10.9
|
| ategory/Toulouse-BranchesToLoop_true-termination.c
|
YES
14.2 /
6.2
|
YES
13.7 /
8.9
|
| ry/Toulouse-MultiBranchesToLoop_true-termination.c
|
YES
21.6 /
12.0
|
YES
16.8 /
7.9
|
| ategory/UrbanMine-ESOP2014-Fig3_true-termination.c
|
YES
299.2 /
203.1
|
YES
16.1 /
8.4
|
| OMP_Termination_Category/aaron2_true-termination.c
|
YES
41.6 /
16.3
|
YES
10.4 /
4.9
|
| OMP_Termination_Category/aaron3_true-termination.c
|
.
323.1 /
86.4
|
YES
28.2 /
19.5
|
| COMP_Termination_Category/aviad_true-termination.c
|
YES
45.5 /
28.9
|
YES
10.7 /
4.7
|
| -COMP_Termination_Category/gcd1_true-termination.c
|
YES
102.3 /
57.4
|
YES
15.7 /
7.6
|
| OMP_Termination_Category/genady_true-termination.c
|
YES
29.5 /
8.7
|
YES
10.6 /
5.6
|
| COMP_Termination_Category/joey_false-termination.c
|
.
7.4 /
2.7
|
NO
19.4 /
8.8
|
| OMP_Termination_Category/min_rf_true-termination.c
|
YES
374.7 /
236.5
|
YES
41.6 /
30.6
|
| ination_Category/svcomp_cstrcmp_true-termination.c
|
YES
21.9 /
12.9
|
.
417.4 /
300.0
|
| nation_Category/svcomp_cstrcspn_true-termination.c
|
YES
306.7 /
197.2
|
.
390.0 /
300.1
|
| ination_Category/svcomp_cstrlen_true-termination.c
|
YES
7.9 /
3.1
|
.
45.8 /
17.0
|
| nation_Category/svcomp_cstrncmp_true-termination.c
|
YES
37.8 /
21.5
|
YES
65.1 /
46.3
|
| nation_Category/svcomp_cstrpbrk_true-termination.c
|
YES
194.4 /
110.2
|
.
404.4 /
300.1
|
| ination_Category/svcomp_cstrspn_true-termination.c
|
YES
295.6 /
157.4
|
.
389.0 /
300.0
|
| mination_Category/svcomp_strchr_true-termination.c
|
YES
13.1 /
6.3
|
YES
26.9 /
12.9
|
| C/Ton_Chanh_15/Ackermann_false-termination.c
|
.
848.5 /
256.7
|
NO
9.8 /
4.5
|
| C/Ton_Chanh_15/Ackermann_true-termination.c
|
YES
12.7 /
6.4
|
.
555.1 /
300.0
|
| C/Ton_Chanh_15/Binary_Search_true-termination.c
|
.
9.8 /
4.1
|
NO
9.0 /
4.9
|
| n_Chanh_15/McCarthy91_Recursion_true-termination.c
|
.
12.1 /
5.8
|
YES
57.1 /
45.8
|
| on_Chanh_15/MutualRecursion_1a_false-termination.c
|
.
7.1 /
2.6
|
NO
16.0 /
9.7
|
| Ton_Chanh_15/MutualRecursion_1b_true-termination.c
|
.
44.6 /
29.0
|
.
518.5 /
300.1
|
| on_Chanh_15/NestedRecursion_1a_false-termination.c
|
.
958.8 /
300.1
|
NO
10.0 /
4.4
|
| Ton_Chanh_15/NestedRecursion_1b_true-termination.c
|
.
948.0 /
300.1
|
YES
27.4 /
16.0
|
| Ton_Chanh_15/NestedRecursion_1c_true-termination.c
|
YES
6.8 /
2.8
|
YES
12.8 /
6.5
|
| Ton_Chanh_15/NestedRecursion_1d_true-termination.c
|
YES
13.3 /
5.5
|
.
528.7 /
300.1
|
| on_Chanh_15/NestedRecursion_2a_false-termination.c
|
.
5.5 /
2.3
|
NO
9.5 /
5.1
|
| on_Chanh_15/NestedRecursion_2b_false-termination.c
|
.
6.2 /
2.3
|
NO
17.0 /
8.0
|
| Ton_Chanh_15/NestedRecursion_2c_true-termination.c
|
YES
7.0 /
2.5
|
.
414.4 /
300.1
|
| C/Ultimate/4BitCounterPointer_true-termination.c
|
YES
21.3 /
5.0
|
.
315.1 /
300.1
|
| ays01-EquivalentConstantIndices_true-termination.c
|
YES
6.1 /
3.0
|
YES
10.0 /
5.0
|
| ys02-EquivalentConstantIndices_false-termination.c
|
NO
5.4 /
2.8
|
NO
9.4 /
6.3
|
| ate/Arrays03-ValueRestictsIndex_true-termination.c
|
.
11.1 /
4.8
|
.
16.0 /
6.0
|
| C/Ultimate/Bangalore_true-termination.c
|
YES
7.3 /
3.6
|
YES
9.8 /
5.1
|
| C/Ultimate/Cairo_true-termination.c
|
YES
7.0 /
3.2
|
YES
10.3 /
4.9
|
| C/Ultimate/Collatz_unknown-termination.c
|
.
591.8 /
300.1
|
.
33.6 /
19.3
|
| C/Ultimate/Division_false-termination.c
|
NO
7.3 /
4.2
|
NO
8.1 /
3.9
|
| C/Ultimate/Gothenburg_true-termination.c
|
YES
56.1 /
23.7
|
YES
24.9 /
16.4
|
| C/Ultimate/LICENSE.txt
|
.
0.3 /
0.2
|
.
6.9 /
3.5
|
| C/Ultimate/LexIndexValue-Array_true-termination.c
|
.
7.6 /
3.2
|
.
355.0 /
300.1
|
| /Ultimate/LexIndexValue-Pointer_true-termination.c
|
.
7.9 /
2.8
|
.
354.9 /
300.1
|
| timate/Lobnya-Boolean-Reordered_true-termination.c
|
YES
7.9 /
3.2
|
YES
26.9 /
11.7
|
| C/Ultimate/Madrid_false-termination.c
|
NO
3.9 /
2.1
|
NO
8.6 /
4.1
|
| C/Ultimate/Mysore_true-termination.c
|
YES
14.7 /
5.9
|
YES
14.6 /
10.1
|
| C/Ultimate/NonTermination2_false-termination.c
|
.
834.5 /
300.1
|
NO
18.3 /
4.3
|
| C/Ultimate/NonTermination3_false-termination.c
|
.
3.9 /
1.7
|
.
9.0 /
4.2
|
| Ultimate/NonTerminationSimple2_false-termination.c
|
NO
5.3 /
2.5
|
NO
9.7 /
5.1
|
| Ultimate/NonTerminationSimple3_false-termination.c
|
NO
6.7 /
3.2
|
NO
8.1 /
3.8
|
| Ultimate/NonTerminationSimple4_false-termination.c
|
NO
8.2 /
3.7
|
NO
9.4 /
6.4
|
| Ultimate/NonTerminationSimple5_false-termination.c
|
.
1119.6 /
300.0
|
NO
12.6 /
6.4
|
| Ultimate/NonTerminationSimple6_false-termination.c
|
NO
5.8 /
3.6
|
NO
9.3 /
5.0
|
| Ultimate/NonTerminationSimple7_false-termination.c
|
NO
5.7 /
2.8
|
NO
8.4 /
4.0
|
| Ultimate/NonTerminationSimple8_false-termination.c
|
.
956.6 /
300.1
|
NO
9.4 /
4.9
|
| Ultimate/NonTerminationSimple9_false-termination.c
|
NO
5.7 /
2.9
|
NO
8.3 /
4.5
|
| C/Ultimate/Nyala-2lex_true-termination.c
|
YES
57.9 /
16.5
|
YES
11.8 /
5.5
|
| C/Ultimate/Parallel_true-termination.c
|
YES
10.9 /
4.7
|
YES
10.4 /
5.6
|
| C/Ultimate/Pure3Phase_true-termination.c
|
.
1151.2 /
300.0
|
YES
17.5 /
9.0
|
| C/Ultimate/README.txt
|
.
0.3 /
0.2
|
.
6.2 /
3.1
|
| ltimate/RecursiveMultiplication_true-termination.c
|
YES
9.2 /
3.9
|
YES
12.6 /
6.3
|
| timate/RecursiveNonterminating_false-termination.c
|
NO
7.2 /
2.9
|
NO
9.3 /
4.9
|
| C/Ultimate/Rotation180_false-termination.c
|
NO
6.3 /
3.0
|
NO
9.2 /
6.0
|
| C/Ultimate/Stockholm_true-termination.c
|
YES
11.3 /
4.7
|
YES
11.2 /
6.1
|
| Ultimate/SyntaxSupportPointer01_true-termination.c
|
YES
5.3 /
2.4
|
YES
12.3 /
5.6
|
| C/Ultimate/WhileFalse_true-termination.c
|
YES
3.5 /
1.8
|
YES
8.2 /
3.7
|
| C/Ultimate/WhileTrue_false-termination.c
|
NO
3.8 /
1.9
|
NO
8.2 /
3.8
|