Tool CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-05 05:46:16 CET 2018-12-06 09:44:44 CET 2018-12-06 10:50:29 CET
Run set cpa-seq.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-termination.Termination-MainHeap
Options -svcomp19 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
termination-libowfat/atoi_true-termination.c.i unknown 0 --- inspect 130   95    3800 1500 0   0   - --- inspect - --- inspect
termination-libowfat/atol_true-termination.c.i unknown 0 --- inspect 61   35    2900 540 0   0   - --- inspect - --- inspect
termination-libowfat/atoll_true-termination.c.i unknown 0 --- inspect 110   74    3800 1400 0   0   - --- inspect - --- inspect
termination-libowfat/basename_true-termination.c.i unknown 0 --- inspect 65   41    2200 770 0   0   - --- inspect - --- inspect
termination-libowfat/build_fullname_true-termination.c.i timeout 0 --- inspect 900   870    3900 12000 0   0   - --- inspect - --- inspect
termination-libowfat/dirname_true-termination.c.i timeout 0 --- inspect 900   820    4300 11000 0   0   - --- inspect - --- inspect
termination-libowfat/skip_to_true-termination.c.i unknown 0 --- inspect 9.2 2.8  510 77 0   0   - --- inspect - --- inspect
termination-libowfat/stpcpy_true-termination.c.i timeout 0 --- inspect 900   820    4200 12000 0   0   - --- inspect - --- inspect
termination-libowfat/strcasecmp_true-termination.c.i timeout 0 --- inspect 900   840    4300 12000 0   0   - --- inspect - --- inspect
termination-libowfat/strcat_short_true-termination.c.i timeout 0 --- inspect 900   820    4300 12000 0   0   - --- inspect - --- inspect
termination-libowfat/strcat_true-termination.c.i timeout 0 --- inspect 900   830    4200 12000 0   0   - --- inspect - --- inspect
termination-libowfat/strchr_short_true-termination.c.i unknown 0 --- inspect 9.8 2.9  520 83 0   0   - --- inspect - --- inspect
termination-libowfat/strchr_true-termination.c.i timeout 0 --- inspect 900   840    4100 13000 0   0   - --- inspect - --- inspect
termination-libowfat/strcmp_short_true-termination.c.i timeout 0 --- inspect 900   850    3400 13000 0   0   - --- inspect - --- inspect
termination-libowfat/strcpy_small_true-termination.c.i timeout 0 --- inspect 900   820    4200 12000 0   0   - --- inspect - --- inspect
termination-libowfat/strcspn_true-termination.c.i true 2 --- inspect 470   420    2500 6000 0   0   - --- inspect - --- inspect
termination-libowfat/strdup_true-termination.c.i timeout 0 --- inspect 900   840    4200 11000 0   0   - --- inspect - --- inspect
termination-libowfat/strlcat_true-termination.c.i error (parsing failed) 0 --- inspect 1.9 .80 160 16 0   0   - --- inspect - --- inspect
termination-libowfat/strlcpy_true-termination.c.i error (parsing failed) 0 --- inspect 2.0 .84 160 18 0   0   - --- inspect - --- inspect
termination-libowfat/strlen_true-termination.c.i unknown 0 --- inspect 8.3 2.7  480 75 0   0   - --- inspect - --- inspect
termination-libowfat/strpbrk_true-termination.c.i true 2 --- inspect 440   400    2600 6000 0   0   - --- inspect - --- inspect
termination-libowfat/strrchr_short_true-termination.c.i unknown 0 --- inspect 7.9 2.5  470 74 0   0   - --- inspect - --- inspect
termination-libowfat/strrchr_true-termination.c.i timeout 0 --- inspect 900   820    4600 13000 0   0   - --- inspect - --- inspect
termination-libowfat/strspn_true-termination.c.i timeout 0 --- inspect 900   850    3900 13000 0   0   - --- inspect - --- inspect
termination-libowfat/strstr_true-termination.c.i timeout 0 --- inspect 900   840    3800 11000 0   0   - --- inspect - --- inspect
termination-libowfat/strtok_r_true-termination.c.i unknown 0 --- inspect 29   8.6  1400 240 0   0   - --- inspect - --- inspect
termination-libowfat/strtol_true-termination.c.i exception 0 --- inspect 26   6.9  1300 210 0   0   - --- inspect - --- inspect
termination-libowfat/strtoul_true-termination.c.i exception 0 --- inspect 8.3 2.6  460 69 0   0   - --- inspect - --- inspect
termination-libowfat/strtoull_true-termination.c.i exception 0 --- inspect 8.5 2.7  460 70 0   0   - --- inspect - --- inspect
termination-libowfat/wcsrchr_true-termination.c.i unknown 0 --- inspect 7.9 2.6  470 63 0   0   - --- inspect - --- inspect
termination-libowfat/wcsstr_true-termination.c.i timeout 0 --- inspect 900   830    4200 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i unknown 0 --- inspect 5.0 1.9  280 44 0   0   error (invalid witness file) 0 --- inspect .62 .37 40 0     0   error (2) 0 --- inspect .021 .021 5.7 0    0  
termination-memory-alloca/Velroyen-alloca_false-termination.c.i unknown 0 --- inspect 6.5 2.2  360 58 0   0   error (invalid witness file) 0 --- inspect .63 .39 40 0     0   error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 900   820    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i true 2 --- inspect 410   350    4200 5100 0   0   - --- inspect - --- inspect
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 910   850    4200 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i true 2 --- inspect 370   310    4300 4400 0   0   - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i unknown 0 --- inspect 860   780    4200 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 900   830    4200 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i true 2 --- inspect 6.4 2.3  320 56 0   0   - --- inspect - --- inspect
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 910   860    4100 9700 0   0   - --- inspect - --- inspect
termination-memory-alloca/Masse-alloca_true-termination.c.i unknown 0 --- inspect 5.9 2.1  300 60 0   0   - --- inspect - --- inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i timeout 0 --- inspect 900   860    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i true 2 --- inspect 150   110    4100 1900 0   0   - --- inspect - --- inspect
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i timeout 0 --- inspect 910   850    4400 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i timeout 0 --- inspect 900   860    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i unknown 0 --- inspect 880   810    4200 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i out of memory 0 --- inspect 800   750    15000 10000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Urban-alloca_true-termination.c.i true 2 --- inspect 110   72    4000 1200 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   850    4200 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   850    4500 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   860    4500 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   850    4200 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 920   870    4300 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   850    4300 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/add_last-alloca_true-termination.c.i true 2 --- inspect 11   3.4  390 100 0   0   - --- inspect - --- inspect
termination-memory-alloca/array01-alloca_true-termination.c.i unknown 0 --- inspect 8.2 2.6  480 73 0   0   - --- inspect - --- inspect
termination-memory-alloca/array02-alloca_true-termination.c.i unknown 0 --- inspect 22   6.0  940 190 0   0   - --- inspect - --- inspect
termination-memory-alloca/array03-alloca_true-termination.c.i true 2 --- inspect 4.4 1.8  260 37 0   0   - --- inspect - --- inspect
termination-memory-alloca/aviad_true-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4200 15000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   850    4200 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   850    4400 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i unknown 0 --- inspect 57   20    2900 520 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i unknown 0 --- inspect 54   20    2900 510 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   850    4400 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    3900 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4000 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4000 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   850    4300 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   850    4300 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   840    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   870    4000 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   840    4200 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   870    4000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 490   410    4700 5900 0   0   - --- inspect - --- inspect
termination-memory-alloca/bubblesort-alloca_true-termination.c.i true 2 --- inspect 7.3 2.4  450 72 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   830    4300 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    3900 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/count_down-alloca_true-termination.c.i unknown 0 --- inspect 19   5.4  620 170 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrcat-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrchr-alloca_true-termination.c.i unknown 0 --- inspect 34   9.5  1300 280 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i timeout 0 --- inspect 900   860    3000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4400 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 15000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrlen-alloca_true-termination.c.i unknown 0 --- inspect 26   7.1  1100 230 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrncat-alloca_true-termination.c.i timeout 0 --- inspect 900   830    4200 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i timeout 0 --- inspect 900   860    3200 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i true 2 --- inspect 790   700    4800 9300 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrspn-alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/diff-alloca_true-termination.c.i true 2 --- inspect 44   29    940 460 0   0   - --- inspect - --- inspect
termination-memory-alloca/easySum-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4200 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/ex1-alloca_true-termination.c.i exception 0 --- inspect 3.9 1.6  260 38 0   0   - --- inspect - --- inspect
termination-memory-alloca/ex2-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i exception 0 --- inspect 3.8 1.6  260 37 0   0   - --- inspect - --- inspect
termination-memory-alloca/ex3b-alloca_true-termination.c.i exception 0 --- inspect 3.8 1.6  260 35 0   0   - --- inspect - --- inspect
termination-memory-alloca/fermat-alloca_true-termination.c.i exception 0 --- inspect 4.1 1.6  260 36 0   0   - --- inspect - --- inspect
termination-memory-alloca/flag-alloca_true-termination.c.i timeout 0 --- inspect 910   860    4300 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/gcd1-alloca_true-termination.c.i timeout 0 --- inspect 910   860    4200 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/genady-alloca_true-termination.c.i timeout 0 --- inspect 900   860    4400 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/insertionsort-alloca_true-termination.c.i true 2 --- inspect 14   4.0  660 120 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_AG313-alloca_true-termination.c.i timeout 0 --- inspect 910   840    4400 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_Break-alloca_true-termination.c.i timeout 0 --- inspect 900   840    3900 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i true 2 --- inspect 10   3.2  400 81 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i true 2 --- inspect 330   260    4600 3700 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i timeout 0 --- inspect 900   840    3900 10000 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_Nested-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/lis-alloca_true-termination.c.i timeout 0 --- inspect 900   830    4200 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/min_rf-alloca_true-termination.c.i timeout 0 --- inspect 910   840    4400 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/mult_array-alloca_true-termination.c.i exception 0 --- inspect 3.8 1.6  270 37 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i true 2 --- inspect 7.6 2.5  350 63 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i true 2 --- inspect 7.2 2.4  340 61 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i true 2 --- inspect 6.8 2.3  400 58 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i true 2 --- inspect 6.8 2.3  310 55 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i unknown 0 --- inspect 360   310    4400 5100 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i timeout 0 --- inspect 900   820    4400 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i timeout 0 --- inspect 900   830    4200 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i unknown 0 --- inspect 460   390    4500 5500 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i timeout 0 --- inspect 900   870    2000 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i timeout 0 --- inspect 900   850    3900 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i unknown 0 --- inspect 8.3 2.6  410 76 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i timeout 0 --- inspect 900   830    4200 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i unknown 0 --- inspect 650   590    4100 10000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i true 2 --- inspect 890   800    4500 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i true 2 --- inspect 8.8 2.7  470 77 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i timeout 0 --- inspect 900   870    2000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i timeout 0 --- inspect 900   860    3300 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i timeout 0 --- inspect 900   830    4300 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i unknown 0 --- inspect 7.3 2.4  470 63 0   0   - --- inspect - --- inspect
termination-memory-alloca/selectionsort-alloca_true-termination.c.i out of memory 0 --- inspect 480   440    15000 6000 0   0   - --- inspect - --- inspect
termination-memory-alloca/stroeder1-alloca_true-termination.c.i true 2 --- inspect 6.0 2.2  340 48 0   0   - --- inspect - --- inspect
termination-memory-alloca/stroeder2-alloca_true-termination.c.i true 2 --- inspect 7.6 2.5  350 66 0   0   - --- inspect - --- inspect
termination-memory-alloca/strreplace-alloca_true-termination.c.i unknown 0 --- inspect 33   10    1400 290 0   0   - --- inspect - --- inspect
termination-memory-alloca/subseq-alloca_true-termination.c.i timeout 0 --- inspect 900   860    2500 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/substring-alloca_true-termination.c.i timeout 0 --- inspect 900   830    4200 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/twisted-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i error (recursion) 0 --- inspect 4.6 1.8  270 49 0   0   error (invalid witness file) 0 --- inspect .60 .37 41 0     0   error (2) 0 --- inspect .042 .043 5.6 0    0  
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i false(termination) 1 wit inspect 8.6 2.7  470 77 0   0   false(termination) 1 --- inspect 4.9  2.7  250 .033 0   false(termination) 1 --- inspect 12     6.8   390   .62 0  
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i unknown 0 --- inspect 59   29    3700 590 0   0   error (invalid witness file) 0 --- inspect .59 .37 40 0     0   error (2) 0 --- inspect .022 .023 5.7 0    0  
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i error (recursion) 0 --- inspect 4.7 1.8  270 39 0   0   error (invalid witness file) 0 --- inspect .58 .37 41 0     0   error (2) 0 --- inspect .022 .023 5.7 0    0  
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i error (recursion) 0 --- inspect 4.7 1.8  270 46 0   0   error (invalid witness file) 0 --- inspect .60 .37 41 0     0   error (2) 0 --- inspect .022 .024 5.6 0    0  
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i unknown 0 --- inspect 8.8 2.7  480 77 0   0   error (invalid witness file) 0 --- inspect .60 .38 40 0     0   error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i unknown 0 --- inspect 67   31    3600 600 0   0   error (invalid witness file) 0 --- inspect .73 .46 41 0     0   error (2) 0 --- inspect .024 .024 5.6 0    0  
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i unknown 0 --- inspect 57   30    3500 600 0   0   error (invalid witness file) 0 --- inspect .71 .44 41 0     0   error (2) 0 --- inspect .023 .028 5.7 0    0  
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i error (recursion) 0 --- inspect 4.6 1.8  260 42 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i exception 0 --- inspect 4.2 1.7  270 35 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i error (recursion) 0 --- inspect 4.8 1.9  280 41 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i error (recursion) 0 --- inspect 4.6 1.8  260 40 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i true 2 --- inspect 6.4 2.2  330 58 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i exception 0 --- inspect 4.2 1.8  270 43 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i unknown 0 --- inspect 15   4.3  630 130 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i unknown 0 --- inspect 9.2 2.9  470 79 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i exception 0 --- inspect 4.2 1.7  260 40 0   0   - --- inspect - --- inspect
termination-15/add_first_alloca_true-termination.c.i true 2 --- inspect 12   4.5  520 99 0   0   - --- inspect - --- inspect
termination-15/array05_alloca_true-termination.c.i true 2 --- inspect 7.5 2.6  360 69 0   0   - --- inspect - --- inspect
termination-15/array06_alloca_true-termination.c.i true 2 --- inspect 7.5 2.6  360 67 0   0   - --- inspect - --- inspect
termination-15/array07_alloca_true-termination.c.i true 2 --- inspect 7.5 2.6  360 69 0   0   - --- inspect - --- inspect
termination-15/array08_alloca_true-termination.c.i timeout 0 --- inspect 900   840    4500 11000 0   0   - --- inspect - --- inspect
termination-15/array09_alloca_true-termination.c.i timeout 0 --- inspect 900   840    4500 11000 0   0   - --- inspect - --- inspect
termination-15/array10_alloca_true-termination.c.i true 2 --- inspect 7.9 2.7  360 69 0   0   - --- inspect - --- inspect
termination-15/array12_alloca_true-termination.c.i timeout 0 --- inspect 900   830    4500 9500 0   0   - --- inspect - --- inspect
termination-15/array13_alloca_true-termination.c.i timeout 0 --- inspect 900   830    4400 14000 0   0   - --- inspect - --- inspect
termination-15/array16_alloca_fixed_true-termination.c.i timeout 0 --- inspect 900   800    5000 12000 0   0   - --- inspect - --- inspect
termination-15/array17_alloca_true-termination.c.i unknown 0 --- inspect 14   4.0  550 110 0   0   - --- inspect - --- inspect
termination-15/array18_alloca_true-termination.c.i timeout 0 --- inspect 900   830    4400 13000 0   0   - --- inspect - --- inspect
termination-15/count_up_alloca_true-termination.c.i unknown 0 --- inspect 25   7.0  800 210 0   0   - --- inspect - --- inspect
termination-15/count_up_and_down_alloca_true-termination.c.i unknown 0 --- inspect 18   5.3  650 150 0   0   - --- inspect - --- inspect
termination-15/cstrcat_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   850    4000 12000 0   0   - --- inspect - --- inspect
termination-15/cstrcat_malloc_true-termination.c.i timeout 0 --- inspect 900   850    4000 14000 0   0   - --- inspect - --- inspect
termination-15/cstrcat_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   850    4000 13000 0   0   - --- inspect - --- inspect
termination-15/cstrcat_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   800    5000 11000 0   0   - --- inspect - --- inspect
termination-15/cstrchr_diffterm_alloca_true-termination.c.i unknown 0 --- inspect 27   7.3  990 220 0   0   - --- inspect - --- inspect
termination-15/cstrchr_malloc_true-termination.c.i unknown 0 --- inspect 36   10    1500 290 0   0   - --- inspect - --- inspect
termination-15/cstrchr_reverse_alloca_true-termination.c.i unknown 0 --- inspect 15   4.3  670 140 0   0   - --- inspect - --- inspect
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3400 11000 0   0   - --- inspect - --- inspect
termination-15/cstrcmp_malloc_true-termination.c.i timeout 0 --- inspect 900   860    3500 12000 0   0   - --- inspect - --- inspect
termination-15/cstrcmp_mixed_alloca_true-termination.c.i unknown 0 --- inspect 870   830    3300 13000 0   0   - --- inspect - --- inspect
termination-15/cstrcmp_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3400 12000 0   0   - --- inspect - --- inspect
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i unknown 0 --- inspect 140   120    3000 1700 0   0   - --- inspect - --- inspect
termination-15/cstrcpy_malloc_true-termination.c.i unknown 0 --- inspect 140   120    2700 1800 0   0   - --- inspect - --- inspect
termination-15/cstrcpy_mixed_alloca_true-termination.c.i unknown 0 --- inspect 140   120    2700 1800 0   0   - --- inspect - --- inspect
termination-15/cstrcpy_reverse_alloca_true-termination.c.i unknown 0 --- inspect 140   120    2700 2200 0   0   - --- inspect - --- inspect
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   850    3700 12000 0   0   - --- inspect - --- inspect
termination-15/cstrcspn_malloc_true-termination.c.i timeout 0 --- inspect 900   850    3700 11000 0   0   - --- inspect - --- inspect
termination-15/cstrcspn_mixed_alloca_true-termination.c.i unknown 0 --- inspect 300   260    3700 4300 0   0   - --- inspect - --- inspect
termination-15/cstrcspn_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 12000 0   0   - --- inspect - --- inspect
termination-15/cstrlen_diffterm_alloca_true-termination.c.i unknown 0 --- inspect 22   6.2  940 200 0   0   - --- inspect - --- inspect
termination-15/cstrlen_malloc_true-termination.c.i unknown 0 --- inspect 30   8.7  1000 250 0   0   - --- inspect - --- inspect
termination-15/cstrlen_reverse_alloca_true-termination.c.i unknown 0 --- inspect 37   11    1500 320 0   0   - --- inspect - --- inspect
termination-15/cstrncat_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   830    4200 12000 0   0   - --- inspect - --- inspect
termination-15/cstrncat_malloc_true-termination.c.i timeout 0 --- inspect 900   830    4200 12000 0   0   - --- inspect - --- inspect
termination-15/cstrncat_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 12000 0   0   - --- inspect - --- inspect
termination-15/cstrncat_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   820    4300 13000 0   0   - --- inspect - --- inspect
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3400 11000 0   0   - --- inspect - --- inspect
termination-15/cstrncmp_malloc_true-termination.c.i timeout 0 --- inspect 900   860    3300 13000 0   0   - --- inspect - --- inspect
termination-15/cstrncmp_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3300 12000 0   0   - --- inspect - --- inspect
termination-15/cstrncmp_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3300 11000 0   0   - --- inspect - --- inspect
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   820    4700 13000 0   0   - --- inspect - --- inspect
termination-15/cstrncpy_malloc_true-termination.c.i timeout 0 --- inspect 900   830    4600 11000 0   0   - --- inspect - --- inspect
termination-15/cstrncpy_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   810    4800 11000 0   0   - --- inspect - --- inspect
termination-15/cstrncpy_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   830    4300 11000 0   0   - --- inspect - --- inspect
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   850    3700 12000 0   0   - --- inspect - --- inspect
termination-15/cstrpbrk_malloc_true-termination.c.i timeout 0 --- inspect 900   860    3700 15000 0   0   - --- inspect - --- inspect
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i unknown 0 --- inspect 290   250    3700 4100 0   0   - --- inspect - --- inspect
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   850    3700 10000 0   0   - --- inspect - --- inspect
termination-15/cstrspn_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 12000 0   0   - --- inspect - --- inspect
termination-15/cstrspn_malloc_true-termination.c.i timeout 0 --- inspect 900   860    3700 12000 0   0   - --- inspect - --- inspect
termination-15/cstrspn_mixed_alloca_true-termination.c.i unknown 0 --- inspect 300   250    3700 3500 0   0   - --- inspect - --- inspect
termination-15/cstrspn_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   850    3700 14000 0   0   - --- inspect - --- inspect
termination-15/array04_alloca_false-termination.c.i false(termination) 1 wit inspect 8.2 2.8  390 75 0   0   false(termination) 1 --- inspect 4.9  2.7  250 .033 0   false(termination) 1 --- inspect 9.8   5.5   330   .62 0  
termination-15/array14_alloca_false-termination.c.i timeout 0 --- inspect 900   840    4400 11000 0   0   error (invalid witness file) 0 --- inspect .61 .39 42 0     0   error (2) 0 --- inspect .053 .055 5.7 0    0  
termination-15/array15_alloca_false-termination.c.i timeout 0 --- inspect 900   840    4400 12000 0   0   error (invalid witness file) 0 --- inspect .61 .37 41 0     0   error (2) 0 --- inspect .022 .024 5.7 0    0  
termination-15/array16_alloca_original_false-termination.c.i timeout 0 --- inspect 900   800    5300 9900 0   0   error (invalid witness file) 0 --- inspect .58 .37 41 0     0   error (2) 0 --- inspect .049 .050 5.5 0    0  
termination-15/array19_alloca_false-termination.c.i false(termination) 1 wit inspect 8.0 2.7  390 71 0   0   false(termination) 1 --- inspect 6.0  3.2  250 .033 0   false(termination) 1 --- inspect 10     5.8   320   .66 0  
termination-15/array20_alloca_false-termination.c.i exception 0 --- inspect 5.3 2.2  310 53 0   0   error (invalid witness file) 0 --- inspect .63 .38 41 0     0   error (2) 0 --- inspect .022 .023 5.6 0    0  
termination-recursive-malloc/chunk1_true-termination.c.i unknown 0 --- inspect 830   760    4100 11000 0   0   - --- inspect - --- inspect
termination-recursive-malloc/chunk2_true-termination.c.i timeout 0 --- inspect 900   860    4100 10000 0   0   - --- inspect - --- inspect
termination-recursive-malloc/chunk3_true-termination.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i error (recursion) 0 --- inspect 4.5 1.7  290 39 0   0   - --- inspect - --- inspect
termination-recursive-malloc/mergeSort_true-termination.c.i error (recursion) 0 --- inspect 3.9 1.6  280 35 0   0   - --- inspect - --- inspect
termination-recursive-malloc/mutual_simple2_true-termination.c.i timeout 0 --- inspect 910   850    4100 12000 0   0   - --- inspect - --- inspect
termination-recursive-malloc/mutual_simple_true-termination.c.i true 2 --- inspect 6.8 2.3  480 58 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i timeout 0 --- inspect 910   840    4300 13000 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i error (recursion) 0 --- inspect 4.4 1.8  280 36 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i error (recursion) 0 --- inspect 4.4 1.8  280 40 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i error (recursion) 0 --- inspect 4.1 1.7  280 36 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i error (recursion) 0 --- inspect 4.4 1.8  280 39 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i error (recursion) 0 --- inspect 4.2 1.7  280 41 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i error (recursion) 0 --- inspect 4.3 1.8  280 41 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i error (recursion) 0 --- inspect 4.1 1.7  280 39 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i timeout 0 --- inspect 910   850    4200 11000 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i error (recursion) 0 --- inspect 4.0 1.7  270 35 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i timeout 0 --- inspect 910   840    4200 11000 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i timeout 0 --- inspect 900   840    4100 11000 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i unknown 0 --- inspect 840   760    4200 9400 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i unknown 0 --- inspect 830   760    4200 12000 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i timeout 0 --- inspect 900   840    4100 11000 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i error (recursion) 0 --- inspect 4.1 1.7  280 35 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i error (recursion) 0 --- inspect 8.0 2.6  360 71 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i unknown 0 --- inspect 670   590    4500 8800 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i unknown 0 --- inspect 7.1 2.4  470 65 0   0   - --- inspect - --- inspect
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i error (recursion) 0 --- inspect 4.3 1.7  280 38 0   0   - --- inspect - --- inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 259 65 140000 130000   750000 1800000 0   0   16 3 24 14   1300 .098 0   16 3 32 18 1100 1.9 0  
    correct results 34 65 4700 3900   50000 57000 0   0   3 3 16 8.6 750 .098 0   3 3 32 18 1000 1.9 0  
        correct true 31 62 4600 3900   49000 57000 0   0   0 0
        correct false 3 3 25 8.2 1200 220 0   0   3 3 16 8.6 750 .098 0   3 3 32 18 1000 1.9 0  
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (259 tasks, max score: 502) 65 3 3
Run set cpa-seq.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-termination.Termination-MainHeap