Tool CBMC CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:48:40 CET 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET
Run set cbmc.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-termination.Termination-MainHeap
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
termination-libowfat/atoi_true-termination.c.i 0 880     880     13000   8400    8.8   0      - -
termination-libowfat/atol_true-termination.c.i 0 880     880     13000   8300    12     0      - -
termination-libowfat/atoll_true-termination.c.i 0 880     880     13000   8200    11     0      - -
termination-libowfat/basename_true-termination.c.i 0 880     880     4600   6100    72     0      - -
termination-libowfat/build_fullname_true-termination.c.i 0 880     880     14000   9300    3.2   .13   - -
termination-libowfat/dirname_true-termination.c.i 0 880     880     14000   8700    14     0      - -
termination-libowfat/skip_to_true-termination.c.i 0 880     880     1000   7700    2.9   0      - -
termination-libowfat/stpcpy_true-termination.c.i 0 880     880     14000   4600    6.5   0      - -
termination-libowfat/strcasecmp_true-termination.c.i 0 880     880     2200   9800    18     0      - -
termination-libowfat/strcat_short_true-termination.c.i 0 880     880     14000   6500    11     0      - -
termination-libowfat/strcat_true-termination.c.i 0 880     880     14000   8100    16     0      - -
termination-libowfat/strchr_short_true-termination.c.i 0 880     880     2700   7200    4.7   0      - -
termination-libowfat/strchr_true-termination.c.i 0 880     880     1100   7700    3.0   0      - -
termination-libowfat/strcmp_short_true-termination.c.i 0 880     880     6400   8600    6.5   0      - -
termination-libowfat/strcpy_small_true-termination.c.i 0 880     880     14000   4800    7.3   0      - -
termination-libowfat/strcspn_true-termination.c.i 0 880     880     240   5600    3.1   0      - -
termination-libowfat/strdup_true-termination.c.i 0 880     880     14000   5900    13     .13   - -
termination-libowfat/strlcat_true-termination.c.i 0 880     880     15000   6400    25     0      - -
termination-libowfat/strlcpy_true-termination.c.i 0 880     880     15000   6900    15     0      - -
termination-libowfat/strlen_true-termination.c.i 0 880     880     5200   3800    5.5   0      - -
termination-libowfat/strpbrk_true-termination.c.i 0 880     880     230   4000    3.0   0      - -
termination-libowfat/strrchr_short_true-termination.c.i 0 880     880     250   12000    2.6   0      - -
termination-libowfat/strrchr_true-termination.c.i 0 880     880     540   9200    13     0      - -
termination-libowfat/strspn_true-termination.c.i 0 880     880     1100   5900    35     0      - -
termination-libowfat/strstr_true-termination.c.i 0 870     880     660   10000    6.6   0      - -
termination-libowfat/strtok_r_true-termination.c.i 0 880     880     1100   7500    6.4   0      - -
termination-libowfat/strtol_true-termination.c.i 0 880     880     13000   7300    20     0      - -
termination-libowfat/strtoul_true-termination.c.i 0 880     880     14000   7500    17     0      - -
termination-libowfat/strtoull_true-termination.c.i 0 880     880     14000   6800    18     0      - -
termination-libowfat/wcsrchr_true-termination.c.i 0 880     880     1600   7400    6.3   0      - -
termination-libowfat/wcsstr_true-termination.c.i 0 880     880     1100   6400    34     0      - -
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i 0 880     880     1700   7900    5.0   0      0 .75 .46 40 0   0   0 .021 .022 5.6 0   0  
termination-memory-alloca/Velroyen-alloca_false-termination.c.i 0 880     880     1800   13000    13     0      0 .60 .36 42 0   0   0 .020 .021 5.7 0   0  
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i 0 880     880     3400   4200    11     0      - -
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i 0 880     880     990   7100    9.0   0      - -
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i 0 880     880     560   4700    39     0      - -
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i 0 880     880     4100   3700    7.2   0      - -
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i 0 880     880     3000   3300    9.5   0      - -
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i 0 880     880     1900   9600    13     0      - -
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i 0 880     880     980   9700    18     0      - -
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i 0 880     880     1300   10000    16     .070  - -
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i 0 880     880     1800   9600    9.7   0      - -
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i 2 .093 .091 7.4 .93 .016 0      - -
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i 0 880     880     1300   7500    4.8   0      - -
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i 0 880     880     1600   8900    10     0      - -
termination-memory-alloca/Masse-alloca_true-termination.c.i 0 880     880     280   9400    .54  .0041 - -
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i 0 880     880     640   8400    11     0      - -
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i 0 880     880     1500   8100    15     0      - -
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i 0 880     880     2000   9000    9.4   0      - -
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i 0 880     880     4400   5800    8.2   0      - -
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i 0 880     880     4400   6300    7.5   0      - -
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i 0 880     880     980   4100    13     0      - -
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i 0 880     880     3900   9800    120     .0041 - -
termination-memory-alloca/Urban-alloca_true-termination.c.i 0 880     880     3700   9600    19     0      - -
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i 0 880     880     560   4500    38     0      - -
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i 0 880     880     5000   3700    3.1   0      - -
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i 0 880     880     5300   5900    5.3   0      - -
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i 0 880     880     1600   9700    5.4   0      - -
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i 0 880     880     4000   5700    8.1   0      - -
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i 0 880     880     4900   6600    7.3   0      - -
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i 0 880     880     720   9600    2.3   0      - -
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i 0 880     880     1700   9800    8.1   0      - -
termination-memory-alloca/add_last-alloca_true-termination.c.i 0 870     880     13000   7000    7.8   .13   - -
termination-memory-alloca/array01-alloca_true-termination.c.i 0 880     880     14000   6300    72     0      - -
termination-memory-alloca/array02-alloca_true-termination.c.i 0 880     880     13000   6200    150     .13   - -
termination-memory-alloca/array03-alloca_true-termination.c.i 0 880     880     14000   5800    76     0      - -
termination-memory-alloca/aviad_true-alloca_true-termination.c.i 2 2.6   2.6   120   33    .75  0      - -
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i 0 880     880     5200   3800    3.6   0      - -
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i 0 880     880     4400   5600    7.0   0      - -
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i 0 880     880     4900   7300    5.8   0      - -
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i 0 880     880     710   9500    2.7   0      - -
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i 2 .084 .081 7.0 .64 .016 0      - -
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i 0 880     880     930   9100    10     0      - -
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i 0 880     880     4000   5700    10     0      - -
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i 0 880     880     4200   6400    8.1   0      - -
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i 0 880     880     1700   9200    11     .0082 - -
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i 0 880     880     150   10000    1.7   0      - -
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i 0 880     880     1400   7800    6.8   0      - -
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i 0 880     880     360   12000    2.3   0      - -
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i 0 880     880     380   11000    5.1   0      - -
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i 0 880     880     420   11000    3.9   0      - -
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i 0 880     880     1100   4800    86     0      - -
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i 0 870     880     870   4900    63     0      - -
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i 0 880     880     570   5000    38     0      - -
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i 0 880     880     570   7500    38     0      - -
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i 0 880     880     1200   5300    78     0      - -
termination-memory-alloca/bubblesort-alloca_true-termination.c.i 0 880     880     13000   6600    140     0      - -
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i 0 880     880     2100   13000    49     0      - -
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i 0 880     880     2200   11000    71     0      - -
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i 0 880     880     590   5400    38     0      - -
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i 0 880     880     2000   9800    9.5   0      - -
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i 0 880     880     1800   11000    12     0      - -
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i 0 870     880     560   4600    38     0      - -
termination-memory-alloca/count_down-alloca_true-termination.c.i 0 880     880     14000   6300    52     0      - -
termination-memory-alloca/cstrcat-alloca_true-termination.c.i 0 880     880     14000   5800    10     0      - -
termination-memory-alloca/cstrchr-alloca_true-termination.c.i 0 870     880     5700   6700    5.0   0      - -
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i 0 880     880     5000   5900    7.7   0      - -
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i 0 880     880     14000   4300    7.5   0      - -
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i 0 880     880     990   5500    52     0      - -
termination-memory-alloca/cstrlen-alloca_true-termination.c.i 0 880     880     6800   4900    3.4   0      - -
termination-memory-alloca/cstrncat-alloca_true-termination.c.i 0 880     880     14000   8700    14     0      - -
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i 0 880     880     1100   8800    5.6   0      - -
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i 0 880     880     14000   10000    83     0      - -
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i 0 880     880     990   6300    52     0      - -
termination-memory-alloca/cstrspn-alloca_true-termination.c.i 0 870     880     990   5600    51     0      - -
termination-memory-alloca/diff-alloca_true-termination.c.i 0 880     880     12000   5600    70     0      - -
termination-memory-alloca/easySum-alloca_true-termination.c.i 0 880     880     4400   4200    6.4   0      - -
termination-memory-alloca/ex1-alloca_true-termination.c.i 0 880     880     3600   3700    6.7   0      - -
termination-memory-alloca/ex2-alloca_true-termination.c.i 0 880     880     560   5500    1.1   0      - -
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i 2 .17  .16  11   1.4  .045 0      - -
termination-memory-alloca/ex3b-alloca_true-termination.c.i 2 8.2   8.2   56   110    .24  0      - -
termination-memory-alloca/fermat-alloca_true-termination.c.i 0 880     880     14000   12000    7.5   0      - -
termination-memory-alloca/flag-alloca_true-termination.c.i 0 880     880     2900   3600    7.4   0      - -
termination-memory-alloca/gcd1-alloca_true-termination.c.i 0 880     880     560   5200    38     0      - -
termination-memory-alloca/genady-alloca_true-termination.c.i 2 3.8   3.8   66   49    12     0      - -
termination-memory-alloca/insertionsort-alloca_true-termination.c.i 0 880     880     14000   10000    140     0      - -
termination-memory-alloca/java_AG313-alloca_true-termination.c.i 0 880     880     4300   5700    7.8   0      - -
termination-memory-alloca/java_Break-alloca_true-termination.c.i 2 .14  .14  8.3 1.6  .070 0      - -
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i 0 870     880     13000   5300    150     .0041 - -
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i 2 .21  .20  8.3 2.0  .13  0      - -
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i 2 .59  .59  16   6.9  .21  0      - -
termination-memory-alloca/java_Nested-alloca_true-termination.c.i 2 .20  .19  8.0 2.0  .23  0      - -
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i 2 .33  .32  8.2 4.0  .34  0      - -
termination-memory-alloca/lis-alloca_true-termination.c.i 0 870     880     14000   8900    250     .0041 - -
termination-memory-alloca/min_rf-alloca_true-termination.c.i 0 880     880     950   8600    3.3   0      - -
termination-memory-alloca/mult_array-alloca_true-termination.c.i 0 880     880     14000   5900    16     0      - -
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i 0 880     880     14000   4800    8.7   .13   - -
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i 0 880     880     1300   7500    6.8   0      - -
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i 0 880     880     13000   6400    6.5   0      - -
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i 0 880     880     14000   4300    8.8   0      - -
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i 0 880     880     14000   4100    9.2   0      - -
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i 0 880     880     14000   9900    86     0      - -
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i 0 880     880     14000   7400    15     0      - -
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i 0 880     880     1600   8100    7.9   0      - -
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i 0 880     880     14000   4500    9.2   0      - -
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i 0 880     880     330   4200    5.8   0      - -
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i 0 880     880     15000   7400    13     0      - -
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i 0 880     880     6200   3700    3.5   0      - -
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i 0 880     880     14000   6400    17     0      - -
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i 0 880     880     970   7100    12     0      - -
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i 0 880     880     14000   9900    86     0      - -
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i 0 880     880     990   8100    5.1   0      - -
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i 0 880     880     270   6600    5.9   0      - -
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i 0 880     880     740   7300    21     0      - -
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i 0 880     880     13000   10000    5.0   0      - -
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i 0 840     840     15000   4400    3.0   0      - -
termination-memory-alloca/selectionsort-alloca_true-termination.c.i 0 880     880     14000   6400    74     0      - -
termination-memory-alloca/stroeder1-alloca_true-termination.c.i 0 880     880     3300   3900    10     0      - -
termination-memory-alloca/stroeder2-alloca_true-termination.c.i 0 880     880     2400   4600    63     0      - -
termination-memory-alloca/strreplace-alloca_true-termination.c.i 0 880     880     13000   9400    8.7   .16   - -
termination-memory-alloca/subseq-alloca_true-termination.c.i 0 880     880     13000   8700    7.0   0      - -
termination-memory-alloca/substring-alloca_true-termination.c.i 0 880     880     1300   6700    75     0      - -
termination-memory-alloca/twisted-alloca_true-termination.c.i 2 .080 .077 7.0 .88 .016 0      - -
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i 0 880     880     6200   9600    61     0      0 .66 .40 42 0   0   0 .022 .022 5.6 0   0  
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i 0 880     880     9300   11000    14     0      0 .68 .42 42 0   0   0 .025 .026 5.7 0   0  
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i 0 880     880     9000   9800    14     0      0 .71 .45 41 0   0   0 .024 .025 5.6 0   0  
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i 0 880     880     8400   9900    11     0      0 .77 .48 40 0   0   0 .025 .027 5.7 0   0  
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i 0 880     880     12000   8700    11     0      0 .60 .37 41 0   0   0 .026 .027 5.6 0   0  
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i 0 880     880     9500   6200    12     0      0 .67 .40 41 0   0   0 .024 .026 5.7 0   0  
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i 0 880     880     13000   11000    12     0      0 .58 .35 42 0   0   0 .023 .024 5.6 0   0  
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i 0 870     880     12000   13000    14     0      0 .60 .37 42 0   0   0 .023 .024 5.6 0   0  
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i 0 880     880     8900   4900    12     0      - -
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i 0 880     880     9300   10000    14     0      - -
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i 0 880     880     8900   9200    16     0      - -
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i 0 880     880     10000   5800    13     0      - -
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i 0 880     880     9800   6100    11     0      - -
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i 0 880     880     2500   11000    62     0      - -
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i 0 880     880     2500   11000    60     0      - -
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i 0 880     880     4200   11000    62     0      - -
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i 0 880     880     13000   11000    14     0      - -
termination-15/add_first_alloca_true-termination.c.i 0 880     880     13000   6900    7.3   0      - -
termination-15/array05_alloca_true-termination.c.i 0 880     880     15000   9100    14     0      - -
termination-15/array06_alloca_true-termination.c.i 0 880     880     14000   8300    11     0      - -
termination-15/array07_alloca_true-termination.c.i 0 880     880     14000   10000    14     .13   - -
termination-15/array08_alloca_true-termination.c.i 0 880     880     14000   9700    15     0      - -
termination-15/array09_alloca_true-termination.c.i 0 880     880     14000   9200    14     0      - -
termination-15/array10_alloca_true-termination.c.i 0 870     880     15000   10000    16     .13   - -
termination-15/array12_alloca_true-termination.c.i 0 880     880     14000   8300    17     .13   - -
termination-15/array13_alloca_true-termination.c.i 0 880     880     14000   8800    15     0      - -
termination-15/array16_alloca_fixed_true-termination.c.i 0 870     880     14000   8300    16     .16   - -
termination-15/array17_alloca_true-termination.c.i 0 880     880     14000   7800    12     0      - -
termination-15/array18_alloca_true-termination.c.i 0 880     880     14000   8000    14     0      - -
termination-15/count_up_alloca_true-termination.c.i 0 880     880     14000   7100    50     0      - -
termination-15/count_up_and_down_alloca_true-termination.c.i 0 880     880     13000   7400    51     0      - -
termination-15/cstrcat_diffterm_alloca_true-termination.c.i 0 880     880     14000   6800    13     0      - -
termination-15/cstrcat_malloc_true-termination.c.i 0 110     110     13000   1100    .34  0      - -
termination-15/cstrcat_mixed_alloca_true-termination.c.i 0 880     880     14000   6300    13     .13   - -
termination-15/cstrcat_reverse_alloca_true-termination.c.i 0 880     880     14000   5600    14     .13   - -
termination-15/cstrchr_diffterm_alloca_true-termination.c.i 0 880     880     5600   6600    5.0   0      - -
termination-15/cstrchr_malloc_true-termination.c.i 0 880     880     5500   5500    4.7   0      - -
termination-15/cstrchr_reverse_alloca_true-termination.c.i 0 880     880     13000   5400    4.1   .13   - -
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i 0 880     880     5300   7500    7.7   0      - -
termination-15/cstrcmp_malloc_true-termination.c.i 0 880     880     5700   6800    5.6   0      - -
termination-15/cstrcmp_mixed_alloca_true-termination.c.i 0 880     880     13000   5300    6.2   0      - -
termination-15/cstrcmp_reverse_alloca_true-termination.c.i 0 880     880     13000   8000    6.6   0      - -
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i 0 880     880     14000   5000    8.9   0      - -
termination-15/cstrcpy_malloc_true-termination.c.i 0 150     150     13000   1600    1.2   0      - -
termination-15/cstrcpy_mixed_alloca_true-termination.c.i 0 880     880     14000   5800    6.8   0      - -
termination-15/cstrcpy_reverse_alloca_true-termination.c.i 0 870     880     14000   6400    8.6   0      - -
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i 0 880     880     990   5900    50     0      - -
termination-15/cstrcspn_malloc_true-termination.c.i 0 880     880     4200   6500    49     0      - -
termination-15/cstrcspn_mixed_alloca_true-termination.c.i 0 880     880     13000   7000    49     0      - -
termination-15/cstrcspn_reverse_alloca_true-termination.c.i 0 880     880     13000   7400    50     0      - -
termination-15/cstrlen_diffterm_alloca_true-termination.c.i 0 880     880     6300   3300    3.4   0      - -
termination-15/cstrlen_malloc_true-termination.c.i 0 880     880     6300   3500    2.7   0      - -
termination-15/cstrlen_reverse_alloca_true-termination.c.i 0 880     880     13000   4900    2.7   0      - -
termination-15/cstrncat_diffterm_alloca_true-termination.c.i 0 880     880     14000   7400    15     .13   - -
termination-15/cstrncat_malloc_true-termination.c.i 0 150     150     13000   1400    .40  0      - -
termination-15/cstrncat_mixed_alloca_true-termination.c.i 0 870     880     14000   7200    16     0      - -
termination-15/cstrncat_reverse_alloca_true-termination.c.i 0 880     880     14000   7100    16     0      - -
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i 0 880     880     1100   9100    5.6   0      - -
termination-15/cstrncmp_malloc_true-termination.c.i 0 880     880     1400   11000    4.5   0      - -
termination-15/cstrncmp_mixed_alloca_true-termination.c.i 0 880     880     13000   8200    5.4   0      - -
termination-15/cstrncmp_reverse_alloca_true-termination.c.i 0 880     880     13000   6600    5.3   0      - -
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i 0 880     880     14000   9500    83     0      - -
termination-15/cstrncpy_malloc_true-termination.c.i 0 270     270     13000   3100    4.7   0      - -
termination-15/cstrncpy_mixed_alloca_true-termination.c.i 0 880     880     14000   9300    83     0      - -
termination-15/cstrncpy_reverse_alloca_true-termination.c.i 0 880     880     14000   11000    83     0      - -
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i 0 880     880     990   5500    51     0      - -
termination-15/cstrpbrk_malloc_true-termination.c.i 0 880     880     4200   8000    49     0      - -
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i 0 880     880     13000   6200    49     0      - -
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i 0 880     880     13000   7000    50     .0041 - -
termination-15/cstrspn_diffterm_alloca_true-termination.c.i 0 880     880     990   7700    51     0      - -
termination-15/cstrspn_malloc_true-termination.c.i 0 880     880     4200   5300    50     0      - -
termination-15/cstrspn_mixed_alloca_true-termination.c.i 0 880     880     13000   7600    49     0      - -
termination-15/cstrspn_reverse_alloca_true-termination.c.i 0 870     880     13000   6500    49     0      - -
termination-15/array04_alloca_false-termination.c.i 0 880     880     14000   7400    12     0      0 .78 .49 41 0   0   0 .021 .021 5.6 0   0  
termination-15/array14_alloca_false-termination.c.i 0 880     880     14000   10000    15     0      0 .60 .37 40 0   0   0 .026 .027 5.6 0   0  
termination-15/array15_alloca_false-termination.c.i 0 880     880     14000   11000    17     0      0 .76 .46 42 0   0   0 .022 .023 5.8 0   0  
termination-15/array16_alloca_original_false-termination.c.i 0 880     880     14000   9700    16     0      0 .72 .45 41 0   0   0 .024 .024 5.6 0   0  
termination-15/array19_alloca_false-termination.c.i 0 880     880     14000   6700    12     0      0 .61 .38 40 0   0   0 .023 .025 5.7 0   0  
termination-15/array20_alloca_false-termination.c.i 0 880     880     14000   8800    17     0      0 .70 .43 40 0   0   0 .021 .022 5.6 0   0  
termination-recursive-malloc/chunk1_true-termination.c.i 0 540     540     15000   2800    6.3   0      - -
termination-recursive-malloc/chunk2_true-termination.c.i 0 .12  .12  6.6 .51 .012 0      - -
termination-recursive-malloc/chunk3_true-termination.c.i 0 .066 .065 7.7 .75 .012 0      - -
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i 0 880     880     14000   9100    31     0      - -
termination-recursive-malloc/mergeSort_true-termination.c.i 0 87     87     14000   960    .020 0      - -
termination-recursive-malloc/mutual_simple2_true-termination.c.i 0 450     450     8200   3600    3.7   0      - -
termination-recursive-malloc/mutual_simple_true-termination.c.i 0 880     880     15000   8000    9.4   0      - -
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i 0 880     880     7300   7900    8.2   0      - -
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i 0 870     880     970   5400    11     0      - -
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i 0 880     880     940   6100    5.7   0      - -
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i 0 880     880     960   6100    10     0      - -
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i 0 880     880     1100   6100    3.9   0      - -
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i 0 880     880     1300   4600    9.5   0      - -
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i 0 870     880     1100   4500    11     0      - -
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i 0 880     880     620   3600    6.5   0      - -
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i 0 880     880     7600   7600    9.2   0      - -
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i 0 880     880     680   5000    11     0      - -
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i 0 450     450     770   2800    4.7   0      - -
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i 0 600     600     15000   3600    11     0      - -
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i 0 750     750     10000   6500    6.5   0      - -
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i 0 840     840     10000   7500    6.9   0      - -
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i 0 160     160     3800   1500    3.7   0      - -
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i 0 880     880     1300   4700    8.4   .13   - -
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i 0 330     330     14000   3500    1.4   0      - -
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i 0 160     160     13000   1800    .96  0      - -
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i 0 810     810     15000   5600    3.2   0      - -
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i 0 880     880     14000   7100    75     0      - -
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 259 24 210000 210000 1900000 1700000 5600 2.1 16 0 11 6.6 650 0   0   16 0 .37 .39 90 0   0  
    correct results 12 24 16 16 330 210 14 0   0 0
        correct true 12 24 16 16 330 210 14 0   0 0
        correct false 0 0 0
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (259 tasks, max score: 502) 24 0 0
Run set cbmc.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-termination.Termination-MainHeap