Tool CBMC Path 5.10 () CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:45:10 CET 2018-12-06 08:53:36 CET 2018-12-06 10:12:52 CET
Run set cbmc-path.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-termination.Termination-MainHeap
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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 error (42) 0 --- inspect 880     880     2500   6900    4.0   0      - --- inspect - --- inspect
termination-libowfat/atol_true-termination.c.i error (42) 0 --- inspect 880     880     2500   8200    4.0   0      - --- inspect - --- inspect
termination-libowfat/atoll_true-termination.c.i error (42) 0 --- inspect 880     880     2400   7000    4.1   0      - --- inspect - --- inspect
termination-libowfat/basename_true-termination.c.i out of memory 0 --- inspect 180     180     15000   2100    .037 .0041 - --- inspect - --- inspect
termination-libowfat/build_fullname_true-termination.c.i error (42) 0 --- inspect 880     880     2300   9100    2.5   0      - --- inspect - --- inspect
termination-libowfat/dirname_true-termination.c.i out of memory 0 --- inspect 160     150     15000   2000    .037 0      - --- inspect - --- inspect
termination-libowfat/skip_to_true-termination.c.i error (42) 0 --- inspect 880     880     350   6500    .87  0      - --- inspect - --- inspect
termination-libowfat/stpcpy_true-termination.c.i error (42) 0 --- inspect 880     880     14000   6400    .36  0      - --- inspect - --- inspect
termination-libowfat/strcasecmp_true-termination.c.i out of memory 0 --- inspect 260     260     15000   3000    3.8   0      - --- inspect - --- inspect
termination-libowfat/strcat_short_true-termination.c.i error (42) 0 --- inspect 880     880     1700   6300    2.0   0      - --- inspect - --- inspect
termination-libowfat/strcat_true-termination.c.i error (42) 0 --- inspect 880     880     14000   7800    .52  0      - --- inspect - --- inspect
termination-libowfat/strchr_short_true-termination.c.i error (42) 0 --- inspect 880     880     390   7700    .47  0      - --- inspect - --- inspect
termination-libowfat/strchr_true-termination.c.i error (42) 0 --- inspect 880     880     340   6600    .48  0      - --- inspect - --- inspect
termination-libowfat/strcmp_short_true-termination.c.i error (42) 0 --- inspect 880     880     370   6700    .88  0      - --- inspect - --- inspect
termination-libowfat/strcpy_small_true-termination.c.i error (42) 0 --- inspect 880     880     14000   6200    .59  0      - --- inspect - --- inspect
termination-libowfat/strcspn_true-termination.c.i error (42) 0 --- inspect 880     880     11000   11000    .094 0      - --- inspect - --- inspect
termination-libowfat/strdup_true-termination.c.i error (42) 0 --- inspect 880     880     2600   11000    6.0   0      - --- inspect - --- inspect
termination-libowfat/strlcat_true-termination.c.i error (42) 0 --- inspect 880     880     11000   9900    1.1   0      - --- inspect - --- inspect
termination-libowfat/strlcpy_true-termination.c.i error (42) 0 --- inspect 880     880     2300   6800    5.5   0      - --- inspect - --- inspect
termination-libowfat/strlen_true-termination.c.i error (42) 0 --- inspect 880     880     340   7700    .58  0      - --- inspect - --- inspect
termination-libowfat/strpbrk_true-termination.c.i error (42) 0 --- inspect 880     880     11000   10000    .090 0      - --- inspect - --- inspect
termination-libowfat/strrchr_short_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2400    12     .0041 - --- inspect - --- inspect
termination-libowfat/strrchr_true-termination.c.i out of memory 0 --- inspect 170     170     15000   2000    .037 0      - --- inspect - --- inspect
termination-libowfat/strspn_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2600    .045 0      - --- inspect - --- inspect
termination-libowfat/strstr_true-termination.c.i out of memory 0 --- inspect 210     210     15000   3100    2.1   0      - --- inspect - --- inspect
termination-libowfat/strtok_r_true-termination.c.i out of memory 0 --- inspect 170     170     15000   2400    .045 0      - --- inspect - --- inspect
termination-libowfat/strtol_true-termination.c.i out of memory 0 --- inspect 840     840     15000   11000    .29  0      - --- inspect - --- inspect
termination-libowfat/strtoul_true-termination.c.i error (42) 0 --- inspect 880     880     2800   9300    6.7   0      - --- inspect - --- inspect
termination-libowfat/strtoull_true-termination.c.i error (42) 0 --- inspect 880     880     2800   11000    6.2   0      - --- inspect - --- inspect
termination-libowfat/wcsrchr_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2400    9.0   0      - --- inspect - --- inspect
termination-libowfat/wcsstr_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2400    .037 .0041 - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i out of memory 0 --- inspect 160     160     15000   2000    8.6   .0041 error (invalid witness file) 0 --- inspect .73 .44 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0   0  
termination-memory-alloca/Velroyen-alloca_false-termination.c.i error (42) 0 --- inspect 880     880     140   11000    .80  0      error (invalid witness file) 0 --- inspect .62 .40 41 0   0   error (2) 0 --- inspect .026 .028 5.6 0   0  
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     1300   6600    1.9   0      - --- inspect - --- inspect
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i out of memory 0 --- inspect 370     370     15000   4500    .18  .0041 - --- inspect - --- inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i out of memory 0 --- inspect 650     650     15000   8500    .061 0      - --- inspect - --- inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     340   8000    .68  0      - --- inspect - --- inspect
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     500   5700    .61  0      - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i out of memory 0 --- inspect 320     320     15000   4100    13     .0041 - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i out of memory 0 --- inspect 380     380     15000   4200    .34  0      - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i out of memory 0 --- inspect 240     240     15000   3300    1.3   0      - --- inspect - --- inspect
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i out of memory 0 --- inspect 240     240     15000   3100    1.3   0      - --- inspect - --- inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i true 2 wit inspect .095 .095 7.7 .82 .016 0      - --- inspect - --- inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i out of memory 0 --- inspect 170     170     15000   2200    8.8   0      - --- inspect - --- inspect
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i out of memory 0 --- inspect 170     170     15000   2200    9.3   0      - --- inspect - --- inspect
termination-memory-alloca/Masse-alloca_true-termination.c.i out of memory 0 --- inspect 160     160     15000   2100    8.5   0      - --- inspect - --- inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i out of memory 0 --- inspect 160     160     15000   2200    7.9   0      - --- inspect - --- inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i out of memory 0 --- inspect 180     180     15000   2200    1.3   0      - --- inspect - --- inspect
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2600    6.4   0      - --- inspect - --- inspect
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     340   6400    .83  0      - --- inspect - --- inspect
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     370   8200    .85  0      - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     410   6300    1.8   0      - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     1900   5700    1.2   0      - --- inspect - --- inspect
termination-memory-alloca/Urban-alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2700    6.2   .0041 - --- inspect - --- inspect
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 740     740     15000   7700    .18  0      - --- inspect - --- inspect
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     370   6300    .68  0      - --- inspect - --- inspect
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     410   6900    .89  0      - --- inspect - --- inspect
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 340     340     15000   3800    4.5   0      - --- inspect - --- inspect
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     400   8900    .59  0      - --- inspect - --- inspect
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     400   8300    .88  0      - --- inspect - --- inspect
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     350   8200    .29  0      - --- inspect - --- inspect
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 200     200     15000   2400    8.9   0      - --- inspect - --- inspect
termination-memory-alloca/add_last-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     14000   6400    .24  0      - --- inspect - --- inspect
termination-memory-alloca/array01-alloca_true-termination.c.i out of memory 0 --- inspect 650     650     15000   7400    .11  .0041 - --- inspect - --- inspect
termination-memory-alloca/array02-alloca_true-termination.c.i out of memory 0 --- inspect 110     110     15000   1300    .041 0      - --- inspect - --- inspect
termination-memory-alloca/array03-alloca_true-termination.c.i out of memory 0 --- inspect 120     120     15000   1700    .045 0      - --- inspect - --- inspect
termination-memory-alloca/aviad_true-alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2600    8.5   0      - --- inspect - --- inspect
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     370   6400    .69  0      - --- inspect - --- inspect
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     420   6800    .66  .0041 - --- inspect - --- inspect
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     410   7200    .90  0      - --- inspect - --- inspect
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     320   11000    .29  0      - --- inspect - --- inspect
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .087 .086 8.0 .71 .016 0      - --- inspect - --- inspect
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     450   7700    .72  0      - --- inspect - --- inspect
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     360   5900    .48  0      - --- inspect - --- inspect
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     390   7400    .48  0      - --- inspect - --- inspect
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 210     210     15000   2700    8.9   .0041 - --- inspect - --- inspect
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 250     250     15000   3600    2.1   0      - --- inspect - --- inspect
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 150     150     15000   1800    .045 0      - --- inspect - --- inspect
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 150     150     15000   1900    .037 0      - --- inspect - --- inspect
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 240     240     15000   3700    5.5   0      - --- inspect - --- inspect
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 270     270     15000   3300    3.7   .0041 - --- inspect - --- inspect
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     11000   9300    .46  0      - --- inspect - --- inspect
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     12000   9600    .098 0      - --- inspect - --- inspect
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 730     730     15000   6200    .60  0      - --- inspect - --- inspect
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 860     860     15000   9900    .074 0      - --- inspect - --- inspect
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 140     140     15000   1700    .045 0      - --- inspect - --- inspect
termination-memory-alloca/bubblesort-alloca_true-termination.c.i out of memory 0 --- inspect 110     110     15000   1500    .045 0      - --- inspect - --- inspect
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 750     750     15000   8200    .41  0      - --- inspect - --- inspect
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 690     690     15000   7800    .28  0      - --- inspect - --- inspect
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     10000   9400    .23  0      - --- inspect - --- inspect
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 270     270     15000   3100    3.3   0      - --- inspect - --- inspect
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i error (42) 0 --- inspect 880     880     610   7000    .59  0      - --- inspect - --- inspect
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i out of memory 0 --- inspect 750     750     15000   8500    .25  0      - --- inspect - --- inspect
termination-memory-alloca/count_down-alloca_true-termination.c.i out of memory 0 --- inspect 140     140     15000   1700    .041 0      - --- inspect - --- inspect
termination-memory-alloca/cstrcat-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     4100   9000    7.9   0      - --- inspect - --- inspect
termination-memory-alloca/cstrchr-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     370   6400    .59  0      - --- inspect - --- inspect
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     340   6600    .81  0      - --- inspect - --- inspect
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     14000   4600    .70  0      - --- inspect - --- inspect
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2200    .037 0      - --- inspect - --- inspect
termination-memory-alloca/cstrlen-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     340   5200    .65  0      - --- inspect - --- inspect
termination-memory-alloca/cstrncat-alloca_true-termination.c.i error (42) 0 --- inspect 870     880     2400   7000    6.6   0      - --- inspect - --- inspect
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     270   8200    .58  0      - --- inspect - --- inspect
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     5200   6900    1.3   0      - --- inspect - --- inspect
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2500    .045 .0041 - --- inspect - --- inspect
termination-memory-alloca/cstrspn-alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2700    .037 0      - --- inspect - --- inspect
termination-memory-alloca/diff-alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2300    .045 .0041 - --- inspect - --- inspect
termination-memory-alloca/easySum-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     320   6100    .60  0      - --- inspect - --- inspect
termination-memory-alloca/ex1-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     2600   6500    .59  0      - --- inspect - --- inspect
termination-memory-alloca/ex2-alloca_true-termination.c.i out of memory 0 --- inspect 220     220     15000   3100    2.9   0      - --- inspect - --- inspect
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect .16  .16  11   2.1  .033 0      - --- inspect - --- inspect
termination-memory-alloca/ex3b-alloca_true-termination.c.i true 2 wit inspect 7.7   7.7   56   92    .17  0      - --- inspect - --- inspect
termination-memory-alloca/fermat-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     15000   12000    .80  .32   - --- inspect - --- inspect
termination-memory-alloca/flag-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     390   6600    .63  0      - --- inspect - --- inspect
termination-memory-alloca/gcd1-alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2600    .037 0      - --- inspect - --- inspect
termination-memory-alloca/genady-alloca_true-termination.c.i true 2 wit inspect 3.8   3.8   36   56    1.6   0      - --- inspect - --- inspect
termination-memory-alloca/insertionsort-alloca_true-termination.c.i out of memory 0 --- inspect 150     150     15000   1900    8.3   .0041 - --- inspect - --- inspect
termination-memory-alloca/java_AG313-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     370   6700    .87  0      - --- inspect - --- inspect
termination-memory-alloca/java_Break-alloca_true-termination.c.i true 2 wit inspect .13  .13  8.6 1.3  .041 0      - --- inspect - --- inspect
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i out of memory 0 --- inspect 110     110     15000   1400    .045 0      - --- inspect - --- inspect
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i true 2 wit inspect .20  .20  8.6 2.7  .066 0      - --- inspect - --- inspect
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i true 2 wit inspect .67  .67  16   8.4  .12  0      - --- inspect - --- inspect
termination-memory-alloca/java_Nested-alloca_true-termination.c.i true 2 wit inspect .17  .17  8.4 1.8  .061 0      - --- inspect - --- inspect
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i true 2 wit inspect .32  .32  8.1 3.4  .12  0      - --- inspect - --- inspect
termination-memory-alloca/lis-alloca_true-termination.c.i out of memory 0 --- inspect 110     110     15000   1400    .045 0      - --- inspect - --- inspect
termination-memory-alloca/min_rf-alloca_true-termination.c.i out of memory 0 --- inspect 230     230     15000   3100    6.3   .0041 - --- inspect - --- inspect
termination-memory-alloca/mult_array-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     2200   7000    5.2   0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i error (42) 0 --- inspect 870     880     14000   5100    .54  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     420   7300    .59  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i error (42) 0 --- inspect 870     880     13000   8500    .68  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i error (42) 0 --- inspect 870     880     14000   5400    .85  .094  - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i error (42) 0 --- inspect 870     880     14000   5100    .72  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     5200   5900    .79  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     3900   8000    8.0   0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     350   5300    .78  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     14000   5900    .72  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i out of memory 0 --- inspect 260     260     15000   3000    8.3   0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     2200   7700    3.6   0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     340   6000    .61  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     2300   6200    1.7   0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     240   4900    .70  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     5200   6400    .79  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     350   6100    .90  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     13000   12000    .10  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i out of memory 0 --- inspect 210     210     15000   3000    .037 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i out of memory 0 --- inspect 480     480     15000   6100    .045 0      - --- inspect - --- inspect
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     610   8200    .31  0      - --- inspect - --- inspect
termination-memory-alloca/selectionsort-alloca_true-termination.c.i out of memory 0 --- inspect 120     120     15000   1600    .045 0      - --- inspect - --- inspect
termination-memory-alloca/stroeder1-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     430   5700    .62  0      - --- inspect - --- inspect
termination-memory-alloca/stroeder2-alloca_true-termination.c.i out of memory 0 --- inspect 690     690     15000   6600    .85  0      - --- inspect - --- inspect
termination-memory-alloca/strreplace-alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2800    8.7   0      - --- inspect - --- inspect
termination-memory-alloca/subseq-alloca_true-termination.c.i out of memory 0 --- inspect 300     300     15000   4100    4.9   0      - --- inspect - --- inspect
termination-memory-alloca/substring-alloca_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2500    .037 0      - --- inspect - --- inspect
termination-memory-alloca/twisted-alloca_true-termination.c.i true 2 wit inspect .084 .083 8.7 .83 .016 0      - --- inspect - --- inspect
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i error (42) 0 --- inspect 880     880     3000   5400    2.0   0      error (invalid witness file) 0 --- inspect .65 .40 42 0   0   error (2) 0 --- inspect .021 .023 5.7 0   0  
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i error (42) 0 --- inspect 870     880     2700   5700    1.9   0      error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .023 .025 5.6 0   0  
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i error (42) 0 --- inspect 880     880     2700   5800    2.0   0      error (invalid witness file) 0 --- inspect .75 .45 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0   0  
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i error (42) 0 --- inspect 880     880     3900   9200    6.0   0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0  
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i error (42) 0 --- inspect 880     880     4400   8800    1.9   0      error (invalid witness file) 0 --- inspect .73 .45 41 0   0   error (2) 0 --- inspect .022 .024 5.6 0   0  
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i error (42) 0 --- inspect 880     880     1800   8100    .31  0      error (invalid witness file) 0 --- inspect .76 .45 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0   0  
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i error (42) 0 --- inspect 880     880     3000   7000    2.5   0      error (invalid witness file) 0 --- inspect .77 .49 41 0   0   error (2) 0 --- inspect .023 .023 5.6 0   0  
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i error (42) 0 --- inspect 880     880     3200   6800    5.0   0      error (invalid witness file) 0 --- inspect .60 .35 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     1800   8300    .21  0      - --- inspect - --- inspect
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     2700   5800    2.1   0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     6100   9900    1.8   0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     6400   9300    1.0   0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     1800   8600    .32  0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     2600   5800    1.2   0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     2700   5300    1.2   0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     2800   6100    1.9   0      - --- inspect - --- inspect
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i error (42) 0 --- inspect 880     880     3000   6500    2.5   0      - --- inspect - --- inspect
termination-15/add_first_alloca_true-termination.c.i error (42) 0 --- inspect 870     880     14000   8900    .24  0      - --- inspect - --- inspect
termination-15/array05_alloca_true-termination.c.i error (42) 0 --- inspect 870     880     13000   6800    .47  0      - --- inspect - --- inspect
termination-15/array06_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     1100   8100    2.0   0      - --- inspect - --- inspect
termination-15/array07_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     1100   7000    2.0   0      - --- inspect - --- inspect
termination-15/array08_alloca_true-termination.c.i out of memory 0 --- inspect 490     490     15000   7000    2.3   0      - --- inspect - --- inspect
termination-15/array09_alloca_true-termination.c.i out of memory 0 --- inspect 500     500     15000   6000    2.1   0      - --- inspect - --- inspect
termination-15/array10_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     13000   6400    .46  0      - --- inspect - --- inspect
termination-15/array12_alloca_true-termination.c.i out of memory 0 --- inspect 220     220     15000   2800    5.4   0      - --- inspect - --- inspect
termination-15/array13_alloca_true-termination.c.i out of memory 0 --- inspect 220     220     15000   2700    5.7   0      - --- inspect - --- inspect
termination-15/array16_alloca_fixed_true-termination.c.i out of memory 0 --- inspect 220     220     15000   2700    5.5   0      - --- inspect - --- inspect
termination-15/array17_alloca_true-termination.c.i out of memory 0 --- inspect 270     270     15000   3500    3.7   0      - --- inspect - --- inspect
termination-15/array18_alloca_true-termination.c.i out of memory 0 --- inspect 490     490     15000   7100    1.2   0      - --- inspect - --- inspect
termination-15/count_up_alloca_true-termination.c.i out of memory 0 --- inspect 140     140     15000   2100    .045 .0041 - --- inspect - --- inspect
termination-15/count_up_and_down_alloca_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2900    .037 0      - --- inspect - --- inspect
termination-15/cstrcat_diffterm_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     4100   7900    7.9   0      - --- inspect - --- inspect
termination-15/cstrcat_malloc_true-termination.c.i error (42) 0 --- inspect 880     880     2600   13000    8.1   0      - --- inspect - --- inspect
termination-15/cstrcat_mixed_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     3900   8000    7.7   0      - --- inspect - --- inspect
termination-15/cstrcat_reverse_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     4000   9200    8.1   0      - --- inspect - --- inspect
termination-15/cstrchr_diffterm_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     370   6900    .88  0      - --- inspect - --- inspect
termination-15/cstrchr_malloc_true-termination.c.i error (42) 0 --- inspect 880     880     280   7100    1.4   0      - --- inspect - --- inspect
termination-15/cstrchr_reverse_alloca_true-termination.c.i error (42) 0 --- inspect 870     880     13000   6200    .48  0      - --- inspect - --- inspect
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     340   5900    .81  0      - --- inspect - --- inspect
termination-15/cstrcmp_malloc_true-termination.c.i error (42) 0 --- inspect 880     880     230   8100    2.5   0      - --- inspect - --- inspect
termination-15/cstrcmp_mixed_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     13000   6800    .77  0      - --- inspect - --- inspect
termination-15/cstrcmp_reverse_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     13000   6500    .77  0      - --- inspect - --- inspect
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     14000   6600    .70  .094  - --- inspect - --- inspect
termination-15/cstrcpy_malloc_true-termination.c.i error (42) 0 --- inspect 880     880     5900   6500    1.8   0      - --- inspect - --- inspect
termination-15/cstrcpy_mixed_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     15000   6600    .35  0      - --- inspect - --- inspect
termination-15/cstrcpy_reverse_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     15000   6200    .35  0      - --- inspect - --- inspect
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2400    .037 .0041 - --- inspect - --- inspect
termination-15/cstrcspn_malloc_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2400    .037 .0041 - --- inspect - --- inspect
termination-15/cstrcspn_mixed_alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2700    .037 .0041 - --- inspect - --- inspect
termination-15/cstrcspn_reverse_alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2500    .045 0      - --- inspect - --- inspect
termination-15/cstrlen_diffterm_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     350   7300    .63  0      - --- inspect - --- inspect
termination-15/cstrlen_malloc_true-termination.c.i error (42) 0 --- inspect 880     880     340   6700    1.5   0      - --- inspect - --- inspect
termination-15/cstrlen_reverse_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     13000   6100    .36  0      - --- inspect - --- inspect
termination-15/cstrncat_diffterm_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     2400   7700    6.6   0      - --- inspect - --- inspect
termination-15/cstrncat_malloc_true-termination.c.i error (42) 0 --- inspect 880     880     1800   9500    8.8   0      - --- inspect - --- inspect
termination-15/cstrncat_mixed_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     2400   7800    6.4   0      - --- inspect - --- inspect
termination-15/cstrncat_reverse_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     2400   8500    6.4   0      - --- inspect - --- inspect
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     260   7600    .59  0      - --- inspect - --- inspect
termination-15/cstrncmp_malloc_true-termination.c.i error (42) 0 --- inspect 880     880     250   8600    6.0   0      - --- inspect - --- inspect
termination-15/cstrncmp_mixed_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     4300   6400    .54  0      - --- inspect - --- inspect
termination-15/cstrncmp_reverse_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     8400   6900    .54  0      - --- inspect - --- inspect
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     5200   6500    1.3   0      - --- inspect - --- inspect
termination-15/cstrncpy_malloc_true-termination.c.i error (42) 0 --- inspect 880     880     5300   11000    9.2   0      - --- inspect - --- inspect
termination-15/cstrncpy_mixed_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     15000   8700    .19  0      - --- inspect - --- inspect
termination-15/cstrncpy_reverse_alloca_true-termination.c.i error (42) 0 --- inspect 880     880     15000   7300    .20  0      - --- inspect - --- inspect
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2500    .037 0      - --- inspect - --- inspect
termination-15/cstrpbrk_malloc_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2200    .037 0      - --- inspect - --- inspect
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2400    .037 0      - --- inspect - --- inspect
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2600    .037 .0041 - --- inspect - --- inspect
termination-15/cstrspn_diffterm_alloca_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2900    .037 .0041 - --- inspect - --- inspect
termination-15/cstrspn_malloc_true-termination.c.i out of memory 0 --- inspect 190     190     15000   2200    .037 .0041 - --- inspect - --- inspect
termination-15/cstrspn_mixed_alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2700    .037 0      - --- inspect - --- inspect
termination-15/cstrspn_reverse_alloca_true-termination.c.i out of memory 0 --- inspect 200     200     15000   2800    .037 0      - --- inspect - --- inspect
termination-15/array04_alloca_false-termination.c.i error (42) 0 --- inspect 880     880     9200   8300    .76  .13   error (invalid witness file) 0 --- inspect .74 .45 40 0   0   error (2) 0 --- inspect .027 .028 5.7 0   0  
termination-15/array14_alloca_false-termination.c.i out of memory 0 --- inspect 220     220     15000   3000    5.5   0      error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
termination-15/array15_alloca_false-termination.c.i out of memory 0 --- inspect 220     220     15000   2900    5.6   0      error (invalid witness file) 0 --- inspect .63 .39 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0  
termination-15/array16_alloca_original_false-termination.c.i out of memory 0 --- inspect 220     220     15000   2600    5.8   .0041 error (invalid witness file) 0 --- inspect .77 .48 42 0   0   error (2) 0 --- inspect .027 .027 5.6 0   0  
termination-15/array19_alloca_false-termination.c.i error (42) 0 --- inspect 880     880     9200   6600    .76  0      error (invalid witness file) 0 --- inspect .64 .40 40 0   0   error (2) 0 --- inspect .031 .032 5.6 0   0  
termination-15/array20_alloca_false-termination.c.i out of memory 0 --- inspect 490     490     15000   6300    1.3   0      error (invalid witness file) 0 --- inspect .63 .40 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0  
termination-recursive-malloc/chunk1_true-termination.c.i error (42) 0 --- inspect 880     880     930   9000    .50  0      - --- inspect - --- inspect
termination-recursive-malloc/chunk2_true-termination.c.i error (134) 0 --- inspect .088 .087 9.8 1.3  .066 0      - --- inspect - --- inspect
termination-recursive-malloc/chunk3_true-termination.c.i error (134) 0 --- inspect .13  .13  10   .87 .070 0      - --- inspect - --- inspect
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i out of memory 0 --- inspect 390     390     15000   5200    .045 0      - --- inspect - --- inspect
termination-recursive-malloc/mergeSort_true-termination.c.i out of memory 0 --- inspect 130     130     15000   1700    .037 0      - --- inspect - --- inspect
termination-recursive-malloc/mutual_simple2_true-termination.c.i out of memory 0 --- inspect 210     210     15000   2500    .037 .0041 - --- inspect - --- inspect
termination-recursive-malloc/mutual_simple_true-termination.c.i error (42) 0 --- inspect 880     880     1000   10000    .81  0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i out of memory 0 --- inspect 140     140     15000   1800    .045 .0041 - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i out of memory 0 --- inspect 160     160     15000   1900    .045 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i out of memory 0 --- inspect 150     140     15000   1900    .045 .0041 - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i out of memory 0 --- inspect 140     140     15000   2000    .045 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i out of memory 0 --- inspect 170     170     15000   1900    .045 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i out of memory 0 --- inspect 130     130     15000   1400    .045 .0041 - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i out of memory 0 --- inspect 120     120     15000   1400    28     .0041 - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i out of memory 0 --- inspect 120     120     15000   1400    .045 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i out of memory 0 --- inspect 150     140     15000   1800    .045 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i out of memory 0 --- inspect 120     120     15000   1600    .045 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i out of memory 0 --- inspect 180     180     15000   2000    .037 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i error (42) 0 --- inspect 880     880     2000   7500    .36  0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i out of memory 0 --- inspect 270     270     15000   4000    .42  .0041 - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i out of memory 0 --- inspect 280     280     15000   3200    1.9   0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i out of memory 0 --- inspect 270     270     15000   3100    1.5   0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i out of memory 0 --- inspect 120     120     15000   1700    .045 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i error (42) 0 --- inspect 880     880     2700   7300    8.2   .0041 - --- inspect - --- inspect
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i error (42) 0 --- inspect 880     880     5900   10000    .70  0      - --- inspect - --- inspect
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i error (42) 0 --- inspect 880     880     600   9700    .31  0      - --- inspect - --- inspect
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i out of memory 0 --- inspect 120     120     15000   1500    .041 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 22 150000 150000 2300000 1400000 530   .77 16 0 11 6.8 650 0   0   16 0 .38 .40 90 0   0  
    correct results 11 22 13 13 180 170 2.3 0    0 0
        correct true 11 22 13 13 180 170 2.3 0    0 0
        correct false 0 0 0
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (259 tasks, max score: 502) 22 0 0
Run set cbmc-path.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-termination.Termination-MainHeap