Tool AProVE CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon077; apollon078; apollon084; apollon161] [apollon077; apollon078; apollon084; apollon124]
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-11-30 15:55:47 CET 2017-11-30 15:57:34 CET
Run set aprove.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-aprove.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-aprove.sv-comp18-violation-witness.Termination-MainHeap
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/aprove.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/aprove.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
termination-libowfat/atoi_true-termination.c.i true 2 wit inspect 87   5300 740 - wit inspect - wit inspect
termination-libowfat/atol_true-termination.c.i true 2 wit inspect 77   5400 620 - wit inspect - wit inspect
termination-libowfat/atoll_true-termination.c.i true 2 wit inspect 75   5400 610 - wit inspect - wit inspect
termination-libowfat/basename_true-termination.c.i timeout 0 wit inspect 910   14000 4900 - wit inspect - wit inspect
termination-libowfat/build_fullname_true-termination.c.i error (1) 0 wit inspect 54   3500 490 - wit inspect - wit inspect
termination-libowfat/dirname_true-termination.c.i error (1) 0 wit inspect 22   3600 200 - wit inspect - wit inspect
termination-libowfat/skip_to_true-termination.c.i true 2 wit inspect 29   3600 240 - wit inspect - wit inspect
termination-libowfat/stpcpy_true-termination.c.i timeout 0 wit inspect 900   5200 15000 - wit inspect - wit inspect
termination-libowfat/strcasecmp_true-termination.c.i error (1) 0 wit inspect 5.8 420 45 - wit inspect - wit inspect
termination-libowfat/strcat_short_true-termination.c.i error (1) 0 wit inspect 7.5 690 64 - wit inspect - wit inspect
termination-libowfat/strcat_true-termination.c.i error (1) 0 wit inspect 7.6 700 66 - wit inspect - wit inspect
termination-libowfat/strchr_short_true-termination.c.i true 2 wit inspect 11   760 81 - wit inspect - wit inspect
termination-libowfat/strchr_true-termination.c.i true 2 wit inspect 64   3600 520 - wit inspect - wit inspect
termination-libowfat/strcmp_short_true-termination.c.i true 2 wit inspect 15   1300 110 - wit inspect - wit inspect
termination-libowfat/strcpy_small_true-termination.c.i timeout 0 wit inspect 900   5200 11000 - wit inspect - wit inspect
termination-libowfat/strcspn_true-termination.c.i timeout 0 wit inspect 900   6100 6700 - wit inspect - wit inspect
termination-libowfat/strdup_true-termination.c.i true 2 wit inspect 45   3600 460 - wit inspect - wit inspect
termination-libowfat/strlcat_true-termination.c.i error (1) 0 wit inspect 210   5500 2100 - wit inspect - wit inspect
termination-libowfat/strlcpy_true-termination.c.i timeout 0 wit inspect 910   6100 5900 - wit inspect - wit inspect
termination-libowfat/strlen_true-termination.c.i true 2 wit inspect 42   3600 330 - wit inspect - wit inspect
termination-libowfat/strpbrk_true-termination.c.i timeout 0 wit inspect 900   11000 8700 - wit inspect - wit inspect
termination-libowfat/strrchr_short_true-termination.c.i true 2 wit inspect 40   3100 280 - wit inspect - wit inspect
termination-libowfat/strrchr_true-termination.c.i timeout 0 wit inspect 900   5100 11000 - wit inspect - wit inspect
termination-libowfat/strspn_true-termination.c.i true 2 wit inspect 120   5200 1100 - wit inspect - wit inspect
termination-libowfat/strstr_true-termination.c.i true 2 wit inspect 250   3600 2200 - wit inspect - wit inspect
termination-libowfat/strtok_r_true-termination.c.i timeout 0 wit inspect 900   6500 10000 - wit inspect - wit inspect
termination-libowfat/strtol_true-termination.c.i timeout 0 wit inspect 900   200 10000 - wit inspect - wit inspect
termination-libowfat/strtoul_true-termination.c.i timeout 0 wit inspect 900   200 9800 - wit inspect - wit inspect
termination-libowfat/strtoull_true-termination.c.i timeout 0 wit inspect 900   190 9800 - wit inspect - wit inspect
termination-libowfat/wcsrchr_true-termination.c.i out of memory 0 wit inspect 900   15000 4700 - wit inspect - wit inspect
termination-libowfat/wcsstr_true-termination.c.i timeout 0 wit inspect 910   10000 5300 - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i false(termination) 1 wit inspect 7.3 420 62 error 0 wit inspect 2.5  180 false(termination) 1 wit inspect 6.3   260  
termination-memory-alloca/Velroyen-alloca_false-termination.c.i false(termination) 1 wit inspect 17   590 110 error 0 wit inspect 2.4  170 false(termination) 1 wit inspect 4.8   280  
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i true 2 wit inspect 38   2400 300 - wit inspect - wit inspect
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i true 2 wit inspect 17   1200 110 - wit inspect - wit inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i true 2 wit inspect 25   1800 150 - wit inspect - wit inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i true 2 wit inspect 7.8 500 58 - wit inspect - wit inspect
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i true 2 wit inspect 8.5 540 68 - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i true 2 wit inspect 18   1000 120 - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i true 2 wit inspect 25   1500 150 - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i true 2 wit inspect 170   5600 920 - wit inspect - wit inspect
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i timeout 0 wit inspect 900   4500 12000 - wit inspect - wit inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i true 2 wit inspect 6.6 520 54 - wit inspect - wit inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i true 2 wit inspect 17   1000 110 - wit inspect - wit inspect
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i timeout 0 wit inspect 900   3500 12000 - wit inspect - wit inspect
termination-memory-alloca/Masse-alloca_true-termination.c.i timeout 0 wit inspect 910   10000 4100 - wit inspect - wit inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i true 2 wit inspect 56   3700 440 - wit inspect - wit inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i true 2 wit inspect 43   3700 370 - wit inspect - wit inspect
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i timeout 0 wit inspect 910   14000 4700 - wit inspect - wit inspect
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i true 2 wit inspect 10   730 70 - wit inspect - wit inspect
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i true 2 wit inspect 11   760 71 - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i true 2 wit inspect 8.2 590 62 - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i true 2 wit inspect 8.7 660 64 - wit inspect - wit inspect
termination-memory-alloca/Urban-alloca_true-termination.c.i true 2 wit inspect 76   4600 450 - wit inspect - wit inspect
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 22   1600 160 - wit inspect - wit inspect
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 5.9 460 44 - wit inspect - wit inspect
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 7.5 460 54 - wit inspect - wit inspect
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   3700 11000 - wit inspect - wit inspect
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 12   750 82 - wit inspect - wit inspect
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 8.2 600 66 - wit inspect - wit inspect
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 14   890 100 - wit inspect - wit inspect
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 3.4 270 29 - wit inspect - wit inspect
termination-memory-alloca/add_last-alloca_true-termination.c.i error (1) 0 wit inspect 19   1100 160 - wit inspect - wit inspect
termination-memory-alloca/array01-alloca_true-termination.c.i true 2 wit inspect 65   3900 490 - wit inspect - wit inspect
termination-memory-alloca/array02-alloca_true-termination.c.i true 2 wit inspect 160   5300 1300 - wit inspect - wit inspect
termination-memory-alloca/array03-alloca_true-termination.c.i true 2 wit inspect 270   5900 2000 - wit inspect - wit inspect
termination-memory-alloca/aviad_true-alloca_true-termination.c.i true 2 wit inspect 55   3500 360 - wit inspect - wit inspect
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 6.7 440 51 - wit inspect - wit inspect
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 7.2 470 54 - wit inspect - wit inspect
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 12   810 87 - wit inspect - wit inspect
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 13   840 110 - wit inspect - wit inspect
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 3.6 290 32 - wit inspect - wit inspect
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 8.1 680 65 - wit inspect - wit inspect
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 17   1300 130 - wit inspect - wit inspect
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 12   750 87 - wit inspect - wit inspect
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 3.8 330 34 - wit inspect - wit inspect
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 3.9 320 32 - wit inspect - wit inspect
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 39   3500 300 - wit inspect - wit inspect
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i error (1) 0 wit inspect 7.4 690 70 - wit inspect - wit inspect
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 13   1000 95 - wit inspect - wit inspect
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 16   1200 110 - wit inspect - wit inspect
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 15   1200 120 - wit inspect - wit inspect
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 9.1 710 67 - wit inspect - wit inspect
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 14   880 90 - wit inspect - wit inspect
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 14   1100 100 - wit inspect - wit inspect
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 9.8 740 68 - wit inspect - wit inspect
termination-memory-alloca/bubblesort-alloca_true-termination.c.i true 2 wit inspect 230   5600 1800 - wit inspect - wit inspect
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 31   2200 190 - wit inspect - wit inspect
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 33   2100 220 - wit inspect - wit inspect
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 23   1800 170 - wit inspect - wit inspect
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 21   1900 150 - wit inspect - wit inspect
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 15   1300 110 - wit inspect - wit inspect
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 21   1500 150 - wit inspect - wit inspect
termination-memory-alloca/count_down-alloca_true-termination.c.i true 2 wit inspect 110   5400 1000 - wit inspect - wit inspect
termination-memory-alloca/cstrcat-alloca_true-termination.c.i timeout 0 wit inspect 910   5700 4900 - wit inspect - wit inspect
termination-memory-alloca/cstrchr-alloca_true-termination.c.i true 2 wit inspect 11   740 80 - wit inspect - wit inspect
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i true 2 wit inspect 24   1600 160 - wit inspect - wit inspect
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i true 2 wit inspect 95   3500 1000 - wit inspect - wit inspect
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i true 2 wit inspect 96   5300 670 - wit inspect - wit inspect
termination-memory-alloca/cstrlen-alloca_true-termination.c.i true 2 wit inspect 7.7 630 59 - wit inspect - wit inspect
termination-memory-alloca/cstrncat-alloca_true-termination.c.i error (1) 0 wit inspect 90   3700 740 - wit inspect - wit inspect
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i true 2 wit inspect 30   2300 240 - wit inspect - wit inspect
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i true 2 wit inspect 84   3800 710 - wit inspect - wit inspect
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i true 2 wit inspect 52   4000 390 - wit inspect - wit inspect
termination-memory-alloca/cstrspn-alloca_true-termination.c.i true 2 wit inspect 56   4600 420 - wit inspect - wit inspect
termination-memory-alloca/diff-alloca_true-termination.c.i true 2 wit inspect 61   3600 490 - wit inspect - wit inspect
termination-memory-alloca/easySum-alloca_true-termination.c.i true 2 wit inspect 67   2300 750 - wit inspect - wit inspect
termination-memory-alloca/ex1-alloca_true-termination.c.i true 2 wit inspect 8.5 520 61 - wit inspect - wit inspect
termination-memory-alloca/ex2-alloca_true-termination.c.i timeout 0 wit inspect 910   6100 5300 - wit inspect - wit inspect
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 9.8 730 80 - wit inspect - wit inspect
termination-memory-alloca/ex3b-alloca_true-termination.c.i true 2 wit inspect 15   1200 120 - wit inspect - wit inspect
termination-memory-alloca/fermat-alloca_true-termination.c.i true 2 wit inspect 120   4100 870 - wit inspect - wit inspect
termination-memory-alloca/flag-alloca_true-termination.c.i true 2 wit inspect 16   1300 110 - wit inspect - wit inspect
termination-memory-alloca/gcd1-alloca_true-termination.c.i true 2 wit inspect 83   4200 550 - wit inspect - wit inspect
termination-memory-alloca/genady-alloca_true-termination.c.i timeout 0 wit inspect 900   3600 14000 - wit inspect - wit inspect
termination-memory-alloca/insertionsort-alloca_true-termination.c.i true 2 wit inspect 100   3800 1000 - wit inspect - wit inspect
termination-memory-alloca/java_AG313-alloca_true-termination.c.i true 2 wit inspect 26   2000 170 - wit inspect - wit inspect
termination-memory-alloca/java_Break-alloca_true-termination.c.i true 2 wit inspect 7.3 500 54 - wit inspect - wit inspect
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i error (1) 0 wit inspect 190   5100 2000 - wit inspect - wit inspect
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i true 2 wit inspect 9.7 740 66 - wit inspect - wit inspect
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i true 2 wit inspect 7.7 530 64 - wit inspect - wit inspect
termination-memory-alloca/java_Nested-alloca_true-termination.c.i true 2 wit inspect 34   2400 210 - wit inspect - wit inspect
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i true 2 wit inspect 10   740 71 - wit inspect - wit inspect
termination-memory-alloca/lis-alloca_true-termination.c.i timeout 0 wit inspect 900   3600 11000 - wit inspect - wit inspect
termination-memory-alloca/min_rf-alloca_true-termination.c.i true 2 wit inspect 94   3600 750 - wit inspect - wit inspect
termination-memory-alloca/mult_array-alloca_true-termination.c.i error (1) 0 wit inspect 50   3600 510 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i true 2 wit inspect 12   800 89 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i true 2 wit inspect 20   1500 150 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i true 2 wit inspect 25   2300 200 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i true 2 wit inspect 24   1400 160 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i true 2 wit inspect 81   3600 970 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i true 2 wit inspect 72   3700 720 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i timeout 0 wit inspect 910   5700 5500 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i true 2 wit inspect 22   2100 170 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i true 2 wit inspect 89   2300 930 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i timeout 0 wit inspect 910   8100 5100 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i true 2 wit inspect 43   4200 310 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i true 2 wit inspect 10   630 66 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i error (1) 0 wit inspect 79   3800 730 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i true 2 wit inspect 29   2400 230 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i true 2 wit inspect 48   4800 390 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i true 2 wit inspect 18   1300 120 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i true 2 wit inspect 34   3700 280 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i timeout 0 wit inspect 910   7900 4100 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i true 2 wit inspect 160   5800 1100 - wit inspect - wit inspect
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i true 2 wit inspect 13   1200 91 - wit inspect - wit inspect
termination-memory-alloca/selectionsort-alloca_true-termination.c.i timeout 0 wit inspect 900   11000 6900 - wit inspect - wit inspect
termination-memory-alloca/stroeder1-alloca_true-termination.c.i true 2 wit inspect 21   2300 170 - wit inspect - wit inspect
termination-memory-alloca/stroeder2-alloca_true-termination.c.i true 2 wit inspect 76   3900 560 - wit inspect - wit inspect
termination-memory-alloca/strreplace-alloca_true-termination.c.i true 2 wit inspect 45   3600 320 - wit inspect - wit inspect
termination-memory-alloca/subseq-alloca_true-termination.c.i true 2 wit inspect 42   3700 320 - wit inspect - wit inspect
termination-memory-alloca/substring-alloca_true-termination.c.i true 2 wit inspect 56   3700 450 - wit inspect - wit inspect
termination-memory-alloca/twisted-alloca_true-termination.c.i true 2 wit inspect 5.9 410 43 - wit inspect - wit inspect
termination-memory-linkedlists/cll_by_lseg-alloca_false-termination.c.i false(termination) 0 wit inspect 16   1100 97 error 0 wit inspect 2.5  180 unknown 0 wit inspect 30     1600  
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i error (1) 0 wit inspect 26   1600 210 error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .023 4.8
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i error (1) 0 wit inspect 52   3700 410 error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .018 5.0
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i error (1) 0 wit inspect 43   3700 330 error (invalid witness file) 0 wit inspect .44 43 error (2) 0 wit inspect .049 4.8
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i error (1) 0 wit inspect 11   1000 87 error (invalid witness file) 0 wit inspect .43 41 error (2) 0 wit inspect .018 4.8
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i error (1) 0 wit inspect 11   880 86 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .020 4.9
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i error (1) 0 wit inspect 19   1100 140 error (invalid witness file) 0 wit inspect .42 41 error (2) 0 wit inspect .040 4.9
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i error (1) 0 wit inspect 66   3900 480 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.8
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i error (1) 0 wit inspect 58   2600 430 error (invalid witness file) 0 wit inspect .45 44 error (2) 0 wit inspect .018 4.8
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i true 2 wit inspect 15   1300 120 - wit inspect - wit inspect
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i error (1) 0 wit inspect 48   3700 420 - wit inspect - wit inspect
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i error (1) 0 wit inspect 14   1000 96 - wit inspect - wit inspect
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i error (1) 0 wit inspect 9.7 710 68 - wit inspect - wit inspect
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i true 2 wit inspect 9.2 620 76 - wit inspect - wit inspect
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i error (1) 0 wit inspect 37   2400 320 - wit inspect - wit inspect
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i error (1) 0 wit inspect 33   1900 260 - wit inspect - wit inspect
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i error (1) 0 wit inspect 24   1400 180 - wit inspect - wit inspect
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i error (1) 0 wit inspect 61   3600 470 - wit inspect - wit inspect
termination-15/add_first_alloca_true-termination.c.i error (1) 0 wit inspect 14   970 110 - wit inspect - wit inspect
termination-15/array05_alloca_true-termination.c.i error (1) 0 wit inspect 30   1600 230 - wit inspect - wit inspect
termination-15/array06_alloca_true-termination.c.i true 2 wit inspect 27   1700 160 - wit inspect - wit inspect
termination-15/array07_alloca_true-termination.c.i true 2 wit inspect 29   1700 210 - wit inspect - wit inspect
termination-15/array08_alloca_true-termination.c.i timeout 0 wit inspect 900   14000 4700 - wit inspect - wit inspect
termination-15/array09_alloca_true-termination.c.i out of memory 0 wit inspect 900   15000 4700 - wit inspect - wit inspect
termination-15/array10_alloca_true-termination.c.i error (1) 0 wit inspect 30   1700 220 - wit inspect - wit inspect
termination-15/array12_alloca_true-termination.c.i error (1) 0 wit inspect 55   5200 640 - wit inspect - wit inspect
termination-15/array13_alloca_true-termination.c.i error (1) 0 wit inspect 61   3600 640 - wit inspect - wit inspect
termination-15/array16_alloca_fixed_true-termination.c.i error (1) 0 wit inspect 46   5200 500 - wit inspect - wit inspect
termination-15/array17_alloca_true-termination.c.i error (1) 0 wit inspect 63   3800 470 - wit inspect - wit inspect
termination-15/array18_alloca_true-termination.c.i timeout 0 wit inspect 910   14000 4800 - wit inspect - wit inspect
termination-15/count_up_alloca_true-termination.c.i true 2 wit inspect 98   5400 770 - wit inspect - wit inspect
termination-15/count_up_and_down_alloca_true-termination.c.i true 2 wit inspect 65   3600 640 - wit inspect - wit inspect
termination-15/cstrcat_diffterm_alloca_true-termination.c.i timeout 0 wit inspect 910   5200 5200 - wit inspect - wit inspect
termination-15/cstrcat_malloc_true-termination.c.i timeout 0 wit inspect 910   5800 6200 - wit inspect - wit inspect
termination-15/cstrcat_mixed_alloca_true-termination.c.i timeout 0 wit inspect 910   5700 5300 - wit inspect - wit inspect
termination-15/cstrcat_reverse_alloca_true-termination.c.i timeout 0 wit inspect 910   5500 5500 - wit inspect - wit inspect
termination-15/cstrchr_diffterm_alloca_true-termination.c.i true 2 wit inspect 10   750 78 - wit inspect - wit inspect
termination-15/cstrchr_malloc_true-termination.c.i true 2 wit inspect 10   740 74 - wit inspect - wit inspect
termination-15/cstrchr_reverse_alloca_true-termination.c.i true 2 wit inspect 10   750 73 - wit inspect - wit inspect
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i true 2 wit inspect 22   1600 160 - wit inspect - wit inspect
termination-15/cstrcmp_malloc_true-termination.c.i true 2 wit inspect 24   2400 210 - wit inspect - wit inspect
termination-15/cstrcmp_mixed_alloca_true-termination.c.i true 2 wit inspect 22   1400 150 - wit inspect - wit inspect
termination-15/cstrcmp_reverse_alloca_true-termination.c.i true 2 wit inspect 23   1600 170 - wit inspect - wit inspect
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i timeout 0 wit inspect 900   5200 14000 - wit inspect - wit inspect
termination-15/cstrcpy_malloc_true-termination.c.i true 2 wit inspect 87   2300 1100 - wit inspect - wit inspect
termination-15/cstrcpy_mixed_alloca_true-termination.c.i timeout 0 wit inspect 900   5200 13000 - wit inspect - wit inspect
termination-15/cstrcpy_reverse_alloca_true-termination.c.i timeout 0 wit inspect 900   5200 14000 - wit inspect - wit inspect
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i true 2 wit inspect 95   5400 660 - wit inspect - wit inspect
termination-15/cstrcspn_malloc_true-termination.c.i true 2 wit inspect 98   5400 690 - wit inspect - wit inspect
termination-15/cstrcspn_mixed_alloca_true-termination.c.i true 2 wit inspect 88   5400 680 - wit inspect - wit inspect
termination-15/cstrcspn_reverse_alloca_true-termination.c.i true 2 wit inspect 99   5300 630 - wit inspect - wit inspect
termination-15/cstrlen_diffterm_alloca_true-termination.c.i true 2 wit inspect 8.0 670 66 - wit inspect - wit inspect
termination-15/cstrlen_malloc_true-termination.c.i true 2 wit inspect 10   750 79 - wit inspect - wit inspect
termination-15/cstrlen_reverse_alloca_true-termination.c.i true 2 wit inspect 8.1 660 66 - wit inspect - wit inspect
termination-15/cstrncat_diffterm_alloca_true-termination.c.i error (1) 0 wit inspect 87   3600 730 - wit inspect - wit inspect
termination-15/cstrncat_malloc_true-termination.c.i error (1) 0 wit inspect 120   3900 1000 - wit inspect - wit inspect
termination-15/cstrncat_mixed_alloca_true-termination.c.i error (1) 0 wit inspect 99   3700 800 - wit inspect - wit inspect
termination-15/cstrncat_reverse_alloca_true-termination.c.i error (1) 0 wit inspect 100   3700 900 - wit inspect - wit inspect
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i true 2 wit inspect 29   2900 240 - wit inspect - wit inspect
termination-15/cstrncmp_malloc_true-termination.c.i true 2 wit inspect 34   3400 300 - wit inspect - wit inspect
termination-15/cstrncmp_mixed_alloca_true-termination.c.i true 2 wit inspect 29   3000 220 - wit inspect - wit inspect
termination-15/cstrncmp_reverse_alloca_true-termination.c.i true 2 wit inspect 30   2600 270 - wit inspect - wit inspect
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i true 2 wit inspect 81   3800 650 - wit inspect - wit inspect
termination-15/cstrncpy_malloc_true-termination.c.i true 2 wit inspect 78   3800 590 - wit inspect - wit inspect
termination-15/cstrncpy_mixed_alloca_true-termination.c.i error (1) 0 wit inspect 71   3800 590 - wit inspect - wit inspect
termination-15/cstrncpy_reverse_alloca_true-termination.c.i error (1) 0 wit inspect 73   3800 640 - wit inspect - wit inspect
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i true 2 wit inspect 53   4800 430 - wit inspect - wit inspect
termination-15/cstrpbrk_malloc_true-termination.c.i true 2 wit inspect 55   5000 400 - wit inspect - wit inspect
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i true 2 wit inspect 51   4800 390 - wit inspect - wit inspect
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i true 2 wit inspect 53   4900 420 - wit inspect - wit inspect
termination-15/cstrspn_diffterm_alloca_true-termination.c.i true 2 wit inspect 58   5000 440 - wit inspect - wit inspect
termination-15/cstrspn_malloc_true-termination.c.i true 2 wit inspect 60   5100 410 - wit inspect - wit inspect
termination-15/cstrspn_mixed_alloca_true-termination.c.i true 2 wit inspect 53   5100 390 - wit inspect - wit inspect
termination-15/cstrspn_reverse_alloca_true-termination.c.i true 2 wit inspect 60   4800 430 - wit inspect - wit inspect
termination-15/array04_alloca_false-termination.c.i false(termination) 1 wit inspect 28   1800 190 error 0 wit inspect 2.5  170 false(termination) 1 wit inspect 4.8   270  
termination-15/array14_alloca_false-termination.c.i error (1) 0 wit inspect 66   5200 680 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.9
termination-15/array15_alloca_false-termination.c.i error (1) 0 wit inspect 54   2900 590 error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .019 4.9
termination-15/array16_alloca_original_false-termination.c.i timeout 0 wit inspect 900   14000 9300 error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .020 4.9
termination-15/array19_alloca_false-termination.c.i false(termination) 1 wit inspect 32   2000 200 error 0 wit inspect 1.8  180 false(termination) 1 wit inspect 6.8   270  
termination-15/array20_alloca_false-termination.c.i timeout 0 wit inspect 900   13000 4900 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .036 4.8
termination-recursive-malloc/chunk1_true-termination.c.i error (1) 0 wit inspect 5.5 440 38 - wit inspect - wit inspect
termination-recursive-malloc/chunk2_true-termination.c.i error (1) 0 wit inspect 16   1200 110 - wit inspect - wit inspect
termination-recursive-malloc/chunk3_true-termination.c.i error (1) 0 wit inspect 13   1200 89 - wit inspect - wit inspect
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i error (1) 0 wit inspect 17   1300 150 - wit inspect - wit inspect
termination-recursive-malloc/mergeSort_true-termination.c.i error (1) 0 wit inspect 20   1200 150 - wit inspect - wit inspect
termination-recursive-malloc/mutual_simple2_true-termination.c.i true 2 wit inspect 13   760 97 - wit inspect - wit inspect
termination-recursive-malloc/mutual_simple_true-termination.c.i true 2 wit inspect 5.8 370 39 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i true 2 wit inspect 12   790 86 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i true 2 wit inspect 35   2000 240 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i true 2 wit inspect 18   1400 140 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i true 2 wit inspect 25   1600 180 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i true 2 wit inspect 16   1100 100 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i true 2 wit inspect 18   1200 120 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i true 2 wit inspect 18   1300 140 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i true 2 wit inspect 27   1300 160 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i true 2 wit inspect 15   1300 120 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i true 2 wit inspect 47   3100 300 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i true 2 wit inspect 19   1500 140 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i error (1) 0 wit inspect 15   1000 130 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i true 2 wit inspect 9.3 710 72 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i true 2 wit inspect 12   720 94 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i true 2 wit inspect 14   1200 100 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i true 2 wit inspect 18   1000 110 - wit inspect - wit inspect
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i error (1) 0 wit inspect 19   1300 130 - wit inspect - wit inspect
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i error (1) 0 wit inspect 7.0 670 52 - wit inspect - wit inspect
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i true 2 wit inspect 8.4 660 69 - wit inspect - wit inspect
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i error (1) 0 wit inspect 19   1000 140 - wit inspect - wit inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 260 336 43000 800000 380000 17 0 17 1400 17 4 53 2800
    correct results 170 336 6800 390000 53000 0 4 4 23 1100
        correct true 166 332 6700 390000 53000 0 0
        correct false 4 4 83 4800 560 0 4 4 23 1100
    correct-unconfimed results 1 0 16 1100 97 0 0
        correct-unconfirmed true 0 0 0
        correct-unconfirmed false 1 0 16 1100 97 0 0
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (260 tasks, max score: 503) 336 0 4
Run set aprove.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-aprove.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-aprove.sv-comp18-violation-witness.Termination-MainHeap