Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 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-01 15:15:10 CET 2017-12-01 21:58:57 CET 2017-12-01 21:59:47 CET
Run set depthk.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Termination-MainHeap
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_1515.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/depthk.2017-12-01_1515.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 unknown 0 wit inspect 1.5  57 19   - wit inspect - wit inspect
termination-libowfat/atol_true-termination.c.i unknown 0 wit inspect 1.5  58 20   - wit inspect - wit inspect
termination-libowfat/atoll_true-termination.c.i unknown 0 wit inspect 1.5  56 15   - wit inspect - wit inspect
termination-libowfat/basename_true-termination.c.i unknown 0 wit inspect 900    350 11000   - wit inspect - wit inspect
termination-libowfat/build_fullname_true-termination.c.i unknown 0 wit inspect 900    100 9600   - wit inspect - wit inspect
termination-libowfat/dirname_true-termination.c.i unknown 0 wit inspect 10    160 120   - wit inspect - wit inspect
termination-libowfat/skip_to_true-termination.c.i unknown 0 wit inspect 1.5  58 18   - wit inspect - wit inspect
termination-libowfat/stpcpy_true-termination.c.i unknown 0 wit inspect 84    29 1100   - wit inspect - wit inspect
termination-libowfat/strcasecmp_true-termination.c.i unknown 0 wit inspect 1.6  56 16   - wit inspect - wit inspect
termination-libowfat/strcat_short_true-termination.c.i unknown 0 wit inspect 1.5  57 16   - wit inspect - wit inspect
termination-libowfat/strcat_true-termination.c.i unknown 0 wit inspect 1.7  57 19   - wit inspect - wit inspect
termination-libowfat/strchr_short_true-termination.c.i unknown 0 wit inspect 1.5  56 17   - wit inspect - wit inspect
termination-libowfat/strchr_true-termination.c.i unknown 0 wit inspect 1.7  58 19   - wit inspect - wit inspect
termination-libowfat/strcmp_short_true-termination.c.i unknown 0 wit inspect 1.5  56 17   - wit inspect - wit inspect
termination-libowfat/strcpy_small_true-termination.c.i unknown 0 wit inspect 84    29 1100   - wit inspect - wit inspect
termination-libowfat/strcspn_true-termination.c.i unknown 0 wit inspect 6.7  69 94   - wit inspect - wit inspect
termination-libowfat/strdup_true-termination.c.i unknown 0 wit inspect 97    33 1100   - wit inspect - wit inspect
termination-libowfat/strlcat_true-termination.c.i unknown 0 wit inspect 1.6  56 22   - wit inspect - wit inspect
termination-libowfat/strlcpy_true-termination.c.i unknown 0 wit inspect 120    68 1400   - wit inspect - wit inspect
termination-libowfat/strlen_true-termination.c.i unknown 0 wit inspect 1.4  56 16   - wit inspect - wit inspect
termination-libowfat/strpbrk_true-termination.c.i unknown 0 wit inspect 5.8  64 73   - wit inspect - wit inspect
termination-libowfat/strrchr_short_true-termination.c.i unknown 0 wit inspect 1.5  56 18   - wit inspect - wit inspect
termination-libowfat/strrchr_true-termination.c.i unknown 0 wit inspect 1.6  56 23   - wit inspect - wit inspect
termination-libowfat/strspn_true-termination.c.i unknown 0 wit inspect 2.0  56 26   - wit inspect - wit inspect
termination-libowfat/strstr_true-termination.c.i unknown 0 wit inspect 900    610 12000   - wit inspect - wit inspect
termination-libowfat/strtok_r_true-termination.c.i unknown 0 wit inspect 7.4  83 88   - wit inspect - wit inspect
termination-libowfat/strtol_true-termination.c.i unknown 0 wit inspect 1.7  57 18   - wit inspect - wit inspect
termination-libowfat/strtoul_true-termination.c.i unknown 0 wit inspect 1.7  57 20   - wit inspect - wit inspect
termination-libowfat/strtoull_true-termination.c.i unknown 0 wit inspect 1.7  56 17   - wit inspect - wit inspect
termination-libowfat/wcsrchr_true-termination.c.i unknown 0 wit inspect 1.5  57 16   - wit inspect - wit inspect
termination-libowfat/wcsstr_true-termination.c.i unknown 0 wit inspect 3.2  57 42   - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i true -32 wit inspect .83 28 10   error (1) 0 wit inspect .68 45 false(termination) 1 wit inspect 5.9 260
termination-memory-alloca/Velroyen-alloca_false-termination.c.i true -32 wit inspect .88 29 11   error (1) 0 wit inspect .64 45 false(termination) 1 wit inspect 9.5 400
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i true 2 wit inspect .90 29 11   - wit inspect - wit inspect
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i true 2 wit inspect .90 28 10   - wit inspect - wit inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i true 2 wit inspect 1.1  28 14   - wit inspect - wit inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i true 2 wit inspect .86 28 11   - wit inspect - wit inspect
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i true 2 wit inspect .86 29 11   - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i true 2 wit inspect .86 29 12   - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i true 2 wit inspect .90 29 10   - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i true 2 wit inspect .92 28 11   - wit inspect - wit inspect
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i true 2 wit inspect .87 28 11   - wit inspect - wit inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i true 2 wit inspect .97 29 15   - wit inspect - wit inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i true 2 wit inspect .87 28 11   - wit inspect - wit inspect
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i true 2 wit inspect .87 28 11   - wit inspect - wit inspect
termination-memory-alloca/Masse-alloca_true-termination.c.i true 2 wit inspect .85 29 10   - wit inspect - wit inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i true 2 wit inspect .89 29 11   - wit inspect - wit inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i true 2 wit inspect .91 29 11   - wit inspect - wit inspect
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i true 2 wit inspect .89 29 11   - wit inspect - wit inspect
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i true 2 wit inspect .87 29 11   - wit inspect - wit inspect
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i true 2 wit inspect .92 29 11   - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i true 2 wit inspect .88 29 11   - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i true 2 wit inspect .85 28 11   - wit inspect - wit inspect
termination-memory-alloca/Urban-alloca_true-termination.c.i true 2 wit inspect .91 28 12   - wit inspect - wit inspect
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 1.1  29 16   - wit inspect - wit inspect
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .84 28 11   - wit inspect - wit inspect
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .86 29 12   - wit inspect - wit inspect
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .92 35 13   - wit inspect - wit inspect
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .86 29 12   - wit inspect - wit inspect
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .85 29 11   - wit inspect - wit inspect
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .89 29 9.5 - wit inspect - wit inspect
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .86 29 13   - wit inspect - wit inspect
termination-memory-alloca/add_last-alloca_true-termination.c.i true 2 wit inspect 1.1  28 15   - wit inspect - wit inspect
termination-memory-alloca/array01-alloca_true-termination.c.i true 2 wit inspect 3.0  51 42   - wit inspect - wit inspect
termination-memory-alloca/array02-alloca_true-termination.c.i true 2 wit inspect 5.1  96 61   - wit inspect - wit inspect
termination-memory-alloca/array03-alloca_true-termination.c.i true 2 wit inspect 3.4  60 47   - wit inspect - wit inspect
termination-memory-alloca/aviad_true-alloca_true-termination.c.i true 2 wit inspect .86 29 12   - wit inspect - wit inspect
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .83 28 12   - wit inspect - wit inspect
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .87 28 10   - wit inspect - wit inspect
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .85 28 10   - wit inspect - wit inspect
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .88 28 9.8 - wit inspect - wit inspect
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .86 29 11   - wit inspect - wit inspect
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .87 28 9.5 - wit inspect - wit inspect
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .87 28 9.9 - wit inspect - wit inspect
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .85 29 11   - wit inspect - wit inspect
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .87 29 13   - wit inspect - wit inspect
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .90 29 12   - wit inspect - wit inspect
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .92 29 10   - wit inspect - wit inspect
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .93 29 11   - wit inspect - wit inspect
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .89 29 11   - wit inspect - wit inspect
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .89 29 13   - wit inspect - wit inspect
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 1.4  31 20   - wit inspect - wit inspect
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 1.3  29 18   - wit inspect - wit inspect
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 1.1  29 13   - wit inspect - wit inspect
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 1.2  28 17   - wit inspect - wit inspect
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 1.4  29 20   - wit inspect - wit inspect
termination-memory-alloca/bubblesort-alloca_true-termination.c.i true 2 wit inspect 4.8  93 58   - wit inspect - wit inspect
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 1.2  29 15   - wit inspect - wit inspect
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 1.3  29 15   - wit inspect - wit inspect
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 1.1  28 16   - wit inspect - wit inspect
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .89 29 11   - wit inspect - wit inspect
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .90 29 11   - wit inspect - wit inspect
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 1.2  29 13   - wit inspect - wit inspect
termination-memory-alloca/count_down-alloca_true-termination.c.i true 2 wit inspect 3.0  49 34   - wit inspect - wit inspect
termination-memory-alloca/cstrcat-alloca_true-termination.c.i unknown 0 wit inspect 110    35 1400   - wit inspect - wit inspect
termination-memory-alloca/cstrchr-alloca_true-termination.c.i true 2 wit inspect 1.0  29 13   - wit inspect - wit inspect
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i true 2 wit inspect 1.1  29 12   - wit inspect - wit inspect
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i unknown 0 wit inspect 90    29 1200   - wit inspect - wit inspect
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i true 2 wit inspect 1.7  29 19   - wit inspect - wit inspect
termination-memory-alloca/cstrlen-alloca_true-termination.c.i true 2 wit inspect 1.0  28 12   - wit inspect - wit inspect
termination-memory-alloca/cstrncat-alloca_true-termination.c.i true 2 wit inspect 1.1  29 13   - wit inspect - wit inspect
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i unknown 0 wit inspect 120    62 1500   - wit inspect - wit inspect
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i timeout 0 wit inspect 900    870 11000   - wit inspect - wit inspect
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i true 2 wit inspect 1.6  28 23   - wit inspect - wit inspect
termination-memory-alloca/cstrspn-alloca_true-termination.c.i true 2 wit inspect 1.7  29 20   - wit inspect - wit inspect
termination-memory-alloca/diff-alloca_true-termination.c.i true 2 wit inspect 2.5  40 32   - wit inspect - wit inspect
termination-memory-alloca/easySum-alloca_true-termination.c.i true 2 wit inspect .85 28 13   - wit inspect - wit inspect
termination-memory-alloca/ex1-alloca_true-termination.c.i true 2 wit inspect .85 29 12   - wit inspect - wit inspect
termination-memory-alloca/ex2-alloca_true-termination.c.i true 2 wit inspect .90 29 12   - wit inspect - wit inspect
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .85 29 12   - wit inspect - wit inspect
termination-memory-alloca/ex3b-alloca_true-termination.c.i true 2 wit inspect .87 28 11   - wit inspect - wit inspect
termination-memory-alloca/fermat-alloca_true-termination.c.i true 2 wit inspect .86 29 9.9 - wit inspect - wit inspect
termination-memory-alloca/flag-alloca_true-termination.c.i true 2 wit inspect .86 28 11   - wit inspect - wit inspect
termination-memory-alloca/gcd1-alloca_true-termination.c.i true 2 wit inspect 1.2  29 15   - wit inspect - wit inspect
termination-memory-alloca/genady-alloca_true-termination.c.i true 2 wit inspect .82 29 10   - wit inspect - wit inspect
termination-memory-alloca/insertionsort-alloca_true-termination.c.i true 2 wit inspect 2.2  36 25   - wit inspect - wit inspect
termination-memory-alloca/java_AG313-alloca_true-termination.c.i true 2 wit inspect .85 28 10   - wit inspect - wit inspect
termination-memory-alloca/java_Break-alloca_true-termination.c.i true 2 wit inspect .84 28 11   - wit inspect - wit inspect
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i true 2 wit inspect 7.3  120 89   - wit inspect - wit inspect
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i true 2 wit inspect .81 28 10   - wit inspect - wit inspect
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i true 2 wit inspect .85 28 9.5 - wit inspect - wit inspect
termination-memory-alloca/java_Nested-alloca_true-termination.c.i true 2 wit inspect .87 29 13   - wit inspect - wit inspect
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i true 2 wit inspect .86 29 10   - wit inspect - wit inspect
termination-memory-alloca/lis-alloca_true-termination.c.i true 2 wit inspect 3.6  110 38   - wit inspect - wit inspect
termination-memory-alloca/min_rf-alloca_true-termination.c.i true 2 wit inspect .92 29 11   - wit inspect - wit inspect
termination-memory-alloca/mult_array-alloca_true-termination.c.i true 2 wit inspect 1.1  29 13   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i unknown 0 wit inspect 82    29 1200   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i unknown 0 wit inspect 89    32 1100   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i unknown 0 wit inspect 83    29 1200   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i unknown 0 wit inspect 80    30 1200   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i unknown 0 wit inspect 86    29 1100   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i timeout 0 wit inspect 900    820 12000   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i unknown 0 wit inspect 100    35 1600   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i unknown 0 wit inspect 100    41 1300   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i unknown 0 wit inspect 86    31 1000   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i timeout 0 wit inspect 900    1100 11000   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i unknown 0 wit inspect 120    71 1700   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i true 2 wit inspect 1.0  29 13   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i unknown 0 wit inspect 120    45 1800   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i unknown 0 wit inspect 120    58 1500   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i timeout 0 wit inspect 900    820 11000   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i true 2 wit inspect 1.0  29 13   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i unknown 0 wit inspect 900    290 13000   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i unknown 0 wit inspect 900    510 9400   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i unknown 0 wit inspect 900    220 10000   - wit inspect - wit inspect
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i true 2 wit inspect 1.0  28 12   - wit inspect - wit inspect
termination-memory-alloca/selectionsort-alloca_true-termination.c.i true 2 wit inspect 2.3  39 33   - wit inspect - wit inspect
termination-memory-alloca/stroeder1-alloca_true-termination.c.i true 2 wit inspect 1.0  29 15   - wit inspect - wit inspect
termination-memory-alloca/stroeder2-alloca_true-termination.c.i true 2 wit inspect 1.7  31 20   - wit inspect - wit inspect
termination-memory-alloca/strreplace-alloca_true-termination.c.i true 2 wit inspect 1.1  29 13   - wit inspect - wit inspect
termination-memory-alloca/subseq-alloca_true-termination.c.i true 2 wit inspect 1.1  29 13   - wit inspect - wit inspect
termination-memory-alloca/substring-alloca_true-termination.c.i true 2 wit inspect 3.3  43 43   - wit inspect - wit inspect
termination-memory-alloca/twisted-alloca_true-termination.c.i true 2 wit inspect .88 28 11   - wit inspect - wit inspect
termination-memory-linkedlists/cll_by_lseg-alloca_false-termination.c.i true -32 wit inspect .89 29 11   error (1) 0 wit inspect .60 47 unknown 0 wit inspect 29   920
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i true -32 wit inspect 1.0  29 15   error (1) 0 wit inspect .70 46 false(termination) 1 wit inspect 14   500
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i true -32 wit inspect 1.1  29 13   error (1) 0 wit inspect .68 45 false(termination) 1 wit inspect 12   460
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i true -32 wit inspect 1.1  29 13   error (1) 0 wit inspect .72 45 false(termination) 1 wit inspect 12   500
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i true -32 wit inspect 1.1  29 15   error (1) 0 wit inspect .63 48 false(termination) 1 wit inspect 15   560
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i true -32 wit inspect 1.1  29 12   error (1) 0 wit inspect .62 48 false(termination) 1 wit inspect 37   1400
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i true -32 wit inspect .94 28 13   error (1) 0 wit inspect .59 47 unknown 0 wit inspect 19   610
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i true -32 wit inspect 1.1  29 13   error (1) 0 wit inspect .64 45 false(termination) 1 wit inspect 12   500
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i true -32 wit inspect 1.1  29 13   error (1) 0 wit inspect .63 48 false(termination) 1 wit inspect 12   490
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i true 2 wit inspect .94 28 13   - wit inspect - wit inspect
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i true 2 wit inspect 1.2  29 15   - wit inspect - wit inspect
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i true 2 wit inspect 1.2  29 17   - wit inspect - wit inspect
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i true 2 wit inspect 1.2  29 18   - wit inspect - wit inspect
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i true 2 wit inspect .91 29 14   - wit inspect - wit inspect
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i true 2 wit inspect 1.0  29 15   - wit inspect - wit inspect
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i true 2 wit inspect 1.0  29 13   - wit inspect - wit inspect
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i true 2 wit inspect .96 28 12   - wit inspect - wit inspect
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i true 2 wit inspect 1.3  29 16   - wit inspect - wit inspect
termination-15/add_first_alloca_true-termination.c.i unknown 0 wit inspect 1.5  55 19   - wit inspect - wit inspect
termination-15/array05_alloca_true-termination.c.i unknown 0 wit inspect 1.6  58 18   - wit inspect - wit inspect
termination-15/array06_alloca_true-termination.c.i unknown 0 wit inspect 1.6  57 20   - wit inspect - wit inspect
termination-15/array07_alloca_true-termination.c.i unknown 0 wit inspect 1.6  57 19   - wit inspect - wit inspect
termination-15/array08_alloca_true-termination.c.i unknown 0 wit inspect 1.6  56 18   - wit inspect - wit inspect
termination-15/array09_alloca_true-termination.c.i unknown 0 wit inspect 1.6  56 16   - wit inspect - wit inspect
termination-15/array10_alloca_true-termination.c.i unknown 0 wit inspect 1.6  56 18   - wit inspect - wit inspect
termination-15/array12_alloca_true-termination.c.i unknown 0 wit inspect 1.6  56 21   - wit inspect - wit inspect
termination-15/array13_alloca_true-termination.c.i unknown 0 wit inspect 1.6  57 21   - wit inspect - wit inspect
termination-15/array16_alloca_fixed_true-termination.c.i unknown 0 wit inspect 1.6  57 18   - wit inspect - wit inspect
termination-15/array17_alloca_true-termination.c.i unknown 0 wit inspect 1.6  57 22   - wit inspect - wit inspect
termination-15/array18_alloca_true-termination.c.i unknown 0 wit inspect 1.6  57 18   - wit inspect - wit inspect
termination-15/count_up_alloca_true-termination.c.i unknown 0 wit inspect 3.4  57 45   - wit inspect - wit inspect
termination-15/count_up_and_down_alloca_true-termination.c.i unknown 0 wit inspect 3.4  56 50   - wit inspect - wit inspect
termination-15/cstrcat_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 110    35 1300   - wit inspect - wit inspect
termination-15/cstrcat_malloc_true-termination.c.i unknown 0 wit inspect 110    35 1400   - wit inspect - wit inspect
termination-15/cstrcat_mixed_alloca_true-termination.c.i unknown 0 wit inspect 110    48 1500   - wit inspect - wit inspect
termination-15/cstrcat_reverse_alloca_true-termination.c.i unknown 0 wit inspect 120    58 1600   - wit inspect - wit inspect
termination-15/cstrchr_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 1.5  56 18   - wit inspect - wit inspect
termination-15/cstrchr_malloc_true-termination.c.i unknown 0 wit inspect 1.5  57 17   - wit inspect - wit inspect
termination-15/cstrchr_reverse_alloca_true-termination.c.i unknown 0 wit inspect 1.5  57 17   - wit inspect - wit inspect
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 1.5  55 19   - wit inspect - wit inspect
termination-15/cstrcmp_malloc_true-termination.c.i unknown 0 wit inspect 1.5  56 18   - wit inspect - wit inspect
termination-15/cstrcmp_mixed_alloca_true-termination.c.i unknown 0 wit inspect 1.5  56 17   - wit inspect - wit inspect
termination-15/cstrcmp_reverse_alloca_true-termination.c.i unknown 0 wit inspect 1.5  57 18   - wit inspect - wit inspect
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 90    30 1300   - wit inspect - wit inspect
termination-15/cstrcpy_malloc_true-termination.c.i unknown 0 wit inspect 90    30 1300   - wit inspect - wit inspect
termination-15/cstrcpy_mixed_alloca_true-termination.c.i unknown 0 wit inspect 95    31 1200   - wit inspect - wit inspect
termination-15/cstrcpy_reverse_alloca_true-termination.c.i unknown 0 wit inspect 99    41 1300   - wit inspect - wit inspect
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 2.1  56 27   - wit inspect - wit inspect
termination-15/cstrcspn_malloc_true-termination.c.i unknown 0 wit inspect 2.2  56 27   - wit inspect - wit inspect
termination-15/cstrcspn_mixed_alloca_true-termination.c.i unknown 0 wit inspect 2.2  56 28   - wit inspect - wit inspect
termination-15/cstrcspn_reverse_alloca_true-termination.c.i unknown 0 wit inspect 2.2  57 29   - wit inspect - wit inspect
termination-15/cstrlen_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 1.5  57 17   - wit inspect - wit inspect
termination-15/cstrlen_malloc_true-termination.c.i unknown 0 wit inspect 1.5  56 15   - wit inspect - wit inspect
termination-15/cstrlen_reverse_alloca_true-termination.c.i unknown 0 wit inspect 1.5  57 16   - wit inspect - wit inspect
termination-15/cstrncat_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 1.6  57 19   - wit inspect - wit inspect
termination-15/cstrncat_malloc_true-termination.c.i unknown 0 wit inspect 1.6  56 18   - wit inspect - wit inspect
termination-15/cstrncat_mixed_alloca_true-termination.c.i unknown 0 wit inspect 1.6  57 18   - wit inspect - wit inspect
termination-15/cstrncat_reverse_alloca_true-termination.c.i unknown 0 wit inspect 1.6  56 16   - wit inspect - wit inspect
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 120    62 1300   - wit inspect - wit inspect
termination-15/cstrncmp_malloc_true-termination.c.i unknown 0 wit inspect 130    62 1600   - wit inspect - wit inspect
termination-15/cstrncmp_mixed_alloca_true-termination.c.i unknown 0 wit inspect 120    69 1900   - wit inspect - wit inspect
termination-15/cstrncmp_reverse_alloca_true-termination.c.i unknown 0 wit inspect 130    83 1800   - wit inspect - wit inspect
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i timeout 0 wit inspect 900    870 12000   - wit inspect - wit inspect
termination-15/cstrncpy_malloc_true-termination.c.i timeout 0 wit inspect 900    880 10000   - wit inspect - wit inspect
termination-15/cstrncpy_mixed_alloca_true-termination.c.i unknown 0 wit inspect 900    450 10000   - wit inspect - wit inspect
termination-15/cstrncpy_reverse_alloca_true-termination.c.i unknown 0 wit inspect 900    450 12000   - wit inspect - wit inspect
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 2.1  57 27   - wit inspect - wit inspect
termination-15/cstrpbrk_malloc_true-termination.c.i unknown 0 wit inspect 2.2  57 29   - wit inspect - wit inspect
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i unknown 0 wit inspect 2.1  56 28   - wit inspect - wit inspect
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i unknown 0 wit inspect 2.1  57 22   - wit inspect - wit inspect
termination-15/cstrspn_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 2.1  57 28   - wit inspect - wit inspect
termination-15/cstrspn_malloc_true-termination.c.i unknown 0 wit inspect 2.3  57 29   - wit inspect - wit inspect
termination-15/cstrspn_mixed_alloca_true-termination.c.i unknown 0 wit inspect 2.2  56 29   - wit inspect - wit inspect
termination-15/cstrspn_reverse_alloca_true-termination.c.i unknown 0 wit inspect 2.2  56 28   - wit inspect - wit inspect
termination-15/array04_alloca_false-termination.c.i unknown 0 wit inspect 1.5  56 17   error (1) 0 wit inspect .62 45 false(termination) 1 wit inspect 10   380
termination-15/array14_alloca_false-termination.c.i unknown 0 wit inspect 1.6  56 19   error (1) 0 wit inspect .60 47 false(termination) 1 wit inspect 16   560
termination-15/array15_alloca_false-termination.c.i unknown 0 wit inspect 1.6  58 18   error (1) 0 wit inspect .62 45 false(termination) 1 wit inspect 16   550
termination-15/array16_alloca_original_false-termination.c.i unknown 0 wit inspect 1.6  56 18   error (1) 0 wit inspect .46 45 false(termination) 1 wit inspect 22   610
termination-15/array19_alloca_false-termination.c.i unknown 0 wit inspect 1.5  57 17   error (1) 0 wit inspect .71 45 false(termination) 1 wit inspect 11   390
termination-15/array20_alloca_false-termination.c.i unknown 0 wit inspect 1.6  56 16   error (1) 0 wit inspect .62 46 false(termination) 1 wit inspect 12   480
termination-recursive-malloc/chunk1_true-termination.c.i unknown 0 wit inspect 1.3  56 15   - wit inspect - wit inspect
termination-recursive-malloc/chunk2_true-termination.c.i unknown 0 wit inspect 1.5  56 16   - wit inspect - wit inspect
termination-recursive-malloc/chunk3_true-termination.c.i unknown 0 wit inspect 1.7  56 20   - wit inspect - wit inspect
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i unknown 0 wit inspect 2.6  57 31   - wit inspect - wit inspect
termination-recursive-malloc/mergeSort_true-termination.c.i unknown 0 wit inspect 900    7800 11000   - wit inspect - wit inspect
termination-recursive-malloc/mutual_simple2_true-termination.c.i unknown 0 wit inspect 1.4  56 16   - wit inspect - wit inspect
termination-recursive-malloc/mutual_simple_true-termination.c.i unknown 0 wit inspect 1.2  56 14   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i unknown 0 wit inspect 1.3  57 17   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i unknown 0 wit inspect 6.3  110 78   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i unknown 0 wit inspect 8.4  220 98   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i unknown 0 wit inspect 8.2  200 86   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i unknown 0 wit inspect 8.4  210 100   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i unknown 0 wit inspect 5.0  96 64   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i unknown 0 wit inspect 3.7  84 48   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i unknown 0 wit inspect 2.6  56 32   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i unknown 0 wit inspect 1.4  57 15   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i unknown 0 wit inspect 13    200 150   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i unknown 0 wit inspect 4.6  100 53   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i unknown 0 wit inspect 1.3  57 16   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i unknown 0 wit inspect 1.3  56 14   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i unknown 0 wit inspect 1.3  56 16   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i unknown 0 wit inspect 1.4  56 15   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i unknown 0 wit inspect 4.8  92 57   - wit inspect - wit inspect
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i unknown 0 wit inspect 1.5  56 16   - wit inspect - wit inspect
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i unknown 0 wit inspect 1.4  57 16   - wit inspect - wit inspect
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i unknown 0 wit inspect 1.4  57 16   - wit inspect - wit inspect
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i unknown 0 wit inspect 3.0  56 45   - wit inspect - wit inspect
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 -136 17000 28000 210000 17 0 11 780 17 15 260 9500
    correct results 108 216 140 3500 1700 0 15 15 220 8000
        correct true 108 216 140 3500 1700 0 0
        correct false 0 0 15 15 220 8000
    incorrect results 11 -352 11 310 140 0 0
        incorrect true 11 -352 11 310 140 0 0
        incorrect false 0 0 0
score (260 tasks, max score: 503) -136 0 15
Run set depthk.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Termination-MainHeap