Tool 2LS 0.7.2-sv-comp19 AProVE 84fce4cdfd CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux PeSCo 1.7-svn b8d6131600+ Pinaka 0.1 SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
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-04 22:44:17 CET 2018-12-04 22:41:51 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:44:04 CET 2018-12-06 20:14:43 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET
Run set 2ls.sv-comp19_prop-termination.Termination-MainHeap aprove.sv-comp19_prop-termination.Termination-MainHeap cbmc.sv-comp19_prop-termination.Termination-MainHeap cbmc-path.sv-comp19_prop-termination.Termination-MainHeap cpa-seq.sv-comp19_prop-termination.Termination-MainHeap depthk.sv-comp19_prop-termination.Termination-MainHeap divine-explicit.sv-comp19_prop-termination.Termination-MainHeap divine-smt.sv-comp19_prop-termination.Termination-MainHeap esbmc-kind.sv-comp19_prop-termination.Termination-MainHeap pesco.sv-comp19_prop-termination.Termination-MainHeap pinaka.sv-comp19_prop-termination.Termination-MainHeap smack.sv-comp19_prop-termination.Termination-MainHeap symbiotic.sv-comp19_prop-termination.Termination-MainHeap uautomizer.sv-comp19_prop-termination.Termination-MainHeap ukojak.sv-comp19_prop-termination.Termination-MainHeap utaipan.sv-comp19_prop-termination.Termination-MainHeap
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s --graphml-witness witness.graphml -w error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
termination-libowfat/atoi_true-termination.c.i error (134) .26 46 1.8 0 true 72   2500 590 2 error (42) 880     13000   8400    0 error (42) 880     2500   6900    0 unknown 130   3800 1500 0 true .49 36 7.0 2 unknown .037 4.6 .25 0 unknown .044 4.6 .23  0 timeout 900     1700 11000    0 unknown 110   3700 1300 0 timeout 900    4500 12000   0 disqualified .045 9.5 .36 0 true .20 17 2.3 2 true 11   470 99 2 error (5) .023 5.6 .17  0 error (5) .024 5.6 .15  0
termination-libowfat/atol_true-termination.c.i error (134) .27 46 1.9 0 true 78   2500 580 2 error (42) 880     13000   8300    0 error (42) 880     2500   8200    0 unknown 61   2900 540 0 true .51 36 5.7 2 unknown .055 4.5 .19 0 unknown .035 4.6 .28  0 timeout 900     1700 11000    0 unknown 48   3200 540 0 timeout 900    4500 10000   0 disqualified .069 9.2 .40 0 true .22 17 2.5 2 true 10   470 87 2 error (5) .022 5.7 .16  0 error (5) .025 5.7 .17  0
termination-libowfat/atoll_true-termination.c.i error (134) .26 46 2.4 0 true 71   3800 600 2 error (42) 880     13000   8200    0 error (42) 880     2400   7000    0 unknown 110   3800 1400 0 true .50 36 6.7 2 unknown .050 4.7 .14 0 unknown .023 4.6 .16  0 timeout 900     1700 12000    0 unknown 86   3800 890 0 timeout 900    4500 11000   0 disqualified .048 9.6 .39 0 true .20 18 2.4 2 true 11   470 99 2 error (5) .049 5.6 .095 0 error (5) .023 5.7 .17  0
termination-libowfat/basename_true-termination.c.i error (134) .27 46 2.0 0 out of memory 900   15000 4600 0 error (42) 880     4600   6100    0 out of memory 180     15000   2100    0 unknown 65   2200 770 0 true .77 41 11   2 unknown .029 4.6 .15 0 unknown .031 4.6 .19  0 timeout 900     740 11000    0 unknown 67   2200 760 0 out of memory 82    15000 1200   0 disqualified .048 9.2 .39 0 timeout (verification) 900    320 11000   0 timeout 910   13000 7400 0 error (5) .041 5.8 .11  0 error (5) .028 5.6 .13  0
termination-libowfat/build_fullname_true-termination.c.i error (134) .27 46 1.9 0 error (1) 51   1900 630 0 error (42) 880     14000   9300    0 error (42) 880     2300   9100    0 timeout 900   3900 12000 0 true .54 36 6.5 2 unknown .055 4.6 .15 0 unknown .040 4.7 .34  0 timeout 900     510 11000    0 timeout 900   3900 11000 0 error (8) .72 64 6.2 0 disqualified .044 9.0 .43 0 timeout (verification) 900    220 12000   0 true 31   890 270 2 error (5) .024 5.6 .12  0 error (5) .026 5.6 .14  0
termination-libowfat/dirname_true-termination.c.i error (134) .26 46 2.0 0 timeout 910   13000 5100 0 error (42) 880     14000   8700    0 out of memory 160     15000   2000    0 timeout 900   4300 11000 0 true 3.9  96 48   2 unknown .028 4.6 .20 0 unknown .050 4.6 .15  0 timeout 900     3700 8500    0 timeout 900   4200 12000 0 error (8) .92 76 9.0 0 disqualified .049 9.4 .38 0 timeout (verification) 900    370 11000   0 timeout 900   11000 6800 0 error (5) .032 5.6 .22  0 error (5) .023 5.6 .16  0
termination-libowfat/skip_to_true-termination.c.i error (134) .26 46 2.1 0 true 25   2300 220 2 error (42) 880     1000   7700    0 error (42) 880     350   6500    0 unknown 9.2 510 77 0 true .51 36 6.1 2 unknown .046 4.6 .17 0 unknown .031 4.6 .17  0 timeout 900     4300 10000    0 unknown 9.8 430 90 0 timeout 900    1100 10000   0 disqualified .044 9.2 .36 0 timeout (verification) 900    620 11000   0 unknown 49   2500 490 0 error (5) .023 5.6 .12  0 error (5) .022 5.6 .15  0
termination-libowfat/stpcpy_true-termination.c.i error (134) .29 46 2.1 0 error (1) 15   810 120 0 error (42) 880     14000   4600    0 error (42) 880     14000   6400    0 timeout 900   4200 12000 0 true .48 36 6.0 2 unknown .030 4.5 .17 0 unknown .059 4.6 .23  0 timeout 900     3100 11000    0 timeout 900   4200 13000 0 error (8) .73 64 6.4 0 disqualified .048 9.5 .39 0 timeout (verification) 900    210 12000   0 true 12   580 95 2 error (5) .024 5.5 .16  0 error (5) .025 5.6 .096 0
termination-libowfat/strcasecmp_true-termination.c.i error (134) .26 46 2.1 0 error (1) 5.9 470 57 0 error (42) 880     2200   9800    0 out of memory 260     15000   3000    0 timeout 900   4300 12000 0 true .49 35 6.8 2 unknown .029 4.7 .16 0 unknown .031 4.7 .19  0 timeout 900     1600 9700    0 timeout 900   4200 13000 0 timeout 900    990 5300   0 disqualified .050 9.1 .41 0 timeout (verification) 900    200 9400   0 true 13   580 110 2 error (5) .024 5.6 .12  0 error (5) .024 5.6 .11  0
termination-libowfat/strcat_short_true-termination.c.i error (134) .29 46 1.8 0 error (1) 7.5 680 63 0 error (42) 880     14000   6500    0 error (42) 880     1700   6300    0 timeout 900   4300 12000 0 true .50 36 6.0 2 unknown .053 4.6 .13 0 unknown .054 4.6 .16  0 timeout 900     2300 10000    0 timeout 900   4300 12000 0 timeout 900    1300 10000   0 disqualified .048 9.3 .34 0 timeout (verification) 900    350 13000   0 true 21   740 160 2 error (5) .026 5.6 .17  0 error (5) .029 5.5 .19  0
termination-libowfat/strcat_true-termination.c.i error (134) .26 46 1.9 0 error (1) 7.7 680 63 0 error (42) 880     14000   8100    0 error (42) 880     14000   7800    0 timeout 900   4200 12000 0 true .54 36 8.4 2 unknown .032 4.7 .18 0 unknown .032 4.6 .19  0 timeout 900     2800 9300    0 timeout 910   4300 13000 0 timeout 900    1300 14000   0 disqualified .085 9.0 .36 0 timeout (verification) 900    430 11000   0 error (7) 15   510 110 0 error (5) .027 5.6 .14  0 error (5) .028 5.5 .23  0
termination-libowfat/strchr_short_true-termination.c.i error (134) .26 46 1.9 0 true 13   740 100 2 error (42) 880     2700   7200    0 error (42) 880     390   7700    0 unknown 9.8 520 83 0 true .48 35 6.6 2 unknown .044 4.6 .17 0 unknown .034 4.7 .19  0 timeout 900     1700 12000    0 unknown 9.9 530 89 0 out of memory 89    15000 1100   0 disqualified .049 9.1 .36 0 timeout (verification) 900    490 12000   0 true 11   540 110 2 error (5) .037 5.7 .12  0 error (5) .025 5.5 .16  0
termination-libowfat/strchr_true-termination.c.i error (134) .27 46 1.7 0 true 49   2300 440 2 error (42) 880     1100   7700    0 error (42) 880     340   6600    0 timeout 900   4100 13000 0 true .54 36 6.8 2 unknown .040 5.1 .22 0 unknown .028 4.5 .23  0 timeout 900     1900 12000    0 timeout 900   4100 11000 0 out of memory 89    15000 1200   0 disqualified .043 9.2 .42 0 timeout (verification) 900    430 11000   0 true 20   800 180 2 error (5) .025 5.6 .11  0 error (5) .028 5.6 .23  0
termination-libowfat/strcmp_short_true-termination.c.i error (134) .26 47 2.0 0 true 15   1200 140 2 error (42) 880     6400   8600    0 error (42) 880     370   6700    0 timeout 900   3400 13000 0 true .48 36 6.5 2 unknown .028 4.6 .28 0 unknown .029 4.6 .16  0 timeout 900     3100 10000    0 timeout 900   3300 12000 0 timeout 900    800 5100   0 disqualified .048 9.1 .49 0 timeout (verification) 900    270 12000   0 true 12   510 91 2 error (5) .025 5.6 .091 0 error (5) .024 5.6 .15  0
termination-libowfat/strcpy_small_true-termination.c.i error (134) .27 47 1.9 0 error (1) 15   810 120 0 error (42) 880     14000   4800    0 error (42) 880     14000   6200    0 timeout 900   4200 12000 0 true .49 35 6.2 2 unknown .045 4.8 .19 0 unknown .030 4.8 .19  0 timeout 900     3100 10000    0 timeout 900   4100 13000 0 error (8) .70 64 6.1 0 disqualified .073 9.5 .49 0 timeout (verification) 900    330 11000   0 true 11   500 100 2 error (5) .044 5.6 .14  0 error (5) .021 5.7 .10  0
termination-libowfat/strcspn_true-termination.c.i error (134) .29 46 1.9 0 timeout 910   6400 7000 0 error (42) 880     240   5600    0 error (42) 880     11000   11000    0 true 470   2500 6000 2 true 2.1  57 27   2 unknown .030 4.6 .18 0 unknown .031 4.6 .25  0 timeout 900     810 10000    0 true 570   2400 7400 2 out of memory 72    15000 820   0 disqualified .044 9.2 .48 0 timeout (verification) 900    330 13000   0 true 22   740 190 2 error (5) .024 5.6 .097 0 error (5) .024 5.7 .11  0
termination-libowfat/strdup_true-termination.c.i error (134) .27 47 1.6 0 true 36   2300 350 2 error (42) 880     14000   5900    0 error (42) 880     2600   11000    0 timeout 900   4200 11000 0 true .51 36 6.9 2 unknown .037 4.7 .13 0 unknown .032 4.6 .20  0 timeout 900     1600 9900    0 timeout 920   4300 12000 0 timeout 900    1200 11000   0 disqualified .045 9.2 .36 0 timeout (verification) 900    560 13000   0 true 15   520 140 2 error (5) .027 5.6 .13  0 error (5) .023 5.7 .16  0
termination-libowfat/strlcat_true-termination.c.i error (134) .26 46 2.0 0 error (1) 210   4600 1800 0 error (42) 880     15000   6400    0 error (42) 880     11000   9900    0 error (parsing failed) 1.9 160 16 0 true .53 36 7.2 2 unknown .028 4.6 .13 0 unknown .043 4.6 .15  0 timeout 900     3600 12000    0 error (parsing failed) 1.9 160 16 0 timeout 900    450 4800   0 disqualified .049 9.5 .40 0 timeout (verification) 900    600 11000   0 true 18   540 160 2 error (5) .021 5.6 .16  0 error (5) .024 5.7 .14  0
termination-libowfat/strlcpy_true-termination.c.i error (134) .25 46 2.5 0 error (1) 130   3700 1100 0 error (42) 880     15000   6900    0 error (42) 880     2300   6800    0 error (parsing failed) 2.0 160 18 0 true .52 36 6.3 2 unknown .054 4.7 .18 0 unknown .041 4.6 .19  0 timeout 900     1200 11000    0 error (parsing failed) 1.9 160 18 0 error (8) .70 65 6.1 0 disqualified .046 9.1 .42 0 timeout (verification) 900    600 11000   0 true 19   690 180 2 error (5) .024 5.5 .17  0 error (5) .024 5.8 .098 0
termination-libowfat/strlen_true-termination.c.i error (134) .27 46 1.8 0 true 27   2300 270 2 error (42) 880     5200   3800    0 error (42) 880     340   7700    0 unknown 8.3 480 75 0 true .48 35 6.3 2 unknown .031 4.6 .16 0 unknown .027 4.6 .22  0 timeout 900     2600 10000    0 unknown 8.8 500 78 0 timeout 900    1200 11000   0 disqualified .049 9.3 .43 0 timeout (verification) 900    370 13000   0 true 11   440 91 2 error (5) .024 5.6 .11  0 error (5) .027 5.6 .068 0
termination-libowfat/strpbrk_true-termination.c.i error (134) .26 46 2.9 0 timeout 900   9600 7600 0 error (42) 880     230   4000    0 error (42) 880     11000   10000    0 true 440   2600 6000 2 true 1.8  56 22   2 unknown .055 4.6 .15 0 unknown .037 4.6 .13  0 timeout 900     920 12000    0 true 540   2000 7700 2 out of memory 72    15000 1100   0 disqualified .080 9.3 .33 0 timeout (verification) 900    420 11000   0 unknown 35   1100 260 0 error (5) .021 5.7 .11  0 error (5) .028 5.6 .16  0
termination-libowfat/strrchr_short_true-termination.c.i error (134) .25 46 2.0 0 true 40   2800 260 2 error (42) 880     250   12000    0 out of memory 200     15000   2400    0 unknown 7.9 470 74 0 true .51 35 5.6 2 unknown .040 4.7 .29 0 unknown .035 4.6 .19  0 timeout 900     3200 10000    0 unknown 7.8 470 78 0 out of memory 85    15000 1200   0 disqualified .063 9.1 .37 0 timeout (verification) 900    340 11000   0 true 11   510 100 2 error (5) .031 5.7 .13  0 error (5) .050 5.5 .12  0
termination-libowfat/strrchr_true-termination.c.i error (134) .25 46 2.4 0 timeout 900   2500 12000 0 error (42) 880     540   9200    0 out of memory 170     15000   2000    0 timeout 900   4600 13000 0 true .52 35 6.6 2 unknown .052 4.6 .22 0 unknown .032 4.6 .17  0 timeout 900     2500 8100    0 timeout 900   4000 10000 0 out of memory 86    15000 1300   0 disqualified .046 9.1 .37 0 timeout (verification) 900    520 13000   0 true 14   590 110 2 error (5) .027 5.6 .15  0 error (5) .031 5.6 .21  0
termination-libowfat/strspn_true-termination.c.i error (134) .26 46 2.1 0 true 110   2300 1100 2 error (42) 880     1100   5900    0 out of memory 190     15000   2600    0 timeout 900   3900 13000 0 true .64 36 7.4 2 unknown .029 4.7 .23 0 unknown .029 4.6 .29  0 timeout 900     1900 11000    0 timeout 900   3900 12000 0 timeout 900    720 5900   0 disqualified .043 9.4 .42 0 timeout (verification) 900    410 13000   0 true 19   570 150 2 error (5) .019 5.6 .076 0 error (5) .030 5.7 .20  0
termination-libowfat/strstr_true-termination.c.i error (6) .25 47 1.9 0 true 180   3400 1800 2 error (42) 870     660   10000    0 out of memory 210     15000   3100    0 timeout 900   3800 11000 0 true .95 49 11   2 unknown .030 4.5 .23 0 unknown .028 4.6 .21  0 timeout 900     3900 11000    0 timeout 900   3700 14000 0 timeout 900    1200 12000   0 disqualified .045 9.3 .51 0 timeout (verification) 900    460 13000   0 true 46   1000 420 2 error (5) .029 5.7 .22  0 error (5) .036 5.5 .15  0
termination-libowfat/strtok_r_true-termination.c.i error (134) .27 46 2.0 0 timeout 900   7700 8000 0 error (42) 880     1100   7500    0 out of memory 170     15000   2400    0 unknown 29   1400 240 0 true 2.3  67 29   2 unknown .030 4.7 .14 0 unknown .052 4.7 .13  0 timeout 900     1100 10000    0 timeout 900   4200 11000 0 timeout 900    630 5100   0 disqualified .042 8.8 .39 0 timeout (verification) 900    320 11000   0 true 56   1300 600 2 error (5) .025 5.6 .16  0 error (5) .026 5.7 .15  0
termination-libowfat/strtol_true-termination.c.i error (134) .26 47 2.9 0 timeout 900   160 11000 0 error (42) 880     13000   7300    0 out of memory 840     15000   11000    0 exception 26   1300 210 0 true .57 36 6.9 2 unknown .055 4.6 .18 0 unknown .053 4.6 .16  0 timeout 900     7700 9200    0 exception 26   1300 230 0 timeout 900    5100 12000   0 disqualified .050 9.0 .45 0 true .31 17 4.2 2 true 16   540 140 2 error (5) .023 5.6 .10  0 error (5) .030 5.6 .22  0
termination-libowfat/strtoul_true-termination.c.i error (134) .27 46 1.8 0 timeout 900   150 12000 0 error (42) 880     14000   7500    0 error (42) 880     2800   9300    0 exception 8.3 460 69 0 true .55 35 8.6 2 unknown .038 4.7 .13 0 unknown .041 4.7 .20  0 timeout 900     12000 7500    0 exception 7.9 460 67 0 timeout 900    4200 12000   0 disqualified .046 9.4 .46 0 true .27 18 3.3 2 true 13   500 100 2 error (5) .026 5.6 .15  0 error (5) .029 5.7 .14  0
termination-libowfat/strtoull_true-termination.c.i error (134) .26 47 2.0 0 timeout 900   150 12000 0 error (42) 880     14000   6800    0 error (42) 880     2800   11000    0 exception 8.5 460 70 0 true .54 36 6.6 2 unknown .025 4.7 .38 0 unknown .031 4.8 .18  0 timeout 900     12000 9300    0 exception 8.1 470 66 0 timeout 900    4200 12000   0 disqualified .042 9.5 .41 0 true .28 17 3.3 2 true 11   490 92 2 error (5) .049 5.7 .16  0 error (5) .031 5.6 .24  0
termination-libowfat/wcsrchr_true-termination.c.i error (134) .29 46 2.9 0 out of memory 880   15000 4900 0 error (42) 880     1600   7400    0 out of memory 190     15000   2400    0 unknown 7.9 470 63 0 true .52 35 5.7 2 unknown .052 4.6 .18 0 unknown .030 4.7 .24  0 timeout 900     2900 11000    0 unknown 8.0 360 69 0 timeout 900    480 4200   0 disqualified .045 9.3 .47 0 timeout (verification) 900    50 14000   0 true 11   500 91 2 error (5) .026 5.5 .17  0 error (5) .025 5.6 .13  0
termination-libowfat/wcsstr_true-termination.c.i error (134) .30 46 1.8 0 timeout 910   12000 6300 0 error (42) 880     1100   6400    0 out of memory 200     15000   2400    0 timeout 900   4200 13000 0 true .80 37 9.4 2 unknown .037 4.5 .15 0 unknown .028 4.6 .23  0 timeout 900     4000 9800    0 timeout 900   4100 14000 0 timeout 900    730 5800   0 disqualified .048 9.2 .45 0 error(unknown, verification-finished) 1.7  19 27   0 true 8.4 380 76 2 error (5) .024 5.7 .15  0 error (5) .031 5.6 .14  0
termination-memory-alloca/Urban-2013WST-Fig1-alloca_false-termination.c.i timeout 900    2600 11000   0 false(termination) 6.8 380 55 1 error (42) 880     1700   7900    0 out of memory 160     15000   2000    0 unknown 5.0 280 44 0 true .37 35 4.9 -32 unknown .028 4.6 .26 0 unknown .036 4.7 .20  0 timeout 900     450 12000    0 unknown 5.4 300 46 0 timeout 900    5000 6100   0 disqualified .046 8.9 .59 0 probably out of memory (killed (signal 9, verification)) 110    15000 1600   0 false(termination) 9.1 380 71 1 error (5) .028 5.6 .21  0 error (5) .020 5.6 .29  0
termination-memory-alloca/Velroyen-alloca_false-termination.c.i timeout 900    2300 12000   0 false(termination) 16   550 100 1 error (42) 880     1800   13000    0 error (42) 880     140   11000    0 unknown 6.5 360 58 0 true .36 35 4.4 -32 unknown .032 4.6 .19 0 unknown .048 4.7 .22  0 timeout 900     690 9800    0 unknown 6.6 370 54 0 out of memory 720    15000 9800   0 disqualified .047 9.4 .38 0 timeout (verification) 900    180 10000   0 false(termination) 11   510 91 1 error (5) .026 5.6 .14  0 error (5) .052 5.5 .10  0
termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i out of memory 43    15000 450   0 true 26   2300 210 2 error (42) 880     3400   4200    0 error (42) 880     1300   6600    0 timeout 900   4100 13000 0 true .40 35 4.5 2 unknown .034 4.6 .16 0 unknown .030 4.6 .26  0 timeout 900     500 12000    0 timeout 900   4100 12000 0 timeout 900    440 5000   0 disqualified .046 9.7 .40 0 timeout (verification) 900    440 7400   0 true 18   550 150 2 error (5) .048 5.6 .13  0 error (5) .045 5.6 .13  0
termination-memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-termination.c.i timeout 900    4500 8100   0 true 14   1000 110 2 error (42) 880     990   7100    0 out of memory 370     15000   4500    0 timeout 900   4100 11000 0 true .37 35 4.4 2 unknown .030 4.6 .17 0 unknown .032 4.6 .20  0 timeout 900     210 11000    0 timeout 900   4000 11000 0 timeout 900    240 7000   0 disqualified .046 9.0 .39 0 timeout (verification) 900    430 8500   0 true 25   640 240 2 error (5) .030 5.6 .18  0 error (5) .032 5.5 .11  0
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-termination.c.i out of memory 40    15000 390   0 true 24   1900 160 2 error (42) 880     560   4700    0 out of memory 650     15000   8500    0 timeout 900   4100 12000 0 true .46 35 5.7 2 unknown .036 4.5 .14 0 unknown .027 4.5 .17  0 timeout 900     1500 12000    0 timeout 900   4200 11000 0 timeout 900    370 4200   0 disqualified .048 9.5 .43 0 true .11 15 1.4 2 timeout 900   1500 9500 0 error (5) .024 5.6 .15  0 error (5) .021 5.6 .17  0
termination-memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-termination.c.i timeout 900    3400 11000   0 true 7.6 470 57 2 error (42) 880     4100   3700    0 error (42) 880     340   8000    0 true 410   4200 5100 2 true .35 35 5.0 2 unknown .045 4.6 .18 0 unknown .042 4.6 .20  0 timeout 900     690 12000    0 true 410   4100 5900 2 timeout 900    410 4100   0 disqualified .045 9.3 .35 0 true .11 15 1.5 2 true 10   440 88 2 error (5) .025 5.5 .12  0 error (5) .024 5.6 .19  0
termination-memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-termination.c.i timeout 900    110 2800   0 true 7.9 460 57 2 error (42) 880     3000   3300    0 error (42) 880     500   5700    0 timeout 910   4200 12000 0 true .37 35 5.0 2 unknown .023 4.6 .10 0 unknown .034 4.6 .28  0 timeout 900     340 12000    0 timeout 900   4100 13000 0 timeout 900    7200 3800   0 disqualified .055 9.2 .41 0 timeout (verification) 900    77 11000   0 true 14   590 120 2 error (5) .023 5.7 .10  0 error (5) .025 5.6 .13  0
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-termination.c.i timeout 900    8700 11000   0 true 16   1100 110 2 error (42) 880     1900   9600    0 out of memory 320     15000   4100    0 true 370   4300 4400 2 true .36 35 4.5 2 unknown .027 4.6 .22 0 unknown .029 4.6 .16  0 timeout 900     650 11000    0 true 570   4300 6800 2 timeout 900    380 4400   0 disqualified .046 9.1 .43 0 true .15 15 1.4 2 true 18   690 150 2 error (5) .032 5.7 .081 0 error (5) .027 5.6 .24  0
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-termination.c.i timeout 900    3600 8700   0 true 23   1700 150 2 error (42) 880     980   9700    0 out of memory 380     15000   4200    0 timeout 900   4100 12000 0 true .36 35 4.2 2 unknown .024 4.8 .29 0 unknown .027 4.6 .20  0 timeout 900     710 9600    0 timeout 910   4200 12000 0 timeout 900    410 6200   0 disqualified .044 9.4 .36 0 true .13 16 1.5 2 true 52   790 540 2 error (5) .029 5.7 .15  0 error (5) .049 5.6 .10  0
termination-memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-termination.c.i out of memory 560    15000 6400   0 true 68   5500 480 2 error (42) 880     1300   10000    0 out of memory 240     15000   3300    0 unknown 860   4200 11000 0 true .37 35 4.1 2 unknown .033 4.7 .24 0 unknown .034 4.8 .13  0 timeout 900     880 11000    0 timeout 900   4100 14000 0 timeout 900    370 5900   0 disqualified .048 9.4 .38 0 true .13 16 1.5 2 true 140   1000 1500 2 error (5) .023 5.6 .13  0 error (5) .036 5.5 .20  0
termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i timeout 900    250 6600   0 true 14   760 110 2 error (42) 880     1800   9600    0 out of memory 240     15000   3100    0 timeout 900   4200 11000 0 true .39 35 4.6 2 unknown .031 4.5 .24 0 unknown .035 4.6 .11  0 timeout 900     640 10000    0 timeout 910   4300 11000 0 timeout 900    440 4500   0 disqualified .042 10   .47 0 timeout (verification) 900    64 12000   0 timeout 900   1500 11000 0 error (5) .024 5.6 .12  0 error (5) .039 5.5 .20  0
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i out of memory 37    15000 470   0 true 6.4 450 56 2 true .093 7.4 .93 2 true .095 7.7 .82 2 timeout 900   4100 13000 0 true .38 35 4.3 2 unknown .031 4.6 .26 0 unknown .037 4.6 .19  0 true .095 27 1.1  2 timeout 910   4100 12000 0 true .74 64 7.4 2 disqualified .047 9.4 .53 0 true .15 17 1.7 2 true 27   810 250 2 error (5) .039 5.6 .11  0 error (5) .051 5.5 .12  0
termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i timeout 900    4500 12000   0 true 14   1300 86 2 error (42) 880     1300   7500    0 out of memory 170     15000   2200    0 true 6.4 320 56 2 true .36 35 4.3 2 unknown .032 4.6 .13 0 unknown .031 4.6 .19  0 timeout 900     1200 10000    0 true 6.6 380 53 2 timeout 900    440 5500   0 disqualified .048 9.4 .46 0 timeout (verification) 900    460 6600   0 true 11   400 71 2 error (5) .028 5.6 .21  0 error (5) .024 5.5 .13  0
termination-memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-termination.c.i out of memory 43    15000 340   0 timeout 900   2300 12000 0 error (42) 880     1600   8900    0 out of memory 170     15000   2200    0 timeout 910   4100 9700 0 true .36 35 4.7 2 unknown .030 4.6 .22 0 unknown .032 4.6 .23  0 timeout 900     520 12000    0 timeout 900   4000 11000 0 out of memory 41    15000 670   0 disqualified .045 9.3 .50 0 timeout (verification) 900    130 9800   0 true 15   560 130 2 error (5) .029 5.6 .22  0 error (5) .024 5.6 .094 0
termination-memory-alloca/Masse-alloca_true-termination.c.i timeout 900    140 2700   0 timeout 910   10000 4800 0 error (42) 880     280   9400    0 out of memory 160     15000   2100    0 unknown 5.9 300 60 0 true .39 35 6.7 2 unknown .027 4.6 .27 0 unknown .043 4.6 .24  0 timeout 900     97 11000    0 unknown 6.3 400 57 0 out of memory 120    15000 1800   0 disqualified .049 9.2 .50 0 true 3.2  23 41   2 unknown 18   700 130 0 error (5) .025 5.7 .074 0 error (5) .024 5.8 .058 0
termination-memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-termination.c.i timeout 900    4200 9800   0 true 45   2800 420 2 error (42) 880     640   8400    0 out of memory 160     15000   2200    0 timeout 900   4100 13000 0 true .39 35 6.2 2 unknown .031 4.6 .19 0 unknown .029 4.6 .21  0 timeout 900     400 11000    0 timeout 900   4100 12000 0 out of memory 130    15000 1600   0 disqualified .045 9.5 .40 0 true .13 15 1.1 2 true 45   890 440 2 error (5) .026 5.7 .16  0 error (5) .057 5.6 .10  0
termination-memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-termination.c.i out of memory 32    15000 310   0 true 39   2400 330 2 error (42) 880     1500   8100    0 out of memory 180     15000   2200    0 timeout 900   4100 11000 0 true .43 35 5.1 2 unknown .031 4.8 .13 0 unknown .043 4.6 .17  0 timeout 900     350 12000    0 timeout 910   4200 12000 0 timeout 900    4700 6100   0 disqualified .046 9.2 .42 0 true .11 16 1.2 2 true 680   13000 7700 2 error (5) .024 5.6 .18  0 error (5) .024 5.7 .13  0
termination-memory-alloca/TelAviv-Amir-Minimum-alloca_true-termination.c.i false(termination) .37 49 2.3 -16 out of memory 800   15000 4600 0 error (42) 880     2000   9000    0 out of memory 200     15000   2600    0 true 150   4100 1900 2 true .37 36 4.7 2 unknown .050 4.9 .17 0 unknown .036 4.7 .26  0 timeout 900     360 14000    0 true 160   3400 2100 2 timeout 900    260 7300   0 disqualified .046 9.2 .53 0 true .13 16 1.3 2 timeout 910   14000 5800 0 error (5) .022 5.6 .14  0 error (5) .029 5.6 .095 0
termination-memory-alloca/Toulouse-BranchesToLoop-alloca_true-termination.c.i timeout 900    6600 13000   0 true 9.4 660 70 2 error (42) 880     4400   5800    0 error (42) 880     340   6400    0 timeout 910   4400 12000 0 true .36 36 4.4 2 unknown .028 4.6 .21 0 unknown .054 4.6 .17  0 timeout 900     330 13000    0 timeout 900   4100 14000 0 timeout 900    410 6600   0 disqualified .054 9.2 .38 0 true .92 18 10   2 true 16   670 130 2 error (5) .023 5.6 .094 0 error (5) .023 5.7 .20  0
termination-memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-termination.c.i out of memory 32    15000 270   0 true 11   780 83 2 error (42) 880     4400   6300    0 error (42) 880     370   8200    0 timeout 900   4100 12000 0 true .40 35 4.5 2 unknown .029 4.6 .18 0 unknown .031 4.7 .19  0 timeout 900     340 13000    0 timeout 900   4000 12000 0 timeout 900    420 6400   0 disqualified .049 9.3 .39 0 true .53 20 6.8 2 true 31   750 300 2 error (5) .025 5.6 .076 0 error (5) .024 5.6 .12  0
termination-memory-alloca/Urban-2013WST-Fig2-alloca_true-termination.c.i out of memory 39    15000 470   0 true 8.7 630 63 2 error (42) 880     980   4100    0 error (42) 880     410   6300    0 unknown 880   4200 13000 0 true .36 35 3.9 2 unknown .056 4.6 .23 0 unknown .028 4.6 .28  0 timeout 900     1100 13000    0 timeout 900   4100 12000 0 timeout 900    670 4100   0 disqualified .045 9.6 .41 0 true .11 15 1.3 2 true 21   560 200 2 error (5) .025 5.7 .15  0 error (5) .056 5.6 .14  0
termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i out of memory 38    15000 470   0 true 9.3 640 73 2 error (42) 880     3900   9800    0 error (42) 880     1900   5700    0 out of memory 800   15000 10000 0 true .35 35 4.1 2 unknown .028 4.6 .21 0 unknown .029 4.6 .19  0 timeout 900     4400 10000    0 out of memory 580   15000 6500 0 timeout 900    14000 9400   0 disqualified .047 9.5 .40 0 true .11 15 1.5 2 timeout 900   780 9300 0 error (5) .029 5.6 .12  0 error (5) .022 5.6 .18  0
termination-memory-alloca/Urban-alloca_true-termination.c.i out of memory 39    15000 390   0 true 52   4600 330 2 error (42) 880     3700   9600    0 out of memory 200     15000   2700    0 true 110   4000 1200 2 true .38 36 4.6 2 unknown .028 4.8 .26 0 unknown .027 4.8 .39  0 timeout 900     770 12000    0 true 160   4000 1800 2 timeout 900    390 5500   0 disqualified .046 9.4 .41 0 true .16 16 1.4 2 true 26   660 210 2 error (5) .030 5.6 .21  0 error (5) .021 5.5 .16  0
termination-memory-alloca/a.01-alloca_true-termination_true-no-overflow.c.i out of memory 39    15000 400   0 true 24   2000 190 2 error (42) 880     560   4500    0 out of memory 740     15000   7700    0 timeout 900   4000 12000 0 true .45 35 5.5 2 unknown .029 4.6 .22 0 unknown .029 4.6 .16  0 timeout 900     1400 8700    0 timeout 900   4000 12000 0 timeout 900    460 4500   0 disqualified .056 9.3 .38 0 timeout (verification) 900    460 7800   0 true 30   820 290 2 error (5) .024 5.6 .22  0 error (5) .028 5.7 .17  0
termination-memory-alloca/a.04-alloca_true-termination_true-no-overflow.c.i timeout 900    2800 11000   0 true 6.9 440 51 2 error (42) 880     5000   3700    0 error (42) 880     370   6300    0 timeout 910   4200 14000 0 true .36 35 4.7 2 unknown .048 4.6 .26 0 unknown .032 4.6 .20  0 timeout 900     310 11000    0 timeout 920   4300 12000 0 timeout 900    420 3700   0 disqualified .045 9.3 .52 0 true .15 16 1.5 2 true 11   540 88 2 error (5) .025 5.5 .094 0 error (5) .029 5.6 .13  0
termination-memory-alloca/a.05-alloca_true-termination_true-no-overflow.c.i timeout 900    4300 10000   0 true 7.0 450 56 2 error (42) 880     5300   5900    0 error (42) 880     410   6900    0 timeout 910   4500 12000 0 true .42 35 3.9 2 unknown .048 4.7 .23 0 unknown .032 4.6 .18  0 timeout 900     340 11000    0 timeout 900   4100 14000 0 timeout 900    370 3400   0 disqualified .045 9.6 .43 0 timeout (verification) 900    550 6900   0 true 11   490 94 2 error (5) .020 5.6 .16  0 error (5) .032 5.6 .20  0
termination-memory-alloca/a.06-alloca_true-termination_true-no-overflow.c.i timeout 900    15000 10000   0 true 390   2500 4500 2 error (42) 880     1600   9700    0 out of memory 340     15000   3800    0 timeout 910   4500 13000 0 true .44 35 4.8 2 unknown .031 4.6 .18 0 unknown .037 4.7 .18  0 timeout 900     330 12000    0 timeout 900   4000 12000 0 timeout 900    400 3900   0 disqualified .048 9.2 .39 0 timeout (verification) 900    370 6800   0 true 23   750 200 2 error (5) .050 5.5 .12  0 error (5) .024 5.6 .11  0
termination-memory-alloca/a.07-alloca_true-termination_true-no-overflow.c.i timeout 900    5100 9400   0 true 11   730 84 2 error (42) 880     4000   5700    0 error (42) 880     400   8900    0 timeout 910   4200 13000 0 true .38 35 4.6 2 unknown .055 4.6 .15 0 unknown .043 4.7 .16  0 timeout 900     400 11000    0 timeout 900   4100 14000 0 timeout 900    430 4100   0 disqualified .050 9.5 .34 0 timeout (verification) 900    370 8600   0 true 14   560 140 2 error (5) .023 5.6 .16  0 error (5) .023 5.6 .084 0
termination-memory-alloca/a.08-alloca_true-termination_true-no-overflow.c.i timeout 900    6600 12000   0 true 7.8 490 61 2 error (42) 880     4900   6600    0 error (42) 880     400   8300    0 timeout 900   4100 13000 0 true .37 35 5.9 2 unknown .048 4.8 .20 0 unknown .033 4.6 .24  0 timeout 900     330 12000    0 timeout 900   4000 12000 0 timeout 900    420 4500   0 disqualified .047 9.3 .47 0 timeout (verification) 900    560 6300   0 true 12   520 92 2 error (5) .021 5.7 .18  0 error (5) .023 5.7 .11  0
termination-memory-alloca/a.09_assume-alloca_true-termination_true-no-overflow.c.i timeout 900    370 12000   0 true 15   830 110 2 error (42) 880     720   9600    0 error (42) 880     350   8200    0 timeout 920   4300 12000 0 true .38 36 4.3 2 unknown .029 4.6 .22 0 unknown .024 4.8 .21  0 timeout 900     320 11000    0 timeout 900   4100 11000 0 out of memory 300    15000 2300   0 disqualified .046 9.0 .38 0 timeout (verification) 900    280 7400   0 true 13   500 110 2 error (5) .027 5.6 .11  0 error (5) .027 5.6 .089 0
termination-memory-alloca/a.10-alloca_true-termination_true-no-overflow.c.i timeout 900    4500 10000   0 true 3.4 260 29 2 error (42) 880     1700   9800    0 out of memory 200     15000   2400    0 timeout 910   4300 11000 0 true .39 35 6.5 2 unknown .027 4.6 .23 0 unknown .028 4.6 .18  0 timeout 900     340 12000    0 timeout 900   4100 12000 0 timeout 900    360 3900   0 disqualified .047 9.6 .42 0 timeout (verification) 900    96 9000   0 true 18   710 160 2 error (5) .030 5.5 .062 0 error (5) .025 5.6 .11  0
termination-memory-alloca/add_last-alloca_true-termination.c.i error (134) .27 46 2.9 0 error (1) 16   850 130 0 error (42) 870     13000   7000    0 error (42) 880     14000   6400    0 true 11   390 100 2 true .54 36 6.1 2 unknown .029 4.6 .14 0 unknown .028 4.7 .17  0 timeout 900     970 13000    0 timeout 900   710 10000 0 timeout 900    1900 8100   0 disqualified .051 9.7 .39 0 true .14 18 1.6 2 true 11   470 89 2 error (5) .025 5.6 .14  0 error (5) .025 5.7 .20  0
termination-memory-alloca/array01-alloca_true-termination.c.i error (134) .29 46 1.7 0 true 62   3400 470 2 error (42) 880     14000   6300    0 out of memory 650     15000   7400    0 unknown 8.2 480 73 0 true 1.8  50 24   2 unknown .030 4.8 .19 0 unknown .029 4.6 .18  0 timeout 900     610 13000    0 unknown 9.0 470 72 0 timeout 900    430 5000   0 disqualified .048 9.3 .36 0 timeout (verification) 900    1200 11000   0 true 15   560 100 2 error (5) .024 5.6 .13  0 error (5) .027 5.6 .088 0
termination-memory-alloca/array02-alloca_true-termination.c.i error (134) .26 46 1.8 0 true 120   2800 1200 2 error (42) 880     13000   6200    0 out of memory 110     15000   1300    0 unknown 22   940 190 0 true 4.5  76 61   2 unknown .029 4.6 .17 0 unknown .052 4.6 .20  0 timeout 900     330 13000    0 unknown 27   1000 240 0 timeout 900    410 5300   0 disqualified .067 9.3 .40 0 probably out of memory (killed (signal 9, verification)) 770    15000 12000   0 true 17   560 140 2 error (5) .023 5.7 .16  0 error (5) .020 5.7 .22  0
termination-memory-alloca/array03-alloca_true-termination.c.i error (134) .28 46 1.9 0 true 130   3800 1200 2 error (42) 880     14000   5800    0 out of memory 120     15000   1700    0 true 4.4 260 37 2 true 2.0  55 27   2 unknown .031 4.6 .20 0 unknown .033 4.6 .26  0 timeout 900     1800 11000    0 true 4.3 270 41 2 timeout 900    2300 5200   0 disqualified .046 9.5 .49 0 timeout (verification) 900    1200 14000   0 true 17   600 150 2 error (5) .025 5.6 .10  0 error (5) .027 5.6 .13  0
termination-memory-alloca/aviad_true-alloca_true-termination.c.i timeout 900    150 2400   0 true 48   3300 350 2 true 2.6   120   33    2 out of memory 200     15000   2600    0 timeout 900   4200 15000 0 true .38 35 4.9 2 unknown .025 4.6 .15 0 unknown .029 4.6 .20  0 true 4.4   30 50    2 timeout 900   4100 13000 0 out of memory 54    15000 750   0 disqualified .045 8.9 .43 0 timeout (verification) 900    400 14000   0 true 14   590 120 2 error (5) .044 5.6 .10  0 error (5) .037 5.4 .13  0
termination-memory-alloca/b.01-alloca_true-termination_true-no-overflow.c.i timeout 900    2800 14000   0 true 6.5 440 52 2 error (42) 880     5200   3800    0 error (42) 880     370   6400    0 timeout 910   4200 13000 0 true .37 35 5.4 2 unknown .033 4.8 .21 0 unknown .055 4.6 .14  0 timeout 900     350 12000    0 timeout 900   4100 11000 0 timeout 900    410 4100   0 disqualified .048 9.6 .37 0 true .15 16 1.2 2 true 11   490 83 2 error (5) .030 5.6 .11  0 error (5) .025 5.6 .15  0
termination-memory-alloca/b.02-alloca_true-termination_true-no-overflow.c.i timeout 900    4400 9700   0 true 7.5 450 66 2 error (42) 880     4400   5600    0 error (42) 880     420   6800    0 timeout 910   4400 13000 0 true .37 35 4.9 2 unknown .029 4.6 .15 0 unknown .028 4.6 .18  0 timeout 900     320 13000    0 timeout 900   4100 13000 0 timeout 900    520 6000   0 disqualified .046 9.4 .51 0 timeout (verification) 900    480 6000   0 true 11   550 100 2 error (5) .021 5.6 .16  0 error (5) .049 5.7 .11  0
termination-memory-alloca/b.03-no-inv_assume-alloca_true-termination_true-no-overflow.c.i timeout 900    330 12000   0 true 12   780 100 2 error (42) 880     4900   7300    0 error (42) 880     410   7200    0 unknown 57   2900 520 0 true .38 35 4.5 2 unknown .028 4.6 .20 0 unknown .032 4.6 .31  0 timeout 900     180 10000    0 unknown 57   3500 580 0 timeout 900    4800 7100   0 disqualified .058 9.5 .48 0 timeout (verification) 900    110 11000   0 true 12   550 94 2 error (5) .029 5.5 .13  0 error (5) .027 5.8 .17  0
termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i timeout 900    380 9700   0 true 13   750 100 2 error (42) 880     710   9500    0 error (42) 880     320   11000    0 unknown 54   2900 510 0 true .38 35 4.3 2 unknown .051 4.7 .18 0 unknown .030 4.6 .18  0 timeout 900     290 13000    0 unknown 51   3700 490 0 out of memory 420    15000 2400   0 disqualified .047 9.5 .42 0 timeout (verification) 900    110 11000   0 true 12   540 99 2 error (5) .030 5.6 .14  0 error (5) .025 5.6 .16  0
termination-memory-alloca/b.04-alloca_true-termination_true-no-overflow.c.i true .49 57 3.9 2 true 3.8 260 32 2 true .084 7.0 .64 2 true .087 8.0 .71 2 timeout 910   4400 11000 0 true .36 35 4.5 2 unknown .031 4.6 .18 0 unknown .034 4.7 .19  0 true .12  26 .84 2 timeout 900   4100 13000 0 true .72 64 5.9 2 disqualified .046 9.2 .48 0 true .15 17 1.7 2 true 11   480 99 2 error (5) .029 5.6 .17  0 error (5) .027 5.5 .12  0
termination-memory-alloca/b.05-alloca_true-termination_true-no-overflow.c.i timeout 900    8700 11000   0 true 8.1 560 62 2 error (42) 880     930   9100    0 error (42) 880     450   7700    0 timeout 900   3900 12000 0 true .36 35 5.1 2 unknown .050 4.6 .17 0 unknown .029 4.6 .19  0 timeout 900     850 9700    0 timeout 900   3900 13000 0 timeout 900    340 4500   0 disqualified .049 9.4 .40 0 timeout (verification) 900    560 11000   0 true 12   580 99 2 error (5) .025 5.6 .14  0 error (5) .026 5.6 .16  0
termination-memory-alloca/b.06-alloca_true-termination_true-no-overflow.c.i timeout 900    5200 9900   0 true 17   1300 130 2 error (42) 880     4000   5700    0 error (42) 880     360   5900    0 timeout 900   4100 13000 0 true .36 35 4.5 2 unknown .029 4.8 .19 0 unknown .028 4.6 .20  0 timeout 900     720 12000    0 timeout 920   4300 13000 0 timeout 900    420 5100   0 disqualified .045 9.0 .40 0 timeout (verification) 900    530 6400   0 true 12   590 110 2 error (5) .029 5.6 .21  0 error (5) .030 5.6 .13  0
termination-memory-alloca/b.07-alloca_true-termination_true-no-overflow.c.i timeout 900    6200 11000   0 true 11   750 95 2 error (42) 880     4200   6400    0 error (42) 880     390   7400    0 timeout 900   4100 13000 0 true .40 35 5.6 2 unknown .031 4.7 .22 0 unknown .032 4.7 .23  0 timeout 900     440 11000    0 timeout 910   4100 12000 0 timeout 900    440 4700   0 disqualified .048 9.1 .38 0 timeout (verification) 900    460 5400   0 true 14   520 110 2 error (5) .029 5.9 .13  0 error (5) .026 5.6 .16  0
termination-memory-alloca/b.09-no-inv_assume-alloca_true-termination_true-no-overflow.c.i timeout 900    4100 11000   0 true 3.7 270 34 2 error (42) 880     1700   9200    0 out of memory 210     15000   2700    0 timeout 900   4000 13000 0 true .36 35 4.3 2 unknown .031 4.8 .14 0 unknown .056 4.6 .22  0 timeout 900     620 12000    0 timeout 910   4100 13000 0 out of memory 99    15000 950   0 disqualified .045 9.4 .43 0 timeout (verification) 900    240 7700   0 unknown 39   1700 340 0 error (5) .028 5.6 .12  0 error (5) .029 5.6 .17  0
termination-memory-alloca/b.09_assume-alloca_true-termination_true-no-overflow.c.i timeout 900    5100 12000   0 true 3.8 330 35 2 error (42) 880     150   10000    0 out of memory 250     15000   3600    0 timeout 900   4000 11000 0 true .40 35 4.7 2 unknown .028 4.7 .19 0 unknown .037 4.8 .23  0 timeout 900     760 11000    0 timeout 900   4000 12000 0 out of memory 69    15000 920   0 disqualified .046 9.4 .45 0 timeout (verification) 900    390 11000   0 true 26   760 230 2 error (5) .031 5.6 .23  0 error (5) .037 5.7 .14  0
termination-memory-alloca/b.10-alloca_true-termination_true-no-overflow.c.i timeout 900    7100 8000   0 true 28   1600 220 2 error (42) 880     1400   7800    0 out of memory 150     15000   1800    0 timeout 910   4300 14000 0 true .42 35 5.8 2 unknown .028 4.8 .21 0 unknown .055 4.6 .16  0 timeout 900     410 13000    0 timeout 920   4200 14000 0 timeout 900    420 4300   0 disqualified .045 9.0 .49 0 timeout (verification) 900    180 6400   0 true 18   660 160 2 error (5) .024 5.6 .10  0 error (5) .027 5.6 .095 0
termination-memory-alloca/b.11-alloca_true-termination_true-no-overflow.c.i error (139) .41 84 3.8 0 error (1) 7.0 470 69 0 error (42) 880     360   12000    0 out of memory 150     15000   1900    0 timeout 910   4300 11000 0 true .43 35 6.3 2 unknown .033 4.6 .16 0 unknown .027 4.6 .24  0 timeout 900     430 10000    0 timeout 910   4100 11000 0 timeout 900    420 4100   0 disqualified .069 9.2 .42 0 timeout (verification) 900    180 7700   0 true 25   750 220 2 error (5) .028 5.7 .094 0 error (5) .022 5.6 .17  0
termination-memory-alloca/b.12-alloca_true-termination_true-no-overflow.c.i timeout 900    4500 11000   0 true 16   810 120 2 error (42) 880     380   11000    0 out of memory 240     15000   3700    0 timeout 900   4100 11000 0 true .39 35 4.8 2 unknown .027 4.6 .20 0 unknown .047 4.7 .14  0 timeout 900     580 12000    0 timeout 900   4100 12000 0 out of memory 39    15000 570   0 disqualified .047 9.2 .40 0 timeout (verification) 900    440 7700   0 true 18   550 160 2 error (5) .025 5.6 .14  0 error (5) .024 5.6 .12  0
termination-memory-alloca/b.13-alloca_true-termination_true-no-overflow.c.i timeout 900    4500 10000   0 true 20   1200 140 2 error (42) 880     420   11000    0 out of memory 270     15000   3300    0 timeout 900   4100 11000 0 true .43 35 6.2 2 unknown .027 4.6 .23 0 unknown .042 4.7 .18  0 timeout 900     590 11000    0 timeout 900   4100 12000 0 out of memory 78    15000 1100   0 disqualified .046 9.3 .42 0 timeout (verification) 900    430 7600   0 true 22   630 180 2 error (5) .024 5.7 .11  0 error (5) .032 5.7 .20  0
termination-memory-alloca/b.14-alloca_true-termination_true-no-overflow.c.i error (139) .40 84 4.2 0 true 14   1100 120 2 error (42) 880     1100   4800    0 error (42) 880     11000   9300    0 timeout 900   4000 12000 0 true .80 35 10   2 unknown .035 4.6 .40 0 unknown .028 4.6 .17  0 timeout 900     860 14000    0 timeout 900   4000 14000 0 timeout 900    460 3800   0 disqualified .044 9.6 .45 0 timeout (verification) 900    460 6600   0 true 27   720 250 2 error (5) .023 5.6 .17  0 error (5) .031 5.6 .24  0
termination-memory-alloca/b.15-alloca_true-termination_true-no-overflow.c.i error (139) .40 84 4.4 0 true 9.1 660 71 2 error (42) 870     870   4900    0 error (42) 880     12000   9600    0 timeout 910   4000 11000 0 true .80 35 10   2 unknown .051 4.6 .16 0 unknown .037 4.7 .19  0 timeout 900     960 9800    0 timeout 910   4100 12000 0 timeout 900    500 4100   0 disqualified .043 9.1 .42 0 true .24 18 2.9 2 true 27   610 260 2 error (5) .031 5.7 .17  0 error (5) .023 5.7 .17  0
termination-memory-alloca/b.16-alloca_true-termination_true-no-overflow.c.i out of memory 40    15000 370   0 true 16   910 120 2 error (42) 880     570   5000    0 out of memory 730     15000   6200    0 timeout 900   4200 11000 0 true .62 35 7.0 2 unknown .033 4.7 .22 0 unknown .038 4.6 .18  0 timeout 900     810 11000    0 timeout 920   4500 13000 0 timeout 900    410 4100   0 disqualified .048 8.9 .39 0 timeout (verification) 900    490 9600   0 true 15   520 120 2 error (5) .027 5.6 .15  0 error (5) .047 5.6 .11  0
termination-memory-alloca/b.17-alloca_true-termination_true-no-overflow.c.i out of memory 39    15000 390   0 true 15   980 110 2 error (42) 880     570   7500    0 out of memory 860     15000   9900    0 timeout 900   4000 12000 0 true .66 35 8.3 2 unknown .042 4.6 .22 0 unknown .049 4.7 .25  0 timeout 900     1100 10000    0 timeout 900   4100 12000 0 timeout 900    420 3700   0 disqualified .072 9.5 .40 0 timeout (verification) 900    480 6700   0 true 22   750 170 2 error (5) .031 5.7 .21  0 error (5) .025 5.6 .13  0
termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i out of memory 38    15000 480   0 true 10   670 92 2 error (42) 880     1200   5300    0 out of memory 140     15000   1700    0 true 490   4700 5900 2 true 1.3  35 19   2 unknown .047 4.6 .17 0 unknown .030 4.6 .17  0 timeout 900     1000 12000    0 true 510   4700 7700 2 timeout 900    390 4300   0 disqualified .050 9.2 .35 0 timeout (verification) 900    390 7400   0 true 21   750 170 2 error (5) .027 5.6 .15  0 error (5) .036 5.5 .13  0
termination-memory-alloca/bubblesort-alloca_true-termination.c.i error (134) .27 46 2.5 0 timeout 910   11000 5600 0 error (42) 880     13000   6600    0 out of memory 110     15000   1500    0 true 7.3 450 72 2 true 1.6  73 20   2 unknown .027 4.5 .19 0 unknown .060 4.7 .18  0 timeout 900     7300 9800    0 true 7.7 460 73 2 timeout 900    940 6400   0 disqualified .050 9.2 .35 0 timeout (verification) 900    1800 12000   0 true 16   630 130 2 error (5) .025 5.6 .13  0 error (5) .027 5.6 .12  0
termination-memory-alloca/c.01-no-inv-alloca_true-termination_true-no-overflow.c.i out of memory 70    15000 730   0 true 30   2400 210 2 error (42) 880     2100   13000    0 out of memory 750     15000   8200    0 timeout 900   4100 11000 0 true .49 35 5.7 2 unknown .055 4.6 .14 0 unknown .031 4.6 .18  0 timeout 900     2000 12000    0 timeout 900   4100 12000 0 timeout 900    500 8200   0 disqualified .045 9.1 .36 0 timeout (verification) 900    310 11000   0 timeout 900   750 12000 0 error (5) .033 5.6 .18  0 error (5) .027 5.5 .25  0
termination-memory-alloca/c.01_assume-alloca_true-termination_true-no-overflow.c.i out of memory 70    15000 870   0 true 33   2600 250 2 error (42) 880     2200   11000    0 out of memory 690     15000   7800    0 timeout 900   4300 14000 0 true .48 35 6.8 2 unknown .033 4.6 .21 0 unknown .030 4.6 .23  0 timeout 900     1900 10000    0 timeout 900   4200 13000 0 timeout 900    480 4800   0 disqualified .048 9.2 .43 0 timeout (verification) 900    300 14000   0 true 38   680 430 2 error (5) .024 5.6 .12  0 error (5) .025 5.6 .21  0
termination-memory-alloca/c.02-alloca_true-termination_true-no-overflow.c.i out of memory 39    15000 380   0 true 24   2100 170 2 error (42) 880     590   5400    0 error (42) 880     10000   9400    0 timeout 900   3900 12000 0 true .47 35 6.1 2 unknown .030 4.6 .21 0 unknown .036 4.6 .20  0 timeout 900     1400 9900    0 timeout 900   3900 13000 0 timeout 900    460 5900   0 disqualified .046 9.2 .44 0 timeout (verification) 900    470 7800   0 timeout 900   990 11000 0 error (5) .027 5.6 .17  0 error (5) .020 5.6 .19  0
termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i timeout 900    6600 11000   0 true 25   1700 180 2 error (42) 880     2000   9800    0 out of memory 270     15000   3100    0 timeout 900   4100 11000 0 true .38 36 4.4 2 unknown .051 4.7 .15 0 unknown .031 4.6 .18  0 timeout 900     360 11000    0 timeout 900   4100 12000 0 timeout 900    360 5000   0 disqualified .070 9.5 .39 0 timeout (verification) 900    170 11000   0 true 20   740 190 2 error (5) .049 5.6 .11  0 error (5) .023 5.7 .14  0
termination-memory-alloca/c.07-alloca_true-termination_true-no-overflow.c.i timeout 900    10000 11000   0 true 15   1200 120 2 error (42) 880     1800   11000    0 error (42) 880     610   7000    0 timeout 900   4100 13000 0 true .39 35 5.3 2 unknown .027 4.6 .29 0 unknown .040 4.6 .15  0 timeout 900     640 11000    0 timeout 900   4000 12000 0 timeout 900    460 6200   0 disqualified .042 9.4 .42 0 timeout (verification) 900    620 8500   0 true 15   600 120 2 error (5) .024 5.7 .10  0 error (5) .025 5.7 .14  0
termination-memory-alloca/c.08-alloca_true-termination_true-no-overflow.c.i out of memory 39    15000 460   0 true 22   2100 170 2 error (42) 870     560   4600    0 out of memory 750     15000   8500    0 timeout 900   4100 12000 0 true .46 35 6.2 2 unknown .031 4.6 .19 0 unknown .059 4.6 .23  0 timeout 900     1500 8400    0 timeout 900   4000 12000 0 timeout 900    330 4500   0 disqualified .071 9.7 .36 0 timeout (verification) 900    530 8400   0 timeout 900   1000 13000 0 error (5) .029 5.6 .23  0 error (5) .023 5.7 .13  0
termination-memory-alloca/count_down-alloca_true-termination.c.i error (134) .26 46 1.8 0 true 110   3400 950 2 error (42) 880     14000   6300    0 out of memory 140     15000   1700    0 unknown 19   620 170 0 true 1.9  50 19   2 unknown .027 4.7 .18 0 unknown .031 4.7 .17  0 timeout 900     390 13000    0 unknown 19   820 170 0 timeout 900    750 9200   0 disqualified .047 9.0 .33 0 timeout (verification) 900    1400 14000   0 true 17   520 130 2 error (5) .025 5.5 .15  0 error (5) .045 5.7 .20  0
termination-memory-alloca/cstrcat-alloca_true-termination.c.i error (134) .26 46 2.0 0 error (1) 75   2900 550 0 error (42) 880     14000   5800    0 error (42) 880     4100   9000    0 timeout 900   4100 12000 0 true .51 36 6.0 2 unknown .028 4.6 .15 0 unknown .054 4.6 .16  0 timeout 900     2000 11000    0 timeout 900   4100 12000 0 timeout 900    10000 12000   0 disqualified .049 9.5 .37 0 timeout (verification) 900    280 14000   0 true 12   560 90 2 error (5) .031 5.6 .27  0 error (5) .029 5.6 .13  0
termination-memory-alloca/cstrchr-alloca_true-termination.c.i error (134) .27 46 2.5 0 true 11   730 94 2 error (42) 870     5700   6700    0 error (42) 880     370   6400    0 unknown 34   1300 280 0 true .47 35 6.3 2 unknown .026 4.6 .23 0 unknown .027 4.6 .19  0 timeout 900     1200 14000    0 unknown 31   1400 260 0 timeout 900    640 6600   0 disqualified .045 9.4 .51 0 timeout (verification) 900    460 11000   0 true 12   560 98 2 error (5) .026 5.6 .13  0 error (5) .028 5.7 .17  0
termination-memory-alloca/cstrcmp-alloca_true-termination.c.i error (134) .26 46 1.5 0 true 21   1400 170 2 error (42) 880     5000   5900    0 error (42) 880     340   6600    0 timeout 900   3000 12000 0 true .48 36 6.6 2 unknown .026 4.7 .28 0 unknown .028 4.6 .17  0 timeout 900     2900 11000    0 timeout 900   3200 12000 0 timeout 900    850 6300   0 disqualified .044 9.3 .38 0 timeout (verification) 900    240 12000   0 true 12   570 99 2 error (5) .027 5.5 .21  0 error (5) .037 5.7 .15  0
termination-memory-alloca/cstrcpy-alloca_true-termination.c.i error (134) .27 46 1.8 0 true 96   2300 1300 2 error (42) 880     14000   4300    0 error (42) 880     14000   4600    0 timeout 900   4400 12000 0 true .49 36 6.2 2 unknown .028 4.7 .18 0 unknown .052 4.6 .16  0 timeout 900     3000 10000    0 timeout 900   4200 12000 0 error (8) .76 65 4.8 0 disqualified .047 9.5 .44 0 timeout (verification) 900    210 14000   0 true 13   550 100 2 error (5) .025 5.7 .10  0 error (5) .024 5.6 .11  0
termination-memory-alloca/cstrcspn-alloca_true-termination.c.i error (134) .27 47 1.9 0 true 72   4700 610 2 error (42) 880     990   5500    0 out of memory 200     15000   2200    0 timeout 900   3700 15000 0 true .67 36 7.8 2 unknown .056 4.7 .25 0 unknown .027 4.6 .20  0 timeout 900     1500 13000    0 timeout 900   3700 13000 0 timeout 900    610 4500   0 disqualified .046 9.5 .58 0 timeout (verification) 900    480 11000   0 true 110   1300 1400 2 error (5) .028 5.5 .14  0 error (5) .026 5.6 .090 0
termination-memory-alloca/cstrlen-alloca_true-termination.c.i error (134) .26 46 1.8 0 true 8.3 570 73 2 error (42) 880     6800   4900    0 error (42) 880     340   5200    0 unknown 26   1100 230 0 true .47 36 6.1 2 unknown .034 4.6 .19 0 unknown .028 4.6 .21  0 timeout 900     2100 13000    0 unknown 20   800 190 0 timeout 900    1100 12000   0 disqualified .049 9.1 .38 0 timeout (verification) 900    340 12000   0 true 11   450 83 2 error (5) .021 5.6 .19  0 error (5) .044 5.5 .12  0
termination-memory-alloca/cstrncat-alloca_true-termination.c.i error (134) .25 46 2.4 0 error (1) 95   3800 710 0 error (42) 880     14000   8700    0 error (42) 870     2400   7000    0 timeout 900   4200 13000 0 true .52 35 6.8 2 unknown .028 4.7 .23 0 unknown .030 4.8 .18  0 timeout 900     2200 9800    0 timeout 900   4300 14000 0 timeout 900    1100 10000   0 disqualified .045 9.5 .46 0 timeout (verification) 900    290 13000   0 true 13   520 93 2 error (5) .024 5.6 .12  0 error (5) .028 5.6 .20  0
termination-memory-alloca/cstrncmp-alloca_true-termination.c.i error (134) .25 46 2.0 0 true 25   2300 230 2 error (42) 880     1100   8800    0 error (42) 880     270   8200    0 timeout 900   3200 11000 0 true .50 36 6.3 2 unknown .056 4.6 .22 0 unknown .052 4.6 .17  0 timeout 900     1600 11000    0 timeout 900   2900 12000 0 out of memory 74    15000 860   0 disqualified .046 9.3 .40 0 timeout (verification) 900    220 14000   0 true 13   550 110 2 error (5) .024 5.6 .13  0 error (5) .030 5.9 .16  0
termination-memory-alloca/cstrncpy-alloca_true-termination.c.i error (134) .24 46 2.5 0 timeout 900   5200 9200 0 error (42) 880     14000   10000    0 error (42) 880     5200   6900    0 true 790   4800 9300 2 true .73 38 9.0 2 unknown .030 4.6 .21 0 unknown .029 4.7 .14  0 timeout 900     6600 11000    0 true 860   4500 11000 2 error (8) .76 65 6.7 0 disqualified .047 9.6 .43 0 timeout (verification) 900    1300 12000   0 true 16   670 160 2 error (5) .025 5.7 .15  0 error (5) .023 5.6 .15  0
termination-memory-alloca/cstrpbrk-alloca_true-termination.c.i error (134) .26 46 1.9 0 true 47   4600 400 2 error (42) 880     990   6300    0 out of memory 190     15000   2500    0 timeout 900   3700 13000 0 true .65 35 11   2 unknown .029 4.7 .18 0 unknown .047 4.6 .26  0 timeout 900     1900 8900    0 timeout 900   3700 14000 0 timeout 900    610 5200   0 disqualified .044 9.1 .42 0 timeout (verification) 900    520 12000   0 true 32   1100 310 2 error (5) .055 5.5 .18  0 error (5) .024 5.6 .095 0
termination-memory-alloca/cstrspn-alloca_true-termination.c.i error (134) .26 46 1.9 0 true 50   4500 420 2 error (42) 870     990   5600    0 out of memory 200     15000   2700    0 timeout 900   3700 11000 0 true .70 36 9.3 2 unknown .030 4.6 .17 0 unknown .056 4.6 .16  0 timeout 900     1800 8600    0 timeout 900   3700 13000 0 timeout 900    610 5900   0 disqualified .049 9.5 .37 0 timeout (verification) 900    520 11000   0 true 22   670 230 2 error (5) .030 5.7 .11  0 error (5) .024 5.5 .13  0
termination-memory-alloca/diff-alloca_true-termination.c.i error (134) .28 46 1.6 0 true 52   3600 520 2 error (42) 880     12000   5600    0 out of memory 200     15000   2300    0 true 44   940 460 2 true 1.0  44 14   2 unknown .038 4.6 .25 0 unknown .059 4.6 .23  0 timeout 900     260 13000    0 true 16   660 130 2 timeout 900    600 6600   0 disqualified .052 9.5 .40 0 timeout (verification) 900    1100 12000   0 true 19   570 160 2 error (5) .024 5.5 .13  0 error (5) .049 5.5 .098 0
termination-memory-alloca/easySum-alloca_true-termination.c.i timeout 900    3400 10000   0 true 51   2300 580 2 error (42) 880     4400   4200    0 error (42) 880     320   6100    0 timeout 900   4200 14000 0 true .35 35 4.3 2 unknown .028 4.6 .24 0 unknown .046 4.6 .18  0 timeout 900     1100 11000    0 timeout 920   4200 14000 0 timeout 900    440 5000   0 disqualified .048 9.3 .35 0 true .13 16 1.4 2 true 12   570 93 2 error (5) .025 5.6 .11  0 error (5) .050 5.6 .18  0
termination-memory-alloca/ex1-alloca_true-termination.c.i timeout 900    280 8100   0 true 8.3 540 68 2 error (42) 880     3600   3700    0 error (42) 880     2600   6500    0 exception 3.9 260 38 0 true .35 35 4.4 2 unknown .031 4.6 .22 0 unknown .030 4.6 .18  0 timeout 900     630 11000    0 exception 4.2 290 37 0 timeout 900    1900 6400   0 disqualified .043 9.2 .40 0 timeout (verification) 900    470 7000   0 true 13   570 110 2 error (5) .025 5.7 .16  0 error (5) .022 5.6 .16  0
termination-memory-alloca/ex2-alloca_true-termination.c.i out of memory 96    15000 1100   0 timeout 910   8600 5100 0 error (42) 880     560   5500    0 out of memory 220     15000   3100    0 timeout 900   4100 13000 0 true .63 37 7.8 2 unknown .031 4.6 .15 0 unknown .030 4.6 .16  0 timeout 900     220 10000    0 timeout 910   4100 11000 0 timeout 900    1300 8500   0 disqualified .046 9.6 .56 0 timeout (verification) 900    160 6600   0 unknown 45   1200 390 0 error (5) .022 5.7 .13  0 error (5) .043 5.5 .14  0
termination-memory-alloca/ex3a-alloca_true-termination_true-no-overflow.c.i timeout 900    100 5800   0 true 10   700 76 2 true .17  11   1.4  2 true .16  11   2.1  2 exception 3.8 260 37 0 true .35 35 4.1 2 unknown .028 4.6 .22 0 unknown .044 4.6 .13  0 true .12  27 .87 2 exception 3.9 290 35 0 true .74 65 6.9 2 disqualified .050 9.2 .40 0 true .28 30 3.7 2 unknown 25   650 200 0 error (5) .024 5.6 .19  0 error (5) .026 5.6 .11  0
termination-memory-alloca/ex3b-alloca_true-termination.c.i timeout 900    100 9200   0 true 16   1100 140 2 true 8.2   56   110    2 true 7.7   56   92    2 exception 3.8 260 35 0 true .48 35 7.2 2 unknown .055 4.6 .13 0 unknown .029 4.6 .24  0 true 120     47 2000    2 exception 4.3 290 39 0 true 110    920 1600   2 disqualified .048 9.5 .43 0 timeout (verification) 900    1100 6800   0 unknown 30   860 240 0 error (5) .031 5.7 .17  0 error (5) .025 5.6 .11  0
termination-memory-alloca/fermat-alloca_true-termination.c.i true 3.2  280 31   2 true 88   3700 740 2 error (42) 880     14000   12000    0 error (42) 880     15000   12000    0 exception 4.1 260 36 0 true .39 35 4.6 2 unknown .058 4.6 .14 0 unknown .029 4.6 .17  0 timeout 900     5200 11000    0 exception 4.2 290 36 0 out of memory 770    15000 10000   0 disqualified .046 9.1 .44 0 probably out of memory (killed (signal 9, verification)) 290    15000 4300   0 timeout 900   870 13000 0 error (5) .033 5.6 .16  0 error (5) .034 5.5 .22  0
termination-memory-alloca/flag-alloca_true-termination.c.i timeout 900    7300 11000   0 true 17   1300 150 2 error (42) 880     2900   3600    0 error (42) 880     390   6600    0 timeout 910   4300 14000 0 true .36 35 4.2 2 unknown .041 4.6 .23 0 unknown .050 4.6 .17  0 timeout 900     670 12000    0 timeout 910   4100 12000 0 timeout 900    530 4300   0 disqualified .048 9.3 .43 0 timeout (verification) 900    470 5900   0 true 20   780 170 2 error (5) .021 5.6 .14  0 error (5) .022 5.6 .093 0
termination-memory-alloca/gcd1-alloca_true-termination.c.i false(termination) .37 50 2.6 -16 true 80   4200 520 2 error (42) 880     560   5200    0 out of memory 200     15000   2600    0 timeout 910   4200 14000 0 true .68 35 9.6 2 unknown .032 4.7 .21 0 unknown .029 4.6 .21  0 timeout 900     950 12000    0 timeout 910   4200 12000 0 timeout 900    850 6100   0 disqualified .044 9.2 .40 0 timeout (verification) 900    84 11000   0 true 65   860 610 2 error (5) .027 5.6 .26  0 error (5) .024 5.7 .14  0
termination-memory-alloca/genady-alloca_true-termination.c.i timeout 900    3400 11000   0 true 17   1900 140 2 true 3.8   66   49    2 true 3.8   36   56    2 timeout 900   4400 11000 0 true .35 35 4.3 2 unknown .034 4.6 .31 0 unknown .029 4.7 .20  0 true 390     2800 4600    2 timeout 900   7500 11000 0 true 2.4  64 31   2 disqualified .050 9.5 .47 0 true .11 16 1.2 2 true 10   470 97 2 error (5) .024 5.6 .17  0 error (5) .026 5.6 .089 0
termination-memory-alloca/insertionsort-alloca_true-termination.c.i error (134) .27 46 1.7 0 true 86   2600 870 2 error (42) 880     14000   10000    0 out of memory 150     15000   1900    0 true 14   660 120 2 true .83 39 9.4 2 unknown .030 4.7 .19 0 unknown .028 4.6 .17  0 timeout 900     420 15000    0 true 14   660 120 2 timeout 900    870 5700   0 disqualified .044 9.5 .44 0 timeout (verification) 900    1200 11000   0 true 16   580 140 2 error (5) .030 5.6 .086 0 error (5) .028 5.6 .15  0
termination-memory-alloca/java_AG313-alloca_true-termination.c.i timeout 900    8400 10000   0 true 24   1700 200 2 error (42) 880     4300   5700    0 error (42) 880     370   6700    0 timeout 910   4400 11000 0 true .39 35 4.6 2 unknown .034 4.6 .24 0 unknown .028 4.6 .25  0 timeout 900     240 11000    0 timeout 900   4100 11000 0 timeout 900    560 4700   0 disqualified .057 9.4 .31 0 timeout (verification) 900    83 11000   0 true 14   500 120 2 error (5) .028 5.7 .24  0 error (5) .029 5.5 .11  0
termination-memory-alloca/java_Break-alloca_true-termination.c.i timeout 900    5000 11000   0 true 7.0 450 57 2 true .14  8.3 1.6  2 true .13  8.6 1.3  2 timeout 900   3900 13000 0 true .37 35 4.8 2 unknown .034 4.7 .26 0 unknown .044 4.6 .21  0 true .092 26 1.2  2 timeout 900   3900 12000 0 true .74 64 6.7 2 disqualified .045 9.3 .41 0 true .11 15 1.4 2 true 11   460 93 2 error (5) .026 5.5 .13  0 error (5) .019 5.7 .18  0
termination-memory-alloca/java_BubbleSort-alloca_true-termination.c.i error (134) .25 46 2.0 0 timeout 900   12000 6000 0 error (42) 870     13000   5300    0 out of memory 110     15000   1400    0 true 10   400 81 2 true 2.2  100 26   2 unknown .029 4.6 .26 0 unknown .032 4.6 .23  0 timeout 900     4000 7600    0 true 8.9 480 77 2 timeout 900    1000 7000   0 disqualified .064 9.2 .33 0 timeout (verification) 900    630 12000   0 true 18   680 170 2 error (5) .030 5.6 .11  0 error (5) .024 5.7 .091 0
termination-memory-alloca/java_Continue1-alloca_true-termination.c.i true .49 62 4.1 2 true 10   740 73 2 true .21  8.3 2.0  2 true .20  8.6 2.7  2 true 330   4600 3700 2 true .37 35 4.1 2 unknown .052 4.6 .16 0 unknown .052 4.6 .18  0 true .11  26 1.1  2 true 350   4700 4400 2 true .71 64 7.6 2 disqualified .048 9.3 .38 0 true .11 15 1.2 2 true 42   640 490 2 error (5) .023 5.6 .12  0 error (5) .023 5.6 .11  0
termination-memory-alloca/java_LogBuiltIn-alloca_true-termination.c.i timeout 900    150 3000   0 true 8.8 500 75 2 true .59  16   6.9  2 true .67  16   8.4  2 timeout 900   3900 10000 0 true .38 34 5.1 2 unknown .023 4.6 .21 0 unknown .034 4.6 .23  0 true .16  26 2.1  2 timeout 900   3900 10000 0 true .99 130 12   2 disqualified .048 9.1 .42 0 true .38 17 5.4 2 true 12   510 97 2 error (5) .039 5.7 .096 0 error (5) .026 5.6 .093 0
termination-memory-alloca/java_Nested-alloca_true-termination.c.i out of memory 38    15000 400   0 true 25   2400 210 2 true .20  8.0 2.0  2 true .17  8.4 1.8  2 timeout 900   4000 12000 0 true .39 35 5.4 2 unknown .030 4.7 .21 0 unknown .025 4.8 .42  0 true .094 27 1.1  2 timeout 910   4100 13000 0 true .75 64 7.1 2 disqualified .045 9.4 .41 0 true .13 14 1.2 2 error (7) 85   710 1200 0 error (5) .022 5.6 .15  0 error (5) .031 5.6 .067 0
termination-memory-alloca/java_Sequence-alloca_true-termination.c.i out of memory 75    15000 700   0 true 11   760 86 2 true .33  8.2 4.0  2 true .32  8.1 3.4  2 timeout 900   4100 11000 0 true .36 36 3.8 2 unknown .028 4.8 .13 0 unknown .027 4.6 .25  0 true .28  27 3.4  2 timeout 900   4000 13000 0 true .77 64 6.1 2 disqualified .054 9.4 .46 0 true .11 15 1.3 2 timeout 900   1100 10000 0 error (5) .025 5.7 .075 0 error (5) .024 5.6 .21  0
termination-memory-alloca/lis-alloca_true-termination.c.i error (134) .26 46 2.4 0 error (1) 80   2300 980 0 error (42) 870     14000   8900    0 out of memory 110     15000   1400    0 timeout 900   4200 13000 0 true 1.0  50 14   2 unknown .027 4.6 .16 0 unknown .045 4.7 .16  0 timeout 900     10000 11000    0 timeout 900   4100 15000 0 timeout 900    1300 5100   0 disqualified .048 9.1 .37 0 timeout (verification) 900    460 13000   0 timeout 900   1000 13000 0 error (5) .042 5.6 .18  0 error (5) .044 5.6 .095 0
termination-memory-alloca/min_rf-alloca_true-termination.c.i timeout 900    1100 11000   0 true 73   2500 570 2 error (42) 880     950   8600    0 out of memory 230     15000   3100    0 timeout 910   4400 13000 0 true .39 35 5.5 2 unknown .053 4.7 .24 0 unknown .040 4.7 .21  0 timeout 900     210 11000    0 timeout 900   4100 12000 0 out of memory 77    15000 1100   0 disqualified .064 9.6 .36 0 timeout (verification) 900    45 14000   0 true 210   7700 2700 2 error (5) .051 5.6 .13  0 error (5) .042 5.5 .081 0
termination-memory-alloca/mult_array-alloca_true-termination.c.i error (134) .27 46 1.7 0 error (1) 48   2300 530 0 error (42) 880     14000   5900    0 error (42) 880     2200   7000    0 exception 3.8 270 37 0 true .65 36 8.0 2 unknown .034 4.6 .19 0 unknown .044 4.6 .17  0 timeout 900     4300 11000    0 exception 4.0 290 34 0 timeout 900    1100 8400   0 disqualified .047 9.3 .43 0 timeout (verification) 900    630 11000   0 true 15   590 130 2 error (5) .025 5.7 .12  0 error (5) .022 5.6 .16  0
termination-memory-alloca/openbsd_cbzero-alloca_true-termination.c.i error (134) .26 46 2.0 0 true 13   750 96 2 error (42) 880     14000   4800    0 error (42) 870     14000   5100    0 true 7.6 350 63 2 true .51 35 5.6 2 unknown .032 4.6 .21 0 unknown .025 4.7 .22  0 timeout 900     3800 10000    0 true 7.5 360 64 2 error (8) .70 64 8.3 0 disqualified .043 9.1 .42 0 timeout (verification) 900    340 11000   0 true 11   470 95 2 error (5) .029 5.5 .16  0 error (5) .025 5.6 .15  0
termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i error (134) .26 46 1.9 0 true 22   1400 160 2 error (42) 880     1300   7500    0 error (42) 880     420   7300    0 true 7.2 340 61 2 true .49 36 6.3 2 unknown .029 4.6 .21 0 unknown .030 4.6 .24  0 timeout 900     1400 8400    0 true 7.0 430 60 2 out of memory 39    15000 490   0 disqualified .045 9.2 .47 0 timeout (verification) 900    280 12000   0 true 12   500 110 2 error (5) .025 5.5 .099 0 error (5) .033 5.7 .098 0
termination-memory-alloca/openbsd_cmemrchr-alloca_true-termination.c.i error (134) .26 46 1.8 0 true 26   2300 200 2 error (42) 880     13000   6400    0 error (42) 870     13000   8500    0 true 6.8 400 58 2 true .48 36 6.1 2 unknown .023 4.6 .16 0 unknown .028 4.6 .17  0 timeout 900     940 11000    0 true 6.9 440 62 2 error (8) .69 64 7.1 0 disqualified .044 9.5 .36 0 timeout (verification) 900    2000 12000   0 true 11   500 92 2 error (5) .030 5.6 .18  0 error (5) .023 5.7 .10  0
termination-memory-alloca/openbsd_cmemset-alloca_true-termination.c.i error (134) .26 46 1.8 0 true 19   1300 150 2 error (42) 880     14000   4300    0 error (42) 870     14000   5400    0 true 6.8 310 55 2 true .49 36 6.7 2 unknown .029 4.7 .25 0 unknown .030 4.7 .15  0 timeout 900     4000 11000    0 true 7.3 390 65 2 error (8) .71 64 6.6 0 disqualified .043 9.5 .54 0 timeout (verification) 900    280 11000   0 true 12   510 90 2 error (5) .043 5.4 .14  0 error (5) .029 5.7 .23  0
termination-memory-alloca/openbsd_cstpcpy-alloca_true-termination.c.i error (134) .27 46 1.8 0 true 79   2300 900 2 error (42) 880     14000   4100    0 error (42) 870     14000   5100    0 unknown 360   4400 5100 0 true .49 35 5.8 2 unknown .042 4.6 .15 0 unknown .033 4.6 .34  0 timeout 900     2500 13000    0 unknown 430   4400 5300 0 error (8) .74 64 5.8 0 disqualified .044 9.4 .46 0 timeout (verification) 900    240 12000   0 true 11   490 100 2 error (5) .024 5.6 .13  0 error (5) .041 5.7 .095 0
termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i error (134) .28 46 1.9 0 true 64   2700 560 2 error (42) 880     14000   9900    0 error (42) 880     5200   5900    0 timeout 900   4400 13000 0 true .69 36 9.0 2 unknown .028 4.7 .20 0 unknown .033 4.7 .22  0 timeout 900     7600 9000    0 timeout 900   4400 13000 0 error (8) .74 64 6.5 0 disqualified .049 9.2 .38 0 timeout (verification) 900    1700 11000   0 true 27   560 290 2 error (5) .038 5.6 .13  0 error (5) .023 5.6 .16  0
termination-memory-alloca/openbsd_cstrcat-alloca_true-termination.c.i error (134) .27 47 2.0 0 error (1) 73   3100 610 0 error (42) 880     14000   7400    0 error (42) 880     3900   8000    0 timeout 900   4100 11000 0 true .52 35 7.3 2 unknown .028 4.7 .24 0 unknown .041 4.5 .20  0 timeout 900     2000 13000    0 timeout 900   4100 12000 0 timeout 900    10000 12000   0 disqualified .045 9.4 .42 0 timeout (verification) 900    260 14000   0 true 12   570 110 2 error (5) .029 5.7 .12  0 error (5) .023 5.6 .13  0
termination-memory-alloca/openbsd_cstrcmp-alloca_true-termination.c.i error (134) .26 46 2.0 0 true 21   1900 190 2 error (42) 880     1600   8100    0 error (42) 880     350   5300    0 timeout 900   4200 11000 0 true .52 35 6.5 2 unknown .031 4.6 .17 0 unknown .054 4.6 .21  0 timeout 900     2300 11000    0 timeout 900   4200 11000 0 out of memory 85    15000 1100   0 disqualified .051 9.2 .46 0 timeout (verification) 900    170 12000   0 true 12   500 93 2 error (5) .025 5.7 .16  0 error (5) .026 5.6 .10  0
termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i error (134) .27 46 2.0 0 true 74   2300 890 2 error (42) 880     14000   4500    0 error (42) 880     14000   5900    0 unknown 460   4500 5500 0 true .49 35 6.4 2 unknown .031 4.8 .15 0 unknown .028 4.6 .21  0 timeout 900     2500 9800    0 unknown 510   4500 6300 0 error (8) .74 64 6.1 0 disqualified .048 9.6 .40 0 timeout (verification) 900    230 12000   0 true 13   600 100 2 error (5) .025 5.7 .16  0 error (5) .026 5.8 .12  0
termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i error (134) .25 46 2.1 0 timeout 900   11000 4800 0 error (42) 880     330   4200    0 out of memory 260     15000   3000    0 timeout 900   2000 14000 0 true 1.1  60 15   2 unknown .029 4.7 .20 0 unknown .027 4.6 .20  0 timeout 900     1600 9200    0 timeout 900   2400 12000 0 out of memory 57    15000 910   0 disqualified .045 9.3 .38 0 timeout (verification) 900    95 14000   0 unknown 34   1300 330 0 error (5) .028 5.6 .12  0 error (5) .024 5.7 .16  0
termination-memory-alloca/openbsd_cstrlcpy-alloca_true-termination.c.i error (134) .25 46 2.1 0 true 45   2600 360 2 error (42) 880     15000   7400    0 error (42) 880     2200   7700    0 timeout 900   3900 12000 0 true .56 36 6.1 2 unknown .032 4.6 .21 0 unknown .057 4.7 .26  0 timeout 900     870 11000    0 timeout 900   2300 11000 0 timeout 900    760 15000   0 disqualified .045 9.3 .40 0 timeout (verification) 900    480 11000   0 true 16   720 130 2 error (5) .029 5.6 .15  0 error (5) .022 5.6 .11  0
termination-memory-alloca/openbsd_cstrlen-alloca_true-termination.c.i error (134) .26 46 2.0 0 true 8.5 550 71 2 error (42) 880     6200   3700    0 error (42) 880     340   6000    0 unknown 8.3 410 76 0 true .47 35 5.9 2 unknown .034 4.6 .27 0 unknown .043 4.6 .15  0 timeout 900     2200 9700    0 unknown 8.1 460 68 0 timeout 900    1100 13000   0 disqualified .048 9.3 .55 0 timeout (verification) 900    400 11000   0 true 11   450 95 2 error (5) .027 5.6 .19  0 error (5) .028 5.7 .087 0
termination-memory-alloca/openbsd_cstrncat-alloca_true-termination.c.i error (134) .25 47 2.1 0 error (1) 82   2300 710 0 error (42) 880     14000   6400    0 error (42) 880     2300   6200    0 timeout 900   4200 12000 0 true .58 36 8.1 2 unknown .055 4.6 .17 0 unknown .030 4.7 .15  0 timeout 900     2300 11000    0 timeout 900   4300 12000 0 timeout 900    1100 10000   0 disqualified .046 9.6 .43 0 timeout (verification) 900    250 12000   0 true 12   570 100 2 error (5) .023 5.6 .012 0 error (5) .020 5.6 .16  0
termination-memory-alloca/openbsd_cstrncmp-alloca_true-termination.c.i error (134) .27 46 2.2 0 true 27   2300 240 2 error (42) 880     970   7100    0 error (42) 880     240   4900    0 unknown 650   4100 10000 0 true .51 35 6.1 2 unknown .029 4.6 .18 0 unknown .030 4.6 .21  0 timeout 900     2400 10000    0 unknown 840   4100 12000 0 out of memory 67    15000 800   0 disqualified .074 9.2 .33 0 timeout (verification) 900    210 12000   0 true 13   570 99 2 error (5) .024 5.6 .12  0 error (5) .024 5.7 .17  0
termination-memory-alloca/openbsd_cstrncpy-alloca_true-termination.c.i error (134) .25 47 2.0 0 true 51   2500 440 2 error (42) 880     14000   9900    0 error (42) 880     5200   6400    0 true 890   4500 12000 2 true .73 36 8.3 2 unknown .051 4.6 .19 0 unknown .029 4.6 .17  0 timeout 900     7500 9300    0 timeout 900   4400 13000 0 error (8) .72 65 7.6 0 disqualified .043 9.5 .38 0 timeout (verification) 900    1700 10000   0 true 16   530 140 2 error (5) .028 5.7 .20  0 error (5) .023 5.6 .15  0
termination-memory-alloca/openbsd_cstrnlen-alloca_true-termination.c.i error (134) .26 46 2.3 0 true 15   1300 120 2 error (42) 880     990   8100    0 error (42) 880     350   6100    0 true 8.8 470 77 2 true .48 36 6.5 2 unknown .054 4.7 .15 0 unknown .038 4.7 .23  0 timeout 900     1900 13000    0 true 9.1 350 82 2 timeout 900    440 5400   0 disqualified .043 9.2 .50 0 timeout (verification) 900    550 10000   0 true 11   520 86 2 error (5) .028 5.6 .11  0 error (5) .026 5.6 .11  0
termination-memory-alloca/openbsd_cstrpbrk-alloca_true-termination.c.i error (134) .27 47 2.0 0 true 34   2300 260 2 error (42) 880     270   6600    0 error (42) 880     13000   12000    0 timeout 900   2000 12000 0 true 3.0  60 42   2 unknown .028 4.6 .16 0 unknown .056 4.5 .22  0 timeout 900     630 10000    0 timeout 900   2200 12000 0 timeout 900    1000 12000   0 disqualified .042 9.1 .40 0 timeout (verification) 900    350 15000   0 true 33   750 360 2 error (5) .022 5.7 .15  0 error (5) .031 5.6 .11  0
termination-memory-alloca/openbsd_cstrspn-alloca_true-termination.c.i error (134) .26 47 2.0 0 timeout 910   10000 4900 0 error (42) 880     740   7300    0 out of memory 210     15000   3000    0 timeout 900   3300 11000 0 true 2.0  64 25   2 unknown .029 4.6 .19 0 unknown .032 4.5 .20  0 timeout 900     430 10000    0 timeout 900   3000 14000 0 timeout 900    760 10000   0 disqualified .061 9.4 .37 0 timeout (verification) 900    280 12000   0 unknown 37   1700 320 0 error (5) .025 5.6 .13  0 error (5) .022 5.7 .16  0
termination-memory-alloca/openbsd_cstrstr-alloca_true-termination.c.i error (134) .25 46 2.3 0 true 190   5500 1300 2 error (42) 880     13000   10000    0 out of memory 480     15000   6100    0 timeout 900   4300 14000 0 true 5.8  110 73   2 unknown .029 4.6 .22 0 unknown .035 4.6 .24  0 timeout 900     1400 12000    0 timeout 900   4300 12000 0 timeout 900    1200 9500   0 disqualified .048 9.4 .41 0 timeout (verification) 900    250 12000   0 true 41   820 320 2 error (5) .026 5.7 .093 0 error (5) .025 5.6 .081 0
termination-memory-alloca/rec_strlen-alloca_true-termination.c.i error (134) .24 46 2.7 0 true 13   950 120 2 out of memory 840     15000   4400    0 error (42) 880     610   8200    0 unknown 7.3 470 63 0 true .48 36 6.3 2 unknown .058 4.7 .18 0 unknown .046 4.6 .21  0 timeout 900     1600 13000    0 error (recursion) 4.0 280 36 0 out of memory 210    15000 2800   0 disqualified .055 9.5 .30 0 timeout (verification) 900    360 11000   0 true 10   440 85 2 error (5) .025 5.6 .12  0 error (5) .026 5.6 .11  0
termination-memory-alloca/selectionsort-alloca_true-termination.c.i error (134) .26 46 2.0 0 timeout 900   11000 7100 0 error (42) 880     14000   6400    0 out of memory 120     15000   1600    0 out of memory 480   15000 6000 0 true .84 42 9.5 2 unknown .035 4.6 .28 0 unknown .027 4.6 .26  0 timeout 900     3300 8500    0 true 19   770 170 2 timeout 900    260 7900   0 disqualified .045 9.0 .42 0 timeout (verification) 900    980 14000   0 true 19   710 170 2 error (5) .029 5.5 .10  0 error (5) .024 5.6 .21  0
termination-memory-alloca/stroeder1-alloca_true-termination.c.i error (134) .26 46 1.9 0 true 24   2100 190 2 error (42) 880     3300   3900    0 error (42) 880     430   5700    0 true 6.0 340 48 2 true .47 35 5.9 2 unknown .028 4.6 .21 0 unknown .030 4.6 .23  0 timeout 900     1700 11000    0 true 6.0 300 55 2 timeout 900    1200 7400   0 disqualified .043 9.3 .50 0 timeout (verification) 900    1300 13000   0 true 11   410 85 2 error (5) .039 5.7 .082 0 error (5) .033 5.6 .23  0
termination-memory-alloca/stroeder2-alloca_true-termination.c.i error (134) .26 46 2.1 0 true 61   2600 510 2 error (42) 880     2400   4600    0 out of memory 690     15000   6600    0 true 7.6 350 66 2 true .83 36 10   2 unknown .030 4.6 .17 0 unknown .033 4.6 .19  0 timeout 900     1200 11000    0 true 130   4000 1500 2 timeout 900    990 4400   0 disqualified .042 9.5 .48 0 timeout (verification) 900    1200 12000   0 true 13   580 110 2 error (5) .030 5.6 .21  0 error (5) .022 5.6 .15  0
termination-memory-alloca/strreplace-alloca_true-termination.c.i error (134) .30 46 2.0 0 true 43   2500 320 2 error (42) 880     13000   9400    0 out of memory 200     15000   2800    0 unknown 33   1400 290 0 true .49 35 6.0 2 unknown .032 4.6 .15 0 unknown .026 4.6 .20  0 timeout 900     170 14000    0 unknown 28   1400 250 0 error (8) .74 64 6.8 0 disqualified .061 9.1 .35 0 timeout (verification) 900    240 12000   0 true 12   560 100 2 error (5) .030 5.7 .15  0 error (5) .029 5.6 .15  0
termination-memory-alloca/subseq-alloca_true-termination.c.i error (134) .26 46 1.9 0 true 40   3400 310 2 error (42) 880     13000   8700    0 out of memory 300     15000   4100    0 timeout 900   2500 12000 0 true .52 36 5.6 2 unknown .041 4.5 .18 0 unknown .046 4.6 .17  0 timeout 900     570 14000    0 timeout 900   3100 12000 0 timeout 900    890 6200   0 disqualified .047 9.3 .42 0 timeout (verification) 900    42 11000   0 true 12   570 100 2 error (5) .026 5.6 .12  0 error (5) .025 5.6 .11  0
termination-memory-alloca/substring-alloca_true-termination.c.i error (134) .25 46 2.3 0 true 55   3500 450 2 error (42) 880     1300   6700    0 out of memory 190     15000   2500    0 timeout 900   4200 11000 0 true 1.2  37 17   2 unknown .032 4.6 .17 0 unknown .046 4.6 .17  0 timeout 900     830 11000    0 timeout 900   4200 12000 0 timeout 900    890 5700   0 disqualified .069 9.4 .38 0 timeout (verification) 900    400 14000   0 true 22   750 180 2 error (5) .033 5.8 .19  0 error (5) .024 5.6 .13  0
termination-memory-alloca/twisted-alloca_true-termination.c.i timeout 900    75 12000   0 true 5.6 390 52 2 true .080 7.0 .88 2 true .084 8.7 .83 2 timeout 900   4100 12000 0 true .40 35 4.8 2 unknown .033 4.6 .18 0 unknown .029 4.6 .21  0 true .085 27 1.1  2 timeout 900   4000 11000 0 true .72 65 8.3 2 disqualified .045 9.3 .47 0 true .16 17 1.9 2 true 24   620 250 2 error (5) .030 5.6 .12  0 error (5) .024 5.7 .11  0
termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i error (5) .25 46 2.6 0 error (1) 23   1400 170 0 error (42) 880     6200   9600    0 error (42) 880     3000   5400    0 error (recursion) 4.6 270 49 0 true .42 35 5.4 -32 unknown .032 4.6 .18 0 unknown .034 4.8 .25  0 timeout 900     2900 9000    0 error (recursion) 3.8 290 38 0 out of memory 890    15000 13000   0 disqualified .052 9.2 .35 0 probably out of memory (killed (signal 9, verification)) 530    15000 6900   0 false(termination) 13   560 110 1 error (5) .030 5.6 .22  0 error (5) .023 5.6 .17  0
termination-memory-linkedlists/cll_search-alloca_false-termination.c.i error (5) .26 46 2.5 0 error (1) 39   2400 300 0 error (42) 880     9300   11000    0 error (42) 870     2700   5700    0 false(termination) 8.6 470 77 1 true .44 38 6.1 -32 unknown .029 4.5 .21 0 unknown .038 4.6 .14  0 timeout 900     3400 8600    0 false(termination) 9.1 470 83 1 timeout 900    470 13000   0 disqualified .070 9.2 .37 0 timeout (verification) 900    460 12000   0 false(termination) 13   600 110 1 error (5) .049 5.7 .12  0 error (5) .032 5.7 .15  0
termination-memory-linkedlists/cll_traverse-alloca_false-termination.c.i error (5) .27 46 1.8 0 error (1) 33   2000 290 0 error (42) 880     9000   9800    0 error (42) 880     2700   5800    0 unknown 59   3700 590 0 true .43 37 5.3 -32 unknown .026 4.7 .25 0 unknown .046 4.6 .20  0 timeout 900     3400 9400    0 unknown 58   3900 600 0 timeout 900    470 9700   0 disqualified .052 9.5 .33 0 probably out of memory (killed (signal 9, verification)) 650    15000 8000   0 false(termination) 14   590 120 1 error (5) .024 5.7 .11  0 error (5) .026 5.6 .27  0
termination-memory-linkedlists/ll_append-alloca_false-termination.c.i error (5) .27 47 2.0 0 error (1) 12   990 97 0 error (42) 880     8400   9900    0 error (42) 880     3900   9200    0 error (recursion) 4.7 270 39 0 true .44 35 5.1 -32 unknown .038 4.6 .19 0 unknown .027 4.8 .28  0 timeout 900     2900 7900    0 error (recursion) 4.0 290 35 0 out of memory 460    15000 5800   0 disqualified .063 9.3 .47 0 probably out of memory (killed (signal 9, verification)) 600    15000 9100   0 false(termination) 15   510 140 1 error (5) .026 5.7 .14  0 error (5) .030 5.6 .10  0
termination-memory-linkedlists/ll_append_rec-alloca_false-termination.c.i error (5) .27 47 1.9 0 error (1) 11   880 100 0 error (42) 880     12000   8700    0 error (42) 880     4400   8800    0 error (recursion) 4.7 270 46 0 true .46 35 7.2 -32 unknown .025 4.7 .25 0 unknown .041 4.6 .12  0 timeout 900     3300 8700    0 error (recursion) 4.1 290 38 0 out of memory 460    15000 5500   0 disqualified .043 9.3 .42 0 probably out of memory (killed (signal 9, verification)) 530    15000 8400   0 false(termination) 34   1300 280 1 error (5) .035 5.5 .14  0 error (5) .026 5.6 .12  0
termination-memory-linkedlists/ll_create_rec-alloca_false-termination.c.i error (5) .26 46 2.4 0 error (1) 22   1000 140 0 error (42) 880     9500   6200    0 error (42) 880     1800   8100    0 unknown 8.8 480 77 0 true .38 35 4.6 -32 unknown .033 4.6 .13 0 unknown .032 4.6 .22  0 out of memory 610     15000 5300    0 error (recursion) 4.0 280 36 0 out of memory 140    15000 1700   0 disqualified .046 9.2 .37 0 timeout (verification) 900    850 9200   0 unknown 25   720 170 0 error (5) .024 5.6 .15  0 error (5) .027 5.6 .15  0
termination-memory-linkedlists/nondet_ll_search-alloca_false-termination.c.i error (5) .26 46 2.7 0 error (1) 58   2600 440 0 error (42) 880     13000   11000    0 error (42) 880     3000   7000    0 unknown 67   3600 600 0 true .45 38 5.3 -32 unknown .052 4.6 .16 0 unknown .049 4.6 .18  0 timeout 900     3400 9700    0 unknown 71   3800 630 0 timeout 900    470 12000   0 disqualified .044 9.2 .41 0 timeout (verification) 900    58 11000   0 false(termination) 28   880 230 1 error (5) .026 5.6 .093 0 error (5) .030 5.6 .20  0
termination-memory-linkedlists/nondet_ll_traverse-alloca_false-termination.c.i error (5) .26 46 1.9 0 error (1) 46   2500 380 0 error (42) 870     12000   13000    0 error (42) 880     3200   6800    0 unknown 57   3500 600 0 true .46 38 5.6 -32 unknown .027 4.6 .24 0 unknown .052 4.6 .14  0 timeout 900     3500 9300    0 unknown 63   3900 610 0 timeout 900    470 9500   0 disqualified .053 9.6 .45 0 timeout (verification) 900    61 11000   0 false(termination) 31   1300 270 1 error (5) .030 5.6 .21  0 error (5) .022 5.6 .20  0
termination-memory-linkedlists/cll_by_lseg-alloca_true-termination.c.i error (5) .27 46 1.8 0 true 13   1200 120 2 error (42) 880     8900   4900    0 error (42) 880     1800   8300    0 error (recursion) 4.6 260 42 0 true .38 35 5.1 2 unknown .032 4.6 .20 0 unknown .045 4.7 .17  0 out of memory 700     15000 6400    0 error (recursion) 4.1 280 33 0 out of memory 190    15000 2600   0 disqualified .045 9.3 .45 0 timeout (verification) 900    2100 11000   0 true 12   520 91 2 error (5) .029 5.6 .20  0 error (5) .024 5.7 .10  0
termination-memory-linkedlists/cll_search-alloca_true-termination.c.i error (5) .28 46 1.7 0 error (1) 43   2300 400 0 error (42) 880     9300   10000    0 error (42) 880     2700   5800    0 exception 4.2 270 35 0 true .64 39 8.3 2 unknown .031 4.6 .20 0 unknown .028 4.7 .22  0 timeout 900     3200 10000    0 exception 4.3 300 38 0 timeout 900    470 9700   0 disqualified .045 9.4 .41 0 timeout (verification) 900    2600 13000   0 unknown 330   1800 4900 0 error (5) .022 5.6 .23  0 error (5) .024 5.7 .18  0
termination-memory-linkedlists/ll_append-alloca_true-termination.c.i error (5) .26 46 1.9 0 error (1) 13   1100 100 0 error (42) 880     8900   9200    0 error (42) 880     6100   9900    0 error (recursion) 4.8 280 41 0 true .53 35 7.5 2 unknown .028 4.7 .27 0 unknown .029 4.6 .20  0 timeout 900     3200 8400    0 error (recursion) 3.8 260 31 0 out of memory 71    15000 1000   0 disqualified .069 9.0 .40 0 timeout (verification) 900    3300 6700   0 error (7) 210   1600 2600 0 error (5) .044 5.6 .11  0 error (5) .025 5.7 .080 0
termination-memory-linkedlists/ll_append_rec-alloca_true-termination.c.i error (5) .26 46 2.1 0 error (1) 9.7 690 84 0 error (42) 880     10000   5800    0 error (42) 880     6400   9300    0 error (recursion) 4.6 260 40 0 true .53 35 7.4 2 unknown .032 4.6 .22 0 unknown .029 4.6 .18  0 timeout 900     3300 8800    0 error (recursion) 3.9 290 33 0 out of memory 72    15000 1100   0 disqualified .047 9.1 .40 0 timeout (verification) 900    3400 7300   0 error (7) 270   2100 3000 0 error (5) .032 5.6 .17  0 error (5) .031 5.7 .17  0
termination-memory-linkedlists/ll_create_rec-alloca_true-termination.c.i error (5) .25 46 1.9 0 true 10   710 79 2 error (42) 880     9800   6100    0 error (42) 880     1800   8600    0 true 6.4 330 58 2 true .38 35 4.7 2 unknown .032 4.6 .24 0 unknown .032 4.6 .28  0 out of memory 630     15000 5600    0 error (recursion) 3.7 280 37 0 out of memory 190    15000 2100   0 disqualified .045 9.9 .50 0 timeout (verification) 900    870 9300   0 true 9.6 430 78 2 error (5) .023 5.6 .16  0 error (5) .024 5.7 .12  0
termination-memory-linkedlists/ll_search-alloca_true-termination.c.i error (5) .28 46 1.9 0 true 25   1700 190 2 error (42) 880     2500   11000    0 error (42) 880     2600   5800    0 exception 4.2 270 43 0 true .42 35 6.7 2 unknown .029 4.6 .21 0 unknown .049 4.5 .17  0 timeout 900     3500 10000    0 exception 4.1 260 38 0 timeout 900    450 9500   0 disqualified .047 9.4 .40 0 timeout (verification) 900    2900 12000   0 unknown 190   1900 2800 0 error (5) .025 5.6 .16  0 error (5) .027 5.7 .13  0
termination-memory-linkedlists/ll_search_not_found-alloca_true-termination.c.i error (5) .32 46 2.3 0 true 21   1300 170 2 error (42) 880     2500   11000    0 error (42) 880     2700   5300    0 unknown 15   630 130 0 true .43 35 4.8 2 unknown .027 4.8 .23 0 unknown .040 4.7 .22  0 timeout 900     3300 8600    0 unknown 15   530 150 0 timeout 900    440 9300   0 disqualified .058 9.4 .36 0 timeout (verification) 900    540 11000   0 unknown 45   1800 430 0 error (5) .022 5.6 .17  0 error (5) .051 5.6 .12  0
termination-memory-linkedlists/ll_traverse-alloca_true-termination.c.i error (5) .27 46 2.0 0 true 21   1300 160 2 error (42) 880     4200   11000    0 error (42) 880     2800   6100    0 unknown 9.2 470 79 0 true .40 35 5.5 2 unknown .032 4.7 .22 0 unknown .030 4.6 .21  0 timeout 900     3300 8100    0 unknown 8.9 460 84 0 timeout 900    450 11000   0 disqualified .046 9.4 .39 0 timeout (verification) 900    1700 12000   0 unknown 41   1900 430 0 error (5) .032 5.6 .19  0 error (5) .025 5.6 .15  0
termination-memory-linkedlists/nondet_ll_search-alloca_true-termination.c.i error (5) .26 46 2.3 0 error (1) 47   2400 400 0 error (42) 880     13000   11000    0 error (42) 880     3000   6500    0 exception 4.2 260 40 0 true .67 39 7.6 2 unknown .030 4.6 .18 0 unknown .023 4.6 .22  0 timeout 900     3200 11000    0 exception 4.5 300 38 0 timeout 900    470 9900   0 disqualified .070 9.2 .33 0 timeout (verification) 900    2800 11000   0 unknown 300   3800 3700 0 error (5) .024 5.6 .11  0 error (5) .024 5.6 .10  0
termination-15/add_first_alloca_true-termination.c.i error (134) .25 46 1.8 0 error (1) 14   810 110 0 error (42) 880     13000   6900    0 error (42) 870     14000   8900    0 true 12   520 99 2 unknown .98 66 12   0 unknown .027 4.6 .23 0 unknown .032 4.5 .17  0 timeout 900     770 11000    0 true 12   500 110 2 timeout 900    1200 7200   0 disqualified .071 9.2 .38 0 true .14 17 1.6 2 true 11   440 85 2 error (5) .026 5.7 .14  0 error (5) .025 5.7 .14  0
termination-15/array05_alloca_true-termination.c.i error (134) .26 46 1.9 0 error (1) 33   1500 250 0 error (42) 880     15000   9100    0 error (42) 870     13000   6800    0 true 7.5 360 69 2 unknown .95 65 11   0 unknown .055 4.7 .15 0 unknown .032 4.6 .21  0 timeout 900     270 12000    0 true 7.3 340 60 2 timeout 900    1100 5700   0 disqualified .062 9.2 .30 0 timeout (verification) 900    150 7300   0 unknown 18   590 140 0 error (5) .045 5.5 .16  0 error (5) .045 5.6 .086 0
termination-15/array06_alloca_true-termination.c.i error (134) .26 46 1.8 0 true 29   1400 230 2 error (42) 880     14000   8300    0 error (42) 880     1100   8100    0 true 7.5 360 67 2 unknown 1.0  66 11   0 unknown .029 4.6 .19 0 unknown .030 4.6 .22  0 timeout 900     990 9300    0 true 6.9 340 69 2 timeout 900    1000 4500   0 disqualified .046 9.4 .39 0 timeout (verification) 900    860 11000   0 true 13   540 99 2 error (5) .027 5.8 .19  0 error (5) .025 5.6 .098 0
termination-15/array07_alloca_true-termination.c.i error (134) .26 46 2.0 0 true 28   1600 200 2 error (42) 880     14000   10000    0 error (42) 880     1100   7000    0 true 7.5 360 69 2 unknown 1.0  66 11   0 unknown .024 4.6 .13 0 unknown .034 4.7 .17  0 timeout 900     1000 13000    0 true 7.3 350 59 2 timeout 900    1100 6000   0 disqualified .045 9.5 .42 0 timeout (verification) 900    770 14000   0 true 13   550 110 2 error (5) .022 5.6 .16  0 error (5) .024 5.7 .21  0
termination-15/array08_alloca_true-termination.c.i error (134) .25 46 1.9 0 timeout 900   14000 5400 0 error (42) 880     14000   9700    0 out of memory 490     15000   7000    0 timeout 900   4500 11000 0 unknown .98 66 12   0 unknown .034 4.6 .20 0 unknown .029 4.6 .16  0 timeout 900     310 12000    0 timeout 900   4500 12000 0 timeout 900    1000 5600   0 disqualified .053 9.1 .45 0 timeout (verification) 900    450 9500   0 unknown 25   640 220 0 error (5) .059 5.7 .14  0 error (5) .024 5.7 .16  0
termination-15/array09_alloca_true-termination.c.i error (134) .25 47 2.3 0 timeout 910   13000 4900 0 error (42) 880     14000   9200    0 out of memory 500     15000   6000    0 timeout 900   4500 11000 0 unknown 1.0  66 11   0 unknown .045 4.6 .18 0 unknown .027 4.7 .26  0 timeout 900     460 12000    0 timeout 900   4500 12000 0 timeout 900    1000 5800   0 disqualified .046 9.0 .52 0 timeout (verification) 900    110 7400   0 unknown 27   810 210 0 error (5) .027 5.6 .12  0 error (5) .028 5.6 .23  0
termination-15/array10_alloca_true-termination.c.i error (134) .25 46 2.2 0 error (1) 32   1500 240 0 error (42) 870     15000   10000    0 error (42) 880     13000   6400    0 true 7.9 360 69 2 unknown .99 68 12   0 unknown .033 4.6 .20 0 unknown .032 4.6 .21  0 timeout 900     260 13000    0 true 7.1 340 64 2 timeout 900    1100 4600   0 disqualified .047 9.0 .45 0 timeout (verification) 900    140 7300   0 unknown 19   780 150 0 error (5) .046 5.6 .11  0 error (5) .024 5.6 .18  0
termination-15/array12_alloca_true-termination.c.i error (134) .26 46 1.6 0 error (1) 57   2300 700 0 error (42) 880     14000   8300    0 out of memory 220     15000   2800    0 timeout 900   4500 9500 0 unknown .98 67 13   0 unknown .030 4.7 .23 0 unknown .032 4.6 .16  0 timeout 900     1600 11000    0 timeout 900   520 10000 0 timeout 900    1000 6100   0 disqualified .049 9.2 .45 0 timeout (verification) 900    200 5900   0 timeout 900   950 11000 0 error (5) .024 5.5 .16  0 error (5) .024 5.6 .15  0
termination-15/array13_alloca_true-termination.c.i error (134) .25 47 1.9 0 error (1) 67   2300 700 0 error (42) 880     14000   8800    0 out of memory 220     15000   2700    0 timeout 900   4400 14000 0 unknown .97 66 11   0 unknown .030 4.6 .15 0 unknown .026 4.6 .25  0 timeout 900     1200 11000    0 timeout 900   520 11000 0 timeout 900    1000 6300   0 disqualified .048 9.5 .38 0 timeout (verification) 900    190 8900   0 timeout 900   780 6900 0 error (5) .024 5.6 .097 0 error (5) .023 5.6 .13  0
termination-15/array16_alloca_fixed_true-termination.c.i error (134) .24 46 2.6 0 error (1) 51   3500 550 0 error (42) 870     14000   8300    0 out of memory 220     15000   2700    0 timeout 900   5000 12000 0 unknown .99 65 10   0 unknown .054 4.6 .14 0 unknown .028 4.6 .19  0 timeout 900     1300 13000    0 timeout 900   4700 14000 0 timeout 900    1300 6500   0 disqualified .044 9.5 .47 0 timeout (verification) 900    170 7300   0 timeout 900   1200 8900 0 error (5) .024 5.6 .16  0 error (5) .037 5.7 .093 0
termination-15/array17_alloca_true-termination.c.i error (134) .27 46 2.2 0 error (1) 57   2400 420 0 error (42) 880     14000   7800    0 out of memory 270     15000   3500    0 unknown 14   550 110 0 unknown .97 66 12   0 unknown .055 4.6 .13 0 unknown .033 4.6 .24  0 timeout 900     220 12000    0 unknown 14   540 110 0 timeout 900    790 6100   0 disqualified .070 9.4 .34 0 timeout (verification) 900    150 7700   0 timeout 900   760 7000 0 error (5) .024 5.6 .11  0 error (5) .024 5.7 .095 0
termination-15/array18_alloca_true-termination.c.i error (134) .26 46 1.9 0 timeout 910   13000 4700 0 error (42) 880     14000   8000    0 out of memory 490     15000   7100    0 timeout 900   4400 13000 0 unknown .94 66 11   0 unknown .032 4.6 .21 0 unknown .030 4.6 .15  0 timeout 900     480 12000    0 timeout 900   4400 12000 0 timeout 900    1000 7600   0 disqualified .045 9.4 .37 0 timeout (verification) 900    130 9200   0 unknown 25   630 180 0 error (5) .026 5.6 .14  0 error (5) .025 5.5 .12  0
termination-15/count_up_alloca_true-termination.c.i error (134) .26 46 1.7 0 true 100   4300 1000 2 error (42) 880     14000   7100    0 out of memory 140     15000   2100    0 unknown 25   800 210 0 unknown 2.3  66 30   0 unknown .055 4.7 .22 0 unknown .029 4.7 .21  0 timeout 900     350 12000    0 unknown 23   790 220 0 timeout 900    600 5400   0 disqualified .048 9.5 .41 0 timeout (verification) 900    1300 10000   0 true 16   510 140 2 error (5) .028 5.5 .16  0 error (5) .023 5.6 .18  0
termination-15/count_up_and_down_alloca_true-termination.c.i error (134) .26 46 1.9 0 true 69   2500 640 2 error (42) 880     13000   7400    0 out of memory 190     15000   2900    0 unknown 18   650 150 0 unknown 2.3  66 31   0 unknown .056 4.6 .12 0 unknown .032 4.6 .28  0 timeout 900     580 11000    0 unknown 18   510 160 0 timeout 900    1100 5000   0 disqualified .046 9.4 .44 0 timeout (verification) 900    1300 11000   0 true 14   590 110 2 error (5) .022 5.6 .18  0 error (5) .051 5.7 .11  0
termination-15/cstrcat_diffterm_alloca_true-termination.c.i error (134) .27 46 1.9 0 error (1) 77   2700 550 0 error (42) 880     14000   6800    0 error (42) 880     4100   7900    0 timeout 900   4000 12000 0 unknown .96 67 12   0 unknown .024 4.6 .21 0 unknown .029 4.6 .21  0 timeout 900     2000 11000    0 timeout 900   4000 11000 0 timeout 900    10000 13000   0 disqualified .049 9.4 .35 0 timeout (verification) 900    260 11000   0 true 12   570 97 2 error (5) .025 5.7 .078 0 error (5) .045 5.6 .11  0
termination-15/cstrcat_malloc_true-termination.c.i error (134) .28 46 1.8 0 error (1) 69   2600 550 0 out of memory 110     13000   1100    0 error (42) 880     2600   13000    0 timeout 900   4000 14000 0 unknown .97 66 11   0 unknown .032 4.8 .27 0 unknown .028 4.6 .25  0 timeout 900     2000 11000    0 timeout 900   4100 13000 0 timeout 900    10000 14000   0 disqualified .043 9.4 .43 0 timeout (verification) 900    170 13000   0 true 12   580 110 2 error (5) .022 5.6 .15  0 error (5) .031 5.5 .078 0
termination-15/cstrcat_mixed_alloca_true-termination.c.i error (134) .26 46 2.1 0 error (1) 74   3000 570 0 error (42) 880     14000   6300    0 error (42) 880     3900   8000    0 timeout 900   4000 13000 0 unknown .97 67 9.8 0 unknown .027 4.6 .24 0 unknown .031 4.7 .22  0 timeout 900     1900 12000    0 timeout 900   4000 12000 0 error (8) .73 64 6.4 0 disqualified .053 9.1 .38 0 timeout (verification) 900    97 9600   0 true 12   560 110 2 error (5) .050 5.6 .12  0 error (5) .049 5.6 .15  0
termination-15/cstrcat_reverse_alloca_true-termination.c.i error (134) .28 46 2.1 0 error (1) 65   2400 470 0 error (42) 880     14000   5600    0 error (42) 880     4000   9200    0 timeout 900   5000 11000 0 unknown 1.0  66 12   0 unknown .035 4.6 .17 0 unknown .027 4.7 .25  0 timeout 900     2000 13000    0 timeout 900   4900 11000 0 error (8) .70 64 9.0 0 disqualified .045 9.5 .67 0 timeout (verification) 900    92 9400   0 true 13   580 100 2 error (5) .027 5.6 .22  0 error (5) .027 5.6 .19  0
termination-15/cstrchr_diffterm_alloca_true-termination.c.i error (134) .27 46 1.7 0 true 11   740 94 2 error (42) 880     5600   6600    0 error (42) 880     370   6900    0 unknown 27   990 220 0 unknown .93 66 10   0 unknown .031 4.6 .12 0 unknown .031 4.6 .21  0 timeout 900     1200 11000    0 unknown 26   980 240 0 timeout 900    650 7700   0 disqualified .053 9.4 .36 0 timeout (verification) 900    500 11000   0 true 11   510 79 2 error (5) .022 5.6 .087 0 error (5) .052 5.6 .18  0
termination-15/cstrchr_malloc_true-termination.c.i error (134) .29 46 2.0 0 true 11   740 91 2 error (42) 880     5500   5500    0 error (42) 880     280   7100    0 unknown 36   1500 290 0 unknown .95 66 11   0 unknown .035 4.8 .22 0 unknown .032 4.6 .29  0 timeout 900     1200 11000    0 unknown 33   1500 260 0 timeout 900    640 6400   0 disqualified .048 9.5 .34 0 timeout (verification) 900    490 11000   0 true 12   480 100 2 error (5) .025 5.7 .19  0 error (5) .024 5.6 .16  0
termination-15/cstrchr_reverse_alloca_true-termination.c.i error (134) .24 46 1.9 0 true 11   730 90 2 error (42) 880     13000   5400    0 error (42) 870     13000   6200    0 unknown 15   670 140 0 unknown .97 66 10   0 unknown .028 4.6 .20 0 unknown .041 4.6 .083 0 timeout 900     1900 13000    0 unknown 14   690 130 0 error (8) .69 64 7.4 0 disqualified .049 9.5 .40 0 timeout (verification) 900    130 11000   0 true 11   520 110 2 error (5) .038 5.5 .12  0 error (5) .030 5.5 .071 0
termination-15/cstrcmp_diffterm_alloca_true-termination.c.i error (134) .27 46 1.9 0 true 22   1500 170 2 error (42) 880     5300   7500    0 error (42) 880     340   5900    0 timeout 900   3400 11000 0 unknown .96 65 11   0 unknown .042 4.7 .15 0 unknown .030 4.6 .20  0 timeout 900     2800 11000    0 timeout 900   3100 12000 0 timeout 900    850 5300   0 disqualified .048 9.3 .46 0 timeout (verification) 900    220 11000   0 true 12   500 100 2 error (5) .024 5.6 .12  0 error (5) .022 5.7 .17  0
termination-15/cstrcmp_malloc_true-termination.c.i error (134) .29 47 2.0 0 true 24   2300 220 2 error (42) 880     5700   6800    0 error (42) 880     230   8100    0 timeout 900   3500 12000 0 unknown .95 66 10   0 unknown .038 4.7 .23 0 unknown .032 4.6 .17  0 timeout 900     2800 11000    0 timeout 900   3200 11000 0 timeout 900    850 4900   0 disqualified .061 9.3 .46 0 timeout (verification) 900    110 12000   0 true 13   550 120 2 error (5) .026 5.6 .10  0 error (5) .045 5.7 .13  0
termination-15/cstrcmp_mixed_alloca_true-termination.c.i error (134) .27 46 3.0 0 true 20   1600 180 2 error (42) 880     13000   5300    0 error (42) 880     13000   6800    0 unknown 870   3300 13000 0 unknown .98 67 11   0 unknown .027 4.6 .23 0 unknown .033 4.7 .22  0 timeout 900     2800 12000    0 timeout 900   2600 14000 0 error (8) .71 64 6.6 0 disqualified .057 9.4 .38 0 timeout (verification) 900    98 8800   0 true 13   520 120 2 error (5) .027 5.7 .18  0 error (5) .023 5.8 .10  0
termination-15/cstrcmp_reverse_alloca_true-termination.c.i error (134) .26 47 1.6 0 true 22   1800 180 2 error (42) 880     13000   8000    0 error (42) 880     13000   6500    0 timeout 900   3400 12000 0 unknown .97 67 12   0 unknown .030 4.6 .24 0 unknown .027 4.6 .19  0 timeout 900     3400 11000    0 timeout 900   3300 12000 0 error (8) .70 64 6.2 0 disqualified .045 9.1 .40 0 timeout (verification) 900    120 8200   0 true 12   520 94 2 error (5) .025 5.6 .11  0 error (5) .024 5.6 .12  0
termination-15/cstrcpy_diffterm_alloca_true-termination.c.i error (134) .27 46 2.1 0 error (1) 22   1400 190 0 error (42) 880     14000   5000    0 error (42) 880     14000   6600    0 unknown 140   3000 1700 0 unknown .96 66 10   0 unknown .031 4.7 .16 0 unknown .030 4.7 .17  0 timeout 900     3000 11000    0 unknown 170   2400 1900 0 error (8) .72 64 6.2 0 disqualified .060 9.0 .40 0 timeout (verification) 900    220 13000   0 true 12   490 94 2 error (5) .048 5.6 .095 0 error (5) .038 5.5 .11  0
termination-15/cstrcpy_malloc_true-termination.c.i error (134) .25 46 2.1 0 true 97   2300 1300 2 out of memory 150     13000   1600    0 error (42) 880     5900   6500    0 unknown 140   2700 1800 0 unknown .95 67 12   0 unknown .032 4.6 .21 0 unknown .029 4.6 .20  0 timeout 900     3000 12000    0 unknown 170   2500 2200 0 error (8) .76 64 7.5 0 disqualified .048 9.4 .40 0 timeout (verification) 900    77 11000   0 true 12   490 110 2 error (5) .046 5.5 .16  0 error (5) .053 5.5 .16  0
termination-15/cstrcpy_mixed_alloca_true-termination.c.i error (134) .26 46 2.1 0 error (1) 20   1400 160 0 error (42) 880     14000   5800    0 error (42) 880     15000   6600    0 unknown 140   2700 1800 0 unknown .96 67 11   0 unknown .029 4.6 .20 0 unknown .044 4.6 .19  0 timeout 900     2800 13000    0 unknown 180   2600 2300 0 error (8) .71 64 7.8 0 disqualified .046 9.5 .54 0 timeout (verification) 900    260 12000   0 true 12   550 100 2 error (5) .027 5.7 .17  0 error (5) .032 5.7 .17  0
termination-15/cstrcpy_reverse_alloca_true-termination.c.i error (134) .28 46 1.9 0 error (1) 21   1400 180 0 error (42) 870     14000   6400    0 error (42) 880     15000   6200    0 unknown 140   2700 2200 0 unknown .97 67 11   0 unknown .023 4.5 .26 0 unknown .050 4.6 .17  0 timeout 900     2800 11000    0 unknown 180   2500 2700 0 error (8) .71 64 6.6 0 disqualified .068 9.2 .35 0 timeout (verification) 900    92 8000   0 true 12   520 91 2 error (5) .023 5.6 .15  0 error (5) .044 5.5 .094 0
termination-15/cstrcspn_diffterm_alloca_true-termination.c.i error (134) .27 46 1.7 0 true 80   5400 600 2 error (42) 880     990   5900    0 out of memory 200     15000   2400    0 timeout 900   3700 12000 0 unknown 1.2  67 13   0 unknown .032 4.6 .33 0 unknown .029 4.8 .21  0 timeout 900     1400 9700    0 timeout 900   3700 12000 0 timeout 900    720 6000   0 disqualified .046 9.4 .46 0 timeout (verification) 900    510 11000   0 true 34   610 350 2 error (5) .025 5.6 .11  0 error (5) .025 5.6 .14  0
termination-15/cstrcspn_malloc_true-termination.c.i error (134) .26 47 1.8 0 true 81   5100 660 2 error (42) 880     4200   6500    0 out of memory 190     15000   2400    0 timeout 900   3700 11000 0 unknown 1.1  66 14   0 unknown .031 4.7 .21 0 unknown .029 4.6 .27  0 timeout 900     1500 9700    0 timeout 900   3500 12000 0 timeout 900    630 5500   0 disqualified .066 9.4 .69 0 timeout (verification) 900    340 13000   0 true 110   580 1600 2 error (5) .025 5.6 .14  0 error (5) .023 5.6 .11  0
termination-15/cstrcspn_mixed_alloca_true-termination.c.i error (134) .26 46 1.9 0 true 71   4000 510 2 error (42) 880     13000   7000    0 out of memory 200     15000   2700    0 unknown 300   3700 4300 0 unknown 1.4  66 13   0 unknown .031 4.6 .14 0 unknown .029 4.6 .20  0 timeout 900     1200 13000    0 timeout 900   3700 11000 0 error (8) .73 64 9.8 0 disqualified .060 9.2 .28 0 timeout (verification) 900    550 9500   0 true 140   810 1700 2 error (5) .026 5.6 .12  0 error (5) .031 5.5 .19  0
termination-15/cstrcspn_reverse_alloca_true-termination.c.i error (134) .29 46 2.0 0 true 71   4100 630 2 error (42) 880     13000   7400    0 out of memory 200     15000   2500    0 timeout 900   3700 12000 0 unknown 1.3  67 15   0 unknown .029 4.6 .23 0 unknown .028 4.6 .23  0 timeout 900     1200 10000    0 timeout 900   3700 12000 0 error (8) .73 64 6.1 0 disqualified .043 9.5 .45 0 timeout (verification) 900    120 8300   0 true 22   620 210 2 error (5) .026 5.6 .16  0 error (5) .040 5.6 .089 0
termination-15/cstrlen_diffterm_alloca_true-termination.c.i error (134) .24 46 2.2 0 true 8.5 570 65 2 error (42) 880     6300   3300    0 error (42) 880     350   7300    0 unknown 22   940 200 0 unknown .93 67 13   0 unknown .057 4.6 .15 0 unknown .029 4.6 .19  0 timeout 900     2000 12000    0 unknown 30   1400 260 0 timeout 900    1200 13000   0 disqualified .043 9.5 .46 0 timeout (verification) 900    350 13000   0 true 11   460 91 2 error (5) .023 5.5 .23  0 error (5) .025 5.6 .12  0
termination-15/cstrlen_malloc_true-termination.c.i error (134) .27 46 2.1 0 true 9.2 720 70 2 error (42) 880     6300   3500    0 error (42) 880     340   6700    0 unknown 30   1000 250 0 unknown .92 65 12   0 unknown .030 4.8 .18 0 unknown .030 4.6 .21  0 timeout 900     2100 11000    0 unknown 23   930 190 0 timeout 900    1100 10000   0 disqualified .046 9.2 .38 0 timeout (verification) 900    110 13000   0 true 10   440 82 2 error (5) .043 5.5 .14  0 error (5) .024 5.6 .11  0
termination-15/cstrlen_reverse_alloca_true-termination.c.i error (134) .26 46 1.9 0 true 8.6 570 73 2 error (42) 880     13000   4900    0 error (42) 880     13000   6100    0 unknown 37   1500 320 0 unknown .93 66 10   0 unknown .026 4.6 .21 0 unknown .053 4.7 .16  0 timeout 900     2300 12000    0 unknown 32   1300 290 0 error (8) .72 64 6.2 0 disqualified .046 9.8 .47 0 timeout (verification) 900    120 6600   0 true 11   460 82 2 error (5) .030 5.6 .19  0 error (5) .049 5.7 .096 0
termination-15/cstrncat_diffterm_alloca_true-termination.c.i error (134) .28 46 1.8 0 error (1) 96   2500 790 0 error (42) 880     14000   7400    0 error (42) 880     2400   7700    0 timeout 900   4200 12000 0 unknown 1.0  68 10   0 unknown .053 4.6 .17 0 unknown .027 4.6 .22  0 timeout 900     2200 9800    0 timeout 900   4200 11000 0 timeout 900    1300 12000   0 disqualified .046 9.5 .40 0 timeout (verification) 900    310 11000   0 true 12   600 100 2 error (5) .026 5.5 .12  0 error (5) .025 5.6 .11  0
termination-15/cstrncat_malloc_true-termination.c.i error (134) .27 46 2.2 0 error (1) 110   2700 930 0 out of memory 150     13000   1400    0 error (42) 880     1800   9500    0 timeout 900   4200 12000 0 unknown .98 66 10   0 unknown .059 4.8 .16 0 unknown .033 4.7 .23  0 timeout 900     2200 9400    0 timeout 900   4200 12000 0 timeout 900    1100 11000   0 disqualified .085 9.4 .32 0 timeout (verification) 900    410 11000   0 true 12   580 94 2 error (5) .032 5.6 .18  0 error (5) .051 5.6 .13  0
termination-15/cstrncat_mixed_alloca_true-termination.c.i error (134) .27 46 1.6 0 error (1) 92   2200 810 0 error (42) 870     14000   7200    0 error (42) 880     2400   7800    0 timeout 900   4100 12000 0 unknown 1.1  67 10   0 unknown .025 4.8 .34 0 unknown .031 4.6 .19  0 timeout 900     2100 12000    0 timeout 900   4000 10000 0 timeout 900    1100 12000   0 disqualified .048 9.2 .36 0 timeout (verification) 900    180 13000   0 true 12   500 110 2 error (5) .031 5.6 .13  0 error (5) .025 5.6 .14  0
termination-15/cstrncat_reverse_alloca_true-termination.c.i error (134) .25 46 2.0 0 error (1) 84   3900 830 0 error (42) 880     14000   7100    0 error (42) 880     2400   8500    0 timeout 900   4300 13000 0 unknown 1.0  67 11   0 unknown .028 4.7 .25 0 unknown .027 4.6 .25  0 timeout 900     2200 11000    0 timeout 900   4400 12000 0 error (8) .74 64 6.6 0 disqualified .047 9.6 .45 0 timeout (verification) 900    99 12000   0 true 12   550 100 2 error (5) .028 5.7 .20  0 error (5) .025 5.7 .18  0
termination-15/cstrncmp_diffterm_alloca_true-termination.c.i error (134) .25 46 2.0 0 true 28   2300 260 2 error (42) 880     1100   9100    0 error (42) 880     260   7600    0 timeout 900   3400 11000 0 unknown 1.0  67 11   0 unknown .028 4.6 .17 0 unknown .049 4.6 .24  0 timeout 900     1600 13000    0 timeout 900   3100 13000 0 out of memory 72    15000 720   0 disqualified .050 9.1 .49 0 timeout (verification) 900    230 14000   0 true 12   590 110 2 error (5) .026 5.7 .094 0 error (5) .032 5.7 .13  0
termination-15/cstrncmp_malloc_true-termination.c.i error (134) .28 47 1.9 0 true 26   2300 260 2 error (42) 880     1400   11000    0 error (42) 880     250   8600    0 timeout 900   3300 13000 0 unknown .99 64 12   0 unknown .029 4.6 .14 0 unknown .031 4.6 .14  0 timeout 900     1600 11000    0 timeout 900   3100 14000 0 out of memory 65    15000 740   0 disqualified .047 9.1 .38 0 timeout (verification) 900    120 14000   0 true 11   500 97 2 error (5) .036 5.7 .17  0 error (5) .051 5.5 .10  0
termination-15/cstrncmp_mixed_alloca_true-termination.c.i error (134) .25 46 1.9 0 true 27   2300 230 2 error (42) 880     13000   8200    0 error (42) 880     4300   6400    0 timeout 900   3300 12000 0 unknown .98 66 11   0 unknown .033 4.8 .14 0 unknown .026 4.6 .24  0 timeout 900     1700 11000    0 timeout 900   2700 11000 0 error (8) .74 64 7.0 0 disqualified .044 9.0 .43 0 timeout (verification) 900    110 8900   0 true 13   590 100 2 error (5) .024 5.5 .19  0 error (5) .024 5.6 .11  0
termination-15/cstrncmp_reverse_alloca_true-termination.c.i error (134) .26 47 2.3 0 true 27   2300 240 2 error (42) 880     13000   6600    0 error (42) 880     8400   6900    0 timeout 900   3300 11000 0 unknown .97 65 10   0 unknown .024 4.8 .36 0 unknown .052 4.8 .17  0 timeout 900     1900 10000    0 timeout 900   3000 11000 0 error (8) .70 64 6.8 0 disqualified .053 9.5 .52 0 timeout (verification) 900    120 7200   0 true 11   540 100 2 error (5) .049 5.5 .12  0 error (5) .030 5.7 .13  0
termination-15/cstrncpy_diffterm_alloca_true-termination.c.i error (134) .30 46 1.9 0 timeout 900   4200 10000 0 error (42) 880     14000   9500    0 error (42) 880     5200   6500    0 timeout 900   4700 13000 0 unknown 1.2  66 13   0 unknown .028 4.6 .22 0 unknown .030 4.6 .21  0 timeout 900     6700 10000    0 timeout 900   4600 11000 0 error (8) .70 64 8.8 0 disqualified .047 9.6 .51 0 timeout (verification) 900    340 11000   0 true 16   610 140 2 error (5) .022 5.6 .20  0 error (5) .026 5.6 .12  0
termination-15/cstrncpy_malloc_true-termination.c.i error (134) .27 46 1.9 0 timeout 900   3500 11000 0 out of memory 270     13000   3100    0 error (42) 880     5300   11000    0 timeout 900   4600 11000 0 unknown 1.2  67 13   0 unknown .032 4.6 .19 0 unknown .027 4.8 .15  0 timeout 900     6700 8400    0 unknown 620   4400 7000 0 error (8) .71 64 8.4 0 disqualified .061 9.1 .32 0 timeout (verification) 900    340 12000   0 true 16   650 120 2 error (5) .026 5.5 .22  0 error (5) .022 5.6 .16  0
termination-15/cstrncpy_mixed_alloca_true-termination.c.i error (134) .29 46 2.4 0 error (1) 68   2500 600 0 error (42) 880     14000   9300    0 error (42) 880     15000   8700    0 timeout 900   4800 11000 0 unknown 1.4  65 16   0 unknown .037 4.6 .24 0 unknown .027 4.7 .35  0 timeout 900     1600 8700    0 timeout 900   4700 13000 0 timeout 900    770 5500   0 disqualified .042 9.0 .50 0 timeout (verification) 900    440 13000   0 true 15   640 140 2 error (5) .025 5.6 .14  0 error (5) .030 5.6 .12  0
termination-15/cstrncpy_reverse_alloca_true-termination.c.i error (134) .26 46 2.0 0 error (1) 64   2500 500 0 error (42) 880     14000   11000    0 error (42) 880     15000   7300    0 timeout 900   4300 11000 0 unknown 1.4  66 17   0 unknown .057 4.6 .16 0 unknown .028 4.6 .21  0 timeout 900     1600 9300    0 timeout 900   4300 12000 0 error (8) .72 64 6.5 0 disqualified .043 9.4 .37 0 timeout (verification) 900    430 13000   0 true 15   660 120 2 error (5) .025 5.7 .15  0 error (5) .029 5.6 .23  0
termination-15/cstrpbrk_diffterm_alloca_true-termination.c.i error (134) .26 46 2.1 0 true 55   3700 420 2 error (42) 880     990   5500    0 out of memory 190     15000   2500    0 timeout 900   3700 12000 0 unknown 1.2  67 13   0 unknown .029 4.6 .15 0 unknown .030 4.6 .21  0 timeout 900     1900 9000    0 timeout 900   3700 13000 0 timeout 900    710 6700   0 disqualified .072 9.2 .39 0 timeout (verification) 900    550 11000   0 true 40   1600 320 2 error (5) .023 5.6 .019 0 error (5) .041 5.7 .13  0
termination-15/cstrpbrk_malloc_true-termination.c.i error (134) .27 46 2.3 0 true 49   3300 360 2 error (42) 880     4200   8000    0 out of memory 190     15000   2200    0 timeout 900   3700 15000 0 unknown 1.1  66 15   0 unknown .028 4.7 .27 0 unknown .030 4.7 .19  0 timeout 900     1900 10000    0 timeout 900   3700 13000 0 timeout 900    660 5300   0 disqualified .047 9.2 .35 0 timeout (verification) 900    410 12000   0 true 41   1500 360 2 error (5) .023 5.7 .14  0 error (5) .021 5.9 .082 0
termination-15/cstrpbrk_mixed_alloca_true-termination.c.i error (134) .26 46 2.0 0 true 44   3500 360 2 error (42) 880     13000   6200    0 out of memory 190     15000   2400    0 unknown 290   3700 4100 0 unknown 1.3  67 14   0 unknown .030 4.8 .12 0 unknown .029 4.6 .15  0 timeout 900     1400 10000    0 timeout 900   4100 15000 0 error (8) .72 64 7.2 0 disqualified .063 9.1 .35 0 timeout (verification) 900    580 11000   0 true 21   750 190 2 error (5) .025 5.7 .13  0 error (5) .020 5.7 .17  0
termination-15/cstrpbrk_reverse_alloca_true-termination.c.i error (134) .26 46 1.9 0 true 57   5400 430 2 error (42) 880     13000   7000    0 out of memory 190     15000   2600    0 timeout 900   3700 10000 0 unknown 1.3  67 20   0 unknown .037 4.7 .27 0 unknown .029 4.7 .24  0 timeout 900     1300 10000    0 timeout 900   3700 13000 0 error (8) .68 64 9.8 0 disqualified .080 9.2 .35 0 timeout (verification) 900    120 8700   0 true 23   650 210 2 error (5) .029 5.6 .15  0 error (5) .026 5.6 .13  0
termination-15/cstrspn_diffterm_alloca_true-termination.c.i error (134) .24 46 2.4 0 true 58   2800 480 2 error (42) 880     990   7700    0 out of memory 190     15000   2900    0 timeout 900   3700 12000 0 unknown 1.1  66 13   0 unknown .030 4.6 .18 0 unknown .028 4.6 .24  0 timeout 900     1800 9100    0 timeout 900   3700 14000 0 timeout 900    710 6600   0 disqualified .046 9.4 .40 0 timeout (verification) 900    550 9500   0 true 22   760 190 2 error (5) .026 5.6 .17  0 error (5) .026 5.6 .15  0
termination-15/cstrspn_malloc_true-termination.c.i error (134) .26 46 1.9 0 true 54   4400 470 2 error (42) 880     4200   5300    0 out of memory 190     15000   2200    0 timeout 900   3700 12000 0 unknown 1.1  67 14   0 unknown .030 4.6 .20 0 unknown .028 4.8 .20  0 timeout 900     1800 9300    0 timeout 900   3700 14000 0 timeout 900    620 5300   0 disqualified .048 9.7 .42 0 timeout (verification) 900    430 10000   0 true 21   600 200 2 error (5) .020 5.6 .19  0 error (5) .022 5.8 .12  0
termination-15/cstrspn_mixed_alloca_true-termination.c.i error (134) .28 46 1.8 0 true 54   3700 470 2 error (42) 880     13000   7600    0 out of memory 200     15000   2700    0 unknown 300   3700 3500 0 unknown 1.3  66 16   0 unknown .030 4.6 .20 0 unknown .029 4.7 .23  0 timeout 900     1300 12000    0 timeout 900   4100 13000 0 error (8) .70 64 8.5 0 disqualified .045 9.4 .47 0 timeout (verification) 900    580 11000   0 true 23   750 210 2 error (5) .024 5.5 .20  0 error (5) .025 5.6 .069 0
termination-15/cstrspn_reverse_alloca_true-termination.c.i error (134) .25 46 2.2 0 true 59   3800 510 2 error (42) 870     13000   6500    0 out of memory 200     15000   2800    0 timeout 900   3700 14000 0 unknown 1.3  65 17   0 unknown .030 4.6 .21 0 unknown .043 4.7 .13  0 timeout 900     1300 10000    0 timeout 900   3700 14000 0 error (8) .73 64 6.8 0 disqualified .045 9.3 .39 0 timeout (verification) 900    120 9500   0 true 22   610 180 2 error (5) .023 5.7 .073 0 error (5) .023 5.7 .15  0
termination-15/array04_alloca_false-termination.c.i error (134) .27 46 1.9 0 false(termination) 32   1500 240 1 error (42) 880     14000   7400    0 error (42) 880     9200   8300    0 false(termination) 8.2 390 75 1 unknown .96 67 11   0 unknown .032 4.6 .32 0 unknown .031 4.6 .16  0 timeout 900     340 13000    0 false(termination) 7.5 340 73 1 timeout 900    1500 11000   0 disqualified .052 9.0 .41 0 timeout (verification) 900    110 9300   0 false(termination) 12   460 91 1 error (5) .026 5.6 .26  0 error (5) .026 5.7 .15  0
termination-15/array14_alloca_false-termination.c.i error (134) .25 46 1.9 0 error (1) 65   4600 770 0 error (42) 880     14000   10000    0 out of memory 220     15000   3000    0 timeout 900   4400 11000 0 unknown 1.0  66 12   0 unknown .033 4.6 .26 0 unknown .032 4.6 .18  0 timeout 900     860 12000    0 timeout 900   4400 13000 0 timeout 900    1000 6400   0 disqualified .042 9.4 .44 0 timeout (verification) 900    280 5500   0 false(termination) 17   530 140 1 error (5) .025 5.6 .13  0 error (5) .029 5.6 .18  0
termination-15/array15_alloca_false-termination.c.i error (134) .26 46 1.9 0 error (1) 58   2300 740 0 error (42) 880     14000   11000    0 out of memory 220     15000   2900    0 timeout 900   4400 12000 0 unknown 1.0  66 13   0 unknown .027 4.6 .21 0 unknown .028 4.6 .16  0 timeout 900     630 12000    0 timeout 900   4500 12000 0 timeout 900    1000 5900   0 disqualified .046 9.3 .35 0 timeout (verification) 900    220 5700   0 false(termination) 17   590 150 1 error (5) .031 5.8 .17  0 error (5) .024 5.7 .15  0
termination-15/array16_alloca_original_false-termination.c.i error (134) .27 46 1.8 0 out of memory 570   15000 3000 0 error (42) 880     14000   9700    0 out of memory 220     15000   2600    0 timeout 900   5300 9900 0 unknown 1.0  65 11   0 unknown .031 4.6 .21 0 unknown .031 4.7 .17  0 timeout 900     2800 11000    0 timeout 900   5200 11000 0 timeout 900    1300 4600   0 disqualified .046 9.1 .43 0 timeout (verification) 900    220 6400   0 false(termination) 19   550 180 1 error (5) .031 5.6 .21  0 error (5) .023 5.6 .13  0
termination-15/array19_alloca_false-termination.c.i error (134) .26 46 1.8 0 false(termination) 30   1500 220 1 error (42) 880     14000   6700    0 error (42) 880     9200   6600    0 false(termination) 8.0 390 71 1 unknown .99 67 11   0 unknown .025 4.6 .20 0 unknown .029 4.6 .19  0 timeout 900     260 12000    0 false(termination) 7.8 380 77 1 timeout 900    1600 12000   0 disqualified .046 9.3 .38 0 timeout (verification) 900    210 9000   0 false(termination) 11   460 92 1 error (5) .024 5.6 .17  0 error (5) .027 5.6 .15  0
termination-15/array20_alloca_false-termination.c.i error (134) .24 46 2.0 0 timeout 900   13000 5000 0 error (42) 880     14000   8800    0 out of memory 490     15000   6300    0 exception 5.3 310 53 0 unknown .97 66 12   0 unknown .033 4.6 .21 0 unknown .028 4.6 .16  0 timeout 900     240 12000    0 exception 5.1 320 53 0 timeout 900    1000 6800   0 disqualified .053 9.2 .35 0 timeout (verification) 900    350 5100   0 false(termination) 13   490 110 1 error (5) .047 5.5 .12  0 error (5) .025 5.6 .20  0
termination-recursive-malloc/chunk1_true-termination.c.i error (134) .25 47 1.8 0 error (1) 5.7 420 49 0 out of memory 540     15000   2800    0 error (42) 880     930   9000    0 unknown 830   4100 11000 0 unknown .85 66 7.6 0 unknown .031 4.6 .19 0 unknown .029 4.6 .15  0 timeout 900     1200 12000    0 error (recursion) 3.2 270 31 0 timeout 900    3500 3900   0 disqualified .043 9.2 .42 0 timeout (verification) 900    450 9200   0 true 9.2 400 86 2 error (5) .048 5.5 .097 0 error (5) .045 5.4 .13  0
termination-recursive-malloc/chunk2_true-termination.c.i error (134) .28 47 2.1 0 error (1) 14   1200 110 0 error (134) .12  6.6 .51 0 error (134) .088 9.8 1.3  0 timeout 900   4100 10000 0 unknown 1.5  67 17   0 unknown .029 4.6 .19 0 unknown .029 4.6 .16  0 timeout 900     7600 8600    0 error (recursion) 3.4 270 32 0 out of memory 120    15000 1600   0 disqualified .044 9.6 .42 0 timeout (verification) 900    440 4800   0 error (7) 88   1200 1000 0 error (5) .044 5.6 .11  0 error (5) .027 5.7 .14  0
termination-recursive-malloc/chunk3_true-termination.c.i error (134) .27 47 2.3 0 error (1) 13   1200 120 0 error (134) .066 7.7 .75 0 error (134) .13  10   .87 0 timeout 900   4100 13000 0 unknown 2.1  91 26   0 unknown .039 4.6 .20 0 unknown .052 4.6 .20  0 timeout 900     4200 7800    0 error (recursion) 3.3 270 31 0 out of memory 65    15000 870   0 disqualified .044 9.4 .42 0 timeout (verification) 900    530 6500   0 error (7) 190   1300 2600 0 error (5) .027 5.6 .16  0 error (5) .020 5.6 .30  0
termination-recursive-malloc/insertionSort_recursive_true-termination.c.i error (134) .27 47 1.9 0 error (1) 15   1200 140 0 error (42) 880     14000   9100    0 out of memory 390     15000   5200    0 error (recursion) 4.5 290 39 0 unknown 1.3  66 14   0 unknown .052 4.6 .13 0 unknown .030 4.5 .15  0 timeout 900     6800 8400    0 error (recursion) 3.4 270 33 0 timeout 900    1000 4800   0 disqualified .046 9.2 .39 0 timeout (verification) 900    820 11000   0 true 31   850 270 2 error (5) .030 5.5 .17  0 error (5) .030 5.6 .12  0
termination-recursive-malloc/mergeSort_true-termination.c.i error (134) .25 47 1.8 0 error (1) 19   1200 170 0 out of memory 87     14000   960    0 out of memory 130     15000   1700    0 error (recursion) 3.9 280 35 0 unknown 900    10000 8000   0 unknown .027 4.5 .24 0 unknown .030 4.7 .21  0 timeout 900     4600 6000    0 error (recursion) 3.5 270 31 0 timeout 900    1000 5900   0 disqualified .047 9.5 .41 0 timeout (verification) 900    520 14000   0 error (7) 55   1300 560 0 error (5) .023 5.6 .15  0 error (5) .025 5.6 .18  0
termination-recursive-malloc/mutual_simple2_true-termination.c.i error (5) .26 47 2.5 0 true 11   710 97 2 error (6) 450     8200   3600    0 out of memory 210     15000   2500    0 timeout 910   4100 12000 0 unknown .82 67 9.8 0 unknown .056 4.8 .19 0 unknown .056 4.6 .22  0 timeout 900     2300 6100    0 error (recursion) 3.4 270 34 0 timeout 900    2300 9200   0 disqualified .044 9.1 .45 0 timeout (verification) 900    470 7200   0 true 12   590 110 2 error (5) .026 5.6 .18  0 error (5) .026 5.6 .16  0
termination-recursive-malloc/mutual_simple_true-termination.c.i error (5) .26 47 2.1 0 true 6.2 320 52 2 error (42) 880     15000   8000    0 error (42) 880     1000   10000    0 true 6.8 480 58 2 unknown .81 66 9.5 0 unknown .029 4.8 .16 0 unknown .027 4.7 .18  0 timeout 900     1200 10000    0 error (recursion) 3.2 270 31 0 timeout 900    11000 5900   0 disqualified .049 9.1 .42 0 timeout (verification) 900    510 6600   0 true 11   470 83 2 error (5) .032 5.6 .14  0 error (5) .031 5.6 .16  0
termination-recursive-malloc/rec_malloc_ex10_true-termination.c.i error (5) .30 47 1.6 0 true 12   720 93 2 error (42) 880     7300   7900    0 out of memory 140     15000   1800    0 timeout 910   4300 13000 0 unknown .85 66 11   0 unknown .030 4.6 .19 0 unknown .045 4.6 .14  0 timeout 900     5600 8900    0 error (recursion) 3.2 270 33 0 timeout 900    3900 7100   0 disqualified .046 9.2 .49 0 timeout (verification) 900    440 9700   0 true 13   570 120 2 error (5) .022 5.6 .21  0 error (5) .023 5.6 .20  0
termination-recursive-malloc/rec_malloc_ex11B_true-termination.c.i error (5) .28 46 2.1 0 true 40   1900 240 2 error (42) 870     970   5400    0 out of memory 160     15000   1900    0 error (recursion) 4.4 280 36 0 unknown 2.1  110 26   0 unknown .031 4.6 .17 0 unknown .037 4.6 .26  0 timeout 900     3000 7200    0 error (recursion) 3.4 260 32 0 timeout 900    13000 9700   0 disqualified .052 9.2 .45 0 timeout (verification) 900    690 14000   0 true 20   550 190 2 error (5) .022 5.6 .19  0 error (5) .023 5.6 .15  0
termination-recursive-malloc/rec_malloc_ex11C_true-termination.c.i error (5) .29 47 2.1 0 true 24   1200 180 2 error (42) 880     940   6100    0 out of memory 150     15000   1900    0 error (recursion) 4.4 280 40 0 unknown 2.6  140 33   0 unknown .030 4.6 .19 0 unknown .034 4.6 .15  0 timeout 900     3600 7700    0 error (recursion) 3.3 270 32 0 out of memory 62    15000 770   0 disqualified .048 9.4 .37 0 timeout (verification) 900    860 12000   0 true 22   590 220 2 error (5) .030 5.7 .099 0 error (5) .026 5.6 .15  0
termination-recursive-malloc/rec_malloc_ex11D_true-termination.c.i error (5) .29 46 1.8 0 true 26   1400 190 2 error (42) 880     960   6100    0 out of memory 140     15000   2000    0 error (recursion) 4.1 280 36 0 unknown 2.5  130 26   0 unknown .026 4.6 .21 0 unknown .032 4.6 .23  0 timeout 900     3500 6800    0 error (recursion) 3.3 270 32 0 out of memory 63    15000 790   0 disqualified .060 9.1 .42 0 timeout (verification) 900    800 11000   0 true 21   760 210 2 error (5) .025 5.7 .064 0 error (5) .024 5.6 .11  0
termination-recursive-malloc/rec_malloc_ex11_true-termination.c.i error (5) .32 47 2.4 0 true 20   1100 140 2 error (42) 880     1100   6100    0 out of memory 170     15000   1900    0 error (recursion) 4.4 280 39 0 unknown 2.6  130 32   0 unknown .029 4.6 .19 0 unknown .052 4.6 .19  0 timeout 900     3600 7300    0 error (recursion) 3.3 270 33 0 out of memory 60    15000 680   0 disqualified .045 9.9 .48 0 timeout (verification) 900    680 12000   0 true 22   610 240 2 error (5) .046 5.5 .16  0 error (5) .024 5.6 .10  0
termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i error (5) .29 47 1.8 0 true 17   940 120 2 error (42) 880     1300   4600    0 out of memory 130     15000   1400    0 error (recursion) 4.2 280 41 0 unknown 1.9  92 23   0 unknown .029 4.7 .21 0 unknown .033 4.7 .28  0 timeout 900     3300 8600    0 error (recursion) 3.4 270 31 0 out of memory 63    15000 830   0 disqualified .045 9.3 .45 0 timeout (verification) 900    920 9000   0 timeout 900   900 12000 0 error (5) .033 5.5 .090 0 error (5) .036 5.5 .13  0
termination-recursive-malloc/rec_malloc_ex2_true-termination.c.i error (5) .30 46 2.1 0 true 23   1200 170 2 error (42) 870     1100   4500    0 out of memory 120     15000   1400    0 error (recursion) 4.3 280 41 0 unknown 1.4  74 14   0 unknown .028 4.6 .21 0 unknown .032 4.7 .28  0 timeout 900     5700 9300    0 error (recursion) 3.3 270 33 0 out of memory 58    15000 700   0 disqualified .051 9.4 .46 0 timeout (verification) 900    120 12000   0 true 27   790 230 2 error (5) .023 5.6 .11  0 error (5) .032 5.7 .17  0
termination-recursive-malloc/rec_malloc_ex3_true-termination.c.i error (5) .26 47 1.9 0 true 31   1500 210 2 error (42) 880     620   3600    0 out of memory 120     15000   1400    0 error (recursion) 4.1 280 39 0 unknown 1.2  66 13   0 unknown .035 4.6 .18 0 unknown .038 4.7 .13  0 timeout 900     4700 9600    0 error (recursion) 3.3 270 28 0 timeout 900    300 10000   0 disqualified .054 9.3 .45 0 timeout (verification) 900    350 11000   0 true 22   640 190 2 error (5) .047 5.7 .17  0 error (5) .027 5.7 .12  0
termination-recursive-malloc/rec_malloc_ex4_true-termination.c.i error (5) .26 47 2.5 0 true 13   1000 110 2 error (42) 880     7600   7600    0 out of memory 150     15000   1800    0 timeout 910   4200 11000 0 unknown .86 66 9.4 0 unknown .032 4.6 .23 0 unknown .031 4.7 .24  0 timeout 900     4800 11000    0 error (recursion) 3.3 270 30 0 timeout 900    3100 6500   0 disqualified .046 9.5 .49 0 timeout (verification) 900    360 8900   0 true 12   480 110 2 error (5) .028 5.5 .16  0 error (5) .025 5.6 .15  0
termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i error (5) .36 47 2.5 0 true 64   3300 420 2 error (42) 880     680   5000    0 out of memory 120     15000   1600    0 error (recursion) 4.0 270 35 0 unknown 2.6  180 31   0 unknown .031 4.6 .19 0 unknown .029 4.6 .22  0 timeout 900     5900 7700    0 error (recursion) 3.3 270 28 0 out of memory 96    15000 1500   0 disqualified .047 9.4 .41 0 timeout (verification) 900    1100 8300   0 timeout 900   1700 5700 0 error (5) .025 5.6 .16  0 error (5) .030 5.6 .20  0
termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i error (5) .30 47 2.3 0 true 18   1400 130 2 error (6) 450     770   2800    0 out of memory 180     15000   2000    0 timeout 910   4200 11000 0 unknown 1.5  100 19   0 unknown .029 4.6 .11 0 unknown .027 4.6 .22  0 timeout 900     9400 9200    0 error (recursion) 3.4 270 32 0 out of memory 120    15000 1700   0 disqualified .052 8.9 .34 0 timeout (verification) 900    800 6900   0 true 23   750 210 2 error (5) .026 5.6 .10  0 error (5) .027 5.6 .20  0
termination-recursive-malloc/rec_malloc_ex6_true-termination.c.i error (5) .25 47 2.0 0 error (1) 16   970 150 0 out of memory 600     15000   3600    0 error (42) 880     2000   7500    0 timeout 900   4100 11000 0 unknown .84 67 9.5 0 unknown .030 4.7 .19 0 unknown .033 4.6 .20  0 timeout 900     8200 7600    0 error (recursion) 3.3 270 25 0 timeout 900    880 9100   0 disqualified .046 9.3 .34 0 error(unknown, verification-finished) 52    2500 660   0 unknown 39   1100 330 0 error (5) .027 5.6 .16  0 error (5) .025 5.6 .11  0
termination-recursive-malloc/rec_malloc_ex7B_true-termination.c.i error (5) .26 46 1.9 0 true 9.1 650 75 2 error (6) 750     10000   6500    0 out of memory 270     15000   4000    0 unknown 840   4200 9400 0 unknown .84 67 9.0 0 unknown .030 4.6 .22 0 unknown .030 4.6 .17  0 timeout 900     5200 11000    0 error (recursion) 3.3 270 31 0 timeout 900    3200 8400   0 disqualified .049 9.7 .46 0 timeout (verification) 900    390 11000   0 true 13   520 92 2 error (5) .040 5.6 .14  0 error (5) .021 5.6 .16  0
termination-recursive-malloc/rec_malloc_ex7_true-termination.c.i error (5) .26 46 2.1 0 true 10   660 84 2 error (6) 840     10000   7500    0 out of memory 280     15000   3200    0 unknown 830   4200 12000 0 unknown .83 67 8.9 0 unknown .038 4.7 .13 0 unknown .029 4.8 .25  0 timeout 900     5000 11000    0 error (recursion) 3.2 270 27 0 timeout 900    3000 8100   0 disqualified .046 9.2 .45 0 timeout (verification) 900    440 11000   0 unknown 35   1100 320 0 error (5) .031 5.5 .20  0 error (5) .025 5.6 .14  0
termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i error (5) .26 46 2.2 0 true 12   1100 100 2 error (6) 160     3800   1500    0 out of memory 270     15000   3100    0 timeout 900   4100 11000 0 unknown .85 65 9.8 0 unknown .029 4.6 .18 0 unknown .045 4.6 .19  0 timeout 900     6200 6700    0 error (recursion) 3.3 270 30 0 timeout 900    1400 9500   0 disqualified .049 9.4 .40 0 timeout (verification) 900    430 13000   0 unknown 41   1200 340 0 error (5) .024 5.6 .17  0 error (5) .023 5.6 .15  0
termination-recursive-malloc/rec_malloc_ex9_true-termination.c.i error (5) .28 46 2.1 0 true 15   940 110 2 error (42) 880     1300   4700    0 out of memory 120     15000   1700    0 error (recursion) 4.1 280 35 0 unknown 1.8  89 18   0 unknown .033 4.6 .26 0 unknown .035 4.8 .23  0 timeout 900     3300 6300    0 error (recursion) 3.4 270 30 0 out of memory 75    15000 960   0 disqualified .045 9.4 .38 0 timeout (verification) 900    680 8200   0 timeout 900   1200 11000 0 error (5) .023 5.6 .20  0 error (5) .026 5.7 .18  0
termination-recursive-malloc/rec_strcopy_malloc2_true-termination.c.i error (134) .26 47 1.9 0 error (1) 16   1200 150 0 out of memory 330     14000   3500    0 error (42) 880     2700   7300    0 error (recursion) 8.0 360 71 0 unknown .94 66 8.8 0 unknown .035 4.6 .16 0 unknown .027 4.6 .19  0 timeout 900     2300 9600    0 error (recursion) 3.5 270 31 0 out of memory 98    15000 1500   0 disqualified .049 9.9 .39 0 timeout (verification) 900    820 12000   0 true 14   500 110 2 error (5) .025 5.6 .11  0 error (5) .024 5.6 .18  0
termination-recursive-malloc/rec_strcopy_malloc_true-termination.c.i error (134) .25 46 2.0 0 error (1) 6.7 490 60 0 out of memory 160     13000   1800    0 error (42) 880     5900   10000    0 unknown 670   4500 8800 0 unknown .92 67 10   0 unknown .032 4.6 .17 0 unknown .037 4.6 .18  0 timeout 900     2900 9000    0 error (recursion) 3.4 270 34 0 error (8) .67 60 6.4 0 disqualified .045 9.4 .46 0 timeout (verification) 900    310 13000   0 true 12   570 94 2 error (5) .024 5.6 .18  0 error (5) .028 5.5 .12  0
termination-recursive-malloc/rec_strlen_malloc_true-termination.c.i error (134) .26 46 1.7 0 true 8.2 520 63 2 out of memory 810     15000   5600    0 error (42) 880     600   9700    0 unknown 7.1 470 65 0 unknown .92 65 9.8 0 unknown .029 4.5 .22 0 unknown .055 4.7 .27  0 timeout 900     1600 9500    0 error (recursion) 3.4 270 31 0 out of memory 210    15000 2400   0 disqualified .045 9.3 .44 0 timeout (verification) 900    130 11000   0 true 8.8 400 84 2 error (5) .032 5.6 .13  0 error (5) .025 5.7 .10  0
termination-recursive-malloc/selectionSort_recursive_true-termination.c.i error (134) .23 46 2.6 0 error (1) 15   900 140 0 error (42) 880     14000   7100    0 out of memory 120     15000   1500    0 error (recursion) 4.3 280 38 0 unknown 1.3  66 14   0 unknown .033 4.6 .28 0 unknown .045 4.6 .13  0 timeout 900     2500 9600    0 error (recursion) 3.4 270 31 0 timeout 900    1000 4400   0 disqualified .047 8.9 .37 0 timeout (verification) 900    120 7800   0 true 20   730 190 2 error (5) .050 5.6 .12  0 error (5) .049 5.6 .11  0
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 259 42000    500000 460000   -26 259 34000 690000 280000 340 259 210000 1900000 1700000 24 259 150000 2300000 1400000 22 259 140000 750000 1800000 65 259 1100   23000 11000 0 259 9.0 1200 52 0 259 9.1 1200 52 0 259 220000 580000 2600000 24 259 130000 680000 1800000 59 259 150000 980000 1300000 22 259 13 2400 110 0 259 200000 220000 2300000 72 259 24000 240000 260000 405 259 7.4 1500 38 0 259 7.5 1500 37 0
    correct results 3 4.2  400 39   6 172 6100 320000 53000 340 12 16 330 210 24 11 13 180 170 22 34 4700 50000 57000 65 160 110   6200 1400 320 0 0 12 510 3100 6700 24 31 4400 47000 58000 59 11 120 1600 1700 22 0 36 10 610 120 72 210 4900 150000 48000 405 0 0
        correct true 3 4.2  400 39   6 168 6000 320000 53000 336 12 16 330 210 24 11 13 180 170 22 31 4600 49000 57000 62 160 110   6200 1400 320 0 0 12 510 3100 6700 24 28 4400 46000 58000 56 11 120 1600 1700 22 0 36 10 610 120 72 195 4700 140000 46000 390 0 0
        correct false 0 4 85 3900 620 4 0 0 3 25 1200 220 3 0 0 0 0 3 24 1200 230 3 0 0 0 15 260 9700 2200 15 0 0
    incorrect results 2 .74 99 4.9 -32 0 0 0 0 10 4.2 360 54 -320 0 0 0 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 10 4.2 360 54 -320 0 0 0 0 0 0 0 0 0 0
        incorrect false 2 .74 99 4.9 -32 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (259 tasks, max score: 502) -26 340 24 22 65 0 0 0 24 59 22 0 72 405 0 0
Run set 2ls.sv-comp19_prop-termination.Termination-MainHeap aprove.sv-comp19_prop-termination.Termination-MainHeap cbmc.sv-comp19_prop-termination.Termination-MainHeap cbmc-path.sv-comp19_prop-termination.Termination-MainHeap cpa-seq.sv-comp19_prop-termination.Termination-MainHeap depthk.sv-comp19_prop-termination.Termination-MainHeap divine-explicit.sv-comp19_prop-termination.Termination-MainHeap divine-smt.sv-comp19_prop-termination.Termination-MainHeap esbmc-kind.sv-comp19_prop-termination.Termination-MainHeap pesco.sv-comp19_prop-termination.Termination-MainHeap pinaka.sv-comp19_prop-termination.Termination-MainHeap smack.sv-comp19_prop-termination.Termination-MainHeap symbiotic.sv-comp19_prop-termination.Termination-MainHeap uautomizer.sv-comp19_prop-termination.Termination-MainHeap ukojak.sv-comp19_prop-termination.Termination-MainHeap utaipan.sv-comp19_prop-termination.Termination-MainHeap