Tool ULTIMATE Automizer 0.1.23-635dfa2a CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-08 07:42:40 CET 2018-12-09 20:30:54 CET 2018-12-09 21:05:03 CET
Run set uautomizer.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-termination.Termination-MainHeap
Options --full-output -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/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
termination-libowfat/atoi_true-termination.c.i true 2 --- inspect 11   3.7 470 99 .66 0      - --- inspect - --- inspect
termination-libowfat/atol_true-termination.c.i true 2 --- inspect 10   3.5 470 87 .66 0      - --- inspect - --- inspect
termination-libowfat/atoll_true-termination.c.i true 2 --- inspect 11   3.6 470 99 .66 0      - --- inspect - --- inspect
termination-libowfat/basename_true-termination.c.i timeout 0 --- inspect 910   490   13000 7400 .63 0      - --- inspect - --- inspect
termination-libowfat/build_fullname_true-termination.c.i true 2 --- inspect 31   15   890 270 .66 0      - --- inspect - --- inspect
termination-libowfat/dirname_true-termination.c.i timeout 0 --- inspect 900   560   11000 6800 .63 0      - --- inspect - --- inspect
termination-libowfat/skip_to_true-termination.c.i unknown 0 --- inspect 49   18   2500 490 .66 0      - --- inspect - --- inspect
termination-libowfat/stpcpy_true-termination.c.i true 2 --- inspect 12   4.0 580 95 .66 0      - --- inspect - --- inspect
termination-libowfat/strcasecmp_true-termination.c.i true 2 --- inspect 13   4.3 580 110 .66 0      - --- inspect - --- inspect
termination-libowfat/strcat_short_true-termination.c.i true 2 --- inspect 21   7.1 740 160 .66 0      - --- inspect - --- inspect
termination-libowfat/strcat_true-termination.c.i error (7) 0 --- inspect 15   5.8 510 110 .66 0      - --- inspect - --- inspect
termination-libowfat/strchr_short_true-termination.c.i true 2 --- inspect 11   4.1 540 110 .66 0      - --- inspect - --- inspect
termination-libowfat/strchr_true-termination.c.i true 2 --- inspect 20   9.4 800 180 .66 0      - --- inspect - --- inspect
termination-libowfat/strcmp_short_true-termination.c.i true 2 --- inspect 12   4.0 510 91 .66 0      - --- inspect - --- inspect
termination-libowfat/strcpy_small_true-termination.c.i true 2 --- inspect 11   3.9 500 100 .66 0      - --- inspect - --- inspect
termination-libowfat/strcspn_true-termination.c.i true 2 --- inspect 22   9.7 740 190 .66 0      - --- inspect - --- inspect
termination-libowfat/strdup_true-termination.c.i true 2 --- inspect 15   5.5 520 140 .66 0      - --- inspect - --- inspect
termination-libowfat/strlcat_true-termination.c.i true 2 --- inspect 18   7.1 540 160 .66 .82   - --- inspect - --- inspect
termination-libowfat/strlcpy_true-termination.c.i true 2 --- inspect 19   6.5 690 180 .66 0      - --- inspect - --- inspect
termination-libowfat/strlen_true-termination.c.i true 2 --- inspect 11   3.3 440 91 .66 0      - --- inspect - --- inspect
termination-libowfat/strpbrk_true-termination.c.i unknown 0 --- inspect 35   9.6 1100 260 .66 0      - --- inspect - --- inspect
termination-libowfat/strrchr_short_true-termination.c.i true 2 --- inspect 11   3.9 510 100 .66 0      - --- inspect - --- inspect
termination-libowfat/strrchr_true-termination.c.i true 2 --- inspect 14   4.5 590 110 .66 0      - --- inspect - --- inspect
termination-libowfat/strspn_true-termination.c.i true 2 --- inspect 19   6.7 570 150 .66 0      - --- inspect - --- inspect
termination-libowfat/strstr_true-termination.c.i true 2 --- inspect 46   21   1000 420 .66 0      - --- inspect - --- inspect
termination-libowfat/strtok_r_true-termination.c.i true 2 --- inspect 56   27   1300 600 .66 .0082 - --- inspect - --- inspect
termination-libowfat/strtol_true-termination.c.i true 2 --- inspect 16   5.6 540 140 .66 0      - --- inspect - --- inspect
termination-libowfat/strtoul_true-termination.c.i true 2 --- inspect 13   4.2 500 100 .66 0      - --- inspect - --- inspect
termination-libowfat/strtoull_true-termination.c.i true 2 --- inspect 11   4.1 490 92 .66 0      - --- inspect - --- inspect
termination-libowfat/wcsrchr_true-termination.c.i true 2 --- inspect 11   3.6 500 91 .66 0      - --- inspect - --- inspect
termination-libowfat/wcsstr_true-termination.c.i true 2 --- inspect 8.4 2.8 380 76 .66 0      - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i false(termination) 1 wit inspect 9.1 3.0 380 71 .66 0      false(termination) 1 wit inspect 7.9  4.3  290 .033  0      false(termination) 1 --- inspect 8.5   4.8   310   .62 0     
termination-memory-alloca/Velroyen-alloca_false-termination.c.i false(termination) 1 wit inspect 11   4.0 510 91 .66 .23   false(termination) 1 wit inspect 10    5.5  360 .0082 0      false(termination) 1 --- inspect 9.3   5.7   320   .62 0     
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i true 2 --- inspect 18   6.8 550 150 .66 0      - --- inspect - --- inspect
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i true 2 --- inspect 25   11   640 240 .66 0      - --- inspect - --- inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 900   750   1500 9500 .65 0      - --- inspect - --- inspect
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i true 2 --- inspect 10   3.5 440 88 .66 .0082 - --- inspect - --- inspect
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i true 2 --- inspect 14   4.4 590 120 .66 0      - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i true 2 --- inspect 18   6.1 690 150 .66 0      - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i true 2 --- inspect 52   33   790 540 .62 0      - --- inspect - --- inspect
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i true 2 --- inspect 140   110   1000 1500 .62 0      - --- inspect - --- inspect
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i timeout 0 --- inspect 900   800   1500 11000 .64 0      - --- inspect - --- inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i true 2 --- inspect 27   12   810 250 .66 0      - --- inspect - --- inspect
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i true 2 --- inspect 11   3.4 400 71 .66 0      - --- inspect - --- inspect
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i true 2 --- inspect 15   5.2 560 130 .66 0      - --- inspect - --- inspect
termination-memory-alloca/Masse-alloca_true-termination.c.i unknown 0 --- inspect 18   5.1 700 130 .66 0      - --- inspect - --- inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i true 2 --- inspect 45   30   890 440 .66 0      - --- inspect - --- inspect
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i true 2 --- inspect 680   520   13000 7700 .62 0      - --- inspect - --- inspect
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i timeout 0 --- inspect 910   320   14000 5800 .63 0      - --- inspect - --- inspect
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i true 2 --- inspect 16   5.6 670 130 .66 0      - --- inspect - --- inspect
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i true 2 --- inspect 31   15   750 300 .66 0      - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i true 2 --- inspect 21   9.3 560 200 .66 0      - --- inspect - --- inspect
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i timeout 0 --- inspect 900   720   780 9300 .64 0      - --- inspect - --- inspect
termination-memory-alloca/Urban-alloca_true-termination.c.i true 2 --- inspect 26   10   660 210 .66 0      - --- inspect - --- inspect
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 30   14   820 290 .66 0      - --- inspect - --- inspect
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 11   3.8 540 88 .66 0      - --- inspect - --- inspect
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 11   4.2 490 94 .66 0      - --- inspect - --- inspect
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 23   9.1 750 200 .66 .0082 - --- inspect - --- inspect
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 14   5.0 560 140 .66 0      - --- inspect - --- inspect
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 12   4.1 520 92 .66 0      - --- inspect - --- inspect
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 13   4.3 500 110 .66 0      - --- inspect - --- inspect
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 18   6.2 710 160 .66 0      - --- inspect - --- inspect
termination-memory-alloca/add_last-alloca_true-termination.c.i true 2 --- inspect 11   3.8 470 89 .66 0      - --- inspect - --- inspect
termination-memory-alloca/array01-alloca_true-termination.c.i true 2 --- inspect 15   4.7 560 100 .66 0      - --- inspect - --- inspect
termination-memory-alloca/array02-alloca_true-termination.c.i true 2 --- inspect 17   5.7 560 140 .66 0      - --- inspect - --- inspect
termination-memory-alloca/array03-alloca_true-termination.c.i true 2 --- inspect 17   5.6 600 150 .66 0      - --- inspect - --- inspect
termination-memory-alloca/aviad_true-alloca_true-termination.c.i true 2 --- inspect 14   4.8 590 120 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 11   3.9 490 83 .66 .0041 - --- inspect - --- inspect
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 11   4.4 550 100 .66 .0082 - --- inspect - --- inspect
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 12   4.0 550 94 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 12   4.0 540 99 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 11   4.4 480 99 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 12   4.1 580 99 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 12   4.1 590 110 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 14   4.9 520 110 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i unknown 0 --- inspect 39   15   1700 340 .66 .0041 - --- inspect - --- inspect
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 26   10   760 230 .66 .83   - --- inspect - --- inspect
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 18   6.5 660 160 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 25   9.7 750 220 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 18   6.2 550 160 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 22   9.2 630 180 .66 .012  - --- inspect - --- inspect
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 27   14   720 250 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 27   14   610 260 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 15   5.2 520 120 .66 .0082 - --- inspect - --- inspect
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 22   9.0 750 170 .66 0      - --- inspect - --- inspect
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 21   7.3 750 170 .66 0      - --- inspect - --- inspect
termination-memory-alloca/bubblesort-alloca_true-termination.c.i true 2 --- inspect 16   5.3 630 130 .66 0      - --- inspect - --- inspect
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850   750 12000 .63 0      - --- inspect - --- inspect
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 38   18   680 430 .66 0      - --- inspect - --- inspect
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   850   990 11000 .63 0      - --- inspect - --- inspect
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 20   7.8 740 190 .66 0      - --- inspect - --- inspect
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i true 2 --- inspect 15   5.8 600 120 .66 0      - --- inspect - --- inspect
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i timeout 0 --- inspect 900   840   1000 13000 .63 0      - --- inspect - --- inspect
termination-memory-alloca/count_down-alloca_true-termination.c.i true 2 --- inspect 17   5.4 520 130 .66 .0082 - --- inspect - --- inspect
termination-memory-alloca/cstrcat-alloca_true-termination.c.i true 2 --- inspect 12   4.0 560 90 .66 0      - --- inspect - --- inspect
termination-memory-alloca/cstrchr-alloca_true-termination.c.i true 2 --- inspect 12   3.9 560 98 .66 0      - --- inspect - --- inspect
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i true 2 --- inspect 12   4.3 570 99 .66 0      - --- inspect - --- inspect
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i true 2 --- inspect 13   4.2 550 100 .66 0      - --- inspect - --- inspect
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i true 2 --- inspect 110   91   1300 1400 .62 0      - --- inspect - --- inspect
termination-memory-alloca/cstrlen-alloca_true-termination.c.i true 2 --- inspect 11   3.4 450 83 .66 0      - --- inspect - --- inspect
termination-memory-alloca/cstrncat-alloca_true-termination.c.i true 2 --- inspect 13   4.5 520 93 .66 0      - --- inspect - --- inspect
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i true 2 --- inspect 13   4.6 550 110 .66 41      - --- inspect - --- inspect
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i true 2 --- inspect 16   5.5 670 160 .66 0      - --- inspect - --- inspect
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i true 2 --- inspect 32   14   1100 310 .66 0      - --- inspect - --- inspect
termination-memory-alloca/cstrspn-alloca_true-termination.c.i true 2 --- inspect 22   8.5 670 230 .66 0      - --- inspect - --- inspect
termination-memory-alloca/diff-alloca_true-termination.c.i true 2 --- inspect 19   6.9 570 160 .66 0      - --- inspect - --- inspect
termination-memory-alloca/easySum-alloca_true-termination.c.i true 2 --- inspect 12   4.2 570 93 .66 0      - --- inspect - --- inspect
termination-memory-alloca/ex1-alloca_true-termination.c.i true 2 --- inspect 13   4.3 570 110 .66 0      - --- inspect - --- inspect
termination-memory-alloca/ex2-alloca_true-termination.c.i unknown 0 --- inspect 45   18   1200 390 .66 0      - --- inspect - --- inspect
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i unknown 0 --- inspect 25   7.1 650 200 .66 0      - --- inspect - --- inspect
termination-memory-alloca/ex3b-alloca_true-termination.c.i unknown 0 --- inspect 30   9.1 860 240 .66 0      - --- inspect - --- inspect
termination-memory-alloca/fermat-alloca_true-termination.c.i timeout 0 --- inspect 900   880   870 13000 .63 0      - --- inspect - --- inspect
termination-memory-alloca/flag-alloca_true-termination.c.i true 2 --- inspect 20   6.6 780 170 .66 0      - --- inspect - --- inspect
termination-memory-alloca/gcd1-alloca_true-termination.c.i true 2 --- inspect 65   38   860 610 .62 0      - --- inspect - --- inspect
termination-memory-alloca/genady-alloca_true-termination.c.i true 2 --- inspect 10   3.7 470 97 .66 0      - --- inspect - --- inspect
termination-memory-alloca/insertionsort-alloca_true-termination.c.i true 2 --- inspect 16   5.6 580 140 .66 0      - --- inspect - --- inspect
termination-memory-alloca/java_AG313-alloca_true-termination.c.i true 2 --- inspect 14   4.7 500 120 .66 0      - --- inspect - --- inspect
termination-memory-alloca/java_Break-alloca_true-termination.c.i true 2 --- inspect 11   3.6 460 93 .66 .0082 - --- inspect - --- inspect
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i true 2 --- inspect 18   5.9 680 170 .66 .0082 - --- inspect - --- inspect
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i true 2 --- inspect 42   22   640 490 .66 0      - --- inspect - --- inspect
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i true 2 --- inspect 12   3.8 510 97 .66 .78   - --- inspect - --- inspect
termination-memory-alloca/java_Nested-alloca_true-termination.c.i error (7) 0 --- inspect 85   64   710 1200 .62 0      - --- inspect - --- inspect
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i timeout 0 --- inspect 900   790   1100 10000 .63 0      - --- inspect - --- inspect
termination-memory-alloca/lis-alloca_true-termination.c.i timeout 0 --- inspect 900   860   1000 13000 .63 0      - --- inspect - --- inspect
termination-memory-alloca/min_rf-alloca_true-termination.c.i true 2 --- inspect 210   160   7700 2700 .62 .0082 - --- inspect - --- inspect
termination-memory-alloca/mult_array-alloca_true-termination.c.i true 2 --- inspect 15   5.1 590 130 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i true 2 --- inspect 11   4.3 470 95 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i true 2 --- inspect 12   4.2 500 110 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i true 2 --- inspect 11   3.7 500 92 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i true 2 --- inspect 12   3.7 510 90 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i true 2 --- inspect 11   4.0 490 100 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i true 2 --- inspect 27   16   560 290 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i true 2 --- inspect 12   3.9 570 110 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i true 2 --- inspect 12   4.1 500 93 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i true 2 --- inspect 13   4.0 600 100 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i unknown 0 --- inspect 34   11   1300 330 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i true 2 --- inspect 16   6.3 720 130 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i true 2 --- inspect 11   3.8 450 95 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i true 2 --- inspect 12   4.5 570 100 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i true 2 --- inspect 13   4.6 570 99 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i true 2 --- inspect 16   5.6 530 140 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i true 2 --- inspect 11   3.8 520 86 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i true 2 --- inspect 33   20   750 360 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i unknown 0 --- inspect 37   11   1700 320 .66 0      - --- inspect - --- inspect
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i true 2 --- inspect 41   20   820 320 .66 0      - --- inspect - --- inspect
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i true 2 --- inspect 10   3.4 440 85 .66 0      - --- inspect - --- inspect
termination-memory-alloca/selectionsort-alloca_true-termination.c.i true 2 --- inspect 19   6.8 710 170 .66 0      - --- inspect - --- inspect
termination-memory-alloca/stroeder1-alloca_true-termination.c.i true 2 --- inspect 11   4.0 410 85 .66 0      - --- inspect - --- inspect
termination-memory-alloca/stroeder2-alloca_true-termination.c.i true 2 --- inspect 13   4.7 580 110 .66 0      - --- inspect - --- inspect
termination-memory-alloca/strreplace-alloca_true-termination.c.i true 2 --- inspect 12   4.1 560 100 .66 0      - --- inspect - --- inspect
termination-memory-alloca/subseq-alloca_true-termination.c.i true 2 --- inspect 12   4.2 570 100 .66 0      - --- inspect - --- inspect
termination-memory-alloca/substring-alloca_true-termination.c.i true 2 --- inspect 22   9.3 750 180 .66 0      - --- inspect - --- inspect
termination-memory-alloca/twisted-alloca_true-termination.c.i true 2 --- inspect 24   9.7 620 250 .66 0      - --- inspect - --- inspect
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i false(termination) 1 wit inspect 13   5.1 560 110 .66 .070  error (recursion) 0 --- inspect 7.0  3.7  260 .016  0      false(termination) 1 --- inspect 11     7.1   420   .62 0     
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i false(termination) 1 wit inspect 13   4.7 600 110 .66 0      false(termination) 1 wit inspect 12    6.1  440 .033  0      false(termination) 1 --- inspect 11     6.7   400   .62 0     
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i false(termination) 1 wit inspect 14   4.7 590 120 .66 0      false(termination) 1 wit inspect 9.1  4.8  350 .033  0      false(termination) 1 --- inspect 10     6.1   370   .62 .025 
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i false(termination) 1 wit inspect 15   5.8 510 140 .66 0      error (recursion) 0 --- inspect 5.7  3.1  250 .0082 0      false(termination) 1 --- inspect 15     9.0   530   .62 .0041
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i false(termination) 1 wit inspect 34   12   1300 280 .66 .061  error (recursion) 0 --- inspect 6.5  3.5  250 .0082 0      false(termination) 1 --- inspect 18     11     530   .62 0     
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i unknown 0 --- inspect 25   7.2 720 170 .66 0      error (invalid witness file) 0 --- inspect .71 .44 41 0      0      error (2) 0 --- inspect .021 .021 5.6 0    0     
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i false(termination) 1 wit inspect 28   9.0 880 230 .66 0      false(termination) 1 wit inspect 17    9.0  690 .033  0      false(termination) 1 --- inspect 12     6.8   420   .62 0     
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i false(termination) 1 wit inspect 31   9.6 1300 270 .66 0      false(termination) 1 wit inspect 7.9  4.2  360 .033  0      false(termination) 1 --- inspect 11     6.3   390   .62 0     
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i true 2 --- inspect 12   4.0 520 91 .66 0      - --- inspect - --- inspect
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i unknown 0 --- inspect 330   300   1800 4900 .62 0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i error (7) 0 --- inspect 210   190   1600 2600 .62 0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i error (7) 0 --- inspect 270   240   2100 3000 .62 0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i true 2 --- inspect 9.6 3.5 430 78 .66 0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i unknown 0 --- inspect 190   160   1900 2800 .62 0      - --- inspect - --- inspect
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i unknown 0 --- inspect 45   18   1800 430 .66 .72   - --- inspect - --- inspect
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i unknown 0 --- inspect 41   18   1900 430 .66 0      - --- inspect - --- inspect
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i unknown 0 --- inspect 300   260   3800 3700 .62 0      - --- inspect - --- inspect
termination-15/add_first_alloca_true-termination.c.i true 2 --- inspect 11   3.4 440 85 .66 0      - --- inspect - --- inspect
termination-15/array05_alloca_true-termination.c.i unknown 0 --- inspect 18   5.1 590 140 .66 0      - --- inspect - --- inspect
termination-15/array06_alloca_true-termination.c.i true 2 --- inspect 13   4.0 540 99 .66 0      - --- inspect - --- inspect
termination-15/array07_alloca_true-termination.c.i true 2 --- inspect 13   4.3 550 110 .66 0      - --- inspect - --- inspect
termination-15/array08_alloca_true-termination.c.i unknown 0 --- inspect 25   6.9 640 220 .66 0      - --- inspect - --- inspect
termination-15/array09_alloca_true-termination.c.i unknown 0 --- inspect 27   7.1 810 210 .66 0      - --- inspect - --- inspect
termination-15/array10_alloca_true-termination.c.i unknown 0 --- inspect 19   5.3 780 150 .66 0      - --- inspect - --- inspect
termination-15/array12_alloca_true-termination.c.i timeout 0 --- inspect 900   790   950 11000 .63 0      - --- inspect - --- inspect
termination-15/array13_alloca_true-termination.c.i timeout 0 --- inspect 900   780   780 6900 .63 0      - --- inspect - --- inspect
termination-15/array16_alloca_fixed_true-termination.c.i timeout 0 --- inspect 900   790   1200 8900 .64 .29   - --- inspect - --- inspect
termination-15/array17_alloca_true-termination.c.i timeout 0 --- inspect 900   790   760 7000 .64 0      - --- inspect - --- inspect
termination-15/array18_alloca_true-termination.c.i unknown 0 --- inspect 25   6.8 630 180 .66 0      - --- inspect - --- inspect
termination-15/count_up_alloca_true-termination.c.i true 2 --- inspect 16   5.3 510 140 .66 .37   - --- inspect - --- inspect
termination-15/count_up_and_down_alloca_true-termination.c.i true 2 --- inspect 14   4.8 590 110 .66 0      - --- inspect - --- inspect
termination-15/cstrcat_diffterm_alloca_true-termination.c.i true 2 --- inspect 12   3.9 570 97 .66 0      - --- inspect - --- inspect
termination-15/cstrcat_malloc_true-termination.c.i true 2 --- inspect 12   4.0 580 110 .66 0      - --- inspect - --- inspect
termination-15/cstrcat_mixed_alloca_true-termination.c.i true 2 --- inspect 12   4.0 560 110 .66 0      - --- inspect - --- inspect
termination-15/cstrcat_reverse_alloca_true-termination.c.i true 2 --- inspect 13   4.4 580 100 .66 0      - --- inspect - --- inspect
termination-15/cstrchr_diffterm_alloca_true-termination.c.i true 2 --- inspect 11   3.7 510 79 .66 0      - --- inspect - --- inspect
termination-15/cstrchr_malloc_true-termination.c.i true 2 --- inspect 12   3.9 480 100 .66 .27   - --- inspect - --- inspect
termination-15/cstrchr_reverse_alloca_true-termination.c.i true 2 --- inspect 11   3.6 520 110 .66 0      - --- inspect - --- inspect
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i true 2 --- inspect 12   4.1 500 100 .66 0      - --- inspect - --- inspect
termination-15/cstrcmp_malloc_true-termination.c.i true 2 --- inspect 13   4.4 550 120 .66 0      - --- inspect - --- inspect
termination-15/cstrcmp_mixed_alloca_true-termination.c.i true 2 --- inspect 13   4.2 520 120 .66 0      - --- inspect - --- inspect
termination-15/cstrcmp_reverse_alloca_true-termination.c.i true 2 --- inspect 12   4.2 520 94 .66 .78   - --- inspect - --- inspect
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i true 2 --- inspect 12   4.6 490 94 .66 0      - --- inspect - --- inspect
termination-15/cstrcpy_malloc_true-termination.c.i true 2 --- inspect 12   4.2 490 110 .66 0      - --- inspect - --- inspect
termination-15/cstrcpy_mixed_alloca_true-termination.c.i true 2 --- inspect 12   4.3 550 100 .66 0      - --- inspect - --- inspect
termination-15/cstrcpy_reverse_alloca_true-termination.c.i true 2 --- inspect 12   4.2 520 91 .66 0      - --- inspect - --- inspect
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i true 2 --- inspect 34   21   610 350 .66 0      - --- inspect - --- inspect
termination-15/cstrcspn_malloc_true-termination.c.i true 2 --- inspect 110   96   580 1600 .62 0      - --- inspect - --- inspect
termination-15/cstrcspn_mixed_alloca_true-termination.c.i true 2 --- inspect 140   120   810 1700 .62 0      - --- inspect - --- inspect
termination-15/cstrcspn_reverse_alloca_true-termination.c.i true 2 --- inspect 22   8.9 620 210 .66 0      - --- inspect - --- inspect
termination-15/cstrlen_diffterm_alloca_true-termination.c.i true 2 --- inspect 11   3.5 460 91 .66 0      - --- inspect - --- inspect
termination-15/cstrlen_malloc_true-termination.c.i true 2 --- inspect 10   3.6 440 82 .66 0      - --- inspect - --- inspect
termination-15/cstrlen_reverse_alloca_true-termination.c.i true 2 --- inspect 11   3.6 460 82 .66 0      - --- inspect - --- inspect
termination-15/cstrncat_diffterm_alloca_true-termination.c.i true 2 --- inspect 12   4.1 600 100 .66 0      - --- inspect - --- inspect
termination-15/cstrncat_malloc_true-termination.c.i true 2 --- inspect 12   4.1 580 94 .66 0      - --- inspect - --- inspect
termination-15/cstrncat_mixed_alloca_true-termination.c.i true 2 --- inspect 12   4.1 500 110 .66 0      - --- inspect - --- inspect
termination-15/cstrncat_reverse_alloca_true-termination.c.i true 2 --- inspect 12   4.1 550 100 .66 0      - --- inspect - --- inspect
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i true 2 --- inspect 12   4.6 590 110 .66 0      - --- inspect - --- inspect
termination-15/cstrncmp_malloc_true-termination.c.i true 2 --- inspect 11   4.1 500 97 .66 0      - --- inspect - --- inspect
termination-15/cstrncmp_mixed_alloca_true-termination.c.i true 2 --- inspect 13   4.2 590 100 .66 0      - --- inspect - --- inspect
termination-15/cstrncmp_reverse_alloca_true-termination.c.i true 2 --- inspect 11   4.4 540 100 .66 40      - --- inspect - --- inspect
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i true 2 --- inspect 16   5.8 610 140 .66 0      - --- inspect - --- inspect
termination-15/cstrncpy_malloc_true-termination.c.i true 2 --- inspect 16   5.7 650 120 .66 0      - --- inspect - --- inspect
termination-15/cstrncpy_mixed_alloca_true-termination.c.i true 2 --- inspect 15   5.9 640 140 .66 0      - --- inspect - --- inspect
termination-15/cstrncpy_reverse_alloca_true-termination.c.i true 2 --- inspect 15   5.3 660 120 .66 0      - --- inspect - --- inspect
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i true 2 --- inspect 40   19   1600 320 .66 0      - --- inspect - --- inspect
termination-15/cstrpbrk_malloc_true-termination.c.i true 2 --- inspect 41   21   1500 360 .66 0      - --- inspect - --- inspect
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i true 2 --- inspect 21   8.8 750 190 .66 0      - --- inspect - --- inspect
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i true 2 --- inspect 23   11   650 210 .66 0      - --- inspect - --- inspect
termination-15/cstrspn_diffterm_alloca_true-termination.c.i true 2 --- inspect 22   9.6 760 190 .66 0      - --- inspect - --- inspect
termination-15/cstrspn_malloc_true-termination.c.i true 2 --- inspect 21   8.6 600 200 .66 0      - --- inspect - --- inspect
termination-15/cstrspn_mixed_alloca_true-termination.c.i true 2 --- inspect 23   9.2 750 210 .66 0      - --- inspect - --- inspect
termination-15/cstrspn_reverse_alloca_true-termination.c.i true 2 --- inspect 22   8.5 610 180 .66 0      - --- inspect - --- inspect
termination-15/array04_alloca_false-termination.c.i false(termination) 1 wit inspect 12   3.8 460 91 .66 0      error 0 --- inspect 11    6.1  440 .033  0      false(termination) 1 --- inspect 10     5.5   330   .66 .012 
termination-15/array14_alloca_false-termination.c.i false(termination) 1 wit inspect 17   5.4 530 140 .66 0      error 0 --- inspect 13    6.7  430 .033  0      false(termination) 1 --- inspect 10     6.0   340   .62 0     
termination-15/array15_alloca_false-termination.c.i false(termination) 1 wit inspect 17   5.5 590 150 .66 0      error 0 --- inspect 12    6.4  440 .033  0      false(termination) 1 --- inspect 11     6.6   340   .62 0     
termination-15/array16_alloca_original_false-termination.c.i false(termination) 1 wit inspect 19   6.6 550 180 .66 0      timeout 0 --- inspect 92    65    1900 .033  .045  false(termination) 1 --- inspect 12     6.8   460   .62 0     
termination-15/array19_alloca_false-termination.c.i false(termination) 1 wit inspect 11   3.6 460 92 .66 0      error 0 --- inspect 11    5.7  440 .033  0      false(termination) 1 --- inspect 9.7   5.5   320   .66 0     
termination-15/array20_alloca_false-termination.c.i false(termination) 1 wit inspect 13   4.1 490 110 .66 0      exception 0 --- inspect 11    5.6  380 .033  .0041 false(termination) 1 --- inspect 10     6.2   360   .62 0     
termination-recursive-malloc/chunk1_true-termination.c.i true 2 --- inspect 9.2 3.4 400 86 .66 .057  - --- inspect - --- inspect
termination-recursive-malloc/chunk2_true-termination.c.i error (7) 0 --- inspect 88   60   1200 1000 .62 0      - --- inspect - --- inspect
termination-recursive-malloc/chunk3_true-termination.c.i error (7) 0 --- inspect 190   160   1300 2600 .62 0      - --- inspect - --- inspect
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i true 2 --- inspect 31   13   850 270 .62 .020  - --- inspect - --- inspect
termination-recursive-malloc/mergeSort_true-termination.c.i error (7) 0 --- inspect 55   30   1300 560 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/mutual_simple2_true-termination.c.i true 2 --- inspect 12   4.3 590 110 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/mutual_simple_true-termination.c.i true 2 --- inspect 11   4.2 470 83 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i true 2 --- inspect 13   4.6 570 120 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i true 2 --- inspect 20   8.4 550 190 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i true 2 --- inspect 22   9.8 590 220 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i true 2 --- inspect 21   9.4 760 210 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i true 2 --- inspect 22   9.9 610 240 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i timeout 0 --- inspect 900   880   900 12000 .63 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i true 2 --- inspect 27   12   790 230 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i true 2 --- inspect 22   8.9 640 190 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i true 2 --- inspect 12   4.5 480 110 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i timeout 0 --- inspect 900   880   1700 5700 .63 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i true 2 --- inspect 23   11   750 210 .66 .057  - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i unknown 0 --- inspect 39   16   1100 330 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i true 2 --- inspect 13   4.3 520 92 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i unknown 0 --- inspect 35   12   1100 320 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i unknown 0 --- inspect 41   16   1200 340 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i timeout 0 --- inspect 900   860   1200 11000 .64 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i true 2 --- inspect 14   5.2 500 110 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i true 2 --- inspect 12   4.2 570 94 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i true 2 --- inspect 8.8 3.3 400 84 .66 0      - --- inspect - --- inspect
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i true 2 --- inspect 20   7.3 730 190 .66 .057  - --- 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 405 24000 19000 240000 260000 170   87    16 6 230 140 7400 .40 .049 16 15 170 100 5800 9.4 .041
    correct results 210 405 4900 2500 150000 48000 140   86    6 6 64 34 2500 .17 0     15 15 170 100 5800 9.4 .041
        correct true 195 390 4700 2400 140000 46000 130   85    0 0
        correct false 15 15 260 86 9700 2200 9.8 .36 6 6 64 34 2500 .17 0     15 15 170 100 5800 9.4 .041
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (259 tasks, max score: 502) 405 6 15
Run set uautomizer.sv-comp19_prop-termination.Termination-MainHeap cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-termination.Termination-MainHeap uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-termination.Termination-MainHeap