Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 20:38:57 CET 2017-12-03 03:39:33 CET 2017-12-03 03:40:31 CET
Run set esbmc-kind.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Termination-MainHeap
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-02_2038.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_2038.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
termination-libowfat/atoi_true-termination.c.i 0 900     2700 13000    - -
termination-libowfat/atol_true-termination.c.i 0 900     2700 10000    - -
termination-libowfat/atoll_true-termination.c.i 0 900     2500 11000    - -
termination-libowfat/basename_true-termination.c.i 0 900     750 11000    - -
termination-libowfat/build_fullname_true-termination.c.i 0 900     1500 11000    - -
termination-libowfat/dirname_true-termination.c.i 0 900     5100 8500    - -
termination-libowfat/skip_to_true-termination.c.i 0 900     4100 12000    - -
termination-libowfat/stpcpy_true-termination.c.i 0 900     2800 10000    - -
termination-libowfat/strcasecmp_true-termination.c.i 0 900     1600 8900    - -
termination-libowfat/strcat_short_true-termination.c.i 0 900     2100 11000    - -
termination-libowfat/strcat_true-termination.c.i 0 900     2700 9100    - -
termination-libowfat/strchr_short_true-termination.c.i 0 900     1800 9700    - -
termination-libowfat/strchr_true-termination.c.i 0 900     1900 9800    - -
termination-libowfat/strcmp_short_true-termination.c.i 0 900     3400 9500    - -
termination-libowfat/strcpy_small_true-termination.c.i 0 900     2800 9300    - -
termination-libowfat/strcspn_true-termination.c.i 0 900     740 10000    - -
termination-libowfat/strdup_true-termination.c.i 0 900     1600 12000    - -
termination-libowfat/strlcat_true-termination.c.i 0 900     3500 9800    - -
termination-libowfat/strlcpy_true-termination.c.i 0 900     1000 11000    - -
termination-libowfat/strlen_true-termination.c.i 0 900     2300 12000    - -
termination-libowfat/strpbrk_true-termination.c.i 0 900     910 9400    - -
termination-libowfat/strrchr_short_true-termination.c.i 0 900     3000 12000    - -
termination-libowfat/strrchr_true-termination.c.i 0 900     2400 7800    - -
termination-libowfat/strspn_true-termination.c.i 0 900     1900 10000    - -
termination-libowfat/strstr_true-termination.c.i 0 900     3600 9300    - -
termination-libowfat/strtok_r_true-termination.c.i 0 900     1100 10000    - -
termination-libowfat/strtol_true-termination.c.i 0 900     8500 11000    - -
termination-libowfat/strtoul_true-termination.c.i 0 900     12000 9200    - -
termination-libowfat/strtoull_true-termination.c.i 0 900     11000 8900    - -
termination-libowfat/wcsrchr_true-termination.c.i 0 900     2600 11000    - -
termination-libowfat/wcsstr_true-termination.c.i 0 900     3500 9300    - -
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i 0 900     390 9200    0 .51 41 0 .020 4.9
termination-memory-alloca/Velroyen-alloca_false-termination.c.i 0 900     630 9700    0 .68 46 0 .018 4.9
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i 0 900     440 11000    - -
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i 0 900     200 12000    - -
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i 0 900     1400 10000    - -
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i 0 900     580 12000    - -
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i 0 900     300 11000    - -
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i 0 900     560 12000    - -
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i 0 900     620 9700    - -
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i 0 900     770 11000    - -
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i 0 900     560 12000    - -
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i 2 .12  27 .90 - -
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i 0 900     1000 10000    - -
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i 0 900     450 9800    - -
termination-memory-alloca/Masse-alloca_true-termination.c.i 0 900     100 11000    - -
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i 0 900     360 11000    - -
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i 0 900     290 11000    - -
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i 0 900     320 12000    - -
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i 0 900     340 11000    - -
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i 0 900     340 10000    - -
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i 0 900     1000 11000    - -
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i 0 900     4600 9700    - -
termination-memory-alloca/Urban-alloca_true-termination.c.i 0 900     700 9000    - -
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i 0 900     1300 9500    - -
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i 0 900     270 13000    - -
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i 0 900     300 11000    - -
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i 0 900     330 10000    - -
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i 0 900     360 11000    - -
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i 0 900     300 11000    - -
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i 0 900     300 11000    - -
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i 0 900     300 12000    - -
termination-memory-alloca/add_last-alloca_true-termination.c.i 0 900     910 13000    - -
termination-memory-alloca/array01-alloca_true-termination.c.i 0 900     600 13000    - -
termination-memory-alloca/array02-alloca_true-termination.c.i 0 900     320 13000    - -
termination-memory-alloca/array03-alloca_true-termination.c.i 0 900     1700 12000    - -
termination-memory-alloca/aviad_true-alloca_true-termination.c.i 2 4.8   30 57    - -
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i 0 900     310 11000    - -
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i 0 900     270 10000    - -
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i 0 900     180 11000    - -
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i 0 900     270 12000    - -
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i 2 .084 27 .81 - -
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i 0 900     690 11000    - -
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i 0 900     610 11000    - -
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i 0 900     390 11000    - -
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i 0 900     530 10000    - -
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i 0 900     670 9200    - -
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i 0 900     400 12000    - -
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i 0 900     390 12000    - -
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i 0 900     490 12000    - -
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i 0 900     500 11000    - -
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i 0 900     850 11000    - -
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i 0 900     930 8500    - -
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i 0 900     800 14000    - -
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i 0 900     1100 13000    - -
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i 0 900     1000 12000    - -
termination-memory-alloca/bubblesort-alloca_true-termination.c.i 0 900     5600 11000    - -
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i 0 900     1900 12000    - -
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i 0 900     1800 10000    - -
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i 0 900     1300 9500    - -
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i 0 900     320 10000    - -
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i 0 900     630 11000    - -
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i 0 900     1400 12000    - -
termination-memory-alloca/count_down-alloca_true-termination.c.i 0 900     390 13000    - -
termination-memory-alloca/cstrcat-alloca_true-termination.c.i 0 900     2000 10000    - -
termination-memory-alloca/cstrchr-alloca_true-termination.c.i 0 900     1200 11000    - -
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i 0 900     3300 9500    - -
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i 0 900     3000 9900    - -
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i 0 900     1500 8500    - -
termination-memory-alloca/cstrlen-alloca_true-termination.c.i 0 900     2400 10000    - -
termination-memory-alloca/cstrncat-alloca_true-termination.c.i 0 900     2100 10000    - -
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i 0 900     1600 11000    - -
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i 0 900     6200 7600    - -
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i 0 900     1600 7500    - -
termination-memory-alloca/cstrspn-alloca_true-termination.c.i 0 900     1600 8600    - -
termination-memory-alloca/diff-alloca_true-termination.c.i 0 900     260 11000    - -
termination-memory-alloca/easySum-alloca_true-termination.c.i 0 900     940 11000    - -
termination-memory-alloca/ex1-alloca_true-termination.c.i 0 900     560 10000    - -
termination-memory-alloca/ex2-alloca_true-termination.c.i 0 900     200 11000    - -
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i 2 .092 27 .99 - -
termination-memory-alloca/ex3b-alloca_true-termination.c.i 2 120     47 1500    - -
termination-memory-alloca/fermat-alloca_true-termination.c.i 0 900     4500 11000    - -
termination-memory-alloca/flag-alloca_true-termination.c.i 0 900     560 11000    - -
termination-memory-alloca/gcd1-alloca_true-termination.c.i 0 900     910 10000    - -
termination-memory-alloca/genady-alloca_true-termination.c.i 2 480     2800 6700    - -
termination-memory-alloca/insertionsort-alloca_true-termination.c.i 0 900     410 11000    - -
termination-memory-alloca/java_AG313-alloca_true-termination.c.i 0 900     210 9900    - -
termination-memory-alloca/java_Break-alloca_true-termination.c.i 2 .11  27 .85 - -
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i 0 900     3700 7200    - -
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i 2 .13  27 .88 - -
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i 2 .20  27 1.7  - -
termination-memory-alloca/java_Nested-alloca_true-termination.c.i 2 .092 27 1.0  - -
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i 2 .28  27 3.4  - -
termination-memory-alloca/lis-alloca_true-termination.c.i 0 900     9100 12000    - -
termination-memory-alloca/min_rf-alloca_true-termination.c.i 0 900     200 12000    - -
termination-memory-alloca/mult_array-alloca_true-termination.c.i 0 900     3800 8600    - -
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i 0 900     3500 10000    - -
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i 0 900     1300 11000    - -
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i 0 900     840 10000    - -
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i 0 900     3800 10000    - -
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i 0 900     2500 11000    - -
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i 0 900     7100 9400    - -
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i 0 900     1900 12000    - -
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i 0 900     2300 9200    - -
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i 0 900     2500 12000    - -
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i 0 900     1700 13000    - -
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i 0 900     860 11000    - -
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i 0 900     2000 9900    - -
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i 0 900     2300 9800    - -
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i 0 900     2300 9700    - -
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i 0 900     7100 9600    - -
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i 0 900     2000 11000    - -
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i 0 900     620 9900    - -
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i 0 900     380 10000    - -
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i 0 900     640 10000    - -
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i 0 900     1800 9900    - -
termination-memory-alloca/selectionsort-alloca_true-termination.c.i 0 900     3100 9000    - -
termination-memory-alloca/stroeder1-alloca_true-termination.c.i 0 900     1600 9900    - -
termination-memory-alloca/stroeder2-alloca_true-termination.c.i 0 900     1300 13000    - -
termination-memory-alloca/strreplace-alloca_true-termination.c.i 0 900     170 12000    - -
termination-memory-alloca/subseq-alloca_true-termination.c.i 0 900     2200 11000    - -
termination-memory-alloca/substring-alloca_true-termination.c.i 0 900     770 11000    - -
termination-memory-alloca/twisted-alloca_true-termination.c.i 2 .11  27 .91 - -
termination-memory-linkedlists/cll_by_lseg-alloca_false-termination.c.i 0 900     1700 12000    0 .53 42 0 .025 4.8
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i 0 900     3400 8000    0 .51 41 0 .018 4.8
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i 0 900     3800 9400    0 .61 42 0 .019 4.8
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i 0 900     4000 7800    0 .53 41 0 .023 4.8
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i 0 900     3300 9900    0 .74 44 0 .018 5.0
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i 0 900     3800 8800    0 .54 44 0 .018 4.8
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i 0 640     15000 5700    0 .43 41 0 .018 4.9
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i 0 900     4000 11000    0 .50 41 0 .018 5.0
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i 0 900     3900 8400    0 .54 43 0 .018 4.9
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i 0 700     15000 6100    - -
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i 0 900     3600 8900    - -
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i 0 900     3900 7800    - -
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i 0 900     3700 8000    - -
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i 0 630     15000 6200    - -
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i 0 900     3800 7400    - -
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i 0 900     3700 8400    - -
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i 0 900     3800 8700    - -
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i 0 900     3400 11000    - -
termination-15/add_first_alloca_true-termination.c.i 0 900     740 11000    - -
termination-15/array05_alloca_true-termination.c.i 0 900     310 12000    - -
termination-15/array06_alloca_true-termination.c.i 0 900     930 11000    - -
termination-15/array07_alloca_true-termination.c.i 0 900     930 13000    - -
termination-15/array08_alloca_true-termination.c.i 0 900     480 12000    - -
termination-15/array09_alloca_true-termination.c.i 0 900     700 13000    - -
termination-15/array10_alloca_true-termination.c.i 0 900     270 12000    - -
termination-15/array12_alloca_true-termination.c.i 0 900     1800 9900    - -
termination-15/array13_alloca_true-termination.c.i 0 900     1300 9600    - -
termination-15/array16_alloca_fixed_true-termination.c.i 0 900     1300 13000    - -
termination-15/array17_alloca_true-termination.c.i 0 900     230 11000    - -
termination-15/array18_alloca_true-termination.c.i 0 900     640 12000    - -
termination-15/count_up_alloca_true-termination.c.i 0 900     340 14000    - -
termination-15/count_up_and_down_alloca_true-termination.c.i 0 900     1000 11000    - -
termination-15/cstrcat_diffterm_alloca_true-termination.c.i 0 900     2000 10000    - -
termination-15/cstrcat_malloc_true-termination.c.i 0 900     2000 11000    - -
termination-15/cstrcat_mixed_alloca_true-termination.c.i 0 900     1900 12000    - -
termination-15/cstrcat_reverse_alloca_true-termination.c.i 0 900     1900 12000    - -
termination-15/cstrchr_diffterm_alloca_true-termination.c.i 0 900     1200 11000    - -
termination-15/cstrchr_malloc_true-termination.c.i 0 900     1200 10000    - -
termination-15/cstrchr_reverse_alloca_true-termination.c.i 0 900     1900 12000    - -
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i 0 900     3300 9800    - -
termination-15/cstrcmp_malloc_true-termination.c.i 0 900     3300 9500    - -
termination-15/cstrcmp_mixed_alloca_true-termination.c.i 0 900     3100 11000    - -
termination-15/cstrcmp_reverse_alloca_true-termination.c.i 0 900     3700 13000    - -
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i 0 900     3000 12000    - -
termination-15/cstrcpy_malloc_true-termination.c.i 0 900     3000 10000    - -
termination-15/cstrcpy_mixed_alloca_true-termination.c.i 0 900     2500 8600    - -
termination-15/cstrcpy_reverse_alloca_true-termination.c.i 0 900     2700 11000    - -
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i 0 900     1400 9300    - -
termination-15/cstrcspn_malloc_true-termination.c.i 0 900     1500 11000    - -
termination-15/cstrcspn_mixed_alloca_true-termination.c.i 0 900     1300 11000    - -
termination-15/cstrcspn_reverse_alloca_true-termination.c.i 0 900     1300 11000    - -
termination-15/cstrlen_diffterm_alloca_true-termination.c.i 0 900     2400 9800    - -
termination-15/cstrlen_malloc_true-termination.c.i 0 900     2300 10000    - -
termination-15/cstrlen_reverse_alloca_true-termination.c.i 0 900     2500 11000    - -
termination-15/cstrncat_diffterm_alloca_true-termination.c.i 0 900     2100 10000    - -
termination-15/cstrncat_malloc_true-termination.c.i 0 900     2100 9500    - -
termination-15/cstrncat_mixed_alloca_true-termination.c.i 0 900     2100 11000    - -
termination-15/cstrncat_reverse_alloca_true-termination.c.i 0 900     2100 12000    - -
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i 0 900     1600 11000    - -
termination-15/cstrncmp_malloc_true-termination.c.i 0 900     1600 12000    - -
termination-15/cstrncmp_mixed_alloca_true-termination.c.i 0 900     1700 10000    - -
termination-15/cstrncmp_reverse_alloca_true-termination.c.i 0 900     1900 10000    - -
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i 0 900     6200 9800    - -
termination-15/cstrncpy_malloc_true-termination.c.i 0 900     6400 11000    - -
termination-15/cstrncpy_mixed_alloca_true-termination.c.i 0 900     1700 9200    - -
termination-15/cstrncpy_reverse_alloca_true-termination.c.i 0 900     1700 8800    - -
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i 0 900     1800 8500    - -
termination-15/cstrpbrk_malloc_true-termination.c.i 0 900     1700 8500    - -
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i 0 900     1400 11000    - -
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i 0 900     1500 11000    - -
termination-15/cstrspn_diffterm_alloca_true-termination.c.i 0 900     1600 11000    - -
termination-15/cstrspn_malloc_true-termination.c.i 0 900     1600 8700    - -
termination-15/cstrspn_mixed_alloca_true-termination.c.i 0 900     1400 12000    - -
termination-15/cstrspn_reverse_alloca_true-termination.c.i 0 900     1500 10000    - -
termination-15/array04_alloca_false-termination.c.i 0 900     620 13000    0 .56 41 0 .024 4.8
termination-15/array14_alloca_false-termination.c.i 0 900     860 10000    0 .56 43 0 .018 4.9
termination-15/array15_alloca_false-termination.c.i 0 900     650 12000    0 .55 43 0 .018 5.0
termination-15/array16_alloca_original_false-termination.c.i 0 900     3000 10000    0 .52 42 0 .019 4.9
termination-15/array19_alloca_false-termination.c.i 0 900     380 13000    0 .54 43 0 .018 4.9
termination-15/array20_alloca_false-termination.c.i 0 900     330 10000    0 .51 41 0 .018 4.9
termination-recursive-malloc/chunk1_true-termination.c.i 0 900     1100 11000    - -
termination-recursive-malloc/chunk2_true-termination.c.i 0 900     12000 8400    - -
termination-recursive-malloc/chunk3_true-termination.c.i 0 900     9700 9200    - -
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i 0 900     5500 9800    - -
termination-recursive-malloc/mergeSort_true-termination.c.i 0 900     4800 7700    - -
termination-recursive-malloc/mutual_simple2_true-termination.c.i 0 900     2400 8700    - -
termination-recursive-malloc/mutual_simple_true-termination.c.i 0 900     1300 9800    - -
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i 0 900     5700 9700    - -
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i 0 900     2900 8900    - -
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i 0 900     3600 7300    - -
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i 0 900     3500 9100    - -
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i 0 900     3600 8100    - -
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i 0 900     3300 6500    - -
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i 0 900     5100 10000    - -
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i 0 900     4600 9900    - -
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i 0 900     4600 11000    - -
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i 0 900     6500 9100    - -
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i 0 900     8200 9700    - -
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i 0 900     8000 8000    - -
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i 0 900     4800 8900    - -
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i 0 900     4800 9200    - -
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i 0 900     6300 9700    - -
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i 0 900     3300 6600    - -
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i 0 900     2400 8900    - -
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i 0 900     3000 8500    - -
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i 0 900     1800 10000    - -
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i 0 900     2400 8200    - -
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 260 24 220000 590000 2600000 17 0 9.4 720 17 0 .33 83
    correct results 12 24 610 3100 8300 0 0
        correct true 12 24 610 3100 8300 0 0
        correct false 0 0 0
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (260 tasks, max score: 503) 24 0 0
Run set esbmc-kind.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Termination-MainHeap