Tool PeSCo 1.7-svn b8d6131600+ CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon004; apollon069; apollon137; apollon154] [apollon004; apollon006; apollon021; apollon061; apollon109; apollon155]
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 12:44:04 CET 2018-12-08 07:39:30 CET 2018-12-08 12:16:42 CET
Run set pesco.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-termination.Termination-MainHeap
Options -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
termination-libowfat/atoi_true-termination.c.i unknown 0 --- inspect 110   81    3700 1300 0   0   - --- inspect - --- inspect
termination-libowfat/atol_true-termination.c.i unknown 0 --- inspect 48   25    3200 540 0   0   - --- inspect - --- inspect
termination-libowfat/atoll_true-termination.c.i unknown 0 --- inspect 86   57    3800 890 0   0   - --- inspect - --- inspect
termination-libowfat/basename_true-termination.c.i unknown 0 --- inspect 67   48    2200 760 0   0   - --- inspect - --- inspect
termination-libowfat/build_fullname_true-termination.c.i timeout 0 --- inspect 900   870    3900 11000 0   0   - --- inspect - --- inspect
termination-libowfat/dirname_true-termination.c.i timeout 0 --- inspect 900   830    4200 12000 0   0   - --- inspect - --- inspect
termination-libowfat/skip_to_true-termination.c.i unknown 0 --- inspect 9.8 3.0  430 90 0   0   - --- inspect - --- inspect
termination-libowfat/stpcpy_true-termination.c.i timeout 0 --- inspect 900   820    4200 13000 0   0   - --- inspect - --- inspect
termination-libowfat/strcasecmp_true-termination.c.i timeout 0 --- inspect 900   850    4200 13000 0   0   - --- inspect - --- inspect
termination-libowfat/strcat_short_true-termination.c.i timeout 0 --- inspect 900   830    4300 12000 0   0   - --- inspect - --- inspect
termination-libowfat/strcat_true-termination.c.i timeout 0 --- inspect 910   840    4300 13000 0   0   - --- inspect - --- inspect
termination-libowfat/strchr_short_true-termination.c.i unknown 0 --- inspect 9.9 3.0  530 89 0   0   - --- inspect - --- inspect
termination-libowfat/strchr_true-termination.c.i timeout 0 --- inspect 900   840    4100 11000 0   0   - --- inspect - --- inspect
termination-libowfat/strcmp_short_true-termination.c.i timeout 0 --- inspect 900   860    3300 12000 0   0   - --- inspect - --- inspect
termination-libowfat/strcpy_small_true-termination.c.i timeout 0 --- inspect 900   820    4100 13000 0   0   - --- inspect - --- inspect
termination-libowfat/strcspn_true-termination.c.i true 2 --- inspect 570   540    2400 7400 0   0   - --- inspect - --- inspect
termination-libowfat/strdup_true-termination.c.i timeout 0 --- inspect 920   850    4300 12000 0   0   - --- inspect - --- inspect
termination-libowfat/strlcat_true-termination.c.i error (parsing failed) 0 --- inspect 1.9 .83 160 16 0   0   - --- inspect - --- inspect
termination-libowfat/strlcpy_true-termination.c.i error (parsing failed) 0 --- inspect 1.9 .81 160 18 0   0   - --- inspect - --- inspect
termination-libowfat/strlen_true-termination.c.i unknown 0 --- inspect 8.8 2.7  500 78 0   0   - --- inspect - --- inspect
termination-libowfat/strpbrk_true-termination.c.i true 2 --- inspect 540   500    2000 7700 0   0   - --- inspect - --- inspect
termination-libowfat/strrchr_short_true-termination.c.i unknown 0 --- inspect 7.8 2.6  470 78 0   0   - --- inspect - --- inspect
termination-libowfat/strrchr_true-termination.c.i timeout 0 --- inspect 900   850    4000 10000 0   0   - --- inspect - --- inspect
termination-libowfat/strspn_true-termination.c.i timeout 0 --- inspect 900   860    3900 12000 0   0   - --- inspect - --- inspect
termination-libowfat/strstr_true-termination.c.i timeout 0 --- inspect 900   850    3700 14000 0   0   - --- inspect - --- inspect
termination-libowfat/strtok_r_true-termination.c.i timeout 0 --- inspect 900   810    4200 11000 0   0   - --- inspect - --- inspect
termination-libowfat/strtol_true-termination.c.i exception 0 --- inspect 26   6.9  1300 230 0   0   - --- inspect - --- inspect
termination-libowfat/strtoul_true-termination.c.i exception 0 --- inspect 7.9 2.6  460 67 0   0   - --- inspect - --- inspect
termination-libowfat/strtoull_true-termination.c.i exception 0 --- inspect 8.1 2.7  470 66 0   0   - --- inspect - --- inspect
termination-libowfat/wcsrchr_true-termination.c.i unknown 0 --- inspect 8.0 2.6  360 69 0   0   - --- inspect - --- inspect
termination-libowfat/wcsstr_true-termination.c.i timeout 0 --- inspect 900   830    4100 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i unknown 0 --- inspect 5.4 2.0  300 46 0   0   error (invalid witness file) 0 --- inspect .63 .38 42 0     0   error (2) 0 --- inspect .023 .023 5.6 0    0  
termination-memory-alloca/Velroyen-alloca_false-termination.c.i unknown 0 --- inspect 6.6 2.2  370 54 0   0   error (invalid witness file) 0 --- inspect .60 .37 41 0     0   error (2) 0 --- inspect .020 .022 5.6 0    0  
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i timeout 0 --- inspect 900   860    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4000 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 900   830    4200 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i true 2 --- inspect 410   360    4100 5900 0   0   - --- inspect - --- inspect
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i true 2 --- inspect 570   510    4300 6800 0   0   - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i timeout 0 --- inspect 910   840    4200 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4100 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 910   840    4300 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 910   870    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i true 2 --- inspect 6.6 2.2  380 53 0   0   - --- inspect - --- inspect
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 900   860    4000 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Masse-alloca_true-termination.c.i unknown 0 --- inspect 6.3 2.2  400 57 0   0   - --- inspect - --- inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i timeout 0 --- inspect 900   860    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i timeout 0 --- inspect 910   870    4200 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i true 2 --- inspect 160   120    3400 2100 0   0   - --- inspect - --- inspect
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i timeout 0 --- inspect 900   860    4100 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i timeout 0 --- inspect 900   870    4000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i out of memory 0 --- inspect 580   540    15000 6500 0   0   - --- inspect - --- inspect
termination-memory-alloca/Urban-alloca_true-termination.c.i true 2 --- inspect 160   120    4000 1800 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 920   860    4300 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4100 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4100 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/add_last-alloca_true-termination.c.i timeout 0 --- inspect 900   890    710 10000 0   0   - --- inspect - --- inspect
termination-memory-alloca/array01-alloca_true-termination.c.i unknown 0 --- inspect 9.0 2.8  470 72 0   0   - --- inspect - --- inspect
termination-memory-alloca/array02-alloca_true-termination.c.i unknown 0 --- inspect 27   7.4  1000 240 0   0   - --- inspect - --- inspect
termination-memory-alloca/array03-alloca_true-termination.c.i true 2 --- inspect 4.3 1.8  270 41 0   0   - --- inspect - --- inspect
termination-memory-alloca/aviad_true-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   840    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i unknown 0 --- inspect 57   23    3500 580 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i unknown 0 --- inspect 51   23    3700 490 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    3900 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 920   860    4300 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   860    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   870    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 920   860    4200 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   860    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4000 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 910   870    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 920   840    4500 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 510   440    4700 7700 0   0   - --- inspect - --- inspect
termination-memory-alloca/bubblesort-alloca_true-termination.c.i true 2 --- inspect 7.7 2.6  460 73 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   830    4200 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    3900 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   860    4000 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/count_down-alloca_true-termination.c.i unknown 0 --- inspect 19   5.9  820 170 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrcat-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrchr-alloca_true-termination.c.i unknown 0 --- inspect 31   8.9  1400 260 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i timeout 0 --- inspect 900   860    3200 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4200 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i timeout 0 --- inspect 900   850    3700 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrlen-alloca_true-termination.c.i unknown 0 --- inspect 20   5.8  800 190 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrncat-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4300 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i timeout 0 --- inspect 900   860    2900 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i true 2 --- inspect 860   770    4500 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i timeout 0 --- inspect 900   850    3700 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/cstrspn-alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/diff-alloca_true-termination.c.i true 2 --- inspect 16   5.1  660 130 0   0   - --- inspect - --- inspect
termination-memory-alloca/easySum-alloca_true-termination.c.i timeout 0 --- inspect 920   860    4200 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/ex1-alloca_true-termination.c.i exception 0 --- inspect 4.2 1.6  290 37 0   0   - --- inspect - --- inspect
termination-memory-alloca/ex2-alloca_true-termination.c.i timeout 0 --- inspect 910   870    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i exception 0 --- inspect 3.9 1.6  290 35 0   0   - --- inspect - --- inspect
termination-memory-alloca/ex3b-alloca_true-termination.c.i exception 0 --- inspect 4.3 1.6  290 39 0   0   - --- inspect - --- inspect
termination-memory-alloca/fermat-alloca_true-termination.c.i exception 0 --- inspect 4.2 1.6  290 36 0   0   - --- inspect - --- inspect
termination-memory-alloca/flag-alloca_true-termination.c.i timeout 0 --- inspect 910   860    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/gcd1-alloca_true-termination.c.i timeout 0 --- inspect 910   860    4200 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/genady-alloca_true-termination.c.i timeout 0 --- inspect 900   850    7500 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/insertionsort-alloca_true-termination.c.i true 2 --- inspect 14   4.0  660 120 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_AG313-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_Break-alloca_true-termination.c.i timeout 0 --- inspect 900   850    3900 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i true 2 --- inspect 8.9 2.8  480 77 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i true 2 --- inspect 350   280    4700 4400 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i timeout 0 --- inspect 900   850    3900 10000 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_Nested-alloca_true-termination.c.i timeout 0 --- inspect 910   850    4100 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4000 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/lis-alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 15000 0   0   - --- inspect - --- inspect
termination-memory-alloca/min_rf-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/mult_array-alloca_true-termination.c.i exception 0 --- inspect 4.0 1.6  290 34 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i true 2 --- inspect 7.5 2.5  360 64 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i true 2 --- inspect 7.0 2.3  430 60 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i true 2 --- inspect 6.9 2.3  440 62 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i true 2 --- inspect 7.3 2.4  390 65 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i unknown 0 --- inspect 430   370    4400 5300 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i timeout 0 --- inspect 900   830    4400 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i timeout 0 --- inspect 900   830    4200 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i unknown 0 --- inspect 510   450    4500 6300 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i timeout 0 --- inspect 900   860    2400 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i timeout 0 --- inspect 900   850    2300 11000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i unknown 0 --- inspect 8.1 2.6  460 68 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4300 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i unknown 0 --- inspect 840   780    4100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i timeout 0 --- inspect 900   820    4400 13000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i true 2 --- inspect 9.1 2.8  350 82 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i timeout 0 --- inspect 900   860    2200 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i timeout 0 --- inspect 900   860    3000 14000 0   0   - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i timeout 0 --- inspect 900   830    4300 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i error (recursion) 0 --- inspect 4.0 1.6  280 36 0   0   - --- inspect - --- inspect
termination-memory-alloca/selectionsort-alloca_true-termination.c.i true 2 --- inspect 19   5.2  770 170 0   0   - --- inspect - --- inspect
termination-memory-alloca/stroeder1-alloca_true-termination.c.i true 2 --- inspect 6.0 2.1  300 55 0   0   - --- inspect - --- inspect
termination-memory-alloca/stroeder2-alloca_true-termination.c.i true 2 --- inspect 130   100    4000 1500 0   0   - --- inspect - --- inspect
termination-memory-alloca/strreplace-alloca_true-termination.c.i unknown 0 --- inspect 28   8.9  1400 250 0   0   - --- inspect - --- inspect
termination-memory-alloca/subseq-alloca_true-termination.c.i timeout 0 --- inspect 900   860    3100 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/substring-alloca_true-termination.c.i timeout 0 --- inspect 900   840    4200 12000 0   0   - --- inspect - --- inspect
termination-memory-alloca/twisted-alloca_true-termination.c.i timeout 0 --- inspect 900   860    4000 11000 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i error (recursion) 0 --- inspect 3.8 1.5  290 38 0   0   error (invalid witness file) 0 --- inspect .64 .39 41 0     0   error (2) 0 --- inspect .022 .024 5.6 0    0  
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i false(termination) 1 wit inspect 9.1 2.9  470 83 0   0   false(termination) 1 --- inspect 4.8  2.6  250 .033 0   false(termination) 1 --- inspect 11     6.7   400   .66 0  
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i unknown 0 --- inspect 58   31    3900 600 0   0   error (invalid witness file) 0 --- inspect .62 .37 42 0     0   error (2) 0 --- inspect .021 .024 5.7 0    0  
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i error (recursion) 0 --- inspect 4.0 1.6  290 35 0   0   error (invalid witness file) 0 --- inspect .58 .36 40 0     0   error (2) 0 --- inspect .021 .021 5.6 0    0  
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i error (recursion) 0 --- inspect 4.1 1.6  290 38 0   0   error (invalid witness file) 0 --- inspect .59 .36 41 0     0   error (2) 0 --- inspect .022 .023 5.6 0    0  
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i error (recursion) 0 --- inspect 4.0 1.5  280 36 0   0   error (invalid witness file) 0 --- inspect .63 .39 41 0     0   error (2) 0 --- inspect .023 .023 5.6 0    0  
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i unknown 0 --- inspect 71   33    3800 630 0   0   error (invalid witness file) 0 --- inspect .63 .39 42 0     0   error (2) 0 --- inspect .020 .022 5.7 0    0  
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i unknown 0 --- inspect 63   31    3900 610 0   0   error (invalid witness file) 0 --- inspect .68 .42 41 0     0   error (2) 0 --- inspect .024 .025 5.6 0    0  
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i error (recursion) 0 --- inspect 4.1 1.6  280 33 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i exception 0 --- inspect 4.3 1.7  300 38 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i error (recursion) 0 --- inspect 3.8 1.5  260 31 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i error (recursion) 0 --- inspect 3.9 1.6  290 33 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i error (recursion) 0 --- inspect 3.7 1.5  280 37 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i exception 0 --- inspect 4.1 1.7  260 38 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i unknown 0 --- inspect 15   4.5  530 150 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i unknown 0 --- inspect 8.9 2.8  460 84 0   0   - --- inspect - --- inspect
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i exception 0 --- inspect 4.5 1.7  300 38 0   0   - --- inspect - --- inspect
termination-15/add_first_alloca_true-termination.c.i true 2 --- inspect 12   4.4  500 110 0   0   - --- inspect - --- inspect
termination-15/array05_alloca_true-termination.c.i true 2 --- inspect 7.3 2.6  340 60 0   0   - --- inspect - --- inspect
termination-15/array06_alloca_true-termination.c.i true 2 --- inspect 6.9 2.5  340 69 0   0   - --- inspect - --- inspect
termination-15/array07_alloca_true-termination.c.i true 2 --- inspect 7.3 2.6  350 59 0   0   - --- inspect - --- inspect
termination-15/array08_alloca_true-termination.c.i timeout 0 --- inspect 900   840    4500 12000 0   0   - --- inspect - --- inspect
termination-15/array09_alloca_true-termination.c.i timeout 0 --- inspect 900   830    4500 12000 0   0   - --- inspect - --- inspect
termination-15/array10_alloca_true-termination.c.i true 2 --- inspect 7.1 2.6  340 64 0   0   - --- inspect - --- inspect
termination-15/array12_alloca_true-termination.c.i timeout 0 --- inspect 900   890    520 10000 0   0   - --- inspect - --- inspect
termination-15/array13_alloca_true-termination.c.i timeout 0 --- inspect 900   890    520 11000 0   0   - --- inspect - --- inspect
termination-15/array16_alloca_fixed_true-termination.c.i timeout 0 --- inspect 900   830    4700 14000 0   0   - --- inspect - --- inspect
termination-15/array17_alloca_true-termination.c.i unknown 0 --- inspect 14   4.1  540 110 0   0   - --- inspect - --- inspect
termination-15/array18_alloca_true-termination.c.i timeout 0 --- inspect 900   830    4400 12000 0   0   - --- inspect - --- inspect
termination-15/count_up_alloca_true-termination.c.i unknown 0 --- inspect 23   6.8  790 220 0   0   - --- inspect - --- inspect
termination-15/count_up_and_down_alloca_true-termination.c.i unknown 0 --- inspect 18   5.1  510 160 0   0   - --- inspect - --- inspect
termination-15/cstrcat_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   850    4000 11000 0   0   - --- inspect - --- inspect
termination-15/cstrcat_malloc_true-termination.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-15/cstrcat_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   850    4000 12000 0   0   - --- inspect - --- inspect
termination-15/cstrcat_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   810    4900 11000 0   0   - --- inspect - --- inspect
termination-15/cstrchr_diffterm_alloca_true-termination.c.i unknown 0 --- inspect 26   7.2  980 240 0   0   - --- inspect - --- inspect
termination-15/cstrchr_malloc_true-termination.c.i unknown 0 --- inspect 33   9.7  1500 260 0   0   - --- inspect - --- inspect
termination-15/cstrchr_reverse_alloca_true-termination.c.i unknown 0 --- inspect 14   4.1  690 130 0   0   - --- inspect - --- inspect
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3100 12000 0   0   - --- inspect - --- inspect
termination-15/cstrcmp_malloc_true-termination.c.i timeout 0 --- inspect 900   860    3200 11000 0   0   - --- inspect - --- inspect
termination-15/cstrcmp_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   860    2600 14000 0   0   - --- inspect - --- inspect
termination-15/cstrcmp_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3300 12000 0   0   - --- inspect - --- inspect
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i unknown 0 --- inspect 170   150    2400 1900 0   0   - --- inspect - --- inspect
termination-15/cstrcpy_malloc_true-termination.c.i unknown 0 --- inspect 170   150    2500 2200 0   0   - --- inspect - --- inspect
termination-15/cstrcpy_mixed_alloca_true-termination.c.i unknown 0 --- inspect 180   160    2600 2300 0   0   - --- inspect - --- inspect
termination-15/cstrcpy_reverse_alloca_true-termination.c.i unknown 0 --- inspect 180   160    2500 2700 0   0   - --- inspect - --- inspect
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 12000 0   0   - --- inspect - --- inspect
termination-15/cstrcspn_malloc_true-termination.c.i timeout 0 --- inspect 900   860    3500 12000 0   0   - --- inspect - --- inspect
termination-15/cstrcspn_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 11000 0   0   - --- inspect - --- inspect
termination-15/cstrcspn_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 12000 0   0   - --- inspect - --- inspect
termination-15/cstrlen_diffterm_alloca_true-termination.c.i unknown 0 --- inspect 30   11    1400 260 0   0   - --- inspect - --- inspect
termination-15/cstrlen_malloc_true-termination.c.i unknown 0 --- inspect 23   7.0  930 190 0   0   - --- inspect - --- inspect
termination-15/cstrlen_reverse_alloca_true-termination.c.i unknown 0 --- inspect 32   11    1300 290 0   0   - --- inspect - --- inspect
termination-15/cstrncat_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   840    4200 11000 0   0   - --- inspect - --- inspect
termination-15/cstrncat_malloc_true-termination.c.i timeout 0 --- inspect 900   840    4200 12000 0   0   - --- inspect - --- inspect
termination-15/cstrncat_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   850    4000 10000 0   0   - --- inspect - --- inspect
termination-15/cstrncat_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   830    4400 12000 0   0   - --- inspect - --- inspect
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3100 13000 0   0   - --- inspect - --- inspect
termination-15/cstrncmp_malloc_true-termination.c.i timeout 0 --- inspect 900   860    3100 14000 0   0   - --- inspect - --- inspect
termination-15/cstrncmp_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   860    2700 11000 0   0   - --- inspect - --- inspect
termination-15/cstrncmp_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3000 11000 0   0   - --- inspect - --- inspect
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   830    4600 11000 0   0   - --- inspect - --- inspect
termination-15/cstrncpy_malloc_true-termination.c.i unknown 0 --- inspect 620   550    4400 7000 0   0   - --- inspect - --- inspect
termination-15/cstrncpy_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   800    4700 13000 0   0   - --- inspect - --- inspect
termination-15/cstrncpy_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   830    4300 12000 0   0   - --- inspect - --- inspect
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 13000 0   0   - --- inspect - --- inspect
termination-15/cstrpbrk_malloc_true-termination.c.i timeout 0 --- inspect 900   850    3700 13000 0   0   - --- inspect - --- inspect
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   860    4100 15000 0   0   - --- inspect - --- inspect
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 13000 0   0   - --- inspect - --- inspect
termination-15/cstrspn_diffterm_alloca_true-termination.c.i timeout 0 --- inspect 900   860    3700 14000 0   0   - --- inspect - --- inspect
termination-15/cstrspn_malloc_true-termination.c.i timeout 0 --- inspect 900   860    3700 14000 0   0   - --- inspect - --- inspect
termination-15/cstrspn_mixed_alloca_true-termination.c.i timeout 0 --- inspect 900   850    4100 13000 0   0   - --- inspect - --- inspect
termination-15/cstrspn_reverse_alloca_true-termination.c.i timeout 0 --- inspect 900   850    3700 14000 0   0   - --- inspect - --- inspect
termination-15/array04_alloca_false-termination.c.i false(termination) 1 wit inspect 7.5 2.6  340 73 0   0   false(termination) 1 --- inspect 5.1  2.8  260 .033 0   false(termination) 1 --- inspect 11     6.3   320   .66 0  
termination-15/array14_alloca_false-termination.c.i timeout 0 --- inspect 900   840    4400 13000 0   0   error (invalid witness file) 0 --- inspect .65 .39 40 0     0   error (2) 0 --- inspect .022 .023 5.6 0    0  
termination-15/array15_alloca_false-termination.c.i timeout 0 --- inspect 900   840    4500 12000 0   0   error (invalid witness file) 0 --- inspect .68 .41 41 0     0   error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-15/array16_alloca_original_false-termination.c.i timeout 0 --- inspect 900   800    5200 11000 0   0   error (invalid witness file) 0 --- inspect .61 .37 41 0     0   error (2) 0 --- inspect .021 .023 5.6 0    0  
termination-15/array19_alloca_false-termination.c.i false(termination) 1 wit inspect 7.8 2.7  380 77 0   0   false(termination) 1 --- inspect 4.9  2.7  260 .033 0   false(termination) 1 --- inspect 9.8   5.6   330   .62 0  
termination-15/array20_alloca_false-termination.c.i exception 0 --- inspect 5.1 2.1  320 53 0   0   error (invalid witness file) 0 --- inspect .61 .38 42 0     0   error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-recursive-malloc/chunk1_true-termination.c.i error (recursion) 0 --- inspect 3.2 1.4  270 31 0   0   - --- inspect - --- inspect
termination-recursive-malloc/chunk2_true-termination.c.i error (recursion) 0 --- inspect 3.4 1.4  270 32 0   0   - --- inspect - --- inspect
termination-recursive-malloc/chunk3_true-termination.c.i error (recursion) 0 --- inspect 3.3 1.4  270 31 0   0   - --- inspect - --- inspect
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i error (recursion) 0 --- inspect 3.4 1.4  270 33 0   0   - --- inspect - --- inspect
termination-recursive-malloc/mergeSort_true-termination.c.i error (recursion) 0 --- inspect 3.5 1.5  270 31 0   0   - --- inspect - --- inspect
termination-recursive-malloc/mutual_simple2_true-termination.c.i error (recursion) 0 --- inspect 3.4 1.5  270 34 0   0   - --- inspect - --- inspect
termination-recursive-malloc/mutual_simple_true-termination.c.i error (recursion) 0 --- inspect 3.2 1.4  270 31 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i error (recursion) 0 --- inspect 3.2 1.4  270 33 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i error (recursion) 0 --- inspect 3.4 1.5  260 32 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i error (recursion) 0 --- inspect 3.3 1.5  270 32 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i error (recursion) 0 --- inspect 3.3 1.5  270 32 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i error (recursion) 0 --- inspect 3.3 1.4  270 33 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i error (recursion) 0 --- inspect 3.4 1.4  270 31 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i error (recursion) 0 --- inspect 3.3 1.4  270 33 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i error (recursion) 0 --- inspect 3.3 1.4  270 28 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i error (recursion) 0 --- inspect 3.3 1.4  270 30 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i error (recursion) 0 --- inspect 3.3 1.4  270 28 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i error (recursion) 0 --- inspect 3.4 1.4  270 32 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i error (recursion) 0 --- inspect 3.3 1.4  270 25 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i error (recursion) 0 --- inspect 3.3 1.4  270 31 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i error (recursion) 0 --- inspect 3.2 1.4  270 27 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i error (recursion) 0 --- inspect 3.3 1.5  270 30 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i error (recursion) 0 --- inspect 3.4 1.5  270 30 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i error (recursion) 0 --- inspect 3.5 1.5  270 31 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i error (recursion) 0 --- inspect 3.4 1.4  270 34 0   0   - --- inspect - --- inspect
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i error (recursion) 0 --- inspect 3.4 1.5  270 31 0   0   - --- inspect - --- inspect
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i error (recursion) 0 --- inspect 3.4 1.5  270 31 0   0   - --- inspect - --- inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 259 59 130000 120000   680000 1800000 0   0   16 3 23 13   1300 .098 0   16 3 32 19 1100 1.9 0  
    correct results 31 59 4400 3800   47000 58000 0   0   3 3 15 8.0 770 .098 0   3 3 32 19 1000 1.9 0  
        correct true 28 56 4400 3800   46000 58000 0   0   0 0
        correct false 3 3 24 8.2 1200 230 0   0   3 3 15 8.0 770 .098 0   3 3 32 19 1000 1.9 0  
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (259 tasks, max score: 502) 59 3 3
Run set pesco.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-termination.Termination-MainHeap