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-MainControlFlow aprove.sv-comp19_prop-termination.Termination-MainControlFlow cbmc.sv-comp19_prop-termination.Termination-MainControlFlow cbmc-path.sv-comp19_prop-termination.Termination-MainControlFlow cpa-seq.sv-comp19_prop-termination.Termination-MainControlFlow depthk.sv-comp19_prop-termination.Termination-MainControlFlow divine-explicit.sv-comp19_prop-termination.Termination-MainControlFlow divine-smt.sv-comp19_prop-termination.Termination-MainControlFlow esbmc-kind.sv-comp19_prop-termination.Termination-MainControlFlow pesco.sv-comp19_prop-termination.Termination-MainControlFlow pinaka.sv-comp19_prop-termination.Termination-MainControlFlow smack.sv-comp19_prop-termination.Termination-MainControlFlow symbiotic.sv-comp19_prop-termination.Termination-MainControlFlow uautomizer.sv-comp19_prop-termination.Termination-MainControlFlow ukojak.sv-comp19_prop-termination.Termination-MainControlFlow utaipan.sv-comp19_prop-termination.Termination-MainControlFlow
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-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety_true-no-overflow.c false(termination) 7.7   220 96    1 false(termination) 7.6 340 57 1 error (42) 880     4700   3700    0 error (42) 870     2500   5300    0 timeout 900   4300 11000 0 unknown .81 66 8.4 0 unknown .030 4.6 .18  0 unknown .039 4.6 .22  0 timeout 900     1100 11000    0 timeout 900   4100 12000 0 timeout 900    1700 5200   0 disqualified .045 9.2 .47 0 timeout (verification) 900    63 9800   0 false(termination) 8.7 370 63 1 error (5) .025 5.6 .12  0 error (5) .024 5.6 .10  0
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) .16  24 1.0  1 false(termination) 6.8 340 49 1 error (42) 880     6500   4700    0 error (42) 880     390   5300    0 false(termination) 3.5 280 32 1 unknown .77 65 7.5 0 unknown .026 4.6 .23  0 unknown .034 4.6 .19  0 timeout 900     160 12000    0 false(termination) 3.5 280 31 1 timeout 900    540 5100   0 disqualified .050 9.4 .49 0 timeout (verification) 900    75 14000   0 false(termination) 7.1 350 58 1 error (5) .029 5.6 .15  0 error (5) .025 5.6 .12  0
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c error (5) .096 24 .77 0 error (1) 26   1400 210 0 error (42) 880     13000   8900    0 out of memory 300     15000   3700    0 false(termination) 5.2 310 45 1 out of memory 300    15000 3900   0 unknown .030 4.6 .22  0 unknown .054 4.6 .13  0 out of memory 380     15000 3500    0 error (recursion) 3.3 270 29 0 out of memory 210    15000 2700   0 disqualified .046 9.7 .46 0 timeout (verification) 900    93 12000   0 false(termination) 8.6 370 77 1 error (5) .023 5.6 .10  0 error (5) .036 5.5 .12  0
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c error (5) .45  35 4.7  0 false(termination) 12   510 83 0 error (42) 880     6100   3100    0 error (42) 880     380   5500    0 unknown 6.9 450 63 0 unknown .78 66 9.8 0 unknown .030 4.6 .21  0 unknown .029 4.6 .17  0 timeout 900     900 10000    0 unknown 7.1 470 63 0 timeout 900    400 3800   0 disqualified .047 9.5 .41 0 timeout (verification) 900    260 12000   0 unknown 65   570 710 0 error (5) .024 5.6 .12  0 error (5) .069 5.6 .14  0
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) .15  24 1.1  1 false(termination) 6.5 350 53 1 error (42) 880     6200   3800    0 error (42) 870     820   6000    0 false(termination) 3.9 280 35 1 unknown .80 65 8.3 0 unknown .028 4.6 .21  0 unknown .029 4.6 .14  0 timeout 900     1000 11000    0 false(termination) 3.9 280 36 1 timeout 900    1500 5000   0 disqualified .048 9.6 .45 0 timeout (verification) 900    1100 11000   0 false(termination) 7.8 370 63 1 error (5) .051 5.5 .13  0 error (5) .024 5.6 .12  0
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) .13  24 1.0  1 false(termination) 2.9 230 25 1 out of memory 180     15000   2500    0 out of memory 140     15000   1900    0 false(termination) 3.6 280 33 1 unknown .78 66 8.9 0 unknown .030 4.6 .24  0 unknown .030 4.6 .22  0 timeout 900     14000 9900    0 false(termination) 3.6 280 38 1 out of memory 860    15000 11000   0 disqualified .046 9.2 .42 0 false(termination) .13 15 1.6 1 false(termination) 7.9 340 54 1 error (5) .027 5.6 .13  0 error (5) .024 5.6 .10  0
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c error (5) .11  24 .72 0 error (1) 11   510 92 0 error (42) 880     220   3300    0 out of memory 310     15000   4400    0 error (recursion) 6.8 300 65 0 out of memory (false(no-overflow)) 230    15000 2900   0 unknown .023 4.6 .27  0 unknown .028 4.6 .22  0 out of memory 290     15000 3500    0 error (recursion) 3.2 270 29 0 out of memory 39    15000 530   0 disqualified .046 9.8 .41 0 timeout (verification) 900    850 9200   0 false(termination) 11   490 91 0 error (5) .032 5.6 .12  0 error (5) .034 5.6 .15  0
termination-crafted/Mysore_false-termination_true-valid-memsafety.c timeout 900     3000 12000    0 timeout 900   2300 14000 0 error (42) 880     5700   4400    0 error (42) 880     570   4900    0 unknown 11   720 98 0 unknown .77 65 9.5 0 unknown .033 4.7 .24  0 unknown .029 4.6 .23  0 timeout 900     230 11000    0 unknown 14   900 130 0 timeout 900    740 4700   0 disqualified .044 9.9 .45 0 timeout (verification) 900    19 11000   0 unknown 43   700 430 0 error (5) .024 5.6 .11  0 error (5) .032 5.6 .11  0
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c error (5) .096 24 .73 0 error (1) 17   790 130 0 error (42) 870     390   3800    0 error (42) 880     450   4700    0 false(termination) 5.9 320 53 1 out of memory 210    15000 2700   0 unknown .028 4.6 .30  0 unknown .029 4.6 .22  0 out of memory 350     15000 4100    0 error (recursion) 3.3 270 33 0 out of memory 760    15000 9500   0 disqualified .042 8.9 .46 0 timeout (verification) 900    7600 12000   0 false(termination) 8.7 360 68 1 error (5) .027 5.6 .17  0 error (5) .025 5.7 .16  0
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c error (5) .093 23 .85 0 error (1) 8.3 380 75 0 error (42) 880     720   4900    0 error (42) 880     920   7800    0 false(termination) 5.9 350 53 1 out of memory (false(no-overflow)) 200    15000 2500   0 unknown .045 4.6 .14  0 unknown .056 4.6 .17  0 out of memory 340     15000 3700    0 error (recursion) 3.2 270 30 0 out of memory 610    15000 9100   0 disqualified .046 9.5 .42 0 timeout (verification) 900    5000 9700   0 false(termination) 13   500 120 1 error (5) .054 5.5 .16  0 error (5) .023 5.6 .13  0
termination-crafted/NonTermination3_false-termination_false-valid-deref.c false(termination) .51  45 5.1  1 error (1) 15   660 110 0 error (42) 880     2200   12000    0 error (42) 880     870   6600    0 timeout 900   4400 11000 0 unknown .78 66 9.2 0 unknown .028 4.6 .20  0 unknown .036 4.7 .20  0 timeout 900     1800 11000    0 timeout 900   4200 12000 0 timeout 900    960 4900   0 disqualified .049 9.2 .38 0 timeout (verification) 900    170 11000   0 false(termination) 17   560 150 1 error (5) .026 5.6 .18  0 error (5) .024 5.6 .12  0
termination-crafted/NonTermination3_true-no-overflow_false-termination.c false(termination) .51  45 5.5  1 error (1) 13   600 110 0 error (42) 880     2200   10000    0 error (42) 880     920   8800    0 timeout 900   4300 11000 0 unknown .77 66 7.9 0 unknown .030 4.6 .19  0 unknown .045 4.5 .21  0 timeout 900     1400 12000    0 timeout 900   4200 11000 0 timeout 900    930 5000   0 disqualified .065 9.6 .44 0 timeout (verification) 900    150 8100   0 false(termination) 17   520 150 1 error (5) .054 5.5 .27  0 error (5) .027 5.6 .16  0
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) .15  24 .98 1 false(termination) 4.3 280 32 1 error (42) 880     6600   4300    0 error (42) 880     380   7000    0 false(termination) 3.7 280 31 1 unknown .79 66 9.3 0 unknown .035 4.6 .25  0 unknown .032 4.6 .24  0 timeout 900     770 11000    0 false(termination) 3.7 280 34 1 timeout 900    3400 3800   0 disqualified .057 9.1 .35 0 timeout (verification) 900    18 13000   0 false(termination) 8.4 370 62 1 error (5) .024 5.6 .094 0 error (5) .045 5.6 .11  0
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c error (5) .089 24 .84 0 false(termination) 10   510 85 0 out of memory 300     15000   1900    0 error (42) 880     1300   9000    0 false(termination) 4.0 280 39 1 unknown .82 66 8.3 0 unknown .029 4.6 .22  0 unknown .030 4.6 .22  0 timeout 900     1800 10000    0 error (recursion) 3.2 270 32 0 out of memory 580    15000 4200   0 disqualified .046 9.0 .44 0 timeout (verification) 900    51 13000   0 false(termination) 8.8 380 69 1 error (5) .025 5.6 .15  0 error (5) .022 5.7 .18  0
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c false(termination) .16  24 1.3  1 false(termination) 5.3 340 44 1 out of memory 270     15000   3500    0 out of memory 200     15000   2900    0 false(termination) 3.7 280 33 1 unknown .77 65 8.6 0 unknown .042 4.7 .22  0 unknown .028 4.6 .24  0 timeout 900     4600 11000    0 false(termination) 3.6 280 35 1 timeout 900    13000 11000   0 disqualified .047 9.1 .43 0 false(termination) .16 17 2.1 1 false(termination) 7.7 370 58 1 error (5) .049 5.6 .091 0 error (5) .026 5.6 .10  0
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) .16  24 .89 1 false(termination) 2.4 220 23 1 out of memory 150     15000   2000    0 out of memory 150     15000   2300    0 false(termination) 3.5 270 35 1 unknown .80 66 8.4 0 unknown .054 4.6 .15  0 unknown .031 4.6 .17  0 out of memory 280     15000 4000    0 false(termination) 3.6 280 28 1 out of memory 60    15000 920   0 disqualified .046 9.1 .40 0 false(termination) .13 15 1.2 1 false(termination) 7.4 350 65 1 error (5) .022 5.6 .10  0 error (5) .029 5.5 .15  0
termination-crafted/2Nested_true-termination_true-valid-memsafety.c timeout 900     2900 10000    0 true 7.4 390 52 2 error (42) 880     5200   3400    0 error (42) 880     410   6000    0 true 47   460 450 2 unknown .79 65 8.5 0 unknown .052 4.7 .14  0 unknown .031 4.6 .29  0 timeout 900     400 11000    0 true 78   440 930 2 timeout 900    6900 3900   0 disqualified .050 9.3 .42 0 timeout (verification) 900    300 7600   0 true 8.5 350 63 2 error (5) .028 5.7 .16  0 error (5) .025 5.7 .18  0
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true .45  59 3.1  2 true 4.1 330 36 2 true .13  8.0 1.8  2 true .19  8.1 1.3  2 timeout 910   4100 12000 0 unknown .81 66 8.2 0 unknown .031 4.6 .22  0 unknown .032 4.6 .24  0 true .089 26 .97 2 timeout 900   4000 12000 0 true .67 61 6.1 2 disqualified .045 9.4 .47 0 true .11 15 1.2 2 true 37   800 360 2 error (5) .025 5.5 .12  0 error (5) .030 5.5 .19  0
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c timeout 900     200 10000    0 true 19   1200 130 2 error (42) 880     820   5700    0 error (42) 870     1800   5800    0 timeout 900   4500 10000 0 unknown .81 67 9.2 0 unknown .054 4.7 .14  0 unknown .045 4.6 .15  0 timeout 900     300 11000    0 timeout 900   4500 12000 0 timeout 900    9400 5400   0 disqualified .047 9.1 .42 0 timeout (verification) 900    200 5800   0 true 21   370 250 2 error (5) .024 5.6 .11  0 error (5) .023 5.6 .16  0
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c error (5) .093 24 .84 0 true 29   2400 260 2 error (42) 880     250   4500    0 out of memory 170     15000   2000    0 true 6.3 350 56 2 out of memory 280    15000 3300   0 unknown .030 4.6 .15  0 unknown .031 4.6 .19  0 out of memory 450     15000 5500    0 error (recursion) 3.3 270 28 0 out of memory 53    15000 730   0 disqualified .051 9.3 .42 0 probably out of memory (killed (signal 9, verification)) 530    15000 8700   0 timeout 910   14000 4900 0 error (5) .024 5.6 .21  0 error (5) .025 5.7 .17  0
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c true 1.1   330 11    2 true 8.4 470 58 2 error (42) 880     5500   3800    0 error (42) 870     2000   5800    0 out of memory 370   15000 4200 0 unknown .80 66 9.3 0 unknown .027 4.6 .17  0 unknown .032 4.7 .20  0 timeout 900     1100 14000    0 out of memory 370   15000 4200 0 timeout 900    870 4300   0 disqualified .048 9.7 .43 0 true .14 17 1.6 2 timeout 900   960 11000 0 error (5) .023 5.6 .11  0 error (5) .024 5.6 .15  0
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c true 1.7   360 15    2 true 12   720 89 2 error (42) 880     6400   3400    0 error (42) 880     940   6100    0 out of memory 380   15000 5100 0 unknown .79 67 9.3 0 unknown .027 4.8 .25  0 unknown .029 4.7 .20  0 timeout 900     670 10000    0 out of memory 340   15000 4600 0 timeout 900    1300 4300   0 disqualified .063 9.3 .41 0 timeout (verification) 900    210 9900   0 timeout 900   760 12000 0 error (5) .025 5.7 .17  0 error (5) .024 5.6 .17  0
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true .14  24 1.1  2 true 5.2 300 36 2 error (42) 880     6200   4100    0 error (42) 880     380   6400    0 true 4.3 290 41 2 unknown .79 66 8.0 0 unknown .033 4.6 .25  0 unknown .030 4.7 .22  0 timeout 900     98 13000    0 true 4.4 290 41 2 timeout 900    500 6600   0 disqualified .043 9.1 .51 0 timeout (verification) 900    71 12000   0 true 7.8 340 60 2 error (5) .022 5.7 .11  0 error (5) .050 5.6 .092 0
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1900 11000    0 true 2.7 220 25 2 true .12  5.9 .36 2 true .053 6.5 .30 2 unknown 4.2 280 36 0 unknown .82 67 9.3 0 unknown .032 4.6 .31  0 unknown .028 4.6 .27  0 true .11  26 1.2  2 unknown 4.1 290 37 0 true .37 59 3.6 2 disqualified .051 9.4 .41 0 true .16 19 1.6 2 true 11   460 92 2 error (5) .024 5.6 .15  0 error (5) .025 5.6 .12  0
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c timeout 900     3700 7900    0 true 11   660 70 2 error (42) 880     3600   3800    0 error (42) 880     560   6200    0 true 150   530 1700 2 unknown .81 66 8.1 0 unknown .035 4.6 .21  0 unknown .027 4.6 .25  0 timeout 900     310 13000    0 timeout 900   660 9900 0 timeout 900    720 5100   0 disqualified .047 9.2 .42 0 timeout (verification) 900    140 9500   0 true 11   390 120 2 error (5) .045 5.6 .10  0 error (5) .024 5.6 .14  0
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     3900 8300    0 true 8.9 690 73 2 error (42) 880     4300   3900    0 error (42) 880     330   6000    0 true 7.9 340 68 2 unknown .79 67 9.0 0 unknown .054 4.6 .16  0 unknown .028 4.6 .24  0 timeout 900     1400 11000    0 true 7.2 440 62 2 timeout 900    430 2800   0 disqualified .064 9.0 .37 0 timeout (verification) 900    520 6400   0 true 12   350 120 2 error (5) .025 5.6 .086 0 error (5) .026 5.7 .11  0
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     2000 11000    0 true 11   640 84 2 error (42) 880     5700   4400    0 error (42) 880     360   5100    0 true 4.7 300 38 2 unknown .81 66 7.8 0 unknown .031 4.7 .19  0 unknown .029 4.8 .22  0 timeout 900     980 10000    0 true 4.8 290 48 2 timeout 900    420 4700   0 disqualified .047 9.4 .37 0 timeout (verification) 900    560 10000   0 true 10   390 75 2 error (5) .025 5.7 .12  0 error (5) .023 5.6 .15  0
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     2000 12000    0 true 4.2 280 33 2 error (42) 880     6500   3400    0 error (42) 880     390   6400    0 true 4.6 290 45 2 unknown .80 66 11   0 unknown .029 4.6 .24  0 unknown .033 4.6 .33  0 timeout 900     910 10000    0 true 4.4 290 46 2 timeout 900    330 4200   0 disqualified .043 9.9 .46 0 true .12 16 1.5 2 true 9.6 390 67 2 error (5) .026 5.6 .16  0 error (5) .026 5.6 .15  0
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c timeout 900     3000 8500    0 true 13   610 87 2 error (42) 880     5100   5000    0 error (42) 880     420   6500    0 timeout 900   1300 12000 0 unknown .79 67 7.6 0 unknown .038 4.7 .23  0 unknown .055 4.6 .15  0 timeout 900     870 12000    0 timeout 900   2100 11000 0 timeout 900    530 3800   0 disqualified .044 9.5 .42 0 timeout (verification) 900    610 8000   0 unknown 67   1600 690 0 error (5) .026 5.7 .12  0 error (5) .031 5.5 .19  0
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true .48  40 5.6  2 true 5.3 360 47 2 error (42) 880     4700   3500    0 error (42) 880     420   5300    0 true 4.4 290 41 2 unknown .79 66 9.4 0 unknown .044 4.5 .18  0 unknown .050 4.6 .13  0 timeout 900     920 13000    0 true 4.4 290 39 2 timeout 900    500 4200   0 disqualified .046 9.5 .37 0 timeout (verification) 900    620 5900   0 true 8.8 380 74 2 error (5) .024 5.6 .13  0 error (5) .032 5.5 .20  0
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c timeout 900     630 7800    0 true 21   1300 180 2 error (42) 880     6100   5900    0 error (42) 880     840   6400    0 true 7.0 460 64 2 unknown .83 66 8.7 0 unknown .028 4.7 .25  0 unknown .031 4.6 .21  0 timeout 900     330 10000    0 true 6.9 460 62 2 timeout 900    940 3900   0 disqualified .044 9.7 .42 0 timeout (verification) 900    580 6200   0 true 26   820 210 2 error (5) .029 5.5 .14  0 error (5) .031 5.6 .20  0
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c true .41  24 3.6  2 timeout 900   2200 13000 0 error (42) 880     5700   3800    0 error (42) 870     840   4100    0 true 6.4 460 53 2 unknown .83 66 9.2 0 unknown .030 4.6 .23  0 unknown .030 4.6 .23  0 timeout 900     280 11000    0 true 6.9 440 59 2 timeout 900    1100 5600   0 disqualified .049 9.1 .37 0 timeout (verification) 900    330 6200   0 unknown 48   1300 550 0 error (5) .029 5.5 .18  0 error (5) .025 5.6 .16  0
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 57     15000 710    0 true 34   2500 250 2 error (42) 880     13000   8100    0 out of memory 160     15000   2100    0 timeout 910   4400 12000 0 unknown .79 67 8.6 0 unknown .031 4.6 .15  0 unknown .027 4.6 .14  0 timeout 900     2100 13000    0 timeout 910   4400 13000 0 timeout 900    13000 11000   0 disqualified .045 9.0 .45 0 timeout (verification) 900    2800 6700   0 timeout 900   760 11000 0 error (5) .027 5.6 .18  0 error (5) .024 5.6 .12  0
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c error (134) .26  47 1.5  0 timeout 900   14000 9800 0 error (42) 880     13000   7600    0 out of memory 490     15000   5000    0 timeout 910   4300 11000 0 unknown .77 66 10   0 unknown .052 4.6 .15  0 unknown .026 4.6 .25  0 timeout 900     5000 11000    0 timeout 910   4200 13000 0 timeout 900    13000 8600   0 disqualified .064 9.4 .41 0 timeout (verification) 900    2800 7000   0 timeout 900   750 10000 0 error (5) .024 5.6 .13  0 error (5) .037 5.5 .13  0
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c timeout 900     2900 11000    0 true 5.2 330 38 2 error (42) 880     1600   10000    0 error (42) 880     800   7200    0 unknown 6.6 470 55 0 unknown .80 67 10   0 unknown .031 4.8 .24  0 unknown .028 4.8 .22  0 timeout 900     1200 9200    0 unknown 7.1 470 59 0 timeout 900    440 3900   0 disqualified .044 9.4 .39 0 timeout (verification) 900    440 6800   0 true 9.0 380 72 2 error (5) .051 5.6 .14  0 error (5) .049 5.6 .098 0
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c true .23  24 1.9  2 true 10   550 72 2 error (42) 880     1400   7200    0 out of memory 130     15000   1600    0 timeout 900   2000 7000 0 unknown .79 66 8.9 0 unknown .040 4.8 .26  0 unknown .054 4.7 .19  0 timeout 900     360 12000    0 timeout 900   2900 9100 0 out of memory 43    15000 590   0 disqualified .045 9.8 .48 0 timeout (verification) 900    110 9800   0 true 26   800 230 2 error (5) .026 5.6 .22  0 error (5) .028 5.6 .14  0
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .095 24 .71 0 out of memory 800   15000 5500 0 error (42) 880     210   3900    0 out of memory 170     15000   2500    0 true 4.5 290 40 2 out of memory (false(no-overflow)) 200    15000 3400   0 unknown .028 4.6 .20  0 unknown .028 4.6 .18  0 timeout 900     15000 9500    0 error (recursion) 3.4 270 35 0 out of memory 43    15000 650   0 disqualified .043 9.7 .42 0 timeout (verification) 900    270 11000   0 true 53   710 670 2 error (5) .033 5.5 .16  0 error (5) .026 5.6 .11  0
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     2800 11000    0 error (1) 21   770 210 0 error (42) 880     4700   3400    0 error (42) 880     320   6200    0 true 6.4 430 57 2 unknown .78 66 9.3 0 unknown .028 4.6 .16  0 unknown .035 4.6 .14  0 timeout 900     1100 10000    0 true 7.0 450 63 2 timeout 900    420 4000   0 disqualified .052 9.7 .41 0 timeout (verification) 900    530 7800   0 true 10   380 83 2 error (5) .026 5.6 .18  0 error (5) .028 5.7 .18  0
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .097 24 .83 0 true 11   950 88 2 error (42) 880     220   3100    0 out of memory 310     15000   4400    0 error (recursion) 6.7 370 57 0 out of memory (false(no-overflow)) 240    15000 3000   0 unknown .036 4.6 .23  0 unknown .032 4.5 .21  0 out of memory 300     15000 3500    0 error (recursion) 3.4 270 33 0 out of memory 41    15000 560   0 disqualified .064 9.5 .43 0 timeout (verification) 900    470 12000   0 timeout 900   8500 11000 0 error (5) .024 5.6 .15  0 error (5) .025 5.6 .15  0
termination-crafted/Mysore_true-termination_true-valid-memsafety.c timeout 900     3000 11000    0 true 6.2 450 53 2 error (42) 880     1000   10000    0 error (42) 880     1100   12000    0 true 5.3 340 45 2 unknown .82 66 8.6 0 unknown .031 4.6 .19  0 unknown .029 4.8 .075 0 timeout 900     160 11000    0 true 5.3 330 48 2 timeout 900    180 8100   0 disqualified .046 9.0 .41 0 timeout (verification) 900    100 11000   0 true 11   380 94 2 error (5) .027 5.7 .067 0 error (5) .025 5.6 .18  0
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .097 24 .77 0 error (1) 16   740 110 0 error (42) 880     390   5400    0 error (42) 880     450   4700    0 error (recursion) 5.6 300 48 0 out of memory (false(no-overflow)) 210    15000 2800   0 unknown .034 4.6 .22  0 unknown .054 4.6 .13  0 out of memory 750     15000 6800    0 error (recursion) 3.2 270 32 0 out of memory 340    15000 4300   0 disqualified .072 9.3 .37 0 timeout (verification) 900    800 10000   0 true 24   530 230 2 error (5) .030 5.7 .071 0 error (5) .025 5.5 .18  0
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .10  24 1.5  0 true 5.3 350 43 2 error (42) 880     270   3200    0 error (42) 880     310   4600    0 error (recursion) 4.7 280 46 0 out of memory (false(no-overflow)) 240    15000 2900   0 unknown .033 4.7 .29  0 unknown .033 4.6 .18  0 timeout 900     9100 11000    0 error (recursion) 3.3 270 29 0 out of memory 270    15000 3100   0 disqualified .048 9.5 .40 0 timeout (verification) 900    560 8500   0 true 11   530 91 2 error (5) .026 5.7 .089 0 error (5) .019 5.4 .19  0
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .14  24 .79 0 true 11   620 86 2 error (42) 880     390   3600    0 error (42) 880     450   5000    0 error (recursion) 5.5 300 51 0 out of memory (false(no-overflow)) 210    15000 3000   0 unknown .031 4.6 .22  0 unknown .026 4.6 .20  0 out of memory 390     15000 5200    0 error (recursion) 3.2 270 31 0 out of memory 350    15000 4400   0 disqualified .044 9.7 .44 0 timeout (verification) 900    640 7000   0 true 16   680 140 2 error (5) .025 5.6 .12  0 error (5) .032 5.6 .11  0
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .094 24 .91 0 true 8.6 560 70 2 out of memory 860     15000   5500    0 error (42) 870     300   11000    0 true 4.5 290 37 2 out of memory (false(no-overflow)) 200    15000 2800   0 unknown .029 4.6 .23  0 unknown .029 4.7 .16  0 out of memory 320     15000 4100    0 error (recursion) 3.3 270 30 0 out of memory 300    15000 4000   0 disqualified .047 8.9 .74 0 timeout (verification) 900    1300 11000   0 timeout 900   12000 9900 0 error (5) .023 5.7 .16  0 error (5) .023 5.7 .096 0
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true .30  24 3.0  2 true 15   800 88 2 error (42) 880     1500   7800    0 out of memory 210     15000   2500    0 true 5.1 290 42 2 unknown .78 67 8.1 0 unknown .035 4.5 .22  0 unknown .034 4.6 .17  0 timeout 900     310 12000    0 true 5.2 290 45 2 timeout 900    510 4500   0 disqualified .046 9.4 .38 0 timeout (verification) 900    3200 11000   0 true 10   440 78 2 error (5) .024 5.6 .18  0 error (5) .021 5.7 .17  0
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true .21  24 2.3  2 true 9.9 470 67 2 error (42) 870     1700   7800    0 out of memory 200     15000   2400    0 true 5.2 290 46 2 unknown .80 67 8.4 0 unknown .030 4.7 .12  0 unknown .031 4.6 .21  0 timeout 900     310 12000    0 true 5.5 300 49 2 timeout 900    310 4000   0 disqualified .043 9.4 .41 0 true .12 16 1.4 2 true 9.3 400 78 2 error (5) .048 5.5 .11  0 error (5) .024 5.6 .091 0
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     230 12000    0 true 26   1800 170 2 error (42) 880     1400   7700    0 out of memory 140     15000   1900    0 true 5.5 300 49 2 unknown .79 66 8.3 0 unknown .057 4.7 .22  0 unknown .033 4.6 .24  0 timeout 900     280 12000    0 true 5.4 290 53 2 timeout 900    320 4100   0 disqualified .043 9.8 .46 0 timeout (verification) 900    300 14000   0 true 13   550 100 2 error (5) .029 5.6 .12  0 error (5) .023 5.6 .12  0
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c timeout 900     4700 12000    0 true 11   550 74 2 error (42) 870     170   11000    0 out of memory 220     15000   3100    0 true 6.0 340 51 2 unknown .80 65 9.4 0 unknown .054 4.6 .15  0 unknown .028 4.7 .27  0 timeout 900     590 11000    0 true 6.3 340 53 2 out of memory 58    15000 810   0 disqualified .050 9.3 .57 0 timeout (verification) 900    460 8200   0 true 10   460 87 2 error (5) .050 5.5 .20  0 error (5) .024 5.6 .19  0
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c timeout 900     3900 12000    0 timeout 910   11000 4500 0 error (42) 880     1200   7700    0 out of memory 170     15000   2100    0 true 8.9 500 83 2 unknown .83 66 8.6 0 unknown .030 4.6 .15  0 unknown .048 4.6 .19  0 timeout 900     480 9700    0 true 9.2 390 82 2 out of memory 490    15000 2400   0 disqualified .043 9.5 .45 0 timeout (verification) 900    90 11000   0 true 14   480 110 2 error (5) .037 5.5 .15  0 error (5) .040 5.7 .12  0
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c error (5) .095 24 .78 0 true 11   700 83 2 error (42) 880     14000   8700    0 out of memory 240     15000   2900    0 unknown 5.8 330 51 0 out of memory 240    15000 3700   0 unknown .027 4.6 .24  0 unknown .031 4.6 .23  0 out of memory 350     15000 5400    0 error (recursion) 3.3 270 31 0 out of memory 71    15000 960   0 disqualified .049 9.2 .42 0 timeout (verification) 900    660 12000   0 true 12   490 110 2 error (5) .046 5.7 .12  0 error (5) .025 5.6 .15  0
termination-crafted/Singapore_true-termination_true-valid-memsafety.c timeout 900     2900 11000    0 out of memory 560   15000 2800 0 true 6.4   15   82    2 true 3.7   14   37    2 true 7.7 460 69 2 unknown .80 67 9.4 0 unknown .029 4.6 .23  0 unknown .056 4.7 .20  0 true 4.6   32 69    2 true 8.5 470 71 2 timeout 900    9200 6700   0 disqualified .050 9.1 .50 0 true 36    56 480   2 true 23   460 260 2 error (5) .023 5.6 .15  0 error (5) .049 5.5 .11  0
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c true .28  24 2.3  2 true 5.9 410 44 2 error (42) 880     5600   3900    0 error (42) 880     510   5900    0 true 5.0 300 43 2 unknown .82 67 7.2 0 unknown .052 4.6 .15  0 unknown .034 4.7 .25  0 timeout 900     240 13000    0 true 5.1 300 47 2 timeout 900    810 4200   0 disqualified .071 9.4 .42 0 timeout (verification) 900    500 7100   0 true 22   610 220 2 error (5) .026 5.6 .085 0 error (5) .027 5.5 .18  0
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c timeout 900     2800 12000    0 true 4.9 300 43 2 error (42) 880     6000   3800    0 error (42) 870     390   8600    0 true 5.2 290 52 2 unknown .79 66 8.0 0 unknown .051 4.6 .15  0 unknown .031 4.6 .20  0 timeout 900     640 12000    0 true 5.3 300 49 2 timeout 900    380 4100   0 disqualified .046 9.2 .40 0 true .12 16 1.5 2 true 9.9 380 81 2 error (5) .026 5.7 .17  0 error (5) .030 5.7 .16  0
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c true .31  50 2.4  2 true 4.4 300 36 2 error (42) 880     6000   3800    0 error (42) 870     300   6900    0 true 5.1 290 46 2 unknown .77 67 9.1 0 unknown .051 4.7 .19  0 unknown .029 4.6 .25  0 timeout 900     640 10000    0 true 5.4 310 48 2 timeout 900    380 4100   0 disqualified .047 8.9 .52 0 true .12 15 1.4 2 true 9.8 380 77 2 error (5) .028 5.5 .23  0 error (5) .026 5.6 .10  0
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c true .34  52 2.3  2 true 4.0 270 34 2 error (42) 880     5800   3600    0 error (42) 870     300   8200    0 true 4.7 290 49 2 unknown .79 66 9.8 0 unknown .028 4.8 .25  0 unknown .029 4.6 .21  0 timeout 900     650 13000    0 true 4.6 290 44 2 timeout 900    390 6400   0 disqualified .050 9.7 .40 0 timeout (verification) 900    530 8700   0 true 8.5 370 71 2 error (5) .027 5.6 .14  0 error (5) .026 5.6 .13  0
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     180 11000    0 out of memory 740   15000 4000 0 error (42) 880     1700   7600    0 out of memory 120     15000   1500    0 true 6.1 310 56 2 unknown .81 67 8.6 0 unknown .029 4.6 .14  0 unknown .055 4.6 .17  0 timeout 900     370 11000    0 true 6.3 320 57 2 timeout 900    260 6400   0 disqualified .050 9.2 .39 0 timeout (verification) 900    310 12000   0 true 17   630 140 2 error (5) .027 5.6 .11  0 error (5) .032 5.6 .21  0
termination-crafted/Thun_true-termination_true-valid-memsafety.c timeout 900     2600 11000    0 true 6.4 360 48 2 true .18  7.4 2.5  2 true .22  7.2 2.7  2 true 5.6 310 52 2 unknown .78 66 9.1 0 unknown .028 4.6 .27  0 unknown .045 4.6 .19  0 true .95  26 12    2 true 5.8 310 53 2 true 1.8  110 28   2 disqualified .047 9.7 .43 0 true .94 23 13   2 true 9.4 380 74 2 error (5) .025 5.6 .16  0 error (5) .025 5.5 .17  0
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c timeout 900     2700 10000    0 true 9.2 510 68 2 error (42) 880     5100   3900    0 error (42) 880     500   6000    0 true 6.7 430 60 2 unknown .80 67 8.1 0 unknown .028 4.7 .21  0 unknown .029 4.8 .27  0 timeout 900     330 10000    0 true 6.9 460 63 2 timeout 900    530 6600   0 disqualified .048 9.4 .41 0 timeout (verification) 900    170 11000   0 true 34   650 350 2 error (5) .023 5.7 .18  0 error (5) .028 5.7 .17  0
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c timeout 900     2800 10000    0 true 9.0 480 70 2 error (42) 880     5100   4200    0 error (42) 880     500   5700    0 true 8.0 480 71 2 unknown .82 66 9.9 0 unknown .030 4.6 .21  0 unknown .028 4.5 .22  0 timeout 900     330 12000    0 true 8.1 480 65 2 timeout 900    520 3700   0 disqualified .048 9.9 .44 0 timeout (verification) 900    150 12000   0 true 31   730 360 2 error (5) .036 5.7 .12  0 error (5) .023 5.6 .16  0
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true .18  24 1.5  2 true 3.9 280 30 2 error (42) 880     6600   5700    0 error (42) 880     380   6700    0 true 4.1 280 41 2 unknown .76 65 7.7 0 unknown .027 4.6 .25  0 unknown .036 4.6 .16  0 timeout 900     650 11000    0 true 4.0 280 40 2 timeout 900    390 4100   0 disqualified .044 9.7 .60 0 true .15 16 1.3 2 true 7.9 340 62 2 error (5) .038 5.7 .12  0 error (5) .030 5.6 .14  0
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 42     15000 290    0 true 2.1 190 17 2 true .050 6.5 .39 2 true .042 6.9 .34 2 true 3.1 270 29 2 unknown .79 66 7.9 0 unknown .029 4.6 .30  0 unknown .031 4.5 .13  0 true .081 26 .77 2 true 3.3 270 32 2 true .34 58 4.2 2 disqualified .048 9.3 .53 0 true .12 16 1.1 2 true 6.8 330 55 2 error (5) .025 5.5 .18  0 error (5) .031 5.6 .15  0
termination-crafted/aaron2_true-termination_true-valid-memsafety.c true .32  24 2.7  2 true 33   2300 210 2 error (42) 880     1400   8800    0 out of memory 160     15000   2100    0 true 5.1 300 44 2 unknown .88 66 9.0 0 unknown .034 4.6 .26  0 unknown .029 4.6 .18  0 timeout 900     150 13000    0 true 5.1 320 44 2 timeout 900    580 4500   0 disqualified .083 9.5 .36 0 timeout (verification) 900    210 13000   0 true 9.1 360 76 2 error (5) .033 5.7 .18  0 error (5) .038 5.7 .12  0
termination-crafted/aaron3_true-termination_true-valid-memsafety.c timeout 900     270 11000    0 timeout 910   8600 5100 0 error (42) 880     210   11000    0 out of memory 230     15000   3400    0 true 17   520 160 2 unknown .86 66 10   0 unknown .033 4.6 .20  0 unknown .059 4.6 .13  0 timeout 900     300 13000    0 true 17   650 180 2 out of memory 68    15000 1000   0 disqualified .049 9.3 .35 0 timeout (verification) 900    420 12000   0 true 25   530 310 2 error (5) .024 5.6 .20  0 error (5) .043 5.7 .18  0
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true .18  23 1.4  2 true 8.4 490 63 2 true .91  31   11    2 out of memory 86     15000   1200    0 true 170   1400 1800 2 unknown .79 66 10   0 unknown .031 4.6 .23  0 unknown .027 4.6 .20  0 true .19  26 2.5  2 true 69   2100 640 2 true .41 59 3.3 2 disqualified .054 9.7 .36 0 true .12 16 1.4 2 true 8.7 380 62 2 error (5) .030 5.7 .17  0 error (5) .031 5.6 .23  0
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c true .33  35 2.8  2 true 7.1 470 56 2 error (42) 880     4200   3400    0 error (42) 880     320   5800    0 true 4.8 300 41 2 unknown .78 65 8.7 0 unknown .034 4.5 .21  0 unknown .032 4.6 .35  0 timeout 900     890 12000    0 true 4.9 290 43 2 timeout 900    410 3600   0 disqualified .042 9.8 .62 0 true .13 15 1.5 2 true 8.6 360 70 2 error (5) .024 5.6 .13  0 error (5) .022 5.6 .039 0
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c false(termination) .17  24 1.1  1 false(termination) 32   1600 190 0 error (42) 880     1300   8100    0 out of memory 190     15000   2400    0 false(termination) 3.7 280 31 1 unknown .86 67 10   0 unknown .032 4.6 .25  0 unknown .034 4.6 .29  0 timeout 900     260 11000    0 false(termination) 4.0 280 37 1 timeout 900    510 3900   0 disqualified .055 9.5 .37 0 timeout (verification) 900    62 12000   0 false(termination) 7.7 370 68 1 error (5) .031 5.6 .13  0 error (5) .023 5.6 .15  0
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c false(termination) .12  24 1.2  1 false(termination) 6.3 340 54 1 error (42) 880     7000   3300    0 error (42) 880     400   5600    0 false(termination) 3.8 280 38 1 unknown .81 66 9.1 0 unknown .028 4.6 .18  0 unknown .048 4.8 .20  0 timeout 900     1100 11000    0 false(termination) 3.8 280 33 1 timeout 900    510 8600   0 disqualified .043 9.4 .45 0 timeout (verification) 900    65 10000   0 false(termination) 8.0 370 60 1 error (5) .031 5.6 .16  0 error (5) .047 5.5 .12  0
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c false(termination) .15  24 1.1  1 false(termination) 110   6000 670 1 error (42) 880     2400   8300    0 out of memory 610     15000   7000    0 false(termination) 4.4 290 37 1 unknown .80 66 8.2 0 unknown .030 4.6 .17  0 unknown .032 4.6 .22  0 timeout 900     1600 11000    0 false(termination) 4.4 290 41 1 timeout 900    900 12000   0 disqualified .087 9.4 .34 0 timeout (verification) 900    200 7400   0 false(termination) 7.9 360 65 1 error (5) .023 5.7 .16  0 error (5) .049 5.5 .13  0
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c false(termination) .14  24 1.1  1 false(termination) 4.5 370 35 1 error (42) 880     1700   7300    0 out of memory 180     15000   2200    0 false(termination) 3.7 280 34 1 unknown .77 66 8.1 0 unknown .052 4.7 .16  0 unknown .032 4.7 .16  0 timeout 900     450 11000    0 false(termination) 3.6 290 35 1 timeout 900    3200 5800   0 disqualified .069 9.2 .42 0 probably out of memory (killed (signal 9, verification)) 290    15000 4200   0 false(termination) 9.0 380 71 1 error (5) .026 5.6 .17  0 error (5) .037 5.6 .12  0
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c false(termination) .14  24 .99 1 false(termination) 12   490 80 1 error (42) 880     1700   9500    0 error (42) 880     170   11000    0 false(termination) 3.8 280 36 1 unknown .78 66 8.8 0 unknown .033 4.6 .20  0 unknown .030 4.6 .18  0 timeout 900     700 10000    0 false(termination) 3.8 280 40 1 out of memory 490    15000 6900   0 disqualified .046 9.2 .31 0 timeout (verification) 900    180 9000   0 false(termination) 13   570 95 1 error (5) .029 5.6 .14  0 error (5) .024 5.6 .11  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     2800 5000    0 true 12   780 100 2 error (42) 880     1200   5100    0 out of memory 180     15000   2000    0 true 13   510 120 2 unknown 1.7  68 26   0 unknown .053 4.6 .18  0 unknown .029 4.6 .20  0 timeout 900     750 13000    0 true 12   510 100 2 timeout 900    470 7000   0 disqualified .047 9.4 .41 0 timeout (verification) 900    3100 10000   0 true 14   560 120 2 error (5) .025 5.6 .17  0 error (5) .029 5.7 .16  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true .20  24 1.5  2 true 15   850 100 2 error (42) 880     1700   7800    0 out of memory 200     15000   2300    0 true 5.5 290 47 2 unknown .80 65 8.3 0 unknown .042 4.6 .16  0 unknown .033 4.7 .26  0 timeout 900     530 10000    0 true 5.6 310 43 2 timeout 900    290 4300   0 disqualified .047 9.1 .39 0 true .12 17 1.3 2 true 10   490 84 2 error (5) .028 5.5 .16  0 error (5) .032 5.6 .12  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true .18  24 1.5  2 true 6.9 440 55 2 true .87  31   12    2 out of memory 86     15000   1000    0 true 170   1400 2300 2 unknown .81 66 8.6 0 unknown .028 4.7 .24  0 unknown .028 4.6 .22  0 true .19  26 2.9  2 true 71   2100 840 2 true .39 59 3.3 2 disqualified .046 9.2 .45 0 true .15 16 1.4 2 true 8.8 370 64 2 error (5) .025 5.6 .11  0 error (5) .026 5.6 .10  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c true .33  36 2.8  2 true 7.2 460 61 2 error (42) 880     4300   3000    0 error (42) 880     330   7200    0 true 4.8 300 49 2 unknown .78 67 8.3 0 unknown .033 4.6 .18  0 unknown .030 4.7 .19  0 timeout 900     900 11000    0 true 4.8 310 41 2 timeout 900    430 5300   0 disqualified .045 9.4 .39 0 true .12 15 1.5 2 true 8.2 360 59 2 error (5) .022 5.6 .15  0 error (5) .026 5.6 .11  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout 900     5400 5000    0 true 19   1400 120 2 error (42) 880     540   4300    0 error (42) 880     11000   9800    0 true 7.4 410 60 2 unknown .85 66 10   0 unknown .030 4.6 .24  0 unknown .036 4.6 .21  0 timeout 900     1400 8800    0 true 7.8 480 66 2 out of memory 38    15000 480   0 disqualified .047 9.5 .40 0 timeout (verification) 900    310 12000   0 true 24   500 240 2 error (5) .049 5.6 .12  0 error (5) .022 5.6 .12  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 900     1800 6100    0 true 42   2400 320 2 error (42) 880     1200   5200    0 out of memory 100     15000   1200    0 true 7.9 420 69 2 unknown 150    110 1800   0 unknown .026 4.6 .27  0 unknown .027 4.6 .21  0 timeout 900     1800 10000    0 true 7.7 410 66 2 timeout 900    330 6100   0 disqualified .050 9.5 .46 0 timeout (verification) 900    100 11000   0 true 27   660 310 2 error (5) .021 5.6 .13  0 error (5) .033 5.6 .15  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c true .19  24 1.5  2 true 23   1100 160 2 error (42) 880     1700   8700    0 out of memory 160     15000   2200    0 true 5.0 290 42 2 unknown .78 66 9.4 0 unknown .052 4.6 .16  0 unknown .034 4.6 .23  0 timeout 900     1400 12000    0 true 5.2 300 41 2 timeout 900    430 6100   0 disqualified .045 9.8 .49 0 timeout (verification) 900    430 13000   0 true 8.9 380 80 2 error (5) .047 5.5 .11  0 error (5) .038 5.6 .10  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true .49  54 4.8  2 true 46   2300 470 2 true .13  7.1 1.1  2 out of memory 170     15000   2500    0 true 4.8 290 49 2 unknown .80 65 8.9 0 unknown .035 4.6 .17  0 unknown .029 4.6 .23  0 true .091 26 .96 2 true 17   470 170 2 out of memory 120    15000 1600   0 disqualified .046 9.4 .41 0 true 23    120 310   2 true 9.0 380 75 2 error (5) .025 5.6 .19  0 error (5) .027 5.5 .14  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true .34  24 3.2  2 true 9.9 710 79 2 error (42) 880     1800   8700    0 out of memory 210     15000   2500    0 unknown 6.5 450 58 0 unknown .78 66 9.1 0 unknown .032 4.6 .21  0 unknown .045 4.8 .12  0 timeout 900     550 12000    0 unknown 9.2 490 81 0 timeout 900    330 4300   0 disqualified .084 9.9 .33 0 timeout (verification) 900    470 6400   0 true 10   460 87 2 error (5) .025 5.7 .17  0 error (5) .030 5.6 .17  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true .34  24 3.2  2 true 17   1200 120 2 error (42) 880     1600   7900    0 out of memory 190     15000   2100    0 true 7.0 380 57 2 unknown .80 67 8.6 0 unknown .044 4.6 .18  0 unknown .058 4.6 .23  0 timeout 900     500 12000    0 true 6.9 390 59 2 timeout 900    300 4800   0 disqualified .048 9.2 .36 0 true .12 16 1.5 2 true 10   470 85 2 error (5) .032 5.7 .13  0 error (5) .023 5.6 .14  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true .23  24 2.0  2 true 9.4 490 62 2 error (42) 880     1700   7600    0 out of memory 200     15000   2500    0 unknown 4.2 280 37 0 unknown .80 66 8.4 0 unknown .037 4.7 .15  0 unknown .026 4.6 .22  0 timeout 900     310 11000    0 unknown 4.3 280 35 0 timeout 900    350 4300   0 disqualified .046 9.1 .43 0 timeout (verification) 900    630 6100   0 true 11   490 87 2 error (5) .023 5.7 .13  0 error (5) .046 5.5 .13  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true .30  34 2.9  2 true 14   960 110 2 error (42) 880     610   11000    0 out of memory 410     15000   5100    0 true 5.3 300 46 2 unknown .81 67 8.0 0 unknown .037 4.6 .15  0 unknown .028 4.6 .21  0 timeout 900     1500 13000    0 true 5.4 310 49 2 out of memory 38    15000 600   0 disqualified .044 9.5 .41 0 true .13 16 1.6 2 true 11   510 88 2 error (5) .024 5.9 .10  0 error (5) .022 5.6 .065 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true .48  47 4.2  2 true 10   730 72 2 error (42) 880     560   5700    0 out of memory 410     15000   6000    0 true 6.5 330 53 2 unknown 1.0  66 12   0 unknown .030 4.6 .21  0 unknown .030 4.6 .18  0 timeout 900     330 11000    0 true 6.3 340 55 2 timeout 900    350 4900   0 disqualified .049 9.1 .40 0 true .12 15 1.4 2 true 9.8 420 89 2 error (5) .027 5.6 .15  0 error (5) .026 5.6 .12  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true .32  24 2.5  2 true 30   2300 370 2 error (42) 880     1600   8600    0 out of memory 220     15000   2900    0 true 5.5 310 46 2 unknown .90 68 9.1 0 unknown .046 4.6 .15  0 unknown .027 4.6 .16  0 timeout 900     340 11000    0 true 5.4 310 45 2 timeout 900    540 4200   0 disqualified .040 9.4 .48 0 timeout (verification) 900    53 10000   0 true 10   450 86 2 error (5) .044 5.7 .16  0 error (5) .023 5.7 .18  0
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c true .37  36 3.3  2 true 10   740 83 2 error (42) 880     4400   4400    0 error (42) 880     810   5600    0 true 6.9 400 58 2 unknown .80 66 8.3 0 unknown .029 4.6 .35  0 unknown .038 4.6 .16  0 timeout 900     510 12000    0 true 6.4 410 54 2 timeout 900    430 3800   0 disqualified .048 9.3 .40 0 timeout (verification) 900    460 8000   0 true 9.5 400 78 2 error (5) .030 5.6 .19  0 error (5) .024 5.7 .085 0
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c true .36  23 2.9  2 true 44   2000 280 2 error (42) 870     1300   8200    0 out of memory 200     15000   2400    0 unknown 4.2 280 37 0 unknown .83 66 9.7 0 unknown .048 4.6 .19  0 unknown .055 4.5 .15  0 timeout 900     270 14000    0 unknown 4.2 290 41 0 timeout 900    470 6200   0 disqualified .047 9.0 .38 0 timeout (verification) 900    63 11000   0 true 14   500 120 2 error (5) .053 5.6 .15  0 error (5) .024 5.6 .12  0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true .35  39 3.3  2 true 19   1200 120 2 error (42) 880     550   7400    0 out of memory 420     15000   5000    0 true 6.4 350 55 2 unknown .89 66 11   0 unknown .027 4.6 .21  0 unknown .037 4.6 .22  0 timeout 900     1500 11000    0 true 6.5 350 55 2 timeout 900    360 4300   0 disqualified .039 9.1 .43 0 true .13 15 1.3 2 true 11   440 83 2 error (5) .047 5.5 .12  0 error (5) .050 5.8 .11  0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 900     2000 5400    0 true 28   2400 230 2 error (42) 880     560   5000    0 out of memory 240     15000   3000    0 out of memory 780   15000 8500 0 unknown 1.0  68 13   0 unknown .031 4.6 .22  0 unknown .031 4.5 .17  0 timeout 900     440 14000    0 out of memory 590   15000 6900 0 out of memory 37    15000 490   0 disqualified .050 9.4 .36 0 timeout (verification) 900    130 9900   0 true 12   500 110 2 error (5) .023 5.6 .15  0 error (5) .021 5.6 .19  0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 900     2300 13000    0 true 5.9 420 44 2 error (42) 880     4800   3700    0 error (42) 870     340   6000    0 true 4.6 290 44 2 unknown .78 66 8.4 0 unknown .028 4.6 .20  0 unknown .027 4.6 .21  0 timeout 900     680 12000    0 true 4.9 290 46 2 timeout 900    420 6800   0 disqualified .044 8.9 .42 0 timeout (verification) 900    470 8000   0 true 11   360 93 2 error (5) .023 5.6 .094 0 error (5) .023 5.6 .16  0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true .19  23 2.1  2 true 7.6 470 56 2 true .88  30   9.8  2 out of memory 85     15000   1100    0 true 170   1400 1900 2 unknown .78 67 8.1 0 unknown .035 4.8 .27  0 unknown .031 4.6 .22  0 true .18  26 2.4  2 true 70   2200 830 2 true .39 59 3.5 2 disqualified .047 9.3 .40 0 true .13 16 1.5 2 true 8.2 370 69 2 error (5) .027 5.6 .20  0 error (5) .023 5.5 .23  0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c true .25  28 2.2  2 true 6.4 440 54 2 error (42) 880     4700   5700    0 error (42) 880     320   6500    0 true 4.7 300 41 2 unknown .80 66 8.6 0 unknown .031 4.6 .19  0 unknown .045 4.6 .20  0 timeout 900     910 11000    0 true 4.7 290 38 2 timeout 900    430 4400   0 disqualified .049 9.6 .40 0 true .12 16 1.4 2 true 8.9 370 66 2 error (5) .028 5.8 .16  0 error (5) .048 5.5 .12  0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 900     3500 11000    0 true 24   1300 160 2 error (42) 880     1600   8000    0 out of memory 160     15000   2300    0 true 5.6 300 47 2 unknown .79 67 7.8 0 unknown .039 4.7 .24  0 unknown .031 4.6 .12  0 timeout 900     1400 9900    0 true 5.9 350 54 2 timeout 900    420 6300   0 disqualified .049 9.3 .42 0 timeout (verification) 900    1800 11000   0 true 7.9 330 74 2 error (5) .055 5.6 .11  0 error (5) .021 5.6 .22  0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true .52  57 4.7  2 true 44   4100 440 2 true .11  7.6 1.5  2 out of memory 170     15000   2300    0 true 4.8 290 50 2 unknown .79 68 9.1 0 unknown .054 4.7 .17  0 unknown .030 4.6 .15  0 true .092 26 1.2  2 true 16   480 160 2 out of memory 120    15000 1700   0 disqualified .044 9.3 .40 0 true 23    120 280   2 true 9.2 370 71 2 error (5) .053 5.5 .18  0 error (5) .024 5.6 .14  0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true .21  24 1.5  2 true 5.4 320 45 2 error (42) 880     5100   3900    0 error (42) 880     540   6200    0 true 4.4 290 43 2 unknown .79 65 9.4 0 unknown .032 4.6 .18  0 unknown .041 4.6 .12  0 timeout 900     280 12000    0 true 4.5 290 41 2 timeout 900    500 5100   0 disqualified .046 9.4 .43 0 timeout (verification) 900    500 4900   0 true 8.3 360 59 2 error (5) .031 5.5 .11  0 error (5) .024 5.7 .065 0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true .15  24 1.6  2 true 4.8 300 42 2 error (42) 880     5100   3400    0 error (42) 880     350   5400    0 true 5.7 300 54 2 unknown .82 67 8.3 0 unknown .029 4.6 .19  0 unknown .059 4.6 .22  0 timeout 900     380 12000    0 true 5.4 300 44 2 timeout 900    420 4100   0 disqualified .043 9.2 .48 0 timeout (verification) 900    470 6900   0 true 10   370 100 2 error (5) .024 5.6 .074 0 error (5) .048 5.5 .095 0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true .28  24 2.6  2 true 20   1200 120 2 error (42) 880     1600   7900    0 out of memory 190     15000   2700    0 true 5.6 300 46 2 unknown .79 66 8.3 0 unknown .028 4.6 .17  0 unknown .057 4.7 .20  0 timeout 900     640 13000    0 true 5.8 310 50 2 timeout 900    390 5900   0 disqualified .043 9.5 .37 0 timeout (verification) 900    2800 10000   0 true 11   520 95 2 error (5) .044 5.5 .13  0 error (5) .024 5.6 .20  0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true .42  31 4.1  2 true 23   1700 150 2 error (42) 880     1500   7100    0 out of memory 170     15000   2300    0 true 7.1 410 61 2 unknown .84 66 9.3 0 unknown .028 4.6 .24  0 unknown .034 4.6 .21  0 timeout 900     710 11000    0 true 7.6 440 61 2 timeout 900    480 4900   0 disqualified .045 9.0 .38 0 timeout (verification) 900    2600 9600   0 true 12   520 110 2 error (5) .027 5.7 .12  0 error (5) .034 5.6 .090 0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true .43  28 4.4  2 true 73   5700 430 2 error (42) 880     1700   8700    0 out of memory 140     15000   1600    0 true 6.6 390 58 2 unknown .82 66 9.8 0 unknown .045 4.6 .13  0 unknown .030 4.6 .18  0 timeout 900     850 11000    0 true 6.7 380 58 2 timeout 900    430 4600   0 disqualified .050 9.3 .39 0 timeout (verification) 900    2800 8600   0 true 12   510 99 2 error (5) .051 5.5 .12  0 error (5) .021 5.7 .085 0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c timeout 900     320 7200    0 true 6.2 320 43 2 error (42) 880     1600   8800    0 out of memory 190     15000   2300    0 true 5.0 290 42 2 unknown .83 66 9.7 0 unknown .054 4.6 .17  0 unknown .028 4.6 .22  0 timeout 900     310 11000    0 true 5.1 290 43 2 timeout 900    340 3900   0 disqualified .044 8.9 .37 0 timeout (verification) 900    120 9900   0 true 14   490 160 2 error (5) .024 5.6 .10  0 error (5) .028 5.6 .23  0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout 900     2000 11000    0 true 6.7 340 46 2 error (42) 880     1800   7400    0 out of memory 190     15000   2700    0 true 4.7 290 42 2 unknown .80 67 8.9 0 unknown .035 4.6 .31  0 unknown .032 4.6 .18  0 timeout 900     340 11000    0 true 4.7 290 40 2 timeout 900    330 4300   0 disqualified .048 9.2 .45 0 timeout (verification) 900    100 11000   0 true 10   490 92 2 error (5) .059 5.7 .12  0 error (5) .031 5.6 .21  0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c timeout 900     190 12000    0 true 4.9 310 36 2 error (42) 880     1700   9200    0 out of memory 190     15000   2500    0 unknown 4.0 280 33 0 unknown .80 66 8.3 0 unknown .028 4.6 .19  0 unknown .031 4.6 .29  0 timeout 900     430 12000    0 unknown 4.1 290 34 0 out of memory 330    15000 3000   0 disqualified .047 9.4 .49 0 timeout (verification) 900    140 9800   0 true 13   440 120 2 error (5) .025 5.6 .085 0 error (5) .025 5.6 .12  0
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c timeout 900     2700 10000    0 true 6.7 460 57 2 true .27  6.9 1.5  2 true .17  6.6 1.6  2 out of memory 660   15000 7800 0 unknown .81 66 8.5 0 unknown .031 4.6 .41  0 unknown .028 4.7 .21  0 true .18  26 2.6  2 out of memory 490   15000 7200 0 true .40 59 3.9 2 disqualified .046 9.1 .45 0 true .11 14 1.2 2 true 10   470 87 2 error (5) .040 5.6 .13  0 error (5) .026 5.6 .15  0
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     1400 9700    0 true 64   4500 440 2 error (42) 880     2800   7900    0 out of memory 800     15000   9500    0 true 10   510 81 2 unknown .85 68 9.3 0 unknown .033 4.5 .19  0 unknown .039 4.6 .18  0 timeout 900     600 11000    0 true 10   490 86 2 timeout 900    500 5800   0 disqualified .043 9.4 .46 0 timeout (verification) 900    2900 8300   0 true 47   550 570 2 error (5) .025 5.6 .16  0 error (5) .035 5.5 .19  0
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true .16  24 .90 2 true 11   780 71 2 error (42) 880     1600   7700    0 out of memory 150     15000   2000    0 true 4.4 280 42 2 unknown .81 65 8.4 0 unknown .030 4.6 .14  0 unknown .030 4.6 .17  0 timeout 900     1100 11000    0 true 4.3 290 37 2 timeout 900    420 5600   0 disqualified .069 9.6 .38 0 timeout (verification) 900    460 7600   0 true 9.0 370 76 2 error (5) .038 5.5 .098 0 error (5) .048 5.6 .12  0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 900     2700 13000    0 true 5.6 380 43 2 error (42) 880     5600   4400    0 error (42) 880     350   8800    0 true 4.7 290 44 2 unknown .78 67 8.4 0 unknown .029 4.6 .14  0 unknown .049 4.5 .17  0 timeout 900     990 13000    0 true 4.8 290 39 2 timeout 900    400 3900   0 disqualified .045 9.6 .52 0 timeout (verification) 900    520 6900   0 true 11   380 100 2 error (5) .028 5.6 .16  0 error (5) .025 5.7 .12  0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true .18  24 1.6  2 true 4.8 370 37 2 error (42) 880     6400   4200    0 error (42) 880     390   5500    0 true 4.5 290 43 2 unknown .79 67 9.1 0 unknown .054 4.6 .14  0 unknown .034 4.6 .19  0 timeout 900     520 12000    0 true 4.6 290 41 2 timeout 900    390 4000   0 disqualified .047 9.4 .54 0 true .13 16 1.5 2 true 9.2 380 62 2 error (5) .024 5.6 .12  0 error (5) .049 5.6 .097 0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c true .21  24 2.0  2 true 4.9 310 43 2 error (42) 880     5600   4400    0 error (42) 880     350   6000    0 unknown 5.9 450 47 0 unknown .78 65 9.3 0 unknown .029 4.6 .15  0 unknown .026 4.6 .24  0 timeout 900     1000 12000    0 unknown 5.9 440 56 0 timeout 900    400 4100   0 disqualified .053 9.5 .33 0 timeout (verification) 900    520 7000   0 unknown 19   770 140 0 error (5) .036 5.4 .074 0 error (5) .026 5.7 .14  0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true .25  24 2.6  2 true 5.4 320 42 2 error (42) 880     5100   4200    0 error (42) 880     470   5400    0 true 4.3 280 39 2 unknown .78 67 8.9 0 unknown .026 4.7 .20  0 unknown .049 4.7 .19  0 timeout 900     220 13000    0 true 4.4 290 38 2 timeout 900    420 5700   0 disqualified .045 9.3 .62 0 timeout (verification) 900    79 11000   0 true 8.7 370 75 2 error (5) .025 5.6 .14  0 error (5) .051 5.6 .12  0
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true .13  24 1.3  2 true 15   1000 99 2 error (42) 880     1200   8400    0 out of memory 200     15000   2500    0 true 4.7 300 38 2 unknown .80 65 9.7 0 unknown .029 4.7 .17  0 unknown .043 4.6 .19  0 timeout 900     310 12000    0 true 4.8 290 44 2 timeout 900    380 5000   0 disqualified .048 9.2 .40 0 timeout (verification) 900    98 9800   0 true 8.6 380 69 2 error (5) .025 5.6 .13  0 error (5) .027 5.7 .22  0
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout 900     2200 9500    0 timeout 900   2200 11000 0 error (42) 880     1600   7900    0 out of memory 200     15000   2300    0 timeout 900   5100 11000 0 unknown .85 67 9.0 0 unknown .029 4.7 .25  0 unknown .033 4.6 .23  0 timeout 900     520 11000    0 timeout 910   5300 11000 0 out of memory 41    15000 540   0 disqualified .043 9.4 .51 0 timeout (verification) 900    130 10000   0 true 18   580 140 2 error (5) .040 5.7 .087 0 error (5) .025 5.6 .12  0
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 900     210 14000    0 true 39   2500 290 2 error (42) 880     820   4600    0 out of memory 450     15000   5300    0 timeout 900   5400 6800 0 unknown 1.2  66 15   0 unknown .029 4.7 .25  0 unknown .028 4.6 .15  0 timeout 900     930 14000    0 timeout 900   6300 7300 0 timeout 900    500 3800   0 disqualified .058 9.4 .44 0 timeout (verification) 900    140 8100   0 true 20   560 200 2 error (5) .022 5.7 .11  0 error (5) .042 5.5 .097 0
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c error (5) .096 24 .74 0 true 15   1300 130 2 error (42) 880     14000   10000    0 out of memory 230     15000   2700    0 true 5.7 310 53 2 out of memory (false(no-overflow)) 280    15000 3300   0 unknown .028 4.6 .22  0 unknown .032 4.6 .18  0 out of memory 400     15000 5000    0 error (recursion) 3.4 270 31 0 timeout 900    10000 4500   0 disqualified .048 9.5 .41 0 timeout (verification) 900    440 7500   0 true 46   640 520 2 error (5) .028 5.6 .073 0 error (5) .026 5.6 .14  0
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c error (5) .098 24 .86 0 true 8.9 470 62 2 error (42) 880     14000   10000    0 out of memory 310     15000   4100    0 true 5.1 290 46 2 out of memory (false(no-overflow)) 260    15000 2900   0 unknown .044 4.7 .20  0 unknown .036 4.6 .26  0 out of memory 350     15000 4000    0 error (recursion) 3.3 270 31 0 out of memory 98    15000 1300   0 disqualified .049 9.1 .40 0 timeout (verification) 900    470 11000   0 unknown 38   2000 390 0 error (5) .023 5.7 .12  0 error (5) .026 5.7 .11  0
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true .17  24 1.0  2 true 9.9 470 66 2 error (42) 880     1700   9800    0 out of memory 190     15000   2400    0 true 4.4 280 39 2 unknown .79 67 9.1 0 unknown .031 4.6 .19  0 unknown .031 4.6 .18  0 timeout 900     390 10000    0 true 4.4 290 39 2 timeout 900    510 6100   0 disqualified .051 9.1 .44 0 timeout (verification) 900    130 11000   0 true 9.0 380 75 2 error (5) .030 5.7 .092 0 error (5) .030 5.6 .12  0
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true .22  24 2.2  2 true 7.1 420 52 2 error (42) 880     1400   8600    0 out of memory 140     15000   2000    0 true 5.1 300 46 2 unknown .85 67 8.3 0 unknown .027 4.6 .22  0 unknown .050 4.7 .16  0 timeout 900     530 10000    0 true 5.1 290 50 2 timeout 900    370 4000   0 disqualified .074 9.6 .45 0 timeout (verification) 900    42 14000   0 true 9.5 380 77 2 error (5) .039 5.5 .12  0 error (5) .025 5.7 .089 0
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true .17  24 1.4  2 true 3.9 260 32 2 true .32  15   3.6  2 true .39  15   5.0  2 unknown 5.4 350 53 0 unknown .79 68 7.9 0 unknown .028 4.6 .21  0 unknown .032 4.6 .32  0 true .15  26 1.6  2 unknown 5.4 370 53 0 true .65 130 8.0 2 disqualified .048 9.6 .43 0 true .43 18 5.6 2 true 8.7 370 68 2 error (5) .026 5.7 .15  0 error (5) .024 5.6 .23  0
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout 900     5500 4200    0 true 15   970 100 2 error (42) 870     530   5100    0 out of memory 420     15000   5500    0 true 5.7 310 45 2 unknown .86 67 9.3 0 unknown .046 4.6 .18  0 unknown .028 4.6 .22  0 timeout 900     1400 8200    0 true 5.8 330 53 2 out of memory 38    15000 490   0 disqualified .049 9.2 .36 0 timeout (verification) 900    320 12000   0 true 25   530 290 2 error (5) .028 5.6 .14  0 error (5) .024 5.8 .15  0
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true .19  24 1.4  2 true 4.2 280 35 2 error (42) 880     6300   3500    0 error (42) 880     380   5800    0 true 4.1 280 39 2 unknown .78 67 10   0 unknown .043 4.6 .17  0 unknown .035 4.6 .33  0 timeout 900     650 13000    0 true 4.1 280 35 2 timeout 900    410 5900   0 disqualified .047 9.4 .41 0 true .12 16 1.4 2 true 8.2 360 66 2 error (5) .027 5.6 .14  0 error (5) .026 5.6 .13  0
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true .26  28 2.4  2 true 10   740 70 2 error (42) 880     550   4700    0 out of memory 410     15000   5100    0 true 5.2 300 41 2 unknown .85 65 9.1 0 unknown .037 4.6 .099 0 unknown .023 4.7 .15  0 timeout 900     1500 10000    0 true 5.3 300 43 2 timeout 900    430 5900   0 disqualified .048 9.2 .43 0 true .12 16 1.3 2 true 9.8 450 86 2 error (5) .023 5.6 .12  0 error (5) .028 5.6 .14  0
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true .19  24 1.6  2 true 25   1200 140 2 error (42) 880     1600   8900    0 out of memory 190     15000   2700    0 true 5.7 310 53 2 unknown .85 65 9.4 0 unknown .030 4.6 .21  0 unknown .039 4.7 .23  0 timeout 900     650 12000    0 true 5.6 300 54 2 timeout 900    490 6800   0 disqualified .044 9.3 .49 0 timeout (verification) 900    2900 9500   0 true 10   460 81 2 error (5) .024 5.7 .15  0 error (5) .024 5.6 .10  0
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true 1.7   180 19    2 true 11   770 75 2 error (42) 880     4700   12000    0 error (42) 880     2000   4800    0 out of memory 660   15000 7400 0 unknown .79 67 8.9 0 unknown .029 4.6 .21  0 unknown .045 4.6 .16  0 timeout 900     6700 10000    0 out of memory 490   15000 5300 0 timeout 900    14000 9500   0 disqualified .045 9.3 .41 0 true .12 16 1.5 2 timeout 900   840 12000 0 error (5) .025 5.5 .19  0 error (5) .024 5.6 .092 0
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true .23  24 1.8  2 true 10   770 77 2 error (42) 880     1200   4500    0 error (42) 880     370   5500    0 true 11   470 110 2 unknown .79 66 8.6 0 unknown .028 4.7 .22  0 unknown .028 4.8 .17  0 timeout 900     1200 12000    0 true 11   460 100 2 timeout 900    660 4800   0 disqualified .044 9.4 .50 0 true .13 16 1.3 2 true 12   530 90 2 error (5) .035 5.7 .088 0 error (5) .031 5.6 .12  0
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout 900     570 7200    0 true 58   4400 370 2 error (42) 870     2200   13000    0 out of memory 120     15000   1600    0 true 6.5 370 59 2 unknown .84 66 8.7 0 unknown .027 4.6 .23  0 unknown .027 4.6 .19  0 timeout 900     790 11000    0 true 6.9 370 62 2 timeout 900    440 5200   0 disqualified .043 9.5 .42 0 timeout (verification) 900    2900 9300   0 true 12   470 120 2 error (5) .031 5.6 .20  0 error (5) .025 5.6 .16  0
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true .35  30 3.3  2 true 34   3400 240 2 true 2.5   120   33    2 out of memory 160     15000   1700    0 unknown 25   870 190 0 unknown .83 66 9.0 0 unknown .029 4.6 .15  0 unknown .032 4.6 .22  0 true 4.3   30 65    2 timeout 900   5100 10000 0 out of memory 52    15000 740   0 disqualified .046 9.5 .46 0 true 590    120 5800   2 true 8.5 350 71 2 error (5) .027 5.6 .11  0 error (5) .031 5.6 .19  0
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c error (134) .25  46 2.2  0 true 8.9 490 80 2 error (42) 880     5300   5600    0 error (42) 880     340   6900    0 timeout 900   3000 13000 0 unknown .95 65 9.8 0 unknown .032 4.7 .27  0 unknown .044 4.5 .17  0 timeout 900     2900 10000    0 timeout 900   2900 14000 0 timeout 900    890 6900   0 disqualified .043 9.4 .40 0 timeout (verification) 900    120 12000   0 true 12   560 91 2 error (5) .026 5.7 .15  0 error (5) .023 5.6 .13  0
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c error (134) .27  46 1.8  0 true 59   4100 430 2 error (42) 870     1000   6800    0 out of memory 190     15000   2500    0 timeout 900   3400 12000 0 unknown 1.1  66 13   0 unknown .033 4.7 .25  0 unknown .027 4.6 .16  0 timeout 900     1500 11000    0 timeout 900   3700 12000 0 timeout 900    720 8000   0 disqualified .046 9.4 .45 0 timeout (verification) 900    330 11000   0 true 110   760 1300 2 error (5) .031 5.7 .18  0 error (5) .026 5.6 .15  0
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c error (134) .23  46 2.0  0 true 5.6 310 50 2 error (42) 880     6100   3500    0 error (42) 880     340   5700    0 unknown 20   870 170 0 unknown .92 67 9.1 0 unknown .047 4.6 .16  0 unknown .037 4.7 .13  0 timeout 900     2100 10000    0 unknown 20   900 180 0 timeout 900    1100 13000   0 disqualified .060 8.9 .35 0 timeout (verification) 900    420 12000   0 true 10   470 77 2 error (5) .026 5.7 .099 0 error (5) .026 5.6 .12  0
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c error (134) .29  46 1.8  0 true 40   3000 290 2 error (42) 880     1000   5700    0 out of memory 190     15000   2500    0 timeout 900   3700 12000 0 unknown 1.1  67 12   0 unknown .051 4.7 .27  0 unknown .029 4.6 .21  0 timeout 900     1900 9300    0 timeout 900   3700 12000 0 timeout 900    710 6100   0 disqualified .073 9.1 .42 0 timeout (verification) 900    410 13000   0 true 20   610 180 2 error (5) .023 5.7 .082 0 error (5) .028 5.5 .20  0
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c error (134) .25  47 1.8  0 true 37   3100 270 2 error (42) 870     990   6400    0 out of memory 190     15000   2400    0 timeout 900   3700 13000 0 unknown 1.1  66 13   0 unknown .029 4.6 .16  0 unknown .031 4.6 .18  0 timeout 900     1700 8500    0 timeout 900   3400 13000 0 timeout 900    710 5600   0 disqualified .044 9.4 .40 0 timeout (verification) 900    420 12000   0 true 22   730 210 2 error (5) .026 5.6 .12  0 error (5) .023 5.7 .13  0
termination-crafted-lit/genady_true-termination_true-no-overflow.c true .27  24 2.5  2 true 9.7 750 75 2 true 3.1   62   42    2 true 3.1   33   41    2 out of memory 670   15000 6900 0 unknown .77 67 9.0 0 unknown .033 4.6 .21  0 unknown .046 4.6 .21  0 true 160     2900 2200    2 out of memory 500   15000 7100 0 true 2.1  59 26   2 disqualified .050 9.2 .42 0 true .12 15 1.3 2 true 8.7 380 68 2 error (5) .024 5.7 .13  0 error (5) .021 5.6 .19  0
termination-crafted-lit/strchr_true-no-overflow_true-termination.c error (134) .25  46 2.0  0 true 6.1 420 45 2 error (42) 880     5500   5500    0 error (42) 880     380   7100    0 unknown 25   1000 210 0 unknown .89 66 11   0 unknown .027 4.7 .18  0 unknown .036 4.6 .18  0 timeout 900     1200 11000    0 unknown 27   1300 240 0 timeout 900    680 6100   0 disqualified .050 9.2 .45 0 timeout (verification) 900    480 11000   0 true 12   580 100 2 error (5) .022 5.6 .10  0 error (5) .037 5.7 .086 0
termination-numeric/Ackermann01_true-termination_true-no-overflow.c error (5) .093 24 .78 0 true 28   2000 240 2 error (42) 880     240   4200    0 out of memory 170     15000   2400    0 true 6.3 370 55 2 out of memory (false(no-overflow)) 280    15000 3300   0 unknown .032 4.7 .17  0 unknown .028 4.6 .21  0 out of memory 440     15000 5200    0 error (recursion) 3.3 270 28 0 out of memory 54    15000 700   0 disqualified .040 9.0 .41 0 probably out of memory (killed (signal 9, verification)) 830    15000 11000   0 true 40   970 380 2 error (5) .044 5.5 .13  0 error (5) .025 5.6 .11  0
termination-numeric/Binomial_true-termination_false-no-overflow.c error (5) .098 24 .83 0 error (1) 9.9 710 92 0 error (42) 880     600   4500    0 out of memory 220     15000   2500    0 error (recursion) 4.0 280 40 0 unknown 3.1  110 34   0 unknown .029 4.6 .20  0 unknown .034 4.6 .20  0 timeout 900     6300 13000    0 error (recursion) 3.3 270 29 0 timeout 900    15000 10000   0 disqualified .072 9.4 .39 0 true 2.0  110 30   2 timeout 900   1100 11000 0 error (5) .029 5.6 .12  0 error (5) .028 5.7 .14  0
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c error (5) .095 24 .84 0 true 9.1 680 65 2 error (42) 880     2700   7000    0 error (42) 880     320   10000    0 true 4.9 300 40 2 unknown .84 67 9.0 0 unknown .039 4.6 .23  0 unknown .046 4.7 .24  0 timeout 900     1500 10000    0 error (recursion) 3.2 270 31 0 out of memory 100    15000 1300   0 disqualified .046 9.4 .41 0 timeout (verification) 900    1700 13000   0 true 10   480 86 2 error (5) .026 5.6 .10  0 error (5) .027 5.6 .10  0
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c error (5) .13  24 .73 0 true 18   1100 140 2 error (42) 880     190   3400    0 out of memory 140     15000   2000    0 true 4.6 290 42 2 out of memory (false(no-overflow)) 220    15000 2500   0 unknown .055 4.6 .14  0 unknown .030 4.7 .14  0 out of memory 340     15000 4300    0 error (recursion) 3.2 270 29 0 out of memory 44    15000 540   0 disqualified .044 9.6 .44 0 timeout (verification) 900    14000 8600   0 timeout 900   14000 7800 0 error (5) .051 5.5 .15  0 error (5) .045 5.5 .071 0
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c error (5) .12  24 .94 0 true 9.4 600 68 2 out of memory 550     15000   3600    0 error (42) 880     1000   10000    0 true 4.9 290 49 2 unknown .83 66 8.5 0 unknown .029 4.6 .13  0 unknown .028 4.6 .20  0 timeout 900     890 11000    0 error (recursion) 3.2 270 30 0 timeout 900    5100 6200   0 disqualified .076 9.5 .35 0 true .15 18 2.1 2 true 8.8 380 64 2 error (5) .022 5.7 .13  0 error (5) .045 5.5 .17  0
termination-numeric/LogRecursive_true-termination_true-no-overflow.c error (5) .093 24 .86 0 timeout 900   3800 11000 0 true 1.5   68   18    2 true 1.8   68   20    2 exception 3.6 280 33 0 unknown 1.1  66 14   0 unknown .033 4.7 .24  0 unknown .029 4.5 .16  0 true 41     140 490    2 error (recursion) 3.3 270 30 0 true 5.1  620 64   2 disqualified .050 8.9 .40 0 true 21    160 250   2 unknown 58   660 710 0 error (5) .023 5.6 .19  0 error (5) .046 5.5 .14  0
termination-numeric/Parts_true-termination_true-no-overflow.c error (5) .097 24 1.3  0 timeout 900   13000 8800 0 error (42) 870     570   6300    0 error (42) 880     14000   11000    0 error (recursion) 4.1 280 38 0 unknown 260    4600 3900   0 unknown .036 4.6 .23  0 unknown .036 4.6 .25  0 timeout 900     8500 11000    0 error (recursion) 3.4 280 29 0 timeout 900    630 5100   0 disqualified .046 10   .39 0 timeout (verification) 900    10000 11000   0 true 67   1100 560 2 error (5) .024 5.5 .14  0 error (5) .039 5.6 .12  0
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c error (5) .094 24 .76 0 true 7.9 480 63 2 out of memory 650     15000   3300    0 error (42) 880     740   12000    0 true 4.7 290 42 2 unknown .79 66 9.4 0 unknown .028 4.6 .21  0 unknown .030 4.6 .18  0 timeout 900     1200 10000    0 error (recursion) 3.3 270 29 0 timeout 900    7500 4800   0 disqualified .042 9.2 .64 0 timeout (verification) 900    460 8000   0 true 8.8 380 69 2 error (5) .038 5.6 .16  0 error (5) .032 5.5 .091 0
termination-numeric/TwoWay_true-termination_true-no-overflow.c error (5) .096 24 .79 0 true 11   720 91 2 error (42) 880     9800   5100    0 error (42) 880     1000   11000    0 unknown 7.3 490 64 0 unknown .80 65 7.7 0 unknown .033 4.6 .26  0 unknown .033 4.6 .25  0 timeout 900     920 12000    0 error (recursion) 3.2 270 31 0 out of memory 150    15000 2100   0 disqualified .054 9.4 .29 0 timeout (verification) 900    430 6500   0 true 23   460 240 2 error (5) .026 5.6 .13  0 error (5) .026 5.5 .14  0
termination-numeric/gcd01_true-termination_true-no-overflow.c error (5) .096 24 .88 0 true 11   720 87 2 error (42) 870     13000   9800    0 out of memory 520     15000   5900    0 unknown 4.9 310 45 0 out of memory (false(no-overflow)) 270    15000 3100   0 unknown .029 4.7 .21  0 unknown .031 4.6 .18  0 out of memory 410     15000 4900    0 error (recursion) 3.4 270 30 0 out of memory 180    15000 2500   0 disqualified .043 9.4 .39 0 timeout (verification) 900    50 12000   0 true 14   520 150 2 error (5) .024 5.6 .10  0 error (5) .022 5.7 .11  0
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true .27  25 2.6  2 true 5.6 340 49 2 true .45  15   6.2  2 true .61  15   6.9  2 unknown 11   520 100 0 unknown .76 65 9.3 0 unknown .062 4.7 .20  0 unknown .025 4.6 .23  0 true .14  26 1.6  2 unknown 12   530 98 0 true .66 120 6.9 2 disqualified .069 9.2 .42 0 true .38 17 5.0 2 true 8.6 350 79 2 error (5) .023 5.7 .16  0 error (5) .035 5.6 .20  0
termination-numeric/recHanoi02_true-termination_true-no-overflow.c error (5) .097 24 .78 0 true 7.6 460 62 2 true .24  9.3 3.3  2 true .45  9.5 5.2  2 true 4.7 290 42 2 unknown .79 67 8.4 0 unknown .026 4.6 .25  0 unknown .029 4.6 .16  0 true .16  26 1.7  2 error (recursion) 3.2 270 30 0 true .59 61 6.6 2 disqualified .044 9.3 .40 0 true .40 18 4.5 2 true 11   410 84 2 error (5) .023 5.6 .17  0 error (5) .023 5.5 .15  0
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (5) .12  24 .70 0 true 14   780 110 2 error (42) 880     550   4800    0 error (42) 870     300   10000    0 error (recursion) 3.9 280 34 0 unknown .84 66 9.2 0 unknown .027 4.6 .25  0 unknown .058 4.6 .14  0 timeout 900     2000 9700    0 error (recursion) 3.2 270 30 0 out of memory 740    15000 8100   0 disqualified .043 9.1 .45 0 timeout (verification) 900    960 12000   0 true 12   480 89 2 error (5) .023 5.6 .12  0 error (5) .028 5.7 .13  0
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (5) .11  24 .91 0 true 16   800 110 2 error (42) 870     550   2900    0 error (42) 880     300   12000    0 error (recursion) 3.9 280 35 0 unknown .85 66 10   0 unknown .062 4.7 .20  0 unknown .028 4.6 .20  0 timeout 900     1700 8800    0 error (recursion) 3.2 270 29 0 out of memory 740    15000 10000   0 disqualified .043 9.0 .41 0 timeout (verification) 900    800 13000   0 true 12   530 120 2 error (5) .028 5.6 .24  0 error (5) .025 5.5 .16  0
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 900     32 10000    0 true 59   3100 450 2 error (42) 880     1200   6400    0 out of memory 520     15000   6900    0 timeout 900   4100 12000 0 unknown 330    170 4500   0 unknown .030 4.6 .18  0 unknown .030 4.6 .12  0 timeout 900     1900 9800    0 timeout 900   3900 13000 0 timeout 900    460 5500   0 disqualified .056 9.4 .32 0 timeout (verification) 900    1300 11000   0 true 11   400 110 2 error (5) .028 5.7 .25  0 error (5) .029 5.6 .16  0
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c timeout 900     1900 4800    0 true 22   2000 170 2 error (42) 880     1800   5200    0 out of memory 110     15000   1300    0 true 6.9 350 64 2 unknown 1.6  66 21   0 unknown .038 4.6 .15  0 unknown .028 4.6 .23  0 timeout 900     1200 11000    0 true 6.5 370 59 2 timeout 900    350 4300   0 disqualified .046 9.0 .38 0 timeout (verification) 900    410 8500   0 true 11   510 98 2 error (5) .026 5.7 .13  0 error (5) .027 5.6 .16  0
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c true .23  23 2.6  2 true 13   820 97 2 error (42) 880     5300   3500    0 error (42) 880     410   6300    0 unknown 4.8 290 42 0 unknown .81 67 8.3 0 unknown .027 4.6 .19  0 unknown .032 4.6 .19  0 timeout 900     160 12000    0 unknown 5.0 290 52 0 timeout 900    680 5500   0 disqualified .047 9.3 .40 0 timeout (verification) 900    92 13000   0 true 8.7 380 78 2 error (5) .025 5.6 .13  0 error (5) .024 5.5 .15  0
termination-restricted-15/GCD3_true-termination_true-no-overflow.c true .53  24 5.5  2 true 20   1100 140 2 error (42) 880     1100   5100    0 out of memory 98     15000   1300    0 unknown 5.1 290 43 0 unknown 1.8  67 20   0 unknown .030 4.6 .28  0 unknown .038 4.5 .25  0 timeout 900     990 11000    0 unknown 5.1 290 43 0 timeout 900    630 4300   0 disqualified .047 9.3 .37 0 timeout (verification) 900    64 12000   0 true 26   500 270 2 error (5) .025 5.6 .12  0 error (5) .024 5.6 .13  0
termination-restricted-15/GCD4_true-termination_true-no-overflow.c true .71  36 8.3  2 true 21   1300 130 2 error (42) 880     570   4700    0 out of memory 470     15000   6000    0 unknown 4.6 300 40 0 unknown 1.1  67 14   0 unknown .031 4.6 .23  0 unknown .029 4.6 .21  0 timeout 900     1000 11000    0 unknown 4.8 290 37 0 timeout 900    700 5100   0 disqualified .042 9.1 .72 0 timeout (verification) 900    66 12000   0 true 23   530 270 2 error (5) .026 5.8 .16  0 error (5) .027 5.6 .16  0
termination-restricted-15/IntPath_true-termination_true-no-overflow.c timeout 900     3400 12000    0 true 2.8 220 26 2 true .046 7.3 .43 2 true .035 6.7 .34 2 true 3.4 280 36 2 unknown .79 67 7.7 0 unknown .032 4.7 .19  0 unknown .030 4.5 .18  0 true .073 26 .94 2 true 3.4 280 28 2 true .36 58 3.7 2 disqualified .040 9.5 .42 0 true .14 17 1.7 2 true 7.7 340 64 2 error (5) .026 5.6 .12  0 error (5) .023 5.6 .16  0
termination-restricted-15/LogAG_true-termination_true-no-overflow.c out of memory 270     15000 2200    0 true 16   1200 130 2 error (42) 880     810   5500    0 out of memory 470     15000   7000    0 true 5.6 340 52 2 unknown 1.0  65 13   0 unknown .031 4.6 .20  0 unknown .029 4.7 .20  0 timeout 900     880 11000    0 true 5.8 330 55 2 timeout 900    410 4800   0 disqualified .049 9.6 .45 0 true .23 18 3.2 2 true 10   450 99 2 error (5) .026 5.6 .12  0 error (5) .052 5.7 .098 0
termination-restricted-15/Log_true-termination_true-no-overflow.c true .55  71 5.9  2 true 7.1 460 57 2 error (42) 870     810   5100    0 out of memory 470     15000   6100    0 true 6.3 380 54 2 unknown 1.0  66 13   0 unknown .030 4.6 .17  0 unknown .028 4.6 .34  0 timeout 900     870 11000    0 true 6.5 380 54 2 timeout 900    420 4400   0 disqualified .069 9.2 .36 0 true .18 17 1.9 2 true 11   460 94 2 error (5) .023 5.6 .18  0 error (5) .028 5.7 .14  0
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c true .19  24 1.5  2 true 9.2 490 71 2 error (42) 880     1600   7800    0 out of memory 130     15000   1700    0 true 9.6 460 81 2 unknown .79 65 7.6 0 unknown .025 4.8 .19  0 unknown .029 4.6 .16  0 timeout 900     360 12000    0 timeout 900   750 10000 0 out of memory 43    15000 520   0 disqualified .045 9.8 .40 0 timeout (verification) 900    96 9500   0 true 19   550 170 2 error (5) .028 5.6 .16  0 error (5) .024 5.6 .12  0
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c true .14  24 1.5  2 true 2.9 220 23 2 true .078 6.3 .19 2 true .041 6.4 .36 2 true 4.5 290 45 2 unknown .77 66 7.8 0 unknown .052 4.8 .13  0 unknown .030 4.7 .21  0 true .11  26 .94 2 true 4.4 290 47 2 true .36 59 3.4 2 disqualified .043 9.3 .44 0 true .18 17 1.8 2 true 9.7 380 86 2 error (5) .024 5.6 .12  0 error (5) .033 5.6 .13  0
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c timeout 900     1500 5100    0 true 23   1000 140 2 error (42) 880     840   4400    0 out of memory 190     15000   3000    0 true 7.4 350 61 2 unknown 1.3  66 17   0 unknown .042 4.7 .19  0 unknown .029 4.6 .16  0 timeout 900     1100 13000    0 true 7.3 420 63 2 timeout 900    530 5600   0 disqualified .046 9.5 .48 0 timeout (verification) 900    420 8200   0 true 9.3 390 73 2 error (5) .025 5.6 .10  0 error (5) .031 5.7 .19  0
termination-restricted-15/Nested_true-termination_true-no-overflow.c true .27  30 3.2  2 true 7.1 430 55 2 true .089 6.8 .55 2 true .095 6.5 .69 2 true 22   650 220 2 unknown .79 66 8.4 0 unknown .030 4.7 .15  0 unknown .037 4.8 .20  0 true .087 26 1.1  2 true 23   680 240 2 true .35 58 4.2 2 disqualified .059 9.1 .46 0 true .11 15 1.2 2 true 9.8 380 82 2 error (5) .024 5.7 .11  0 error (5) .024 5.6 .11  0
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c true .21  24 1.9  2 true 5.6 320 45 2 error (42) 880     1700   9100    0 out of memory 190     15000   2400    0 true 4.8 290 45 2 unknown .81 68 10   0 unknown .032 4.6 .19  0 unknown .043 4.6 .16  0 timeout 900     350 12000    0 true 5.1 300 43 2 timeout 900    350 3900   0 disqualified .044 9.3 .45 0 timeout (verification) 900    41 12000   0 true 14   490 150 2 error (5) .026 5.7 .17  0 error (5) .027 5.6 .15  0
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c true .31  34 2.9  2 true 12   720 74 2 error (42) 880     550   4800    0 out of memory 400     15000   5200    0 true 5.1 300 43 2 unknown .84 66 9.4 0 unknown .046 4.5 .15  0 unknown .027 4.8 .18  0 timeout 900     1500 9400    0 true 5.1 300 40 2 timeout 900    360 4400   0 disqualified .045 9.2 .41 0 true .13 16 1.6 2 true 11   460 83 2 error (5) .051 5.6 .20  0 error (5) .031 5.5 .17  0
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c true .15  24 1.6  2 true 4.2 300 33 2 error (42) 880     6100   3700    0 error (42) 880     390   7900    0 true 4.3 290 40 2 unknown .77 67 7.9 0 unknown .031 4.6 .19  0 unknown .029 4.6 .18  0 timeout 900     290 14000    0 true 4.3 290 45 2 timeout 900    400 3400   0 disqualified .044 9.4 .40 0 true .13 16 1.3 2 true 8.7 370 68 2 error (5) .024 5.7 .090 0 error (5) .028 5.6 .097 0
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c true .27  24 2.1  2 true 6.2 440 53 2 error (42) 880     5600   4200    0 error (42) 880     510   7500    0 true 4.6 290 38 2 unknown .80 66 7.6 0 unknown .036 4.6 .15  0 unknown .054 4.6 .16  0 timeout 900     410 10000    0 true 4.6 290 40 2 timeout 900    550 3200   0 disqualified .043 9.1 .41 0 true .12 16 1.5 2 true 8.2 360 67 2 error (5) .024 5.6 .18  0 error (5) .025 5.6 .11  0
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c true .34  37 3.2  2 true 5.2 380 42 2 error (42) 870     810   5200    0 out of memory 410     15000   4700    0 true 5.6 300 53 2 unknown 1.2  65 15   0 unknown .065 4.8 .16  0 unknown .032 4.6 .18  0 timeout 900     790 11000    0 true 6.2 320 49 2 timeout 900    410 4200   0 disqualified .044 9.4 .50 0 true .16 17 2.2 2 true 8.9 370 81 2 error (5) .024 5.6 .13  0 error (5) .024 5.6 .15  0
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c true .36  24 3.6  2 true 5.0 300 43 2 error (42) 880     810   4700    0 out of memory 430     15000   5300    0 true 5.7 320 55 2 unknown 1.2  65 15   0 unknown .032 4.5 .24  0 unknown .034 4.6 .17  0 timeout 900     960 11000    0 true 5.8 310 54 2 timeout 900    490 4100   0 disqualified .043 9.1 .42 0 true .28 18 3.3 2 true 10   400 88 2 error (5) .022 5.6 .13  0 error (5) .025 5.7 .14  0
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c true .19  24 2.0  2 true 9.9 480 72 2 error (42) 880     550   5000    0 out of memory 400     15000   4600    0 true 4.7 290 41 2 unknown 1.0  67 12   0 unknown .055 4.6 .14  0 unknown .027 4.5 .28  0 timeout 900     810 12000    0 true 4.8 290 47 2 timeout 900    400 3700   0 disqualified .046 9.3 .47 0 true .13 16 1.6 2 true 8.7 350 78 2 error (5) .028 5.7 .12  0 error (5) .023 5.7 .11  0
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c true .28  24 2.8  2 true 9.6 470 68 2 error (42) 880     550   5500    0 out of memory 410     15000   4600    0 true 4.9 290 44 2 unknown 1.1  66 12   0 unknown .029 4.6 .16  0 unknown .033 4.5 .22  0 timeout 900     1100 11000    0 true 5.2 290 42 2 timeout 900    390 3500   0 disqualified .047 9.6 .43 0 true .14 15 1.5 2 true 9.3 400 80 2 error (5) .025 5.6 .18  0 error (5) .029 5.6 .20  0
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c true .20  24 2.0  2 true 4.4 300 33 2 error (42) 880     6100   4600    0 error (42) 880     380   5600    0 true 4.2 280 35 2 unknown .83 67 9.4 0 unknown .055 4.5 .14  0 unknown .030 4.6 .19  0 timeout 900     340 12000    0 true 4.3 290 39 2 timeout 900    400 4200   0 disqualified .048 9.5 .36 0 true .12 16 1.5 2 true 8.3 360 65 2 error (5) .023 5.6 .16  0 error (5) .029 5.7 .16  0
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c true .20  24 1.3  2 true 5.0 310 41 2 error (42) 880     4900   3200    0 error (42) 870     420   5800    0 true 4.5 300 42 2 unknown .81 66 8.3 0 unknown .035 4.6 .17  0 unknown .055 4.7 .14  0 timeout 900     310 11000    0 true 4.7 290 42 2 timeout 900    510 6200   0 disqualified .044 9.8 .48 0 timeout (verification) 900    490 6200   0 true 8.4 350 66 2 error (5) .026 5.6 .13  0 error (5) .043 5.5 .12  0
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c true .23  24 2.3  2 true 2.6 210 21 2 true .071 6.4 .28 2 true .049 6.8 .33 2 unknown 4.4 290 38 0 unknown .77 67 9.4 0 unknown .031 4.6 .18  0 unknown .027 4.6 .23  0 true .10  26 .76 2 unknown 4.3 300 40 0 true .37 59 3.2 2 disqualified .058 9.3 .50 0 true .15 18 1.8 2 true 11   390 100 2 error (5) .018 5.6 .16  0 error (5) .025 5.6 .15  0
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c true .23  23 2.1  2 true 5.5 350 45 2 error (42) 880     6700   5900    0 error (42) 880     400   5500    0 true 4.4 280 41 2 unknown .83 66 8.9 0 unknown .059 4.7 .20  0 unknown .035 4.6 .25  0 timeout 900     560 11000    0 true 4.4 290 44 2 timeout 900    560 5400   0 disqualified .046 9.3 .38 0 timeout (verification) 900    530 6700   0 true 8.5 360 64 2 error (5) .029 5.6 .15  0 error (5) .026 5.6 .14  0
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c true .26  24 2.7  2 true 6.1 440 48 2 error (42) 880     5700   4200    0 error (42) 880     500   6300    0 true 4.5 290 42 2 unknown .81 66 8.5 0 unknown .030 4.8 .17  0 unknown .027 4.7 .18  0 timeout 900     420 13000    0 true 4.6 290 39 2 timeout 900    550 3800   0 disqualified .046 9.1 .41 0 true .13 16 1.4 2 true 7.8 340 67 2 error (5) .049 5.6 .12  0 error (5) .025 5.6 .16  0
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c true .24  24 2.1  2 true 15   650 93 2 error (42) 880     1700   11000    0 out of memory 190     15000   2500    0 true 5.5 310 48 2 unknown .83 65 8.8 0 unknown .027 4.6 .17  0 unknown .035 4.6 .18  0 timeout 900     300 10000    0 true 5.2 290 41 2 timeout 900    380 4000   0 disqualified .046 9.8 .42 0 timeout (verification) 900    120 13000   0 true 11   450 93 2 error (5) .030 5.5 .22  0 error (5) .025 5.5 .16  0
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c true .28  24 2.2  2 true 6.8 450 56 2 error (42) 880     4500   4700    0 error (42) 880     470   5600    0 true 4.5 290 38 2 unknown .85 66 9.5 0 unknown .031 4.6 .16  0 unknown .032 4.6 .21  0 timeout 900     400 11000    0 true 4.6 290 43 2 timeout 900    550 3700   0 disqualified .049 9.5 .45 0 timeout (verification) 900    570 6600   0 true 19   380 240 2 error (5) .026 5.6 .16  0 error (5) .023 5.6 .076 0
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c true .55  39 5.0  2 true 19   1200 130 2 error (42) 880     1600   8400    0 out of memory 210     15000   2300    0 true 5.5 300 48 2 unknown .78 67 8.7 0 unknown .028 4.6 .17  0 unknown .032 4.6 .24  0 timeout 900     730 11000    0 true 5.6 320 44 2 timeout 900    490 5400   0 disqualified .042 9.3 .38 0 timeout (verification) 900    2800 8700   0 true 10   450 78 2 error (5) .024 5.6 .14  0 error (5) .024 5.5 .13  0
termination-restricted-15/Sequence_true-termination_true-no-overflow.c true .22  24 1.8  2 true 6.2 380 50 2 true .21  6.6 1.1  2 true .13  6.3 2.0  2 true 99   4300 1200 2 unknown .81 66 7.8 0 unknown .041 4.6 .11  0 unknown .046 4.7 .21  0 true .13  26 1.9  2 true 94   3300 1000 2 true .39 59 3.4 2 disqualified .062 9.2 .49 0 true .11 15 1.2 2 true 9.6 380 74 2 error (5) .030 5.6 .14  0 error (5) .028 5.6 .079 0
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c true .17  24 1.4  2 true 4.2 290 33 2 error (42) 880     6100   4400    0 error (42) 880     380   7300    0 true 4.3 290 41 2 unknown .77 67 9.8 0 unknown .032 4.6 .30  0 unknown .026 4.7 .19  0 timeout 900     500 12000    0 true 4.4 280 40 2 timeout 900    380 3400   0 disqualified .044 9.8 .44 0 true .12 16 1.1 2 true 8.7 380 69 2 error (5) .029 5.6 .22  0 error (5) .030 5.6 .19  0
termination-restricted-15/a.01_true-termination_true-no-overflow.c true .31  33 3.0  2 true 13   930 99 2 error (42) 880     550   5400    0 out of memory 420     15000   5400    0 true 5.7 310 46 2 unknown .84 66 9.4 0 unknown .031 4.6 .14  0 unknown .029 4.6 .17  0 timeout 900     1500 11000    0 true 5.3 310 51 2 timeout 900    440 6200   0 disqualified .050 9.1 .29 0 true .14 15 1.4 2 true 11   410 83 2 error (5) .034 5.6 .15  0 error (5) .031 5.5 .15  0
termination-restricted-15/a.04_true-termination_true-no-overflow.c true .16  24 1.2  2 true 4.2 290 36 2 error (42) 880     5700   3400    0 error (42) 880     380   6600    0 true 4.3 280 36 2 unknown .80 67 9.1 0 unknown .055 4.6 .24  0 unknown .027 4.6 .18  0 timeout 900     300 11000    0 true 4.2 290 38 2 timeout 900    410 4300   0 disqualified .058 9.5 .33 0 true .13 16 1.3 2 true 8.2 360 65 2 error (5) .049 5.6 .18  0 error (5) .040 5.5 .093 0
termination-restricted-15/a.05_true-termination_true-no-overflow.c true .16  24 1.1  2 true 4.5 360 33 2 error (42) 880     6600   4800    0 error (42) 880     360   5100    0 true 4.7 290 41 2 unknown .83 66 10   0 unknown .035 4.6 .23  0 unknown .056 4.6 .18  0 timeout 900     340 10000    0 true 4.8 300 42 2 timeout 900    480 5200   0 disqualified .047 9.5 .39 0 true .13 16 1.4 2 true 7.8 350 68 2 error (5) .053 5.5 .15  0 error (5) .028 5.6 .13  0
termination-restricted-15/a.06_true-termination_true-no-overflow.c true .15  24 1.3  2 true 43   2300 460 2 error (42) 880     5500   3600    0 error (42) 880     1200   5500    0 true 5.2 310 48 2 unknown .86 66 9.1 0 unknown .030 4.6 .19  0 unknown .033 4.6 .31  0 timeout 900     320 11000    0 true 5.0 300 50 2 timeout 900    990 3600   0 disqualified .044 9.4 .55 0 timeout (verification) 900    450 8000   0 true 9.8 470 86 2 error (5) .023 5.6 .095 0 error (5) .051 5.5 .17  0
termination-restricted-15/a.07_true-termination_true-no-overflow.c true .25  24 2.1  2 true 6.2 430 54 2 error (42) 880     5300   3700    0 error (42) 880     510   7700    0 true 4.7 290 43 2 unknown .80 66 10   0 unknown .035 4.6 .23  0 unknown .029 4.8 .19  0 timeout 900     410 10000    0 true 4.6 290 43 2 timeout 900    550 3700   0 disqualified .052 9.2 .31 0 true .13 16 1.3 2 true 9.0 370 74 2 error (5) .035 5.5 .17  0 error (5) .043 5.7 .15  0
termination-restricted-15/a.08_true-termination_true-no-overflow.c true .19  23 1.4  2 true 5.3 350 45 2 error (42) 880     5400   4900    0 error (42) 880     420   6100    0 true 4.8 290 41 2 unknown .82 66 8.5 0 unknown .034 4.6 .18  0 unknown .041 4.6 .20  0 timeout 900     320 12000    0 true 5.0 300 50 2 timeout 900    530 4100   0 disqualified .041 9.2 .47 0 timeout (verification) 900    580 6100   0 true 8.7 360 66 2 error (5) .028 5.6 .098 0 error (5) .031 5.6 .11  0
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c true .15  24 1.2  2 true 10   510 85 2 error (42) 880     5100   4200    0 error (42) 880     490   6100    0 unknown 4.3 280 36 0 unknown .81 65 8.1 0 unknown .054 4.6 .16  0 unknown .023 4.8 .065 0 timeout 900     180 10000    0 unknown 4.5 280 40 0 timeout 900    8500 4300   0 disqualified .044 9.6 .38 0 timeout (verification) 900    120 8900   0 true 21   660 210 2 error (5) .025 5.6 .18  0 error (5) .026 5.7 .24  0
termination-restricted-15/a.10_true-termination.c true .20  24 2.1  2 true 2.6 210 22 2 error (42) 880     1700   7900    0 out of memory 200     15000   2700    0 true 4.9 290 48 2 unknown .78 66 8.5 0 unknown .030 4.5 .16  0 unknown .033 4.7 .17  0 timeout 900     330 13000    0 true 5.2 290 44 2 timeout 900    360 5200   0 disqualified .044 9.5 .43 0 timeout (verification) 900    42 12000   0 true 14   450 140 2 error (5) .023 5.6 .15  0 error (5) .049 5.7 .16  0
termination-restricted-15/b.01_true-termination_true-no-overflow.c true .22  24 1.7  2 true 4.6 300 37 2 error (42) 880     6400   4800    0 error (42) 880     390   8500    0 true 4.4 280 38 2 unknown .80 66 7.0 0 unknown .030 4.6 .19  0 unknown .031 4.7 .20  0 timeout 900     340 9600    0 true 4.5 290 46 2 timeout 900    390 3600   0 disqualified .051 9.4 .31 0 true .12 16 1.8 2 true 8.1 350 74 2 error (5) .036 5.6 .17  0 error (5) .025 5.6 .12  0
termination-restricted-15/b.02_true-termination_true-no-overflow.c true .19  24 1.8  2 true 5.6 350 48 2 error (42) 880     5000   2400    0 error (42) 880     420   5900    0 true 4.5 290 40 2 unknown .80 66 8.5 0 unknown .036 4.7 .17  0 unknown .032 4.6 .17  0 timeout 900     320 11000    0 true 4.6 290 39 2 timeout 900    500 5200   0 disqualified .048 9.5 .54 0 timeout (verification) 900    500 7400   0 true 8.7 370 68 2 error (5) .026 5.6 .16  0 error (5) .030 5.7 .12  0
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c true .14  24 1.3  2 true 8.0 450 60 2 error (42) 880     3700   2900    0 error (42) 880     490   5500    0 unknown 4.2 280 35 0 unknown .81 66 10   0 unknown .025 4.6 .22  0 unknown .032 4.7 .23  0 timeout 900     180 10000    0 unknown 4.4 290 39 0 timeout 900    6700 5800   0 disqualified .045 9.2 .56 0 timeout (verification) 900    110 11000   0 true 21   640 190 2 error (5) .041 5.6 .086 0 error (5) .026 5.5 .12  0
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c true .14  23 3.1  2 true 7.8 460 58 2 error (42) 880     3600   3700    0 error (42) 880     490   5900    0 unknown 4.2 280 40 0 unknown .80 66 7.8 0 unknown .061 4.7 .15  0 unknown .054 4.6 .14  0 timeout 900     190 11000    0 unknown 4.2 290 40 0 timeout 900    6800 4000   0 disqualified .044 9.2 .39 0 timeout (verification) 900    120 11000   0 true 20   610 200 2 error (5) .027 5.7 .12  0 error (5) .022 5.6 .16  0
termination-restricted-15/b.04_true-termination_true-no-overflow.c true .32  33 3.2  2 true 2.6 210 23 2 true .053 6.9 .39 2 true .053 6.3 .26 2 unknown 4.5 300 48 0 unknown .82 66 7.7 0 unknown .028 4.7 .27  0 unknown .027 4.6 .19  0 true .082 26 1.1  2 unknown 4.2 280 39 0 true .36 58 3.0 2 disqualified .047 9.4 .36 0 true .15 18 1.7 2 true 13   380 120 2 error (5) .022 5.7 .15  0 error (5) .024 5.6 .093 0
termination-restricted-15/b.05_true-termination_true-no-overflow.c true .23  24 1.9  2 true 27   3500 320 2 true .059 6.4 .36 2 true .042 6.4 .37 2 true 4.8 310 42 2 unknown .82 67 8.7 0 unknown .032 5.3 .19  0 unknown .032 4.7 .20  0 true .085 26 .88 2 true 4.9 310 45 2 true .36 59 3.3 2 disqualified .043 9.3 .49 0 true .16 18 2.1 2 true 9.0 380 71 2 error (5) .024 5.8 .17  0 error (5) .025 5.9 .14  0
termination-restricted-15/b.06_true-termination_true-no-overflow.c true .27  26 2.2  2 true 8.4 560 71 2 error (42) 880     5200   5700    0 error (42) 880     410   5200    0 true 4.6 290 38 2 unknown .81 66 9.3 0 unknown .045 4.7 .13  0 unknown .036 4.7 .27  0 timeout 900     710 10000    0 true 4.7 290 44 2 timeout 900    560 5500   0 disqualified .057 9.5 .35 0 timeout (verification) 900    530 7800   0 true 8.4 350 63 2 error (5) .024 5.6 .10  0 error (5) .024 5.7 .15  0
termination-restricted-15/b.07_true-termination_true-no-overflow.c true .25  24 1.7  2 true 6.6 440 56 2 error (42) 880     5600   4500    0 error (42) 880     510   5400    0 true 4.5 280 39 2 unknown .82 66 8.8 0 unknown .030 4.6 .18  0 unknown .030 4.6 .20  0 timeout 900     430 11000    0 true 4.7 290 40 2 timeout 900    540 4300   0 disqualified .043 9.1 .50 0 true .13 15 1.5 2 true 8.2 350 68 2 error (5) .051 5.6 .14  0 error (5) .031 5.5 .098 0
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c timeout 900     2300 12000    0 true 2.6 220 25 2 error (42) 880     1800   10000    0 out of memory 200     15000   2700    0 true 4.8 290 46 2 unknown .82 67 7.8 0 unknown .028 4.8 .23  0 unknown .039 4.7 .15  0 timeout 900     620 11000    0 true 5.5 320 44 2 out of memory 99    15000 1200   0 disqualified .067 9.3 .38 0 timeout (verification) 900    240 7800   0 true 14   540 110 2 error (5) .036 5.5 .11  0 error (5) .032 5.7 .21  0
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c true .26  26 2.3  2 true 12   720 86 2 error (42) 880     1600   8200    0 out of memory 210     15000   2900    0 true 4.7 290 48 2 unknown .80 67 9.5 0 unknown .029 4.6 .21  0 unknown .055 4.6 .21  0 timeout 900     640 10000    0 true 4.8 290 40 2 out of memory 70    15000 740   0 disqualified .061 9.5 .75 0 timeout (verification) 900    120 9100   0 true 8.8 370 66 2 error (5) .024 5.6 .15  0 error (5) .024 5.6 .11  0
termination-restricted-15/b.10_true-termination_true-no-overflow.c true .23  24 1.9  2 true 16   850 130 2 error (42) 880     1800   9100    0 out of memory 150     15000   2200    0 true 5.8 310 52 2 unknown .86 66 8.1 0 unknown .033 4.8 .19  0 unknown .030 4.8 .21  0 timeout 900     400 12000    0 true 5.3 310 53 2 timeout 900    750 4600   0 disqualified .052 9.2 .33 0 timeout (verification) 900    210 7800   0 true 24   540 210 2 error (5) .020 5.6 .19  0 error (5) .022 5.7 .18  0
termination-restricted-15/b.11_true-termination_true-no-overflow.c true .21  24 1.8  2 true 8.9 560 63 2 error (42) 880     2200   9000    0 out of memory 160     15000   1900    0 true 5.6 300 44 2 unknown .85 66 9.7 0 unknown .030 4.6 .23  0 unknown .028 4.6 .18  0 timeout 900     410 11000    0 true 5.8 310 50 2 timeout 900    730 3500   0 disqualified .047 9.4 .37 0 timeout (verification) 900    150 7400   0 true 43   560 520 2 error (5) .025 5.6 .099 0 error (5) .024 5.6 .17  0
termination-restricted-15/b.12_true-termination_true-no-overflow.c true .25  24 1.9  2 true 11   520 76 2 error (42) 880     1400   8500    0 out of memory 130     15000   1600    0 true 5.0 290 44 2 unknown .81 66 7.9 0 unknown .030 4.7 .19  0 unknown .052 4.6 .16  0 timeout 900     570 11000    0 true 5.0 290 48 2 timeout 900    300 3900   0 disqualified .043 9.2 .45 0 timeout (verification) 900    460 6400   0 true 9.7 420 71 2 error (5) .025 5.6 .14  0 error (5) .027 5.6 .10  0
termination-restricted-15/b.13_true-termination_true-no-overflow.c true .19  24 1.8  2 true 11   540 86 2 error (42) 880     1400   9400    0 out of memory 140     15000   1800    0 true 5.4 290 49 2 unknown .84 66 8.8 0 unknown .037 4.6 .21  0 unknown .025 4.8 .37  0 timeout 900     570 12000    0 true 5.1 290 51 2 timeout 900    320 3700   0 disqualified .046 9.1 .44 0 timeout (verification) 900    480 6800   0 true 10   410 98 2 error (5) .040 5.5 .12  0 error (5) .024 5.7 .11  0
termination-restricted-15/b.14_true-termination_true-no-overflow.c true .69  67 7.1  2 true 6.5 430 51 2 error (42) 880     1100   4900    0 out of memory 450     15000   5200    0 true 5.8 310 58 2 unknown 1.2  66 16   0 unknown .037 4.6 .15  0 unknown .028 4.6 .22  0 timeout 900     850 12000    0 true 5.9 320 49 2 timeout 900    460 3900   0 disqualified .053 9.7 .39 0 true .15 17 1.7 2 true 9.5 400 72 2 error (5) .025 5.7 .15  0 error (5) .028 5.6 .15  0
termination-restricted-15/b.15_true-termination_true-no-overflow.c true .30  23 2.6  2 true 5.6 340 44 2 error (42) 880     810   5100    0 out of memory 440     15000   5400    0 true 5.8 310 52 2 unknown 1.2  65 14   0 unknown .048 4.7 .14  0 unknown .032 4.6 .15  0 timeout 900     950 12000    0 true 6.4 350 58 2 timeout 900    460 3800   0 disqualified .045 9.0 .42 0 true .29 18 2.9 2 true 10   410 84 2 error (5) .027 5.6 .13  0 error (5) .024 5.6 .15  0
termination-restricted-15/b.16_true-termination_true-no-overflow.c true .20  24 1.7  2 true 10   540 74 2 error (42) 880     550   4600    0 out of memory 410     15000   6300    0 true 4.9 300 43 2 unknown 1.0  67 13   0 unknown .027 4.6 .18  0 unknown .030 4.7 .23  0 timeout 900     810 11000    0 true 5.1 290 49 2 timeout 900    390 4900   0 disqualified .044 9.1 .46 0 true .13 16 1.5 2 true 9.4 380 69 2 error (5) .039 5.6 .24  0 error (5) .025 5.6 .15  0
termination-restricted-15/b.17_true-termination_true-no-overflow.c true .24  24 2.5  2 true 9.1 500 67 2 error (42) 880     550   6400    0 out of memory 430     15000   4900    0 true 5.1 300 43 2 unknown 1.1  66 12   0 unknown .031 4.6 .21  0 unknown .047 4.6 .17  0 timeout 900     1100 12000    0 true 5.2 290 44 2 timeout 900    430 4900   0 disqualified .048 9.3 .42 0 true .12 15 1.7 2 true 8.7 350 68 2 error (5) .031 5.5 .22  0 error (5) .027 5.7 .096 0
termination-restricted-15/b.18_true-termination_true-no-overflow.c true .43  40 4.6  2 true 6.4 350 49 2 error (42) 880     1100   4600    0 out of memory 110     15000   1500    0 true 7.1 360 63 2 unknown 1.6  67 19   0 unknown .028 4.6 .20  0 unknown .057 4.6 .22  0 timeout 900     1000 11000    0 true 6.9 360 62 2 timeout 900    360 4000   0 disqualified .043 9.5 .41 0 true .18 18 2.1 2 true 9.6 390 69 2 error (5) .024 5.5 .12  0 error (5) .027 5.6 .14  0
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c out of memory 180     15000 1200    0 true 19   1300 140 2 error (42) 880     2100   11000    0 out of memory 430     15000   5400    0 true 110   4000 1200 2 unknown .86 66 8.5 0 unknown .027 4.8 .22  0 unknown .044 4.6 .16  0 timeout 900     2300 13000    0 true 110   6600 1500 2 timeout 900    350 3900   0 disqualified .046 9.4 .44 0 timeout (verification) 900    300 11000   0 true 12   500 83 2 error (5) .024 5.7 .094 0 error (5) .023 5.6 .18  0
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c true .20  24 1.6  2 true 20   1400 120 2 error (42) 880     2100   10000    0 out of memory 430     15000   5400    0 true 7.5 430 54 2 unknown .88 66 8.9 0 unknown .029 4.6 .21  0 unknown .039 4.5 .27  0 timeout 900     2800 9100    0 true 7.9 420 68 2 timeout 900    420 8700   0 disqualified .048 9.3 .43 0 timeout (verification) 900    300 13000   0 true 9.9 440 93 2 error (5) .025 5.6 .10  0 error (5) .028 5.6 .14  0
termination-restricted-15/c.02_true-termination_true-no-overflow.c true .22  25 1.9  2 true 13   1200 88 2 error (42) 880     550   5400    0 out of memory 430     15000   5400    0 true 5.6 330 50 2 unknown .86 66 9.6 0 unknown .030 4.6 .19  0 unknown .028 4.6 .19  0 timeout 900     1400 10000    0 true 5.6 310 53 2 timeout 900    450 6800   0 disqualified .046 8.9 .67 0 timeout (verification) 900    510 6000   0 true 11   450 100 2 error (5) .029 5.9 .22  0 error (5) .023 5.7 .16  0
termination-restricted-15/c.03_true-termination_true-no-overflow.c true .24  24 2.8  2 true 17   660 130 2 error (42) 870     1700   7900    0 out of memory 210     15000   2700    0 true 5.4 310 50 2 unknown .83 66 11   0 unknown .030 4.6 .20  0 unknown .051 4.6 .21  0 timeout 900     350 14000    0 true 5.5 310 51 2 timeout 900    390 2900   0 disqualified .048 9.5 .35 0 timeout (verification) 900    170 11000   0 true 33   610 400 2 error (5) .021 5.6 .17  0 error (5) .038 5.6 .096 0
termination-restricted-15/c.07_true-termination_true-no-overflow.c true .30  31 3.4  2 true 7.2 450 61 2 error (42) 880     4200   3500    0 error (42) 880     550   4700    0 true 4.9 290 46 2 unknown .81 66 8.4 0 unknown .039 4.5 .16  0 unknown .033 4.6 .21  0 timeout 900     450 12000    0 true 5.1 310 45 2 timeout 900    640 5200   0 disqualified .042 9.3 .54 0 timeout (verification) 900    620 7700   0 true 8.3 360 71 2 error (5) .036 5.6 .095 0 error (5) .040 5.6 .15  0
termination-restricted-15/c.08_true-termination_true-no-overflow.c true .28  29 2.5  2 true 13   1100 100 2 error (42) 870     550   5400    0 out of memory 430     15000   5700    0 true 5.2 310 49 2 unknown .90 66 9.9 0 unknown .032 4.6 .24  0 unknown .032 4.6 .21  0 timeout 900     1600 11000    0 true 5.3 310 46 2 timeout 900    460 5300   0 disqualified .048 8.9 .39 0 true .12 16 1.7 2 true 11   440 84 2 error (5) .029 5.5 .11  0 error (5) .033 5.7 .15  0
termination-restricted-15/ex3a_true-termination_true-no-overflow.c true .27  27 2.4  2 true 6.8 420 54 2 true .11  11   1.1  2 true .18  10   1.0  2 exception 3.5 270 31 0 unknown .83 66 8.6 0 unknown .032 4.7 .30  0 unknown .028 4.7 .16  0 true .093 26 .96 2 exception 3.3 270 34 0 true .37 60 3.7 2 disqualified .045 9.4 .46 0 true .29 31 3.7 2 unknown 16   610 130 0 error (5) .024 5.6 .16  0 error (5) .039 5.5 .18  0
termination-restricted-15/ex3b_true-termination_true-no-overflow.c true .39  41 3.8  2 true 7.8 490 65 2 true .12  11   1.2  2 true .13  11   1.0  2 exception 3.4 270 35 0 unknown .80 67 9.8 0 unknown .054 4.6 .12  0 unknown .032 4.6 .20  0 true .12  28 1.3  2 exception 3.3 280 29 0 true .43 61 3.7 2 disqualified .046 9.6 .54 0 true 1.5  46 18   2 unknown 17   610 150 0 error (5) .027 5.7 .17  0 error (5) .026 5.6 .13  0
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c true .29  27 2.7  2 true 14   880 97 2 error (42) 880     5200   3500    0 error (42) 880     420   6500    0 unknown 4.7 300 40 0 unknown .84 66 9.8 0 unknown .033 4.6 .15  0 unknown .044 4.6 .18  0 timeout 900     240 11000    0 unknown 5.0 300 47 0 timeout 900    630 3800   0 disqualified .069 9.1 .32 0 timeout (verification) 900    80 14000   0 true 8.6 370 75 2 error (5) .024 5.7 .13  0 error (5) .027 5.6 .12  0
termination-restricted-15/java_Break_true-termination_true-no-overflow.c true .23  24 2.3  2 true 5.1 320 37 2 true .068 6.9 .71 2 true .070 6.4 .56 2 true 4.5 290 36 2 unknown .77 66 8.6 0 unknown .055 4.7 .15  0 unknown .029 4.6 .25  0 true .086 26 .86 2 true 4.4 290 41 2 true .37 59 4.1 2 disqualified .048 9.3 .40 0 true .11 15 1.2 2 true 9.1 380 80 2 error (5) .026 5.6 .11  0 error (5) .031 5.5 .11  0
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c true .21  24 2.3  2 true 9.1 510 71 2 true .12  6.8 .91 2 true .14  6.1 .69 2 true 27   820 290 2 unknown .78 65 8.5 0 unknown .027 4.6 .21  0 unknown .037 4.6 .14  0 true .091 26 1.0  2 true 28   880 340 2 true .37 59 3.2 2 disqualified .046 9.7 .41 0 true .11 15 1.5 2 true 9.7 400 78 2 error (5) .025 5.6 .16  0 error (5) .025 5.7 .096 0
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c true .42  53 4.4  2 true 20   2100 150 2 true .11  6.8 1.0  2 true .093 6.6 .78 2 true 13   490 110 2 unknown .80 66 8.4 0 unknown .030 4.7 .18  0 unknown .028 4.7 .20  0 true .085 26 .97 2 true 13   500 110 2 true .42 58 3.2 2 disqualified .047 9.0 .42 0 true .12 16 1.2 2 true 13   550 99 2 error (5) .029 5.7 .10  0 error (5) .054 5.6 .19  0
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c true .40  43 4.0  2 true 8.3 470 57 2 true .18  6.9 2.0  2 true .19  7.2 1.5  2 true 100   3600 1100 2 unknown .79 67 9.0 0 unknown .030 4.6 .19  0 unknown .033 4.8 .16  0 true .15  26 1.9  2 true 100   3300 1000 2 true .40 59 3.8 2 disqualified .064 9.5 .38 0 true .11 15 1.2 2 true 9.6 400 75 2 error (5) .019 5.6 .018 0 error (5) .035 5.7 .20  0
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c false(termination) .16  24 1.1  1 false(termination) 11   830 86 1 error (42) 880     1300   7300    0 out of memory 130     15000   1500    0 false(termination) 4.9 290 44 1 unknown .81 66 10   0 unknown .028 4.6 .18  0 unknown .054 4.5 .17  0 timeout 900     480 11000    0 false(termination) 5.3 300 46 1 out of memory 51    15000 660   0 disqualified .046 9.5 .39 0 timeout (verification) 900    110 11000   0 false(termination) 11   520 96 1 error (5) .027 5.6 .13  0 error (5) .028 5.7 .16  0
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c false(termination) .15  24 1.3  1 false(termination) 6.9 360 53 1 error (42) 880     1300   9900    0 out of memory 140     15000   1900    0 false(termination) 3.8 280 32 1 unknown .79 66 8.9 0 unknown .038 4.7 .22  0 unknown .029 4.7 .17  0 timeout 900     510 10000    0 false(termination) 3.7 280 33 1 timeout 900    9300 6900   0 disqualified .046 9.5 .42 0 timeout (verification) 900    18 12000   0 false(termination) 7.7 350 59 1 error (5) .026 5.6 .14  0 error (5) .030 5.7 .12  0
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c false(termination) .13  24 1.0  1 false(termination) 5.5 350 45 1 error (42) 880     1700   8500    0 out of memory 180     15000   2600    0 false(termination) 3.8 280 34 1 unknown .79 67 9.1 0 unknown .029 4.7 .15  0 unknown .059 4.6 .12  0 timeout 900     430 11000    0 false(termination) 3.7 280 34 1 timeout 900    340 5200   0 disqualified .046 9.8 .43 0 timeout (verification) 900    51 11000   0 false(termination) 9.1 380 71 1 error (5) .024 5.6 .13  0 error (5) .028 5.6 .22  0
termination-restricted-15/Ex02_false-termination_true-no-overflow.c false(termination) .17  24 1.2  1 false(termination) 7.1 350 50 1 error (42) 880     1600   9200    0 out of memory 180     15000   2300    0 false(termination) 3.6 280 37 1 unknown .82 66 9.4 0 unknown .033 4.6 .18  0 unknown .030 4.6 .20  0 timeout 900     420 11000    0 false(termination) 3.6 280 34 1 timeout 900    330 4400   0 disqualified .046 9.3 .38 0 timeout (verification) 900    51 11000   0 false(termination) 8.8 380 72 1 error (5) .024 5.6 .10  0 error (5) .025 5.6 .14  0
termination-restricted-15/Ex03_false-termination_true-no-overflow.c false(termination) .13  24 1.1  1 false(termination) 5.1 320 39 1 error (42) 880     1600   8100    0 out of memory 180     15000   2300    0 false(termination) 3.6 280 30 1 unknown .78 66 8.1 0 unknown .028 4.6 .22  0 unknown .046 4.6 .16  0 timeout 900     480 11000    0 false(termination) 3.6 280 38 1 timeout 900    320 6400   0 disqualified .056 9.5 .34 0 timeout (verification) 900    45 12000   0 false(termination) 8.5 350 78 1 error (5) .025 5.6 .14  0 error (5) .027 5.5 .22  0
termination-restricted-15/Ex05_false-termination_true-no-overflow.c false(termination) .13  24 .88 1 false(termination) 2.8 230 25 1 out of memory 150     15000   2400    0 out of memory 140     15000   2200    0 false(termination) 3.5 280 36 1 unknown .76 66 9.3 0 unknown .032 4.6 .19  0 unknown .027 4.6 .19  0 out of memory 350     15000 5900    0 false(termination) 3.5 280 35 1 out of memory 60    15000 870   0 disqualified .044 9.3 .49 0 false(termination) .14 15 1.6 1 false(termination) 8.0 370 61 1 error (5) .047 5.5 .15  0 error (5) .027 5.7 .13  0
termination-restricted-15/Ex06_false-termination_true-no-overflow.c false(termination) .13  24 1.2  1 false(termination) 8.6 370 59 1 error (42) 880     1200   10000    0 out of memory 110     15000   1600    0 false(termination) 5.0 290 50 1 unknown .80 66 8.1 0 unknown .046 4.7 .14  0 unknown .032 4.6 .32  0 timeout 900     530 12000    0 false(termination) 4.9 300 42 1 out of memory 250    15000 2000   0 disqualified .044 9.4 .39 0 timeout (verification) 900    170 9900   0 false(termination) 9.8 390 76 1 error (5) .030 5.7 .15  0 error (5) .024 5.6 .17  0
termination-restricted-15/Ex07_false-termination_true-no-overflow.c false(termination) .14  24 1.0  1 false(termination) 6.5 340 45 1 out of memory 290     15000   3600    0 out of memory 82     15000   970    0 false(termination) 4.7 290 46 1 unknown .76 65 8.9 0 unknown .030 4.7 .28  0 unknown .032 4.7 .25  0 timeout 900     8600 11000    0 false(termination) 4.8 300 46 1 out of memory 31    15000 430   0 disqualified .049 9.5 .51 0 timeout (verification) 900    15 14000   0 false(termination) 9.6 410 77 1 error (5) .032 5.6 .16  0 error (5) .025 5.6 .16  0
termination-restricted-15/Ex08_false-termination_true-no-overflow.c false(termination) .29  24 2.7  0 false(termination) 33   1700 200 0 error (42) 880     1200   9000    0 out of memory 110     15000   1400    0 false(termination) 250   3800 3200 1 unknown .82 66 8.2 0 unknown .032 4.6 .20  0 unknown .029 4.6 .14  0 timeout 900     590 13000    0 false(termination) 280   3900 3400 1 out of memory 46    15000 610   0 disqualified .043 9.4 .42 0 timeout (verification) 900    75 9900   0 false(termination) 28   820 260 1 error (5) .026 5.6 .12  0 error (5) .021 5.6 .11  0
termination-restricted-15/Flip2_false-termination_true-no-overflow.c false(termination) .24  24 1.8  1 false(termination) 21   870 130 1 error (42) 880     1500   11000    0 out of memory 140     15000   2000    0 unknown 4.2 280 41 0 unknown .84 65 9.2 0 unknown .034 4.7 .29  0 unknown .028 4.6 .20  0 timeout 900     610 10000    0 unknown 4.5 300 40 0 timeout 900    10000 6800   0 disqualified .047 9.4 .39 0 timeout (verification) 900    52 12000   0 false(termination) 13   530 120 1 error (5) .024 5.6 .14  0 error (5) .025 5.6 .14  0
termination-restricted-15/Flip_false-termination_true-no-overflow.c false(termination) .14  24 1.2  1 false(termination) 5.9 380 40 1 error (42) 880     4700   4100    0 error (42) 880     320   5800    0 false(termination) 3.9 280 36 1 unknown .82 66 8.7 0 unknown .029 4.7 .25  0 unknown .047 4.5 .14  0 timeout 900     1300 10000    0 false(termination) 3.7 280 37 1 out of memory 700    15000 10000   0 disqualified .067 9.5 .36 0 probably out of memory (killed (signal 9, verification)) 780    15000 11000   0 false(termination) 9.1 390 70 1 error (5) .022 5.7 .12  0 error (5) .026 5.6 .14  0
termination-restricted-15/GCD2_false-termination_true-no-overflow.c false(termination) .15  24 1.3  1 false(termination) 26   1300 170 1 error (42) 880     560   5500    0 error (42) 880     10000   11000    0 unknown 4.8 290 43 0 unknown 1.1  66 13   0 unknown .034 4.7 .18  0 unknown .048 4.5 .18  0 timeout 900     1200 10000    0 unknown 5.0 300 43 0 timeout 900    1600 13000   0 disqualified .047 9.2 .40 0 timeout (verification) 900    49 12000   0 false(termination) 8.1 360 69 1 error (5) .024 5.6 .18  0 error (5) .021 5.5 .11  0
termination-restricted-15/GCD_false-termination_true-no-overflow.c false(termination) .16  24 1.2  1 false(termination) 32   1300 200 1 error (42) 880     560   5500    0 out of memory 340     15000   4400    0 unknown 4.8 290 43 0 unknown 1.1  67 13   0 unknown .023 4.8 .24  0 unknown .077 4.7 .21  0 timeout 900     1800 9000    0 unknown 4.9 290 46 0 out of memory 640    15000 9000   0 disqualified .046 8.9 .36 0 timeout (verification) 900    92 12000   0 false(termination) 8.0 370 59 1 error (5) .029 5.6 .21  0 error (5) .023 5.6 .099 0
termination-restricted-15/Loop_false-termination_true-no-overflow.c false(termination) .13  24 1.0  1 false(termination) 4.4 290 31 1 out of memory 270     15000   3800    0 out of memory 210     15000   2800    0 false(termination) 3.7 280 30 1 unknown .79 68 8.3 0 unknown .049 4.6 .16  0 unknown .052 4.6 .17  0 out of memory 880     15000 11000    0 false(termination) 3.7 280 37 1 out of memory 810    15000 11000   0 disqualified .072 9.4 .41 0 timeout (verification) 900    14 12000   0 false(termination) 7.9 370 61 1 error (5) .025 5.6 .17  0 error (5) .051 5.6 .15  0
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c false(termination) .14  24 1.1  1 false(termination) 9.2 440 61 1 error (42) 880     1700   9700    0 error (42) 880     170   12000    0 false(termination) 3.8 280 35 1 unknown .80 67 8.2 0 unknown .028 4.6 .16  0 unknown .029 4.6 .29  0 timeout 900     690 11000    0 false(termination) 3.7 280 39 1 out of memory 500    15000 7600   0 disqualified .048 9.1 .45 0 timeout (verification) 900    180 11000   0 false(termination) 13   560 110 1 error (5) .027 5.6 .15  0 error (5) .025 5.7 .13  0
termination-restricted-15/NO_00_false-termination_true-no-overflow.c false(termination) .13  24 1.2  1 false(termination) 3.0 240 27 1 out of memory 290     15000   4600    0 out of memory 230     15000   3000    0 false(termination) 3.8 280 33 1 unknown .82 66 8.2 0 unknown .047 4.7 .17  0 unknown .027 4.5 .24  0 out of memory 870     15000 11000    0 false(termination) 3.6 280 32 1 out of memory 810    15000 10000   0 disqualified .048 9.2 .44 0 timeout (verification) 900    15 13000   0 false(termination) 8.3 360 65 1 error (5) .032 5.5 .16  0 error (5) .022 5.6 .19  0
termination-restricted-15/NO_01_false-termination_true-no-overflow.c false(termination) .15  24 1.2  1 false(termination) 3.6 260 30 1 out of memory 280     15000   3900    0 out of memory 220     15000   3000    0 false(termination) 3.9 280 42 1 unknown .80 67 8.8 0 unknown .034 4.6 .26  0 unknown .031 4.6 .16  0 out of memory 880     15000 11000    0 false(termination) 4.0 280 36 1 out of memory 820    15000 9800   0 disqualified .056 9.5 .33 0 timeout (verification) 900    15 15000   0 false(termination) 8.5 360 69 1 error (5) .029 5.7 .22  0 error (5) .024 5.6 .17  0
termination-restricted-15/NO_02_false-termination_true-no-overflow.c false(termination) .16  24 1.0  1 false(termination) 3.4 250 32 1 out of memory 300     15000   4200    0 out of memory 230     15000   3100    0 false(termination) 3.7 280 34 1 unknown .82 66 9.1 0 unknown .049 4.6 .19  0 unknown .030 4.6 .17  0 out of memory 880     15000 10000    0 false(termination) 3.6 280 34 1 out of memory 820    15000 11000   0 disqualified .047 9.2 .39 0 timeout (verification) 900    15 12000   0 false(termination) 7.8 370 68 1 error (5) .049 5.8 .092 0 error (5) .027 5.6 .13  0
termination-restricted-15/NO_03_false-termination_true-no-overflow.c false(termination) .14  24 1.1  1 false(termination) 4.1 270 35 1 out of memory 280     15000   4400    0 out of memory 220     15000   3100    0 false(termination) 4.8 290 44 1 unknown .82 67 9.5 0 unknown .056 4.6 .16  0 unknown .046 4.6 .21  0 timeout 900     9800 11000    0 false(termination) 4.9 290 46 1 out of memory 880    15000 11000   0 disqualified .070 9.5 .37 0 timeout (verification) 900    15 13000   0 false(termination) 8.0 350 62 1 error (5) .048 5.6 .11  0 error (5) .019 5.6 .18  0
termination-restricted-15/NO_04_false-termination_true-no-overflow.c false(termination) .30  30 2.8  1 false(termination) 8.3 490 57 1 out of memory 450     15000   5300    0 out of memory 370     15000   4200    0 false(termination) 4.0 280 33 1 unknown .80 67 8.3 0 unknown .048 4.5 .20  0 unknown .028 4.6 .23  0 out of memory 880     15000 10000    0 false(termination) 3.8 280 41 1 out of memory 850    15000 10000   0 disqualified .046 9.3 .44 0 timeout (verification) 900    15 13000   0 false(termination) 11   470 98 1 error (5) .029 5.6 .17  0 error (5) .028 5.7 .21  0
termination-restricted-15/NO_13_false-termination_true-no-overflow.c false(termination) .69  61 6.2  0 false(termination) 13   550 100 0 out of memory 330     15000   4200    0 out of memory 240     15000   4000    0 out of memory 770   15000 8500 0 unknown .83 67 9.2 0 unknown .029 4.6 .16  0 unknown .028 4.6 .44  0 timeout 900     10000 13000    0 out of memory 570   15000 6700 0 out of memory 820    15000 13000   0 disqualified .042 9.4 .49 0 probably out of memory (killed (signal 9, verification)) 290    15000 4200   0 false(termination) 47   810 520 0 error (5) .025 5.6 .12  0 error (5) .049 5.6 .10  0
termination-restricted-15/NO_21_false-termination_true-no-overflow.c false(termination) .13  24 1.0  1 false(termination) 3.0 240 28 1 out of memory 290     15000   4100    0 out of memory 210     15000   3300    0 false(termination) 3.5 280 35 1 unknown .82 67 9.0 0 unknown .055 4.8 .21  0 unknown .025 4.6 .21  0 timeout 900     14000 10000    0 false(termination) 3.7 280 38 1 timeout 900    13000 12000   0 disqualified .043 9.1 .44 0 timeout (verification) 900    16 12000   0 false(termination) 7.5 340 58 1 error (5) .022 5.6 .16  0 error (5) .026 5.6 .13  0
termination-restricted-15/NO_22_false-termination_true-no-overflow.c false(termination) .33  34 3.7  0 false(termination) 11   460 79 0 out of memory 310     15000   4200    0 out of memory 240     15000   3100    0 out of memory 770   15000 7700 0 unknown .77 66 8.1 0 unknown .027 4.6 .16  0 unknown .031 4.6 .17  0 timeout 900     9800 11000    0 out of memory 590   15000 6300 0 out of memory 660    15000 8400   0 disqualified .044 9.6 .47 0 timeout (verification) 900    15 13000   0 false(termination) 45   990 470 0 error (5) .032 5.6 .21  0 error (5) .021 5.6 .20  0
termination-restricted-15/NO_23_false-termination_true-no-overflow.c false(termination) .14  23 1.0  1 false(termination) 3.6 250 26 1 out of memory 240     15000   3200    0 out of memory 190     15000   2600    0 false(termination) 6.3 320 60 1 unknown .78 66 8.4 0 unknown .029 4.6 .20  0 unknown .031 4.6 .32  0 timeout 900     5600 11000    0 false(termination) 5.8 310 50 1 out of memory 690    15000 9500   0 disqualified .047 9.3 .42 0 timeout (verification) 900    15 11000   0 false(termination) 12   560 96 1 error (5) .025 5.6 .16  0 error (5) .024 5.6 .17  0
termination-restricted-15/NO_24_false-termination_true-no-overflow.c false(termination) .14  24 1.4  0 false(termination) 8.6 450 60 0 out of memory 370     15000   5600    0 out of memory 270     15000   3600    0 unknown 7.3 530 62 0 unknown .77 66 7.9 0 unknown .050 4.6 .24  0 unknown .029 4.6 .19  0 timeout 900     15000 11000    0 unknown 7.9 550 70 0 timeout 900    14000 11000   0 disqualified .043 9.4 .44 0 probably out of memory (killed (signal 9, verification)) 170    15000 2600   0 unknown 13   580 100 0 error (5) .022 5.6 .10  0 error (5) .035 5.6 .24  0
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c false(termination) 45     370 360    0 timeout 900   15000 4900 0 error (42) 880     1300   8700    0 out of memory 240     15000   3000    0 timeout 900   3800 8800 0 unknown .79 66 8.5 0 unknown .029 4.6 .16  0 unknown .027 4.7 .21  0 timeout 900     550 11000    0 timeout 900   510 11000 0 out of memory 230    15000 3200   0 disqualified .046 9.1 .39 0 probably out of memory (killed (signal 9, verification)) 170    15000 2100   0 false(termination) 84   1000 960 1 error (5) .024 5.6 .15  0 error (5) .025 5.6 .13  0
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c false(termination) .58  36 5.7  1 timeout 900   7900 9300 0 error (42) 880     1700   10000    0 out of memory 130     15000   1600    0 timeout 900   1200 9400 0 unknown .78 65 8.2 0 unknown .035 4.6 .28  0 unknown .031 4.6 .27  0 timeout 900     770 8400    0 false(termination) 630   1200 6700 1 out of memory 86    15000 930   0 disqualified .044 9.4 .43 0 timeout (verification) 900    97 9700   0 false(termination) 30   820 260 1 error (5) .024 5.6 .12  0 error (5) .023 5.7 .13  0
termination-restricted-15/Sunset_false-termination_true-no-overflow.c false(termination) .14  24 1.6  1 false(termination) 21   1400 130 0 error (42) 880     1200   8600    0 error (42) 870     140   11000    0 false(termination) 7.5 390 66 1 unknown .79 66 9.1 0 unknown .042 4.7 .21  0 unknown .049 4.7 .20  0 timeout 900     470 9800    0 false(termination) 6.7 320 64 1 out of memory 610    15000 8500   0 disqualified .052 9.5 .45 0 timeout (verification) 900    67 13000   0 false(termination) 15   650 160 1 error (5) .023 5.6 .17  0 error (5) .028 5.6 .14  0
termination-restricted-15/Swingers_false-termination_true-no-overflow.c false(termination) .14  24 1.1  1 false(termination) 5.0 310 40 0 out of memory 300     15000   4000    0 out of memory 220     15000   3000    0 unknown 7.7 540 68 0 unknown .80 66 9.3 0 unknown .027 4.6 .24  0 unknown .030 4.5 .22  0 timeout 900     7500 9500    0 unknown 7.7 540 65 0 timeout 900    12000 13000   0 disqualified .046 9.5 .39 0 probably out of memory (killed (signal 9, verification)) 170    15000 2300   0 unknown 26   540 290 0 error (5) .023 5.6 .11  0 error (5) .023 5.6 .16  0
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c false(termination) .13  24 1.1  1 false(termination) 9.1 490 62 1 error (42) 880     1300   9300    0 out of memory 120     15000   1500    0 false(termination) 3.6 280 37 1 unknown .81 66 10   0 unknown .042 4.6 .21  0 unknown .042 4.6 .18  0 timeout 900     480 9500    0 false(termination) 3.7 280 36 1 out of memory 190    15000 1600   0 disqualified .048 9.3 .37 0 timeout (verification) 900    100 9100   0 false(termination) 8.7 370 67 1 error (5) .026 5.6 .17  0 error (5) .024 5.6 .13  0
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c false(termination) .37  27 3.5  0 timeout 910   11000 4800 0 error (42) 880     1300   10000    0 out of memory 120     15000   1400    0 false(termination) 310   3900 3900 1 unknown .81 67 9.4 0 unknown .029 4.7 .23  0 unknown .038 4.6 .14  0 timeout 900     1100 9400    0 false(termination) 390   4000 5200 1 out of memory 66    15000 790   0 disqualified .050 9.7 .43 0 timeout (verification) 900    75 9500   0 false(termination) 33   920 300 1 error (5) .021 5.5 .21  0 error (5) .022 5.6 .13  0
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c false(termination) .33  24 3.9  0 false(termination) 590   9600 3400 0 error (42) 880     1200   9900    0 out of memory 120     15000   1600    0 false(termination) 300   3900 3800 1 unknown .84 67 9.7 0 unknown .033 4.5 .22  0 unknown .031 4.7 .19  0 timeout 900     1100 11000    0 unknown 7.3 370 64 0 out of memory 180    15000 1400   0 disqualified .044 9.1 .51 0 timeout (verification) 900    120 8500   0 false(termination) 33   950 310 0 error (5) .025 5.6 .066 0 error (5) .029 5.7 .14  0
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c false(termination) .13  24 1.1  1 false(termination) 4.1 270 35 1 error (42) 880     1600   7600    0 out of memory 180     15000   2400    0 false(termination) 3.7 280 34 1 unknown .84 66 8.6 0 unknown .036 4.6 .18  0 unknown .046 4.6 .22  0 timeout 900     430 12000    0 false(termination) 3.5 280 35 1 timeout 900    3300 4000   0 disqualified .048 9.3 .41 0 probably out of memory (killed (signal 9, verification)) 290    15000 3900   0 false(termination) 9.3 380 73 1 error (5) .025 5.7 .15  0 error (5) .024 5.6 .099 0
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c false(termination) .13  24 .93 1 false(termination) 6.4 360 50 1 error (42) 880     1700   8700    0 out of memory 180     15000   2300    0 false(termination) 3.7 270 31 1 unknown .77 66 9.3 0 unknown .031 4.5 .20  0 unknown .035 4.7 .24  0 timeout 900     420 11000    0 false(termination) 3.6 280 36 1 timeout 900    300 3700   0 disqualified .050 9.2 .41 0 timeout (verification) 900    48 12000   0 false(termination) 8.4 360 71 1 error (5) .025 5.6 .16  0 error (5) .022 5.6 .18  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 249 40000 170000 440000 275 249 16000 340000 140000 397 249 180000 930000 1300000 60 249 110000 2100000 1000000 48 249 24000 290000 290000 320 249 5000 280000 64000 0 249 8.8 1200 50 0 249 8.7 1200 50 0 249 190000 620000 2300000 60 249 25000 290000 310000 290 249 160000 1200000 1100000 52 249 12 2300 110 0 249 150000    250000 1700000   154 249 13000 170000 130000 401 249 7.3 1400 35 0 249 7.2 1400 35 0
    correct results 158 51 5400 490 275 216 2800 180000 21000 397 30 20 540 240 60 24 12 280 130 48 180 2800 83000 31000 320 0 0 0 30 210 3800 2800 60 163 2800 80000 30000 290 26 19 2300 210 52 0 79 710    1900 7300   154 224 3100 100000 29000 401 0 0
        correct true 117 36 4100 340 234 181 2400 160000 19000 362 30 20 540 240 60 24 12 280 130 48 140 1800 61000 19000 280 0 0 0 30 210 3800 2800 60 127 1300 61000 14000 254 26 19 2300 210 52 0 75 710    1900 7300   150 177 2500 81000 23000 354 0 0
        correct false 41 15 1200 160 41 35 370 20000 2500 35 0 0 40 1000 22000 12000 40 0 0 0 0 36 1400 19000 17000 36 0 0 4 .56 62 6.4 4 47 580 21000 5200 47 0 0
    correct-unconfimed results 7 47 560 380 0 10 730 17000 4400 0 0 0 0 0 0 0 0 0 0 0 0 4 140 3200 1400 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 7 47 560 380 0 10 730 17000 4400 0 0 0 0 0 0 0 0 0 0 0 0 4 140 3200 1400 0 0 0
    incorrect results 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (249 tasks, max score: 443) 275 397 60 48 320 0 0 0 60 290 52 0 154 401 0 0
Run set 2ls.sv-comp19_prop-termination.Termination-MainControlFlow aprove.sv-comp19_prop-termination.Termination-MainControlFlow cbmc.sv-comp19_prop-termination.Termination-MainControlFlow cbmc-path.sv-comp19_prop-termination.Termination-MainControlFlow cpa-seq.sv-comp19_prop-termination.Termination-MainControlFlow depthk.sv-comp19_prop-termination.Termination-MainControlFlow divine-explicit.sv-comp19_prop-termination.Termination-MainControlFlow divine-smt.sv-comp19_prop-termination.Termination-MainControlFlow esbmc-kind.sv-comp19_prop-termination.Termination-MainControlFlow pesco.sv-comp19_prop-termination.Termination-MainControlFlow pinaka.sv-comp19_prop-termination.Termination-MainControlFlow smack.sv-comp19_prop-termination.Termination-MainControlFlow symbiotic.sv-comp19_prop-termination.Termination-MainControlFlow uautomizer.sv-comp19_prop-termination.Termination-MainControlFlow ukojak.sv-comp19_prop-termination.Termination-MainControlFlow utaipan.sv-comp19_prop-termination.Termination-MainControlFlow