Tool ULTIMATE Automizer 0.1.23-3204b741 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-03 12:12:33 CET 2017-12-03 12:33:05 CET 2017-12-03 12:34:35 CET
Run set uautomizer.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Termination-MainHeap
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-03_1212.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/uautomizer.2017-12-03_1212.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 7.2 380 62 - wit inspect - wit inspect
termination-libowfat/atol_true-termination.c.i true 2 wit inspect 7.4 380 58 - wit inspect - wit inspect
termination-libowfat/atoll_true-termination.c.i true 2 wit inspect 7.6 380 62 - wit inspect - wit inspect
termination-libowfat/basename_true-termination.c.i timeout 0 wit inspect 900   14000 5500 - wit inspect - wit inspect
termination-libowfat/build_fullname_true-termination.c.i true 2 wit inspect 23   820 220 - wit inspect - wit inspect
termination-libowfat/dirname_true-termination.c.i timeout 0 wit inspect 910   14000 5600 - wit inspect - wit inspect
termination-libowfat/skip_to_true-termination.c.i unknown 0 wit inspect 57   3700 500 - wit inspect - wit inspect
termination-libowfat/stpcpy_true-termination.c.i true 2 wit inspect 8.8 510 81 - wit inspect - wit inspect
termination-libowfat/strcasecmp_true-termination.c.i true 2 wit inspect 9.8 530 88 - wit inspect - wit inspect
termination-libowfat/strcat_short_true-termination.c.i true 2 wit inspect 12   670 100 - wit inspect - wit inspect
termination-libowfat/strcat_true-termination.c.i error (7) 0 wit inspect 14   580 120 - wit inspect - wit inspect
termination-libowfat/strchr_short_true-termination.c.i true 2 wit inspect 9.0 470 77 - wit inspect - wit inspect
termination-libowfat/strchr_true-termination.c.i true 2 wit inspect 160   6700 1200 - wit inspect - wit inspect
termination-libowfat/strcmp_short_true-termination.c.i true 2 wit inspect 8.7 540 78 - wit inspect - wit inspect
termination-libowfat/strcpy_small_true-termination.c.i true 2 wit inspect 9.0 510 78 - wit inspect - wit inspect
termination-libowfat/strcspn_true-termination.c.i true 2 wit inspect 18   710 160 - wit inspect - wit inspect
termination-libowfat/strdup_true-termination.c.i true 2 wit inspect 13   600 110 - wit inspect - wit inspect
termination-libowfat/strlcat_true-termination.c.i true 2 wit inspect 15   680 130 - wit inspect - wit inspect
termination-libowfat/strlcpy_true-termination.c.i true 2 wit inspect 17   670 140 - wit inspect - wit inspect
termination-libowfat/strlen_true-termination.c.i true 2 wit inspect 7.2 350 62 - wit inspect - wit inspect
termination-libowfat/strpbrk_true-termination.c.i unknown 0 wit inspect 30   1100 240 - wit inspect - wit inspect
termination-libowfat/strrchr_short_true-termination.c.i true 2 wit inspect 8.3 470 65 - wit inspect - wit inspect
termination-libowfat/strrchr_true-termination.c.i true 2 wit inspect 9.4 550 76 - wit inspect - wit inspect
termination-libowfat/strspn_true-termination.c.i true 2 wit inspect 15   720 130 - wit inspect - wit inspect
termination-libowfat/strstr_true-termination.c.i true 2 wit inspect 40   1000 450 - wit inspect - wit inspect
termination-libowfat/strtok_r_true-termination.c.i true 2 wit inspect 59   1200 590 - wit inspect - wit inspect
termination-libowfat/strtol_true-termination.c.i true 2 wit inspect 15   670 140 - wit inspect - wit inspect
termination-libowfat/strtoul_true-termination.c.i true 2 wit inspect 9.6 550 79 - wit inspect - wit inspect
termination-libowfat/strtoull_true-termination.c.i true 2 wit inspect 9.3 550 79 - wit inspect - wit inspect
termination-libowfat/wcsrchr_true-termination.c.i true 2 wit inspect 8.0 410 69 - wit inspect - wit inspect
termination-libowfat/wcsstr_true-termination.c.i true 2 wit inspect 5.6 290 48 - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i false(termination) 1 wit inspect 5.4 300 47 unknown 0 wit inspect 4.7  260 false(termination) 1 wit inspect 7.3   320  
termination-memory-alloca/Velroyen-alloca_false-termination.c.i false(termination) 1 wit inspect 7.8 400 63 unknown 0 wit inspect 3.0  200 false(termination) 1 wit inspect 6.7   270  
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i true 2 wit inspect 17   710 180 - wit inspect - wit inspect
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i true 2 wit inspect 15   700 150 - wit inspect - wit inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i true 2 wit inspect 56   970 590 - wit inspect - wit inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i true 2 wit inspect 8.1 490 69 - wit inspect - wit inspect
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i true 2 wit inspect 61   790 700 - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i true 2 wit inspect 14   640 140 - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i true 2 wit inspect 94   810 1000 - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i true 2 wit inspect 720   1000 10000 - wit inspect - wit inspect
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i timeout 0 wit inspect 900   1700 11000 - wit inspect - wit inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i true 2 wit inspect 39   950 370 - wit inspect - wit inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i true 2 wit inspect 7.4 340 53 - wit inspect - wit inspect
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i true 2 wit inspect 13   570 110 - wit inspect - wit inspect
termination-memory-alloca/Masse-alloca_true-termination.c.i unknown 0 wit inspect 15   630 100 - wit inspect - wit inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i true 2 wit inspect 27   760 280 - wit inspect - wit inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i true 2 wit inspect 33   820 300 - wit inspect - wit inspect
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i timeout 0 wit inspect 910   14000 4400 - wit inspect - wit inspect
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i true 2 wit inspect 15   680 130 - wit inspect - wit inspect
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i true 2 wit inspect 41   830 380 - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i true 2 wit inspect 30   700 310 - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i timeout 0 wit inspect 900   3300 11000 - wit inspect - wit inspect
termination-memory-alloca/Urban-alloca_true-termination.c.i true 2 wit inspect 32   880 310 - wit inspect - wit inspect
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 23   730 220 - wit inspect - wit inspect
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 8.4 480 68 - wit inspect - wit inspect
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 8.7 530 69 - wit inspect - wit inspect
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 15   550 120 - wit inspect - wit inspect
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 12   580 110 - wit inspect - wit inspect
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 9.6 540 81 - wit inspect - wit inspect
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 10   520 91 - wit inspect - wit inspect
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 12   590 120 - wit inspect - wit inspect
termination-memory-alloca/add_last-alloca_true-termination.c.i true 2 wit inspect 7.4 390 57 - wit inspect - wit inspect
termination-memory-alloca/array01-alloca_true-termination.c.i true 2 wit inspect 11   540 91 - wit inspect - wit inspect
termination-memory-alloca/array02-alloca_true-termination.c.i true 2 wit inspect 14   610 120 - wit inspect - wit inspect
termination-memory-alloca/array03-alloca_true-termination.c.i true 2 wit inspect 13   580 130 - wit inspect - wit inspect
termination-memory-alloca/aviad_true-alloca_true-termination.c.i timeout 0 wit inspect 900   910 10000 - wit inspect - wit inspect
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 8.9 480 69 - wit inspect - wit inspect
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 9.8 520 76 - wit inspect - wit inspect
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 9.2 530 89 - wit inspect - wit inspect
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 9.7 520 78 - wit inspect - wit inspect
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 13   600 120 - wit inspect - wit inspect
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 8.7 540 79 - wit inspect - wit inspect
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 10   530 84 - wit inspect - wit inspect
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 14   700 120 - wit inspect - wit inspect
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 40   850 440 - wit inspect - wit inspect
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 20   690 170 - wit inspect - wit inspect
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 14   620 120 - wit inspect - wit inspect
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 34   880 330 - wit inspect - wit inspect
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 12   570 110 - wit inspect - wit inspect
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 17   690 160 - wit inspect - wit inspect
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 14   660 110 - wit inspect - wit inspect
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 15   690 140 - wit inspect - wit inspect
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 15   620 140 - wit inspect - wit inspect
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 19   700 170 - wit inspect - wit inspect
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 16   710 150 - wit inspect - wit inspect
termination-memory-alloca/bubblesort-alloca_true-termination.c.i true 2 wit inspect 11   550 82 - wit inspect - wit inspect
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i error (7) 0 wit inspect 310   2100 4300 - wit inspect - wit inspect
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i error (7) 0 wit inspect 520   2000 6300 - wit inspect - wit inspect
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 34   800 320 - wit inspect - wit inspect
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 43   900 410 - wit inspect - wit inspect
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 12   670 110 - wit inspect - wit inspect
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   1900 12000 - wit inspect - wit inspect
termination-memory-alloca/count_down-alloca_true-termination.c.i true 2 wit inspect 13   580 110 - wit inspect - wit inspect
termination-memory-alloca/cstrcat-alloca_true-termination.c.i true 2 wit inspect 11   570 89 - wit inspect - wit inspect
termination-memory-alloca/cstrchr-alloca_true-termination.c.i true 2 wit inspect 7.8 470 67 - wit inspect - wit inspect
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i true 2 wit inspect 8.8 530 72 - wit inspect - wit inspect
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i true 2 wit inspect 8.9 520 74 - wit inspect - wit inspect
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i true 2 wit inspect 100   730 1200 - wit inspect - wit inspect
termination-memory-alloca/cstrlen-alloca_true-termination.c.i true 2 wit inspect 7.1 370 66 - wit inspect - wit inspect
termination-memory-alloca/cstrncat-alloca_true-termination.c.i true 2 wit inspect 8.9 460 76 - wit inspect - wit inspect
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i true 2 wit inspect 8.9 520 79 - wit inspect - wit inspect
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i true 2 wit inspect 14   610 100 - wit inspect - wit inspect
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i true 2 wit inspect 17   700 160 - wit inspect - wit inspect
termination-memory-alloca/cstrspn-alloca_true-termination.c.i true 2 wit inspect 18   690 180 - wit inspect - wit inspect
termination-memory-alloca/diff-alloca_true-termination.c.i true 2 wit inspect 19   780 190 - wit inspect - wit inspect
termination-memory-alloca/easySum-alloca_true-termination.c.i true 2 wit inspect 9.5 520 78 - wit inspect - wit inspect
termination-memory-alloca/ex1-alloca_true-termination.c.i true 2 wit inspect 58   520 770 - wit inspect - wit inspect
termination-memory-alloca/ex2-alloca_true-termination.c.i unknown 0 wit inspect 46   1400 370 - wit inspect - wit inspect
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i unknown 0 wit inspect 21   800 170 - wit inspect - wit inspect
termination-memory-alloca/ex3b-alloca_true-termination.c.i unknown 0 wit inspect 25   1100 210 - wit inspect - wit inspect
termination-memory-alloca/fermat-alloca_true-termination.c.i timeout 0 wit inspect 900   790 10000 - wit inspect - wit inspect
termination-memory-alloca/flag-alloca_true-termination.c.i true 2 wit inspect 27   1000 250 - wit inspect - wit inspect
termination-memory-alloca/gcd1-alloca_true-termination.c.i true 2 wit inspect 20   740 210 - wit inspect - wit inspect
termination-memory-alloca/genady-alloca_true-termination.c.i true 2 wit inspect 9.5 520 73 - wit inspect - wit inspect
termination-memory-alloca/insertionsort-alloca_true-termination.c.i true 2 wit inspect 12   580 100 - wit inspect - wit inspect
termination-memory-alloca/java_AG313-alloca_true-termination.c.i true 2 wit inspect 10   540 90 - wit inspect - wit inspect
termination-memory-alloca/java_Break-alloca_true-termination.c.i true 2 wit inspect 8.8 510 73 - wit inspect - wit inspect
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i true 2 wit inspect 12   550 100 - wit inspect - wit inspect
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i true 2 wit inspect 56   880 640 - wit inspect - wit inspect
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i true 2 wit inspect 8.3 440 67 - wit inspect - wit inspect
termination-memory-alloca/java_Nested-alloca_true-termination.c.i error (7) 0 wit inspect 120   1000 1300 - wit inspect - wit inspect
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i timeout 0 wit inspect 900   4000 12000 - wit inspect - wit inspect
termination-memory-alloca/lis-alloca_true-termination.c.i error (7) 0 wit inspect 350   1500 4900 - wit inspect - wit inspect
termination-memory-alloca/min_rf-alloca_true-termination.c.i error (7) 0 wit inspect 560   13000 4900 - wit inspect - wit inspect
termination-memory-alloca/mult_array-alloca_true-termination.c.i true 2 wit inspect 13   570 98 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i true 2 wit inspect 8.1 390 59 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i true 2 wit inspect 8.3 450 75 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i true 2 wit inspect 8.5 450 64 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i true 2 wit inspect 8.4 430 68 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i true 2 wit inspect 8.7 500 72 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i true 2 wit inspect 28   720 290 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i true 2 wit inspect 11   550 97 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i true 2 wit inspect 9.3 550 84 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i true 2 wit inspect 8.6 500 69 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i true 2 wit inspect 57   720 700 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i true 2 wit inspect 16   730 120 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i true 2 wit inspect 7.2 370 58 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i true 2 wit inspect 9.4 530 77 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i true 2 wit inspect 8.9 520 86 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i true 2 wit inspect 14   650 120 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i true 2 wit inspect 7.5 440 64 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i true 2 wit inspect 48   740 530 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i true 2 wit inspect 15   710 130 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i true 2 wit inspect 33   940 380 - wit inspect - wit inspect
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i true 2 wit inspect 7.2 330 58 - wit inspect - wit inspect
termination-memory-alloca/selectionsort-alloca_true-termination.c.i true 2 wit inspect 12   600 110 - wit inspect - wit inspect
termination-memory-alloca/stroeder1-alloca_true-termination.c.i true 2 wit inspect 7.1 330 55 - wit inspect - wit inspect
termination-memory-alloca/stroeder2-alloca_true-termination.c.i true 2 wit inspect 10   530 91 - wit inspect - wit inspect
termination-memory-alloca/strreplace-alloca_true-termination.c.i true 2 wit inspect 8.9 470 70 - wit inspect - wit inspect
termination-memory-alloca/subseq-alloca_true-termination.c.i true 2 wit inspect 13   610 97 - wit inspect - wit inspect
termination-memory-alloca/substring-alloca_true-termination.c.i true 2 wit inspect 17   720 140 - wit inspect - wit inspect
termination-memory-alloca/twisted-alloca_true-termination.c.i true 2 wit inspect 28   810 290 - wit inspect - wit inspect
termination-memory-linkedlists/cll_by_lseg-alloca_false-termination.c.i unknown 0 wit inspect 28   940 240 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .018 4.9
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i false(termination) 1 wit inspect 9.7 520 76 unknown 0 wit inspect 3.9  250 false(termination) 1 wit inspect 8.8   390  
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i false(termination) 1 wit inspect 9.6 530 75 unknown 0 wit inspect 4.5  260 false(termination) 1 wit inspect 8.7   370  
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i false(termination) 1 wit inspect 9.0 540 74 unknown 0 wit inspect 4.4  260 false(termination) 1 wit inspect 8.7   350  
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i false(termination) 1 wit inspect 12   550 110 unknown 0 wit inspect 3.1  210 false(termination) 1 wit inspect 10     490  
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i false(termination) 1 wit inspect 28   1300 220 unknown 0 wit inspect 3.4  210 false(termination) 1 wit inspect 13     520  
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i unknown 0 wit inspect 18   740 160 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .051 4.8
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i false(termination) 1 wit inspect 9.7 550 78 unknown 0 wit inspect 4.7  260 false(termination) 1 wit inspect 9.0   380  
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i false(termination) 1 wit inspect 9.3 530 83 unknown 0 wit inspect 4.7  260 false(termination) 1 wit inspect 8.8   360  
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i true 2 wit inspect 8.5 440 68 - wit inspect - wit inspect
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i unknown 0 wit inspect 280   1600 3500 - wit inspect - wit inspect
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i error (7) 0 wit inspect 26   970 230 - wit inspect - wit inspect
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i error (7) 0 wit inspect 45   1400 450 - wit inspect - wit inspect
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i true 2 wit inspect 7.3 370 63 - wit inspect - wit inspect
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i unknown 0 wit inspect 210   2600 2400 - wit inspect - wit inspect
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i unknown 0 wit inspect 42   1900 350 - wit inspect - wit inspect
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i unknown 0 wit inspect 43   2400 430 - wit inspect - wit inspect
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i unknown 0 wit inspect 480   4400 5900 - wit inspect - wit inspect
termination-15/add_first_alloca_true-termination.c.i true 2 wit inspect 7.4 380 54 - wit inspect - wit inspect
termination-15/array05_alloca_true-termination.c.i unknown 0 wit inspect 16   700 120 - wit inspect - wit inspect
termination-15/array06_alloca_true-termination.c.i true 2 wit inspect 10   560 86 - wit inspect - wit inspect
termination-15/array07_alloca_true-termination.c.i true 2 wit inspect 11   560 90 - wit inspect - wit inspect
termination-15/array08_alloca_true-termination.c.i unknown 0 wit inspect 20   790 160 - wit inspect - wit inspect
termination-15/array09_alloca_true-termination.c.i unknown 0 wit inspect 21   800 180 - wit inspect - wit inspect
termination-15/array10_alloca_true-termination.c.i unknown 0 wit inspect 16   730 120 - wit inspect - wit inspect
termination-15/array12_alloca_true-termination.c.i error (7) 0 wit inspect 130   1000 1800 - wit inspect - wit inspect
termination-15/array13_alloca_true-termination.c.i error (7) 0 wit inspect 360   1100 4100 - wit inspect - wit inspect
termination-15/array16_alloca_fixed_true-termination.c.i timeout 0 wit inspect 900   1800 12000 - wit inspect - wit inspect
termination-15/array17_alloca_true-termination.c.i timeout 0 wit inspect 900   2300 14000 - wit inspect - wit inspect
termination-15/array18_alloca_true-termination.c.i unknown 0 wit inspect 20   780 150 - wit inspect - wit inspect
termination-15/count_up_alloca_true-termination.c.i true 2 wit inspect 14   620 100 - wit inspect - wit inspect
termination-15/count_up_and_down_alloca_true-termination.c.i true 2 wit inspect 12   520 100 - wit inspect - wit inspect
termination-15/cstrcat_diffterm_alloca_true-termination.c.i true 2 wit inspect 12   550 95 - wit inspect - wit inspect
termination-15/cstrcat_malloc_true-termination.c.i true 2 wit inspect 14   600 140 - wit inspect - wit inspect
termination-15/cstrcat_mixed_alloca_true-termination.c.i true 2 wit inspect 12   580 96 - wit inspect - wit inspect
termination-15/cstrcat_reverse_alloca_true-termination.c.i true 2 wit inspect 12   570 100 - wit inspect - wit inspect
termination-15/cstrchr_diffterm_alloca_true-termination.c.i true 2 wit inspect 7.9 480 63 - wit inspect - wit inspect
termination-15/cstrchr_malloc_true-termination.c.i true 2 wit inspect 8.8 530 72 - wit inspect - wit inspect
termination-15/cstrchr_reverse_alloca_true-termination.c.i true 2 wit inspect 8.7 540 75 - wit inspect - wit inspect
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i true 2 wit inspect 9.0 550 82 - wit inspect - wit inspect
termination-15/cstrcmp_malloc_true-termination.c.i true 2 wit inspect 8.8 560 68 - wit inspect - wit inspect
termination-15/cstrcmp_mixed_alloca_true-termination.c.i true 2 wit inspect 8.9 550 69 - wit inspect - wit inspect
termination-15/cstrcmp_reverse_alloca_true-termination.c.i true 2 wit inspect 9.0 560 83 - wit inspect - wit inspect
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i true 2 wit inspect 9.1 520 75 - wit inspect - wit inspect
termination-15/cstrcpy_malloc_true-termination.c.i true 2 wit inspect 8.8 540 77 - wit inspect - wit inspect
termination-15/cstrcpy_mixed_alloca_true-termination.c.i true 2 wit inspect 9.1 520 82 - wit inspect - wit inspect
termination-15/cstrcpy_reverse_alloca_true-termination.c.i true 2 wit inspect 8.7 530 78 - wit inspect - wit inspect
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i true 2 wit inspect 200   740 2600 - wit inspect - wit inspect
termination-15/cstrcspn_malloc_true-termination.c.i true 2 wit inspect 110   760 1500 - wit inspect - wit inspect
termination-15/cstrcspn_mixed_alloca_true-termination.c.i true 2 wit inspect 21   750 180 - wit inspect - wit inspect
termination-15/cstrcspn_reverse_alloca_true-termination.c.i true 2 wit inspect 19   720 160 - wit inspect - wit inspect
termination-15/cstrlen_diffterm_alloca_true-termination.c.i true 2 wit inspect 7.2 360 59 - wit inspect - wit inspect
termination-15/cstrlen_malloc_true-termination.c.i true 2 wit inspect 7.6 370 69 - wit inspect - wit inspect
termination-15/cstrlen_reverse_alloca_true-termination.c.i true 2 wit inspect 7.9 370 61 - wit inspect - wit inspect
termination-15/cstrncat_diffterm_alloca_true-termination.c.i true 2 wit inspect 8.7 470 75 - wit inspect - wit inspect
termination-15/cstrncat_malloc_true-termination.c.i true 2 wit inspect 9.5 490 73 - wit inspect - wit inspect
termination-15/cstrncat_mixed_alloca_true-termination.c.i true 2 wit inspect 9.1 460 73 - wit inspect - wit inspect
termination-15/cstrncat_reverse_alloca_true-termination.c.i true 2 wit inspect 9.3 530 71 - wit inspect - wit inspect
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i true 2 wit inspect 8.7 520 80 - wit inspect - wit inspect
termination-15/cstrncmp_malloc_true-termination.c.i true 2 wit inspect 9.2 520 71 - wit inspect - wit inspect
termination-15/cstrncmp_mixed_alloca_true-termination.c.i true 2 wit inspect 9.1 530 72 - wit inspect - wit inspect
termination-15/cstrncmp_reverse_alloca_true-termination.c.i true 2 wit inspect 9.6 530 77 - wit inspect - wit inspect
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i true 2 wit inspect 12   590 120 - wit inspect - wit inspect
termination-15/cstrncpy_malloc_true-termination.c.i true 2 wit inspect 13   630 120 - wit inspect - wit inspect
termination-15/cstrncpy_mixed_alloca_true-termination.c.i true 2 wit inspect 12   570 110 - wit inspect - wit inspect
termination-15/cstrncpy_reverse_alloca_true-termination.c.i true 2 wit inspect 12   630 100 - wit inspect - wit inspect
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i true 2 wit inspect 17   670 180 - wit inspect - wit inspect
termination-15/cstrpbrk_malloc_true-termination.c.i true 2 wit inspect 17   680 150 - wit inspect - wit inspect
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i true 2 wit inspect 18   680 150 - wit inspect - wit inspect
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i true 2 wit inspect 17   700 140 - wit inspect - wit inspect
termination-15/cstrspn_diffterm_alloca_true-termination.c.i true 2 wit inspect 18   700 160 - wit inspect - wit inspect
termination-15/cstrspn_malloc_true-termination.c.i true 2 wit inspect 17   680 180 - wit inspect - wit inspect
termination-15/cstrspn_mixed_alloca_true-termination.c.i true 2 wit inspect 18   690 170 - wit inspect - wit inspect
termination-15/cstrspn_reverse_alloca_true-termination.c.i true 2 wit inspect 18   690 160 - wit inspect - wit inspect
termination-15/array04_alloca_false-termination.c.i false(termination) 1 wit inspect 7.8 350 69 unknown 0 wit inspect 4.6  280 false(termination) 1 wit inspect 6.7   270  
termination-15/array14_alloca_false-termination.c.i false(termination) 1 wit inspect 13   570 99 unknown 0 wit inspect 5.2  280 false(termination) 1 wit inspect 9.1   310  
termination-15/array15_alloca_false-termination.c.i false(termination) 1 wit inspect 13   550 100 unknown 0 wit inspect 5.2  280 false(termination) 1 wit inspect 8.6   300  
termination-15/array16_alloca_original_false-termination.c.i false(termination) 1 wit inspect 16   630 140 unknown 0 wit inspect 5.2  280 false(termination) 1 wit inspect 9.9   430  
termination-15/array19_alloca_false-termination.c.i false(termination) 1 wit inspect 7.9 360 73 unknown 0 wit inspect 4.7  270 false(termination) 1 wit inspect 7.3   270  
termination-15/array20_alloca_false-termination.c.i false(termination) 1 wit inspect 9.2 460 82 unknown 0 wit inspect 4.7  280 false(termination) 1 wit inspect 8.3   310  
termination-recursive-malloc/chunk1_true-termination.c.i true 2 wit inspect 7.6 370 64 - wit inspect - wit inspect
termination-recursive-malloc/chunk2_true-termination.c.i error (7) 0 wit inspect 120   1600 1600 - wit inspect - wit inspect
termination-recursive-malloc/chunk3_true-termination.c.i error (7) 0 wit inspect 190   1600 2200 - wit inspect - wit inspect
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i true 2 wit inspect 24   780 210 - wit inspect - wit inspect
termination-recursive-malloc/mergeSort_true-termination.c.i error (7) 0 wit inspect 49   1300 510 - wit inspect - wit inspect
termination-recursive-malloc/mutual_simple2_true-termination.c.i true 2 wit inspect 10   510 91 - wit inspect - wit inspect
termination-recursive-malloc/mutual_simple_true-termination.c.i true 2 wit inspect 7.6 370 70 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i true 2 wit inspect 12   560 120 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i true 2 wit inspect 25   750 280 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i true 2 wit inspect 20   690 200 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i true 2 wit inspect 21   760 210 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i true 2 wit inspect 71   3500 670 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i error (7) 0 wit inspect 37   930 440 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i true 2 wit inspect 36   830 350 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i true 2 wit inspect 21   770 200 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i true 2 wit inspect 13   580 130 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i timeout 0 wit inspect 900   8500 10000 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i true 2 wit inspect 29   920 260 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i unknown 0 wit inspect 31   1100 280 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i true 2 wit inspect 13   550 120 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i unknown 0 wit inspect 55   3200 510 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i unknown 0 wit inspect 96   5600 1000 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i timeout 0 wit inspect 900   1500 12000 - wit inspect - wit inspect
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i true 2 wit inspect 11   540 95 - wit inspect - wit inspect
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i true 2 wit inspect 7.8 430 65 - wit inspect - wit inspect
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i true 2 wit inspect 6.8 370 56 - wit inspect - wit inspect
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i true 2 wit inspect 16   630 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 409 21000 270000 230000 17 0 67 3900 17 15 130 5400
    correct results 212 409 4600 140000 47000 0 15 15 130 5300
        correct true 197 394 4400 130000 46000 0 0
        correct false 15 15 170 8100 1400 0 15 15 130 5300
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (260 tasks, max score: 503) 409 0 15
Run set uautomizer.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Termination-MainHeap