Overview of job-results

flexible query (experimental) | view original jobs on star-exec:5391,

Statistics

1293 pairs, 71980.7 / 43108.1 s

Results

Legend

YES NO MAYBE CERTIFIED ERROR OTHER / Nothing
The results are displayed in the following pattern: cpu-time / wallclock-time (complexity-score)
Jobs C 20252
Solver AProVE_JRE2 UltimateBuchiAutomizer T2 - 2014-07-06v1
Scores 296 271 183
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