Tool CBMC 5.8 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* [apollon029; apollon035; apollon037; apollon075; apollon077; apollon078] [apollon029; apollon077; apollon078]
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 13:00:07 CET 2017-12-01 19:39:59 CET 2017-12-01 19:43:03 CET
Run set cbmc.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Termination-MainHeap
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-12-01_1300.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/cbmc.2017-12-01_1300.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 error (42) 0 wit inspect 870    2200 4900   - wit inspect - wit inspect
termination-libowfat/atol_true-termination.c.i error (42) 0 wit inspect 870    2200 5200   - wit inspect - wit inspect
termination-libowfat/atoll_true-termination.c.i error (42) 0 wit inspect 870    2200 4400   - wit inspect - wit inspect
termination-libowfat/basename_true-termination.c.i error (42) 0 wit inspect 870    6400 4400   - wit inspect - wit inspect
termination-libowfat/build_fullname_true-termination.c.i error (42) 0 wit inspect 870    14000 8100   - wit inspect - wit inspect
termination-libowfat/dirname_true-termination.c.i error (42) 0 wit inspect 870    14000 7800   - wit inspect - wit inspect
termination-libowfat/skip_to_true-termination.c.i error (42) 0 wit inspect 870    2800 6000   - wit inspect - wit inspect
termination-libowfat/stpcpy_true-termination.c.i error (42) 0 wit inspect 870    14000 3600   - wit inspect - wit inspect
termination-libowfat/strcasecmp_true-termination.c.i error (42) 0 wit inspect 870    2500 6200   - wit inspect - wit inspect
termination-libowfat/strcat_short_true-termination.c.i error (42) 0 wit inspect 870    13000 4700   - wit inspect - wit inspect
termination-libowfat/strcat_true-termination.c.i error (42) 0 wit inspect 870    14000 5600   - wit inspect - wit inspect
termination-libowfat/strchr_short_true-termination.c.i error (42) 0 wit inspect 870    6000 5000   - wit inspect - wit inspect
termination-libowfat/strchr_true-termination.c.i error (42) 0 wit inspect 870    1100 5800   - wit inspect - wit inspect
termination-libowfat/strcmp_short_true-termination.c.i error (42) 0 wit inspect 880    8500 3000   - wit inspect - wit inspect
termination-libowfat/strcpy_small_true-termination.c.i error (42) 0 wit inspect 870    14000 3900   - wit inspect - wit inspect
termination-libowfat/strcspn_true-termination.c.i error (42) 0 wit inspect 870    340 4000   - wit inspect - wit inspect
termination-libowfat/strdup_true-termination.c.i error (42) 0 wit inspect 870    13000 5200   - wit inspect - wit inspect
termination-libowfat/strlcat_true-termination.c.i error (42) 0 wit inspect 870    14000 4300   - wit inspect - wit inspect
termination-libowfat/strlcpy_true-termination.c.i error (42) 0 wit inspect 870    14000 4900   - wit inspect - wit inspect
termination-libowfat/strlen_true-termination.c.i error (42) 0 wit inspect 870    6100 3400   - wit inspect - wit inspect
termination-libowfat/strpbrk_true-termination.c.i error (42) 0 wit inspect 870    330 4000   - wit inspect - wit inspect
termination-libowfat/strrchr_short_true-termination.c.i error (42) 0 wit inspect 870    2700 5500   - wit inspect - wit inspect
termination-libowfat/strrchr_true-termination.c.i error (42) 0 wit inspect 870    2600 6100   - wit inspect - wit inspect
termination-libowfat/strspn_true-termination.c.i error (42) 0 wit inspect 870    1300 3500   - wit inspect - wit inspect
termination-libowfat/strstr_true-termination.c.i error (42) 0 wit inspect 870    820 9900   - wit inspect - wit inspect
termination-libowfat/strtok_r_true-termination.c.i error (42) 0 wit inspect 870    1300 4100   - wit inspect - wit inspect
termination-libowfat/strtol_true-termination.c.i error (42) 0 wit inspect 870    14000 5600   - wit inspect - wit inspect
termination-libowfat/strtoul_true-termination.c.i error (42) 0 wit inspect 880    10000 5600   - wit inspect - wit inspect
termination-libowfat/strtoull_true-termination.c.i error (42) 0 wit inspect 870    11000 4400   - wit inspect - wit inspect
termination-libowfat/wcsrchr_true-termination.c.i error (42) 0 wit inspect 870    3200 6700   - wit inspect - wit inspect
termination-libowfat/wcsstr_true-termination.c.i error (42) 0 wit inspect 870    1300 4600   - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i error (42) 0 wit inspect 880    3200 7600   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8
termination-memory-alloca/Velroyen-alloca_false-termination.c.i error (42) 0 wit inspect 870    2600 6000   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 4.9
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i error (42) 0 wit inspect 870    3800 3100   - wit inspect - wit inspect
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i error (42) 0 wit inspect 870    1100 6200   - wit inspect - wit inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i error (42) 0 wit inspect 870    670 3300   - wit inspect - wit inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i error (42) 0 wit inspect 870    4300 4200   - wit inspect - wit inspect
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i error (42) 0 wit inspect 870    3600 4100   - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i error (42) 0 wit inspect 870    2000 5700   - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i error (42) 0 wit inspect 870    3400 7500   - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i error (42) 0 wit inspect 870    4700 6700   - wit inspect - wit inspect
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i error (42) 0 wit inspect 870    3000 6000   - wit inspect - wit inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i true 2 wit inspect .85 36 8.8 - wit inspect - wit inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i error (42) 0 wit inspect 870    1800 5200   - wit inspect - wit inspect
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i error (42) 0 wit inspect 870    3000 7300   - wit inspect - wit inspect
termination-memory-alloca/Masse-alloca_true-termination.c.i error (42) 0 wit inspect 870    260 10000   - wit inspect - wit inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i error (42) 0 wit inspect 870    320 9300   - wit inspect - wit inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i error (42) 0 wit inspect 870    2700 5900   - wit inspect - wit inspect
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i error (42) 0 wit inspect 870    1700 8200   - wit inspect - wit inspect
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i error (42) 0 wit inspect 870    5700 4100   - wit inspect - wit inspect
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i error (42) 0 wit inspect 870    5800 4200   - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i error (42) 0 wit inspect 870    1200 5300   - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i error (42) 0 wit inspect 880    5100 10000   - wit inspect - wit inspect
termination-memory-alloca/Urban-alloca_true-termination.c.i error (42) 0 wit inspect 870    3900 9000   - wit inspect - wit inspect
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    660 3900   - wit inspect - wit inspect
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    5200 3300   - wit inspect - wit inspect
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    8300 4200   - wit inspect - wit inspect
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    2200 6200   - wit inspect - wit inspect
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    5600 3500   - wit inspect - wit inspect
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    6100 4100   - wit inspect - wit inspect
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    780 6100   - wit inspect - wit inspect
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    3200 8400   - wit inspect - wit inspect
termination-memory-alloca/add_last-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 6900   - wit inspect - wit inspect
termination-memory-alloca/array01-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4200   - wit inspect - wit inspect
termination-memory-alloca/array02-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 5200   - wit inspect - wit inspect
termination-memory-alloca/array03-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4600   - wit inspect - wit inspect
termination-memory-alloca/aviad_true-alloca_true-termination.c.i true 2 wit inspect 8.2  160 85   - wit inspect - wit inspect
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    5400 3200   - wit inspect - wit inspect
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    4300 4000   - wit inspect - wit inspect
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    8400 4100   - wit inspect - wit inspect
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    760 7100   - wit inspect - wit inspect
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .88 36 8.4 - wit inspect - wit inspect
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    3400 7900   - wit inspect - wit inspect
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 880    6300 6800   - wit inspect - wit inspect
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    6100 4200   - wit inspect - wit inspect
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    2900 5000   - wit inspect - wit inspect
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    170 9400   - wit inspect - wit inspect
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    1600 8400   - wit inspect - wit inspect
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    1700 5000   - wit inspect - wit inspect
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    1400 6400   - wit inspect - wit inspect
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    1500 7100   - wit inspect - wit inspect
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    1300 6500   - wit inspect - wit inspect
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 880    1000 3100   - wit inspect - wit inspect
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    670 2700   - wit inspect - wit inspect
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 880    670 3700   - wit inspect - wit inspect
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    1400 3800   - wit inspect - wit inspect
termination-memory-alloca/bubblesort-alloca_true-termination.c.i error (42) 0 wit inspect 870    5200 5600   - wit inspect - wit inspect
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    8200 9600   - wit inspect - wit inspect
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    8200 8300   - wit inspect - wit inspect
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    700 3400   - wit inspect - wit inspect
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    3300 6300   - wit inspect - wit inspect
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 870    4100 5100   - wit inspect - wit inspect
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i error (42) 0 wit inspect 880    660 3400   - wit inspect - wit inspect
termination-memory-alloca/count_down-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 6700   - wit inspect - wit inspect
termination-memory-alloca/cstrcat-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4700   - wit inspect - wit inspect
termination-memory-alloca/cstrchr-alloca_true-termination.c.i error (6) 0 wit inspect 770    8500 3300   - wit inspect - wit inspect
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i error (42) 0 wit inspect 880    8100 3600   - wit inspect - wit inspect
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 4200   - wit inspect - wit inspect
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i error (42) 0 wit inspect 870    1200 3400   - wit inspect - wit inspect
termination-memory-alloca/cstrlen-alloca_true-termination.c.i error (42) 0 wit inspect 870    6700 2700   - wit inspect - wit inspect
termination-memory-alloca/cstrncat-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4500   - wit inspect - wit inspect
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i error (42) 0 wit inspect 870    1100 8000   - wit inspect - wit inspect
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 9700   - wit inspect - wit inspect
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i error (42) 0 wit inspect 870    1200 3900   - wit inspect - wit inspect
termination-memory-alloca/cstrspn-alloca_true-termination.c.i error (42) 0 wit inspect 870    1200 3300   - wit inspect - wit inspect
termination-memory-alloca/diff-alloca_true-termination.c.i error (42) 0 wit inspect 880    11000 4200   - wit inspect - wit inspect
termination-memory-alloca/easySum-alloca_true-termination.c.i error (42) 0 wit inspect 870    4400 4100   - wit inspect - wit inspect
termination-memory-alloca/ex1-alloca_true-termination.c.i error (42) 0 wit inspect 870    4100 3500   - wit inspect - wit inspect
termination-memory-alloca/ex2-alloca_true-termination.c.i error (42) 0 wit inspect 870    1500 5700   - wit inspect - wit inspect
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 1.7  36 16   - wit inspect - wit inspect
termination-memory-alloca/ex3b-alloca_true-termination.c.i true 2 wit inspect 16    71 180   - wit inspect - wit inspect
termination-memory-alloca/fermat-alloca_true-termination.c.i error (42) 0 wit inspect 880    7900 12000   - wit inspect - wit inspect
termination-memory-alloca/flag-alloca_true-termination.c.i error (42) 0 wit inspect 870    2300 2900   - wit inspect - wit inspect
termination-memory-alloca/gcd1-alloca_true-termination.c.i error (42) 0 wit inspect 870    680 3300   - wit inspect - wit inspect
termination-memory-alloca/genady-alloca_true-termination.c.i true 2 wit inspect 18    79 210   - wit inspect - wit inspect
termination-memory-alloca/insertionsort-alloca_true-termination.c.i error (42) 0 wit inspect 880    14000 4000   - wit inspect - wit inspect
termination-memory-alloca/java_AG313-alloca_true-termination.c.i error (42) 0 wit inspect 870    5800 3400   - wit inspect - wit inspect
termination-memory-alloca/java_Break-alloca_true-termination.c.i true 2 wit inspect 2.4  36 27   - wit inspect - wit inspect
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i error (42) 0 wit inspect 870    5200 6200   - wit inspect - wit inspect
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i true 2 wit inspect 4.1  38 33   - wit inspect - wit inspect
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i true 2 wit inspect 5.2  41 49   - wit inspect - wit inspect
termination-memory-alloca/java_Nested-alloca_true-termination.c.i true 2 wit inspect 2.6  37 25   - wit inspect - wit inspect
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i true 2 wit inspect 5.9  36 53   - wit inspect - wit inspect
termination-memory-alloca/lis-alloca_true-termination.c.i error (42) 0 wit inspect 870    2500 5300   - wit inspect - wit inspect
termination-memory-alloca/min_rf-alloca_true-termination.c.i error (42) 0 wit inspect 870    510 13000   - wit inspect - wit inspect
termination-memory-alloca/mult_array-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 6500   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 4100   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i error (42) 0 wit inspect 870    2600 4400   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 4500   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4800   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 4600   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 11000   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4900   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i error (42) 0 wit inspect 870    3000 5700   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 4400   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i error (42) 0 wit inspect 870    460 2900   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 4100   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i error (42) 0 wit inspect 870    7600 3500   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 5200   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i error (42) 0 wit inspect 870    1100 5800   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 9700   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i error (42) 0 wit inspect 870    2500 5100   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i error (42) 0 wit inspect 870    310 3600   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i error (42) 0 wit inspect 870    2200 5900   - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 7700   - wit inspect - wit inspect
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i out of memory 0 wit inspect 770    15000 4800   - wit inspect - wit inspect
termination-memory-alloca/selectionsort-alloca_true-termination.c.i error (42) 0 wit inspect 870    15000 5800   - wit inspect - wit inspect
termination-memory-alloca/stroeder1-alloca_true-termination.c.i error (42) 0 wit inspect 870    3400 2700   - wit inspect - wit inspect
termination-memory-alloca/stroeder2-alloca_true-termination.c.i error (42) 0 wit inspect 870    2800 3800   - wit inspect - wit inspect
termination-memory-alloca/strreplace-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 9000   - wit inspect - wit inspect
termination-memory-alloca/subseq-alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 6300   - wit inspect - wit inspect
termination-memory-alloca/substring-alloca_true-termination.c.i error (42) 0 wit inspect 870    1500 4600   - wit inspect - wit inspect
termination-memory-alloca/twisted-alloca_true-termination.c.i true 2 wit inspect .83 36 9.5 - wit inspect - wit inspect
termination-memory-linkedlists/cll_by_lseg-alloca_false-termination.c.i error (42) 0 wit inspect 870    670 12000   error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .018 4.9
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i error (42) 0 wit inspect 870    7700 11000   error (invalid witness file) 0 wit inspect .44 44 error (2) 0 wit inspect .049 4.8
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i error (42) 0 wit inspect 870    13000 9500   error (invalid witness file) 0 wit inspect .39 44 error (2) 0 wit inspect .024 4.8
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i error (42) 0 wit inspect 870    13000 10000   error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 5.0
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i error (42) 0 wit inspect 870    13000 8900   error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .022 4.8
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i error (42) 0 wit inspect 870    14000 9000   error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.8
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i error (42) 0 wit inspect 870    6700 8800   error (invalid witness file) 0 wit inspect .45 43 error (2) 0 wit inspect .020 4.8
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i error (42) 0 wit inspect 870    13000 9100   error (invalid witness file) 0 wit inspect .42 44 error (2) 0 wit inspect .018 5.0
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i error (42) 0 wit inspect 870    13000 10000   error (invalid witness file) 0 wit inspect .43 44 error (2) 0 wit inspect .022 5.0
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i error (42) 0 wit inspect 870    7600 7700   - wit inspect - wit inspect
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 9900   - wit inspect - wit inspect
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 8300   - wit inspect - wit inspect
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 7200   - wit inspect - wit inspect
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i error (42) 0 wit inspect 870    6700 7900   - wit inspect - wit inspect
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i error (42) 0 wit inspect 870    8000 10000   - wit inspect - wit inspect
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i error (42) 0 wit inspect 870    8100 9600   - wit inspect - wit inspect
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i error (42) 0 wit inspect 870    7900 10000   - wit inspect - wit inspect
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 9900   - wit inspect - wit inspect
termination-15/add_first_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4000   - wit inspect - wit inspect
termination-15/array05_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 5500   - wit inspect - wit inspect
termination-15/array06_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4600   - wit inspect - wit inspect
termination-15/array07_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4600   - wit inspect - wit inspect
termination-15/array08_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 6600   - wit inspect - wit inspect
termination-15/array09_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 7100   - wit inspect - wit inspect
termination-15/array10_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 6000   - wit inspect - wit inspect
termination-15/array12_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 7100   - wit inspect - wit inspect
termination-15/array13_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 5400   - wit inspect - wit inspect
termination-15/array16_alloca_fixed_true-termination.c.i error (42) 0 wit inspect 870    14000 6900   - wit inspect - wit inspect
termination-15/array17_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 4800   - wit inspect - wit inspect
termination-15/array18_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 6500   - wit inspect - wit inspect
termination-15/count_up_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4700   - wit inspect - wit inspect
termination-15/count_up_and_down_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4200   - wit inspect - wit inspect
termination-15/cstrcat_diffterm_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4400   - wit inspect - wit inspect
termination-15/cstrcat_malloc_true-termination.c.i error (134) 0 wit inspect 79    13000 810   - wit inspect - wit inspect
termination-15/cstrcat_mixed_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 5400   - wit inspect - wit inspect
termination-15/cstrcat_reverse_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 3800   - wit inspect - wit inspect
termination-15/cstrchr_diffterm_alloca_true-termination.c.i error (6) 0 wit inspect 620    8400 5700   - wit inspect - wit inspect
termination-15/cstrchr_malloc_true-termination.c.i error (6) 0 wit inspect 770    8500 3500   - wit inspect - wit inspect
termination-15/cstrchr_reverse_alloca_true-termination.c.i error (6) 0 wit inspect 800    14000 4500   - wit inspect - wit inspect
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i error (42) 0 wit inspect 870    8500 4600   - wit inspect - wit inspect
termination-15/cstrcmp_malloc_true-termination.c.i error (42) 0 wit inspect 870    8500 4400   - wit inspect - wit inspect
termination-15/cstrcmp_mixed_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 3700   - wit inspect - wit inspect
termination-15/cstrcmp_reverse_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 4000   - wit inspect - wit inspect
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 4500   - wit inspect - wit inspect
termination-15/cstrcpy_malloc_true-termination.c.i error (134) 0 wit inspect 110    14000 1100   - wit inspect - wit inspect
termination-15/cstrcpy_mixed_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 4200   - wit inspect - wit inspect
termination-15/cstrcpy_reverse_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 5300   - wit inspect - wit inspect
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i error (42) 0 wit inspect 870    1200 4500   - wit inspect - wit inspect
termination-15/cstrcspn_malloc_true-termination.c.i error (42) 0 wit inspect 870    4900 4400   - wit inspect - wit inspect
termination-15/cstrcspn_mixed_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4000   - wit inspect - wit inspect
termination-15/cstrcspn_reverse_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4100   - wit inspect - wit inspect
termination-15/cstrlen_diffterm_alloca_true-termination.c.i error (42) 0 wit inspect 870    7900 4500   - wit inspect - wit inspect
termination-15/cstrlen_malloc_true-termination.c.i error (42) 0 wit inspect 870    7600 3900   - wit inspect - wit inspect
termination-15/cstrlen_reverse_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 3100   - wit inspect - wit inspect
termination-15/cstrncat_diffterm_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4500   - wit inspect - wit inspect
termination-15/cstrncat_malloc_true-termination.c.i error (134) 0 wit inspect 81    13000 890   - wit inspect - wit inspect
termination-15/cstrncat_mixed_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4800   - wit inspect - wit inspect
termination-15/cstrncat_reverse_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 5800   - wit inspect - wit inspect
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i error (42) 0 wit inspect 870    1100 6100   - wit inspect - wit inspect
termination-15/cstrncmp_malloc_true-termination.c.i error (42) 0 wit inspect 870    1400 7300   - wit inspect - wit inspect
termination-15/cstrncmp_mixed_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 6800   - wit inspect - wit inspect
termination-15/cstrncmp_reverse_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 6300   - wit inspect - wit inspect
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 11000   - wit inspect - wit inspect
termination-15/cstrncpy_malloc_true-termination.c.i error (134) 0 wit inspect 170    14000 1900   - wit inspect - wit inspect
termination-15/cstrncpy_mixed_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 9700   - wit inspect - wit inspect
termination-15/cstrncpy_reverse_alloca_true-termination.c.i error (42) 0 wit inspect 870    14000 11000   - wit inspect - wit inspect
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i error (42) 0 wit inspect 870    1200 4500   - wit inspect - wit inspect
termination-15/cstrpbrk_malloc_true-termination.c.i error (42) 0 wit inspect 870    4900 4000   - wit inspect - wit inspect
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4100   - wit inspect - wit inspect
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4500   - wit inspect - wit inspect
termination-15/cstrspn_diffterm_alloca_true-termination.c.i error (42) 0 wit inspect 870    1200 4600   - wit inspect - wit inspect
termination-15/cstrspn_malloc_true-termination.c.i error (42) 0 wit inspect 870    4900 6300   - wit inspect - wit inspect
termination-15/cstrspn_mixed_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4600   - wit inspect - wit inspect
termination-15/cstrspn_reverse_alloca_true-termination.c.i error (42) 0 wit inspect 870    13000 4900   - wit inspect - wit inspect
termination-15/array04_alloca_false-termination.c.i error (42) 0 wit inspect 870    14000 5400   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 5.0
termination-15/array14_alloca_false-termination.c.i error (42) 0 wit inspect 870    14000 7500   error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .017 4.8
termination-15/array15_alloca_false-termination.c.i error (42) 0 wit inspect 870    14000 6700   error (invalid witness file) 0 wit inspect .44 43 error (2) 0 wit inspect .023 4.8
termination-15/array16_alloca_original_false-termination.c.i error (42) 0 wit inspect 870    14000 7600   error (invalid witness file) 0 wit inspect .44 44 error (2) 0 wit inspect .019 4.8
termination-15/array19_alloca_false-termination.c.i error (42) 0 wit inspect 870    14000 5400   error (invalid witness file) 0 wit inspect .44 42 error (2) 0 wit inspect .021 4.8
termination-15/array20_alloca_false-termination.c.i error (42) 0 wit inspect 870    14000 6700   error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .021 4.9
termination-recursive-malloc/chunk1_true-termination.c.i out of memory 0 wit inspect 220    15000 1600   - wit inspect - wit inspect
termination-recursive-malloc/chunk2_true-termination.c.i error (6) 0 wit inspect .43 34 3.7 - wit inspect - wit inspect
termination-recursive-malloc/chunk3_true-termination.c.i error (6) 0 wit inspect .41 34 4.1 - wit inspect - wit inspect
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i error (42) 0 wit inspect 870    14000 9100   - wit inspect - wit inspect
termination-recursive-malloc/mergeSort_true-termination.c.i error (134) 0 wit inspect 57    13000 750   - wit inspect - wit inspect
termination-recursive-malloc/mutual_simple2_true-termination.c.i error (6) 0 wit inspect 450    8400 3000   - wit inspect - wit inspect
termination-recursive-malloc/mutual_simple_true-termination.c.i out of memory 0 wit inspect 470    15000 3100   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i error (42) 0 wit inspect 870    9300 5900   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i error (42) 0 wit inspect 870    2600 6600   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i error (42) 0 wit inspect 870    570 6300   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i error (42) 0 wit inspect 870    540 7000   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i error (42) 0 wit inspect 870    580 5900   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i error (42) 0 wit inspect 870    2400 5500   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i error (42) 0 wit inspect 870    1200 5200   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i error (42) 0 wit inspect 870    780 3600   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i error (42) 0 wit inspect 870    9300 6400   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i error (42) 0 wit inspect 870    880 4600   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i error (6) 0 wit inspect 390    920 2500   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i error (42) 0 wit inspect 880    13000 7800   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i error (42) 0 wit inspect 880    11000 7000   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i error (42) 0 wit inspect 870    11000 6900   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i error (6) 0 wit inspect 310    4200 3500   - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i error (42) 0 wit inspect 870    2400 5100   - wit inspect - wit inspect
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i error (134) 0 wit inspect 150    14000 1400   - wit inspect - wit inspect
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i error (134) 0 wit inspect 120    14000 1400   - wit inspect - wit inspect
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i out of memory 0 wit inspect 770    15000 4300   - wit inspect - wit inspect
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i error (42) 0 wit inspect 870    15000 5100   - 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 24 210000 1900000 1400000 17 0 8.1 740 17 0 .37 83
    correct results 12 24 66 640 700 0 0
        correct true 12 24 66 640 700 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 cbmc.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Termination-MainHeap