Tool 2LS 0.6.0 AProVE CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-01 11:41:06 CET 2017-11-30 11:20:26 CET 2017-12-01 13:00:07 CET 2017-12-01 08:46:20 CET 2017-12-01 09:26:34 CET 2017-12-01 12:27:04 CET 2017-12-01 15:15:10 CET 2017-12-02 08:45:19 CET 2017-12-02 20:38:57 CET 2017-12-03 05:53:57 CET 2017-12-03 12:12:33 CET 2017-12-03 12:06:01 CET 2017-12-03 09:20:08 CET
Run set 2ls.sv-comp18.Termination-MainControlFlow aprove.sv-comp18.Termination-MainControlFlow cbmc.sv-comp18.Termination-MainControlFlow cpa-bam-bnb.sv-comp18.Termination-MainControlFlow cpa-bam-slicing.sv-comp18.Termination-MainControlFlow cpa-seq.sv-comp18.Termination-MainControlFlow depthk.sv-comp18.Termination-MainControlFlow esbmc-incr.sv-comp18.Termination-MainControlFlow esbmc-kind.sv-comp18.Termination-MainControlFlow symbiotic.sv-comp18.Termination-MainControlFlow uautomizer.sv-comp18.Termination-MainControlFlow ukojak.sv-comp18.Termination-MainControlFlow utaipan.sv-comp18.Termination-MainControlFlow
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction --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
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety.c 6.9  220 75    1 6.0 350 50 0 880    5000 3700   0 .47 44 4.4 0 .45 40 4.2 0 910   4600 12000 0 1.2 56 13 0 900     970 13000    0 900     970 11000    0 .057 6.6 .34 0 4.5 250 36 1 .024 4.9 .15  0 .048 5.1 .17  0
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c 7.0  220 75    1 7.1 380 52 1 870    4700 3000   0 .49 42 4.7 0 .42 40 3.6 0 900   4500 12000 0 1.2 56 12 0 900     970 12000    0 900     970 15000    0 .040 6.5 .38 0 4.4 270 36 1 .023 4.9 .18  0 .046 4.9 .20  0
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c .26 44 1.3  1 6.0 450 45 0 880    8400 3900   0 .44 41 4.3 0 .44 41 4.4 0 2.8 270 26 1 1.2 56 15 0 900     150 12000    0 900     140 11000    0 .039 6.5 .40 0 4.4 250 34 1 .047 4.9 .12  0 .050 4.9 .15  0
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c .23 44 .98 0 25   1300 180 0 650    15000 6400   0 .48 40 4.3 0 .42 40 3.7 0 2.6 270 21 0 690   15000 10000 0 340     15000 4200    0 350     15000 4100    0 .042 6.5 .39 0 5.5 290 47 1 .025 4.9 .17  0 .047 5.0 .12  0
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c .55 58 5.0  0 11   540 65 0 880    7600 3000   0 .51 42 4.4 0 .45 40 3.7 0 5.6 420 43 0 1.2 56 13 0 .031 15 .30 0 .060 15 .20 0 .067 6.5 .31 0 59   540 670 0 .023 4.9 .24  0 .047 5.0 .14  0
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c .23 45 1.6  1 6.9 390 52 1 880    8400 3900   0 .48 41 4.4 0 .45 40 3.6 0 3.0 270 26 1 1.2 56 12 0 900     840 12000    0 900     860 11000    0 .067 6.5 .31 0 4.4 250 37 1 .046 5.0 .13  0 .046 4.9 .14  0
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c .24 44 1.4  1 5.1 330 39 0 210    15000 2600   0 .46 40 4.2 0 .44 40 4.4 0 2.7 270 23 1 1.2 55 13 0 900     11000 9800    0 900     11000 9300    0 .067 6.5 .35 0 4.7 300 42 1 .048 5.0 .12  0 .044 5.0 .16  0
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c .23 43 1.2  0 11   670 79 0 870    330 4100   0 .45 42 3.7 0 .43 40 4.2 0 2.7 290 27 0 720   15000 8100 0 290     15000 3100    0 290     15000 3500    0 .069 6.5 .34 0 7.6 360 61 0 .046 4.8 .15  0 .048 4.9 .14  0
termination-crafted/Mysore_false-termination_true-valid-memsafety.c 900    3100 9500    0 900   3500 10000 0 870    6600 5200   0 .46 40 4.4 0 .45 40 4.2 0 8.5 560 67 0 1.2 56 13 0 900     210 12000    0 900     210 11000    0 .058 6.5 .37 0 38   720 410 0 .031 5.1 .14  0 .048 4.9 .12  0
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c .17 44 1.2  0 15   820 100 0 870    650 3600   0 .48 40 4.1 0 .43 40 4.1 0 2.5 260 20 0 660   15000 8800 0 330     15000 4200    0 330     15000 4100    0 .041 6.5 .37 0 5.5 300 43 1 .048 4.9 .16  0 .023 4.9 .20  0
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c .24 44 .98 0 8.1 440 65 0 870    750 5600   0 .47 41 4.3 0 .44 41 4.5 0 2.8 290 24 0 730   15000 8400 0 330     15000 3600    0 320     15000 4000    0 .061 6.6 .39 0 17   500 170 1 .025 4.9 .15  0 .047 5.0 .093 0
termination-crafted/NonTermination3_false-termination_false-valid-deref.c .27 50 1.5  1 8.6 540 62 0 870    2700 5800   0 .47 40 4.3 0 .46 40 4.2 0 720   4400 10000 0 1.2 57 14 0 900     1600 11000    0 900     1600 14000    0 .064 6.5 .29 0 4.7 280 37 1 .050 5.1 .14  0 .023 4.9 .17  0
termination-crafted/NonTermination3_true-no-overflow_false-termination.c .30 49 1.6  1 9.8 570 73 0 870    2700 5200   0 .49 42 5.0 0 .46 40 4.1 0 710   4400 9800 0 1.2 57 13 0 900     1600 11000    0 900     1600 12000    0 .062 6.5 .31 0 4.6 270 37 1 .047 5.0 .16  0 .050 5.0 .13  0
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c .24 44 1.1  1 5.6 410 44 0 880    8500 3100   0 .45 41 4.2 0 .43 40 4.1 0 2.8 270 25 1 1.2 57 12 0 900     690 12000    0 900     690 10000    0 .062 6.5 .36 0 4.3 240 35 1 .046 4.9 .15  0 .038 4.9 .14  0
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c .22 44 1.1  0 8.5 590 63 1 270    15000 2400   0 .46 41 4.0 0 .43 40 4.5 0 2.6 270 22 0 1.2 57 13 0 900     1800 8600    0 900     1800 8600    0 .042 6.5 .30 0 4.6 270 40 1 .027 5.1 .16  0 .046 4.9 .13  0
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c .22 45 1.2  1 6.2 370 48 1 310    15000 4300   0 .46 41 4.3 0 .45 40 4.9 0 2.9 270 30 1 1.2 57 13 0 900     3700 13000    0 900     3700 9500    0 .067 6.5 .36 0 4.3 260 41 1 .021 4.9 .17  0 .047 5.0 .18  0
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c .22 43 1.3  0 1.9 230 17 0 210    15000 2900   0 .46 40 4.3 0 .43 37 4.1 0 2.7 280 24 1 1.2 57 13 0 290     15000 4000    0 290     15000 4100    0 .065 6.6 .31 0 4.4 250 36 0 .025 4.9 .17  0 .025 4.9 .14  0
termination-crafted/2Nested_true-termination_true-valid-memsafety.c 900    1700 11000    0 7.1 470 51 2 870    6700 4100   0 .48 41 4.4 0 .43 40 4.9 0 50   490 520 2 1.2 57 14 0 900     370 10000    0 900     360 11000    0 .040 6.6 .32 0 5.6 300 48 2 .025 4.9 .17  0 .047 5.0 .16  0
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c 1.2  100 8.8  2 3.8 340 29 2 2.4  34 20   2 .48 40 4.0 0 .43 40 3.7 0 900   4300 12000 0 1.2 56 14 0 .079 27 .94 2 .081 27 .87 2 .040 6.6 .34 0 39   900 400 2 .049 5.0 .16  0 .021 4.9 .19  0
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c 900    300 10000    0 18   1300 130 2 870    1100 5800   0 .47 41 4.3 0 .44 40 3.9 0 900   4500 11000 0 1.2 55 15 0 900     300 12000    0 900     300 11000    0 .050 6.6 .26 0 18   350 220 2 .048 4.9 .14  0 .044 5.0 .14  0
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c .20 44 1.5  0 30   2700 240 2 870    410 3100   0 .48 41 4.0 0 .45 40 4.0 0 2.6 260 20 0 710   15000 9500 0 430     15000 6500    0 430     15000 6000    0 .059 6.5 .40 0 910   13000 7300 0 .047 4.9 .15  0 .049 4.9 .13  0
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c 1.3  340 14    2 9.2 570 61 2 870    7200 3700   0 .50 40 4.3 0 .43 40 4.2 0 370   15000 3800 0 1.2 57 12 0 900     1100 11000    0 900     1100 12000    0 .069 6.5 .39 0 900   2100 10000 0 .023 4.9 .17  0 .024 4.9 .17  0
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c 1.8  360 18    2 10   770 76 2 870    7600 3000   0 .48 40 4.3 0 .43 40 4.8 0 340   15000 3800 0 1.2 56 14 0 900     670 10000    0 900     660 10000    0 .057 6.5 .33 0 900   2400 12000 0 .021 4.9 .17  0 .041 5.0 .12  0
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c .26 45 1.2  2 6.1 470 46 2 870    7700 3000   0 .47 40 4.4 0 .44 40 4.2 0 3.3 270 30 2 1.2 57 13 0 900     95 11000    0 900     95 12000    0 .066 6.5 .38 0 5.2 320 47 2 .024 5.0 .15  0 .047 4.9 .13  0
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c 900    1900 11000    0 3.3 280 28 2 .44 33 3.9 2 .47 40 4.4 0 .46 40 4.2 0 3.2 280 26 0 1.2 58 15 0 .12  26 1.2  2 .11  26 1.3  2 .038 6.6 .49 0 6.7 360 49 2 .048 4.9 .16  0 .047 4.9 .18  0
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c 900    3800 7900    0 13   850 86 2 870    3800 2600   0 .48 43 4.3 0 .44 40 3.8 0 900   800 11000 0 1.2 56 13 0 900     280 10000    0 900     280 12000    0 .041 6.5 .32 0 17   310 230 2 .048 4.9 .16  0 .036 4.9 .11  0
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c 900    4000 9100    0 6.4 440 45 2 870    3800 3700   0 .47 40 4.4 0 .44 40 4.3 0 7.1 440 56 2 1.2 57 13 0 900     1300 12000    0 900     1300 9500    0 .040 6.6 .33 0 16   310 190 2 .047 4.9 .14  0 .047 4.9 .17  0
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c 900    2100 9700    0 5.7 440 41 2 870    8100 5500   0 .49 41 4.5 0 .46 41 3.8 0 4.0 300 33 2 1.2 56 16 0 900     830 11000    0 900     830 9700    0 .057 6.6 .39 0 6.4 340 55 2 .021 4.8 .16  0 .047 5.1 .18  0
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c 900    2100 9300    0 4.4 360 33 2 880    8100 3600   0 .48 41 4.1 0 .42 38 3.9 0 3.5 280 28 2 1.2 56 12 0 900     800 11000    0 900     810 10000    0 .042 6.5 .36 0 6.0 330 51 2 .025 4.9 .14  0 .048 5.0 .19  0
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c 900    3100 8800    0 9.3 670 65 2 870    5200 3500   0 .47 40 4.7 0 .46 40 4.6 0 900   1200 9400 0 1.2 57 13 0 900     770 10000    0 900     770 10000    0 .066 6.6 .31 0 77   1500 800 0 .040 5.0 .20  0 .047 4.9 .16  0
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c .64 62 5.2  2 2.1 220 18 2 880    5700 4200   0 .48 40 4.3 0 .45 40 3.9 0 3.7 280 35 2 1.2 57 13 0 900     810 12000    0 900     820 11000    0 .042 6.6 .37 0 5.4 300 50 2 .026 5.0 .14  0 .049 4.9 .17  0
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c 900    640 7600    0 29   2200 190 2 870    5800 2900   0 .49 43 4.4 0 .43 40 4.1 0 5.7 420 44 2 1.2 57 14 0 900     290 12000    0 900     290 10000    0 .056 6.5 .39 0 22   520 190 2 .047 4.9 .16  0 .024 4.9 .17  0
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c 900    660 9100    0 900   3600 12000 0 880    6100 4700   0 .47 40 4.3 0 .45 40 3.9 0 5.2 330 46 2 1.2 56 16 0 900     260 11000    0 900     260 11000    0 .038 6.5 .50 0 45   1000 400 0 .041 4.9 .20  0 .048 4.8 .15  0
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c 54    15000 620    0 36   2300 270 2 870    13000 6400   0 .49 40 4.5 0 .40 40 3.8 0 900   4400 11000 0 1.2 57 12 0 900     2100 11000    0 900     2100 11000    0 .038 6.6 .50 0 900   2400 9600 0 .023 4.9 .17  0 .047 4.9 .15  0
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c .37 46 2.4  0 900   14000 8400 0 870    13000 8200   0 .47 40 4.5 0 .45 40 4.6 0 900   4500 11000 0 1.2 56 15 0 900     5100 11000    0 900     5100 12000    0 .069 6.6 .31 0 900   1100 9600 0 .023 4.9 .18  0 .048 4.9 .12  0
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c 900    3000 9600    0 5.1 340 37 2 870    3100 7000   0 .48 40 4.2 0 .47 40 4.6 0 5.1 360 41 0 1.2 56 13 0 900     1100 9600    0 900     1100 11000    0 .066 6.6 .36 0 22   510 230 2 .038 5.0 .18  0 .022 5.0 .23  0
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c .31 49 2.0  2 2.6 250 18 2 870    3000 5500   0 .48 43 4.0 0 .43 40 4.2 0 900   640 9800 0 1.2 57 16 0 900     310 11000    0 900     310 12000    0 .058 6.6 .43 0 12   540 110 2 .034 5.0 .13  0 .038 4.8 .16  0
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c .22 44 1.2  0 730   15000 6300 0 870    280 2900   0 .47 40 4.7 0 .45 40 4.0 0 2.9 290 23 0 750   15000 9200 0 900     15000 7400    0 900     15000 7900    0 .058 6.5 .44 0 49   630 510 2 .024 4.9 .11  0 .047 4.9 .16  0
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c 900    2900 10000    0 23   920 190 0 870    5200 4800   0 .51 43 4.9 0 .43 40 4.2 0 5.7 390 49 2 1.2 56 16 0 900     1000 9700    0 900     1000 11000    0 .066 6.6 .34 0 6.3 330 54 2 .051 4.9 .12  0 .049 4.9 .14  0
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c .24 44 1.0  0 9.5 730 74 2 870    320 2900   0 .46 40 3.9 0 .42 40 4.4 0 2.8 290 23 0 710   15000 8600 0 290     15000 4300    0 290     15000 3700    0 .073 6.6 .26 0 900   13000 5700 0 .023 4.8 .20  0 .037 4.9 .20  0
termination-crafted/Mysore_true-termination_true-valid-memsafety.c 900    3000 11000    0 7.7 490 58 2 870    460 10000   0 .50 41 4.3 0 .42 40 3.8 0 5.9 430 45 2 1.2 56 14 0 900     160 10000    0 900     160 12000    0 .070 6.6 .34 0 18   340 210 2 .038 5.0 .20  0 .044 4.9 .15  0
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c .23 43 1.0  0 13   720 84 0 870    650 3000   0 .47 41 4.3 0 .47 40 4.7 0 2.8 290 23 0 680   15000 9300 0 700     15000 6800    0 710     15000 6700    0 .054 6.6 .35 0 38   670 390 2 .047 4.9 .17  0 .049 4.9 .14  0
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c .21 43 1.2  0 5.6 410 41 2 870    440 3500   0 .50 42 4.9 0 .44 40 3.7 0 2.8 290 24 0 630   15000 7700 0 900     9100 8300    0 900     9100 9200    0 .066 6.5 .26 0 7.4 460 72 2 .047 4.9 .12  0 .048 4.9 .14  0
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c .24 43 1.2  0 8.1 670 60 2 870    660 3000   0 .49 41 4.2 0 .43 40 4.2 0 2.9 290 26 0 690   15000 8200 0 370     15000 4400    0 370     15000 4500    0 .059 6.5 .40 0 11   610 97 2 .047 5.0 .15  0 .048 4.9 .15  0
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c .19 43 1.3  0 8.4 650 58 2 820    15000 6600   0 .47 42 4.1 0 .46 40 4.3 0 2.8 290 20 0 730   15000 8900 0 310     15000 3700    0 320     15000 3900    0 .041 6.5 .41 0 910   13000 8700 0 .049 5.1 .16  0 .041 4.9 .15  0
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c .33 54 2.7  2 2.8 270 22 2 870    3300 7400   0 .46 43 5.0 0 .43 40 3.9 0 4.4 290 38 2 1.2 57 14 0 900     260 9800    0 900     260 11000    0 .066 6.5 .35 0 7.3 350 57 2 .045 4.9 .14  0 .024 4.9 .15  0
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c .25 49 1.7  2 3.0 260 22 2 870    3500 7100   0 .48 40 4.6 0 .45 40 3.9 0 4.5 280 37 2 1.2 56 14 0 900     260 10000    0 900     260 11000    0 .066 6.6 .33 0 5.7 300 44 2 .022 4.9 .14  0 .030 5.0 .16  0
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c 900    250 11000    0 46   2200 260 2 870    670 6200   0 .51 44 4.4 0 .45 40 3.7 0 4.9 320 39 2 1.2 56 16 0 900     270 11000    0 900     260 11000    0 .066 6.5 .38 0 15   490 150 2 .023 4.9 .15  0 .040 4.9 .18  0
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c 900    4800 9500    0 9.8 630 74 2 870    200 9600   0 .47 40 3.8 0 .44 40 4.8 0 5.0 310 46 2 1.2 57 13 0 900     510 11000    0 900     510 11000    0 .062 6.5 .33 0 7.1 370 57 2 .040 5.0 .16  0 .043 5.1 .11  0
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c 900    4000 11000    0 910   10000 4900 0 870    580 7300   0 .48 41 4.6 0 .49 41 4.1 0 6.9 460 54 2 1.2 56 14 0 900     490 8900    0 900     490 10000    0 .048 6.5 .33 0 910   9700 7700 0 .024 4.9 .18  0 .026 4.9 .18  0
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c .22 43 1.0  0 9.6 730 82 2 870    12000 11000   0 .49 41 4.8 0 .51 39 4.2 0 2.5 270 23 0 710   15000 10000 0 350     15000 4100    0 350     15000 3900    0 .045 6.5 .37 0 15   370 140 2 .048 4.9 .15  0 .021 5.0 .20  0
termination-crafted/Singapore_true-termination_true-valid-memsafety.c 900    3000 11000    0 640   15000 3000 0 6.6  39 75   2 .46 43 4.8 0 .43 38 3.6 0 11   990 100 2 1.2 57 14 0 4.8   31 58    2 4.8   31 59    2 .064 6.5 .30 0 16   380 190 2 .046 4.9 .14  0 .048 5.0 .13  0
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c .35 50 2.4  2 6.3 460 45 2 880    7800 4000   0 .45 41 4.0 0 .42 40 3.9 0 4.3 300 38 2 1.2 57 13 0 900     210 12000    0 900     210 13000    0 .042 6.5 .45 0 18   400 170 2 .045 4.9 .16  0 .024 4.8 .12  0
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c .48 51 3.1  2 4.3 310 32 2 870    6500 4500   0 .49 40 4.5 0 .42 40 4.7 0 4.8 320 40 2 1.2 56 13 0 900     580 9800    0 900     580 10000    0 .055 6.5 .35 0 6.8 360 61 2 .023 5.0 .17  0 .039 4.9 .21  0
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c .49 49 2.4  2 4.8 330 36 2 870    6000 3300   0 .49 41 4.1 0 .45 40 4.2 0 4.3 310 34 2 1.2 56 11 0 900     590 11000    0 900     590 9900    0 .038 6.5 .39 0 7.2 350 57 2 .050 4.8 .13  0 .022 4.9 .15  0
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c .47 49 2.3  2 3.8 300 30 2 870    6300 3400   0 .46 40 4.9 0 .48 41 4.2 0 3.8 280 32 2 1.2 56 14 0 900     590 12000    0 900     590 10000    0 .042 6.5 .37 0 6.8 360 57 2 .050 4.9 .15  0 .047 5.0 .13  0
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c 900    190 10000    0 910   14000 4900 0 870    1100 7900   0 .47 40 4.6 0 .43 39 4.0 0 5.3 340 44 2 1.2 56 17 0 900     320 9900    0 900     320 10000    0 .039 6.6 .35 0 23   520 250 2 .048 5.0 .12  0 .024 4.9 .15  0
termination-crafted/Thun_true-termination_true-valid-memsafety.c 900    2700 9300    0 6.1 420 49 2 2.0  33 21   2 .46 40 4.7 0 .44 40 3.7 0 5.1 310 43 2 1.2 57 15 0 1.0   26 11    2 1.0   26 12    2 .066 6.5 .39 0 6.3 310 62 2 .024 5.1 .079 0 .021 5.0 .13  0
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c 900    2900 11000    0 8.0 520 66 2 870    5900 3400   0 .45 40 4.3 0 .48 40 4.2 0 5.6 350 43 2 1.2 56 13 0 900     340 10000    0 900     340 10000    0 .067 6.6 .33 0 25   470 240 2 .046 5.0 .17  0 .048 5.0 .16  0
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c 900    2900 8700    0 7.8 510 54 2 870    6000 4200   0 .47 41 4.8 0 .44 42 4.4 0 7.7 490 61 2 1.2 55 14 0 900     340 13000    0 900     330 12000    0 .038 6.5 .46 0 32   520 400 2 .025 5.0 .16  0 .048 5.0 .14  0
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c .29 47 1.8  2 3.9 320 27 2 880    8200 3000   0 .48 40 4.8 0 .44 41 4.2 0 3.2 280 29 2 1.2 56 14 0 900     600 11000    0 900     600 9900    0 .067 6.5 .34 0 5.1 290 40 2 .024 4.9 .16  0 .039 4.9 .16  0
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c 40    15000 350    0 1.9 200 18 2 .42 33 3.9 2 .49 43 4.5 0 .48 40 4.1 0 2.5 270 23 2 1.3 56 13 0 .074 26 .75 2 .083 26 .70 2 .067 6.5 .41 0 3.9 230 31 2 .047 5.1 .14  0 .049 4.9 .090 0
termination-crafted/aaron2_true-termination_true-valid-memsafety.c .45 51 3.7  2 52   2600 350 2 870    600 7700   0 .47 40 4.3 0 .45 40 3.9 0 4.0 300 35 2 1.2 57 13 0 900     140 14000    0 900     140 10000    0 .067 6.5 .35 0 5.7 300 46 2 .049 4.9 .13  0 .048 5.1 .13  0
termination-crafted/aaron3_true-termination_true-valid-memsafety.c 900    280 10000    0 910   8300 4900 0 870    260 10000   0 .48 40 4.4 0 .43 40 4.4 0 21   640 200 2 1.3 56 17 0 900     280 12000    0 900     280 11000    0 .065 6.5 .31 0 20   430 220 2 .047 4.9 .14  0 .023 4.9 .13  0
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c .27 48 1.9  2 3.1 260 24 2 3.2  43 35   2 .50 43 4.7 0 .46 41 4.6 0 67   2200 720 2 1.2 56 16 0 .22  26 2.4  2 .20  26 2.3  2 .069 6.6 .36 0 5.2 310 47 2 .044 4.9 .15  0 .049 5.0 .16  0
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c .42 59 3.3  2 2.1 220 20 2 870    4700 3100   0 .47 40 3.8 0 .43 40 4.6 0 3.9 280 34 2 1.2 56 15 0 900     820 11000    0 900     810 12000    0 .041 6.7 .35 0 5.6 320 51 2 .047 5.0 .16  0 .040 4.9 .13  0
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c .25 47 1.2  1 5.9 450 43 0 870    3100 6000   0 .49 45 3.9 0 .46 41 4.4 0 3.0 270 28 1 1.2 56 13 0 900     240 11000    0 900     240 10000    0 .040 6.5 .32 0 4.5 250 36 1 .046 5.0 .18  0 .049 4.9 .15  0
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c .25 44 1.3  1 5.7 430 44 0 870    8100 3500   0 .46 40 4.3 0 .45 40 4.0 0 2.9 270 25 1 1.2 56 12 0 900     990 10000    0 900     990 13000    0 .066 6.5 .38 0 4.8 280 38 1 .053 5.0 .15  0 .042 4.9 .22  0
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c .22 46 1.5  1 120   5600 680 1 870    2100 5900   0 .49 41 4.3 0 .48 40 4.1 0 3.4 280 30 1 99   64 1400 0 900     1500 10000    0 900     1500 9800    0 .041 6.5 .34 0 4.5 260 35 1 .046 4.9 .13  0 .050 4.9 .17  0
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c .23 44 1.4  1 6.3 500 45 0 870    3400 6700   0 .49 41 3.9 0 .47 40 4.6 0 2.8 270 27 1 1.2 56 12 0 900     380 11000    0 900     380 10000    0 .040 6.5 .33 0 4.3 240 34 1 .047 4.9 .16  0 .024 4.9 .17  0
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c .27 44 1.3  1 10   630 58 0 870    2400 6800   0 .50 43 4.2 0 .44 40 4.8 0 2.9 270 26 1 1.2 55 15 0 900     640 11000    0 900     640 11000    0 .066 6.7 .39 0 7.7 370 61 1 .048 5.0 .17  0 .048 5.0 .14  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 900    2900 4500    0 3.7 290 27 2 870    1400 4600   0 .48 40 4.8 0 .45 41 4.0 0 43   640 490 2 1.7 56 20 0 900     800 11000    0 900     800 10000    0 .060 6.6 .30 0 23   540 260 2 .025 5.0 .15  0 .024 4.9 .16  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c .42 54 2.6  2 2.7 250 23 2 870    3200 5700   0 .48 42 4.2 0 .41 40 4.0 0 4.9 290 35 2 1.2 57 16 0 900     470 12000    0 900     470 9700    0 .043 6.5 .36 0 6.4 320 53 2 .021 4.9 .21  0 .048 4.9 .16  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c .31 48 1.4  2 8.3 540 57 2 3.3  47 32   2 .47 40 4.1 0 .46 41 3.8 0 67   2200 730 2 1.2 56 13 0 .23  26 2.2  2 .21  26 2.4  2 .067 6.5 .36 0 4.9 300 47 2 .047 4.9 .15  0 .024 4.9 .13  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c .39 59 3.2  2 6.8 490 54 2 870    4700 3800   0 .44 41 4.6 0 .47 41 4.6 0 3.8 280 34 2 1.2 57 16 0 900     820 11000    0 900     820 12000    0 .042 6.5 .33 0 5.3 310 43 2 .047 4.9 .13  0 .048 4.9 .15  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c 900    5500 4200    0 23   1100 160 2 870    640 4900   0 .46 41 4.8 0 .43 40 4.6 0 7.3 460 57 2 1.4 57 14 0 900     1400 9900    0 900     1300 8300    0 .067 6.5 .35 0 20   440 210 2 .040 4.8 .20  0 .024 5.0 .17  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 900    1800 5600    0 4.7 330 36 2 870    1100 3200   0 .51 42 4.5 0 .43 40 4.6 0 7.3 350 60 2 8.1 240 97 0 900     1800 11000    0 900     1800 11000    0 .057 6.6 .34 0 21   560 270 2 .024 4.9 .14  0 .038 5.0 .15  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c .30 53 2.2  2 2.7 250 24 2 870    3000 7800   0 .48 41 4.4 0 .44 39 4.4 0 4.0 280 36 2 1.2 56 13 0 900     1300 10000    0 900     1300 9300    0 .042 6.5 .33 0 5.4 310 44 2 .034 4.9 .11  0 .023 4.9 .12  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c .49 62 4.6  2 8.2 600 57 2 1.2  33 12   2 .51 41 4.9 0 .44 40 3.8 0 4.1 290 34 2 1.2 56 14 0 .088 26 1.1  2 .095 26 .95 2 .067 6.5 .28 0 5.4 310 42 2 .023 4.9 .18  0 .027 5.0 .18  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c .47 54 3.2  2 5.1 430 38 2 870    3200 5900   0 .47 41 4.3 0 .45 40 4.1 0 7.9 470 66 0 1.2 56 12 0 900     470 9800    0 900     480 13000    0 .066 6.5 .25 0 7.1 330 57 2 .047 4.9 .15  0 .043 4.9 .16  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c .42 53 3.0  2 3.0 270 26 2 870    3300 8900   0 .49 43 4.5 0 .43 40 4.1 0 5.5 320 46 2 1.2 56 15 0 900     450 11000    0 900     450 12000    0 .070 6.6 .35 0 7.3 360 60 2 .050 4.9 .15  0 .023 5.0 .17  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c .33 47 2.6  2 5.4 440 41 2 870    3200 7200   0 .46 41 4.9 0 .44 40 3.9 0 3.3 280 28 0 1.2 56 15 0 900     280 11000    0 900     270 9900    0 .055 6.5 .40 0 7.2 370 61 2 .047 5.0 .17  0 .025 4.9 .16  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c .30 55 2.1  2 2.9 270 22 2 870    2400 7100   0 .47 41 4.5 0 .44 40 4.3 0 7.4 400 63 2 1.3 56 14 0 900     1400 12000    0 900     1400 9900    0 .062 6.6 .34 0 9.4 550 75 2 .023 4.9 .18  0 .048 4.9 .12  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c .54 73 4.5  2 2.6 250 21 2 870    670 3500   0 .48 43 4.4 0 .45 41 4.5 0 5.1 300 43 2 1.4 57 16 0 900     320 11000    0 900     320 13000    0 .069 6.5 .33 0 6.6 340 48 2 .024 4.8 .12  0 .030 4.9 .18  0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c .44 52 2.8  2 5.8 440 36 2 870    3300 6200   0 .45 41 5.1 0 .45 40 4.2 0 4.5 300 37 2 1.2 56 15 0 900     320 12000    0 900     320 10000    0 .039 6.6 .50 0 7.1 340 52 2 .047 4.9 .15  0 .048 4.9 .17  0
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c .68 64 5.2  2 2.9 270 25 2 870    6200 5200   0 .49 42 4.3 0 .47 40 4.6 0 5.1 310 45 2 1.2 56 12 0 900     450 9600    0 900     450 12000    0 .050 6.5 .32 0 6.1 310 52 2 .048 5.0 .14  0 .021 4.9 .19  0
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 900    260 10000    0 6.5 460 47 2 870    3100 7000   0 .44 41 4.4 0 .44 41 4.1 0 3.3 280 32 0 1.2 56 15 0 900     240 10000    0 900     240 10000    0 .065 6.6 .33 0 10   550 94 2 .026 5.0 .16  0 .046 4.9 .13  0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c .46 59 3.1  2 2.7 260 24 2 870    660 2800   0 .53 44 4.1 0 .50 40 4.0 0 32   1100 280 2 1.4 56 16 0 900     1400 9200    0 900     1500 12000    0 .066 6.5 .33 0 9.2 430 85 2 .023 5.0 .17  0 .031 4.9 .18  0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 900    2300 4700    0 44   1900 310 2 870    670 3600   0 .49 41 4.3 0 .42 40 3.7 0 18   470 200 2 1.4 56 18 0 900     440 13000    0 900     440 11000    0 .040 6.5 .32 0 12   530 110 2 .025 4.9 .17  0 .024 4.9 .19  0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 900    2300 9900    0 3.6 290 25 2 870    6100 3200   0 .45 40 4.6 0 .42 40 4.5 0 3.8 290 37 2 1.2 56 12 0 900     600 10000    0 900     600 11000    0 .072 6.5 .32 0 9.4 300 99 2 .049 4.9 .15  0 .021 5.0 .12  0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c .29 48 1.8  2 6.8 490 47 2 3.2  45 33   2 .50 41 5.1 0 .45 40 4.9 0 67   2200 710 2 1.2 55 14 0 .23  26 2.1  2 .21  26 2.5  2 .061 6.6 .38 0 5.0 300 39 2 .048 4.9 .16  0 .047 5.0 .14  0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c .42 57 2.5  2 6.1 480 48 2 870    4900 4100   0 .49 41 4.4 0 .45 40 4.0 0 4.1 300 38 2 1.2 56 15 0 900     820 11000    0 900     820 11000    0 .042 6.5 .39 0 5.3 310 43 2 .043 4.9 .15  0 .023 5.0 .17  0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 900    3600 11000    0 2.7 260 20 2 870    2800 5800   0 .47 40 3.9 0 .45 40 3.6 0 4.4 290 41 2 1.3 57 13 0 900     1300 10000    0 900     1300 8300    0 .041 6.5 .43 0 5.4 310 44 2 .025 5.0 .16  0 .045 5.0 .14  0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c .49 64 4.2  2 8.0 510 55 2 1.2  33 12   2 .46 41 4.2 0 .47 40 3.7 0 4.0 280 34 2 1.2 55 13 0 .093 26 1.0  2 .099 26 1.0  2 .040 6.5 .42 0 5.4 310 44 2 .047 4.9 .15  0 .022 4.9 .15  0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c .31 51 1.8  2 2.5 260 19 2 870    5300 3700   0 .49 41 4.2 0 .48 40 4.4 0 3.7 280 32 2 1.2 56 15 0 900     250 12000    0 900     250 11000    0 .051 6.6 .48 0 5.2 310 43 2 .024 4.9 .15  0 .048 4.8 .12  0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c .29 51 1.9  2 2.1 230 19 2 870    6000 3200   0 .45 40 4.3 0 .43 40 4.2 0 4.0 280 35 2 1.2 56 16 0 900     340 12000    0 900     340 11000    0 .041 6.6 .37 0 17   300 220 2 .047 4.9 .12  0 .030 4.9 .17  0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c .42 55 3.1  2 3.0 270 26 2 870    2300 5900   0 .50 42 4.8 0 .47 40 4.2 0 4.7 310 46 2 1.2 57 13 0 900     560 12000    0 900     560 11000    0 .038 6.5 .43 0 7.2 340 57 2 .037 4.9 .13  0 .025 4.9 .17  0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c .62 59 5.5  2 3.2 270 27 2 870    1900 4900   0 .48 41 4.2 0 .45 40 4.0 0 6.2 360 55 2 1.2 56 12 0 900     610 9600    0 900     620 11000    0 .069 6.6 .31 0 8.0 470 69 2 .050 5.0 .11  0 .025 4.9 .15  0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c .79 61 6.9  2 4.0 290 31 2 870    1900 6400   0 .48 40 4.2 0 .43 40 4.7 0 5.6 310 51 2 1.2 56 14 0 900     750 10000    0 900     750 12000    0 .039 6.5 .52 0 8.4 540 69 2 .023 4.9 .18  0 .048 5.0 .14  0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 900    320 8800    0 4.7 400 34 2 870    3200 7200   0 .44 40 3.5 0 .54 40 5.2 0 4.4 280 35 2 1.2 56 13 0 900     270 11000    0 900     270 11000    0 .067 6.6 .33 0 7.4 350 69 2 .046 4.8 .14  0 .023 4.8 .15  0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 900    2100 11000    0 4.3 350 29 2 870    3300 6400   0 .50 41 4.5 0 .47 40 4.1 0 3.8 300 35 2 1.2 57 13 0 900     290 12000    0 900     290 10000    0 .039 6.5 .45 0 6.8 350 52 2 .040 5.0 .16  0 .026 4.9 .14  0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 900    220 10000    0 12   590 80 2 870    3400 5600   0 .49 40 4.0 0 .43 40 3.9 0 3.1 270 28 0 1.2 56 13 0 900     370 12000    0 900     370 9800    0 .065 6.6 .34 0 7.1 330 59 2 .047 4.9 .17  0 .049 4.9 .14  0
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 900    2700 11000    0 2.8 260 20 2 2.7  33 29   2 .48 41 4.5 0 .45 40 4.6 0 470   15000 5800 0 1.2 57 15 0 .21  26 2.2  2 .23  26 2.2  2 .060 6.6 .39 0 7.7 390 57 2 .022 5.0 .20  0 .024 4.9 .16  0
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 900    1600 7000    0 81   3600 580 2 870    2700 7600   0 .47 40 4.3 0 .44 40 4.2 0 8.4 480 69 2 1.3 57 16 0 900     510 9400    0 900     510 9900    0 .037 6.6 .44 0 40   680 430 2 .023 4.9 .14  0 .048 4.9 .14  0
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c .27 48 1.9  2 13   740 72 2 870    1800 6100   0 .48 41 4.2 0 .44 40 3.7 0 3.5 270 34 2 1.2 57 13 0 900     970 9600    0 900     970 12000    0 .066 6.6 .32 0 5.3 310 41 2 .050 4.9 .12  0 .050 4.8 .12  0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 900    2700 10000    0 3.0 280 24 2 870    5400 3300   0 .49 43 4.6 0 .44 40 3.4 0 3.9 290 28 2 1.2 56 14 0 900     880 9600    0 900     880 11000    0 .045 6.5 .42 0 9.6 290 97 2 .038 5.0 .22  0 .026 5.0 .16  0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c .26 47 2.1  2 2.0 270 16 2 860    8500 4300   0 .50 43 4.6 0 .45 40 4.2 0 3.9 280 30 2 1.2 57 14 0 900     470 11000    0 900     470 9200    0 .055 6.5 .25 0 5.0 290 40 2 .026 4.9 .15  0 .023 4.9 .14  0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 900    2100 11000    0 5.0 350 36 2 870    6200 3700   0 .46 40 4.6 0 .47 40 4.1 0 4.3 340 40 0 1.2 56 14 0 900     950 9700    0 900     950 13000    0 .069 6.6 .34 0 16   840 140 0 .046 5.1 .17  0 .046 5.0 .13  0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c .36 53 2.6  2 2.2 240 21 2 870    5900 3400   0 .50 41 4.0 0 .41 40 4.3 0 3.4 270 31 2 1.2 57 14 0 900     210 11000    0 900     190 11000    0 .071 6.5 .24 0 5.1 300 43 2 .023 4.9 .20  0 .047 5.0 .11  0
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c .26 45 1.3  2 2.8 270 22 2 870    1900 8900   0 .47 41 3.9 0 .42 40 4.5 0 4.0 290 33 2 1.2 56 10 0 900     280 11000    0 900     270 10000    0 .041 6.6 .33 0 5.1 310 48 2 .041 4.8 .16  0 .025 4.9 .19  0
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 900    2300 9000    0 900   3500 12000 0 880    3100 5300   0 .49 41 4.5 0 .43 40 3.9 0 900   5200 13000 0 1.2 56 13 0 900     440 9800    0 900     440 11000    0 .057 6.5 .32 0 7.9 410 63 2 .039 5.0 .17  0 .039 4.9 .19  0
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 900    250 11000    0 14   650 88 2 870    990 3300   0 .45 40 3.9 0 .44 40 4.3 0 900   6300 7900 0 1.5 58 16 0 900     920 9900    0 900     920 13000    0 .068 6.6 .32 0 57   670 690 2 .039 5.0 .21  0 .024 5.0 .14  0
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c .18 43 1.2  0 16   1100 110 2 870    13000 10000   0 .48 40 3.9 0 .44 40 3.9 0 2.6 270 22 0 770   15000 8800 0 400     15000 4600    0 400     15000 4200    0 .039 6.6 .35 0 48   580 560 2 .037 5.0 .20  0 .042 4.8 .17  0
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c .22 43 1.2  0 8.7 590 62 2 870    13000 9500   0 .50 40 4.9 0 .45 40 4.0 0 2.5 270 23 0 620   15000 7400 0 340     15000 4000    0 350     15000 3800    0 .041 6.5 .33 0 49   1700 470 0 .048 4.9 .14  0 .034 4.9 .11  0
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c .24 46 1.7  2 2.6 260 22 2 870    3300 6200   0 .48 40 4.2 0 .44 40 4.1 0 3.5 280 31 2 1.2 58 15 0 900     360 11000    0 900     360 10000    0 .038 6.6 .46 0 5.3 300 42 2 .024 5.0 .18  0 .023 5.0 .18  0
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c .32 51 1.6  2 3.3 280 27 2 870    2800 7000   0 .43 40 4.1 0 .42 40 4.4 0 4.2 290 37 2 1.2 56 15 0 900     470 9500    0 900     470 9800    0 .043 6.5 .31 0 6.1 300 51 2 .024 5.0 .15  0 .022 5.0 .19  0
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c .29 50 1.6  2 3.8 310 30 2 2.5  38 25   2 .48 41 4.5 0 .45 40 4.7 0 4.3 300 38 0 1.2 57 12 0 .18  26 2.0  2 .14  26 1.9  2 .042 6.7 .42 0 5.1 310 43 2 .046 5.0 .17  0 .048 4.9 .15  0
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c 900    6400 5100    0 14   710 83 2 880    630 3500   0 .47 41 4.4 0 .44 41 4.6 0 4.6 320 39 2 1.4 56 14 0 900     1300 8300    0 900     1300 9400    0 .041 6.5 .40 0 20   460 210 2 .047 5.0 .16  0 .026 4.9 .16  0
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c .29 47 1.6  2 2.2 220 17 2 880    7900 3900   0 .49 41 4.2 0 .47 40 4.4 0 3.3 280 29 2 1.2 56 13 0 900     590 10000    0 900     590 9100    0 .039 6.6 .41 0 4.9 290 36 2 .022 4.9 .15  0 .049 4.8 .15  0
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c .37 58 3.0  2 2.5 250 20 2 870    660 3300   0 .49 40 3.9 0 .46 40 4.6 0 4.3 280 39 2 1.4 56 18 0 900     1400 8600    0 900     1500 10000    0 .066 6.5 .33 0 6.7 330 57 2 .034 4.9 .11  0 .048 4.9 .16  0
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c .48 60 3.3  2 2.9 270 22 2 870    2200 6400   0 .48 41 4.1 0 .51 40 4.8 0 4.9 310 42 2 1.2 56 15 0 900     550 12000    0 900     550 11000    0 .041 6.6 .40 0 7.1 370 60 2 .041 4.9 .17  0 .025 4.9 .11  0
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 1.9  200 18    2 2.6 260 23 2 870    4900 8500   0 .43 40 3.5 0 .46 40 4.3 0 470   15000 5300 0 1.2 55 13 0 900     6500 9600    0 900     6300 11000    0 .041 6.5 .36 0 900   2600 12000 0 .022 4.9 .13  0 .038 4.9 .22  0
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c .47 62 3.2  2 2.7 260 21 2 870    1100 3800   0 .47 41 4.0 0 .46 40 3.8 0 10   470 85 2 1.2 56 14 0 900     1200 11000    0 900     1200 11000    0 .040 6.5 .48 0 8.1 460 62 2 .049 4.9 .14  0 .048 5.0 .15  0
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 900    670 6600    0 120   4300 660 2 870    2400 5900   0 .45 40 4.1 0 .45 40 3.7 0 5.6 330 47 2 1.2 56 14 0 900     710 10000    0 900     710 11000    0 .056 6.5 .35 0 9.7 530 79 2 .050 4.9 .13  0 .023 4.8 .19  0
termination-crafted-lit/aviad_true-termination_true-no-overflow.c .51 67 3.9  2 34   2700 200 2 5.1  160 55   2 .46 40 4.2 0 .44 40 3.6 0 21   880 160 0 1.2 56 13 0 4.6   30 54    2 4.7   30 58    2 .041 6.6 .42 0 6.2 330 48 2 .048 4.9 .11  0 .048 5.0 .15  0
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c .34 46 2.6  0 14   820 110 2 870    8500 3800   0 .47 40 4.0 0 .46 42 4.1 0 900   3000 13000 0 1.4 56 17 0 900     3300 11000    0 900     3300 12000    0 .041 6.6 .32 0 8.9 540 73 2 .024 4.8 .13  0 .046 5.0 .17  0
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c .37 46 2.1  0 90   5300 530 2 870    1200 3600   0 .46 40 4.6 0 .47 40 3.9 0 900   3700 13000 0 2.0 56 23 0 900     1300 9800    0 900     1300 11000    0 .038 6.6 .36 0 110   750 1500 2 .024 4.9 .17  0 .046 4.9 .17  0
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c .36 46 2.0  0 8.4 480 57 2 880    7700 5000   0 .47 41 4.1 0 .44 40 4.0 0 28   1400 260 0 1.4 56 16 0 900     2400 12000    0 900     2400 12000    0 .061 6.5 .32 0 7.5 460 61 2 .048 5.1 .15  0 .047 4.9 .16  0
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c .41 46 2.0  0 50   4600 350 2 870    1200 3600   0 .50 43 4.6 0 .45 40 4.4 0 900   3700 11000 0 2.0 57 23 0 900     1700 9500    0 900     1700 9000    0 .061 6.6 .37 0 19   720 160 2 .023 4.9 .16  0 .024 5.0 .17  0
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c .39 46 2.0  0 52   3900 320 2 870    1200 3700   0 .45 40 4.3 0 .47 41 4.3 0 900   3500 12000 0 2.0 57 24 0 900     1600 7900    0 900     1600 9900    0 .057 6.5 .35 0 18   710 150 2 .024 4.9 .12  0 .046 5.0 .13  0
termination-crafted-lit/genady_true-termination_true-no-overflow.c .36 53 2.4  2 2.2 230 18 2 7.7  79 82   2 .48 40 4.2 0 .43 40 4.6 0 480   15000 5500 0 1.2 56 13 0 210     2900 3000    2 210     2900 2300    2 .039 6.6 .37 0 5.1 300 44 2 .023 4.9 .19  0 .024 4.9 .17  0
termination-crafted-lit/strchr_true-no-overflow_true-termination.c .38 46 2.4  0 8.2 650 66 2 720    8500 4300   0 .49 40 4.5 0 .45 40 4.9 0 27   940 190 0 1.4 56 15 0 900     1200 12000    0 900     1200 9800    0 .057 6.5 .43 0 8.7 530 64 2 .047 5.0 .14  0 .048 4.9 .16  0
termination-numeric/Ackermann01_true-termination_true-no-overflow.c .18 44 1.4  0 27   2000 240 2 870    440 5900   0 .48 41 4.3 0 .44 38 3.9 0 2.6 270 24 0 730   15000 9000 0 420     15000 5200    0 420     15000 5000    0 .040 6.5 .34 0 910   13000 5600 0 .048 4.9 .13  0 .050 4.9 .13  0
termination-numeric/Binomial_true-termination_false-no-overflow.c .21 44 1.3  0 10   720 81 0 870    1000 5000   0 .49 40 4.2 0 .45 40 4.6 0 2.7 270 22 0 14   340 170 0 900     6100 11000    0 900     6000 12000    0 .066 6.5 .33 0 900   2800 11000 0 .024 5.0 .14  0 .050 4.9 .13  0
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c .23 44 1.2  0 10   720 67 2 870    8700 5200   0 .52 44 4.6 0 .44 40 3.5 0 2.8 260 23 0 1.3 56 15 0 900     2300 8800    0 900     2300 9800    0 .055 6.6 .35 0 7.7 430 70 2 .023 5.0 .13  0 .020 4.9 .19  0
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c .18 44 1.6  0 15   1100 120 2 870    270 2500   0 .51 42 4.1 0 .43 40 4.2 0 2.5 260 23 0 610   15000 8000 0 340     15000 3800    0 340     15000 3600    0 .056 6.5 .35 0 900   13000 9800 0 .048 4.9 .13  0 .023 4.9 .17  0
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c .23 44 1.0  0 8.9 600 58 2 590    15000 3200   0 .44 40 4.4 0 .44 40 4.3 0 2.5 260 24 0 1.2 55 12 0 900     890 9700    0 900     890 9600    0 .038 6.5 .39 0 5.4 310 42 2 .045 4.9 .14  0 .047 5.0 .14  0
termination-numeric/LogRecursive_true-termination_true-no-overflow.c .17 44 1.3  0 900   5500 13000 0 4.3  86 52   2 .49 40 4.4 0 .44 38 3.6 0 2.5 260 24 0 1.2 56 13 0 43     140 500    2 43     130 570    2 .039 6.6 .43 0 71   670 740 0 .028 4.9 .15  0 .047 4.9 .15  0
termination-numeric/Parts_true-termination_true-no-overflow.c .20 44 1.1  0 900   13000 7800 0 870    590 4100   0 .46 43 4.4 0 .48 40 3.9 0 2.7 270 21 0 670   15000 9200 0 900     9600 10000    0 900     9400 13000    0 .062 6.6 .37 0 900   8400 9600 0 .022 4.9 .14  0 .048 5.0 .14  0
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c .18 43 1.1  0 7.2 500 61 2 410    15000 2600   0 .48 41 4.3 0 .47 40 4.0 0 2.8 290 25 0 1.3 57 16 0 900     1200 11000    0 900     1200 12000    0 .057 6.6 .34 0 5.6 310 48 2 .049 5.0 .099 0 .023 5.0 .14  0
termination-numeric/TwoWay_true-termination_true-no-overflow.c .20 43 1.4  0 11   800 71 2 870    11000 4500   0 .50 45 4.4 0 .43 40 4.2 0 2.6 270 22 0 1.2 57 16 0 900     990 9800    0 900     990 9800    0 .039 6.5 .44 0 19   380 230 2 .046 5.0 .18  0 .025 5.0 .18  0
termination-numeric/gcd01_true-termination_true-no-overflow.c .21 44 1.1  0 12   730 93 2 710    15000 10000   0 .44 40 4.4 0 .45 40 3.9 0 2.6 270 22 0 570   15000 6300 0 390     15000 4600    0 400     15000 4100    0 .067 6.6 .39 0 9.7 440 90 2 .022 4.9 .19  0 .048 4.9 .16  0
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c .33 56 2.6  2 5.4 380 43 2 2.6  38 30   2 .46 40 4.6 0 .44 40 4.8 0 19   870 160 0 1.2 55 14 0 .15  26 1.7  2 .17  26 1.6  2 .042 6.7 .40 0 5.8 320 45 2 .039 5.0 .17  0 .023 5.0 .23  0
termination-numeric/recHanoi02_true-termination_true-no-overflow.c .21 43 .97 0 7.3 460 53 2 2.4  35 23   2 .50 40 4.3 0 .44 40 4.4 0 2.5 260 23 0 1.2 56 17 0 .16  26 1.7  2 .19  26 1.7  2 .058 6.6 .38 0 6.9 370 60 2 .021 5.0 .19  0 .042 4.9 .27  0
termination-numeric/rec_counter1_true-termination_true-no-overflow.c .21 43 1.1  0 15   1000 100 2 870    660 3800   0 .44 40 3.7 0 .45 40 4.3 0 2.5 260 20 0 1.5 57 16 0 900     1900 10000    0 900     2000 8300    0 .056 6.6 .39 0 8.4 430 73 2 .041 5.0 .18  0 .025 4.9 .17  0
termination-numeric/rec_counter3_true-termination_true-no-overflow.c .24 44 1.2  0 12   970 87 2 870    660 3400   0 .48 40 4.3 0 .44 40 4.0 0 2.5 270 24 0 1.5 56 15 0 900     1600 7500    0 900     1700 8400    0 .056 6.5 .35 0 8.5 430 73 2 .053 4.9 .12  0 .022 4.9 .17  0
termination-numeric/twisted_true-termination_true-no-overflow.c 900    53 10000    0 69   5200 460 2 870    1300 5100   0 .49 43 4.7 0 .42 40 3.6 0 900   4300 11000 0 900   3800 8800 0 900     1900 9400    0 900     2400 13000    0 .039 6.5 .31 0 6.6 340 61 2 .025 5.0 .13  0 .022 4.8 .13  0
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c 900    2400 5700    0 4.8 410 34 2 870    2100 4100   0 .50 40 4.5 0 .47 40 4.0 0 5.4 310 41 2 1.8 57 25 0 900     1300 11000    0 900     1300 10000    0 .066 6.5 .31 0 7.7 450 65 2 .025 5.1 .20  0 .047 5.0 .12  0
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c .28 55 2.3  2 2.1 230 19 2 870    5300 2900   0 .47 41 4.3 0 .42 40 4.6 0 3.9 290 34 0 1.2 56 13 0 900     140 10000    0 900     130 11000    0 .038 6.6 .48 0 5.4 300 49 2 .023 4.9 .19  0 .021 4.9 .21  0
termination-restricted-15/GCD3_true-termination_true-no-overflow.c .74 59 6.4  2 18   850 110 2 870    1300 3700   0 .50 42 4.9 0 .47 41 4.0 0 4.0 290 37 0 1.7 56 16 0 900     970 9300    0 900     970 11000    0 .066 6.6 .34 0 35   510 400 2 .025 4.9 .17  0 .050 5.1 .15  0
termination-restricted-15/GCD4_true-termination_true-no-overflow.c .73 60 7.3  2 3.4 280 23 2 870    690 3900   0 .51 41 4.6 0 .46 40 4.5 0 3.8 290 33 0 1.4 56 16 0 900     1000 9800    0 900     1000 8900    0 .067 6.7 .34 0 34   540 370 2 .024 4.8 .17  0 .047 4.9 .16  0
termination-restricted-15/IntPath_true-termination_true-no-overflow.c 900    3500 11000    0 3.3 280 29 2 .41 33 3.6 2 .46 43 4.8 0 .43 40 4.2 0 2.7 270 25 2 1.2 57 13 0 .081 26 .67 2 .075 26 .76 2 .054 6.5 .34 0 4.6 290 37 2 .023 4.9 .19  0 .048 4.9 .15  0
termination-restricted-15/LogAG_true-termination_true-no-overflow.c 270    15000 1700    0 2.9 270 22 2 870    960 3800   0 .50 44 4.6 0 .41 40 4.1 0 4.9 300 43 2 1.5 56 19 0 900     890 8700    0 900     890 13000    0 .041 6.5 .29 0 7.1 370 59 2 .048 5.0 .17  0 .024 5.0 .19  0
termination-restricted-15/Log_true-termination_true-no-overflow.c .62 88 6.8  2 2.7 250 22 2 870    960 3900   0 .49 40 4.4 0 .44 40 4.1 0 5.1 300 40 2 1.5 57 16 0 900     870 10000    0 900     870 10000    0 .066 6.6 .34 0 7.4 370 62 2 .024 5.0 .13  0 .024 4.9 .17  0
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c .34 51 1.9  2 2.8 260 23 2 870    2900 6000   0 .50 41 4.4 0 .47 40 4.2 0 900   3500 11000 0 1.2 57 14 0 900     310 11000    0 900     310 11000    0 .059 6.6 .38 0 11   560 76 2 .048 5.1 .15  0 .049 5.0 .13  0
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c .22 46 1.4  2 2.6 230 21 2 .41 33 3.3 2 .44 40 3.9 0 .44 40 4.0 0 4.0 280 32 2 1.2 56 13 0 .11  26 .75 2 .093 26 .92 2 .067 6.5 .33 0 6.4 300 58 2 .046 5.0 .12  0 .035 5.0 .11  0
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c 900    1700 7800    0 3.4 270 24 2 870    1000 3100   0 .46 40 4.6 0 .41 40 4.6 0 6.3 360 56 2 1.5 56 17 0 900     1100 12000    0 900     1100 11000    0 .040 6.6 .44 0 7.7 430 58 2 .041 4.9 .21  0 .036 4.9 .13  0
termination-restricted-15/Nested_true-termination_true-no-overflow.c .33 60 2.9  2 2.7 260 21 2 1.1  33 11   2 .51 43 4.4 0 .44 41 3.9 0 21   670 180 2 1.2 57 13 0 .11  26 .67 2 .10  26 .80 2 .067 6.6 .32 0 5.7 280 44 2 .047 4.9 .16  0 .041 4.9 .17  0
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c .25 53 1.6  2 8.5 550 55 2 870    3300 6200   0 .48 43 5.1 0 .46 42 4.1 0 4.0 280 34 2 1.2 57 16 0 900     290 8300    0 900     290 12000    0 .070 6.7 .25 0 7.3 350 58 2 .021 5.0 .14  0 .046 5.0 .14  0
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c .41 57 3.1  2 2.7 260 21 2 870    660 4900   0 .46 41 4.2 0 .45 40 4.2 0 4.5 310 40 2 1.3 57 16 0 900     1400 11000    0 900     1400 9500    0 .056 6.5 .40 0 6.8 340 56 2 .047 4.9 .13  0 .049 5.0 .10  0
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c .22 45 1.3  2 2.3 250 20 2 880    7400 3700   0 .47 41 4.1 0 .45 40 4.3 0 3.5 280 34 2 1.2 56 13 0 900     270 9800    0 900     270 12000    0 .066 6.5 .38 0 5.0 290 45 2 .049 4.9 .15  0 .024 4.9 .14  0
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c .33 51 1.8  2 2.1 230 18 2 870    5900 3800   0 .50 41 4.4 0 .45 40 4.1 0 4.0 290 34 2 1.2 56 13 0 900     370 11000    0 900     370 10000    0 .038 6.6 .43 0 5.3 300 38 2 .030 5.0 .12  0 .048 5.1 .16  0
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c .47 60 4.4  2 2.7 270 23 2 870    960 4500   0 .50 43 5.0 0 .46 41 4.4 0 5.0 310 47 2 1.5 56 15 0 900     780 11000    0 900     780 10000    0 .056 6.6 .42 0 5.7 290 45 2 .024 4.9 .13  0 .050 4.9 .12  0
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c .50 54 3.7  2 2.6 250 20 2 880    960 3100   0 .46 41 4.3 0 .44 40 3.7 0 5.1 320 43 2 1.5 57 18 0 900     1000 10000    0 900     970 12000    0 .067 6.6 .30 0 5.9 280 49 2 .021 4.9 .19  0 .024 5.0 .15  0
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c .29 56 2.5  2 2.6 250 21 2 870    660 3200   0 .47 42 4.2 0 .43 38 4.1 0 3.8 280 36 2 1.4 56 14 0 900     790 12000    0 900     790 12000    0 .056 6.6 .37 0 5.5 280 41 2 .048 4.9 .15  0 .036 5.0 .16  0
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c .40 54 3.2  2 2.6 250 21 2 870    660 3200   0 .48 40 4.3 0 .45 40 3.7 0 4.0 280 35 2 1.4 56 17 0 900     1100 11000    0 900     1100 10000    0 .056 6.5 .38 0 6.4 290 54 2 .048 5.0 .16  0 .049 5.0 .14  0
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c .24 47 1.9  2 2.2 220 17 2 880    7800 3900   0 .46 42 4.2 0 .42 40 3.9 0 3.4 270 32 2 1.2 56 14 0 900     310 11000    0 900     300 12000    0 .070 6.5 .32 0 5.1 290 44 2 .044 5.0 .14  0 .048 4.9 .12  0
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c .28 49 1.7  2 2.1 230 18 2 870    6200 4800   0 .46 40 3.9 0 .44 40 3.9 0 3.8 280 33 2 1.2 57 13 0 900     270 11000    0 900     270 10000    0 .042 6.5 .34 0 5.1 290 45 2 .022 4.9 .18  0 .023 5.0 .18  0
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c .39 58 2.8  2 2.1 230 18 2 .44 33 4.4 2 .45 40 3.9 0 .44 40 4.0 0 3.5 280 28 0 1.2 57 14 0 .11  26 .64 2 .079 26 .72 2 .066 6.5 .34 0 7.5 300 68 2 .021 4.9 .16  0 .022 4.9 .15  0
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c .27 47 1.3  2 2.5 250 20 2 870    6200 3400   0 .46 40 4.0 0 .42 40 4.9 0 3.5 280 30 2 1.2 56 14 0 900     490 12000    0 900     500 9800    0 .066 6.5 .32 0 4.8 300 44 2 .047 4.9 .14  0 .023 5.0 .16  0
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c .29 51 1.9  2 2.6 260 20 2 870    6300 3800   0 .51 41 3.9 0 .47 40 4.1 0 3.5 280 30 2 1.2 58 14 0 900     380 11000    0 900     380 11000    0 .069 6.5 .32 0 5.5 300 45 2 .035 4.9 .16  0 .046 5.0 .18  0
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c .34 50 1.7  2 2.9 260 20 2 870    3300 6600   0 .48 40 4.8 0 .45 40 4.1 0 4.2 290 35 2 1.2 55 15 0 900     280 12000    0 900     280 11000    0 .037 6.5 .36 0 8.0 360 73 2 .049 4.9 .12  0 .042 4.8 .16  0
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c .42 59 3.4  2 2.5 240 20 2 880    5600 4200   0 .48 42 4.6 0 .43 40 3.7 0 3.7 280 31 2 1.2 56 12 0 900     350 12000    0 900     350 11000    0 .066 6.5 .32 0 11   300 130 2 .023 4.9 .14  0 .045 5.1 .14  0
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c .69 65 6.2  2 3.0 270 19 2 870    1600 5800   0 .48 41 4.0 0 .49 40 4.2 0 4.6 320 38 2 1.2 55 13 0 900     580 12000    0 900     590 13000    0 .055 6.6 .35 0 6.9 380 54 2 .021 4.9 .21  0 .019 4.9 .14  0
termination-restricted-15/Sequence_true-termination_true-no-overflow.c .28 51 2.6  2 2.5 230 19 2 2.7  33 27   2 .46 40 4.3 0 .43 40 3.8 0 90   3100 940 2 1.2 57 14 0 .17  26 1.3  2 .17  26 1.5  2 .066 6.5 .27 0 5.4 290 44 2 .046 4.9 .15  0 .023 4.9 .16  0
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c .27 48 1.6  2 2.1 220 20 2 870    7600 2500   0 .49 41 4.7 0 .41 40 3.9 0 3.4 270 29 2 1.2 56 14 0 900     450 11000    0 900     450 12000    0 .066 6.6 .28 0 4.7 290 37 2 .050 4.9 .13  0 .024 4.9 .11  0
termination-restricted-15/a.01_true-termination_true-no-overflow.c .40 59 3.5  2 2.6 270 22 2 870    650 3000   0 .46 40 4.3 0 .41 40 4.0 0 4.5 280 40 2 1.4 57 14 0 900     1400 8600    0 900     1400 8200    0 .041 6.5 .46 0 6.4 330 62 2 .047 4.9 .15  0 .048 5.1 .16  0
termination-restricted-15/a.04_true-termination_true-no-overflow.c .21 45 1.1  2 2.2 230 20 2 870    7200 2900   0 .47 40 4.4 0 .47 40 4.3 0 3.5 280 29 2 1.2 56 12 0 900     260 10000    0 900     270 10000    0 .043 6.6 .34 0 4.9 300 40 2 .046 5.0 .15  0 .022 4.9 .18  0
termination-restricted-15/a.05_true-termination_true-no-overflow.c .25 47 1.3  2 2.2 230 17 2 870    8300 3500   0 .45 40 4.0 0 .45 40 4.3 0 3.8 300 36 2 1.2 56 14 0 900     290 9500    0 900     290 11000    0 .066 6.6 .28 0 4.8 300 37 2 .024 5.0 .17  0 .024 4.9 .11  0
termination-restricted-15/a.06_true-termination_true-no-overflow.c .26 47 1.4  2 2.9 270 23 2 870    6400 3200   0 .46 40 4.5 0 .43 40 3.9 0 4.3 300 38 2 1.3 57 15 0 900     330 9900    0 900     330 10000    0 .040 6.6 .40 0 6.7 370 53 2 .045 4.8 .15  0 .048 5.0 .16  0
termination-restricted-15/a.07_true-termination_true-no-overflow.c .27 49 2.2  2 2.5 280 23 2 870    5800 3100   0 .50 41 4.2 0 .46 40 4.0 0 3.8 290 37 2 1.2 56 13 0 900     360 10000    0 900     370 9700    0 .039 6.5 .50 0 5.1 300 43 2 .050 4.9 .14  0 .038 4.9 .17  0
termination-restricted-15/a.08_true-termination_true-no-overflow.c .27 49 1.5  2 2.1 230 18 2 880    5000 2900   0 .49 43 4.1 0 .46 40 4.6 0 4.0 290 30 2 1.2 56 14 0 900     290 10000    0 900     300 11000    0 .038 6.6 .35 0 5.3 300 42 2 .022 4.8 .18  0 .021 4.9 .17  0
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c .27 46 1.4  2 2.6 250 23 2 880    8000 2900   0 .49 40 4.0 0 .42 40 4.0 0 3.4 280 30 0 1.2 57 14 0 900     180 11000    0 900     180 10000    0 .039 6.5 .41 0 17   400 210 2 .048 4.9 .13  0 .023 4.9 .14  0
termination-restricted-15/a.10_true-termination.c .26 51 1.8  2 4.5 350 33 2 870    3300 7400   0 .49 42 4.6 0 .41 40 4.0 0 4.1 290 36 2 1.2 56 13 0 900     290 10000    0 900     290 11000    0 .067 6.6 .34 0 7.5 350 67 2 .052 5.1 .15  0 .026 4.9 .15  0
termination-restricted-15/b.01_true-termination_true-no-overflow.c .25 47 1.6  2 2.1 230 19 2 870    7100 2200   0 .49 45 4.5 0 .41 40 3.7 0 3.5 280 28 2 1.2 56 15 0 900     300 11000    0 900     300 10000    0 .064 6.5 .35 0 5.0 290 39 2 .021 5.0 .17  0 .022 4.9 .17  0
termination-restricted-15/b.02_true-termination_true-no-overflow.c .24 50 1.7  2 2.1 220 19 2 880    6100 3200   0 .50 42 4.5 0 .46 40 3.8 0 3.6 270 33 2 1.2 56 13 0 900     260 13000    0 900     270 11000    0 .066 6.5 .33 0 5.1 300 41 2 .040 4.9 .18  0 .036 4.9 .21  0
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c .22 47 1.4  2 6.6 450 44 2 880    4100 3700   0 .45 41 4.0 0 .42 40 3.8 0 3.2 280 28 0 1.2 58 14 0 900     180 10000    0 900     170 11000    0 .067 6.6 .31 0 18   400 160 2 .047 4.9 .16  0 .020 4.9 .16  0
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c .22 45 1.2  2 2.4 270 19 2 870    4000 4500   0 .47 40 4.4 0 .42 40 3.8 0 3.2 270 32 0 1.2 57 13 0 900     180 10000    0 900     170 11000    0 .041 6.6 .35 0 17   380 180 2 .031 4.9 .10  0 .036 5.0 .11  0
termination-restricted-15/b.04_true-termination_true-no-overflow.c .42 57 2.9  2 2.2 230 18 2 .41 33 3.8 2 .47 43 4.7 0 .42 40 3.7 0 3.7 290 32 0 1.2 56 13 0 .10  26 .76 2 .088 26 .83 2 .039 6.6 .38 0 7.0 300 59 2 .050 5.0 .14  0 .024 4.9 .10  0
termination-restricted-15/b.05_true-termination_true-no-overflow.c .38 54 2.4  2 2.5 250 23 2 .42 33 3.8 2 .49 43 3.7 0 .42 41 4.2 0 4.1 300 32 2 1.2 56 15 0 .10  26 .71 2 .087 26 .80 2 .039 6.5 .36 0 5.5 310 47 2 .049 5.0 .12  0 .023 4.9 .21  0
termination-restricted-15/b.06_true-termination_true-no-overflow.c .29 53 2.1  2 2.2 230 19 2 880    4500 3000   0 .47 40 4.0 0 .42 40 3.7 0 4.1 290 34 2 1.2 57 13 0 900     630 11000    0 900     630 11000    0 .065 6.6 .31 0 5.3 310 43 2 .017 5.0 .055 0 .032 4.9 .13  0
termination-restricted-15/b.07_true-termination_true-no-overflow.c .29 51 2.3  2 2.9 280 24 2 870    6300 5000   0 .46 41 4.6 0 .43 40 4.2 0 3.7 280 36 2 1.2 57 15 0 900     380 12000    0 900     380 11000    0 .069 6.6 .28 0 5.5 300 45 2 .047 5.0 .14  0 .046 4.9 .14  0
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c 900    2300 8800    0 4.3 300 29 2 870    3300 6800   0 .50 43 4.2 0 .43 40 3.8 0 4.6 310 42 2 1.2 57 12 0 900     540 10000    0 900     530 12000    0 .068 6.5 .41 0 9.2 530 76 2 .047 4.9 .16  0 .048 5.1 .14  0
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c .40 58 2.5  2 2.8 280 22 2 870    3100 6000   0 .48 40 4.1 0 .45 40 3.7 0 3.9 280 30 2 1.2 56 15 0 900     560 9900    0 900     560 11000    0 .069 6.6 .29 0 5.7 310 44 2 .024 4.9 .15  0 .023 5.0 .17  0
termination-restricted-15/b.10_true-termination_true-no-overflow.c .32 51 2.7  2 4.4 340 30 2 870    2700 6600   0 .50 43 5.0 0 .45 40 3.7 0 4.7 310 43 2 1.3 56 15 0 900     390 9700    0 900     390 9900    0 .037 6.5 .43 0 18   360 200 2 .026 5.1 .18  0 .025 4.9 .15  0
termination-restricted-15/b.11_true-termination_true-no-overflow.c .38 51 2.2  2 3.0 270 23 2 870    3100 6900   0 .50 40 4.4 0 .43 38 4.1 0 5.1 320 47 2 1.2 55 15 0 900     400 10000    0 900     410 12000    0 .065 6.6 .38 0 31   370 380 2 .047 4.9 .12  0 .025 4.9 .16  0
termination-restricted-15/b.12_true-termination_true-no-overflow.c .34 53 2.5  2 3.5 280 26 2 870    2800 6100   0 .51 41 4.2 0 .48 41 4.2 0 4.1 290 37 2 1.2 56 12 0 900     490 11000    0 900     490 11000    0 .060 6.6 .34 0 5.6 300 47 2 .034 4.9 .14  0 .048 4.9 .14  0
termination-restricted-15/b.13_true-termination_true-no-overflow.c .38 49 2.1  2 3.6 280 25 2 870    2900 6600   0 .48 40 4.2 0 .45 40 4.3 0 4.3 280 39 2 1.2 55 14 0 900     490 12000    0 900     500 11000    0 .056 6.5 .36 0 5.9 310 47 2 .043 4.9 .17  0 .024 4.9 .18  0
termination-restricted-15/b.14_true-termination_true-no-overflow.c .94 91 8.8  2 2.8 270 21 2 870    1300 3100   0 .49 45 4.7 0 .45 40 3.8 0 5.1 300 42 2 1.5 56 16 0 900     850 12000    0 900     840 12000    0 .042 6.5 .40 0 5.6 290 49 2 .041 5.0 .15  0 .021 4.9 .20  0
termination-restricted-15/b.15_true-termination_true-no-overflow.c .51 55 4.0  2 2.6 260 22 2 870    960 3400   0 .48 40 4.4 0 .45 40 3.8 0 4.7 290 44 2 1.5 57 17 0 900     1000 11000    0 900     1000 9500    0 .043 6.5 .32 0 6.0 300 48 2 .022 5.0 .18  0 .022 4.8 .15  0
termination-restricted-15/b.16_true-termination_true-no-overflow.c .32 56 2.3  2 2.6 250 24 2 870    660 3700   0 .48 40 4.1 0 .43 40 4.6 0 4.1 280 35 2 1.4 56 16 0 900     790 13000    0 900     790 11000    0 .039 6.5 .43 0 5.6 290 49 2 .026 4.9 .17  0 .024 4.9 .14  0
termination-restricted-15/b.17_true-termination_true-no-overflow.c .39 55 2.7  2 2.8 260 21 2 870    660 3500   0 .49 41 4.2 0 .42 40 4.2 0 4.2 280 38 2 1.4 58 17 0 900     1100 10000    0 900     1100 11000    0 .040 6.6 .30 0 5.9 280 50 2 .023 4.9 .16  0 .023 4.9 .18  0
termination-restricted-15/b.18_true-termination_true-no-overflow.c .55 66 4.6  2 3.4 280 26 2 870    1300 4400   0 .48 41 4.4 0 .44 40 4.3 0 5.9 320 46 2 1.6 56 17 0 900     930 11000    0 900     930 10000    0 .039 6.5 .38 0 6.5 320 54 2 .025 4.9 .16  0 .022 4.9 .16  0
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c 140    15000 1500    0 5.5 430 38 2 870    7900 8000   0 .45 43 3.8 0 .48 41 4.2 0 110   6600 1300 2 1.4 56 17 0 900     2100 9400    0 900     2100 10000    0 .069 6.5 .41 0 11   470 93 2 .025 4.9 .15  0 .044 4.9 .17  0
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c .39 61 2.5  2 3.8 310 26 2 870    7900 7500   0 .48 43 4.2 0 .41 40 3.7 0 6.3 350 51 2 1.4 56 16 0 900     2400 12000    0 900     2400 11000    0 .066 6.5 .32 0 6.7 340 53 2 .044 4.8 .18  0 .039 5.0 .11  0
termination-restricted-15/c.02_true-termination_true-no-overflow.c .39 59 3.4  2 2.3 260 17 2 870    660 4000   0 .48 40 4.3 0 .45 41 4.6 0 4.7 320 40 2 1.4 56 14 0 900     1300 8800    0 900     1300 9100    0 .067 6.5 .30 0 7.0 320 64 2 .024 5.0 .13  0 .039 5.0 .18  0
termination-restricted-15/c.03_true-termination_true-no-overflow.c .30<