Tool AProVE 84fce4cdfd 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:41:51 CET 2018-12-05 09:26:55 CET 2018-12-05 09:29:10 CET
Run set aprove.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-aprove.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-aprove.sv-comp19_prop-termination.Termination-MainHeap
Options -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/aprove.2018-12-04_2241.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/aprove.2018-12-04_2241.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 true 2 --- inspect 72   24   2500 590 .24  0      - --- inspect - --- inspect
termination-libowfat/atol_true-termination.c.i true 2 --- inspect 78   23   2500 580 .26  .25   - --- inspect - --- inspect
termination-libowfat/atoll_true-termination.c.i true 2 --- inspect 71   23   3800 600 .21  18      - --- inspect - --- inspect
termination-libowfat/basename_true-termination.c.i out of memory 0 --- inspect 900   160   15000 4600 2.6   74      - --- inspect - --- inspect
termination-libowfat/build_fullname_true-termination.c.i error (1) 0 --- inspect 51   27   1900 630 .033 57      - --- inspect - --- inspect
termination-libowfat/dirname_true-termination.c.i timeout 0 --- inspect 910   180   13000 5100 17     1.4    - --- inspect - --- inspect
termination-libowfat/skip_to_true-termination.c.i true 2 --- inspect 25   10   2300 220 .18  0      - --- inspect - --- inspect
termination-libowfat/stpcpy_true-termination.c.i error (1) 0 --- inspect 15   4.0 810 120 .17  .21   - --- inspect - --- inspect
termination-libowfat/strcasecmp_true-termination.c.i error (1) 0 --- inspect 5.9 2.2 470 57 .033 57      - --- inspect - --- inspect
termination-libowfat/strcat_short_true-termination.c.i error (1) 0 --- inspect 7.5 2.3 680 63 .033 .48   - --- inspect - --- inspect
termination-libowfat/strcat_true-termination.c.i error (1) 0 --- inspect 7.7 2.3 680 63 .033 .41   - --- inspect - --- inspect
termination-libowfat/strchr_short_true-termination.c.i true 2 --- inspect 13   3.3 740 100 .066 0      - --- inspect - --- inspect
termination-libowfat/strchr_true-termination.c.i true 2 --- inspect 49   25   2300 440 .066 .21   - --- inspect - --- inspect
termination-libowfat/strcmp_short_true-termination.c.i true 2 --- inspect 15   4.0 1200 140 .066 .21   - --- inspect - --- inspect
termination-libowfat/strcpy_small_true-termination.c.i error (1) 0 --- inspect 15   4.0 810 120 .16  .14   - --- inspect - --- inspect
termination-libowfat/strcspn_true-termination.c.i timeout 0 --- inspect 910   260   6400 7000 160     1.4    - --- inspect - --- inspect
termination-libowfat/strdup_true-termination.c.i true 2 --- inspect 36   17   2300 350 .070 0      - --- inspect - --- inspect
termination-libowfat/strlcat_true-termination.c.i error (1) 0 --- inspect 210   100   4600 1800 .93  .0041 - --- inspect - --- inspect
termination-libowfat/strlcpy_true-termination.c.i error (1) 0 --- inspect 130   41   3700 1100 .83  75      - --- inspect - --- inspect
termination-libowfat/strlen_true-termination.c.i true 2 --- inspect 27   12   2300 270 1.0   0      - --- inspect - --- inspect
termination-libowfat/strpbrk_true-termination.c.i timeout 0 --- inspect 900   420   9600 7600 .51  .25   - --- inspect - --- inspect
termination-libowfat/strrchr_short_true-termination.c.i true 2 --- inspect 40   8.2 2800 260 .18  1.6    - --- inspect - --- inspect
termination-libowfat/strrchr_true-termination.c.i timeout 0 --- inspect 900   830   2500 12000 .016 .12   - --- inspect - --- inspect
termination-libowfat/strspn_true-termination.c.i true 2 --- inspect 110   67   2300 1100 .20  0      - --- inspect - --- inspect
termination-libowfat/strstr_true-termination.c.i true 2 --- inspect 180   110   3400 1800 .42  .12   - --- inspect - --- inspect
termination-libowfat/strtok_r_true-termination.c.i timeout 0 --- inspect 900   440   7700 8000 1.0   .21   - --- inspect - --- inspect
termination-libowfat/strtol_true-termination.c.i timeout 0 --- inspect 900   900   160 11000 .016 0      - --- inspect - --- inspect
termination-libowfat/strtoul_true-termination.c.i timeout 0 --- inspect 900   900   150 12000 .016 .21   - --- inspect - --- inspect
termination-libowfat/strtoull_true-termination.c.i timeout 0 --- inspect 900   900   150 12000 .016 0      - --- inspect - --- inspect
termination-libowfat/wcsrchr_true-termination.c.i out of memory 0 --- inspect 880   160   15000 4900 .27  .12   - --- inspect - --- inspect
termination-libowfat/wcsstr_true-termination.c.i timeout 0 --- inspect 910   280   12000 6300 .26  .21   - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i false(termination) 1 wit inspect 6.8 1.9 380 55 .48  0      false(termination) 1 wit inspect 4.8  2.6  260 0   0   true -32 --- inspect 14     8.2   470   .66 0  
termination-memory-alloca/Velroyen-alloca_false-termination.c.i false(termination) 1 wit inspect 16   2.9 550 100 .31  0      false(termination) 1 wit inspect 8.8  4.7  430 0   0   false(termination) 1 --- inspect 9.3   5.6   320   .62 0  
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i true 2 --- inspect 26   9.0 2300 210 .11  0      - --- inspect - --- inspect
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i true 2 --- inspect 14   3.5 1000 110 .14  0      - --- inspect - --- inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i true 2 --- inspect 24   5.1 1900 160 .15  0      - --- inspect - --- inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i true 2 --- inspect 7.6 2.3 470 57 .87  0      - --- inspect - --- inspect
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i true 2 --- inspect 7.9 2.0 460 57 .13  0      - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i true 2 --- inspect 16   3.4 1100 110 .15  74      - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i true 2 --- inspect 23   4.4 1700 150 .26  0      - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i true 2 --- inspect 68   12   5500 480 .23  0      - --- inspect - --- inspect
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i true 2 --- inspect 14   3.3 760 110 .10  0      - --- inspect - --- inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i true 2 --- inspect 6.4 2.0 450 56 .033 0      - --- inspect - --- inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i true 2 --- inspect 14   2.8 1300 86 .15  .086  - --- inspect - --- inspect
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 900   870   2300 12000 .016 0      - --- inspect - --- inspect
termination-memory-alloca/Masse-alloca_true-termination.c.i timeout 0 --- inspect 910   140   10000 4800 28     .27   - --- inspect - --- inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i true 2 --- inspect 45   17   2800 420 .22  0      - --- inspect - --- inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i true 2 --- inspect 39   13   2400 330 .18  0      - --- inspect - --- inspect
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i out of memory 0 --- inspect 800   110   15000 4600 11     0      - --- inspect - --- inspect
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i true 2 --- inspect 9.4 2.6 660 70 .098 72      - --- inspect - --- inspect
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i true 2 --- inspect 11   2.7 780 83 .094 0      - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i true 2 --- inspect 8.7 2.1 630 63 .16  0      - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i true 2 --- inspect 9.3 2.3 640 73 .15  0      - --- inspect - --- inspect
termination-memory-alloca/Urban-alloca_true-termination.c.i true 2 --- inspect 52   10   4600 330 .42  0      - --- inspect - --- inspect
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 24   5.4 2000 190 .14  .086  - --- inspect - --- inspect
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 6.9 1.9 440 51 .061 .0041 - --- inspect - --- inspect
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 7.0 2.0 450 56 .070 0      - --- inspect - --- inspect
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 390   350   2500 4500 .11  .0041 - --- inspect - --- inspect
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 11   3.0 730 84 .070 .0041 - --- inspect - --- inspect
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 7.8 2.2 490 61 .066 .20   - --- inspect - --- inspect
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 15   3.5 830 110 .16  0      - --- inspect - --- inspect
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 3.4 1.3 260 29 .033 0      - --- inspect - --- inspect
termination-memory-alloca/add_last-alloca_true-termination.c.i error (1) 0 --- inspect 16   4.2 850 130 .18  .23   - --- inspect - --- inspect
termination-memory-alloca/array01-alloca_true-termination.c.i true 2 --- inspect 62   18   3400 470 .31  1.0    - --- inspect - --- inspect
termination-memory-alloca/array02-alloca_true-termination.c.i true 2 --- inspect 120   66   2800 1200 .10  0      - --- inspect - --- inspect
termination-memory-alloca/array03-alloca_true-termination.c.i true 2 --- inspect 130   60   3800 1200 .20  0      - --- inspect - --- inspect
termination-memory-alloca/aviad_true-alloca_true-termination.c.i true 2 --- inspect 48   11   3300 350 .27  18      - --- inspect - --- inspect
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 6.5 1.9 440 52 .078 0      - --- inspect - --- inspect
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 7.5 2.1 450 66 .074 .086  - --- inspect - --- inspect
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 12   3.5 780 100 1.1   73      - --- inspect - --- inspect
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 13   3.1 750 100 .14  .086  - --- inspect - --- inspect
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 3.8 1.4 260 32 .033 0      - --- inspect - --- inspect
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 8.1 2.2 560 62 .066 .086  - --- inspect - --- inspect
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 17   4.5 1300 130 .082 0      - --- inspect - --- inspect
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 11   2.9 750 95 .070 0      - --- inspect - --- inspect
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 3.7 1.3 270 34 .033 0      - --- inspect - --- inspect
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 3.8 1.6 330 35 .033 57      - --- inspect - --- inspect
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 28   6.2 1600 220 .15  0      - --- inspect - --- inspect
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i error (1) 0 --- inspect 7.0 2.1 470 69 .033 0      - --- inspect - --- inspect
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 16   3.5 810 120 .14  .086  - --- inspect - --- inspect
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 20   4.2 1200 140 .16  18      - --- inspect - --- inspect
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 14   3.7 1100 120 .057 0      - --- inspect - --- inspect
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 9.1 2.4 660 71 .066 0      - --- inspect - --- inspect
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 16   3.5 910 120 .14  0      - --- inspect - --- inspect
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 15   3.6 980 110 .14  0      - --- inspect - --- inspect
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 10   2.7 670 92 .48  .086  - --- inspect - --- inspect
termination-memory-alloca/bubblesort-alloca_true-termination.c.i timeout 0 --- inspect 910   220   11000 5600 1.9   .13   - --- inspect - --- inspect
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 30   6.7 2400 210 .16  17      - --- inspect - --- inspect
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 33   7.2 2600 250 .14  .098  - --- inspect - --- inspect
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 24   6.0 2100 170 .18  18      - --- inspect - --- inspect
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 25   5.2 1700 180 .18  .086  - --- inspect - --- inspect
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 15   4.2 1200 120 .066 0      - --- inspect - --- inspect
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 22   5.6 2100 170 .18  17      - --- inspect - --- inspect
termination-memory-alloca/count_down-alloca_true-termination.c.i true 2 --- inspect 110   42   3400 950 .32  .81   - --- inspect - --- inspect
termination-memory-alloca/cstrcat-alloca_true-termination.c.i error (1) 0 --- inspect 75   22   2900 550 .57  .0041 - --- inspect - --- inspect
termination-memory-alloca/cstrchr-alloca_true-termination.c.i true 2 --- inspect 11   2.9 730 94 .078 0      - --- inspect - --- inspect
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i true 2 --- inspect 21   5.5 1400 170 .066 0      - --- inspect - --- inspect
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i true 2 --- inspect 96   79   2300 1300 .033 0      - --- inspect - --- inspect
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i true 2 --- inspect 72   21   4700 610 .16  0      - --- inspect - --- inspect
termination-memory-alloca/cstrlen-alloca_true-termination.c.i true 2 --- inspect 8.3 2.3 570 73 .070 .025  - --- inspect - --- inspect
termination-memory-alloca/cstrncat-alloca_true-termination.c.i error (1) 0 --- inspect 95   34   3800 710 .55  0      - --- inspect - --- inspect
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i true 2 --- inspect 25   7.5 2300 230 .11  3.3    - --- inspect - --- inspect
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i timeout 0 --- inspect 900   440   5200 9200 .36  0      - --- inspect - --- inspect
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i true 2 --- inspect 47   15   4600 400 .18  0      - --- inspect - --- inspect
termination-memory-alloca/cstrspn-alloca_true-termination.c.i true 2 --- inspect 50   16   4500 420 .11  .18   - --- inspect - --- inspect
termination-memory-alloca/diff-alloca_true-termination.c.i true 2 --- inspect 52   22   3600 520 .086 0      - --- inspect - --- inspect
termination-memory-alloca/easySum-alloca_true-termination.c.i true 2 --- inspect 51   30   2300 580 .041 0      - --- inspect - --- inspect
termination-memory-alloca/ex1-alloca_true-termination.c.i true 2 --- inspect 8.3 2.4 540 68 .066 0      - --- inspect - --- inspect
termination-memory-alloca/ex2-alloca_true-termination.c.i timeout 0 --- inspect 910   130   8600 5100 18     .0041 - --- inspect - --- inspect
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 10   2.6 700 76 .082 0      - --- inspect - --- inspect
termination-memory-alloca/ex3b-alloca_true-termination.c.i true 2 --- inspect 16   4.1 1100 140 .070 0      - --- inspect - --- inspect
termination-memory-alloca/fermat-alloca_true-termination.c.i true 2 --- inspect 88   28   3700 740 .32  0      - --- inspect - --- inspect
termination-memory-alloca/flag-alloca_true-termination.c.i true 2 --- inspect 17   4.9 1300 150 .92  0      - --- inspect - --- inspect
termination-memory-alloca/gcd1-alloca_true-termination.c.i true 2 --- inspect 80   16   4200 520 .97  3.4    - --- inspect - --- inspect
termination-memory-alloca/genady-alloca_true-termination.c.i true 2 --- inspect 17   6.3 1900 140 .082 71      - --- inspect - --- inspect
termination-memory-alloca/insertionsort-alloca_true-termination.c.i true 2 --- inspect 86   49   2600 870 .16  .086  - --- inspect - --- inspect
termination-memory-alloca/java_AG313-alloca_true-termination.c.i true 2 --- inspect 24   5.5 1700 200 .090 .13   - --- inspect - --- inspect
termination-memory-alloca/java_Break-alloca_true-termination.c.i true 2 --- inspect 7.0 1.9 450 57 .082 0      - --- inspect - --- inspect
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i timeout 0 --- inspect 900   260   12000 6000 1.7   .13   - --- inspect - --- inspect
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i true 2 --- inspect 10   2.7 740 73 .13  0      - --- inspect - --- inspect
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i true 2 --- inspect 8.8 2.4 500 75 .094 0      - --- inspect - --- inspect
termination-memory-alloca/java_Nested-alloca_true-termination.c.i true 2 --- inspect 25   7.4 2400 210 .16  0      - --- inspect - --- inspect
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i true 2 --- inspect 11   2.7 760 86 .12  0      - --- inspect - --- inspect
termination-memory-alloca/lis-alloca_true-termination.c.i error (1) 0 --- inspect 80   52   2300 980 0     0      - --- inspect - --- inspect
termination-memory-alloca/min_rf-alloca_true-termination.c.i true 2 --- inspect 73   28   2500 570 .21  1.0    - --- inspect - --- inspect
termination-memory-alloca/mult_array-alloca_true-termination.c.i error (1) 0 --- inspect 48   26   2300 530 .033 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i true 2 --- inspect 13   3.2 750 96 .066 .012  - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i true 2 --- inspect 22   5.1 1400 160 .082 17      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i true 2 --- inspect 26   6.8 2300 200 .086 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i true 2 --- inspect 19   4.7 1300 150 .066 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i true 2 --- inspect 79   57   2300 900 .037 .037  - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i true 2 --- inspect 64   29   2700 560 .20  .26   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i error (1) 0 --- inspect 73   21   3100 610 .71  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i true 2 --- inspect 21   5.8 1900 190 .070 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i true 2 --- inspect 74   53   2300 890 .037 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i timeout 0 --- inspect 900   150   11000 4800 120     .35   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i true 2 --- inspect 45   13   2600 360 .19  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i true 2 --- inspect 8.5 2.3 550 71 .066 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i error (1) 0 --- inspect 82   35   2300 710 .36  1.8    - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i true 2 --- inspect 27   7.7 2300 240 .090 .086  - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i true 2 --- inspect 51   18   2500 440 .19  0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i true 2 --- inspect 15   4.0 1300 120 .045 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i true 2 --- inspect 34   10   2300 260 .14  .094  - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i timeout 0 --- inspect 910   130   10000 4900 38     1.8    - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i true 2 --- inspect 190   48   5500 1300 1.4   18      - --- inspect - --- inspect
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i true 2 --- inspect 13   3.5 950 120 .070 .086  - --- inspect - --- inspect
termination-memory-alloca/selectionsort-alloca_true-termination.c.i timeout 0 --- inspect 900   330   11000 7100 2.0   .22   - --- inspect - --- inspect
termination-memory-alloca/stroeder1-alloca_true-termination.c.i true 2 --- inspect 24   6.4 2100 190 .082 .11   - --- inspect - --- inspect
termination-memory-alloca/stroeder2-alloca_true-termination.c.i true 2 --- inspect 61   18   2600 510 .25  0      - --- inspect - --- inspect
termination-memory-alloca/strreplace-alloca_true-termination.c.i true 2 --- inspect 43   11   2500 320 .21  0      - --- inspect - --- inspect
termination-memory-alloca/subseq-alloca_true-termination.c.i true 2 --- inspect 40   11   3400 310 .18  0      - --- inspect - --- inspect
termination-memory-alloca/substring-alloca_true-termination.c.i true 2 --- inspect 55   17   3500 450 .20  .0041 - --- inspect - --- inspect
termination-memory-alloca/twisted-alloca_true-termination.c.i true 2 --- inspect 5.6 1.8 390 52 .033 0      - --- inspect - --- inspect
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i error (1) 0 --- inspect 23   5.8 1400 170 .21  0      error (invalid witness file) 0 --- inspect .64 .41 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0  
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i error (1) 0 --- inspect 39   12   2400 300 .24  0      error (invalid witness file) 0 --- inspect .66 .40 40 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0  
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i error (1) 0 --- inspect 33   10   2000 290 .21  74      error (invalid witness file) 0 --- inspect .63 .39 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i error (1) 0 --- inspect 12   3.7 990 97 .033 0      error (invalid witness file) 0 --- inspect .73 .45 40 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i error (1) 0 --- inspect 11   3.2 880 100 .033 .20   error (invalid witness file) 0 --- inspect .58 .35 42 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0  
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i error (1) 0 --- inspect 22   4.5 1000 140 .65  .20   error (invalid witness file) 0 --- inspect .68 .41 42 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i error (1) 0 --- inspect 58   18   2600 440 .28  74      error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i error (1) 0 --- inspect 46   14   2500 380 .29  .34   error (invalid witness file) 0 --- inspect .57 .36 40 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0  
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i true 2 --- inspect 13   3.8 1200 120 .070 .20   - --- inspect - --- inspect
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i error (1) 0 --- inspect 43   14   2300 400 .50  .23   - --- inspect - --- inspect
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i error (1) 0 --- inspect 13   3.7 1100 100 .033 0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i error (1) 0 --- inspect 9.7 2.8 690 84 .033 0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i true 2 --- inspect 10   2.7 710 79 .082 14      - --- inspect - --- inspect
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i true 2 --- inspect 25   6.2 1700 190 .12  0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i true 2 --- inspect 21   5.2 1300 170 .11  .29   - --- inspect - --- inspect
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i true 2 --- inspect 21   5.0 1300 160 .12  0      - --- inspect - --- inspect
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i error (1) 0 --- inspect 47   17   2400 400 .52  .20   - --- inspect - --- inspect
termination-15/add_first_alloca_true-termination.c.i error (1) 0 --- inspect 14   3.7 810 110 .19  .070  - --- inspect - --- inspect
termination-15/array05_alloca_true-termination.c.i error (1) 0 --- inspect 33   7.4 1500 250 .20  .070  - --- inspect - --- inspect
termination-15/array06_alloca_true-termination.c.i true 2 --- inspect 29   6.3 1400 230 .20  .30   - --- inspect - --- inspect
termination-15/array07_alloca_true-termination.c.i true 2 --- inspect 28   6.3 1600 200 .14  74      - --- inspect - --- inspect
termination-15/array08_alloca_true-termination.c.i timeout 0 --- inspect 900   200   14000 5400 .43  .070  - --- inspect - --- inspect
termination-15/array09_alloca_true-termination.c.i timeout 0 --- inspect 910   180   13000 4900 .43  .16   - --- inspect - --- inspect
termination-15/array10_alloca_true-termination.c.i error (1) 0 --- inspect 32   7.5 1500 240 .20  .29   - --- inspect - --- inspect
termination-15/array12_alloca_true-termination.c.i error (1) 0 --- inspect 57   39   2300 700 0     .85   - --- inspect - --- inspect
termination-15/array13_alloca_true-termination.c.i error (1) 0 --- inspect 67   45   2300 700 0     .070  - --- inspect - --- inspect
termination-15/array16_alloca_fixed_true-termination.c.i error (1) 0 --- inspect 51   28   3500 550 .033 .17   - --- inspect - --- inspect
termination-15/array17_alloca_true-termination.c.i error (1) 0 --- inspect 57   18   2400 420 .39  .23   - --- inspect - --- inspect
termination-15/array18_alloca_true-termination.c.i timeout 0 --- inspect 910   190   13000 4700 .35  1.4    - --- inspect - --- inspect
termination-15/count_up_alloca_true-termination.c.i true 2 --- inspect 100   40   4300 1000 .34  0      - --- inspect - --- inspect
termination-15/count_up_and_down_alloca_true-termination.c.i true 2 --- inspect 69   35   2500 640 .22  0      - --- inspect - --- inspect
termination-15/cstrcat_diffterm_alloca_true-termination.c.i error (1) 0 --- inspect 77   22   2700 550 .63  0      - --- inspect - --- inspect
termination-15/cstrcat_malloc_true-termination.c.i error (1) 0 --- inspect 69   22   2600 550 .43  0      - --- inspect - --- inspect
termination-15/cstrcat_mixed_alloca_true-termination.c.i error (1) 0 --- inspect 74   21   3000 570 .41  .070  - --- inspect - --- inspect
termination-15/cstrcat_reverse_alloca_true-termination.c.i error (1) 0 --- inspect 65   18   2400 470 .44  0      - --- inspect - --- inspect
termination-15/cstrchr_diffterm_alloca_true-termination.c.i true 2 --- inspect 11   3.0 740 94 .082 .71   - --- inspect - --- inspect
termination-15/cstrchr_malloc_true-termination.c.i true 2 --- inspect 11   2.8 740 91 .078 .16   - --- inspect - --- inspect
termination-15/cstrchr_reverse_alloca_true-termination.c.i true 2 --- inspect 11   2.9 730 90 .094 0      - --- inspect - --- inspect
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i true 2 --- inspect 22   5.9 1500 170 .066 .16   - --- inspect - --- inspect
termination-15/cstrcmp_malloc_true-termination.c.i true 2 --- inspect 24   6.9 2300 220 .066 .070  - --- inspect - --- inspect
termination-15/cstrcmp_mixed_alloca_true-termination.c.i true 2 --- inspect 20   5.7 1600 180 .074 .070  - --- inspect - --- inspect
termination-15/cstrcmp_reverse_alloca_true-termination.c.i true 2 --- inspect 22   5.9 1800 180 .082 .070  - --- inspect - --- inspect
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i error (1) 0 --- inspect 22   5.5 1400 190 .17  .070  - --- inspect - --- inspect
termination-15/cstrcpy_malloc_true-termination.c.i true 2 --- inspect 97   78   2300 1300 .033 .070  - --- inspect - --- inspect
termination-15/cstrcpy_mixed_alloca_true-termination.c.i error (1) 0 --- inspect 20   5.0 1400 160 .21  .29   - --- inspect - --- inspect
termination-15/cstrcpy_reverse_alloca_true-termination.c.i error (1) 0 --- inspect 21   5.2 1400 180 .18  .070  - --- inspect - --- inspect
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i true 2 --- inspect 80   22   5400 600 .19  .070  - --- inspect - --- inspect
termination-15/cstrcspn_malloc_true-termination.c.i true 2 --- inspect 81   23   5100 660 .23  .070  - --- inspect - --- inspect
termination-15/cstrcspn_mixed_alloca_true-termination.c.i true 2 --- inspect 71   20   4000 510 .15  .16   - --- inspect - --- inspect
termination-15/cstrcspn_reverse_alloca_true-termination.c.i true 2 --- inspect 71   21   4100 630 .21  .070  - --- inspect - --- inspect
termination-15/cstrlen_diffterm_alloca_true-termination.c.i true 2 --- inspect 8.5 2.4 570 65 .066 .16   - --- inspect - --- inspect
termination-15/cstrlen_malloc_true-termination.c.i true 2 --- inspect 9.2 2.5 720 70 .066 0      - --- inspect - --- inspect
termination-15/cstrlen_reverse_alloca_true-termination.c.i true 2 --- inspect 8.6 2.4 570 73 .061 0      - --- inspect - --- inspect
termination-15/cstrncat_diffterm_alloca_true-termination.c.i error (1) 0 --- inspect 96   35   2500 790 .48  0      - --- inspect - --- inspect
termination-15/cstrncat_malloc_true-termination.c.i error (1) 0 --- inspect 110   46   2700 930 1.1   .070  - --- inspect - --- inspect
termination-15/cstrncat_mixed_alloca_true-termination.c.i error (1) 0 --- inspect 92   35   2200 810 .48  74      - --- inspect - --- inspect
termination-15/cstrncat_reverse_alloca_true-termination.c.i error (1) 0 --- inspect 84   35   3900 830 .58  0      - --- inspect - --- inspect
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i true 2 --- inspect 28   7.8 2300 260 .11  1.1    - --- inspect - --- inspect
termination-15/cstrncmp_malloc_true-termination.c.i true 2 --- inspect 26   8.5 2300 260 .11  .25   - --- inspect - --- inspect
termination-15/cstrncmp_mixed_alloca_true-termination.c.i true 2 --- inspect 27   7.6 2300 230 .12  .070  - --- inspect - --- inspect
termination-15/cstrncmp_reverse_alloca_true-termination.c.i true 2 --- inspect 27   7.6 2300 240 .14  .16   - --- inspect - --- inspect
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   430   4200 10000 .33  0      - --- inspect - --- inspect
termination-15/cstrncpy_malloc_true-termination.c.i timeout 0 --- inspect 900   430   3500 11000 .35  .070  - --- inspect - --- inspect
termination-15/cstrncpy_mixed_alloca_true-termination.c.i error (1) 0 --- inspect 68   22   2500 600 .32  0      - --- inspect - --- inspect
termination-15/cstrncpy_reverse_alloca_true-termination.c.i error (1) 0 --- inspect 64   22   2500 500 .32  .070  - --- inspect - --- inspect
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i true 2 --- inspect 55   16   3700 420 .22  .16   - --- inspect - --- inspect
termination-15/cstrpbrk_malloc_true-termination.c.i true 2 --- inspect 49   15   3300 360 .21  74      - --- inspect - --- inspect
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i true 2 --- inspect 44   14   3500 360 .13  5.0    - --- inspect - --- inspect
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i true 2 --- inspect 57   17   5400 430 .29  .070  - --- inspect - --- inspect
termination-15/cstrspn_diffterm_alloca_true-termination.c.i true 2 --- inspect 58   16   2800 480 .20  .070  - --- inspect - --- inspect
termination-15/cstrspn_malloc_true-termination.c.i true 2 --- inspect 54   17   4400 470 .18  .070  - --- inspect - --- inspect
termination-15/cstrspn_mixed_alloca_true-termination.c.i true 2 --- inspect 54   16   3700 470 .20  .070  - --- inspect - --- inspect
termination-15/cstrspn_reverse_alloca_true-termination.c.i true 2 --- inspect 59   17   3800 510 .27  17      - --- inspect - --- inspect
termination-15/array04_alloca_false-termination.c.i false(termination) 1 wit inspect 32   6.9 1500 240 .31  .16   error 0 --- inspect 8.2  4.5  330 0   0   false(termination) 1 --- inspect 9.2   5.5   320   .66 0  
termination-15/array14_alloca_false-termination.c.i error (1) 0 --- inspect 65   44   4600 770 0     .16   error (invalid witness file) 0 --- inspect .70 .42 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0  
termination-15/array15_alloca_false-termination.c.i error (1) 0 --- inspect 58   39   2300 740 0     .25   error (invalid witness file) 0 --- inspect .62 .38 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
termination-15/array16_alloca_original_false-termination.c.i out of memory 0 --- inspect 570   98   15000 3000 4.0   .20   error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0  
termination-15/array19_alloca_false-termination.c.i false(termination) 1 wit inspect 30   6.4 1500 220 .25  .074  error 0 --- inspect 7.8  4.2  330 0   0   false(termination) 1 --- inspect 8.9   5.4   320   .62 0  
termination-15/array20_alloca_false-termination.c.i timeout 0 --- inspect 900   200   13000 5000 .60  0      error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
termination-recursive-malloc/chunk1_true-termination.c.i error (1) 0 --- inspect 5.7 1.8 420 49 .033 0      - --- inspect - --- inspect
termination-recursive-malloc/chunk2_true-termination.c.i error (1) 0 --- inspect 14   3.8 1200 110 .033 .21   - --- inspect - --- inspect
termination-recursive-malloc/chunk3_true-termination.c.i error (1) 0 --- inspect 13   3.7 1200 120 .033 .19   - --- inspect - --- inspect
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i error (1) 0 --- inspect 15   4.6 1200 140 .033 0      - --- inspect - --- inspect
termination-recursive-malloc/mergeSort_true-termination.c.i error (1) 0 --- inspect 19   5.0 1200 170 .033 0      - --- inspect - --- inspect
termination-recursive-malloc/mutual_simple2_true-termination.c.i true 2 --- inspect 11   2.8 710 97 .074 0      - --- inspect - --- inspect
termination-recursive-malloc/mutual_simple_true-termination.c.i true 2 --- inspect 6.2 1.7 320 52 .078 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i true 2 --- inspect 12   3.0 720 93 .070 9.8    - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i true 2 --- inspect 40   6.9 1900 240 .30  0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i true 2 --- inspect 24   5.0 1200 180 .14  0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i true 2 --- inspect 26   5.9 1400 190 .16  0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i true 2 --- inspect 20   4.0 1100 140 .15  0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i true 2 --- inspect 17   3.7 940 120 .14  16      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i true 2 --- inspect 23   4.7 1200 170 .14  0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i true 2 --- inspect 31   5.4 1500 210 .35  0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i true 2 --- inspect 13   3.3 1000 110 .078 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i true 2 --- inspect 64   13   3300 420 .32  .10   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i true 2 --- inspect 18   4.7 1400 130 .12  .10   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i error (1) 0 --- inspect 16   5.3 970 150 .15  0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i true 2 --- inspect 9.1 2.4 650 75 .082 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i true 2 --- inspect 10   2.7 660 84 .082 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i true 2 --- inspect 12   3.2 1100 100 .078 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i true 2 --- inspect 15   3.5 940 110 .16  0      - --- inspect - --- inspect
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i error (1) 0 --- inspect 16   4.6 1200 150 .033 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i error (1) 0 --- inspect 6.7 2.1 490 60 .033 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i true 2 --- inspect 8.2 2.2 520 63 .082 0      - --- inspect - --- inspect
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i error (1) 0 --- inspect 15   4.1 900 140 .033 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 340 34000 13000 690000 280000 460   1200    16 2 37 21   1800 0   0   16 -29 42 25   1500 2.6  0  
    correct results 172 340 6100 2300 320000 53000 30   720    2 2 14 7.3 700 0   0   3 3 27 16   960 1.9  0  
        correct true 168 336 6000 2300 320000 53000 29   720    0 0
        correct false 4 4 85 18 3900 620 1.3 .23 2 2 14 7.3 700 0   0   3 3 27 16   960 1.9  0  
    incorrect results 0 0 1 -32 14 8.2 470 .66 0  
        incorrect true 0 0 1 -32 14 8.2 470 .66 0  
        incorrect false 0 0 0
score (259 tasks, max score: 502) 340 2 -29
Run set aprove.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-aprove.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-aprove.sv-comp19_prop-termination.Termination-MainHeap