Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux Map2Check v7.2-Flock : Tue Nov 27 22:00:00 -04 2018 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 VeriFuzz 1.0.0
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: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:20:21 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 2018-12-09 02:47:33 CET
Run set 2ls.sv-comp19_prop-nooverflow.NoOverflows-BitVectors cbmc.sv-comp19_prop-nooverflow.NoOverflows-BitVectors cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-BitVectors cpa-seq.sv-comp19_prop-nooverflow.NoOverflows-BitVectors depthk.sv-comp19_prop-nooverflow.NoOverflows-BitVectors divine-explicit.sv-comp19_prop-nooverflow.NoOverflows-BitVectors divine-smt.sv-comp19_prop-nooverflow.NoOverflows-BitVectors esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-BitVectors map2check.sv-comp19_prop-nooverflow.NoOverflows-BitVectors pesco.sv-comp19_prop-nooverflow.NoOverflows-BitVectors pinaka.sv-comp19_prop-nooverflow.NoOverflows-BitVectors smack.sv-comp19_prop-nooverflow.NoOverflows-BitVectors symbiotic.sv-comp19_prop-nooverflow.NoOverflows-BitVectors uautomizer.sv-comp19_prop-nooverflow.NoOverflows-BitVectors ukojak.sv-comp19_prop-nooverflow.NoOverflows-BitVectors utaipan.sv-comp19_prop-nooverflow.NoOverflows-BitVectors verifuzz.sv-comp19_prop-nooverflow.NoOverflows-BitVectors
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 status cpu (s) mem (MB) energy (J) score
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i false(no-overflow) .15  25 1.1  1 false(no-overflow) .074 9.2 .62 1 false(no-overflow) .081 9.2 .43 1 false(no-overflow) 3.9 280 36 1 false(no-overflow) .14 34 1.6 0 unknown .035 4.6 .20 0 unknown .054 4.6 .16  0 false(no-overflow) .078 26 1.1  1 timeout 900    230 10000   0 false(no-overflow) 3.9 280 34 1 false(no-overflow) .38 61 3.4 1 disqualified 2.6 72 26 0 false(no-overflow) .21 15 2.3 1 false(no-overflow) 8.7 370 70 1 false(no-overflow) 8.0 340 53 1 false(no-overflow) 8.1 350 62 1 false(no-overflow) 4.4 170 41 1
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .14  26 1.1  1 false(no-overflow) .062 9.3 .57 1 false(no-overflow) .095 10   .51 1 false(no-overflow) 4.3 280 38 1 false(no-overflow) .14 34 1.5 0 unknown .028 4.6 .25 0 unknown .051 4.6 .14  0 false(no-overflow) .090 26 .99 1 false(no-overflow) .39 83 4.3 0 false(no-overflow) 4.2 280 37 1 false(no-overflow) .39 61 3.5 1 disqualified 2.7 75 33 0 false(no-overflow) .19 16 1.9 1 false(no-overflow) 9.2 380 62 1 false(no-overflow) 8.8 360 69 1 false(no-overflow) 7.6 350 69 1 false(no-overflow) 4.3 170 50 1
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .11  25 1.1  1 false(no-overflow) .12  9.4 .42 1 false(no-overflow) .061 9.3 .79 1 false(no-overflow) 4.2 290 37 1 false(no-overflow) .16 33 1.6 0 unknown .046 4.6 .17 0 unknown .044 4.6 .13  0 false(no-overflow) .083 26 1.0  1 false(no-overflow) .82 83 10   0 false(no-overflow) 4.3 280 38 1 false(no-overflow) .38 61 3.7 1 disqualified 2.7 75 33 0 false(no-overflow) .21 16 2.3 1 false(no-overflow) 8.4 360 65 1 false(no-overflow) 7.9 350 61 1 false(no-overflow) 8.9 360 64 1 false(no-overflow) 4.5 170 42 1
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .11  25 .95 1 false(no-overflow) .059 9.7 .60 1 false(no-overflow) .062 8.9 .60 1 false(no-overflow) 3.8 280 34 1 false(no-overflow) .15 34 1.9 0 unknown .031 4.6 .30 0 unknown .029 4.6 .22  0 false(no-overflow) .077 26 .92 1 timeout 900    230 9700   0 false(no-overflow) 3.7 280 36 1 false(no-overflow) .40 61 4.4 1 disqualified 2.6 72 29 0 false(no-overflow) .19 16 2.6 1 false(no-overflow) 7.7 340 59 1 false(no-overflow) 7.7 340 68 1 false(no-overflow) 8.4 350 71 1 false(no-overflow) 4.4 160 45 1
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .12  25 .96 1 false(no-overflow) .061 9.7 .55 1 false(no-overflow) .076 8.9 .56 1 false(no-overflow) 4.0 280 37 1 false(no-overflow) .14 34 1.5 0 unknown .044 4.6 .16 0 unknown .031 4.6 .18  0 false(no-overflow) .095 26 .72 1 timeout 900    250 10000   0 false(no-overflow) 3.9 280 34 1 false(no-overflow) .38 61 3.1 1 disqualified 2.6 72 31 0 false(no-overflow) .19 16 2.1 1 false(no-overflow) 7.9 340 64 1 false(no-overflow) 7.5 330 55 1 false(no-overflow) 7.6 350 70 1 false(no-overflow) 4.5 170 45 1
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .12  25 1.1  1 false(no-overflow) .068 9.8 .55 1 false(no-overflow) .063 9.1 .60 1 false(no-overflow) 4.0 280 37 1 false(no-overflow) .14 34 1.7 0 unknown .033 4.6 .27 0 unknown .029 4.6 .20  0 false(no-overflow) .084 26 .89 1 false(no-overflow) .40 83 5.2 0 false(no-overflow) 4.2 290 36 1 false(no-overflow) .38 61 4.1 1 disqualified 2.7 73 32 0 false(no-overflow) .19 16 2.1 1 false(no-overflow) 8.9 370 68 1 false(no-overflow) 8.5 370 69 1 false(no-overflow) 9.2 370 70 1 false(no-overflow) 4.7 170 50 1
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .11  26 .99 1 false(no-overflow) .071 9.7 .53 1 false(no-overflow) .065 9.1 .55 1 false(no-overflow) 4.0 280 35 1 false(no-overflow) .14 34 1.5 0 unknown .031 4.6 .14 0 unknown .030 4.7 .20  0 false(no-overflow) .080 26 .89 1 false(no-overflow) .40 83 4.5 0 false(no-overflow) 4.0 280 38 1 false(no-overflow) .39 61 4.2 1 disqualified 2.6 72 31 0 false(no-overflow) .20 16 2.3 1 false(no-overflow) 8.9 370 62 1 false(no-overflow) 8.1 360 61 1 false(no-overflow) 8.0 380 72 1 false(no-overflow) 4.5 160 44 1
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .12  25 1.0  1 false(no-overflow) .062 9.8 .69 1 false(no-overflow) .064 8.7 .50 1 false(no-overflow) 4.0 280 38 1 false(no-overflow) .14 34 1.9 0 unknown .024 4.7 .18 0 unknown .033 4.6 .29  0 false(no-overflow) .077 26 .87 1 false(no-overflow) .41 82 4.8 0 false(no-overflow) 4.2 280 39 1 false(no-overflow) .39 61 3.5 1 disqualified 2.7 73 30 0 false(no-overflow) .18 17 2.0 1 false(no-overflow) 9.0 380 65 1 false(no-overflow) 8.6 370 64 1 false(no-overflow) 8.7 370 70 1 false(no-overflow) 4.6 170 44 1
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .12  26 .87 1 false(no-overflow) .15  7.6 .33 1 false(no-overflow) .13  8.8 .41 1 false(no-overflow) 3.9 280 35 1 false(no-overflow) .16 34 1.9 0 unknown .046 4.6 .20 0 unknown .041 4.6 .14  0 false(no-overflow) .090 26 1.4  1 false(no-overflow) .40 83 5.0 0 false(no-overflow) 4.0 280 34 1 false(no-overflow) .37 61 4.3 1 disqualified 2.6 72 35 0 false(no-overflow) .21 17 2.1 1 false(no-overflow) 8.9 370 63 1 false(no-overflow) 7.8 350 65 1 false(no-overflow) 8.7 370 70 1 false(no-overflow) 4.3 170 41 1
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .14  25 1.7  1 false(no-overflow) .064 9.6 .51 1 false(no-overflow) .058 9.4 .58 1 false(no-overflow) 4.3 280 36 1 false(no-overflow) .14 34 1.5 0 unknown .032 4.6 .21 0 unknown .034 4.6 .17  0 false(no-overflow) .10  26 .82 1 false(no-overflow) .41 83 4.6 0 false(no-overflow) 4.2 280 38 1 false(no-overflow) .39 61 3.7 1 disqualified 2.7 73 32 0 false(no-overflow) .18 15 2.5 1 false(no-overflow) 9.2 380 78 1 false(no-overflow) 8.3 360 64 1 false(no-overflow) 8.0 360 60 1 timeout 900   170 14000 0
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true .10  26 1.1  2 true .078 6.4 .32 2 witness invalid (true) .045 7.3 .33 0 true 3.5 270 34 2 unknown .79 67 8.5 0 unknown .034 4.6 .26 0 unknown .033 4.7 .25  0 true .085 26 .87 2 timeout 900    240 9800   0 true 3.6 280 35 2 true .39 61 3.4 2 disqualified 2.0 67 24 0 true .14 15 1.7 2 true 7.1 330 60 2 true 8.6 360 63 2 true 8.3 370 65 2 timeout 900   170 11000 0
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true .099 25 .85 2 true .069 5.9 .30 2 true .087 6.4 .37 2 true 3.7 280 35 2 unknown .81 67 8.7 0 unknown .037 4.5 .14 0 unknown .055 4.6 .15  0 true .084 26 .95 2 timeout 900    230 9900   0 true 3.9 280 32 2 true .38 61 3.7 2 disqualified 2.0 67 23 0 true .17 16 2.1 2 true 8.7 380 71 2 true 8.9 350 62 2 true 8.8 360 70 2 timeout 900   170 11000 0
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true .10  25 .83 2 true .052 6.5 .38 2 true .095 7.0 .32 2 true 3.7 280 34 2 unknown .80 66 8.8 0 unknown .033 4.6 .19 0 unknown .039 4.8 .22  0 true .081 26 .84 2 timeout 900    240 9500   0 true 3.7 280 32 2 true .38 61 4.1 2 disqualified 2.0 68 25 0 true .15 16 2.0 2 true 8.8 370 64 2 true 8.5 370 63 2 true 8.5 350 63 2 timeout 900   160 11000 0
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true .096 25 1.0  2 true .048 7.4 .47 2 true .051 7.3 .37 2 true 3.4 270 35 2 unknown .80 66 9.3 0 unknown .029 4.6 .21 0 unknown .032 4.6 .27  0 true .082 26 1.2  2 timeout 900    250 9900   0 true 3.4 270 33 2 true .38 61 3.6 2 disqualified 2.0 67 24 0 true .16 16 1.9 2 true 8.3 350 62 2 true 8.3 370 62 2 true 8.3 360 63 2 timeout 900   170 12000 0
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true .10  25 .92 2 true .059 6.4 .40 2 true .054 7.1 .34 2 true 3.6 280 34 2 unknown .81 65 9.7 0 unknown .047 4.6 .18 0 unknown .032 4.6 .20  0 true .084 26 .83 2 timeout 900    230 10000   0 true 3.8 280 36 2 true .40 61 3.0 2 disqualified 2.1 68 26 0 true .15 16 2.4 2 true 8.7 370 64 2 true 9.2 360 63 2 true 7.9 350 60 2 timeout 900   170 13000 0
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .12  24 .93 1 false(no-overflow) .077 9.2 .44 1 false(no-overflow) .12  7.4 .37 1 false(no-overflow) 3.0 270 28 1 false(no-overflow) .14 34 1.5 0 unknown .029 4.6 .21 0 unknown .027 4.7 .26  0 false(no-overflow) .083 26 1.2  1 false(no-overflow) .40 83 4.4 0 false(no-overflow) 3.1 270 29 1 false(no-overflow) .38 59 3.2 1 disqualified 3.1 110 40 0 false(no-overflow) .23 18 2.7 1 false(no-overflow) 7.7 360 61 1 false(no-overflow) 7.9 370 55 1 false(no-overflow) 7.8 360 65 1 false(no-overflow) 3.5 150 38 1
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .16  24 1.0  1 false(no-overflow) .091 9.2 .80 1 false(no-overflow) .087 9.0 .70 1 false(no-overflow) 3.1 260 31 1 false(no-overflow) .21 33 2.0 0 unknown .052 4.6 .25 0 unknown .028 4.6 .17  0 false(no-overflow) .14  26 1.6  1 false(no-overflow) .43 83 4.6 0 false(no-overflow) 3.0 270 30 1 false(no-overflow) .35 58 4.4 1 disqualified 3.4 85 44 0 false(no-overflow) .26 18 2.3 1 false(no-overflow) 7.8 370 64 1 false(no-overflow) 7.0 340 61 1 false(no-overflow) 7.6 370 62 1 false(no-overflow) 3.5 150 40 1
termination-crafted/Ackermann_false-no-overflow.c error (5) .095 24 .86 0 false(no-overflow) .095 9.9 .91 1 false(no-overflow) .058 9.4 .58 1 timeout 900   3400 9800 0 false(no-overflow) .13 33 1.8 0 unknown .030 4.6 .19 0 unknown .032 4.7 .27  0 false(no-overflow) .080 26 1.1  1 false(no-overflow) 44    130 550   0 timeout 900   3600 10000 0 false(no-overflow) .38 59 3.4 1 disqualified 2.7 76 40 0 false(no-overflow) .28 18 3.3 1 false(no-overflow) 7.2 360 56 1 false(no-overflow) 7.0 330 53 1 false(no-overflow) 6.4 330 51 1 timeout 900   150 11000 0
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .067 9.8 .48 1 false(no-overflow) .067 9.2 .54 1 false(no-overflow) 3.2 270 28 1 false(no-overflow) .13 33 1.7 0 unknown .030 4.6 .17 0 unknown .031 4.6 .20  0 false(no-overflow) .10  26 .76 1 timeout 900    74 9600   0 false(no-overflow) 3.0 270 31 1 false(no-overflow) .35 59 3.1 1 disqualified 880   1100 10000 0 false(no-overflow) .24 18 3.3 1 false(no-overflow) 7.6 360 65 1 false(no-overflow) 7.5 350 67 1 false(no-overflow) 7.6 360 68 1 false(no-overflow) 12   150 140 1
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .15  23 .93 1 false(no-overflow) .083 9.4 .42 1 false(no-overflow) .063 9.8 .48 1 false(no-overflow) 3.0 270 25 1 false(no-overflow) .14 33 1.4 0 unknown .029 4.6 .21 0 unknown .029 4.6 .23  0 false(no-overflow) .078 26 .92 1 timeout 900    75 10000   0 false(no-overflow) 3.2 260 33 1 false(no-overflow) .40 59 3.3 1 disqualified 3.1 77 47 0 false(no-overflow) .24 18 3.3 1 false(no-overflow) 7.3 340 55 1 false(no-overflow) 7.3 350 55 1 false(no-overflow) 7.7 360 56 1 false(no-overflow) 8.6 150 100 1
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .080 9.4 .56 1 false(no-overflow) .062 10   .62 1 false(no-overflow) 2.9 270 27 1 false(no-overflow) .14 34 1.6 0 unknown .037 4.6 .19 0 unknown .029 4.7 .21  0 false(no-overflow) .085 26 .80 1 timeout 900    80 12000   0 false(no-overflow) 3.1 270 30 1 false(no-overflow) .37 59 3.2 1 disqualified 3.1 84 44 0 false(no-overflow) .26 17 2.7 1 false(no-overflow) 7.8 370 61 1 false(no-overflow) 8.2 370 67 1 false(no-overflow) 7.5 340 58 1 false(no-overflow) 3.6 150 41 1
termination-crafted/Binary_Search_false-no-overflow.c error (5) .090 24 .76 0 false(no-overflow) .10  9.4 .97 1 false(no-overflow) .068 9.1 .60 1 false(no-overflow) 2.9 270 31 1 false(no-overflow) .17 34 1.7 0 unknown .037 4.7 .26 0 unknown .054 4.6 .14  0 false(no-overflow) .11  26 1.3  1 false(no-overflow) 570    130 6700   0 false(no-overflow) 3.1 270 31 1 false(no-overflow) .36 59 3.7 1 disqualified 2.7 74 39 0 false(no-overflow) .24 19 2.8 1 false(no-overflow) 7.5 370 60 1 false(no-overflow) 7.9 360 69 1 false(no-overflow) 8.0 370 63 1 false(no-overflow) 3.5 150 35 1
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .14  24 1.1  1 false(no-overflow) .12  8.4 .28 1 false(no-overflow) .068 9.4 .43 1 false(no-overflow) 3.2 270 29 1 false(no-overflow) .38 35 4.0 0 unknown .028 4.7 .20 0 unknown .030 4.6 .19  0 false(no-overflow) .090 26 .97 1 false(no-overflow) 210    100 2400   0 false(no-overflow) 3.2 270 28 1 false(no-overflow) .35 59 3.1 1 disqualified 3.1 79 43 0 false(no-overflow) .25 18 2.6 1 false(no-overflow) 7.7 350 58 1 false(no-overflow) 8.6 370 64 1 false(no-overflow) 7.8 370 58 1 false(no-overflow) 95   150 1100 1
termination-crafted/Cairo_step2_false-no-overflow.c timeout 900     1300 11000    0 error (42) 880     4500   4100    0 error (42) 880     110   11000    0 timeout 910   2500 11000 0 unknown 41    40 520   0 unknown .028 4.7 .26 0 unknown .029 4.6 .21  0 timeout 900     480 12000    0 false(no-overflow) 180    77 2100   0 timeout 910   2600 12000 0 timeout 900    410 4100   0 disqualified 880   600 11000 0 timeout (verification) 900    260 11000   0 timeout 900   1200 14000 0 timeout 900   3800 10000 0 timeout 900   1100 12000 0 timeout 900   150 10000 0
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .12  24 .99 1 false(no-overflow) .086 9.4 .73 1 false(no-overflow) .075 9.5 .44 1 false(no-overflow) 3.3 280 30 1 false(no-overflow) .16 33 2.5 0 unknown .059 4.6 .17 0 unknown .026 4.6 .18  0 false(no-overflow) .11  26 1.1  1 false(no-overflow) .40 79 6.0 0 false(no-overflow) 3.3 280 34 1 false(no-overflow) .43 60 3.5 1 disqualified 3.1 80 41 0 false(no-overflow) .24 18 2.8 1 false(no-overflow) 7.3 330 65 1 false(no-overflow) 7.0 340 61 1 false(no-overflow) 8.8 370 67 1 false(no-overflow) 3.6 150 35 1
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .16  24 1.0  1 false(no-overflow) .078 8.9 .49 1 false(no-overflow) .063 9.6 .54 1 false(no-overflow) 3.0 270 31 1 false(no-overflow) .13 33 1.5 0 unknown .036 4.7 .13 0 unknown .030 4.6 .20  0 false(no-overflow) .081 26 .80 1 timeout 900    74 11000   0 false(no-overflow) 3.0 270 27 1 false(no-overflow) .35 59 3.7 1 disqualified 3.1 82 43 0 false(no-overflow) .22 17 2.8 1 false(no-overflow) 7.2 340 56 1 false(no-overflow) 7.5 350 64 1 false(no-overflow) 7.9 370 68 1 false(no-overflow) 10   150 120 1
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .13  24 1.3  1 false(no-overflow) .071 9.4 .61 1 false(no-overflow) .12  9.1 .40 1 false(no-overflow) 3.0 270 27 1 false(no-overflow) .18 34 2.1 0 unknown .057 4.6 .14 0 unknown .027 4.6 .21  0 false(no-overflow) .13  26 1.3  1 false(no-overflow) 820    78 12000   0 false(no-overflow) 3.1 270 30 1 false(no-overflow) .37 59 4.0 1 disqualified 3.2 82 41 0 false(no-overflow) .24 18 2.9 1 false(no-overflow) 7.8 350 58 1 false(no-overflow) 7.8 350 62 1 false(no-overflow) 7.7 360 64 1 false(no-overflow) 3.5 150 36 1
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .081 9.6 .69 1 false(no-overflow) .057 9.6 .59 1 false(no-overflow) 3.0 270 30 1 false(no-overflow) .20 33 3.1 0 unknown .030 4.6 .18 0 unknown .051 4.5 .24  0 false(no-overflow) .13  26 2.2  1 false(no-overflow) 210    83 3300   0 false(no-overflow) 3.1 270 25 1 false(no-overflow) .40 59 3.2 1 disqualified 3.2 81 36 0 false(no-overflow) .24 17 2.0 1 false(no-overflow) 7.4 350 61 1 false(no-overflow) 7.4 350 56 1 false(no-overflow) 7.6 350 59 1 false(no-overflow) 5.0 150 52 1
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .12  24 .89 1 false(no-overflow) .057 9.5 .46 1 false(no-overflow) .068 9.2 .45 1 false(no-overflow) 3.0 270 26 1 false(no-overflow) .14 33 1.7 0 unknown .027 4.6 .18 0 unknown .031 4.6 .26  0 false(no-overflow) .086 26 .74 1 false(no-overflow) .39 83 5.2 0 false(no-overflow) 3.0 270 31 1 false(no-overflow) .37 59 3.2 1 disqualified 3.1 110 39 0 false(no-overflow) .23 18 2.8 1 false(no-overflow) 7.4 360 58 1 false(no-overflow) 7.7 360 58 1 false(no-overflow) 7.6 370 60 1 false(no-overflow) 3.3 150 33 1
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .11  24 1.3  1 false(no-overflow) .074 9.9 .65 1 false(no-overflow) .077 9.8 .42 1 false(no-overflow) 3.0 270 32 1 false(no-overflow) .15 34 1.9 0 unknown .056 4.7 .16 0 unknown .030 4.6 .16  0 false(no-overflow) .092 26 1.0  1 false(no-overflow) .40 83 5.0 0 false(no-overflow) 3.1 270 30 1 false(no-overflow) .36 59 3.4 1 disqualified 3.1 84 38 0 false(no-overflow) .24 19 2.8 1 false(no-overflow) 7.2 340 63 1 false(no-overflow) 7.2 330 52 1 false(no-overflow) 8.0 370 64 1 false(no-overflow) 3.4 150 34 1
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .11  24 .99 1 false(no-overflow) .071 9.6 .62 1 false(no-overflow) .066 8.9 .54 1 false(no-overflow) 3.1 270 27 1 false(no-overflow) .19 33 2.1 0 unknown .028 4.6 .23 0 unknown .030 4.6 .18  0 false(no-overflow) .11  26 1.2  1 false(no-overflow) .39 82 4.6 0 false(no-overflow) 3.0 270 29 1 false(no-overflow) .35 59 4.3 1 disqualified 3.1 84 40 0 false(no-overflow) .23 18 2.8 1 false(no-overflow) 7.1 340 55 1 false(no-overflow) 6.7 320 58 1 false(no-overflow) 7.9 370 65 1 false(no-overflow) 3.2 150 35 1
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .074 9.3 .47 1 false(no-overflow) .092 9.2 .36 1 false(no-overflow) 3.0 280 31 1 false(no-overflow) .14 34 1.5 0 unknown .053 4.6 .16 0 unknown .046 4.6 .17  0 false(no-overflow) .087 26 1.0  1 false(no-overflow) 140    4500 1500   0 false(no-overflow) 3.0 270 28 1 false(no-overflow) .38 59 3.0 1 disqualified 3.1 78 45 0 false(no-overflow) .22 19 2.7 1 false(no-overflow) 8.2 370 67 1 false(no-overflow) 7.9 370 61 1 false(no-overflow) 8.4 380 68 1 false(no-overflow) 92   150 1200 1
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .11  24 1.1  1 false(no-overflow) .071 11   .50 1 false(no-overflow) .13  8.9 .34 1 false(no-overflow) 3.0 270 26 1 false(no-overflow) .16 33 1.8 0 unknown .037 4.8 .20 0 unknown .049 4.6 .13  0 false(no-overflow) .10  26 1.1  1 timeout 900    83 11000   0 false(no-overflow) 3.1 270 29 1 false(no-overflow) .36 59 3.7 1 disqualified 3.1 83 38 0 false(no-overflow) .23 18 2.8 1 false(no-overflow) 7.6 370 66 1 false(no-overflow) 7.8 370 56 1 false(no-overflow) 7.9 370 65 1 false(no-overflow) 3.7 160 37 1
termination-crafted/NestedRecursion_1a_false-no-overflow.c error (5) .092 24 .88 0 false(no-overflow) .084 9.7 .84 1 false(no-overflow) .11  8.7 .47 1 false(no-overflow) 3.1 270 25 1 false(no-overflow) .14 33 1.8 0 unknown .037 4.6 .20 0 unknown .027 4.8 .16  0 false(no-overflow) .080 26 .86 1 false(no-overflow) 13    91 160   0 false(no-overflow) 3.0 270 27 1 false(no-overflow) .35 59 4.0 1 disqualified 2.7 75 33 0 false(no-overflow) .24 18 3.3 1 false(no-overflow) 8.3 360 64 1 false(no-overflow) 8.3 350 67 1 false(no-overflow) 7.3 340 55 1 false(no-overflow) 7.6 200 80 1
termination-crafted/NestedRecursion_2a_false-no-overflow.c error (5) .085 23 .76 0 false(no-overflow) .065 9.9 .59 1 false(no-overflow) .066 10   .51 1 false(no-overflow) 3.1 280 31 1 false(no-overflow) .13 34 1.6 0 unknown .036 4.6 .14 0 unknown .028 4.6 .17  0 false(no-overflow) .090 26 .81 1 false(no-overflow) 6.8  91 84   0 false(no-overflow) 3.2 280 29 1 false(no-overflow) .37 59 4.1 1 disqualified 2.6 73 33 0 false(no-overflow) .24 18 2.5 1 false(no-overflow) 7.8 360 62 1 false(no-overflow) 8.2 360 62 1 false(no-overflow) 8.3 360 69 1 false(no-overflow) 3.6 150 33 1
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .11  24 1.2  1 false(no-overflow) .066 9.4 .70 1 false(no-overflow) .079 9.2 .34 1 false(no-overflow) 3.3 280 34 1 false(no-overflow) .14 34 1.6 0 unknown .043 4.6 .14 0 unknown .032 4.6 .21  0 false(no-overflow) .10  26 .74 1 false(no-overflow) .42 82 4.5 0 false(no-overflow) 3.3 280 31 1 false(no-overflow) .36 58 3.6 1 disqualified 4.4 80 50 0 false(no-overflow) .22 19 2.6 1 false(no-overflow) 6.4 340 57 1 false(no-overflow) 8.2 360 59 1 false(no-overflow) 6.7 350 51 1 false(no-overflow) 3.3 150 33 1
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .12  24 .98 1 false(no-overflow) .089 9.3 .51 1 false(no-overflow) .070 9.6 .46 1 false(no-overflow) 3.3 280 31 1 false(no-overflow) .13 33 1.5 0 unknown .031 4.7 .24 0 unknown .056 4.6 .25  0 false(no-overflow) .084 26 .73 1 false(no-overflow) .42 78 4.8 0 false(no-overflow) 3.3 280 33 1 false(no-overflow) .40 59 3.1 1 disqualified 3.1 80 37 0 false(no-overflow) .23 18 2.7 1 false(no-overflow) 7.9 360 67 1 false(no-overflow) 8.2 370 71 1 false(no-overflow) 8.0 350 65 1 false(no-overflow) 3.5 150 32 1
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) .43  30 5.1  1 false(no-overflow) .14  9.9 1.7  1 false(no-overflow) .15  9.7 1.2  1 false(no-overflow) 200   1300 1500 1 false(no-overflow) 15    55 210   0 unknown .047 4.8 .26 0 unknown .055 4.7 .17  0 false(no-overflow) .11  26 1.3  1 false(no-overflow) .40 82 5.0 0 false(no-overflow) 210   1200 1500 1 false(no-overflow) .39 59 3.9 1 disqualified 140   450 1200 0 false(no-overflow) .18 16 2.0 1 false(no-overflow) 27   800 270 1 false(no-overflow) 590   3400 4800 1 false(no-overflow) 59   1500 650 1 false(no-overflow) 3.3 150 34 1
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .12  24 .99 1 false(no-overflow) .075 9.0 .55 1 false(no-overflow) .070 8.5 .39 1 false(no-overflow) 3.1 270 30 1 false(no-overflow) .14 34 1.4 0 unknown .035 4.6 .27 0 unknown .030 4.6 .31  0 false(no-overflow) .084 26 .75 1 false(no-overflow) 170    78 2000   0 false(no-overflow) 3.0 270 31 1 false(no-overflow) .37 59 3.1 1 disqualified 880   1900 10000 0 false(no-overflow) .22 17 2.5 1 false(no-overflow) 7.6 350 57 1 false(no-overflow) 7.5 360 56 1 false(no-overflow) 7.9 360 65 1 error (1) 51   150 610 0
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .11  24 1.1  1 false(no-overflow) .091 8.4 .33 1 false(no-overflow) .067 8.9 .48 1 false(no-overflow) 3.1 270 28 1 false(no-overflow) .14 33 1.5 0 unknown .057 4.6 .18 0 unknown .045 4.6 .17  0 false(no-overflow) .077 26 .95 1 timeout 900    75 8900   0 false(no-overflow) 3.0 270 31 1 false(no-overflow) .35 59 4.1 1 disqualified 3.0 77 39 0 false(no-overflow) .27 20 2.5 1 false(no-overflow) 8.6 370 64 1 false(no-overflow) 8.1 360 57 1 false(no-overflow) 7.7 370 64 1 false(no-overflow) 12   150 140 1
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 900     1200 11000    0 error (42) 880     4400   4400    0 error (42) 880     100   9500    0 timeout 900   2000 12000 0 unknown 34    40 490   0 unknown .028 4.7 .16 0 unknown .035 4.6 .24  0 timeout 900     480 11000    0 false(no-overflow) 220    77 2600   0 timeout 900   2000 12000 0 timeout 900    400 3800   0 disqualified 880   700 12000 0 false(no-overflow) .21 18 3.0 1 timeout 900   1200 13000 0 timeout 900   5200 12000 0 timeout 900   1100 12000 0 timeout 900   150 13000 0
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) .11  24 1.2  1 false(no-overflow) .089 9.1 .39 1 out of memory 860     15000   11000    0 false(no-overflow) 3.1 270 27 1 false(no-overflow) .14 34 1.5 0 unknown .030 4.6 .17 0 unknown .028 4.6 .15  0 false(no-overflow) .081 26 .92 1 false(no-overflow) 120    4000 1400   0 false(no-overflow) 3.1 270 32 1 timeout 900    360 4600   0 disqualified 3.1 83 40 0 false(no-overflow) .27 18 2.8 1 false(no-overflow) 7.1 340 56 1 false(no-overflow) 7.8 360 55 1 false(no-overflow) 7.9 350 61 1 timeout 900   150 12000 0
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .11  24 1.1  1 false(no-overflow) .076 10   .41 1 false(no-overflow) .061 9.3 .58 1 false(no-overflow) 3.2 270 30 1 false(no-overflow) .13 34 1.6 0 unknown .047 4.6 .17 0 unknown .032 4.6 .21  0 false(no-overflow) .082 26 .95 1 false(no-overflow) 35    78 400   0 false(no-overflow) 3.1 270 32 1 false(no-overflow) .37 58 2.7 1 disqualified 880   1400 9000 0 false(no-overflow) .23 17 4.6 1 false(no-overflow) 6.4 330 54 1 false(no-overflow) 7.8 360 62 1 false(no-overflow) 6.9 350 52 1 false(no-overflow) 6.6 150 72 1
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .13  24 .88 1 false(no-overflow) .077 9.6 .51 1 false(no-overflow) .058 9.2 .55 1 false(no-overflow) 3.0 260 25 1 false(no-overflow) .14 34 1.6 0 unknown .045 4.6 .21 0 unknown .033 4.6 .17  0 false(no-overflow) .099 26 .83 1 false(no-overflow) 110    4400 1300   0 false(no-overflow) 3.1 270 31 1 false(no-overflow) .34 59 3.1 1 disqualified 3.2 86 47 0 false(no-overflow) .26 17 2.8 1 false(no-overflow) 8.1 360 62 1 false(no-overflow) 7.1 340 51 1 false(no-overflow) 8.0 370 63 1 timeout 900   150 12000 0
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .11  23 1.2  1 false(no-overflow) .072 9.4 .43 1 false(no-overflow) .12  8.3 .30 1 false(no-overflow) 3.1 270 27 1 false(no-overflow) .14 33 1.4 0 unknown .053 4.7 .18 0 unknown .034 4.7 .11  0 false(no-overflow) .083 26 .85 1 timeout 900    4000 11000   0 false(no-overflow) 3.1 270 27 1 false(no-overflow) .37 59 3.0 1 disqualified 3.1 77 36 0 false(no-overflow) .22 18 3.2 1 false(no-overflow) 7.6 360 63 1 false(no-overflow) 6.5 330 57 1 false(no-overflow) 7.8 360 65 1 false(no-overflow) 3.9 150 37 1
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .12  24 .94 1 false(no-overflow) .077 9.7 .47 1 false(no-overflow) .068 9.3 .49 1 false(no-overflow) 3.1 270 29 1 false(no-overflow) .15 33 2.3 0 unknown .028 4.6 .18 0 unknown .030 4.6 .18  0 false(no-overflow) .10  26 .79 1 false(no-overflow) 140    4500 1500   0 false(no-overflow) 2.9 270 27 1 false(no-overflow) .36 59 3.4 1 disqualified 3.1 82 37 0 false(no-overflow) .24 23 2.7 1 false(no-overflow) 7.9 370 65 1 false(no-overflow) 6.9 340 53 1 false(no-overflow) 8.0 360 57 1 false(no-overflow) 8.8 150 94 1
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .11  24 1.8  1 false(no-overflow) .073 9.5 .58 1 false(no-overflow) .12  8.6 .33 1 false(no-overflow) 3.2 270 32 1 false(no-overflow) .16 33 1.9 0 unknown .045 4.6 .18 0 unknown .061 4.7 .21  0 false(no-overflow) .10  26 1.3  1 false(no-overflow) .41 83 5.2 0 false(no-overflow) 3.1 270 30 1 false(no-overflow) .36 59 3.3 1 disqualified 3.2 83 36 0 false(no-overflow) .24 17 2.7 1 false(no-overflow) 7.2 340 60 1 false(no-overflow) 7.4 350 64 1 false(no-overflow) 6.6 330 52 1 false(no-overflow) 3.6 150 34 1
termination-crafted/RecursiveMultiplication_false-no-overflow.c error (5) .12  24 .71 0 false(no-overflow) .078 9.5 .65 1 false(no-overflow) .13  8.1 .31 1 false(no-overflow) 3.5 290 38 1 false(no-overflow) .16 33 1.5 0 unknown .055 4.6 .12 0 unknown .032 4.6 .21  0 false(no-overflow) .11  26 .74 1 false(no-overflow) 46    300 550   0 false(no-overflow) 3.6 290 33 1 false(no-overflow) .37 59 2.9 1 disqualified 2.7 77 40 0 false(no-overflow) .27 18 3.0 1 false(no-overflow) 6.7 330 52 1 false(no-overflow) 7.0 350 58 1 false(no-overflow) 7.5 360 68 1 false(no-overflow) 4.3 200 40 1
termination-crafted/RecursiveNonterminating_false-no-overflow.c error (5) .080 24 .93 0 false(no-overflow) .095 9.0 .52 1 false(no-overflow) .065 9.4 .43 1 false(no-overflow) 3.0 270 28 1 false(no-overflow) .14 33 1.6 0 unknown .033 4.6 .17 0 unknown .028 4.6 .24  0 false(no-overflow) .089 26 .79 1 false(no-overflow) 88    91 1000   0 false(no-overflow) 3.8 270 52 1 false(no-overflow) .36 59 3.3 1 disqualified 2.7 72 33 0 false(no-overflow) .28 22 2.3 1 false(no-overflow) 7.2 330 63 1 false(no-overflow) 7.8 360 60 1 false(no-overflow) 8.2 370 60 1 false(no-overflow) 13   150 150 1
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .12  24 .94 1 false(no-overflow) .072 8.7 .33 1 false(no-overflow) .080 9.5 .46 1 false(no-overflow) 2.9 270 26 1 false(no-overflow) .14 34 1.5 0 unknown .032 4.8 .12 0 unknown .032 4.7 .18  0 false(no-overflow) .078 26 .89 1 timeout 900    74 10000   0 false(no-overflow) 3.1 270 27 1 false(no-overflow) .36 59 3.1 1 disqualified 3.1 76 39 0 false(no-overflow) .23 17 2.7 1 false(no-overflow) 8.0 370 63 1 false(no-overflow) 7.2 340 66 1 false(no-overflow) 7.7 360 56 1 error (1) 51   150 440 0
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .066 9.5 .51 1 false(no-overflow) .068 9.0 .35 1 false(no-overflow) 3.1 270 27 1 false(no-overflow) .15 33 2.1 0 unknown .046 4.6 .14 0 unknown .054 4.6 .21  0 false(no-overflow) .10  26 1.1  1 false(no-overflow) .41 83 4.7 0 false(no-overflow) 3.0 270 28 1 false(no-overflow) .40 59 3.2 1 disqualified 3.1 83 40 0 false(no-overflow) .25 18 2.7 1 false(no-overflow) 8.0 370 58 1 false(no-overflow) 7.1 340 54 1 false(no-overflow) 7.7 360 58 1 false(no-overflow) 3.7 150 36 1
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .15  24 .97 1 false(no-overflow) .11  9.2 .49 1 false(no-overflow) .074 8.8 .71 1 false(no-overflow) 2.8 270 27 1 false(no-overflow) .15 34 1.6 0 unknown .026 4.6 .21 0 unknown .034 4.6 .25  0 false(no-overflow) .092 26 1.1  1 false(no-overflow) .41 83 4.6 0 false(no-overflow) 3.0 270 30 1 false(no-overflow) .37 59 3.8 1 disqualified 12   120 160 0 false(no-overflow) .22 18 2.8 1 false(no-overflow) 7.8 360 63 1 false(no-overflow) 8.0 370 65 1 false(no-overflow) 7.8 360 59 1 false(no-overflow) 3.4 150 34 1
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .12  24 1.3  1 false(no-overflow) .076 10   .50 1 false(no-overflow) .070 8.8 .43 1 false(no-overflow) 3.0 270 28 1 false(no-overflow) .16 33 1.7 0 unknown .048 4.6 .17 0 unknown .033 4.6 .15  0 false(no-overflow) .10  26 1.3  1 false(no-overflow) .41 83 5.7 0 false(no-overflow) 2.9 270 29 1 false(no-overflow) .38 58 3.3 1 disqualified 880   440 11000 0 false(no-overflow) .22 18 2.4 1 false(no-overflow) 7.2 350 59 1 false(no-overflow) 7.4 350 61 1 false(no-overflow) 6.8 330 62 1 false(no-overflow) 3.4 150 33 1
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .12  24 .93 1 false(no-overflow) .10  9.7 .38 1 false(no-overflow) .16  8.6 .30 1 false(no-overflow) 2.9 260 27 1 false(no-overflow) .15 34 2.0 0 unknown .036 4.6 .23 0 unknown .051 4.6 .20  0 false(no-overflow) .10  26 1.3  1 false(no-overflow) .40 79 5.1 0 false(no-overflow) 3.0 270 25 1 false(no-overflow) .37 59 2.7 1 disqualified 11   110 140 0 false(no-overflow) .22 19 2.5 1 false(no-overflow) 7.9 370 63 1 false(no-overflow) 8.1 360 62 1 false(no-overflow) 7.6 370 61 1 false(no-overflow) 3.4 200 35 1
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .12  24 1.2  1 false(no-overflow) .078 9.3 .50 1 false(no-overflow) .094 9.1 .54 1 false(no-overflow) 3.1 270 31 1 false(no-overflow) .20 34 2.0 0 unknown .048 4.6 .21 0 unknown .031 4.6 .16  0 false(no-overflow) .13  26 1.0  1 timeout 900    78 11000   0 false(no-overflow) 3.1 270 32 1 false(no-overflow) .35 59 3.2 1 disqualified 3.1 85 43 0 false(no-overflow) .23 18 2.7 1 false(no-overflow) 7.8 370 61 1 false(no-overflow) 8.2 370 55 1 false(no-overflow) 7.3 340 51 1 false(no-overflow) 220   200 3000 1
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .12  24 .96 1 false(no-overflow) .078 10   .46 1 false(no-overflow) .067 9.0 .70 1 false(no-overflow) 3.1 270 26 1 false(no-overflow) .14 33 2.0 0 unknown .031 4.6 .17 0 unknown .029 4.6 .18  0 false(no-overflow) .098 26 .84 1 false(no-overflow) .39 83 5.1 0 false(no-overflow) 3.0 270 26 1 false(no-overflow) .35 58 3.5 1 disqualified 3.2 84 38 0 false(no-overflow) .23 18 2.7 1 false(no-overflow) 7.8 370 61 1 false(no-overflow) 7.5 340 61 1 false(no-overflow) 7.5 360 61 1 false(no-overflow) 3.6 150 40 1
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .15  24 1.0  1 false(no-overflow) .075 9.5 .52 1 false(no-overflow) .065 9.1 .61 1 false(no-overflow) 3.0 270 28 1 false(no-overflow) .14 34 1.5 0 unknown .030 4.6 .20 0 unknown .031 4.6 .21  0 false(no-overflow) .083 26 .88 1 false(no-overflow) 77    82 1200   0 false(no-overflow) 3.1 270 26 1 false(no-overflow) .36 59 3.7 1 disqualified 3.1 84 40 0 false(no-overflow) .24 18 2.9 1 false(no-overflow) 7.4 340 50 1 false(no-overflow) 7.9 370 67 1 false(no-overflow) 7.4 350 55 1 false(no-overflow) 6.3 150 77 1
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .14  24 1.0  1 false(no-overflow) .14  10   .63 1 false(no-overflow) .082 8.8 .51 1 false(no-overflow) 3.5 280 35 1 false(no-overflow) .15 33 1.7 0 unknown .036 4.6 .25 0 unknown .029 4.6 .29  0 false(no-overflow) .11  26 1.0  1 false(no-overflow) 5.8  83 79   0 false(no-overflow) 3.6 280 35 1 false(no-overflow) .36 59 3.9 1 disqualified 3.5 91 39 0 false(no-overflow) .26 18 3.4 1 false(no-overflow) 16   540 140 1 false(no-overflow) 15   520 140 1 false(no-overflow) 17   520 150 1 false(no-overflow) 4.0 160 41 1
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .13  24 .85 1 false(no-overflow) .086 9.3 .45 1 false(no-overflow) .075 8.8 .49 1 false(no-overflow) 3.0 270 26 1 false(no-overflow) .17 34 2.1 0 unknown .049 4.6 .13 0 unknown .031 4.6 .20  0 false(no-overflow) .14  26 1.3  1 timeout 900    4300 11000   0 false(no-overflow) 3.2 270 28 1 false(no-overflow) .40 59 3.7 1 disqualified 3.2 85 45 0 false(no-overflow) .24 18 2.6 1 false(no-overflow) 7.7 360 53 1 false(no-overflow) 6.8 340 56 1 false(no-overflow) 9.1 370 69 1 false(no-overflow) 200   150 2300 1
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .12  24 1.3  1 false(no-overflow) .071 9.4 .51 1 false(no-overflow) .072 8.9 .42 1 false(no-overflow) 2.9 270 27 1 false(no-overflow) .14 33 1.7 0 unknown .031 4.6 .13 0 unknown .029 4.7 .21  0 false(no-overflow) .12  26 .96 1 false(no-overflow) 780    5300 10000   0 false(no-overflow) 3.0 270 32 1 false(no-overflow) .39 59 3.1 1 disqualified 3.2 86 40 0 false(no-overflow) .24 18 3.3 1 false(no-overflow) 7.7 370 65 1 false(no-overflow) 7.1 340 61 1 false(no-overflow) 8.0 370 69 1 false(no-overflow) 3.7 200 36 1
termination-crafted/easy2_false-no-overflow.c timeout 900     1600 10000    0 error (42) 880     2200   4800    0 error (42) 880     160   11000    0 timeout 910   13000 11000 0 unknown 58    48 760   0 unknown .032 4.5 .27 0 unknown .049 4.6 .13  0 timeout 900     1100 11000    0 timeout 900    75 9400   0 timeout 910   13000 11000 0 timeout 900    410 4000   0 disqualified 880   710 9000 0 timeout (verification) 900    410 7800   0 timeout 900   2600 11000 0 timeout 900   5700 7700 0 timeout 900   1600 13000 0 timeout 900   150 10000 0
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true .18  25 1.6  2 true .13  8.2 1.5  2 witness invalid (true) .18  7.4 1.5  0 true 3.0 270 27 2 unknown .78 65 8.1 0 unknown .055 4.6 .15 0 unknown .054 4.7 .16  0 true .088 26 1.0  2 timeout 900    84 10000   0 true 3.0 270 30 2 true .77 60 6.4 2 disqualified 2.4 75 31 0 true .13 16 1.6 2 true 7.4 350 59 2 true 7.1 340 61 2 true 7.6 370 66 2 timeout 890   1600 11000 0
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c true 6.8   200 80    2 error (42) 880     2800   4600    0 error (42) 880     1300   12000    0 true 3.1 270 31 2 unknown .84 68 8.7 0 unknown .032 4.6 .19 0 unknown .032 4.8 .33  0 timeout 900     1800 13000    0 timeout 900    87 10000   0 true 3.2 270 27 2 timeout 900    770 6700   0 disqualified 880   1700 6000 0 timeout (verification) 900    450 7100   0 true 28   620 250 2 timeout 900   4600 9500 0 timeout 900   850 13000 0 timeout 900   150 11000 0
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety_true-no-overflow.c true 3.3   96 43    2 error (42) 880     3100   5000    0 error (42) 870     780   12000    0 true 3.1 270 29 2 unknown .79 66 7.9 0 unknown .035 4.8 .25 0 unknown .028 4.8 .19  0 timeout 900     1600 11000    0 timeout 900    4000 8200   0 true 3.1 270 30 2 timeout 900    1400 5300   0 disqualified 880   460 11000 0 timeout (verification) 900    69 11000   0 true 8.0 350 65 2 true 8.8 360 66 2 true 8.2 370 66 2 timeout 900   150 13000 0
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c true 3.7   170 42    2 error (42) 880     4600   4200    0 error (42) 880     920   9600    0 timeout 910   6800 11000 0 unknown .81 66 9.6 0 unknown .029 4.6 .25 0 unknown .036 4.6 .23  0 timeout 900     1200 11000    0 timeout 900    4800 10000   0 timeout 910   6800 10000 0 timeout 900    920 5200   0 disqualified 880   1800 5500 0 timeout (verification) 900    200 12000   0 true 9.8 390 70 2 timeout 900   5500 10000 0 true 11   430 92 2 timeout 900   150 13000 0
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true .10  24 .80 2 error (42) 880     4300   5000    0 error (42) 880     200   12000    0 true 3.0 270 25 2 unknown .81 65 8.5 0 unknown .028 4.7 .17 0 unknown .030 4.6 .20  0 timeout 900     140 11000    0 timeout 900    90 9900   0 true 3.0 270 26 2 timeout 900    460 5400   0 disqualified 880   550 11000 0 timeout (verification) 900    78 12000   0 true 9.0 350 64 2 true 9.5 430 78 2 true 8.9 360 70 2 timeout 900   150 12000 0
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c true .093 24 .90 2 error (42) 880     4100   4200    0 error (42) 880     190   11000    0 true 3.0 270 28 2 unknown .82 67 8.2 0 unknown .026 4.6 .21 0 unknown .029 4.7 .21  0 timeout 900     220 11000    0 timeout 900    75 9500   0 true 3.1 270 23 2 timeout 900    410 4100   0 disqualified 880   470 10000 0 timeout (verification) 900    74 12000   0 true 9.1 380 65 2 true 9.6 410 74 2 true 9.1 380 72 2 timeout 900   150 9900 0
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true .17  24 1.8  2 true .061 6.5 .41 2 true .058 6.2 .47 2 true 3.1 270 31 2 unknown .85 66 9.7 0 unknown .030 4.6 .13 0 unknown .054 4.5 .17  0 true .12  26 1.3  2 timeout 900    4100 9800   0 true 3.1 270 29 2 true .36 59 3.5 2 disqualified 2.4 76 35 0 true .21 18 2.8 2 true 8.2 360 73 2 true 8.6 350 80 2 true 8.5 370 61 2 timeout 900   150 11000 0
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     300 9900    0 error (42) 880     2500   5100    0 error (42) 880     170   11000    0 timeout 900   5000 11000 0 unknown 470    63 6500   0 unknown .046 4.6 .16 0 unknown .036 4.7 .21  0 timeout 900     1500 10000    0 timeout 900    190 9000   0 timeout 900   5100 11000 0 timeout 900    390 6500   0 disqualified 880   840 9300 0 timeout (verification) 900    430 7700   0 true 81   620 1000 2 timeout 900   2100 8300 0 true 60   810 710 2 timeout 900   150 11000 0
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c true .093 24 .84 2 error (42) 880     6800   6300    0 error (42) 880     380   6000    0 true 2.9 270 25 2 unknown .81 66 7.9 0 unknown .032 4.6 .19 0 unknown .055 4.5 .20  0 timeout 900     890 13000    0 timeout 900    74 10000   0 true 2.9 260 26 2 timeout 900    420 6300   0 disqualified 2.4 74 29 0 true .16 17 1.6 2 true 6.8 320 55 2 true 6.6 320 53 2 true 7.4 360 58 2 timeout 900   150 10000 0
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1300 12000    0 error (42) 880     4100   4500    0 error (42) 880     110   10000    0 timeout 910   2500 12000 0 unknown 43    40 540   0 unknown .028 4.6 .14 0 unknown .027 4.6 .19  0 timeout 900     560 10000    0 timeout 900    75 9700   0 timeout 900   2300 11000 0 timeout 900    420 4600   0 disqualified 880   390 9600 0 timeout (verification) 900    430 11000   0 true 8.4 360 70 2 true 8.6 370 74 2 true 7.7 360 69 2 timeout 900   150 10000 0
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1400 12000    0 error (42) 880     4500   4800    0 error (42) 880     120   11000    0 true 3.0 270 29 2 unknown 42    40 530   0 unknown .026 4.6 .23 0 unknown .034 4.7 .27  0 timeout 900     480 11000    0 timeout 900    74 10000   0 true 3.0 270 28 2 timeout 900    390 3700   0 disqualified 880   730 9600 0 timeout (verification) 900    250 13000   0 true 8.1 350 59 2 true 9.1 370 56 2 true 7.5 330 59 2 timeout 900   150 11000 0
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true .10  24 .78 2 error (42) 880     3200   5000    0 error (42) 880     220   10000    0 true 3.0 270 26 2 unknown .81 66 9.0 0 unknown .043 4.6 .17 0 unknown .032 4.6 .19  0 timeout 900     930 11000    0 timeout 900    75 11000   0 true 2.9 270 27 2 timeout 900    440 4600   0 disqualified 880   700 9200 0 timeout (verification) 900    520 8900   0 true 8.6 350 66 2 true 9.9 450 93 2 true 8.3 350 67 2 timeout 900   150 13000 0
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c true .099 24 .99 2 error (42) 880     3600   6500    0 error (42) 870     350   11000    0 true 3.1 280 27 2 unknown .82 67 8.8 0 unknown .029 4.6 .20 0 unknown .027 4.6 .20  0 timeout 900     780 11000    0 timeout 900    74 8800   0 true 3.1 280 26 2 timeout 900    1900 6100   0 disqualified 880   2200 12000 0 timeout (verification) 900    680 10000   0 true 7.2 350 56 2 true 9.0 380 77 2 true 7.2 340 55 2 error (1) 51   150 580 0
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c true 7.2   270 85    1 out of memory 52     13000   710    0 error (42) 880     13000   11000    0 true 3.2 270 31 1 unknown .82 66 7.9 0 unknown .031 4.7 .20 0 unknown .038 4.6 .22  0 timeout 900     15000 11000    0 timeout 900    4300 7800   0 true 3.1 270 29 1 timeout 900    14000 9600   0 disqualified 880   1700 7300 0 timeout (verification) 900    2700 6200   0 timeout 900   990 10000 0 timeout 900   4800 10000 0 timeout 900   1100 11000 0 timeout 900   150 11000 0
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c error (134) .16  24 1.7  0 out of memory 55     13000   680    0 error (134) .059 15   .52 0 timeout 910   6800 12000 0 unknown 52    60 770   0 unknown .034 4.7 .16 0 unknown .029 4.9 .23  0 timeout 900     5900 13000    0 timeout 900    4400 5600   0 timeout 900   6700 11000 0 timeout 900    14000 9300   0 disqualified 880   1700 5600 0 error(unknown, verification-finished) 740    2500 6400   0 timeout 900   1000 13000 0 timeout 900   5500 9800 0 timeout 900   890 14000 0 error (1) 4.0 200 39 0
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true .12  24 .83 2 out of memory 180     15000   2200    0 out of memory 140     15000   1800    0 true 3.0 270 27 2 unknown .84 66 8.9 0 unknown .028 4.6 .22 0 unknown .025 4.6 .022 0 timeout 900     15000 13000    0 timeout 900    74 7600   0 true 2.8 270 25 2 out of memory 840    15000 11000   0 disqualified 2.3 74 31 0 true .14 15 1.5 2 true 7.0 340 57 2 true 7.4 350 53 2 true 8.0 370 64 2 error (1) 51   160 660 0
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1500 12000    0 error (42) 880     1400   7600    0 error (42) 870     4100   11000    0 timeout 900   560 12000 0 unknown 510    67 5500   0 unknown .029 4.7 .19 0 unknown .030 4.6 .17  0 timeout 900     160 11000    0 timeout 900    75 10000   0 timeout 900   570 14000 0 out of memory 43    15000 610   0 disqualified 880   370 10000 0 timeout (verification) 900    280 12000   0 timeout 900   1900 13000 0 timeout 900   3600 8300 0 timeout 900   1400 12000 0 timeout 900   150 9900 0
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .12  24 .57 0 error (42) 880     1600   3700    0 error (42) 870     5900   13000    0 true 3.4 280 28 2 out of memory 170    15000 2500   0 unknown .037 4.5 .17 0 unknown .028 4.6 .17  0 timeout 900     6400 6900    0 timeout 900    320 14000   0 true 3.4 280 30 2 out of memory 43    15000 660   0 disqualified 880   180 9700 0 timeout (verification) 900    290 12000   0 true 11   380 84 2 true 9.7 410 71 2 true 9.9 400 73 2 timeout 900   150 12000 0
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     660 7400    0 error (42) 880     3100   3100    0 error (42) 880     170   11000    0 true 3.3 270 34 1 unknown 470    83 5900   0 unknown .030 4.6 .19 0 unknown .051 4.6 .18  0 timeout 900     1200 13000    0 timeout 900    76 10000   0 true 3.4 280 37 1 timeout 900    390 4800   0 disqualified 880   770 9200 0 timeout (verification) 900    440 8100   0 true 12   550 100 2 true 24   640 260 2 true 19   510 180 2 timeout 900   150 9600 0
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c error (5) .088 24 .83 0 error (42) 880     220   3700    0 error (42) 880     5000   11000    0 true 4.6 290 39 2 out of memory 180    15000 2500   0 unknown .026 4.7 .20 0 unknown .051 4.6 .27  0 timeout 900     12000 7700    0 timeout 900    780 12000   0 true 4.5 300 48 2 out of memory 40    15000 570   0 disqualified 890   240 10000 0 timeout (verification) 900    520 12000   0 true 12   510 91 2 timeout 900   1000 10000 0 true 13   550 110 2 timeout 900   460 10000 0
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .086 24 .79 0 error (42) 880     220   2900    0 error (42) 880     5000   11000    0 true 4.4 300 41 2 out of memory 180    15000 2100   0 unknown .033 4.6 .19 0 unknown .029 4.6 .23  0 timeout 900     12000 6200    0 timeout 900    280 10000   0 true 4.5 300 41 2 out of memory 42    15000 620   0 disqualified 890   200 11000 0 timeout (verification) 900    280 11000   0 true 21   730 170 2 timeout 900   1100 11000 0 true 20   640 180 2 timeout 900   200 13000 0
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .088 24 .96 0 error (42) 880     460   3600    0 error (42) 880     500   7200    0 timeout 900   1200 14000 0 out of memory 160    15000 2000   0 unknown .054 4.6 .16 0 unknown .052 4.6 .19  0 timeout 900     4900 5200    0 timeout 900    420 12000   0 timeout 900   1200 10000 0 out of memory 320    15000 3800   0 disqualified 880   350 7700 0 timeout (verification) 900    620 12000   0 true 16   570 120 2 timeout 900   1100 9500 0 true 19   660 150 2 timeout 900   200 12000 0
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .085 24 .81 0 error (42) 880     320   3500    0 error (42) 880     340   5600    0 true 3.7 290 34 2 out of memory 170    15000 2000   0 unknown .032 4.6 .19 0 unknown .026 4.6 .28  0 timeout 900     4800 4700    0 timeout 900    450 9800   0 true 3.9 290 41 2 out of memory 250    15000 3300   0 disqualified 880   540 7400 0 timeout (verification) 900    500 7600   0 true 13   570 99 2 timeout 900   1200 11000 0 true 13   570 110 2 timeout 900   200 13000 0
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .085 24 .71 0 error (42) 880     460   4500    0 error (42) 880     500   6700    0 timeout 900   1400 10000 0 out of memory 160    15000 2100   0 unknown .031 4.7 .21 0 unknown .037 4.7 .21  0 timeout 900     4800 8100    0 timeout 900    480 9900   0 timeout 900   1800 11000 0 out of memory 320    15000 4100   0 disqualified 880   350 8300 0 timeout (verification) 900    550 8100   0 true 15   550 130 2 timeout 900   1100 10000 0 true 16   570 140 2 timeout 900   200 11000 0
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c error (5) .089 24 .89 0 error (42) 870     860   5300    0 error (42) 880     690   10000    0 timeout 900   4100 11000 0 out of memory 170    15000 2700   0 unknown .029 4.6 .17 0 unknown .031 4.6 .19  0 timeout 900     6000 6000    0 timeout 900    2300 8400   0 timeout 900   4000 10000 0 timeout 900    4600 14000   0 disqualified 880   240 7800 0 timeout (verification) 900    4200 10000   0 true 13   490 120 2 timeout 900   1200 12000 0 true 13   500 110 2 timeout 900   430 13000 0
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .092 24 .78 0 error (42) 880     4200   6800    0 error (42) 870     180   11000    0 timeout 910   4400 12000 0 out of memory 170    15000 2200   0 unknown .031 4.7 .19 0 unknown .027 4.8 .22  0 timeout 900     15000 8700    0 timeout 900    1100 11000   0 timeout 900   4100 11000 0 out of memory 290    15000 3600   0 disqualified 880   480 7900 0 timeout (verification) 900    1000 12000   0 true 17   520 160 2 timeout 900   5200 13000 0 true 36   750 330 2 timeout 900   150 13000 0
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true .10  24 1.2  2 error (42) 880     2300   10000    0 error (42) 880     880   6500    0 true 3.2 270 29 2 unknown .79 67 8.4 0 unknown .034 4.6 .20 0 unknown .027 4.7 .22  0 timeout 900     2200 13000    0 timeout 900    4500 9100   0 true 3.1 270 27 2 timeout 900    880 4400   0 disqualified 2.5 80 33 0 true .17 16 1.9 2 true 8.1 340 61 2 true 8.8 370 72 2 true 8.5 360 66 2 timeout 900   150 12000 0
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c true .098 24 .96 2 error (42) 880     4700   4800    0 error (42) 880     210   10000    0 true 3.0 270 28 2 unknown 1.0  66 11   0 unknown .045 4.6 .17 0 unknown .028 4.6 .21  0 timeout 900     190 10000    0 timeout 900    74 9200   0 true 3.1 270 26 2 timeout 900    3400 3400   0 disqualified 880   3100 9200 0 timeout (verification) 900    17 11000   0 true 9.1 370 72 2 true 8.7 380 80 2 true 9.0 370 71 2 timeout 900   150 11000 0
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true .13  24 .76 2 error (42) 880     1200   8500    0 error (42) 870     8200   13000    0 true 3.0 270 29 2 unknown .79 67 8.7 0 unknown .036 4.6 .17 0 unknown .032 4.6 .19  0 timeout 900     470 11000    0 timeout 900    75 9600   0 true 3.1 270 27 2 timeout 900    520 5000   0 disqualified 880   290 9600 0 timeout (verification) 900    3300 11000   0 true 8.5 360 70 2 true 9.1 380 65 2 true 7.9 350 58 2 timeout 900   150 11000 0
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true .10  24 .79 2 error (42) 880     1200   9700    0 out of memory 850     15000   13000    0 true 3.0 270 25 2 unknown .84 66 7.9 0 unknown .035 4.6 .29 0 unknown .033 4.6 .16  0 timeout 900     500 11000    0 timeout 900    75 10000   0 true 3.0 270 28 2 timeout 900    300 6300   0 disqualified 880   580 9600 0 timeout (verification) 900    440 7600   0 true 8.6 370 66 2 true 9.5 400 85 2 true 8.2 360 68 2 timeout 900   150 11000 0
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true .14  24 .85 2 error (42) 880     1800   9400    0 out of memory 520     15000   6900    0 true 3.0 270 29 2 unknown 1.3  66 18   0 unknown .054 4.6 .25 0 unknown .031 4.6 .22  0 timeout 900     240 12000    0 timeout 900    4500 14000   0 true 3.0 270 27 2 timeout 900    210 4500   0 disqualified 880   350 10000 0 timeout (verification) 900    280 11000   0 true 8.1 370 60 2 true 8.7 360 74 2 true 8.3 370 64 2 timeout 890   150 11000 0
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true .17  25 1.5  2 error (42) 880     4500   4000    0 error (42) 880     160   9800    0 true 3.0 270 29 2 unknown 28    41 360   0 unknown .028 4.8 .21 0 unknown .033 4.6 .20  0 timeout 900     870 11000    0 timeout 900    74 9700   0 true 3.0 270 28 2 timeout 900    380 4600   0 disqualified 880   760 12000 0 timeout (verification) 900    450 10000   0 true 7.7 360 65 2 true 8.2 330 61 2 true 8.4 380 67 2 error (1) 3.9 200 33 0
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true .099 24 .94 2 error (42) 880     2100   7200    0 out of memory 450     15000   5900    0 true 3.2 270 30 2 unknown .89 66 9.0 0 unknown .056 4.5 .16 0 unknown .032 4.6 .21  0 timeout 900     490 14000    0 timeout 900    5000 10000   0 true 3.2 270 31 2 timeout 900    300 7600   0 disqualified 880   410 10000 0 timeout (verification) 900    530 11000   0 true 9.0 360 76 2 true 9.7 400 85 2 true 8.7 380 67 2 timeout 900   150 12000 0
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true .095 24 .84 2 error (42) 880     4800   4300    0 error (42) 880     150   11000    0 true 3.0 270 25 2 unknown .78 67 9.3 0 unknown .031 4.6 .19 0 unknown .031 4.6 .19  0 timeout 900     890 11000    0 timeout 900    75 9400   0 true 3.1 270 28 2 timeout 900    350 4300   0 disqualified 880   640 9300 0 timeout (verification) 900    440 7300   0 true 7.6 350 69 2 true 8.1 370 69 2 true 8.0 370 59 2 timeout 900   150 11000 0
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true .092 23 .78 2 true .056 7.0 .26 2 witness invalid (true) .042 6.1 .29 0 true 2.9 270 29 2 unknown .81 68 8.6 0 unknown .030 4.7 .20 0 unknown .028 4.6 .25  0 true .082 26 .87 2 timeout 900    84 9800   0 true 2.9 270 25 2 true .34 59 3.5 2 disqualified 2.0 66 27 0 true .13 15 1.6 2 true 7.4 360 60 2 true 7.9 360 60 2 true 8.2 350 65 2 timeout 900   150 13000 0
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true .096 24 .81 2 true .053 6.8 .34 1 witness invalid (true) .047 6.1 .24 0 true 2.8 260 25 2 unknown .78 66 8.3 0 unknown .028 4.6 .19 0 unknown .024 4.6 .19  0 out of memory 280     15000 4100    0 timeout 900    75 7000   0 true 2.9 270 27 2 out of memory 60    15000 870   0 disqualified 2.4 74 30 0 true .17 16 1.6 2 true 7.7 370 62 2 true 7.2 360 56 2 true 7.3 340 63 2 error (1) 51   150 640 0
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true .098 24 .88 2 true 1.6   50   21    2 out of memory 180     15000   2800    0 true 3.0 270 29 2 unknown .83 66 8.9 0 unknown .027 4.6 .29 0 unknown .048 4.6 .21  0 true .60  26 9.3  2 timeout 900    2000 9200   0 true 3.0 270 33 2 true .38 59 4.5 2 disqualified 27   170 340 0 true .19 18 2.5 2 true 7.3 340 56 2 true 9.1 350 80 2 true 8.6 370 59 2 timeout 900   150 11000 0
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1700 10000    0 error (42) 880     2300   4300    0 error (42) 880     170   12000    0 timeout 910   13000 11000 0 unknown 58    49 750   0 unknown .034 4.6 .19 0 unknown .026 4.7 .22  0 timeout 900     1100 12000    0 timeout 900    75 11000   0 timeout 910   13000 10000 0 timeout 900    410 4900   0 disqualified 880   790 12000 0 timeout (verification) 900    410 7900   0 timeout 900   3100 12000 0 timeout 900   5700 7300 0 timeout 900   1800 12000 0 timeout 900   150 13000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .077 10   .63 1 false(no-overflow) .12  8.0 .33 1 false(no-overflow) 2.9 270 25 1 false(no-overflow) .19 33 1.8 0 unknown .034 4.8 .27 0 unknown .032 4.6 .18  0 false(no-overflow) .14  26 1.3  1 false(no-overflow) 380    4400 4300   0 false(no-overflow) 3.1 270 31 1 false(no-overflow) .35 59 4.4 1 disqualified 3.3 91 41 0 false(no-overflow) .26 18 2.9 1 false(no-overflow) 8.2 370 69 1 false(no-overflow) 7.8 340 70 1 false(no-overflow) 8.3 370 67 1 false(no-overflow) 110   150 1400 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .10  9.7 1.1  1 false(no-overflow) .067 9.0 .56 1 false(no-overflow) 3.1 270 28 1 false(no-overflow) .22 34 2.8 0 unknown .056 4.6 .13 0 unknown .028 4.6 .18  0 false(no-overflow) .14  26 1.6  1 false(no-overflow) 340    4200 3600   0 false(no-overflow) 3.2 260 32 1 false(no-overflow) .40 59 3.0 1 disqualified 3.4 98 42 0 false(no-overflow) .25 18 2.9 1 false(no-overflow) 8.4 370 69 1 false(no-overflow) 8.1 340 63 1 false(no-overflow) 8.6 360 77 1 false(no-overflow) 140   150 2100 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .079 9.3 .60 1 false(no-overflow) .067 9.2 .38 1 false(no-overflow) 3.0 270 28 1 false(no-overflow) .17 33 2.3 0 unknown .053 4.6 .14 0 unknown .033 4.7 .19  0 false(no-overflow) .11  26 1.3  1 timeout 900    4200 13000   0 false(no-overflow) 3.1 270 31 1 false(no-overflow) .35 59 4.1 1 disqualified 3.2 85 39 0 false(no-overflow) .24 18 3.7 1 false(no-overflow) 7.8 370 60 1 false(no-overflow) 7.5 360 55 1 false(no-overflow) 8.2 360 64 1 false(no-overflow) 200   150 2600 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .12  24 .97 1 false(no-overflow) .075 9.6 .51 1 false(no-overflow) .066 9.7 .59 1 false(no-overflow) 3.0 270 27 1 false(no-overflow) .15 33 1.9 0 unknown .046 4.7 .11 0 unknown .038 4.5 .095 0 false(no-overflow) .11  26 1.2  1 false(no-overflow) 770    4300 10000   0 false(no-overflow) 2.9 270 25 1 false(no-overflow) .37 59 3.5 1 disqualified 3.2 82 50 0 false(no-overflow) .25 19 2.9 1 false(no-overflow) 8.2 370 60 1 false(no-overflow) 7.8 370 64 1 false(no-overflow) 7.5 370 56 1 false(no-overflow) 3.4 150 35 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .13  24 .82 1 false(no-overflow) .084 9.1 .79 1 false(no-overflow) .072 9.2 .50 1 false(no-overflow) 3.1 270 31 1 false(no-overflow) .16 33 1.8 0 unknown .031 4.7 .21 0 unknown .054 4.5 .23  0 false(no-overflow) .10  26 1.1  1 timeout 900    82 8900   0 false(no-overflow) 3.1 270 28 1 false(no-overflow) .37 59 3.2 1 disqualified 3.4 88 42 0 false(no-overflow) .26 18 3.9 1 false(no-overflow) 9.2 380 70 1 false(no-overflow) 8.6 370 80 1 false(no-overflow) 8.8 350 77 1 false(no-overflow) 290   150 4200 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .13  9.4 .43 1 false(no-overflow) .12  8.5 .37 1 false(no-overflow) 3.1 270 27 1 false(no-overflow) .14 33 1.7 0 unknown .028 4.6 .27 0 unknown .035 4.5 .20  0 false(no-overflow) .088 26 .95 1 false(no-overflow) 220    4400 2500   0 false(no-overflow) 3.2 270 29 1 false(no-overflow) .36 59 4.4 1 disqualified 3.2 86 44 0 false(no-overflow) .27 18 3.1 1 false(no-overflow) 7.4 340 67 1 false(no-overflow) 7.6 370 68 1 false(no-overflow) 7.6 370 65 1 timeout 900   150 12000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .081 9.7 .68 1 out of memory 310     15000   4600    0 false(no-overflow) 3.1 270 32 1 false(no-overflow) .14 34 1.4 0 unknown .031 4.6 .21 0 unknown .029 4.6 .20  0 false(no-overflow) .086 26 .85 1 false(no-overflow) 640    4200 7300   0 false(no-overflow) 3.2 270 27 1 timeout 900    360 4900   0 disqualified 3.3 89 37 0 false(no-overflow) .41 18 5.0 1 false(no-overflow) 8.4 360 71 1 false(no-overflow) 9.6 380 73 1 false(no-overflow) 8.1 350 61 1 timeout 900   150 12000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 900     1700 10000    0 error (42) 880     2400   4300    0 error (42) 880     160   10000    0 timeout 910   13000 12000 0 unknown 58    48 810   0 unknown .033 4.6 .11 0 unknown .030 4.8 .23  0 timeout 900     1100 11000    0 timeout 900    74 9300   0 timeout 910   13000 11000 0 timeout 900    420 4500   0 disqualified 880   710 10000 0 timeout (verification) 900    430 11000   0 timeout 900   2500 12000 0 timeout 900   4400 6000 0 timeout 900   2400 14000 0 timeout 900   150 11000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .11  24 .97 1 false(no-overflow) .067 9.9 .70 1 false(no-overflow) .12  7.8 .45 1 false(no-overflow) 3.0 270 32 1 false(no-overflow) .14 34 2.0 0 unknown .054 4.6 .16 0 unknown .029 4.8 .22  0 false(no-overflow) .11  26 .80 1 timeout 900    84 11000   0 false(no-overflow) 3.2 270 30 1 false(no-overflow) .41 59 3.2 1 disqualified 3.2 84 36 0 false(no-overflow) .24 18 2.5 1 false(no-overflow) 7.6 360 63 1 false(no-overflow) 8.9 370 68 1 false(no-overflow) 7.6 350 65 1 false(no-overflow) 6.2 150 81 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .12  23 1.0  1 false(no-overflow) .062 9.3 .62 1 false(no-overflow) .067 9.0 .46 1 false(no-overflow) 3.0 270 27 1 false(no-overflow) .13 33 1.5 0 unknown .048 4.8 .19 0 unknown .032 4.6 .21  0 false(no-overflow) .10  26 .65 1 timeout 900    75 11000   0 false(no-overflow) 2.9 270 30 1 false(no-overflow) .37 59 3.3 1 disqualified 3.0 80 38 0 false(no-overflow) .23 18 2.6 1 false(no-overflow) 8.5 370 71 1 false(no-overflow) 8.3 370 67 1 false(no-overflow) 8.1 370 70 1 false(no-overflow) 54   150 720 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 900     2400 6000    0 error (42) 880     1500   5900    0 out of memory 210     15000   3400    0 timeout 910   6600 10000 0 unknown 900    710 11000   0 unknown .030 4.6 .19 0 unknown .046 4.7 .22  0 timeout 900     1100 10000    0 timeout 900    74 8400   0 timeout 910   6600 13000 0 timeout 900    410 3700   0 disqualified 880   440 9000 0 timeout (verification) 900    1200 12000   0 timeout 900   1300 12000 0 timeout 900   1800 6800 0 timeout 900   1300 12000 0 timeout 900   150 11000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 900     960 11000    0 error (42) 880     1300   9300    0 out of memory 330     15000   4200    0 timeout 910   620 12000 0 unknown 720    75 10000   0 unknown .043 4.6 .19 0 unknown .027 4.6 .24  0 timeout 900     130 13000    0 timeout 900    4200 7700   0 timeout 910   500 12000 0 timeout 900    540 8000   0 disqualified 880   180 11000 0 timeout (verification) 900    3100 9100   0 timeout 900   8200 11000 0 timeout 900   3300 5900 0 timeout 900   7500 9300 0 timeout 900   150 12000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .12  24 1.6  1 false(no-overflow) .069 9.8 .61 1 false(no-overflow) .061 9.3 .42 1 false(no-overflow) 3.3 280 32 1 false(no-overflow) .14 33 1.7 0 unknown .030 4.6 .19 0 unknown .027 4.6 .27  0 false(no-overflow) .088 26 .91 1 false(no-overflow) 110    5000 1300   0 false(no-overflow) 3.3 280 28 1 false(no-overflow) .37 59 3.0 1 disqualified 3.1 80 41 0 false(no-overflow) .22 19 2.5 1 false(no-overflow) 8.1 370 65 1 false(no-overflow) 8.1 360 60 1 false(no-overflow) 7.2 340 54 1 false(no-overflow) 13   150 170 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .12  24 .97 1 false(no-overflow) .071 9.6 .63 1 false(no-overflow) .068 8.9 .52 1 false(no-overflow) 3.1 270 32 1 false(no-overflow) .15 34 1.8 0 unknown .034 4.6 .22 0 unknown .046 4.6 .17  0 false(no-overflow) .11  26 1.5  1 timeout 900    83 9700   0 false(no-overflow) 3.2 270 31 1 false(no-overflow) .38 59 3.5 1 disqualified 3.1 83 38 0 false(no-overflow) .27 18 2.8 1 false(no-overflow) 7.5 360 61 1 false(no-overflow) 7.7 360 61 1 false(no-overflow) 8.1 360 59 1 timeout 900   150 12000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .11  24 1.0  1 false(no-overflow) .14  8.9 .48 1 false(no-overflow) .071 10   .47 1 false(no-overflow) 3.1 270 26 1 false(no-overflow) .15 33 1.5 0 unknown .033 4.6 .23 0 unknown .030 4.6 .26  0 false(no-overflow) .11  26 .87 1 timeout 900    83 10000   0 false(no-overflow) 3.1 270 31 1 false(no-overflow) .38 59 3.6 1 disqualified 3.1 84 37 0 false(no-overflow) .23 17 3.4 1 false(no-overflow) 8.2 360 61 1 false(no-overflow) 8.7 350 65 1 false(no-overflow) 7.9 340 58 1 false(no-overflow) 8.7 150 110 1
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .13  24 .99 1 false(no-overflow) .071 9.6 .64 1 error (42) 880     8100   12000    0 false(no-overflow) 3.0 270 33 1 false(no-overflow) .13 34 1.7 0 unknown .037 4.6 .15 0 unknown .033 4.6 .24  0 false(no-overflow) .083 26 .96 1 false(no-overflow) 340    4100 3700   0 false(no-overflow) 3.1 270 30 1 false(no-overflow) .37 58 3.7 1 disqualified 3.2 87 40 0 false(no-overflow) .27 19 2.8 1 false(no-overflow) 7.7 340 59 1 false(no-overflow) 7.6 340 59 1 false(no-overflow) 7.7 350 60 1 false(no-overflow) 3.5 200 36 1
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .15  24 1.2  1 false(no-overflow) .079 9.5 .73 1 false(no-overflow) .070 9.0 .44 1 false(no-overflow) 3.1 270 28 1 false(no-overflow) .16 34 1.9 0 unknown .055 4.6 .18 0 unknown .054 4.6 .16  0 false(no-overflow) .12  26 .97 1 false(no-overflow) 570    190 8500   0 false(no-overflow) 3.0 270 29 1 false(no-overflow) .37 59 3.2 1 disqualified 3.2 90 39 0 false(no-overflow) .23 18 3.1 1 false(no-overflow) 8.2 380 58 1 false(no-overflow) 7.9 370 69 1 false(no-overflow) 8.8 370 67 1 false(no-overflow) 3.8 150 37 1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .14  24 1.4  1 false(no-overflow) .16  15   1.1  1 false(no-overflow) .071 9.1 .46 1 false(no-overflow) 3.1 280 26 1 false(no-overflow) .32 35 4.3 0 unknown .053 4.6 .14 0 unknown .050 4.6 .16  0 false(no-overflow) .25  27 2.9  1 false(no-overflow) .40 83 4.9 0 false(no-overflow) 3.0 270 27 1 false(no-overflow) .38 59 3.2 1 disqualified 3.5 90 43 0 false(no-overflow) .26 18 2.9 1 false(no-overflow) 6.8 360 60 1 false(no-overflow) 7.6 360 59 1 false(no-overflow) 7.4 370 61 1 false(no-overflow) 3.7 150 36 1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .13  24 1.0  1 false(no-overflow) .091 9.4 .48 1 false(no-overflow) .10  8.6 .41 1 false(no-overflow) 3.1 270 26 1 false(no-overflow) .16 34 1.9 0 unknown .029 4.6 .18 0 unknown .031 4.6 .20  0 false(no-overflow) .11  26 1.1  1 false(no-overflow) 570    4200 8600   0 false(no-overflow) 3.1 270 30 1 false(no-overflow) .39 59 3.6 1 disqualified 3.3 87 42 0 false(no-overflow) .24 18 2.7 1 false(no-overflow) 8.0 360 58 1 false(no-overflow) 7.4 350 58 1 false(no-overflow) 7.6 330 64 1 timeout 900   150 13000 0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .16  24 1.1  1 false(no-overflow) .098 9.7 .41 1 false(no-overflow) .076 9.1 .48 1 false(no-overflow) 2.9 270 27 1 false(no-overflow) .17 33 1.9 0 unknown .029 4.6 .24 0 unknown .028 4.5 .19  0 false(no-overflow) .11  26 1.2  1 timeout 900    3900 14000   0 false(no-overflow) 3.0 270 27 1 false(no-overflow) .38 59 3.8 1 disqualified 3.2 85 38 0 false(no-overflow) .23 18 2.8 1 false(no-overflow) 7.6 350 65 1 false(no-overflow) 7.7 350 60 1 false(no-overflow) 8.4 370 66 1 false(no-overflow) 200   200 2900 1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .12  24 .97 1 false(no-overflow) .080 9.5 .48 1 false(no-overflow) .055 9.4 .42 1 false(no-overflow) 3.0 270 31 1 false(no-overflow) .15 34 1.9 0 unknown .028 4.6 .20 0 unknown .028 4.6 .16  0 false(no-overflow) .10  26 1.1  1 false(no-overflow) 770    4100 11000   0 false(no-overflow) 2.9 270 26 1 false(no-overflow) .36 59 3.4 1 disqualified 3.2 86 39 0 false(no-overflow) .26 18 3.0 1 false(no-overflow) 7.1 340 53 1 false(no-overflow) 7.0 340 64 1 false(no-overflow) 6.8 330 53 1 false(no-overflow) 3.5 150 39 1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .11  9.7 .66 1 false(no-overflow) .093 9.4 .36 1 false(no-overflow) 3.1 270 27 1 false(no-overflow) .19 34 1.9 0 unknown .056 4.7 .15 0 unknown .030 4.7 .20  0 false(no-overflow) .11  26 1.0  1 false(no-overflow) 190    79 2700   0 false(no-overflow) 3.1 270 29 1 false(no-overflow) .36 59 3.9 1 disqualified 3.3 86 45 0 false(no-overflow) .27 18 3.6 1 false(no-overflow) 8.3 380 61 1 false(no-overflow) 8.2 380 73 1 false(no-overflow) 7.3 340 55 1 false(no-overflow) 8.7 200 100 1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .17  24 .91 1 false(no-overflow) .14  9.3 .56 1 false(no-overflow) .065 9.4 .67 1 false(no-overflow) 3.0 260 33 1 false(no-overflow) .16 34 2.1 0 unknown .029 4.6 .13 0 unknown .028 4.6 .15  0 false(no-overflow) .11  26 1.2  1 false(no-overflow) .41 82 4.5 0 false(no-overflow) 3.1 270 26 1 false(no-overflow) .37 59 3.0 1 disqualified 3.3 91 37 0 false(no-overflow) .24 18 3.4 1 false(no-overflow) 7.2 350 56 1 false(no-overflow) 6.9 330 54 1 false(no-overflow) 7.2 340 53 1 false(no-overflow) 3.7 150 41 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .12  24 .88 1 false(no-overflow) .13  8.7 .43 1 false(no-overflow) .068 8.9 .47 1 false(no-overflow) 3.1 270 33 1 false(no-overflow) .14 33 1.5 0 unknown .031 4.6 .16 0 unknown .036 4.6 .24  0 false(no-overflow) .080 26 .93 1 false(no-overflow) .43 80 5.2 0 false(no-overflow) 3.1 270 26 1 false(no-overflow) .36 59 3.9 1 disqualified 3.1 82 37 0 false(no-overflow) .23 18 3.0 1 false(no-overflow) 8.2 370 57 1 false(no-overflow) 8.3 370 60 1 false(no-overflow) 8.2 370 63 1 false(no-overflow) 3.5 150 39 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .13  23 1.0  1 false(no-overflow) .15  8.6 .39 1 false(no-overflow) .069 8.9 .43 1 false(no-overflow) 3.0 270 26 1 false(no-overflow) .15 33 2.2 0 unknown .031 4.8 .18 0 unknown .035 4.6 .19  0 false(no-overflow) .085 26 .96 1 false(no-overflow) 72    88 980   0 false(no-overflow) 3.1 270 25 1 false(no-overflow) .38 59 3.0 1 disqualified 3.1 83 38 0 false(no-overflow) .23 17 2.9 1 false(no-overflow) 7.6 360 57 1 false(no-overflow) 8.0 350 68 1 false(no-overflow) 8.2 360 57 1 false(no-overflow) 3.5 150 43 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .12  24 1.2  1 false(no-overflow) .082 9.4 .54 1 false(no-overflow) .071 9.2 .44 1 false(no-overflow) 3.2 280 33 1 false(no-overflow) .13 33 1.6 0 unknown .057 4.6 .11 0 unknown .047 4.6 .16  0 false(no-overflow) .11  26 .83 1 false(no-overflow) 15    81 210   0 false(no-overflow) 3.1 290 29 1 false(no-overflow) .36 59 3.7 1 disqualified 3.1 83 39 0 false(no-overflow) .23 17 2.7 1 false(no-overflow) 8.4 370 69 1 false(no-overflow) 7.4 350 61 1 false(no-overflow) 8.2 360 59 1 false(no-overflow) 3.4 150 41 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .12  24 .93 1 false(no-overflow) .080 9.7 .46 1 false(no-overflow) .075 9.6 .43 1 false(no-overflow) 3.4 280 29 1 false(no-overflow) .14 33 1.3 0 unknown .029 4.6 .12 0 unknown .030 4.6 .18  0 false(no-overflow) .079 26 .83 1 false(no-overflow) .41 83 4.3 0 false(no-overflow) 3.3 280 31 1 false(no-overflow) .37 59 3.1 1 disqualified 3.1 79 37 0 false(no-overflow) .22 18 2.5 1 false(no-overflow) 8.1 370 55 1 false(no-overflow) 7.5 360 64 1 false(no-overflow) 6.6 320 56 1 false(no-overflow) 3.6 150 35 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .13  24 .97 1 false(no-overflow) .096 8.6 .38 1 false(no-overflow) .067 9.2 .46 1 false(no-overflow) 3.3 280 30 1 false(no-overflow) .13 34 1.7 0 unknown .030 4.6 .14 0 unknown .027 4.6 .23  0 false(no-overflow) .080 26 .85 1 false(no-overflow) .42 84 4.4 0 false(no-overflow) 3.2 280 30 1 false(no-overflow) .37 59 3.1 1 disqualified 3.0 79 51 0 false(no-overflow) .22 18 2.5 1 false(no-overflow) 8.0 370 56 1 false(no-overflow) 7.4 350 61 1 false(no-overflow) 7.7 360 58 1 false(no-overflow) 3.5 150 36 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .064 9.5 .71 1 false(no-overflow) .085 8.9 .40 1 false(no-overflow) 3.0 270 26 1 false(no-overflow) .14 33 1.6 0 unknown .044 4.6 .24 0 unknown .029 4.6 .24  0 false(no-overflow) .082 26 .94 1 false(no-overflow) .39 83 4.8 0 false(no-overflow) 3.1 270 29 1 false(no-overflow) .35 59 3.3 1 disqualified 3.1 110 43 0 false(no-overflow) .23 18 2.6 1 false(no-overflow) 7.5 350 64 1 false(no-overflow) 6.7 330 56 1 false(no-overflow) 7.4 360 61 1 false(no-overflow) 3.5 150 33 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .072 10   .51 1 false(no-overflow) .15  7.8 .35 1 false(no-overflow) 3.0 270 28 1 false(no-overflow) .14 33 1.7 0 unknown .026 4.6 .21 0 unknown .029 4.7 .17  0 false(no-overflow) .078 26 .94 1 false(no-overflow) .41 79 5.6 0 false(no-overflow) 2.9 280 28 1 false(no-overflow) .37 59 3.1 1 disqualified 3.1 110 36 0 false(no-overflow) .24 23 3.0 1 false(no-overflow) 8.1 380 67 1 false(no-overflow) 7.4 330 56 1 false(no-overflow) 7.3 340 58 1 false(no-overflow) 3.5 150 41 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .068 9.1 .57 1 false(no-overflow) .077 8.3 .48 1 false(no-overflow) 3.0 270 26 1 false(no-overflow) .14 33 1.8 0 unknown .030 4.6 .18 0 unknown .048 4.7 .23  0 false(no-overflow) .089 26 .87 1 false(no-overflow) .39 79 5.2 0 false(no-overflow) 3.0 270 31 1 false(no-overflow) .36 59 3.5 1 disqualified 3.1 83 41 0 false(no-overflow) .23 18 3.2 1 false(no-overflow) 8.1 360 60 1 false(no-overflow) 7.6 350 49 1 false(no-overflow) 7.9 370 57 1 false(no-overflow) 6.3 150 82 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .13  24 1.2  1 false(no-overflow) .064 9.3 .56 1 false(no-overflow) .070 9.2 .51 1 false(no-overflow) 3.1 270 29 1 false(no-overflow) .14 33 2.0 0 unknown .050 4.6 .27 0 unknown .026 4.6 .28  0 false(no-overflow) .099 26 1.1  1 timeout 900    160 13000   0 false(no-overflow) 2.9 270 27 1 false(no-overflow) .36 58 3.6 1 disqualified 3.2 82 44 0 false(no-overflow) .23 18 3.0 1 false(no-overflow) 7.4 350 57 1 false(no-overflow) 7.8 360 61 1 false(no-overflow) 7.6 360 59 1 false(no-overflow) 9.5 150 100 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .13  23 .80 1 false(no-overflow) .071 9.3 .50 1 false(no-overflow) .064 8.6 .53 1 false(no-overflow) 3.0 270 32 1 false(no-overflow) .13 33 1.8 0 unknown .057 4.7 .17 0 unknown .028 4.6 .24  0 false(no-overflow) .095 26 .94 1 timeout 900    84 12000   0 false(no-overflow) 2.9 270 31 1 false(no-overflow) .37 59 2.9 1 disqualified 3.1 80 36 0 false(no-overflow) .23 18 2.7 1 false(no-overflow) 7.8 370 63 1 false(no-overflow) 8.2 370 60 1 false(no-overflow) 8.0 370 57 1 timeout 900   150 13000 0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .13  24 1.0  1 false(no-overflow) .080 9.7 .89 1 false(no-overflow) .072 8.9 .43 1 false(no-overflow) 3.0 270 27 1 false(no-overflow) .16 33 2.0 0 unknown .045 4.6 .14 0 unknown .027 4.6 .27  0 false(no-overflow) .12  26 1.0  1 false(no-overflow) .41 82 4.8 0 false(no-overflow) 3.0 270 27 1 false(no-overflow) .37 58 3.1 1 disqualified 3.3 82 43 0 false(no-overflow) .22 17 2.6 1 false(no-overflow) 7.9 370 67 1 false(no-overflow) 7.4 330 53 1 false(no-overflow) 7.9 350 55 1 false(no-overflow) 3.5 150 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .13  24 .92 1 false(no-overflow) .074 9.6 .53 1 false(no-overflow) .067 9.1 .53 1 false(no-overflow) 3.3 280 31 1 false(no-overflow) .14 33 1.5 0 unknown .038 4.6 .17 0 unknown .043 4.7 .17  0 false(no-overflow) .085 26 .97 1 false(no-overflow) .43 85 5.6 0 false(no-overflow) 3.3 280 31 1 false(no-overflow) .34 58 4.2 1 disqualified 3.1 84 45 0 false(no-overflow) .23 18 2.8 1 false(no-overflow) 7.7 350 61 1 false(no-overflow) 6.8 340 57 1 false(no-overflow) 7.6 340 63 1 false(no-overflow) 3.5 150 39 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .13  24 .97 1 false(no-overflow) .070 8.9 .49 1 false(no-overflow) .087 8.8 .46 1 false(no-overflow) 3.2 260 31 1 false(no-overflow) .14 34 1.8 0 unknown .038 4.6 .17 0 unknown .030 4.8 .16  0 false(no-overflow) .10  26 .86 1 false(no-overflow) .43 83 5.1 0 false(no-overflow) 3.1 260 28 1 false(no-overflow) .38 59 3.2 1 disqualified 3.1 83 42 0 false(no-overflow) .23 17 2.5 1 false(no-overflow) 8.0 370 55 1 false(no-overflow) 8.0 370 68 1 false(no-overflow) 7.7 350 57 1 false(no-overflow) 3.6 150 44 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .072 9.3 .57 1 false(no-overflow) .071 9.3 .56 1 false(no-overflow) 3.1 270 29 1 false(no-overflow) .15 33 1.8 0 unknown .027 4.6 .23 0 unknown .029 4.6 .17  0 false(no-overflow) .095 26 1.3  1 false(no-overflow) .44 80 6.2 0 false(no-overflow) 3.0 270 32 1 false(no-overflow) .36 59 3.4 1 disqualified 3.2 86 44 0 false(no-overflow) .25 18 3.3 1 false(no-overflow) 8.7 360 67 1 false(no-overflow) 8.9 350 71 1 false(no-overflow) 8.7 370 68 1 false(no-overflow) 3.4 150 35 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .11  24 1.1  1 false(no-overflow) .068 9.3 .55 1 false(no-overflow) .065 9.6 .49 1 false(no-overflow) 3.1 260 27 1 false(no-overflow) .17 33 1.4 0 unknown .036 4.7 .16 0 unknown .030 4.6 .14  0 false(no-overflow) .084 26 .83 1 timeout 900    200 12000   0 false(no-overflow) 3.1 270 31 1 false(no-overflow) .36 59 3.5 1 disqualified 3.1 83 39 0 false(no-overflow) .27 18 2.7 1 false(no-overflow) 8.6 350 78 1 false(no-overflow) 9.7 410 81 1 false(no-overflow) 8.4 370 64 1 false(no-overflow) 3.5 150 32 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .14  24 1.0  1 false(no-overflow) .092 9.7 .78 1 false(no-overflow) .074 9.1 .47 1 false(no-overflow) 3.0 270 27 1 false(no-overflow) .22 33 2.7 0 unknown .033 4.6 .19 0 unknown .031 4.6 .20  0 false(no-overflow) .16  26 1.9  1 false(no-overflow) .42 83 4.3 0 false(no-overflow) 3.0 270 31 1 false(no-overflow) .37 59 3.4 1 disqualified 3.3 82 34 0 false(no-overflow) .24 18 3.0 1 false(no-overflow) 7.8 370 61 1 false(no-overflow) 7.0 340 55 1 false(no-overflow) 7.9 370 60 1 false(no-overflow) 3.6 150 37 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .11  24 1.2  1 false(no-overflow) .066 9.3 .86 1 false(no-overflow) .069 9.3 .47 1 false(no-overflow) 3.0 270 27 1 false(no-overflow) .16 34 1.9 0 unknown .033 4.7 .29 0 unknown .051 4.7 .16  0 false(no-overflow) .10  26 1.2  1 timeout 900    75 9800   0 false(no-overflow) 3.0 270 31 1 false(no-overflow) .36 59 3.0 1 disqualified 3.1 81 40 0 false(no-overflow) .22 19 2.5 1 false(no-overflow) 6.8 340 61 1 false(no-overflow) 8.1 360 57 1 false(no-overflow) 7.9 370 57 1 false(no-overflow) 6.5 150 74 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .065 9.4 .50 1 false(no-overflow) .13  8.6 .35 1 false(no-overflow) 3.0 270 25 1 false(no-overflow) .17 33 2.1 0 unknown .031 4.7 .12 0 unknown .037 4.6 .23  0 false(no-overflow) .11  26 1.5  1 false(no-overflow) 110    83 1400   0 false(no-overflow) 3.0 270 29 1 false(no-overflow) .36 59 3.5 1 disqualified 3.1 83 39 0 false(no-overflow) .23 20 3.1 1 false(no-overflow) 7.7 340 59 1 false(no-overflow) 7.0 360 52 1 false(no-overflow) 7.7 360 55 1 false(no-overflow) 5.2 150 62 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .13  23 1.0  1 false(no-overflow) .12  9.8 .51 1 false(no-overflow) .070 9.8 .48 1 false(no-overflow) 3.1 270 30 1 false(no-overflow) .19 33 2.0 0 unknown .031 4.6 .15 0 unknown .035 4.6 .25  0 false(no-overflow) .11  26 1.1  1 false(no-overflow) .40 83 6.2 0 false(no-overflow) 3.0 270 29 1 false(no-overflow) .41 59 2.9 1 disqualified 3.1 82 38 0 false(no-overflow) .23 18 2.6 1 false(no-overflow) 7.9 350 59 1 false(no-overflow) 7.9 370 58 1 false(no-overflow) 7.3 340 57 1 false(no-overflow) 3.5 150 33 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .12  24 .89 1 false(no-overflow) .079 10   .45 1 false(no-overflow) .12  8.5 .32 1 false(no-overflow) 3.1 270 25 1 false(no-overflow) .14 34 1.5 0 unknown .028 4.6 .18 0 unknown .032 4.7 .28  0 false(no-overflow) .11  26 .83 1 false(no-overflow) .39 82 5.6 0 false(no-overflow) 3.0 270 28 1 false(no-overflow) .36 59 3.4 1 disqualified 3.1 76 39 0 false(no-overflow) .22 18 2.8 1 false(no-overflow) 7.7 370 61 1 false(no-overflow) 7.8 370 54 1 false(no-overflow) 7.9 370 63 1 false(no-overflow) 11   150 120 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .11  24 1.0  1 false(no-overflow) .11  9.3 .34 1 false(no-overflow) .064 9.7 .62 1 false(no-overflow) 3.0 270 28 1 false(no-overflow) .13 33 1.7 0 unknown .044 4.6 .15 0 unknown .030 4.8 .33  0 false(no-overflow) .081 26 .80 1 timeout 900    78 11000   0 false(no-overflow) 3.0 270 28 1 false(no-overflow) .35 59 4.8 1 disqualified 3.0 77 40 0 false(no-overflow) .22 17 2.5 1 false(no-overflow) 7.4 350 64 1 false(no-overflow) 7.1 340 57 1 false(no-overflow) 7.1 340 55 1 false(no-overflow) 55   150 650 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .15  23 .94 1 false(no-overflow) .061 10   .57 1 false(no-overflow) .060 9.6 .62 1 false(no-overflow) 3.0 270 29 1 false(no-overflow) .13 33 1.7 0 unknown .028 4.7 .18 0 unknown .036 4.6 .22  0 false(no-overflow) .083 26 .88 1 false(no-overflow) 250    77 2800   0 false(no-overflow) 2.9 270 28 1 false(no-overflow) .36 59 3.0 1 disqualified 3.1 110 38 0 false(no-overflow) .23 18 3.4 1 false(no-overflow) 7.0 360 55 1 false(no-overflow) 7.7 370 66 1 false(no-overflow) 7.2 340 59 1 error (1) 51   150 590 0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .12  24 .89 1 false(no-overflow) .12  8.9 .37 1 false(no-overflow) .078 9.2 .43 1 false(no-overflow) 2.9 270 27 1 false(no-overflow) .14 33 1.7 0 unknown .027 4.6 .24 0 unknown .059 4.6 .25  0 false(no-overflow) .092 26 .91 1 false(no-overflow) 3.1  79 40   0 false(no-overflow) 2.9 270 30 1 false(no-overflow) .36 59 3.4 1 disqualified 3.1 84 46 0 false(no-overflow) .24 18 2.9 1 false(no-overflow) 7.5 340 58 1 false(no-overflow) 7.8 370 67 1 false(no-overflow) 7.0 340 55 1 false(no-overflow) 3.7 150 42 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .12  24 .96 1 false(no-overflow) .062 10   .68 1 false(no-overflow) .059 9.8 .57 1 false(no-overflow) 2.8 270 28 1 false(no-overflow) .17 34 1.7 0 unknown .034 4.6 .21 0 unknown .029 4.7 .19  0 false(no-overflow) .12  26 .98 1 false(no-overflow) .42 79 5.6 0 false(no-overflow) 2.9 270 28 1 false(no-overflow) .38 58 3.8 1 disqualified 3.2 81 41 0 false(no-overflow) .23 19 2.9 1 false(no-overflow) 7.8 360 60 1 false(no-overflow) 8.3 370 64 1 false(no-overflow) 7.9 360 58 1 false(no-overflow) 14   150 170 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .11  24 .99 1 false(no-overflow) .080 9.8 .38 1 false(no-overflow) .066 9.2 .46 1 false(no-overflow) 3.1 270 28 1 false(no-overflow) .15 34 1.5 0 unknown .034 4.6 .18 0 unknown .028 4.6 .21  0 false(no-overflow) .11  26 .96 1 timeout 900    78 11000   0 false(no-overflow) 3.0 270 27 1 false(no-overflow) .38 59 3.1 1 disqualified 3.1 82 37 0 false(no-overflow) .25 18 2.6 1 false(no-overflow) 7.2 330 52 1 false(no-overflow) 7.3 350 50 1 false(no-overflow) 6.8 340 57 1 false(no-overflow) 96   150 1200 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .12  24 .95 1 false(no-overflow) .071 9.5 .41 1 false(no-overflow) .073 9.1 .41 1 false(no-overflow) 3.1 270 27 1 false(no-overflow) .13 33 1.8 0 unknown .057 4.6 .18 0 unknown .036 4.8 .21  0 false(no-overflow) .084 26 .94 1 timeout 900    4300 9800   0 false(no-overflow) 2.9 260 29 1 false(no-overflow) .37 59 2.9 1 disqualified 3.1 82 40 0 false(no-overflow) .24 18 2.7 1 false(no-overflow) 7.6 350 60 1 false(no-overflow) 7.6 340 60 1 false(no-overflow) 8.3 370 63 1 timeout 900   150 11000 0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .12  24 .97 1 false(no-overflow) .068 9.3 .59 1 false(no-overflow) .062 9.2 .47 1 false(no-overflow) 3.0 270 28 1 false(no-overflow) .14 33 1.6 0 unknown .036 4.6 .24 0 unknown .031 4.6 .21  0 false(no-overflow) .10  26 .80 1 false(no-overflow) .40 82 4.2 0 false(no-overflow) 3.0 270 31 1 false(no-overflow) .38 59 3.7 1 disqualified 3.1 82 34 0 false(no-overflow) .27 23 2.4 1 false(no-overflow) 6.6 330 57 1 false(no-overflow) 7.9 370 56 1 false(no-overflow) 7.6 360 60 1 false(no-overflow) 3.4 150 32 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .12  24 .95 1 false(no-overflow) .072 9.5 .50 1 false(no-overflow) .080 9.0 .42 1 false(no-overflow) 3.0 270 31 1 false(no-overflow) .15 33 1.9 0 unknown .053 4.6 .15 0 unknown .028 4.6 .18  0 false(no-overflow) .11  26 .92 1 false(no-overflow) .39 83 4.2 0 false(no-overflow) 3.1 270 27 1 false(no-overflow) .37 58 3.7 1 disqualified 3.1 85 39 0 false(no-overflow) .25 18 2.9 1 false(no-overflow) 6.6 340 53 1 false(no-overflow) 8.4 360 61 1 false(no-overflow) 7.9 360 57 1 false(no-overflow) 3.6 150 36 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .13  24 .97 1 false(no-overflow) .077 9.5 .54 1 false(no-overflow) .072 9.1 .40 1 false(no-overflow) 3.0 270 25 1 false(no-overflow) .17 34 1.9 0 unknown .040 4.7 .27 0 unknown .029 4.6 .18  0 false(no-overflow) .10  26 1.4  1 false(no-overflow) .40 82 5.8 0 false(no-overflow) 2.9 280 27 1 false(no-overflow) .40 59 3.6 1 disqualified 3.2 87 42 0 false(no-overflow) .23 18 2.4 1 false(no-overflow) 7.7 370 64 1 false(no-overflow) 8.1 370 67 1 false(no-overflow) 8.1 370 57 1 false(no-overflow) 3.6 200 39 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .15  24 1.1  1 false(no-overflow) .11  8.2 .42 1 false(no-overflow) .11  9.6 .36 1 false(no-overflow) 3.1 270 29 1 false(no-overflow) .15 34 1.9 0 unknown .031 4.7 .13 0 unknown .027 4.6 .23  0 false(no-overflow) .087 26 .89 1 false(no-overflow) .40 79 5.4 0 false(no-overflow) 3.1 270 26 1 false(no-overflow) .37 59 2.7 1 disqualified 3.2 85 44 0 false(no-overflow) .23 18 3.0 1 false(no-overflow) 7.2 340 57 1 false(no-overflow) 7.6 350 55 1 false(no-overflow) 8.0 370 59 1 false(no-overflow) 3.7 150 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .11  24 1.0  1 false(no-overflow) .072 8.9 .54 1 false(no-overflow) .076 9.6 .40 1 false(no-overflow) 3.0 260 26 1 false(no-overflow) .15 34 1.5 0 unknown .047 4.6 .15 0 unknown .028 4.7 .17  0 false(no-overflow) .081 26 .87 1 false(no-overflow) .41 83 4.5 0 false(no-overflow) 2.9 260 28 1 false(no-overflow) .39 59 3.9 1 disqualified 3.2 85 37 0 false(no-overflow) .23 18 2.8 1 false(no-overflow) 8.4 360 62 1 false(no-overflow) 8.4 370 63 1 false(no-overflow) 8.0 370 69 1 false(no-overflow) 3.8 150 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .068 9.7 .57 1 false(no-overflow) .069 9.2 .44 1 false(no-overflow) 3.1 270 27 1 false(no-overflow) .14 33 2.0 0 unknown .047 4.5 .21 0 unknown .038 4.8 .24  0 false(no-overflow) .086 26 .94 1 false(no-overflow) 530    78 7100   0 false(no-overflow) 3.1 270 29 1 false(no-overflow) .40 59 3.0 1 disqualified 3.2 85 39 0 false(no-overflow) .23 18 2.5 1 false(no-overflow) 7.7 350 62 1 false(no-overflow) 6.6 330 53 1 false(no-overflow) 8.0 360 70 1 false(no-overflow) 180   150 2600 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .096 8.4 .42 1 false(no-overflow) .061 10   .59 1 false(no-overflow) 3.0 270 26 1 false(no-overflow) .14 33 1.4 0 unknown .036 4.7 .19 0 unknown .031 4.6 .16  0 false(no-overflow) .098 26 .87 1 false(no-overflow) 330    100 4800   0 false(no-overflow) 3.0 270 28 1 false(no-overflow) .37 59 3.4 1 disqualified 3.2 82 42 0 false(no-overflow) .22 17 2.6 1 false(no-overflow) 7.1 330 59 1 false(no-overflow) 7.8 360 70 1 false(no-overflow) 7.5 370 59 1 false(no-overflow) 12   150 130 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .12  24 .98 1 false(no-overflow) .097 9.3 .43 1 false(no-overflow) .13  8.9 .34 1 false(no-overflow) 3.3 290 29 1 false(no-overflow) .15 34 1.7 0 unknown .034 4.6 .18 0 unknown .033 4.5 .19  0 false(no-overflow) .11  26 .78 1 false(no-overflow) 270    630 2700   0 false(no-overflow) 3.3 290 27 1 false(no-overflow) .36 59 3.2 1 disqualified 3.1 83 40 0 false(no-overflow) .24 17 2.8 1 false(no-overflow) 7.8 370 55 1 false(no-overflow) 7.8 360 68 1 false(no-overflow) 8.0 360 60 1 false(no-overflow) 3.6 150 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .12  24 .95 1 false(no-overflow) .080 9.5 .54 1 false(no-overflow) .062 9.7 .49 1 false(no-overflow) 3.2 270 31 1 false(no-overflow) .16 33 1.9 0 unknown .033 4.8 .24 0 unknown .027 4.6 .20  0 false(no-overflow) .11  26 .89 1 false(no-overflow) 150    77 2200   0 false(no-overflow) 3.1 270 26 1 false(no-overflow) .38 59 3.3 1 disqualified 3.2 86 39 0 false(no-overflow) .24 19 3.0 1 false(no-overflow) 7.8 360 60 1 false(no-overflow) 8.1 360 61 1 false(no-overflow) 7.2 350 56 1 false(no-overflow) 180   150 2400 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .085 9.5 .57 1 false(no-overflow) .061 9.1 .56 1 false(no-overflow) 2.9 270 26 1 false(no-overflow) .14 34 1.8 0 unknown .039 4.6 .15 0 unknown .046 4.6 .18  0 false(no-overflow) .11  26 .87 1 false(no-overflow) .42 79 4.7 0 false(no-overflow) 3.0 280 27 1 false(no-overflow) .37 59 2.9 1 disqualified 3.2 87 44 0 false(no-overflow) .26 18 2.8 1 false(no-overflow) 7.8 360 56 1 false(no-overflow) 7.7 350 60 1 false(no-overflow) 7.9 370 59 1 false(no-overflow) 3.6 150 38 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .16  24 .81 1 false(no-overflow) .068 9.6 .54 1 false(no-overflow) .064 9.6 .53 1 false(no-overflow) 3.1 270 28 1 false(no-overflow) .14 33 1.6 0 unknown .049 4.6 .21 0 unknown .033 4.6 .29  0 false(no-overflow) .16  26 2.6  1 false(no-overflow) 740    77 9600   0 false(no-overflow) 3.0 270 29 1 false(no-overflow) .36 59 3.3 1 disqualified 3.2 83 48 0 false(no-overflow) .23 18 2.6 1 false(no-overflow) 7.9 360 65 1 false(no-overflow) 8.4 370 56 1 false(no-overflow) 7.6 360 66 1 false(no-overflow) 180   150 2100 1
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .063 9.4 .60 1 false(no-overflow) .074 9.1 .46 1 false(no-overflow) 3.0 270 30 1 false(no-overflow) .17 33 1.7 0 unknown .048 4.6 .19 0 unknown .048 4.6 .16  0 false(no-overflow) .085 26 .89 1 timeout 900    83 9300   0 false(no-overflow) 3.0 270 29 1 false(no-overflow) .39 59 4.4 1 disqualified 3.1 84 42 0 false(no-overflow) .24 18 2.9 1 false(no-overflow) 8.4 370 62 1 false(no-overflow) 8.3 340 61 1 false(no-overflow) 8.3 360 64 1 false(no-overflow) 33   150 440 1
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .13  24 1.0  1 false(no-overflow) .073 8.8 .56 1 false(no-overflow) .064 9.0 .53 1 false(no-overflow) 3.1 270 26 1 false(no-overflow) .16 33 1.6 0 unknown .058 4.6 .15 0 unknown .041 4.7 .22  0 false(no-overflow) .090 26 .99 1 timeout 900    83 11000   0 false(no-overflow) 3.0 270 26 1 false(no-overflow) .37 58 3.2 1 disqualified 3.1 83 34 0 false(no-overflow) .25 18 2.6 1 false(no-overflow) 7.4 340 64 1 false(no-overflow) 7.2 350 61 1 false(no-overflow) 8.1 370 61 1 false(no-overflow) 490   150 5600 1
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .071 9.6 .53 1 false(no-overflow) .059 9.2 .62 1 false(no-overflow) 3.0 270 26 1 false(no-overflow) .14 33 1.7 0 unknown .031 4.6 .26 0 unknown .036 4.6 .12  0 false(no-overflow) .086 26 .98 1 timeout 900    82 12000   0 false(no-overflow) 3.0 270 34 1 false(no-overflow) .36 59 4.0 1 disqualified 3.2 90 44 0 false(no-overflow) .24 19 2.9 1 false(no-overflow) 8.0 360 57 1 false(no-overflow) 7.3 340 55 1 false(no-overflow) 8.2 370 63 1 false(no-overflow) 230   150 3000 1
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .12  8.9 .39 1 false(no-overflow) .077 8.7 .39 1 false(no-overflow) 3.0 260 27 1 false(no-overflow) .14 33 1.7 0 unknown .030 4.7 .23 0 unknown .036 4.6 .24  0 false(no-overflow) .10  26 .94 1 false(no-overflow) 250    670 3300   0 false(no-overflow) 3.1 270 30 1 false(no-overflow) .39 59 3.3 1 disqualified 3.1 83 36 0 false(no-overflow) .22 17 2.6 1 false(no-overflow) 7.5 350 62 1 false(no-overflow) 6.8 340 55 1 false(no-overflow) 6.9 330 62 1 false(no-overflow) 200   150 2200 1
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .12  24 .98 1 false(no-overflow) .14  9.4 .41 1 false(no-overflow) .076 9.1 .36 1 false(no-overflow) 3.2 270 27 1 false(no-overflow) .14 33 2.0 0 unknown .046 4.8 .16 0 unknown .036 4.6 .11  0 false(no-overflow) .084 26 .83 1 false(no-overflow) 330    4100 3800   0 false(no-overflow) 3.1 270 27 1 false(no-overflow) .38 59 3.2 1 disqualified 3.1 96 36 0 false(no-overflow) .27 18 3.3 1 false(no-overflow) 8.3 360 62 1 false(no-overflow) 7.9 340 67 1 false(no-overflow) 8.0 360 59 1 false(no-overflow) 480   150 7100 1
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .14  24 1.1  1 false(no-overflow) .080 9.5 .57 1 false(no-overflow) 110     4500   1300    1 false(no-overflow) 3.6 290 33 1 false(no-overflow) .14 34 1.6 0 unknown .055 4.8 .16 0 unknown .031 4.6 .23  0 false(no-overflow) .082 26 1.0  1 false(no-overflow) 180    78 2000   0 false(no-overflow) 3.6 290 33 1 false(no-overflow) .38 59 3.5 1 disqualified 3.3 86 37 0 false(no-overflow) .24 18 2.9 1 false(no-overflow) 10   390 78 1 false(no-overflow) 13   490 120 1 false(no-overflow) 9.0 380 77 1 timeout 900   150 12000 0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .13  24 1.1  1 false(no-overflow) .088 10   .67 1 false(no-overflow) .075 9.6 .34 1 false(no-overflow) 3.0 270 31 1 false(no-overflow) .17 34 2.2 0 unknown .052 4.7 .12 0 unknown .031 4.6 .24  0 false(no-overflow) .10  26 1.4  1 false(no-overflow) 93    78 1200   0 false(no-overflow) 2.9 270 26 1 false(no-overflow) .37 58 3.8 1 disqualified 3.2 82 37 0 false(no-overflow) .22 18 3.0 1 false(no-overflow) 6.7 330 55 1 false(no-overflow) 7.6 360 63 1 false(no-overflow) 7.2 330 58 1 false(no-overflow) 3.6 150 36 1
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) .25  23 3.0  1 false(no-overflow) .078 9.5 .81 1 error (42) 880     1400   10000    0 false(no-overflow) 3.3 280 29 1 false(no-overflow) .16 33 1.7 0 unknown .034 4.7 .18 0 unknown .036 4.6 .26  0 false(no-overflow) .091 26 .78 0 timeout 900    77 12000   0 false(no-overflow) 3.3 270 31 1 timeout 900    8000 7000   0 disqualified 3.3 90 36 0 false(no-overflow) .29 18 3.4 1 false(no-overflow) 11   450 84 1 false(no-overflow) 11   520 95 1 false(no-overflow) 12   470 79 1 false(no-overflow) 4.2 150 43 1
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .11  24 1.2  1 false(no-overflow) .12  8.9 .42 1 false(no-overflow) .10  8.7 .44 1 false(no-overflow) 3.1 280 29 1 false(no-overflow) .14 34 1.8 0 unknown .052 4.7 .17 0 unknown .032 4.6 .18  0 false(no-overflow) .083 26 1.0  1 false(no-overflow) .41 82 5.9 0 false(no-overflow) 3.2 280 32 1 false(no-overflow) .40 59 3.0 1 disqualified 3.2 84 36 0 false(no-overflow) .23 17 2.6 1 false(no-overflow) 7.6 340 56 1 false(no-overflow) 7.9 360 67 1 false(no-overflow) 7.7 370 54 1 false(no-overflow) 12   150 140 1
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .13  24 .77 1 false(no-overflow) .069 9.1 .61 1 false(no-overflow) .060 9.5 .52 1 false(no-overflow) 3.2 280 32 1 false(no-overflow) .14 33 1.6 0 unknown .051 4.7 .22 0 unknown .058 4.6 .17  0 false(no-overflow) .11  26 .75 1 false(no-overflow) .40 79 4.9 0 false(no-overflow) 3.3 280 34 1 false(no-overflow) .36 59 3.1 1 disqualified 3.1 85 45 0 false(no-overflow) .22 17 2.8 1 false(no-overflow) 8.2 360 61 1 false(no-overflow) 7.3 350 59 1 false(no-overflow) 7.9 370 59 1 false(no-overflow) 13   150 150 1
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c error (5) .081 24 .77 0 false(no-overflow) .078 8.9 .54 1 false(no-overflow) .084 9.0 .34 1 false(no-overflow) 3.3 280 30 1 false(no-overflow) .15 34 1.7 0 unknown .027 4.6 .19 0 unknown .033 4.7 .16  0 false(no-overflow) .097 26 .83 1 false(no-overflow) .41 83 5.0 0 false(no-overflow) 3.4 290 30 1 false(no-overflow) .37 59 3.3 1 disqualified 2.7 74 36 0 false(no-overflow) .26 18 2.7 1 false(no-overflow) 8.7 380 69 1 false(no-overflow) 8.5 350 61 1 false(no-overflow) 8.1 340 62 1 false(no-overflow) 3.7 150 37 1
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c error (5) .083 24 .78 0 false(no-overflow) .083 10   .50 1 false(no-overflow) .066 9.1 .47 1 false(no-overflow) 3.4 290 34 1 false(no-overflow) .16 34 1.5 0 unknown .032 4.6 .21 0 unknown .029 4.6 .23  0 false(no-overflow) .083 26 .89 1 false(no-overflow) .39 83 6.4 0 false(no-overflow) 3.5 290 31 1 false(no-overflow) .35 59 4.1 1 disqualified 2.7 75 34 0 false(no-overflow) .24 18 2.9 1 false(no-overflow) 8.3 350 74 1 false(no-overflow) 8.0 350 63 1 false(no-overflow) 8.1 340 61 1 false(no-overflow) 3.7 150 40 1
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c error (5) .081 24 .82 0 false(no-overflow) .083 9.2 .76 1 false(no-overflow) .12  9.3 .30 1 error 3.8 290 35 0 false(no-overflow) .14 34 1.5 0 unknown .055 4.6 .18 0 unknown .031 4.7 .15  0 false(no-overflow) .10  26 .82 1 false(no-overflow) 48    120 620   0 error 3.9 290 36 0 false(no-overflow) .37 59 3.2 1 disqualified 2.7 76 37 0 false(no-overflow) .28 18 3.1 1 false(no-overflow) 7.3 350 64 1 false(no-overflow) 8.2 370 60 1 false(no-overflow) 7.5 350 49 1 timeout 900   150 11000 0
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c error (5) .091 23 .72 0 false(no-overflow) .075 9.7 .73 1 false(no-overflow) .066 9.2 .64 1 false(no-overflow) 3.3 290 28 1 false(no-overflow) .14 34 1.4 0 unknown .054 4.7 .17 0 unknown .030 4.7 .14  0 false(no-overflow) .10  26 .72 1 false(no-overflow) 59    140 690   0 false(no-overflow) 3.2 290 32 1 false(no-overflow) .37 59 3.2 1 disqualified 2.7 76 36 0 false(no-overflow) .23 18 2.9 1 false(no-overflow) 8.4 360 62 1 false(no-overflow) 7.5 350 54 1 false(no-overflow) 8.1 370 58 1 false(no-overflow) 4.0 150 40 1
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .11  24 1.2  1 false(no-overflow) .074 9.4 .61 1 false(no-overflow) .072 9.0 .45 1 false(no-overflow) 2.9 270 27 1 false(no-overflow) .15 34 1.7 0 unknown .057 4.6 .24 0 unknown .029 4.6 .19  0 false(no-overflow) .089 26 .99 1 timeout 900    78 11000   0 false(no-overflow) 3.0 270 26 1 false(no-overflow) .38 59 3.5 1 disqualified 3.1 83 35 0 false(no-overflow) .23 18 2.7 1 false(no-overflow) 7.2 340 63 1 false(no-overflow) 6.9 330 53 1 false(no-overflow) 7.4 350 53 1 false(no-overflow) 73   150 870 1
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .11  24 .93 1 false(no-overflow) .069 9.5 .46 1 false(no-overflow) .063 9.2 .48 1 false(no-overflow) 2.9 270 28 1 false(no-overflow) .14 34 1.4 0 unknown .055 4.6 .17 0 unknown .030 4.6 .25  0 false(no-overflow) .080 26 .86 1 timeout 900    74 11000   0 false(no-overflow) 3.0 260 28 1 timeout 900    410 4900   0 disqualified 3.1 83 39 0 false(no-overflow) .25 17 2.5 1 false(no-overflow) 7.9 340 54 1 false(no-overflow) 8.0 370 64 1 false(no-overflow) 7.7 340 62 1 false(no-overflow) 73   150 790 1
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .12  24 .93 1 false(no-overflow) .13  9.4 .53 1 false(no-overflow) .15  8.5 .36 1 false(no-overflow) 3.0 270 32 1 false(no-overflow) .15 33 1.5 0 unknown .026 4.6 .24 0 unknown .030 4.6 .19  0 false(no-overflow) .10  26 .84 1 false(no-overflow) .42 80 5.3 0 false(no-overflow) 3.1 270 25 1 false(no-overflow) .35 59 3.9 1 disqualified 3.1 110 36 0 false(no-overflow) .23 18 2.4 1 false(no-overflow) 7.8 360 62 1 false(no-overflow) 8.2 350 59 1 false(no-overflow) 7.5 330 63 1 false(no-overflow) 3.5 150 36 1
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .11  24 .93 1 false(no-overflow) .075 9.6 .45 1 false(no-overflow) .063 9.3 .67 1 false(no-overflow) 3.0 270 25 1 false(no-overflow) .13 33 2.4 0 unknown .033 4.8 .26 0 unknown .031 4.7 .19  0 false(no-overflow) .082 26 .89 1 false(no-overflow) 320    77 3700   0 false(no-overflow) 3.0 270 27 1 false(no-overflow) .36 59 2.7 1 disqualified 3.1 77 44 0 false(no-overflow) .22 19 3.3 1 false(no-overflow) 7.7 360 64 1 false(no-overflow) 6.7 320 56 1 false(no-overflow) 6.9 340 58 1 false(no-overflow) 6.5 150 68 1
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .13  24 .90 1 false(no-overflow) .14  9.8 .58 1 false(no-overflow) .075 9.1 .59 1 false(no-overflow) 3.2 280 34 1 false(no-overflow) .14 34 1.5 0 unknown .023 4.6 .28 0 unknown .052 4.7 .27  0 false(no-overflow) .11  26 .92 1 false(no-overflow) .41 82 4.9 0 false(no-overflow) 3.3 280 29 1 false(no-overflow) .37 58 3.4 1 disqualified 3.1 83 35 0 false(no-overflow) .27 22 2.8 1 false(no-overflow) 7.1 350 60 1 false(no-overflow) 8.0 370 62 1 false(no-overflow) 7.2 360 61 1 false(no-overflow) 3.5 150 33 1
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .12  24 .98 1 false(no-overflow) .064 9.5 .47 1 false(no-overflow) .13  8.0 .32 1 false(no-overflow) 3.0 260 28 1 false(no-overflow) .14 34 1.5 0 unknown .029 4.6 .19 0 unknown .031 4.6 .19  0 false(no-overflow) .12  26 .77 1 false(no-overflow) .39 83 4.5 0 false(no-overflow) 3.1 270 31 1 false(no-overflow) .36 59 3.0 1 disqualified 3.1 84 37 0 false(no-overflow) .23 18 2.8 1 false(no-overflow) 7.9 370 56 1 false(no-overflow) 7.1 340 53 1 false(no-overflow) 8.1 360 61 1 false(no-overflow) 14   200 180 1
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .12  24 1.1  1 false(no-overflow) .077 9.6 .49 1 false(no-overflow) .061 9.0 .47 1 false(no-overflow) 3.0 270 31 1 false(no-overflow) .14 33 1.6 0 unknown .031 4.7 .21 0 unknown .031 4.6 .21  0 false(no-overflow) .10  26 .84 1 timeout 900    78 11000   0 false(no-overflow) 3.0 270 28 1 false(no-overflow) .37 59 3.6 1 disqualified 3.1 84 50 0 false(no-overflow) .24 17 2.7 1 false(no-overflow) 7.6 370 66 1 false(no-overflow) 7.7 340 59 1 false(no-overflow) 8.0 360 63 1 false(no-overflow) 130   150 1600 1
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .077 9.4 .77 1 false(no-overflow) .066 9.6 .70 1 false(no-overflow) 3.0 270 30 1 false(no-overflow) .17 33 1.9 0 unknown .030 4.7 .22 0 unknown .033 4.6 .23  0 false(no-overflow) .12  26 1.3  1 false(no-overflow) .44 83 5.1 0 false(no-overflow) 3.2 280 30 1 false(no-overflow) .35 59 3.8 1 disqualified 3.3 90 40 0 false(no-overflow) .23 18 3.1 1 false(no-overflow) 7.7 350 59 1 false(no-overflow) 8.2 360 60 1 false(no-overflow) 7.5 370 57 1 false(no-overflow) 3.5 150 35 1
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .11  24 .95 1 false(no-overflow) .066 9.5 .56 1 false(no-overflow) .071 9.2 .45 1 false(no-overflow) 3.1 270 27 1 false(no-overflow) .15 33 1.6 0 unknown .031 4.6 .24 0 unknown .035 4.7 .21  0 false(no-overflow) .084 26 .95 1 timeout 900    83 10000   0 false(no-overflow) 3.1 270 32 1 false(no-overflow) .38 59 3.4 1 disqualified 3.1 83 38 0 false(no-overflow) .23 18 2.7 1 false(no-overflow) 7.6 360 58 1 false(no-overflow) 7.9 370 55 1 false(no-overflow) 7.9 360 67 1 false(no-overflow) 360   160 4600 1
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .13  24 .96 1 false(no-overflow) .080 9.4 .51 1 false(no-overflow) .087 8.9 .40 1 false(no-overflow) 3.1 270 27 1 false(no-overflow) .18 34 2.0 0 unknown .038 4.6 .15 0 unknown .054 4.6 .24  0 false(no-overflow) .10  26 1.6  1 false(no-overflow) .39 83 4.7 0 false(no-overflow) 3.1 270 28 1 false(no-overflow) .38 59 2.6 1 disqualified 3.2 83 44 0 false(no-overflow) .24 18 3.3 1 false(no-overflow) 8.9 360 74 1 false(no-overflow) 8.8 370 65 1 false(no-overflow) 8.0 360 66 1 false(no-overflow) 370   200 4300 1
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .11  24 1.1  1 false(no-overflow) .082 9.7 .42 1 error (42) 880     12000   11000    0 false(no-overflow) 3.1 270 29 1 false(no-overflow) .14 33 2.0 0 unknown .038 4.8 .25 0 unknown .051 4.6 .31  0 false(no-overflow) .10  26 .84 1 false(no-overflow) 140    4600 1400   0 false(no-overflow) 3.0 270 29 1 timeout 900    430 4800   0 disqualified 3.2 86 44 0 false(no-overflow) .27 18 3.0 1 false(no-overflow) 8.3 360 64 1 false(no-overflow) 10   380 78 1 false(no-overflow) 8.7 360 69 1 timeout 900   150 12000 0
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) .13  24 .89 1 false(no-overflow) .085 9.7 .72 1 error (42) 880     13000   12000    0 false(no-overflow) 3.1 270 29 1 false(no-overflow) .15 33 1.4 0 unknown .044 4.6 .14 0 unknown .043 4.6 .14  0 false(no-overflow) .083 26 .85 1 false(no-overflow) 140    4900 1600   0 false(no-overflow) 3.0 270 25 1 timeout 900    450 6100   0 disqualified 3.1 84 38 0 false(no-overflow) .26 18 3.1 1 false(no-overflow) 8.4 380 72 1 false(no-overflow) 9.9 380 86 1 false(no-overflow) 7.7 340 72 1 timeout 900   150 13000 0
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .12  9.6 .48 1 error (42) 880     13000   12000    0 false(no-overflow) 3.0 270 28 1 false(no-overflow) .13 34 1.8 0 unknown .059 4.7 .19 0 unknown .042 4.6 .17  0 false(no-overflow) .10  26 .70 1 false(no-overflow) 140    4100 1700   0 false(no-overflow) 3.1 270 28 1 timeout 900    460 5800   0 disqualified 3.1 84 39 0 false(no-overflow) .26 18 3.1 1 false(no-overflow) 8.3 360 66 1 false(no-overflow) 9.9 380 85 1 false(no-overflow) 7.6 350 58 1 timeout 900   150 12000 0
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .13  24 .99 1 false(no-overflow) .081 9.6 .60 1 false(no-overflow) .071 9.0 .41 1 false(no-overflow) 3.0 270 27 1 false(no-overflow) .19 33 2.2 0 unknown .029 4.6 .19 0 unknown .049 4.6 .13  0 false(no-overflow) .13  26 1.8  1 timeout 900    83 12000   0 false(no-overflow) 3.0 270 29 1 false(no-overflow) .36 59 3.2 1 disqualified 3.2 83 44 0 false(no-overflow) .27 23 2.5 1 false(no-overflow) 8.0 360 60 1 false(no-overflow) 7.9 370 63 1 false(no-overflow) 7.8 360 62 1 false(no-overflow) 3.7 150 38 1
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .12  24 1.0  1 false(no-overflow) .079 9.3 .50 1 false(no-overflow) .087 8.8 .32 1 false(no-overflow) 3.1 270 30 1 false(no-overflow) .14 34 1.6 0 unknown .034 4.6 .21 0 unknown .030 4.7 .15  0 false(no-overflow) .085 26 .82 1 false(no-overflow) .40 79 3.8 0 false(no-overflow) 3.2 280 29 1 false(no-overflow) .37 58 3.3 1 disqualified 3.1 82 35 0 false(no-overflow) .25 18 2.6 1 false(no-overflow) 6.7 330 61 1 false(no-overflow) 7.7 350 56 1 false(no-overflow) 7.7 350 61 1 false(no-overflow) 3.5 150 35 1
termination-crafted-lit/cstrncmp_false-no-overflow.c error (134) .20  24 1.4  0 false(no-overflow) .083 9.2 .69 1 error (134) .049 8.5 .37 0 false(no-overflow) 4.0 320 46 1 false(no-overflow) .17 34 2.2 0 unknown .023 4.6 .21 0 unknown .031 4.6 .20  0 false(no-overflow) .11  26 1.2  1 false(no-overflow) 28    760 330   0 false(no-overflow) 4.1 320 45 1 false(no-overflow) .70 61 6.4 1 disqualified 3.3 86 38 0 false(no-overflow) .80 18 12   1 false(no-overflow) 9.1 370 69 1 false(no-overflow) 8.7 360 68 1 false(no-overflow) 9.2 380 75 1 error (1) 4.3 200 36 0
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .12  23 1.0  1 false(no-overflow) .068 9.0 .61 1 false(no-overflow) .068 9.0 .39 1 false(no-overflow) 2.9 270 22 1 false(no-overflow) .16 33 2.0 0 unknown .047 4.8 .20 0 unknown .053 4.6 .15  0 false(no-overflow) .11  26 1.1  1 timeout 900    75 11000   0 false(no-overflow) 3.0 270 30 1 false(no-overflow) .38 59 3.0 1 disqualified 3.1 83 37 0 false(no-overflow) .27 18 3.7 1 false(no-overflow) 7.4 360 57 1 false(no-overflow) 8.7 380 72 1 false(no-overflow) 7.3 340 55 1 timeout 900   150 10000 0
termination-crafted-lit/joey_false-no-overflow.c error (5) .14  24 .72 0 false(no-overflow) .12  11   1.2  1 false(no-overflow) .065 9.4 .53 1 false(no-overflow) 3.1 270 29 1 false(no-overflow) .14 34 1.3 0 unknown .030 4.6 .17 0 unknown .030 4.5 .23  0 false(no-overflow) .077 26 .91 1 timeout 900    120 9700   0 false(no-overflow) 3.0 270 28 1 false(no-overflow) .37 58 3.8 1 disqualified 2.7 74 33 0 false(no-overflow) .25 18 3.3 1 false(no-overflow) 8.6 370 64 1 false(no-overflow) 8.7 370 67 1 false(no-overflow) 8.7 370 69 1 timeout 900   200 11000 0
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .12  24 1.2  1 false(no-overflow) .12  9.3 .51 1 false(no-overflow) .065 9.2 .55 1 false(no-overflow) 3.1 270 28 1 false(no-overflow) .18 34 1.9 0 unknown .030 4.6 .21 0 unknown .044 4.7 .21  0 false(no-overflow) .10  26 1.4  1 false(no-overflow) .40 82 4.6 0 false(no-overflow) 3.1 270 30 1 false(no-overflow) .37 59 3.5 1 disqualified 3.2 82 43 0 false(no-overflow) .24 18 2.5 1 false(no-overflow) 8.1 360 56 1 false(no-overflow) 8.0 370 64 1 false(no-overflow) 7.0 340 48 1 false(no-overflow) 3.4 150 42 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     830 9800    0 error (42) 880     1300   8900    0 out of memory 560     15000   8000    0 out of memory 870   15000 12000 0 unknown 900    290 11000   0 unknown .028 4.6 .16 0 unknown .046 4.6 .16  0 timeout 900     650 10000    0 timeout 900    4400 6900   0 out of memory 870   15000 13000 0 timeout 900    490 6400   0 disqualified 880   180 13000 0 timeout (verification) 900    3300 10000   0 timeout 900   1500 12000 0 timeout 900   5400 6900 0 timeout 900   1300 11000 0 timeout 900   150 11000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true .099 24 .65 2 error (42) 880     1200   8800    0 error (42) 880     15000   13000    0 true 3.2 270 27 2 unknown .81 67 8.8 0 unknown .031 4.7 .20 0 unknown .033 4.6 .20  0 timeout 900     730 9800    0 timeout 900    75 10000   0 true 3.0 270 27 2 timeout 900    320 4300   0 disqualified 880   370 11000 0 timeout (verification) 900    1400 12000   0 true 8.5 370 65 2 true 17   520 150 2 true 8.5 330 70 2 timeout 900   150 13000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true .11  24 .94 2 true 1.7   50   21    2 out of memory 190     15000   2900    0 true 3.0 270 29 2 unknown .83 66 9.2 0 unknown .032 4.7 .23 0 unknown .029 4.6 .21  0 true .63  26 6.9  2 timeout 900    2100 10000   0 true 3.0 270 28 2 true .41 59 3.6 2 disqualified 27   170 330 0 true .21 19 2.1 2 true 8.1 370 65 2 true 8.2 350 74 2 true 8.4 370 67 2 timeout 900   150 13000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 900     1700 10000    0 error (42) 880     2300   4000    0 error (42) 880     220   10000    0 timeout 900   13000 14000 0 unknown 58    48 650   0 unknown .033 4.6 .20 0 unknown .030 4.6 .20  0 timeout 900     1100 11000    0 timeout 900    75 9400   0 timeout 910   13000 12000 0 timeout 900    410 4500   0 disqualified 880   780 11000 0 timeout (verification) 900    420 7200   0 timeout 900   2500 12000 0 timeout 900   5700 9100 0 timeout 900   1800 14000 0 timeout 900   200 9800 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 25     580 260    2 error (42) 880     1300   5100    0 error (42) 870     8000   14000    0 true 110   1100 890 2 unknown 900    200 12000   0 unknown .028 4.5 .24 0 unknown .027 4.6 .18  0 timeout 900     340 11000    0 timeout 900    75 8600   0 true 110   1100 880 2 out of memory 38    15000 470   0 disqualified 880   170 12000 0 timeout (verification) 900    310 14000   0 true 8.2 340 65 2 true 11   560 98 2 true 8.1 360 64 2 timeout 900   150 11000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 900     2200 5600    0 error (42) 880     1500   5900    0 out of memory 340     15000   4600    0 timeout 910   6600 11000 0 unknown 900    590 11000   0 unknown .023 4.7 .22 0 unknown .028 4.6 .19  0 timeout 900     870 10000    0 timeout 900    75 8700   0 timeout 910   6600 12000 0 timeout 900    380 4000   0 disqualified 880   420 10000 0 timeout (verification) 900    1300 13000   0 true 19   550 150 2 timeout 900   2300 6700 0 true 17   680 130 2 timeout 900   150 12000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 900     920 9700    0 error (42) 880     1400   9300    0 out of memory 330     15000   3800    0 timeout 910   520 14000 0 unknown 680    69 8500   0 unknown .031 4.7 .19 0 unknown .051 4.6 .19  0 timeout 900     130 13000    0 timeout 900    4200 7400   0 timeout 910   520 14000 0 timeout 900    550 7100   0 disqualified 880   180 12000 0 timeout (verification) 900    3100 7500   0 timeout 900   5400 11000 0 timeout 900   5600 9200 0 timeout 900   3200 13000 0 timeout 900   150 13000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true .75  28 9.7  2 true .32  9.7 3.9  2 out of memory 340     15000   4800    0 true 59   550 760 2 unknown 4.7  68 63   0 unknown .036 4.6 .17 0 unknown .029 4.7 .18  0 true .16  26 1.7  2 timeout 900    4300 6400   0 true 59   530 820 2 out of memory 130    15000 1800   0 disqualified 97   120 1500 0 timeout (verification) 900    4000 6800   0 true 180   4700 2100 2 timeout 900   4100 6700 0 true 170   4700 2200 2 timeout 900   150 11000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true .10  24 .98 2 error (42) 880     1300   7700    0 out of memory 380     15000   4300    0 true 3.1 270 25 2 unknown .83 65 10   0 unknown .033 4.7 .25 0 unknown .028 4.6 .17  0 timeout 900     270 12000    0 timeout 900    75 9900   0 true 3.1 270 25 2 timeout 900    350 4800   0 disqualified 880   470 14000 0 timeout (verification) 900    480 8400   0 true 9.4 380 81 2 true 20   710 180 2 true 9.4 370 73 2 timeout 900   150 14000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true .10  24 .93 2 error (42) 880     1400   8300    0 out of memory 290     15000   4500    0 true 3.1 270 33 2 unknown .86 67 9.0 0 unknown .035 4.6 .32 0 unknown .051 4.7 .16  0 timeout 900     220 11000    0 timeout 900    75 9200   0 true 3.1 270 28 2 timeout 900    320 4900   0 disqualified 880   510 9400 0 timeout (verification) 900    1200 12000   0 true 10   420 77 2 timeout 900   2200 6000 0 true 9.7 440 83 2 timeout 900   150 11000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true .097 24 .93 2 error (42) 880     1500   9300    0 error (42) 880     8800   12000    0 true 3.2 270 31 2 unknown .85 67 9.5 0 unknown .038 4.6 .24 0 unknown .034 4.6 .18  0 timeout 900     310 11000    0 timeout 900    84 11000   0 true 3.2 270 34 2 timeout 900    400 4100   0 disqualified 880   380 11000 0 timeout (verification) 900    170 11000   0 true 8.7 360 70 2 true 12   570 110 2 true 9.4 370 72 2 timeout 900   150 9500 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true .093 24 1.1  2 error (42) 880     2600   12000    0 error (42) 870     5100   11000    0 true 4.8 290 46 2 unknown .91 67 10   0 unknown .059 4.6 .20 0 unknown .031 4.7 .23  0 timeout 900     1300 11000    0 timeout 900    83 10000   0 true 4.9 290 42 2 out of memory 40    15000 590   0 disqualified 880   460 10000 0 timeout (verification) 900    220 10000   0 true 7.6 360 63 2 true 11   540 95 2 true 7.9 350 60 2 timeout 900   150 9100 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true .091 24 .95 2 error (42) 880     5000   5100    0 error (42) 870     4400   13000    0 true 3.1 270 25 2 unknown 1.9  68 22   0 unknown .029 4.6 .21 0 unknown .034 4.7 .26  0 timeout 900     320 13000    0 timeout 900    75 10000   0 true 3.1 270 29 2 timeout 900    360 4100   0 disqualified 880   850 8500 0 timeout (verification) 900    1000 9600   0 true 7.4 330 65 2 true 11   520 88 2 true 7.8 350 63 2 timeout 900   150 13000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true .48  24 5.8  2 error (42) 880     1200   7800    0 error (42) 880     1900   13000    0 true 3.4 280 33 2 unknown 900    91 13000   0 unknown .044 4.6 .14 0 unknown .029 4.7 .17  0 timeout 900     130 13000    0 timeout 900    75 10000   0 true 3.3 270 31 2 timeout 900    520 5500   0 disqualified 880   770 9700 0 timeout (verification) 900    120 8100   0 true 10   410 75 2 true 23   800 230 2 true 10   420 73 2 timeout 900   150 12000 0
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 900     2100 11000    0 error (42) 880     1100   6900    0 error (42) 870     440   12000    0 timeout 910   7000 11000 0 unknown 250    58 3500   0 unknown .055 4.6 .15 0 unknown .032 4.7 .19  0 timeout 900     380 11000    0 timeout 900    75 9800   0 timeout 910   7100 13000 0 timeout 900    380 4500   0 disqualified 880   490 8900 0 timeout (verification) 900    380 9000   0 timeout 900   1800 12000 0 timeout 900   5400 9300 0 timeout 900   1400 13000 0 timeout 900   150 9500 0
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout 900     430 7200    0 error (42) 880     660   6700    0 error (42) 880     4000   12000    0 true 3.1 270 28 2 unknown 900    92 11000   0 unknown .036 4.7 .23 0 unknown .033 4.6 .14  0 timeout 900     100 12000    0 timeout 900    83 9400   0 true 3.2 270 32 2 timeout 900    420 5700   0 disqualified 880   180 11000 0 timeout (verification) 900    62 14000   0 true 11   510 83 2 true 15   700 130 2 true 13   550 110 2 timeout 900   200 12000 0
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout 900     440 7200    0 error (42) 880     660   8300    0 error (42) 880     4100   14000    0 true 3.2 270 30 2 unknown 900    93 13000   0 unknown .028 4.6 .18 0 unknown .029 4.6 .18  0 timeout 900     110 12000    0 timeout 900    86 9000   0 true 3.1 270 28 2 timeout 900    550 8300   0 disqualified 880   190 12000 0 timeout (verification) 900    62 11000   0 true 11   490 90 2 true 19   570 180 2 true 11   510 82 2 timeout 900   160 13000 0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true .10  24 .84 2 error (42) 880     2200   5300    0 error (42) 870     4900   12000    0 timeout 910   8200 11000 0 unknown 1.8  66 24   0 unknown .031 4.7 .20 0 unknown .052 4.7 .16  0 timeout 900     380 14000    0 timeout 900    77 9600   0 timeout 900   8200 10000 0 timeout 900    390 4800   0 disqualified 880   490 9900 0 timeout (verification) 900    320 13000   0 true 9.7 380 72 2 true 95   1500 940 2 true 10   400 83 2 timeout 900   150 12000 0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 900     1200 5500    0 error (42) 880     6400   7000    0 error (42) 870     2500   10000    0 timeout 900   15000 11000 0 unknown 900    220 13000   0 unknown .053 4.6 .23 0 unknown .035 4.6 .22  0 timeout 900     370 11000    0 timeout 900    75 9600   0 timeout 900   15000 12000 0 out of memory 38    15000 460   0 disqualified 880   590 11000 0 timeout (verification) 900    140 12000   0 timeout 900   2000 13000 0 timeout 900   2000 7300 0 timeout 900   1900 11000 0 timeout 900   150 9900 0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 900     1100 9600    0 error (42) 880     3100   4400    0 error (42) 880     200   11000    0 timeout 900   4100 11000 0 unknown 380    64 3800   0 unknown .030 4.6 .16 0 unknown .028 4.6 .27  0 timeout 900     840 10000    0 timeout 900    250 8800   0 timeout 900   4100 9300 0 timeout 900    410 6100   0 disqualified 880   820 11000 0 timeout (verification) 900    420 8400   0 true 12   500 92 2 true 120   1600 1500 2 true 10   450 83 2 timeout 900   150 12000 0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true .10  24 .79 2 true 1.8   50   22    2 out of memory 190     15000   2200    0 true 2.9 270 28 2 unknown .83 66 8.8 0 unknown .026 4.7 .22 0 unknown .043 4.7 .15  0 true .60  26 8.1  2 timeout 900    2100 9900   0 true 3.1 260 28 2 true .39 59 4.1 2 disqualified 27   170 440 0 true .19 18 2.0 2 true 8.2 380 71 2 true 9.5 380 71 2 true 8.3 370 58 2 timeout 900   150 13000 0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 900     1700 12000    0 error (42) 880     2400   4800    0 error (42) 880     210   10000    0 timeout 910   13000 11000 0 unknown 58    49 750   0 unknown .029 4.8 .24 0 unknown .033 4.7 .24  0 timeout 900     1100 13000    0 timeout 900    75 9400   0 timeout 910   13000 12000 0 timeout 900    410 3800   0 disqualified 880   720 9600 0 timeout (verification) 900    430 7700   0 timeout 900   3200 14000 0 timeout 900   5700 7100 0 timeout 900   1800 14000 0 timeout 900   150 12000 0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 900     900 11000    0 error (42) 880     1400   10000    0 out of memory 330     15000   4200    0 timeout 910   620 13000 0 unknown 720    73 8700   0 unknown .034 4.6 .24 0 unknown .035 4.6 .11  0 timeout 900     130 14000    0 timeout 900    4000 7600   0 timeout 910   620 12000 0 timeout 900    470 8500   0 disqualified 880   180 11000 0 timeout (verification) 900    3200 9900   0 timeout 900   7800 8400 0 timeout 900   3900 6700 0 timeout 900   7400 9700 0 timeout 900   150 12000 0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true .84  29 10    2 true .33  10   3.6  2 out of memory 340     15000   4900    0 true 59   540 830 2 unknown 4.7  67 61   0 unknown .034 4.6 .28 0 unknown .035 4.7 .24  0 true .17  26 2.0  2 timeout 900    4300 6500   0 true 58   550 770 2 out of memory 120    15000 1400   0 disqualified 95   120 1400 0 timeout (verification) 900    4000 7700   0 true 180   4800 2000 2 timeout 900   2700 6000 0 true 170   4700 1800 2 timeout 900   150 13000 0
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true .11  24 .81 2 error (42) 880     7000   3600    0 error (42) 880     410   7000    0 true 3.1 270 30 2 unknown .77 66 8.3 0 unknown .036 4.6 .23 0 unknown .029 4.6 .26  0 timeout 900     1400 12000    0 killed by signal 9 890    4500 8700   0 true 3.1 270 32 2 timeout 900    510 8200   0 disqualified 2.4 74 30 0 true .16 15 2.3 2 true 7.6 350 55 2 true 7.8 360 58 2 true 6.9 340 53 2 timeout 900   150 13000 0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true .14  24 .86 2 error (42) 880     2000   6800    0 error (42) 870     180   10000    0 true 3.1 260 27 2 unknown .80 67 8.9 0 unknown .024 4.8 .24 0 unknown .028 4.6 .23  0 timeout 900     280 11000    0 timeout 900    4300 9400   0 true 3.0 270 30 2 timeout 900    430 6400   0 disqualified 880   530 13000 0 timeout (verification) 900    480 5800   0 true 8.0 370 59 2 true 8.6 360 65 2 true 7.7 370 66 2 timeout 900   150 11000 0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true .10  24 .81 2 error (42) 880     430   6500    0 error (42) 880     100   11000    0 true 2.9 270 26 2 unknown 1.0  67 11   0 unknown .030 4.6 .22 0 unknown .027 4.6 .25  0 timeout 900     220 11000    0 timeout 900    83 10000   0 true 3.1 270 32 2 timeout 900    330 5900   0 disqualified 880   810 11000 0 timeout (verification) 900    420 9200   0 true 8.6 380 69 2 true 8.9 380 63 2 true 8.6 370 73 2 timeout 900   150 10000 0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true .12  24 1.0  2 error (42) 880     1300   8200    0 error (42) 880     14000   13000    0 true 3.0 260 26 2 unknown .79 66 7.7 0 unknown .027 4.6 .29 0 unknown .031 4.6 .22  0 timeout 900     610 11000    0 timeout 900    4100 8900   0 true 3.0 270 29 2 timeout 900    390 5000   0 disqualified 880   360 9800 0 timeout (verification) 900    2800 10000   0 true 8.5 360 67 2 true 10   410 77 2 true 8.2 370 71 2 timeout 900   150 11000 0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true .095 24 1.1  2 error (42) 880     1600   8100    0 error (42) 880     11000   10000    0 true 3.1 270 28 2 unknown .87 67 9.0 0 unknown .029 4.6 .18 0 unknown .027 4.7 .18  0 timeout 900     540 11000    0 killed by signal 9 590    5000 6800   0 true 3.1 270 26 2 timeout 900    380 5100   0 disqualified 880   360 11000 0 timeout (verification) 900    2700 12000   0 true 8.2 350 66 2 true 12   550 110 2 true 8.8 380 69 2 timeout 900   150 11000 0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true .098 24 1.3  2 error (42) 880     2200   10000    0 out of memory 540     15000   7200    0 true 3.1 270 30 2 unknown .86 66 11   0 unknown .028 4.6 .14 0 unknown .034 4.5 .23  0 timeout 900     770 12000    0 killed by signal 9 590    5300 7000   0 true 3.1 270 26 2 timeout 900    400 6800   0 disqualified 880   360 9000 0 timeout (verification) 900    2900 8500   0 true 8.8 370 65 2 true 12   490 93 2 true 7.8 340 70 2 timeout 900   150 11000 0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true .10  24 .83 2 error (42) 880     550   6500    0 error (42) 880     9700   11000    0 true 3.2 270 26 2 unknown 1.3  67 15   0 unknown .031 4.6 .19 0 unknown .039 4.6 .24  0 timeout 900     140 12000    0 timeout 900    82 9600   0 true 3.0 270 26 2 timeout 900    300 5900   0 disqualified 880   640 9800 0 timeout (verification) 900    45 11000   0 true 8.7 370 69 2 true 11   570 98 2 true 8.9 370 76 2 timeout 900   150 11000 0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true .10  24 .73 2 error (42) 880     1200   9200    0 error (42) 870     14000   11000    0 true 3.0 270 26 2 unknown 1.1  66 12   0 unknown .031 4.8 .24 0 unknown .030 4.6 .19  0 timeout 900     200 12000    0 timeout 900    75 10000   0 true 2.9 270 28 2 timeout 900    320 4500   0 disqualified 880   600 9000 0 timeout (verification) 900    600 12000   0 true 8.2 360 60 2 true 8.4 350 72 2 true 8.0 350 60 2 timeout 900   150 11000 0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true .11  24 .72 2 error (42) 880     1000   7900    0 out of memory 300     15000   4800    0 true 3.0 260 28 2 unknown 1.0  67 13   0 unknown .031 4.6 .20 0 unknown .035 4.6 .23  0 timeout 900     180 11000    0 timeout 900    83 10000   0 true 3.0 270 28 2 out of memory 290    15000 2900   0 disqualified 880   610 11000 0 timeout (verification) 900    50 12000   0 true 8.3 340 70 2 true 9.3 400 79 2 true 8.9 390 71 2 timeout 900   150 13000 0
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 6.1   110 91    2 true .22  7.0 2.1  2 true .26  7.5 1.7  2 timeout 900   7200 10000 0 unknown 76    60 930   0 unknown .030 4.6 .14 0 unknown .032 4.6 .20  0 true .39  26 4.8  2 timeout 900    84 8700   0 timeout 910   7400 10000 0 true .44 59 3.7 2 disqualified 880   680 9100 0 true .15 15 1.8 2 true 120   1400 1300 2 timeout 900   2600 6900 0 true 190   1200 2300 2 timeout 900   150 11000 0
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     2600 10000    0 error (42) 880     1900   9000    0 error (42) 870     9800   14000    0 timeout 900   560 13000 0 unknown 900    100 12000   0 unknown .030 4.7 .19 0 unknown .055 4.5 .19  0 timeout 900     270 11000    0 timeout 900    5300 8300   0 timeout 900   460 13000 0 timeout 900    400 5300   0 disqualified 26   120 320 0 timeout (verification) 900    2800 12000   0 timeout 900   2900 12000 0 timeout 900   4900 6600 0 timeout 900   1600 12000 0 timeout 900   150 11000 0
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true .10  24 .81 2 error (42) 880     1200   7600    0 out of memory 790     15000   11000    0 true 3.2 270 28 2 unknown .79 67 8.8 0 unknown .031 4.6 .18 0 unknown .030 4.7 .26  0 timeout 900     1100 10000    0 timeout 900    4200 8300   0 true 3.1 270 31 2 timeout 900    350 5000   0 disqualified 890   330 11000 0 timeout (verification) 900    400 9500   0 true 8.5 360 68 2 true 9.0 370 74 2 true 8.3 360 63 2 error (1) 3.2 150 33 0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 900     1200 11000    0 error (42) 880     3300   4000    0 error (42) 880     200   12000    0 timeout 900   4200 10000 0 unknown 340    58 4200   0 unknown .048 4.6 .16 0 unknown .028 4.6 .23  0 timeout 900     1200 10000    0 timeout 900    230 10000   0 timeout 900   4100 10000 0 timeout 900    440 4500   0 disqualified 880   900 10000 0 timeout (verification) 900    430 7900   0 true 10   490 78 2 true 140   1300 1400 2 true 11   470 100 2 timeout 900   150 12000 0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true .088 24 1.0  2 error (42) 880     4500   4600    0 error (42) 870     170   9400    0 true 3.1 270 27 2 unknown .80 66 8.2 0 unknown .028 4.6 .18 0 unknown .036 4.6 .26  0 timeout 900     600 11000    0 timeout 900    75 10000   0 true 3.1 270 30 2 timeout 900    400 6000   0 disqualified 880   720 12000 0 timeout (verification) 900    460 9500   0 true 7.2 340 52 2 true 8.9 360 69 2 true 8.3 360 64 2 timeout 900   150 10000 0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c true 1.2   45 13    2 error (42) 880     3200   2800    0 error (42) 880     200   10000    0 true 3.2 270 32 2 unknown 29    67 350   0 unknown .030 4.6 .17 0 unknown .027 4.6 .25  0 timeout 900     1200 11000    0 timeout 900    74 9100   0 true 3.2 270 27 2 timeout 900    380 4000   0 disqualified 880   8000 10000 0 timeout (verification) 900    430 6600   0 true 8.8 360 64 2 true 14   620 130 2 true 11   400 87 2 timeout 900   150 8500 0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true .091 24 .98 2 error (42) 880     3500   5700    0 error (42) 870     200   11000    0 true 3.0 270 27 2 unknown .84 66 10   0 unknown .054 4.6 .16 0 unknown .055 4.6 .21  0 timeout 900     200 13000    0 timeout 900    4200 9900   0 true 3.0 270 24 2 timeout 900    620 6400   0 disqualified 880   310 12000 0 timeout (verification) 900    77 13000   0 true 8.4 370 59 2 true 8.3 340 63 2 true 7.8 370 66 2 timeout 900   150 13000 0
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 900     2300 13000    0 error (42) 880     2100   8900    0 error (42) 870     4800   11000    0 timeout 900   6700 12000 0 unknown 88    47 1200   0 unknown .031 4.6 .19 0 unknown .034 4.6 .18  0 timeout 900     880 11000    0 timeout 900    4700 8000   0 timeout 900   6900 11000 0 timeout 900    970 12000   0 disqualified 890   380 10000 0 timeout (verification) 900    57 11000   0 timeout 900   4100 10000 0 timeout 900   5400 10000 0 timeout 900   3700 13000 0 error (1) 3.2 150 30 0
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true .10  24 .76 2 error (42) 870     1400   10000    0 out of memory 830     15000   13000    0 true 3.0 260 28 2 unknown .98 65 11   0 unknown .049 4.6 .16 0 unknown .035 4.6 .26  0 timeout 900     210 11000    0 timeout 900    4800 7400   0 true 3.0 260 28 2 timeout 900    400 4300   0 disqualified 880   460 11000 0 timeout (verification) 900    2500 11000   0 true 6.8 340 58 2 true 8.4 360 64 2 true 7.1 340 58 2 timeout 900   150 15000 0
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c true .10  24 .95 2 error (42) 880     1700   8400    0 error (42) 880     4400   12000    0 true 3.1 270 31 2 unknown .95 67 10   0 unknown .027 4.6 .15 0 unknown .042 4.6 .20  0 timeout 900     230 11000    0 timeout 900    82 9500   0 true 3.0 270 25 2 out of memory 42    15000 520   0 disqualified 880   360 13000 0 timeout (verification) 900    390 8900   0 true 8.7 380 72 2 true 9.9 370 78 2 true 8.4 370 63 2 timeout 900   150 9800 0
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 900     830 7000    0 error (42) 880     910   9800    0 error (42) 880     3100   12000    0 timeout 900   560 13000 0 unknown 900    170 11000   0 unknown .028 4.6 .26 0 unknown .035 4.6 .13  0 timeout 900     260 14000    0 timeout 900    4300 9800   0 timeout 900   570 13000 0 timeout 900    540 5500   0 disqualified 880   290 13000 0 timeout (verification) 900    55 12000   0 timeout 900   990 12000 0 timeout 900   3600 8900 0 timeout 900   1900 13000 0 timeout 900   150 11000 0
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c error (5) .084 24 .80 0 out of memory 520     14000   6200    0 error (42) 880     13000   13000    0 true 3.6 280 31 2 out of memory 250    15000 3000   0 unknown .032 4.6 .16 0 unknown .027 4.6 .21  0 out of memory 620     15000 6300    0 timeout 900    2200 7200   0 true 3.5 290 32 2 timeout 900    4500 5400   0 disqualified 880   140 11000 0 timeout (verification) 900    380 12000   0 true 12   500 88 2 true 13   620 130 2 true 13   590 100 2 timeout 900   150 12000 0
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c error (5) .11  24 .59 0 out of memory 410     14000   4300    0 error (42) 880     13000   11000    0 timeout 900   4200 10000 0 out of memory 230    15000 2400   0 unknown .049 4.6 .15 0 unknown .035 4.6 .22  0 out of memory 530     15000 5000    0 timeout 900    2100 13000   0 timeout 900   5400 10000 0 out of memory 98    15000 1400   0 disqualified 890   210 11000 0 timeout (verification) 900    500 12000   0 true 19   730 150 2 timeout 900   2300 9000 0 true 17   550 130 2 timeout 900   150 13000 0
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true .10  24 .88 2 error (42) 880     1900   8100    0 error (42) 880     6300   11000    0 true 3.0 270 27 2 unknown 2.8  67 38   0 unknown .039 4.6 .13 0 unknown .051 4.6 .21  0 timeout 900     180 11000    0 timeout 900    76 11000   0 true 3.1 270 28 2 timeout 900    320 5800   0 disqualified 880   280 11000 0 timeout (verification) 900    100 10000   0 true 8.1 360 62 2 true 15   650 140 2 true 8.7 370 72 2 timeout 900   150 11000 0
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true .11  24 .74 2 error (42) 880     1700   9200    0 out of memory 500     15000   6500    0 true 3.0 270 30 2 unknown .84 66 8.3 0 unknown .033 4.6 .26 0 unknown .041 4.6 .22  0 timeout 900     660 11000    0 timeout 900    82 9900   0 true 3.0 260 29 2 timeout 900    410 4700   0 disqualified 880   630 10000 0 timeout (verification) 900    220 7300   0 true 8.6 380 61 2 true 8.5 360 76 2 true 7.6 350 60 2 timeout 900   150 11000 0
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true .15  24 .74 2 true .42  15   3.9  2 witness invalid (true) .39  15   5.1  0 true 3.0 270 28 2 unknown .85 67 9.4 0 unknown .045 4.6 .13 0 unknown .049 4.6 .19  0 true .21  26 2.5  2 timeout 900    2100 9700   0 true 2.9 270 26 2 true .66 130 7.0 2 disqualified 16   110 190 0 true .16 15 1.8 2 true 8.0 360 66 2 true 7.5 330 58 2 true 7.2 340 59 2 timeout 900   150 11000 0
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 20     600 170    2 error (42) 870     1300   4600    0 error (42) 870     4800   13000    0 true 110   1100 780 2 unknown 900    200 13000   0 unknown .035 4.6 .26 0 unknown .032 4.6 .17  0 timeout 900     330 12000    0 timeout 900    75 9700   0 true 110   1100 840 2 out of memory 38    15000 520   0 disqualified 880   250 10000 0 timeout (verification) 900    310 14000   0 true 8.1 340 64 2 true 10   450 84 2 true 9.4 380 76 2 timeout 900   150 12000 0
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true .092 24 .95 2 error (42) 880     4500   3900    0 error (42) 870     150   9800    0 true 3.0 270 28 2 unknown .79 66 9.1 0 unknown .037 4.8 .23 0 unknown .028 4.6 .29  0 timeout 900     890 10000    0 timeout 900    74 10000   0 true 2.9 270 30 2 timeout 900    360 6000   0 disqualified 880   650 9000 0 timeout (verification) 900    430 7100   0 true 8.2 370 74 2 true 8.2 360 74 2 true 8.1 370 62 2 timeout 900   150 11000 0
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true .10  24 .73 2 error (42) 880     2100   5500    0 error (42) 870     4800   13000    0 true 3.0 270 26 2 unknown 1.3  65 16   0 unknown .030 4.7 .19 0 unknown .031 4.6 .21  0 timeout 900     390 13000    0 timeout 900    74 9700   0 true 3.1 270 29 2 timeout 900    490 3600   0 disqualified 880   830 11000 0 timeout (verification) 900    980 12000   0 true 9.6 380 71 2 timeout 900   2200 8100 0 true 8.7 360 69 2 timeout 900   150 12000 0
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true .13  24 .78 2 error (42) 880     1300   11000    0 error (42) 880     14000   12000    0 true 3.0 270 28 2 unknown .84 67 7.7 0 unknown .031 4.7 .18 0 unknown .035 4.7 .29  0 timeout 900     550 12000    0 killed by signal 9 830    4500 11000   0 true 3.1 270 28 2 timeout 900    370 5200   0 disqualified 880   340 8800 0 timeout (verification) 900    2900 12000   0 true 8.0 360 63 2 true 9.0 360 76 2 true 8.0 350 70 2 timeout 900   150 11000 0
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true .10  24 .77 2 error (42) 880     1400   11000    0 out of memory 440     15000   5000    0 true 2.9 270 28 2 unknown .96 67 11   0 unknown .033 4.6 .29 0 unknown .042 4.7 .21  0 timeout 900     350 10000    0 timeout 900    75 9500   0 true 3.0 270 29 2 timeout 900    3200 4600   0 disqualified 890   1200 12000 0 true .22 18 2.6 2 true 8.4 360 63 2 true 7.5 340 61 2 true 7.9 350 57 2 error (1) 51   150 650 0
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true .092 24 1.1  2 error (42) 870     10000   12000    0 error (42) 880     1400   8800    0 timeout 910   5200 11000 0 unknown .82 66 8.3 0 unknown .032 4.6 .18 0 unknown .056 4.6 .19  0 timeout 900     3500 11000    0 timeout 900    75 8600   0 timeout 910   5300 12000 0 out of memory 770    15000 8100   0 disqualified 880   500 12000 0 timeout (verification) 900    410 12000   0 true 9.0 380 69 2 true 10   460 82 2 true 8.8 370 75 2 timeout 900   150 12000 0
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true .13  24 .78 2 error (42) 880     890   4900    0 error (42) 880     200   10000    0 true 4.8 290 46 2 unknown .88 67 12   0 unknown .031 4.6 .18 0 unknown .053 4.5 .22  0 timeout 900     810 13000    0 timeout 900    82 8700   0 true 4.6 290 44 2 timeout 900    730 4900   0 disqualified 880   790 9200 0 timeout (verification) 900    410 9700   0 true 9.0 370 75 2 true 10   460 88 2 true 9.1 380 72 2 timeout 900   150 10000 0
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true .10  24 .79 2 error (42) 880     2900   11000    0 out of memory 370     15000   4800    0 true 3.1 270 29 2 unknown 1.3  67 16   0 unknown .028 4.6 .22 0 unknown .035 4.6 .26  0 timeout 900     480 12000    0 timeout 900    4400 9100   0 true 3.2 270 27 2 timeout 900    370 5900   0 disqualified 880   340 12000 0 timeout (verification) 900    3000 12000   0 true 8.6 350 72 2 true 11   500 100 2 true 9.0 380 75 2 timeout 900   150 12000 0
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c true .15  23 .71 2 error (42) 880     2100   9700    0 error (42) 880     150   12000    0 true 3.1 270 28 2 unknown .82 68 9.1 0 unknown .031 4.6 .15 0 unknown .059 4.5 .23  0 timeout 900     450 13000    0 timeout 900    84 9800   0 true 3.0 270 27 2 out of memory 540    15000 7000   0 disqualified 2.5 81 33 0 probably out of memory (killed (signal 9, verification)) 170    15000 2700   0 true 8.4 370 58 2 true 7.8 360 61 2 true 8.1 370 70 2 timeout 900   150 9900 0
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 3.6   99 50    1 true 5.1   140   72    1 error (42) 880     3200   9300    0 timeout 910   8200 12000 0 unknown 34    68 450   0 unknown .053 4.6 .16 0 unknown .030 4.6 .19  0 true 5.3   33 61    1 timeout 900    2100 12000   0 timeout 900   8300 10000 0 out of memory 52    15000 830   0 disqualified 880   320 11000 0 timeout (verification) 900    370 12000   0 timeout 900   7100 7500 0 timeout 900   1600 6900 0 timeout 900   6400 9400 0 timeout 900   150 13000 0
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c error (134) .21  25 1.5  0 error (42) 880     5300   5800    0 error (134) .051 8.1 .30 0 true 3.7 310 35 2 unknown .95 68 10   0 unknown .053 4.6 .16 0 unknown .034 4.6 .17  0 timeout 900     5600 10000    0 true 73    5500 770   2 true 3.7 310 40 2 timeout 900    890 7400   0 disqualified 2.6 75 30 0 true .20 17 2.8 2 true 8.9 360 70 2 true 7.8 340 70 2 true 9.0 380 65 2 error (1) 4.1 200 39 0
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c error (134) .18  24 1.1  0 error (42) 880     1000   6100    0 error (134) .050 6.8 .25 0 true 3.6 300 34 2 unknown 1.1  67 13   0 unknown .052 4.6 .16 0 unknown .030 4.6 .22  0 timeout 900     1800 11000    0 true 62    5000 770   2 true 3.6 310 35 2 timeout 900    710 5500   0 disqualified 2.6 81 28 0 timeout (verification) 900    330 11000   0 true 8.7 370 72 2 true 8.7 360 69 2 true 8.7 370 63 2 error (1) 4.1 200 40 0
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c error (134) .16  24 1.7  0 error (42) 880     6300   3400    0 error (134) .050 7.2 .34 0 true 3.2 280 26 2 unknown .92 68 9.8 0 unknown .059 4.6 .22 0 unknown .050 4.5 .18  0 timeout 900     2600 11000    0 true 75    4500 720   2 true 3.2 280 33 2 timeout 900    1100 11000   0 disqualified 2.5 73 33 0 timeout (verification) 900    430 11000   0 true 7.9 350 61 2 true 7.6 350 61 2 true 8.0 350 67 2 error (1) 4.1 200 37 0
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c error (134) .16  25 1.4  0 error (42) 880     1000   5200    0 error (134) .047 8.2 .41 0 true 3.6 310 37 2 unknown 1.1  65 12   0 unknown .053 4.7 .25 0 unknown .030 4.6 .20  0 timeout 900     2100 9500    0 true 74    5800 790   2 true 3.6 310 30 2 timeout 900    690 5100   0 disqualified 2.5 79 28 0 true .21 17 2.5 2 true 8.6 340 70 2 true 9.3 360 72 2 true 8.8 370 67 2 error (1) 4.2 200 34 0
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c error (134) .17  25 1.4  0 error (42) 880     1000   6900    0 error (134) .055 8.1 .38 0 true 3.6 310 34 2 unknown 1.1  67 15   0 unknown .056 4.6 .18 0 unknown .029 4.6 .20  0 timeout 900     2000 8900    0 true 61    5700 790   2 true 3.5 310 35 2 timeout 900    700 5200   0 disqualified 2.5 81 36 0 timeout (verification) 900    450 12000   0 true 7.5 340 65 2 true 8.4 350 62 2 true 9.1 380 84 2 error (1) 4.1 200 35 0
termination-crafted-lit/genady_true-termination_true-no-overflow.c true .69  24 9.1  2 true 4.4   130   57    2 true 4.6   170   64    2 timeout 910   4400 10000 0 unknown 130    67 1400   0 unknown .030 4.6 .23 0 unknown .032 4.6 .18  0 out of memory 860     15000 8300    0 timeout 900    76 9400   0 timeout 910   4500 9500 0 true 2.6  85 30   2 disqualified 880   960 7800 0 true .22 15 2.9 2 true 11   510 86 2 true 48   930 490 2 true 11   480 97 2 timeout 900   150 11000 0
termination-crafted-lit/strchr_true-no-overflow_true-termination.c error (134) .16  24 1.4  0 error (42) 880     5500   5800    0 error (134) .050 7.9 .27 0 true 3.2 280 32 2 unknown .92 66 9.8 0 unknown .054 4.6 .15 0 unknown .035 4.7 .23  0 timeout 900     1800 12000    0 true 130    5000 1300   2 true 3.2 260 29 2 timeout 900    630 6300   0 disqualified 2.5 77 33 0 true .23 19 2.1 2 true 9.1 380 66 2 true 8.8 340 65 2 true 8.3 360 70 2 error (1) 4.3 210 35 0
termination-numeric/Addition01_false-no-overflow.c error (5) .097 24 .71 0 false(no-overflow) .096 9.1 .64 1 false(no-overflow) .093 8.7 .40 1 false(no-overflow) 3.2 280 28 1 false(no-overflow) .15 33 1.5 0 unknown .032 4.6 .17 0 unknown .030 4.6 .21  0 false(no-overflow) .080 26 .92 1 false(no-overflow) 21    91 250   0 false(no-overflow) 3.3 280 27 1 false(no-overflow) .35 59 3.5 1 disqualified 2.7 76 34 0 false(no-overflow) .24 18 2.8 1 false(no-overflow) 7.6 370 58 1 false(no-overflow) 8.1 360 71 1 false(no-overflow) 6.9 330 54 1 false(no-overflow) 4.8 150 52 1
termination-numeric/Avg_true_false-no-overflow.c error (5) .082 24 .87 0 false(no-overflow) .082 9.6 .77 1 false(no-overflow) .067 9.6 .58 1 false(no-overflow) 3.1 270 29 1 false(no-overflow) .17 34 1.9 0 unknown .035 4.6 .12 0 unknown .028 4.6 .21  0 false(no-overflow) .11  26 1.3  1 timeout 900    2100 7700   0 false(no-overflow) 3.1 270 28 1 false(no-overflow) .36 59 3.9 1 disqualified 2.8 80 32 0 false(no-overflow) .24 18 3.0 1 false(no-overflow) 7.3 340 59 1 false(no-overflow) 7.8 370 62 1 false(no-overflow) 7.7 370 58 1 false(no-overflow) 7.2 200 82 1
termination-numeric/Binomial_true-termination_false-no-overflow.c error (5) .086 24 .87 0 false(no-overflow) 25     210   240    1 out of memory 430     15000   5400    0 timeout 900   1400 9400 0 unknown 900    860 9400   0 unknown .029 4.6 .24 0 unknown .029 4.9 .20  0 false(no-overflow) 7.6   77 93    1 false(no-overflow) .42 83 5.2 0 timeout 900   1400 9700 0 false(no-overflow) .56 59 5.9 1 disqualified 880   200 13000 0 false(no-overflow) .36 18 4.8 1 timeout 900   930 11000 0 timeout 900   1500 10000 0 timeout 910   13000 8900 0 false(no-overflow) 4.5 200 42 1
termination-numeric/Et1_true_false-no-overflow.c error (5) .085 24 .73 0 false(no-overflow) .078 9.5 .54 1 false(no-overflow) .069 9.9 .45 1 false(no-overflow) 3.0 270 27 1 false(no-overflow) .17 33 1.9 0 unknown .027 4.6 .23 0 unknown .028 4.7 .25  0 false(no-overflow) .13  26 1.2  1 false(no-overflow) .41 83 4.9 0 false(no-overflow) 3.0 270 31 1 false(no-overflow) .38 59 4.0 1 disqualified 3.1 83 44 0 false(no-overflow) .24 19 3.2 1 false(no-overflow) 7.6 350 63 1 false(no-overflow) 7.9 360 63 1 false(no-overflow) 8.3 370 71 1 false(no-overflow) 3.6 160 36 1
termination-numeric/Et2_true_false-no-overflow.c error (5) .12  24 .77 0 false(no-overflow) .079 9.8 .84 1 false(no-overflow) .058 9.4 .59 1 false(no-overflow) 2.9 270 29 1 false(no-overflow) .18 34 1.7 0 unknown .028 4.8 .15 0 unknown .033 4.6 .26  0 false(no-overflow) .12  26 1.3  1 timeout 900    1500 8900   0 false(no-overflow) 3.1 270 28 1 false(no-overflow) .39 59 3.2 1 disqualified 3.1 82 36 0 false(no-overflow) .23 18 3.1 1 false(no-overflow) 7.4 350 58 1 false(no-overflow) 8.4 360 60 1 false(no-overflow) 8.0 370 69 1 false(no-overflow) 3.4 150 36 1
termination-numeric/Et3_true_false-no-overflow.c error (5) .083 24 .78 0 false(no-overflow) .079 9.5 .55 1 false(no-overflow) .068 9.4 .50 1 false(no-overflow) 3.0 270 29 1 false(no-overflow) .16 33 1.9 0 unknown .029 4.6 .25 0 unknown .033 4.6 .19  0 false(no-overflow) .10  26 1.3  1 false(no-overflow) .42 83 4.8 0 false(no-overflow) 3.0 270 30 1 false(no-overflow) .39 59 3.6 1 disqualified 3.1 100 39 0 false(no-overflow) .23 18 2.5 1 false(no-overflow) 7.9 370 69 1 false(no-overflow) 7.9 370 61 1 false(no-overflow) 6.8 330 60 1 false(no-overflow) 3.6 150 41 1
termination-numeric/Et4_true_false-no-overflow.c error (5) .13  24 .72 0 false(no-overflow) .13  9.1 .62 1 false(no-overflow) .066 9.0 .58 1 false(no-overflow) 3.1 260 27 1 false(no-overflow) .19 33 2.3 0 unknown .034 4.7 .29 0 unknown .028 4.8 .18  0 false(no-overflow) .14  26 1.6  1 timeout 900    1800 8300   0 false(no-overflow) 2.9 270 27 1 false(no-overflow) .36 59 3.6 1 disqualified 3.1 82 37 0 false(no-overflow) .23 18 2.7 1 false(no-overflow) 8.2 370 57 1 false(no-overflow) 8.5 370 67 1 false(no-overflow) 8.1 360 62 1 false(no-overflow) 3.4 150 33 1
termination-numeric/MultCommutative_false-no-overflow.c error (5) .092 24 .72 0 false(no-overflow) .081 9.8 1.1  1 error (42) 870     6500   13000    0 error 6.3 300 63 0 out of memory 200    15000 3100   0 unknown .032 4.6 .29 0 unknown .028 4.6 .25  0 false(no-overflow) .21  26 2.0  1 false(no-overflow) 49    200 570   0 error 5.9 310 51 0 false(no-overflow) .39 59 3.3 1 disqualified 2.9 79 38 0 false(no-overflow) .43 18 6.3 1 false(no-overflow) 11   510 85 1 false(no-overflow) 13   620 120 1 false(no-overflow) 12   540 95 1 false(no-overflow) 4.7 200 43 1
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c error (5) .092 24 .70 0 false(no-overflow) 1.0   63   12    1 false(no-overflow) 2.9   67   44    1 timeout 900   1300 7900 0 false(no-overflow) 6.5  84 89   0 unknown .029 4.6 .22 0 unknown .030 4.6 .19  0 false(no-overflow) 14     50 180    1 timeout 900    210 11000   0 timeout 900   1300 7700 0 timeout 900    3000 4300   0 disqualified 36   87 530 0 false(no-overflow) 9.8  50 140   1 timeout 900   1100 7000 0 timeout 900   1300 12000 0 timeout 900   2600 7600 0 false(no-overflow) 4.3 200 39 1
termination-numeric/Ackermann01_true-termination_true-no-overflow.c error (5) .086 24 .83 0 error (42) 870     240   3400    0 error (42) 870     10000   13000    0 timeout 910   6900 10000 0 out of memory 220    15000 3100   0 unknown .060 4.8 .13 0 unknown .031 4.6 .18  0 out of memory 460     15000 5800    0 timeout 900    150 9900   0 timeout 900   4000 11000 0 out of memory 55    15000 800   0 disqualified 890   230 9500 0 timeout (verification) 900    14000 14000   0 timeout 900   8900 7200 0 timeout 900   1000 9900 0 timeout 900   7600 7500 0 timeout 900   150 11000 0
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c error (5) .12  24 .69 0 error (42) 880     2800   9200    0 error (42) 880     280   11000    0 timeout 900   4300 10000 0 unknown .90 66 9.6 0 unknown .028 4.6 .24 0 unknown .057 4.7 .22  0 timeout 900     1100 9200    0 timeout 900    1900 11000   0 timeout 910   4100 11000 0 out of memory 100    15000 1500   0 disqualified 890   190 13000 0 timeout (verification) 900    1300 14000   0 true 13   530 110 2 timeout 900   4600 9100 0 true 13   550 110 2 timeout 900   150 11000 0
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c error (5) .094 24 .77 0 error (42) 880     180   3300    0 error (42) 880     12000   11000    0 true 6.1 320 54 1 out of memory 180    15000 2200   0 unknown .046 4.6 .14 0 unknown .030 4.6 .12  0 timeout 900     8800 7900    0 timeout 900    1300 10000   0 true 5.5 310 53 1 out of memory 45    15000 700   0 disqualified 890   290 9000 0 timeout (verification) 900    2900 12000   0 timeout 900   6600 11000 0 timeout 900   1100 11000 0 timeout 900   5400 10000 0 timeout 900   200 13000 0
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c error (5) .087 24 .71 0 out of memory 690     15000   4500    0 error (42) 880     350   9100    0 true 3.3 280 30 2 unknown .85 66 9.4 0 unknown .032 4.8 .22 0 unknown .031 4.6 .22  0 timeout 900     960 10000    0 timeout 900    770 8700   0 true 3.3 280 32 2 timeout 900    1800 7800   0 disqualified 890   200 11000 0 timeout (verification) 900    460 9100   0 true 8.6 360 67 2 true 10   490 82 2 true 8.1 340 59 2 timeout 900   150 12000 0
termination-numeric/LogRecursive_true-termination_true-no-overflow.c error (5) .089 24 .77 0 true 2.6   71   29    1 true 25     79   310    1 timeout 900   1300 10000 0 unknown 4.0  120 46   0 unknown .031 4.6 .20 0 unknown .056 4.6 .17  0 true 81     160 1100    1 timeout 900    4300 10000   0 timeout 900   1400 10000 0 true 4.9  620 67   1 disqualified 880   360 8900 0 true 23    160 220   1 timeout 900   770 12000 0 timeout 900   5400 11000 0 timeout 900   960 13000 0 timeout 900   200 12000 0
termination-numeric/Parts_true-termination_true-no-overflow.c error (5) .092 24 .70 0 error (42) 880     730   4500    0 error (42) 880     14000   11000    0 timeout 900   3000 10000 0 unknown 900    7700 11000   0 unknown .027 4.6 .21 0 unknown .037 4.6 .15  0 timeout 900     2800 11000    0 timeout 900    75 9000   0 timeout 900   3000 11000 0 timeout 900    680 5500   0 disqualified 890   390 7100 0 timeout (verification) 900    10000 13000   0 timeout 900   4600 13000 0 timeout 900   1400 10000 0 timeout 900   5600 13000 0 timeout 900   200 10000 0
termination-numeric/TwoWay_true-termination_true-no-overflow.c error (5) .083 24 .88 0 error (42) 880     5500   5700    0 error (42) 880     930   7900    0 timeout 900   640 8400 0 unknown 14    84 180   0 unknown .042 4.6 .19 0 unknown .053 4.6 .22  0 timeout 900     200 11000    0 timeout 900    680 11000   0 timeout 900   650 9700 0 out of memory 54    15000 770   0 disqualified 45   98 540 0 timeout (verification) 900    9000 11000   0 true 16   610 140 2 timeout 900   1100 8700 0 true 53   710 660 2 timeout 900   200 12000 0
termination-numeric/gcd01_true-termination_true-no-overflow.c error (5) .095 24 .79 0 error (42) 880     4800   5600    0 error (42) 880     12000   11000    0 true 3.6 280 32 2 out of memory 250    15000 3100   0 unknown .055 4.6 .17 0 unknown .034 4.7 .22  0 timeout 900     890 7800    0 timeout 900    93 13000   0 true 3.5 290 38 2 out of memory 180    15000 2600   0 disqualified 880   100 10000 0 timeout (verification) 900    59 11000   0 true 9.5 370 69 2 true 12   560 96 2 true 8.7 350 73 2 timeout 900   150 11000 0
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true .52  31 7.6  2 true .52  15   6.4  2 true 1.4   16   22    2 true 16   540 160 1 unknown 7.4  67 110   0 unknown .029 4.6 .16 0 unknown .033 4.6 .20  0 true .19  26 2.7  2 timeout 900    2000 9300   0 true 17   540 180 1 true .66 120 7.3 2 disqualified 32   130 470 0 true .42 18 5.4 2 true 49   990 490 2 true 220   1500 2800 1 true 73   1200 840 2 timeout 900   150 13000 0
termination-numeric/recHanoi02_true-termination_true-no-overflow.c error (5) .087 24 .86 0 true .47  12   4.3  2 true 2.5   16   38    2 timeout 910   4400 10000 0 unknown .87 66 9.7 0 unknown .055 4.5 .21 0 unknown .032 4.6 .16  0 true 1.8   27 27    2 timeout 900    2200 12000   0 timeout 900   4400 12000 0 true .59 62 7.4 2 disqualified 12   84 190 0 true .66 18 8.3 2 true 66   1100 650 2 timeout 900   1300 10000 0 error (7) 120   2900 1600 0 timeout 900   200 11000 0
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (5) .082 24 .84 0 error (42) 870     5000   6400    0 error (42) 880     500   11000    0 timeout 900   4100 10000 0 unknown 3.4  82 39   0 unknown .033 4.7 .15 0 unknown .029 4.7 .20  0 timeout 900     1200 12000    0 timeout 900    1100 10000   0 timeout 900   4300 13000 0 out of memory 840    15000 11000   0 disqualified 880   320 9000 0 timeout (verification) 900    2800 11000   0 timeout 900   4400 9600 0 timeout 900   2100 7300 0 timeout 900   3200 11000 0 timeout 900   200 9800 0
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (5) .090 24 .84 0 error (42) 880     5000   6900    0 error (42) 880     500   11000    0 timeout 900   4400 11000 0 unknown 3.4  82 51   0 unknown .056 4.6 .16 0 unknown .031 4.6 .18  0 timeout 900     1200 9700    0 timeout 900    1100 8600   0 timeout 910   4600 9100 0 out of memory 850    15000 12000   0 disqualified 880   330 10000 0 timeout (verification) 900    2800 11000   0 timeout 900   4600 9600 0 timeout 900   1800 7200 0 timeout 900   3600 11000 0 timeout 900   200 12000 0
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 900     24 9900    0 out of memory 290     14000   3600    0 error (42) 870     5100   11000    0 timeout 900   7900 13000 0 unknown 900    740 11000   0 unknown .030 4.6 .18 0 unknown .028 4.7 .22  0 timeout 900     1200 11000    0 timeout 900    78 11000   0 timeout 900   7900 10000 0 timeout 900    500 5100   0 disqualified 880   180 12000 0 timeout (verification) 900    1200 11000   0 timeout 900   1000 11000 0 timeout 900   1900 7400 0 timeout 900   990 13000 0 timeout 900   150 11000 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 status cpu (s) mem (MB) energy (J) score
total 280 25000 44000 270000 273 280 90000   350000 670000 191 280 88000   770000 1100000 161 280 44000 320000 540000 311 280 21000 230000 270000 0 280 10 1300 54 0 280 9.9 1300 57 0 280 97000     270000 1200000    187 280 160000 310000 1800000 12 280 44000 320000 540000 311 280 88000   540000 590000 177 280 92000 84000 1100000 0 280 90000   150000 1000000 204 280 30000 200000 360000 350 280 48000 260000 470000 309 280 31000 200000 390000 346 280 120000 47000 1600000 131
    correct results 201 92 6500 940 271 170 51   2100 480 188 151 130   6100 1500 160 227 1200 65000 11000 307 0 0 0 168 42     4400 500    185 6 470 31000 5200 12 227 1200 65000 11000 307 160 64   9600 600 176 0 178 52   3200 640 203 250 2800 110000 24000 350 229 2900 94000 25000 308 248 2800 110000 26000 346 131 5300 21000 67000 131
        correct true 70 75 3300 800 140 18 12   400 150 36 9 9.1 240 130 18 80 580 24000 5500 160 0 0 0 17 5.4   440 73    34 6 470 31000 5200 12 80 580 24000 5600 160 16 9.6 1100 99 32 0 25 5.1 410 62 50 100 1600 51000 15000 200 79 1200 37000 11000 158 98 1600 50000 16000 196 0
        correct false 131 17 3100 140 131 152 39   1700 330 152 142 120   5800 1400 142 147 660 41000 5700 147 0 0 0 151 37     4000 430    151 0 147 670 41000 5800 147 144 54   8500 500 144 0 153 47   2800 580 153 150 1200 55000 9600 150 150 1800 57000 14000 150 150 1200 55000 10000 150 131 5300 21000 67000 131
    correct-unconfimed results 2 11 370 140 2 3 7.8 220 100 3 1 25   79 310 1 4 29 1400 280 4 150 44 5100 570 0 0 0 3 86     220 1100    2 112 13000 89000 170000 0 4 29 1400 300 4 1 4.9 620 67 1 0 1 23   160 220 1 0 1 220 1500 2800 1 0 0
        correct-unconfirmed true 2 11 370 140 2 3 7.8 220 100 3 1 25   79 310 1 4 29 1400 280 4 0 0 0 2 86     200 1100    2 0 4 29 1400 300 4 1 4.9 620 67 1 0 1 23   160 220 1 0 1 220 1500 2800 1 0 0
        correct-unconfirmed false 0 0 0 0 150 44 5100 570 0 0 0 1 .091 26 .78 0 112 13000 89000 170000 0 0 0 0 0 0 0 0 0
    incorrect results 0 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 0
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (280 tasks, max score: 402) 273 191 161 311 0 0 0 187 12 311 177 0 204 350 309 346 131
Run set 2ls.sv-comp19_prop-nooverflow.NoOverflows-BitVectors cbmc.sv-comp19_prop-nooverflow.NoOverflows-BitVectors cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-BitVectors cpa-seq.sv-comp19_prop-nooverflow.NoOverflows-BitVectors depthk.sv-comp19_prop-nooverflow.NoOverflows-BitVectors divine-explicit.sv-comp19_prop-nooverflow.NoOverflows-BitVectors divine-smt.sv-comp19_prop-nooverflow.NoOverflows-BitVectors esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-BitVectors map2check.sv-comp19_prop-nooverflow.NoOverflows-BitVectors pesco.sv-comp19_prop-nooverflow.NoOverflows-BitVectors pinaka.sv-comp19_prop-nooverflow.NoOverflows-BitVectors smack.sv-comp19_prop-nooverflow.NoOverflows-BitVectors symbiotic.sv-comp19_prop-nooverflow.NoOverflows-BitVectors uautomizer.sv-comp19_prop-nooverflow.NoOverflows-BitVectors ukojak.sv-comp19_prop-nooverflow.NoOverflows-BitVectors utaipan.sv-comp19_prop-nooverflow.NoOverflows-BitVectors verifuzz.sv-comp19_prop-nooverflow.NoOverflows-BitVectors