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