Tool 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-01 12:27:04 CET 2017-12-01 18:45:24 CET 2017-12-01 18:50:14 CET
Run set cpa-seq.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Termination-MainHeap
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-12-01_1227.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/cpa-seq.2017-12-01_1227.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 unknown 0 wit inspect 62   3700 590 - wit inspect - wit inspect
termination-libowfat/atol_true-termination.c.i unknown 0 wit inspect 45   2000 340 - wit inspect - wit inspect
termination-libowfat/atoll_true-termination.c.i unknown 0 wit inspect 100   3800 1100 - wit inspect - wit inspect
termination-libowfat/basename_true-termination.c.i unknown 0 wit inspect 47   2000 550 - wit inspect - wit inspect
termination-libowfat/build_fullname_true-termination.c.i timeout 0 wit inspect 910   4200 12000 - wit inspect - wit inspect
termination-libowfat/dirname_true-termination.c.i timeout 0 wit inspect 900   4500 12000 - wit inspect - wit inspect
termination-libowfat/skip_to_true-termination.c.i unknown 0 wit inspect 8.1 490 67 - wit inspect - wit inspect
termination-libowfat/stpcpy_true-termination.c.i exception 0 wit inspect 110   3900 1300 - wit inspect - wit inspect
termination-libowfat/strcasecmp_true-termination.c.i timeout 0 wit inspect 900   2800 11000 - wit inspect - wit inspect
termination-libowfat/strcat_short_true-termination.c.i timeout 0 wit inspect 900   4300 11000 - wit inspect - wit inspect
termination-libowfat/strcat_true-termination.c.i timeout 0 wit inspect 900   4300 11000 - wit inspect - wit inspect
termination-libowfat/strchr_short_true-termination.c.i unknown 0 wit inspect 8.9 500 67 - wit inspect - wit inspect
termination-libowfat/strchr_true-termination.c.i unknown 0 wit inspect 850   4200 10000 - wit inspect - wit inspect
termination-libowfat/strcmp_short_true-termination.c.i timeout 0 wit inspect 900   3100 14000 - wit inspect - wit inspect
termination-libowfat/strcpy_small_true-termination.c.i exception 0 wit inspect 600   4000 8000 - wit inspect - wit inspect
termination-libowfat/strcspn_true-termination.c.i true 2 wit inspect 350   2200 4900 - wit inspect - wit inspect
termination-libowfat/strdup_true-termination.c.i unknown 0 wit inspect 16   650 120 - wit inspect - wit inspect
termination-libowfat/strlcat_true-termination.c.i error (parsing failed) 0 wit inspect 1.6 130 15 - wit inspect - wit inspect
termination-libowfat/strlcpy_true-termination.c.i error (parsing failed) 0 wit inspect 1.5 140 16 - wit inspect - wit inspect
termination-libowfat/strlen_true-termination.c.i unknown 0 wit inspect 7.9 500 63 - wit inspect - wit inspect
termination-libowfat/strpbrk_true-termination.c.i true 2 wit inspect 330   2200 3900 - wit inspect - wit inspect
termination-libowfat/strrchr_short_true-termination.c.i unknown 0 wit inspect 6.2 460 51 - wit inspect - wit inspect
termination-libowfat/strrchr_true-termination.c.i timeout 0 wit inspect 900   5100 10000 - wit inspect - wit inspect
termination-libowfat/strspn_true-termination.c.i timeout 0 wit inspect 900   3900 14000 - wit inspect - wit inspect
termination-libowfat/strstr_true-termination.c.i timeout 0 wit inspect 900   3800 13000 - wit inspect - wit inspect
termination-libowfat/strtok_r_true-termination.c.i exception 0 wit inspect 680   4900 8300 - wit inspect - wit inspect
termination-libowfat/strtol_true-termination.c.i unknown 0 wit inspect 810   4300 11000 - wit inspect - wit inspect
termination-libowfat/strtoul_true-termination.c.i unknown 0 wit inspect 580   4200 8100 - wit inspect - wit inspect
termination-libowfat/strtoull_true-termination.c.i timeout 0 wit inspect 900   4200 11000 - wit inspect - wit inspect
termination-libowfat/wcsrchr_true-termination.c.i unknown 0 wit inspect 6.6 480 58 - wit inspect - wit inspect
termination-libowfat/wcsstr_true-termination.c.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i unknown 0 wit inspect 4.7 320 37 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .019 4.8
termination-memory-alloca/Velroyen-alloca_false-termination.c.i unknown 0 wit inspect 5.4 330 49 error (invalid witness file) 0 wit inspect .81 41 error (2) 0 wit inspect .019 4.8
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i timeout 0 wit inspect 910   4300 14000 - wit inspect - wit inspect
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i timeout 0 wit inspect 900   4200 13000 - wit inspect - wit inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i true 2 wit inspect 330   3800 4500 - wit inspect - wit inspect
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i timeout 0 wit inspect 900   4100 13000 - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i true 2 wit inspect 270   4200 3300 - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i timeout 0 wit inspect 910   4200 14000 - wit inspect - wit inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i timeout 0 wit inspect 910   4100 12000 - wit inspect - wit inspect
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i timeout 0 wit inspect 900   4400 12000 - wit inspect - wit inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i timeout 0 wit inspect 910   4500 11000 - wit inspect - wit inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i true 2 wit inspect 6.2 360 56 - wit inspect - wit inspect
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i timeout 0 wit inspect 910   4200 12000 - wit inspect - wit inspect
termination-memory-alloca/Masse-alloca_true-termination.c.i unknown 0 wit inspect 5.1 320 47 - wit inspect - wit inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i timeout 0 wit inspect 910   4400 12000 - wit inspect - wit inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i timeout 0 wit inspect 910   4500 14000 - wit inspect - wit inspect
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i true 2 wit inspect 100   3700 1000 - wit inspect - wit inspect
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i timeout 0 wit inspect 900   4200 11000 - wit inspect - wit inspect
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i timeout 0 wit inspect 910   4400 13000 - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i unknown 0 wit inspect 640   4100 9100 - wit inspect - wit inspect
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i out of memory 0 wit inspect 530   15000 7800 - wit inspect - wit inspect
termination-memory-alloca/Urban-alloca_true-termination.c.i true 2 wit inspect 120   4000 1300 - wit inspect - wit inspect
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4100 10000 - wit inspect - wit inspect
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4100 13000 - wit inspect - wit inspect
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4200 11000 - wit inspect - wit inspect
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 920   4300 11000 - wit inspect - wit inspect
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 910   4400 13000 - wit inspect - wit inspect
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 910   4300 15000 - wit inspect - wit inspect
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4100 13000 - wit inspect - wit inspect
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect
termination-memory-alloca/add_last-alloca_true-termination.c.i timeout 0 wit inspect 900   3900 12000 - wit inspect - wit inspect
termination-memory-alloca/array01-alloca_true-termination.c.i unknown 0 wit inspect 29   970 220 - wit inspect - wit inspect
termination-memory-alloca/array02-alloca_true-termination.c.i unknown 0 wit inspect 26   890 190 - wit inspect - wit inspect
termination-memory-alloca/array03-alloca_true-termination.c.i true 2 wit inspect 3.9 290 35 - wit inspect - wit inspect
termination-memory-alloca/aviad_true-alloca_true-termination.c.i timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4100 11000 - wit inspect - wit inspect
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4100 11000 - wit inspect - wit inspect
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i unknown 0 wit inspect 43   2700 400 - wit inspect - wit inspect
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i unknown 0 wit inspect 41   2700 370 - wit inspect - wit inspect
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   3200 13000 - wit inspect - wit inspect
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4100 13000 - wit inspect - wit inspect
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4100 14000 - wit inspect - wit inspect
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4100 11000 - wit inspect - wit inspect
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 910   4200 13000 - wit inspect - wit inspect
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4100 14000 - wit inspect - wit inspect
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 910   4400 12000 - wit inspect - wit inspect
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4000 13000 - wit inspect - wit inspect
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 910   4200 14000 - wit inspect - wit inspect
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i true 2 wit inspect 430   4600 6100 - wit inspect - wit inspect
termination-memory-alloca/bubblesort-alloca_true-termination.c.i true 2 wit inspect 6.5 380 53 - wit inspect - wit inspect
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 910   4400 13000 - wit inspect - wit inspect
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4500 13000 - wit inspect - wit inspect
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 910   4200 12000 - wit inspect - wit inspect
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 910   4400 12000 - wit inspect - wit inspect
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 910   4500 12000 - wit inspect - wit inspect
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect
termination-memory-alloca/count_down-alloca_true-termination.c.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect
termination-memory-alloca/cstrcat-alloca_true-termination.c.i timeout 0 wit inspect 900   4000 12000 - wit inspect - wit inspect
termination-memory-alloca/cstrchr-alloca_true-termination.c.i unknown 0 wit inspect 19   690 150 - wit inspect - wit inspect
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i timeout 0 wit inspect 900   3100 11000 - wit inspect - wit inspect
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i timeout 0 wit inspect 900   4500 12000 - wit inspect - wit inspect
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i timeout 0 wit inspect 900   3700 12000 - wit inspect - wit inspect
termination-memory-alloca/cstrlen-alloca_true-termination.c.i unknown 0 wit inspect 25   1000 190 - wit inspect - wit inspect
termination-memory-alloca/cstrncat-alloca_true-termination.c.i timeout 0 wit inspect 900   4200 14000 - wit inspect - wit inspect
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i timeout 0 wit inspect 900   3300 12000 - wit inspect - wit inspect
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i true 2 wit inspect 620   4700 7000 - wit inspect - wit inspect
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i timeout 0 wit inspect 900   3700 12000 - wit inspect - wit inspect
termination-memory-alloca/cstrspn-alloca_true-termination.c.i timeout 0 wit inspect 900   3700 13000 - wit inspect - wit inspect
termination-memory-alloca/diff-alloca_true-termination.c.i true 2 wit inspect 18   990 150 - wit inspect - wit inspect
termination-memory-alloca/easySum-alloca_true-termination.c.i timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect
termination-memory-alloca/ex1-alloca_true-termination.c.i timeout 0 wit inspect 900   4100 9400 - wit inspect - wit inspect
termination-memory-alloca/ex2-alloca_true-termination.c.i timeout 0 wit inspect 900   4200 14000 - wit inspect - wit inspect
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect
termination-memory-alloca/ex3b-alloca_true-termination.c.i timeout 0 wit inspect 910   4300 13000 - wit inspect - wit inspect
termination-memory-alloca/fermat-alloca_true-termination.c.i timeout 0 wit inspect 910   4300 13000 - wit inspect - wit inspect
termination-memory-alloca/flag-alloca_true-termination.c.i timeout 0 wit inspect 920   4500 11000 - wit inspect - wit inspect
termination-memory-alloca/gcd1-alloca_true-termination.c.i timeout 0 wit inspect 910   4300 13000 - wit inspect - wit inspect
termination-memory-alloca/genady-alloca_true-termination.c.i timeout 0 wit inspect 900   3100 11000 - wit inspect - wit inspect
termination-memory-alloca/insertionsort-alloca_true-termination.c.i true 2 wit inspect 15   630 120 - wit inspect - wit inspect
termination-memory-alloca/java_AG313-alloca_true-termination.c.i timeout 0 wit inspect 900   4300 14000 - wit inspect - wit inspect
termination-memory-alloca/java_Break-alloca_true-termination.c.i timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i true 2 wit inspect 7.7 460 61 - wit inspect - wit inspect
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i true 2 wit inspect 330   4500 3600 - wit inspect - wit inspect
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i timeout 0 wit inspect 900   3900 13000 - wit inspect - wit inspect
termination-memory-alloca/java_Nested-alloca_true-termination.c.i timeout 0 wit inspect 900   4100 11000 - wit inspect - wit inspect
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i timeout 0 wit inspect 900   4100 15000 - wit inspect - wit inspect
termination-memory-alloca/lis-alloca_true-termination.c.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect
termination-memory-alloca/min_rf-alloca_true-termination.c.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect
termination-memory-alloca/mult_array-alloca_true-termination.c.i timeout 0 wit inspect 920   4500 10000 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i true 2 wit inspect 6.5 410 47 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i true 2 wit inspect 6.4 430 48 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i true 2 wit inspect 6.1 380 50 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i true 2 wit inspect 5.1 300 37 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i unknown 0 wit inspect 310   4400 3800 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i true 2 wit inspect 810   4300 10000 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i unknown 0 wit inspect 720   4200 11000 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i unknown 0 wit inspect 400   4600 5200 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i true 2 wit inspect 870   2200 12000 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i timeout 0 wit inspect 900   3900 12000 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i unknown 0 wit inspect 7.0 470 59 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i timeout 0 wit inspect 900   4200 11000 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i unknown 0 wit inspect 510   4100 7000 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i timeout 0 wit inspect 900   4400 12000 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i true 2 wit inspect 7.9 470 59 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i true 2 wit inspect 810   2200 11000 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i timeout 0 wit inspect 900   3300 12000 - wit inspect - wit inspect
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i error (recursion) 0 wit inspect 3.3 280 30 - wit inspect - wit inspect
termination-memory-alloca/selectionsort-alloca_true-termination.c.i out of memory 0 wit inspect 300   15000 4200 - wit inspect - wit inspect
termination-memory-alloca/stroeder1-alloca_true-termination.c.i true 2 wit inspect 5.6 340 45 - wit inspect - wit inspect
termination-memory-alloca/stroeder2-alloca_true-termination.c.i true 2 wit inspect 6.5 390 57 - wit inspect - wit inspect
termination-memory-alloca/strreplace-alloca_true-termination.c.i unknown 0 wit inspect 26   1100 230 - wit inspect - wit inspect
termination-memory-alloca/subseq-alloca_true-termination.c.i timeout 0 wit inspect 900   2900 12000 - wit inspect - wit inspect
termination-memory-alloca/substring-alloca_true-termination.c.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect
termination-memory-alloca/twisted-alloca_true-termination.c.i timeout 0 wit inspect 910   4400 13000 - wit inspect - wit inspect
termination-memory-linkedlists/cll_by_lseg-alloca_false-termination.c.i error (recursion) 0 wit inspect 3.5 300 31 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.8
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i error (recursion) 0 wit inspect 3.4 310 29 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i false(termination) 1 wit inspect 7.8 460 69 unknown 0 wit inspect 4.4  270 false(termination) 1 wit inspect 8.9   360  
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i unknown 0 wit inspect 61   3600 510 error (invalid witness file) 0 wit inspect .71 45 error (2) 0 wit inspect .018 4.8
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i error (recursion) 0 wit inspect 3.2 280 29 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 4.8
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i error (recursion) 0 wit inspect 3.5 300 33 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i error (recursion) 0 wit inspect 3.5 300 28 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i unknown 0 wit inspect 62   3200 510 error (invalid witness file) 0 wit inspect .52 46 error (2) 0 wit inspect .019 4.8
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i unknown 0 wit inspect 50   3700 420 error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .049 4.8
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i error (recursion) 0 wit inspect 3.5 310 27 - wit inspect - wit inspect
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i timeout 0 wit inspect 900   3700 11000 - wit inspect - wit inspect
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i error (recursion) 0 wit inspect 3.4 300 28 - wit inspect - wit inspect
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i error (recursion) 0 wit inspect 3.4 300 32 - wit inspect - wit inspect
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i error (recursion) 0 wit inspect 3.5 300 31 - wit inspect - wit inspect
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i timeout 0 wit inspect 900   3800 12000 - wit inspect - wit inspect
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i unknown 0 wit inspect 13   600 100 - wit inspect - wit inspect
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i unknown 0 wit inspect 8.2 480 62 - wit inspect - wit inspect
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i timeout 0 wit inspect 900   3900 15000 - wit inspect - wit inspect
termination-15/add_first_alloca_true-termination.c.i true 2 wit inspect 10   480 85 - wit inspect - wit inspect
termination-15/array05_alloca_true-termination.c.i true 2 wit inspect 6.4 340 58 - wit inspect - wit inspect
termination-15/array06_alloca_true-termination.c.i true 2 wit inspect 6.3 340 48 - wit inspect - wit inspect
termination-15/array07_alloca_true-termination.c.i true 2 wit inspect 6.9 330 60 - wit inspect - wit inspect
termination-15/array08_alloca_true-termination.c.i timeout 0 wit inspect 900   4500 10000 - wit inspect - wit inspect
termination-15/array09_alloca_true-termination.c.i timeout 0 wit inspect 900   4500 13000 - wit inspect - wit inspect
termination-15/array10_alloca_true-termination.c.i true 2 wit inspect 6.4 330 60 - wit inspect - wit inspect
termination-15/array12_alloca_true-termination.c.i timeout 0 wit inspect 900   4400 11000 - wit inspect - wit inspect
termination-15/array13_alloca_true-termination.c.i timeout 0 wit inspect 900   4200 14000 - wit inspect - wit inspect
termination-15/array16_alloca_fixed_true-termination.c.i timeout 0 wit inspect 900   5400 11000 - wit inspect - wit inspect
termination-15/array17_alloca_true-termination.c.i error 0 wit inspect 10   490 80 - wit inspect - wit inspect
termination-15/array18_alloca_true-termination.c.i timeout 0 wit inspect 900   4400 14000 - wit inspect - wit inspect
termination-15/count_up_alloca_true-termination.c.i unknown 0 wit inspect 20   780 160 - wit inspect - wit inspect
termination-15/count_up_and_down_alloca_true-termination.c.i unknown 0 wit inspect 16   630 130 - wit inspect - wit inspect
termination-15/cstrcat_diffterm_alloca_true-termination.c.i timeout 0 wit inspect 900   4000 14000 - wit inspect - wit inspect
termination-15/cstrcat_malloc_true-termination.c.i timeout 0 wit inspect 900   4000 10000 - wit inspect - wit inspect
termination-15/cstrcat_mixed_alloca_true-termination.c.i timeout 0 wit inspect 900   4000 12000 - wit inspect - wit inspect
termination-15/cstrcat_reverse_alloca_true-termination.c.i timeout 0 wit inspect 900   4900 11000 - wit inspect - wit inspect
termination-15/cstrchr_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 29   1000 230 - wit inspect - wit inspect
termination-15/cstrchr_malloc_true-termination.c.i unknown 0 wit inspect 18   700 150 - wit inspect - wit inspect
termination-15/cstrchr_reverse_alloca_true-termination.c.i unknown 0 wit inspect 16   680 130 - wit inspect - wit inspect
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i timeout 0 wit inspect 900   3000 11000 - wit inspect - wit inspect
termination-15/cstrcmp_malloc_true-termination.c.i timeout 0 wit inspect 900   3400 12000 - wit inspect - wit inspect
termination-15/cstrcmp_mixed_alloca_true-termination.c.i timeout 0 wit inspect 900   3400 13000 - wit inspect - wit inspect
termination-15/cstrcmp_reverse_alloca_true-termination.c.i timeout 0 wit inspect 900   4000 11000 - wit inspect - wit inspect
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i timeout 0 wit inspect 900   4400 12000 - wit inspect - wit inspect
termination-15/cstrcpy_malloc_true-termination.c.i timeout 0 wit inspect 900   4400 11000 - wit inspect - wit inspect
termination-15/cstrcpy_mixed_alloca_true-termination.c.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect
termination-15/cstrcpy_reverse_alloca_true-termination.c.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i timeout 0 wit inspect 900   3700 13000 - wit inspect - wit inspect
termination-15/cstrcspn_malloc_true-termination.c.i timeout 0 wit inspect 900   3700 13000 - wit inspect - wit inspect
termination-15/cstrcspn_mixed_alloca_true-termination.c.i exception 0 wit inspect 520   3700 6600 - wit inspect - wit inspect
termination-15/cstrcspn_reverse_alloca_true-termination.c.i timeout 0 wit inspect 900   3700 12000 - wit inspect - wit inspect
termination-15/cstrlen_diffterm_alloca_true-termination.c.i unknown 0 wit inspect 25   940 200 - wit inspect - wit inspect
termination-15/cstrlen_malloc_true-termination.c.i unknown 0 wit inspect 27   970 200 - wit inspect - wit inspect
termination-15/cstrlen_reverse_alloca_true-termination.c.i unknown 0 wit inspect 28   980 240 - wit inspect - wit inspect
termination-15/cstrncat_diffterm_alloca_true-termination.c.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect
termination-15/cstrncat_malloc_true-termination.c.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect
termination-15/cstrncat_mixed_alloca_true-termination.c.i timeout 0 wit inspect 900   4000 12000 - wit inspect - wit inspect
termination-15/cstrncat_reverse_alloca_true-termination.c.i timeout 0 wit inspect 900   4400 11000 - wit inspect - wit inspect
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i timeout 0 wit inspect 900   2900 11000 - wit inspect - wit inspect
termination-15/cstrncmp_malloc_true-termination.c.i timeout 0 wit inspect 900   3200 11000 - wit inspect - wit inspect
termination-15/cstrncmp_mixed_alloca_true-termination.c.i timeout 0 wit inspect 900   3400 12000 - wit inspect - wit inspect
termination-15/cstrncmp_reverse_alloca_true-termination.c.i timeout 0 wit inspect 900   3300 12000 - wit inspect - wit inspect
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i true 2 wit inspect 730   4300 9100 - wit inspect - wit inspect
termination-15/cstrncpy_malloc_true-termination.c.i true 2 wit inspect 640   4600 7900 - wit inspect - wit inspect
termination-15/cstrncpy_mixed_alloca_true-termination.c.i timeout 0 wit inspect 900   4300 13000 - wit inspect - wit inspect
termination-15/cstrncpy_reverse_alloca_true-termination.c.i timeout 0 wit inspect 900   4500 12000 - wit inspect - wit inspect
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i timeout 0 wit inspect 900   3700 12000 - wit inspect - wit inspect
termination-15/cstrpbrk_malloc_true-termination.c.i timeout 0 wit inspect 900   3700 11000 - wit inspect - wit inspect
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i timeout 0 wit inspect 900   3700 13000 - wit inspect - wit inspect
termination-15/cstrspn_diffterm_alloca_true-termination.c.i timeout 0 wit inspect 900   3700 11000 - wit inspect - wit inspect
termination-15/cstrspn_malloc_true-termination.c.i timeout 0 wit inspect 900   3200 14000 - wit inspect - wit inspect
termination-15/cstrspn_mixed_alloca_true-termination.c.i timeout 0 wit inspect 900   4100 13000 - wit inspect - wit inspect
termination-15/cstrspn_reverse_alloca_true-termination.c.i timeout 0 wit inspect 900   3700 12000 - wit inspect - wit inspect
termination-15/array04_alloca_false-termination.c.i false(termination) 1 wit inspect 6.4 340 53 false(termination) 1 wit inspect 4.3  260 false(termination) 1 wit inspect 7.4   280  
termination-15/array14_alloca_false-termination.c.i timeout 0 wit inspect 900   4200 11000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .024 4.8
termination-15/array15_alloca_false-termination.c.i timeout 0 wit inspect 900   4200 14000 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .021 4.9
termination-15/array16_alloca_original_false-termination.c.i timeout 0 wit inspect 900   5000 10000 error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .019 4.9
termination-15/array19_alloca_false-termination.c.i false(termination) 1 wit inspect 7.1 350 63 false(termination) 1 wit inspect 4.4  260 false(termination) 1 wit inspect 9.6   290  
termination-15/array20_alloca_false-termination.c.i unknown 0 wit inspect 40   2000 310 error (invalid witness file) 0 wit inspect .49 45 error (2) 0 wit inspect .019 4.9
termination-recursive-malloc/chunk1_true-termination.c.i error (recursion) 0 wit inspect 2.9 290 26 - wit inspect - wit inspect
termination-recursive-malloc/chunk2_true-termination.c.i error (recursion) 0 wit inspect 2.9 290 25 - wit inspect - wit inspect
termination-recursive-malloc/chunk3_true-termination.c.i error (recursion) 0 wit inspect 2.9 290 28 - wit inspect - wit inspect
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i error (recursion) 0 wit inspect 2.9 290 27 - wit inspect - wit inspect
termination-recursive-malloc/mergeSort_true-termination.c.i error (recursion) 0 wit inspect 2.8 270 25 - wit inspect - wit inspect
termination-recursive-malloc/mutual_simple2_true-termination.c.i error (recursion) 0 wit inspect 2.6 270 23 - wit inspect - wit inspect
termination-recursive-malloc/mutual_simple_true-termination.c.i error (recursion) 0 wit inspect 2.8 290 22 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i error (recursion) 0 wit inspect 2.8 290 23 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i error (recursion) 0 wit inspect 2.6 270 25 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i error (recursion) 0 wit inspect 2.7 270 25 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i error (recursion) 0 wit inspect 3.0 290 22 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i error (recursion) 0 wit inspect 2.7 270 22 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i error (recursion) 0 wit inspect 2.8 310 24 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i error (recursion) 0 wit inspect 2.9 290 26 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i error (recursion) 0 wit inspect 2.6 270 22 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i error (recursion) 0 wit inspect 3.0 290 23 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i error (recursion) 0 wit inspect 3.0 300 24 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i error (recursion) 0 wit inspect 2.8 270 24 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i error (recursion) 0 wit inspect 2.6 260 22 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i error (recursion) 0 wit inspect 2.8 290 24 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i error (recursion) 0 wit inspect 2.9 290 23 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i error (recursion) 0 wit inspect 2.8 290 22 - wit inspect - wit inspect
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i error (recursion) 0 wit inspect 2.9 290 25 - wit inspect - wit inspect
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i error (recursion) 0 wit inspect 2.8 300 25 - wit inspect - wit inspect
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i error (recursion) 0 wit inspect 2.9 290 24 - wit inspect - wit inspect
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i error (recursion) 0 wit inspect 2.6 260 26 - wit inspect - wit inspect
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i error (recursion) 0 wit inspect 2.9 290 23 - 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 67 140000 750000 1800000 17 2 21   1400 17 3 26 1000
    correct results 35 67 6900 60000 87000 2 2 8.7 520 3 3 26 940
        correct true 32 64 6900 59000 87000 0 0
        correct false 3 3 21 1100 180 2 2 8.7 520 3 3 26 940
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (260 tasks, max score: 503) 67 2 3
Run set cpa-seq.sv-comp18.Termination-MainHeap cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Termination-MainHeap uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Termination-MainHeap