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; sv-comp19_prop-nooverflow.NoOverflows-Other] cbmc.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] cbmc-path.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] cpa-seq.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] depthk.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] divine-explicit.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] divine-smt.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] esbmc-kind.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] map2check.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] pesco.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] pinaka.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] smack.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] symbiotic.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] uautomizer.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] ukojak.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] utaipan.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] verifuzz.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other]
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) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i false(no-overflow) .15  25 1.1  false(no-overflow) .074 9.2 .62 false(no-overflow) .081 9.2 .43 false(no-overflow) 3.9 280 36 false(no-overflow) .14 34 1.6 unknown .035 4.6 .20 unknown .054 4.6 .16  false(no-overflow) .078 26 1.1  timeout 900    230 10000   false(no-overflow) 3.9 280 34 false(no-overflow) .38 61 3.4 disqualified 2.6 72 26 false(no-overflow) .21 15 2.3 false(no-overflow) 8.7 370 70 false(no-overflow) 8.0 340 53 false(no-overflow) 8.1 350 62 false(no-overflow) 4.4 170 41
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .14  26 1.1  false(no-overflow) .062 9.3 .57 false(no-overflow) .095 10   .51 false(no-overflow) 4.3 280 38 false(no-overflow) .14 34 1.5 unknown .028 4.6 .25 unknown .051 4.6 .14  false(no-overflow) .090 26 .99 false(no-overflow) .39 83 4.3 false(no-overflow) 4.2 280 37 false(no-overflow) .39 61 3.5 disqualified 2.7 75 33 false(no-overflow) .19 16 1.9 false(no-overflow) 9.2 380 62 false(no-overflow) 8.8 360 69 false(no-overflow) 7.6 350 69 false(no-overflow) 4.3 170 50
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .11  25 1.1  false(no-overflow) .12  9.4 .42 false(no-overflow) .061 9.3 .79 false(no-overflow) 4.2 290 37 false(no-overflow) .16 33 1.6 unknown .046 4.6 .17 unknown .044 4.6 .13  false(no-overflow) .083 26 1.0  false(no-overflow) .82 83 10   false(no-overflow) 4.3 280 38 false(no-overflow) .38 61 3.7 disqualified 2.7 75 33 false(no-overflow) .21 16 2.3 false(no-overflow) 8.4 360 65 false(no-overflow) 7.9 350 61 false(no-overflow) 8.9 360 64 false(no-overflow) 4.5 170 42
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .11  25 .95 false(no-overflow) .059 9.7 .60 false(no-overflow) .062 8.9 .60 false(no-overflow) 3.8 280 34 false(no-overflow) .15 34 1.9 unknown .031 4.6 .30 unknown .029 4.6 .22  false(no-overflow) .077 26 .92 timeout 900    230 9700   false(no-overflow) 3.7 280 36 false(no-overflow) .40 61 4.4 disqualified 2.6 72 29 false(no-overflow) .19 16 2.6 false(no-overflow) 7.7 340 59 false(no-overflow) 7.7 340 68 false(no-overflow) 8.4 350 71 false(no-overflow) 4.4 160 45
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .12  25 .96 false(no-overflow) .061 9.7 .55 false(no-overflow) .076 8.9 .56 false(no-overflow) 4.0 280 37 false(no-overflow) .14 34 1.5 unknown .044 4.6 .16 unknown .031 4.6 .18  false(no-overflow) .095 26 .72 timeout 900    250 10000   false(no-overflow) 3.9 280 34 false(no-overflow) .38 61 3.1 disqualified 2.6 72 31 false(no-overflow) .19 16 2.1 false(no-overflow) 7.9 340 64 false(no-overflow) 7.5 330 55 false(no-overflow) 7.6 350 70 false(no-overflow) 4.5 170 45
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .12  25 1.1  false(no-overflow) .068 9.8 .55 false(no-overflow) .063 9.1 .60 false(no-overflow) 4.0 280 37 false(no-overflow) .14 34 1.7 unknown .033 4.6 .27 unknown .029 4.6 .20  false(no-overflow) .084 26 .89 false(no-overflow) .40 83 5.2 false(no-overflow) 4.2 290 36 false(no-overflow) .38 61 4.1 disqualified 2.7 73 32 false(no-overflow) .19 16 2.1 false(no-overflow) 8.9 370 68 false(no-overflow) 8.5 370 69 false(no-overflow) 9.2 370 70 false(no-overflow) 4.7 170 50
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .11  26 .99 false(no-overflow) .071 9.7 .53 false(no-overflow) .065 9.1 .55 false(no-overflow) 4.0 280 35 false(no-overflow) .14 34 1.5 unknown .031 4.6 .14 unknown .030 4.7 .20  false(no-overflow) .080 26 .89 false(no-overflow) .40 83 4.5 false(no-overflow) 4.0 280 38 false(no-overflow) .39 61 4.2 disqualified 2.6 72 31 false(no-overflow) .20 16 2.3 false(no-overflow) 8.9 370 62 false(no-overflow) 8.1 360 61 false(no-overflow) 8.0 380 72 false(no-overflow) 4.5 160 44
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .12  25 1.0  false(no-overflow) .062 9.8 .69 false(no-overflow) .064 8.7 .50 false(no-overflow) 4.0 280 38 false(no-overflow) .14 34 1.9 unknown .024 4.7 .18 unknown .033 4.6 .29  false(no-overflow) .077 26 .87 false(no-overflow) .41 82 4.8 false(no-overflow) 4.2 280 39 false(no-overflow) .39 61 3.5 disqualified 2.7 73 30 false(no-overflow) .18 17 2.0 false(no-overflow) 9.0 380 65 false(no-overflow) 8.6 370 64 false(no-overflow) 8.7 370 70 false(no-overflow) 4.6 170 44
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .12  26 .87 false(no-overflow) .15  7.6 .33 false(no-overflow) .13  8.8 .41 false(no-overflow) 3.9 280 35 false(no-overflow) .16 34 1.9 unknown .046 4.6 .20 unknown .041 4.6 .14  false(no-overflow) .090 26 1.4  false(no-overflow) .40 83 5.0 false(no-overflow) 4.0 280 34 false(no-overflow) .37 61 4.3 disqualified 2.6 72 35 false(no-overflow) .21 17 2.1 false(no-overflow) 8.9 370 63 false(no-overflow) 7.8 350 65 false(no-overflow) 8.7 370 70 false(no-overflow) 4.3 170 41
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .14  25 1.7  false(no-overflow) .064 9.6 .51 false(no-overflow) .058 9.4 .58 false(no-overflow) 4.3 280 36 false(no-overflow) .14 34 1.5 unknown .032 4.6 .21 unknown .034 4.6 .17  false(no-overflow) .10  26 .82 false(no-overflow) .41 83 4.6 false(no-overflow) 4.2 280 38 false(no-overflow) .39 61 3.7 disqualified 2.7 73 32 false(no-overflow) .18 15 2.5 false(no-overflow) 9.2 380 78 false(no-overflow) 8.3 360 64 false(no-overflow) 8.0 360 60 timeout 900   170 14000
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true .10  26 1.1  true .078 6.4 .32 witness invalid (true) .045 7.3 .33 true 3.5 270 34 unknown .79 67 8.5 unknown .034 4.6 .26 unknown .033 4.7 .25  true .085 26 .87 timeout 900    240 9800   true 3.6 280 35 true .39 61 3.4 disqualified 2.0 67 24 true .14 15 1.7 true 7.1 330 60 true 8.6 360 63 true 8.3 370 65 timeout 900   170 11000
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true .099 25 .85 true .069 5.9 .30 true .087 6.4 .37 true 3.7 280 35 unknown .81 67 8.7 unknown .037 4.5 .14 unknown .055 4.6 .15  true .084 26 .95 timeout 900    230 9900   true 3.9 280 32 true .38 61 3.7 disqualified 2.0 67 23 true .17 16 2.1 true 8.7 380 71 true 8.9 350 62 true 8.8 360 70 timeout 900   170 11000
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true .10  25 .83 true .052 6.5 .38 true .095 7.0 .32 true 3.7 280 34 unknown .80 66 8.8 unknown .033 4.6 .19 unknown .039 4.8 .22  true .081 26 .84 timeout 900    240 9500   true 3.7 280 32 true .38 61 4.1 disqualified 2.0 68 25 true .15 16 2.0 true 8.8 370 64 true 8.5 370 63 true 8.5 350 63 timeout 900   160 11000
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true .096 25 1.0  true .048 7.4 .47 true .051 7.3 .37 true 3.4 270 35 unknown .80 66 9.3 unknown .029 4.6 .21 unknown .032 4.6 .27  true .082 26 1.2  timeout 900    250 9900   true 3.4 270 33 true .38 61 3.6 disqualified 2.0 67 24 true .16 16 1.9 true 8.3 350 62 true 8.3 370 62 true 8.3 360 63 timeout 900   170 12000
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true .10  25 .92 true .059 6.4 .40 true .054 7.1 .34 true 3.6 280 34 unknown .81 65 9.7 unknown .047 4.6 .18 unknown .032 4.6 .20  true .084 26 .83 timeout 900    230 10000   true 3.8 280 36 true .40 61 3.0 disqualified 2.1 68 26 true .15 16 2.4 true 8.7 370 64 true 9.2 360 63 true 7.9 350 60 timeout 900   170 13000
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .12  24 .93 false(no-overflow) .077 9.2 .44 false(no-overflow) .12  7.4 .37 false(no-overflow) 3.0 270 28 false(no-overflow) .14 34 1.5 unknown .029 4.6 .21 unknown .027 4.7 .26  false(no-overflow) .083 26 1.2  false(no-overflow) .40 83 4.4 false(no-overflow) 3.1 270 29 false(no-overflow) .38 59 3.2 disqualified 3.1 110 40 false(no-overflow) .23 18 2.7 false(no-overflow) 7.7 360 61 false(no-overflow) 7.9 370 55 false(no-overflow) 7.8 360 65 false(no-overflow) 3.5 150 38
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .16  24 1.0  false(no-overflow) .091 9.2 .80 false(no-overflow) .087 9.0 .70 false(no-overflow) 3.1 260 31 false(no-overflow) .21 33 2.0 unknown .052 4.6 .25 unknown .028 4.6 .17  false(no-overflow) .14  26 1.6  false(no-overflow) .43 83 4.6 false(no-overflow) 3.0 270 30 false(no-overflow) .35 58 4.4 disqualified 3.4 85 44 false(no-overflow) .26 18 2.3 false(no-overflow) 7.8 370 64 false(no-overflow) 7.0 340 61 false(no-overflow) 7.6 370 62 false(no-overflow) 3.5 150 40
termination-crafted/Ackermann_false-no-overflow.c error (5) .095 24 .86 false(no-overflow) .095 9.9 .91 false(no-overflow) .058 9.4 .58 timeout 900   3400 9800 false(no-overflow) .13 33 1.8 unknown .030 4.6 .19 unknown .032 4.7 .27  false(no-overflow) .080 26 1.1  false(no-overflow) 44    130 550   timeout 900   3600 10000 false(no-overflow) .38 59 3.4 disqualified 2.7 76 40 false(no-overflow) .28 18 3.3 false(no-overflow) 7.2 360 56 false(no-overflow) 7.0 330 53 false(no-overflow) 6.4 330 51 timeout 900   150 11000
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .067 9.8 .48 false(no-overflow) .067 9.2 .54 false(no-overflow) 3.2 270 28 false(no-overflow) .13 33 1.7 unknown .030 4.6 .17 unknown .031 4.6 .20  false(no-overflow) .10  26 .76 timeout 900    74 9600   false(no-overflow) 3.0 270 31 false(no-overflow) .35 59 3.1 disqualified 880   1100 10000 false(no-overflow) .24 18 3.3 false(no-overflow) 7.6 360 65 false(no-overflow) 7.5 350 67 false(no-overflow) 7.6 360 68 false(no-overflow) 12   150 140
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .15  23 .93 false(no-overflow) .083 9.4 .42 false(no-overflow) .063 9.8 .48 false(no-overflow) 3.0 270 25 false(no-overflow) .14 33 1.4 unknown .029 4.6 .21 unknown .029 4.6 .23  false(no-overflow) .078 26 .92 timeout 900    75 10000   false(no-overflow) 3.2 260 33 false(no-overflow) .40 59 3.3 disqualified 3.1 77 47 false(no-overflow) .24 18 3.3 false(no-overflow) 7.3 340 55 false(no-overflow) 7.3 350 55 false(no-overflow) 7.7 360 56 false(no-overflow) 8.6 150 100
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .080 9.4 .56 false(no-overflow) .062 10   .62 false(no-overflow) 2.9 270 27 false(no-overflow) .14 34 1.6 unknown .037 4.6 .19 unknown .029 4.7 .21  false(no-overflow) .085 26 .80 timeout 900    80 12000   false(no-overflow) 3.1 270 30 false(no-overflow) .37 59 3.2 disqualified 3.1 84 44 false(no-overflow) .26 17 2.7 false(no-overflow) 7.8 370 61 false(no-overflow) 8.2 370 67 false(no-overflow) 7.5 340 58 false(no-overflow) 3.6 150 41
termination-crafted/Binary_Search_false-no-overflow.c error (5) .090 24 .76 false(no-overflow) .10  9.4 .97 false(no-overflow) .068 9.1 .60 false(no-overflow) 2.9 270 31 false(no-overflow) .17 34 1.7 unknown .037 4.7 .26 unknown .054 4.6 .14  false(no-overflow) .11  26 1.3  false(no-overflow) 570    130 6700   false(no-overflow) 3.1 270 31 false(no-overflow) .36 59 3.7 disqualified 2.7 74 39 false(no-overflow) .24 19 2.8 false(no-overflow) 7.5 370 60 false(no-overflow) 7.9 360 69 false(no-overflow) 8.0 370 63 false(no-overflow) 3.5 150 35
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .14  24 1.1  false(no-overflow) .12  8.4 .28 false(no-overflow) .068 9.4 .43 false(no-overflow) 3.2 270 29 false(no-overflow) .38 35 4.0 unknown .028 4.7 .20 unknown .030 4.6 .19  false(no-overflow) .090 26 .97 false(no-overflow) 210    100 2400   false(no-overflow) 3.2 270 28 false(no-overflow) .35 59 3.1 disqualified 3.1 79 43 false(no-overflow) .25 18 2.6 false(no-overflow) 7.7 350 58 false(no-overflow) 8.6 370 64 false(no-overflow) 7.8 370 58 false(no-overflow) 95   150 1100
termination-crafted/Cairo_step2_false-no-overflow.c timeout 900     1300 11000    error (42) 880     4500   4100    error (42) 880     110   11000    timeout 910   2500 11000 unknown 41    40 520   unknown .028 4.7 .26 unknown .029 4.6 .21  timeout 900     480 12000    false(no-overflow) 180    77 2100   timeout 910   2600 12000 timeout 900    410 4100   disqualified 880   600 11000 timeout (verification) 900    260 11000   timeout 900   1200 14000 timeout 900   3800 10000 timeout 900   1100 12000 timeout 900   150 10000
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .12  24 .99 false(no-overflow) .086 9.4 .73 false(no-overflow) .075 9.5 .44 false(no-overflow) 3.3 280 30 false(no-overflow) .16 33 2.5 unknown .059 4.6 .17 unknown .026 4.6 .18  false(no-overflow) .11  26 1.1  false(no-overflow) .40 79 6.0 false(no-overflow) 3.3 280 34 false(no-overflow) .43 60 3.5 disqualified 3.1 80 41 false(no-overflow) .24 18 2.8 false(no-overflow) 7.3 330 65 false(no-overflow) 7.0 340 61 false(no-overflow) 8.8 370 67 false(no-overflow) 3.6 150 35
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .16  24 1.0  false(no-overflow) .078 8.9 .49 false(no-overflow) .063 9.6 .54 false(no-overflow) 3.0 270 31 false(no-overflow) .13 33 1.5 unknown .036 4.7 .13 unknown .030 4.6 .20  false(no-overflow) .081 26 .80 timeout 900    74 11000   false(no-overflow) 3.0 270 27 false(no-overflow) .35 59 3.7 disqualified 3.1 82 43 false(no-overflow) .22 17 2.8 false(no-overflow) 7.2 340 56 false(no-overflow) 7.5 350 64 false(no-overflow) 7.9 370 68 false(no-overflow) 10   150 120
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .13  24 1.3  false(no-overflow) .071 9.4 .61 false(no-overflow) .12  9.1 .40 false(no-overflow) 3.0 270 27 false(no-overflow) .18 34 2.1 unknown .057 4.6 .14 unknown .027 4.6 .21  false(no-overflow) .13  26 1.3  false(no-overflow) 820    78 12000   false(no-overflow) 3.1 270 30 false(no-overflow) .37 59 4.0 disqualified 3.2 82 41 false(no-overflow) .24 18 2.9 false(no-overflow) 7.8 350 58 false(no-overflow) 7.8 350 62 false(no-overflow) 7.7 360 64 false(no-overflow) 3.5 150 36
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .081 9.6 .69 false(no-overflow) .057 9.6 .59 false(no-overflow) 3.0 270 30 false(no-overflow) .20 33 3.1 unknown .030 4.6 .18 unknown .051 4.5 .24  false(no-overflow) .13  26 2.2  false(no-overflow) 210    83 3300   false(no-overflow) 3.1 270 25 false(no-overflow) .40 59 3.2 disqualified 3.2 81 36 false(no-overflow) .24 17 2.0 false(no-overflow) 7.4 350 61 false(no-overflow) 7.4 350 56 false(no-overflow) 7.6 350 59 false(no-overflow) 5.0 150 52
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .12  24 .89 false(no-overflow) .057 9.5 .46 false(no-overflow) .068 9.2 .45 false(no-overflow) 3.0 270 26 false(no-overflow) .14 33 1.7 unknown .027 4.6 .18 unknown .031 4.6 .26  false(no-overflow) .086 26 .74 false(no-overflow) .39 83 5.2 false(no-overflow) 3.0 270 31 false(no-overflow) .37 59 3.2 disqualified 3.1 110 39 false(no-overflow) .23 18 2.8 false(no-overflow) 7.4 360 58 false(no-overflow) 7.7 360 58 false(no-overflow) 7.6 370 60 false(no-overflow) 3.3 150 33
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .11  24 1.3  false(no-overflow) .074 9.9 .65 false(no-overflow) .077 9.8 .42 false(no-overflow) 3.0 270 32 false(no-overflow) .15 34 1.9 unknown .056 4.7 .16 unknown .030 4.6 .16  false(no-overflow) .092 26 1.0  false(no-overflow) .40 83 5.0 false(no-overflow) 3.1 270 30 false(no-overflow) .36 59 3.4 disqualified 3.1 84 38 false(no-overflow) .24 19 2.8 false(no-overflow) 7.2 340 63 false(no-overflow) 7.2 330 52 false(no-overflow) 8.0 370 64 false(no-overflow) 3.4 150 34
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .11  24 .99 false(no-overflow) .071 9.6 .62 false(no-overflow) .066 8.9 .54 false(no-overflow) 3.1 270 27 false(no-overflow) .19 33 2.1 unknown .028 4.6 .23 unknown .030 4.6 .18  false(no-overflow) .11  26 1.2  false(no-overflow) .39 82 4.6 false(no-overflow) 3.0 270 29 false(no-overflow) .35 59 4.3 disqualified 3.1 84 40 false(no-overflow) .23 18 2.8 false(no-overflow) 7.1 340 55 false(no-overflow) 6.7 320 58 false(no-overflow) 7.9 370 65 false(no-overflow) 3.2 150 35
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .074 9.3 .47 false(no-overflow) .092 9.2 .36 false(no-overflow) 3.0 280 31 false(no-overflow) .14 34 1.5 unknown .053 4.6 .16 unknown .046 4.6 .17  false(no-overflow) .087 26 1.0  false(no-overflow) 140    4500 1500   false(no-overflow) 3.0 270 28 false(no-overflow) .38 59 3.0 disqualified 3.1 78 45 false(no-overflow) .22 19 2.7 false(no-overflow) 8.2 370 67 false(no-overflow) 7.9 370 61 false(no-overflow) 8.4 380 68 false(no-overflow) 92   150 1200
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .11  24 1.1  false(no-overflow) .071 11   .50 false(no-overflow) .13  8.9 .34 false(no-overflow) 3.0 270 26 false(no-overflow) .16 33 1.8 unknown .037 4.8 .20 unknown .049 4.6 .13  false(no-overflow) .10  26 1.1  timeout 900    83 11000   false(no-overflow) 3.1 270 29 false(no-overflow) .36 59 3.7 disqualified 3.1 83 38 false(no-overflow) .23 18 2.8 false(no-overflow) 7.6 370 66 false(no-overflow) 7.8 370 56 false(no-overflow) 7.9 370 65 false(no-overflow) 3.7 160 37
termination-crafted/NestedRecursion_1a_false-no-overflow.c error (5) .092 24 .88 false(no-overflow) .084 9.7 .84 false(no-overflow) .11  8.7 .47 false(no-overflow) 3.1 270 25 false(no-overflow) .14 33 1.8 unknown .037 4.6 .20 unknown .027 4.8 .16  false(no-overflow) .080 26 .86 false(no-overflow) 13    91 160   false(no-overflow) 3.0 270 27 false(no-overflow) .35 59 4.0 disqualified 2.7 75 33 false(no-overflow) .24 18 3.3 false(no-overflow) 8.3 360 64 false(no-overflow) 8.3 350 67 false(no-overflow) 7.3 340 55 false(no-overflow) 7.6 200 80
termination-crafted/NestedRecursion_2a_false-no-overflow.c error (5) .085 23 .76 false(no-overflow) .065 9.9 .59 false(no-overflow) .066 10   .51 false(no-overflow) 3.1 280 31 false(no-overflow) .13 34 1.6 unknown .036 4.6 .14 unknown .028 4.6 .17  false(no-overflow) .090 26 .81 false(no-overflow) 6.8  91 84   false(no-overflow) 3.2 280 29 false(no-overflow) .37 59 4.1 disqualified 2.6 73 33 false(no-overflow) .24 18 2.5 false(no-overflow) 7.8 360 62 false(no-overflow) 8.2 360 62 false(no-overflow) 8.3 360 69 false(no-overflow) 3.6 150 33
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .11  24 1.2  false(no-overflow) .066 9.4 .70 false(no-overflow) .079 9.2 .34 false(no-overflow) 3.3 280 34 false(no-overflow) .14 34 1.6 unknown .043 4.6 .14 unknown .032 4.6 .21  false(no-overflow) .10  26 .74 false(no-overflow) .42 82 4.5 false(no-overflow) 3.3 280 31 false(no-overflow) .36 58 3.6 disqualified 4.4 80 50 false(no-overflow) .22 19 2.6 false(no-overflow) 6.4 340 57 false(no-overflow) 8.2 360 59 false(no-overflow) 6.7 350 51 false(no-overflow) 3.3 150 33
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .12  24 .98 false(no-overflow) .089 9.3 .51 false(no-overflow) .070 9.6 .46 false(no-overflow) 3.3 280 31 false(no-overflow) .13 33 1.5 unknown .031 4.7 .24 unknown .056 4.6 .25  false(no-overflow) .084 26 .73 false(no-overflow) .42 78 4.8 false(no-overflow) 3.3 280 33 false(no-overflow) .40 59 3.1 disqualified 3.1 80 37 false(no-overflow) .23 18 2.7 false(no-overflow) 7.9 360 67 false(no-overflow) 8.2 370 71 false(no-overflow) 8.0 350 65 false(no-overflow) 3.5 150 32
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) .43  30 5.1  false(no-overflow) .14  9.9 1.7  false(no-overflow) .15  9.7 1.2  false(no-overflow) 200   1300 1500 false(no-overflow) 15    55 210   unknown .047 4.8 .26 unknown .055 4.7 .17  false(no-overflow) .11  26 1.3  false(no-overflow) .40 82 5.0 false(no-overflow) 210   1200 1500 false(no-overflow) .39 59 3.9 disqualified 140   450 1200 false(no-overflow) .18 16 2.0 false(no-overflow) 27   800 270 false(no-overflow) 590   3400 4800 false(no-overflow) 59   1500 650 false(no-overflow) 3.3 150 34
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .12  24 .99 false(no-overflow) .075 9.0 .55 false(no-overflow) .070 8.5 .39 false(no-overflow) 3.1 270 30 false(no-overflow) .14 34 1.4 unknown .035 4.6 .27 unknown .030 4.6 .31  false(no-overflow) .084 26 .75 false(no-overflow) 170    78 2000   false(no-overflow) 3.0 270 31 false(no-overflow) .37 59 3.1 disqualified 880   1900 10000 false(no-overflow) .22 17 2.5 false(no-overflow) 7.6 350 57 false(no-overflow) 7.5 360 56 false(no-overflow) 7.9 360 65 error (1) 51   150 610
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .11  24 1.1  false(no-overflow) .091 8.4 .33 false(no-overflow) .067 8.9 .48 false(no-overflow) 3.1 270 28 false(no-overflow) .14 33 1.5 unknown .057 4.6 .18 unknown .045 4.6 .17  false(no-overflow) .077 26 .95 timeout 900    75 8900   false(no-overflow) 3.0 270 31 false(no-overflow) .35 59 4.1 disqualified 3.0 77 39 false(no-overflow) .27 20 2.5 false(no-overflow) 8.6 370 64 false(no-overflow) 8.1 360 57 false(no-overflow) 7.7 370 64 false(no-overflow) 12   150 140
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 900     1200 11000    error (42) 880     4400   4400    error (42) 880     100   9500    timeout 900   2000 12000 unknown 34    40 490   unknown .028 4.7 .16 unknown .035 4.6 .24  timeout 900     480 11000    false(no-overflow) 220    77 2600   timeout 900   2000 12000 timeout 900    400 3800   disqualified 880   700 12000 false(no-overflow) .21 18 3.0 timeout 900   1200 13000 timeout 900   5200 12000 timeout 900   1100 12000 timeout 900   150 13000
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) .11  24 1.2  false(no-overflow) .089 9.1 .39 out of memory 860     15000   11000    false(no-overflow) 3.1 270 27 false(no-overflow) .14 34 1.5 unknown .030 4.6 .17 unknown .028 4.6 .15  false(no-overflow) .081 26 .92 false(no-overflow) 120    4000 1400   false(no-overflow) 3.1 270 32 timeout 900    360 4600   disqualified 3.1 83 40 false(no-overflow) .27 18 2.8 false(no-overflow) 7.1 340 56 false(no-overflow) 7.8 360 55 false(no-overflow) 7.9 350 61 timeout 900   150 12000
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .11  24 1.1  false(no-overflow) .076 10   .41 false(no-overflow) .061 9.3 .58 false(no-overflow) 3.2 270 30 false(no-overflow) .13 34 1.6 unknown .047 4.6 .17 unknown .032 4.6 .21  false(no-overflow) .082 26 .95 false(no-overflow) 35    78 400   false(no-overflow) 3.1 270 32 false(no-overflow) .37 58 2.7 disqualified 880   1400 9000 false(no-overflow) .23 17 4.6 false(no-overflow) 6.4 330 54 false(no-overflow) 7.8 360 62 false(no-overflow) 6.9 350 52 false(no-overflow) 6.6 150 72
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .13  24 .88 false(no-overflow) .077 9.6 .51 false(no-overflow) .058 9.2 .55 false(no-overflow) 3.0 260 25 false(no-overflow) .14 34 1.6 unknown .045 4.6 .21 unknown .033 4.6 .17  false(no-overflow) .099 26 .83 false(no-overflow) 110    4400 1300   false(no-overflow) 3.1 270 31 false(no-overflow) .34 59 3.1 disqualified 3.2 86 47 false(no-overflow) .26 17 2.8 false(no-overflow) 8.1 360 62 false(no-overflow) 7.1 340 51 false(no-overflow) 8.0 370 63 timeout 900   150 12000
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .11  23 1.2  false(no-overflow) .072 9.4 .43 false(no-overflow) .12  8.3 .30 false(no-overflow) 3.1 270 27 false(no-overflow) .14 33 1.4 unknown .053 4.7 .18 unknown .034 4.7 .11  false(no-overflow) .083 26 .85 timeout 900    4000 11000   false(no-overflow) 3.1 270 27 false(no-overflow) .37 59 3.0 disqualified 3.1 77 36 false(no-overflow) .22 18 3.2 false(no-overflow) 7.6 360 63 false(no-overflow) 6.5 330 57 false(no-overflow) 7.8 360 65 false(no-overflow) 3.9 150 37
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .12  24 .94 false(no-overflow) .077 9.7 .47 false(no-overflow) .068 9.3 .49 false(no-overflow) 3.1 270 29 false(no-overflow) .15 33 2.3 unknown .028 4.6 .18 unknown .030 4.6 .18  false(no-overflow) .10  26 .79 false(no-overflow) 140    4500 1500   false(no-overflow) 2.9 270 27 false(no-overflow) .36 59 3.4 disqualified 3.1 82 37 false(no-overflow) .24 23 2.7 false(no-overflow) 7.9 370 65 false(no-overflow) 6.9 340 53 false(no-overflow) 8.0 360 57 false(no-overflow) 8.8 150 94
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .11  24 1.8  false(no-overflow) .073 9.5 .58 false(no-overflow) .12  8.6 .33 false(no-overflow) 3.2 270 32 false(no-overflow) .16 33 1.9 unknown .045 4.6 .18 unknown .061 4.7 .21  false(no-overflow) .10  26 1.3  false(no-overflow) .41 83 5.2 false(no-overflow) 3.1 270 30 false(no-overflow) .36 59 3.3 disqualified 3.2 83 36 false(no-overflow) .24 17 2.7 false(no-overflow) 7.2 340 60 false(no-overflow) 7.4 350 64 false(no-overflow) 6.6 330 52 false(no-overflow) 3.6 150 34
termination-crafted/RecursiveMultiplication_false-no-overflow.c error (5) .12  24 .71 false(no-overflow) .078 9.5 .65 false(no-overflow) .13  8.1 .31 false(no-overflow) 3.5 290 38 false(no-overflow) .16 33 1.5 unknown .055 4.6 .12 unknown .032 4.6 .21  false(no-overflow) .11  26 .74 false(no-overflow) 46    300 550   false(no-overflow) 3.6 290 33 false(no-overflow) .37 59 2.9 disqualified 2.7 77 40 false(no-overflow) .27 18 3.0 false(no-overflow) 6.7 330 52 false(no-overflow) 7.0 350 58 false(no-overflow) 7.5 360 68 false(no-overflow) 4.3 200 40
termination-crafted/RecursiveNonterminating_false-no-overflow.c error (5) .080 24 .93 false(no-overflow) .095 9.0 .52 false(no-overflow) .065 9.4 .43 false(no-overflow) 3.0 270 28 false(no-overflow) .14 33 1.6 unknown .033 4.6 .17 unknown .028 4.6 .24  false(no-overflow) .089 26 .79 false(no-overflow) 88    91 1000   false(no-overflow) 3.8 270 52 false(no-overflow) .36 59 3.3 disqualified 2.7 72 33 false(no-overflow) .28 22 2.3 false(no-overflow) 7.2 330 63 false(no-overflow) 7.8 360 60 false(no-overflow) 8.2 370 60 false(no-overflow) 13   150 150
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .12  24 .94 false(no-overflow) .072 8.7 .33 false(no-overflow) .080 9.5 .46 false(no-overflow) 2.9 270 26 false(no-overflow) .14 34 1.5 unknown .032 4.8 .12 unknown .032 4.7 .18  false(no-overflow) .078 26 .89 timeout 900    74 10000   false(no-overflow) 3.1 270 27 false(no-overflow) .36 59 3.1 disqualified 3.1 76 39 false(no-overflow) .23 17 2.7 false(no-overflow) 8.0 370 63 false(no-overflow) 7.2 340 66 false(no-overflow) 7.7 360 56 error (1) 51   150 440
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .066 9.5 .51 false(no-overflow) .068 9.0 .35 false(no-overflow) 3.1 270 27 false(no-overflow) .15 33 2.1 unknown .046 4.6 .14 unknown .054 4.6 .21  false(no-overflow) .10  26 1.1  false(no-overflow) .41 83 4.7 false(no-overflow) 3.0 270 28 false(no-overflow) .40 59 3.2 disqualified 3.1 83 40 false(no-overflow) .25 18 2.7 false(no-overflow) 8.0 370 58 false(no-overflow) 7.1 340 54 false(no-overflow) 7.7 360 58 false(no-overflow) 3.7 150 36
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .15  24 .97 false(no-overflow) .11  9.2 .49 false(no-overflow) .074 8.8 .71 false(no-overflow) 2.8 270 27 false(no-overflow) .15 34 1.6 unknown .026 4.6 .21 unknown .034 4.6 .25  false(no-overflow) .092 26 1.1  false(no-overflow) .41 83 4.6 false(no-overflow) 3.0 270 30 false(no-overflow) .37 59 3.8 disqualified 12   120 160 false(no-overflow) .22 18 2.8 false(no-overflow) 7.8 360 63 false(no-overflow) 8.0 370 65 false(no-overflow) 7.8 360 59 false(no-overflow) 3.4 150 34
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .12  24 1.3  false(no-overflow) .076 10   .50 false(no-overflow) .070 8.8 .43 false(no-overflow) 3.0 270 28 false(no-overflow) .16 33 1.7 unknown .048 4.6 .17 unknown .033 4.6 .15  false(no-overflow) .10  26 1.3  false(no-overflow) .41 83 5.7 false(no-overflow) 2.9 270 29 false(no-overflow) .38 58 3.3 disqualified 880   440 11000 false(no-overflow) .22 18 2.4 false(no-overflow) 7.2 350 59 false(no-overflow) 7.4 350 61 false(no-overflow) 6.8 330 62 false(no-overflow) 3.4 150 33
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .12  24 .93 false(no-overflow) .10  9.7 .38 false(no-overflow) .16  8.6 .30 false(no-overflow) 2.9 260 27 false(no-overflow) .15 34 2.0 unknown .036 4.6 .23 unknown .051 4.6 .20  false(no-overflow) .10  26 1.3  false(no-overflow) .40 79 5.1 false(no-overflow) 3.0 270 25 false(no-overflow) .37 59 2.7 disqualified 11   110 140 false(no-overflow) .22 19 2.5 false(no-overflow) 7.9 370 63 false(no-overflow) 8.1 360 62 false(no-overflow) 7.6 370 61 false(no-overflow) 3.4 200 35
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .12  24 1.2  false(no-overflow) .078 9.3 .50 false(no-overflow) .094 9.1 .54 false(no-overflow) 3.1 270 31 false(no-overflow) .20 34 2.0 unknown .048 4.6 .21 unknown .031 4.6 .16  false(no-overflow) .13  26 1.0  timeout 900    78 11000   false(no-overflow) 3.1 270 32 false(no-overflow) .35 59 3.2 disqualified 3.1 85 43 false(no-overflow) .23 18 2.7 false(no-overflow) 7.8 370 61 false(no-overflow) 8.2 370 55 false(no-overflow) 7.3 340 51 false(no-overflow) 220   200 3000
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .12  24 .96 false(no-overflow) .078 10   .46 false(no-overflow) .067 9.0 .70 false(no-overflow) 3.1 270 26 false(no-overflow) .14 33 2.0 unknown .031 4.6 .17 unknown .029 4.6 .18  false(no-overflow) .098 26 .84 false(no-overflow) .39 83 5.1 false(no-overflow) 3.0 270 26 false(no-overflow) .35 58 3.5 disqualified 3.2 84 38 false(no-overflow) .23 18 2.7 false(no-overflow) 7.8 370 61 false(no-overflow) 7.5 340 61 false(no-overflow) 7.5 360 61 false(no-overflow) 3.6 150 40
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .15  24 1.0  false(no-overflow) .075 9.5 .52 false(no-overflow) .065 9.1 .61 false(no-overflow) 3.0 270 28 false(no-overflow) .14 34 1.5 unknown .030 4.6 .20 unknown .031 4.6 .21  false(no-overflow) .083 26 .88 false(no-overflow) 77    82 1200   false(no-overflow) 3.1 270 26 false(no-overflow) .36 59 3.7 disqualified 3.1 84 40 false(no-overflow) .24 18 2.9 false(no-overflow) 7.4 340 50 false(no-overflow) 7.9 370 67 false(no-overflow) 7.4 350 55 false(no-overflow) 6.3 150 77
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .14  24 1.0  false(no-overflow) .14  10   .63 false(no-overflow) .082 8.8 .51 false(no-overflow) 3.5 280 35 false(no-overflow) .15 33 1.7 unknown .036 4.6 .25 unknown .029 4.6 .29  false(no-overflow) .11  26 1.0  false(no-overflow) 5.8  83 79   false(no-overflow) 3.6 280 35 false(no-overflow) .36 59 3.9 disqualified 3.5 91 39 false(no-overflow) .26 18 3.4 false(no-overflow) 16   540 140 false(no-overflow) 15   520 140 false(no-overflow) 17   520 150 false(no-overflow) 4.0 160 41
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .13  24 .85 false(no-overflow) .086 9.3 .45 false(no-overflow) .075 8.8 .49 false(no-overflow) 3.0 270 26 false(no-overflow) .17 34 2.1 unknown .049 4.6 .13 unknown .031 4.6 .20  false(no-overflow) .14  26 1.3  timeout 900    4300 11000   false(no-overflow) 3.2 270 28 false(no-overflow) .40 59 3.7 disqualified 3.2 85 45 false(no-overflow) .24 18 2.6 false(no-overflow) 7.7 360 53 false(no-overflow) 6.8 340 56 false(no-overflow) 9.1 370 69 false(no-overflow) 200   150 2300
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .12  24 1.3  false(no-overflow) .071 9.4 .51 false(no-overflow) .072 8.9 .42 false(no-overflow) 2.9 270 27 false(no-overflow) .14 33 1.7 unknown .031 4.6 .13 unknown .029 4.7 .21  false(no-overflow) .12  26 .96 false(no-overflow) 780    5300 10000   false(no-overflow) 3.0 270 32 false(no-overflow) .39 59 3.1 disqualified 3.2 86 40 false(no-overflow) .24 18 3.3 false(no-overflow) 7.7 370 65 false(no-overflow) 7.1 340 61 false(no-overflow) 8.0 370 69 false(no-overflow) 3.7 200 36
termination-crafted/easy2_false-no-overflow.c timeout 900     1600 10000    error (42) 880     2200   4800    error (42) 880     160   11000    timeout 910   13000 11000 unknown 58    48 760   unknown .032 4.5 .27 unknown .049 4.6 .13  timeout 900     1100 11000    timeout 900    75 9400   timeout 910   13000 11000 timeout 900    410 4000   disqualified 880   710 9000 timeout (verification) 900    410 7800   timeout 900   2600 11000 timeout 900   5700 7700 timeout 900   1600 13000 timeout 900   150 10000
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true .18  25 1.6  true .13  8.2 1.5  witness invalid (true) .18  7.4 1.5  true 3.0 270 27 unknown .78 65 8.1 unknown .055 4.6 .15 unknown .054 4.7 .16  true .088 26 1.0  timeout 900    84 10000   true 3.0 270 30 true .77 60 6.4 disqualified 2.4 75 31 true .13 16 1.6 true 7.4 350 59 true 7.1 340 61 true 7.6 370 66 timeout 890   1600 11000
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c true 6.8   200 80    error (42) 880     2800   4600    error (42) 880     1300   12000    true 3.1 270 31 unknown .84 68 8.7 unknown .032 4.6 .19 unknown .032 4.8 .33  timeout 900     1800 13000    timeout 900    87 10000   true 3.2 270 27 timeout 900    770 6700   disqualified 880   1700 6000 timeout (verification) 900    450 7100   true 28   620 250 timeout 900   4600 9500 timeout 900   850 13000 timeout 900   150 11000
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety_true-no-overflow.c true 3.3   96 43    error (42) 880     3100   5000    error (42) 870     780   12000    true 3.1 270 29 unknown .79 66 7.9 unknown .035 4.8 .25 unknown .028 4.8 .19  timeout 900     1600 11000    timeout 900    4000 8200   true 3.1 270 30 timeout 900    1400 5300   disqualified 880   460 11000 timeout (verification) 900    69 11000   true 8.0 350 65 true 8.8 360 66 true 8.2 370 66 timeout 900   150 13000
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c true 3.7   170 42    error (42) 880     4600   4200    error (42) 880     920   9600    timeout 910   6800 11000 unknown .81 66 9.6 unknown .029 4.6 .25 unknown .036 4.6 .23  timeout 900     1200 11000    timeout 900    4800 10000   timeout 910   6800 10000 timeout 900    920 5200   disqualified 880   1800 5500 timeout (verification) 900    200 12000   true 9.8 390 70 timeout 900   5500 10000 true 11   430 92 timeout 900   150 13000
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true .10  24 .80 error (42) 880     4300   5000    error (42) 880     200   12000    true 3.0 270 25 unknown .81 65 8.5 unknown .028 4.7 .17 unknown .030 4.6 .20  timeout 900     140 11000    timeout 900    90 9900   true 3.0 270 26 timeout 900    460 5400   disqualified 880   550 11000 timeout (verification) 900    78 12000   true 9.0 350 64 true 9.5 430 78 true 8.9 360 70 timeout 900   150 12000
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c true .093 24 .90 error (42) 880     4100   4200    error (42) 880     190   11000    true 3.0 270 28 unknown .82 67 8.2 unknown .026 4.6 .21 unknown .029 4.7 .21  timeout 900     220 11000    timeout 900    75 9500   true 3.1 270 23 timeout 900    410 4100   disqualified 880   470 10000 timeout (verification) 900    74 12000   true 9.1 380 65 true 9.6 410 74 true 9.1 380 72 timeout 900   150 9900
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true .17  24 1.8  true .061 6.5 .41 true .058 6.2 .47 true 3.1 270 31 unknown .85 66 9.7 unknown .030 4.6 .13 unknown .054 4.5 .17  true .12  26 1.3  timeout 900    4100 9800   true 3.1 270 29 true .36 59 3.5 disqualified 2.4 76 35 true .21 18 2.8 true 8.2 360 73 true 8.6 350 80 true 8.5 370 61 timeout 900   150 11000
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     300 9900    error (42) 880     2500   5100    error (42) 880     170   11000    timeout 900   5000 11000 unknown 470    63 6500   unknown .046 4.6 .16 unknown .036 4.7 .21  timeout 900     1500 10000    timeout 900    190 9000   timeout 900   5100 11000 timeout 900    390 6500   disqualified 880   840 9300 timeout (verification) 900    430 7700   true 81   620 1000 timeout 900   2100 8300 true 60   810 710 timeout 900   150 11000
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c true .093 24 .84 error (42) 880     6800   6300    error (42) 880     380   6000    true 2.9 270 25 unknown .81 66 7.9 unknown .032 4.6 .19 unknown .055 4.5 .20  timeout 900     890 13000    timeout 900    74 10000   true 2.9 260 26 timeout 900    420 6300   disqualified 2.4 74 29 true .16 17 1.6 true 6.8 320 55 true 6.6 320 53 true 7.4 360 58 timeout 900   150 10000
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1300 12000    error (42) 880     4100   4500    error (42) 880     110   10000    timeout 910   2500 12000 unknown 43    40 540   unknown .028 4.6 .14 unknown .027 4.6 .19  timeout 900     560 10000    timeout 900    75 9700   timeout 900   2300 11000 timeout 900    420 4600   disqualified 880   390 9600 timeout (verification) 900    430 11000   true 8.4 360 70 true 8.6 370 74 true 7.7 360 69 timeout 900   150 10000
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1400 12000    error (42) 880     4500   4800    error (42) 880     120   11000    true 3.0 270 29 unknown 42    40 530   unknown .026 4.6 .23 unknown .034 4.7 .27  timeout 900     480 11000    timeout 900    74 10000   true 3.0 270 28 timeout 900    390 3700   disqualified 880   730 9600 timeout (verification) 900    250 13000   true 8.1 350 59 true 9.1 370 56 true 7.5 330 59 timeout 900   150 11000
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true .10  24 .78 error (42) 880     3200   5000    error (42) 880     220   10000    true 3.0 270 26 unknown .81 66 9.0 unknown .043 4.6 .17 unknown .032 4.6 .19  timeout 900     930 11000    timeout 900    75 11000   true 2.9 270 27 timeout 900    440 4600   disqualified 880   700 9200 timeout (verification) 900    520 8900   true 8.6 350 66 true 9.9 450 93 true 8.3 350 67 timeout 900   150 13000
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c true .099 24 .99 error (42) 880     3600   6500    error (42) 870     350   11000    true 3.1 280 27 unknown .82 67 8.8 unknown .029 4.6 .20 unknown .027 4.6 .20  timeout 900     780 11000    timeout 900    74 8800   true 3.1 280 26 timeout 900    1900 6100   disqualified 880   2200 12000 timeout (verification) 900    680 10000   true 7.2 350 56 true 9.0 380 77 true 7.2 340 55 error (1) 51   150 580
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c true 7.2   270 85    out of memory 52     13000   710    error (42) 880     13000   11000    true 3.2 270 31 unknown .82 66 7.9 unknown .031 4.7 .20 unknown .038 4.6 .22  timeout 900     15000 11000    timeout 900    4300 7800   true 3.1 270 29 timeout 900    14000 9600   disqualified 880   1700 7300 timeout (verification) 900    2700 6200   timeout 900   990 10000 timeout 900   4800 10000 timeout 900   1100 11000 timeout 900   150 11000
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c error (134) .16  24 1.7  out of memory 55     13000   680    error (134) .059 15   .52 timeout 910   6800 12000 unknown 52    60 770   unknown .034 4.7 .16 unknown .029 4.9 .23  timeout 900     5900 13000    timeout 900    4400 5600   timeout 900   6700 11000 timeout 900    14000 9300   disqualified 880   1700 5600 error(unknown, verification-finished) 740    2500 6400   timeout 900   1000 13000 timeout 900   5500 9800 timeout 900   890 14000 error (1) 4.0 200 39
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true .12  24 .83 out of memory 180     15000   2200    out of memory 140     15000   1800    true 3.0 270 27 unknown .84 66 8.9 unknown .028 4.6 .22 unknown .025 4.6 .022 timeout 900     15000 13000    timeout 900    74 7600   true 2.8 270 25 out of memory 840    15000 11000   disqualified 2.3 74 31 true .14 15 1.5 true 7.0 340 57 true 7.4 350 53 true 8.0 370 64 error (1) 51   160 660
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1500 12000    error (42) 880     1400   7600    error (42) 870     4100   11000    timeout 900   560 12000 unknown 510    67 5500   unknown .029 4.7 .19 unknown .030 4.6 .17  timeout 900     160 11000    timeout 900    75 10000   timeout 900   570 14000 out of memory 43    15000 610   disqualified 880   370 10000 timeout (verification) 900    280 12000   timeout 900   1900 13000 timeout 900   3600 8300 timeout 900   1400 12000 timeout 900   150 9900
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .12  24 .57 error (42) 880     1600   3700    error (42) 870     5900   13000    true 3.4 280 28 out of memory 170    15000 2500   unknown .037 4.5 .17 unknown .028 4.6 .17  timeout 900     6400 6900    timeout 900    320 14000   true 3.4 280 30 out of memory 43    15000 660   disqualified 880   180 9700 timeout (verification) 900    290 12000   true 11   380 84 true 9.7 410 71 true 9.9 400 73 timeout 900   150 12000
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     660 7400    error (42) 880     3100   3100    error (42) 880     170   11000    true 3.3 270 34 unknown 470    83 5900   unknown .030 4.6 .19 unknown .051 4.6 .18  timeout 900     1200 13000    timeout 900    76 10000   true 3.4 280 37 timeout 900    390 4800   disqualified 880   770 9200 timeout (verification) 900    440 8100   true 12   550 100 true 24   640 260 true 19   510 180 timeout 900   150 9600
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c error (5) .088 24 .83 error (42) 880     220   3700    error (42) 880     5000   11000    true 4.6 290 39 out of memory 180    15000 2500   unknown .026 4.7 .20 unknown .051 4.6 .27  timeout 900     12000 7700    timeout 900    780 12000   true 4.5 300 48 out of memory 40    15000 570   disqualified 890   240 10000 timeout (verification) 900    520 12000   true 12   510 91 timeout 900   1000 10000 true 13   550 110 timeout 900   460 10000
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .086 24 .79 error (42) 880     220   2900    error (42) 880     5000   11000    true 4.4 300 41 out of memory 180    15000 2100   unknown .033 4.6 .19 unknown .029 4.6 .23  timeout 900     12000 6200    timeout 900    280 10000   true 4.5 300 41 out of memory 42    15000 620   disqualified 890   200 11000 timeout (verification) 900    280 11000   true 21   730 170 timeout 900   1100 11000 true 20   640 180 timeout 900   200 13000
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .088 24 .96 error (42) 880     460   3600    error (42) 880     500   7200    timeout 900   1200 14000 out of memory 160    15000 2000   unknown .054 4.6 .16 unknown .052 4.6 .19  timeout 900     4900 5200    timeout 900    420 12000   timeout 900   1200 10000 out of memory 320    15000 3800   disqualified 880   350 7700 timeout (verification) 900    620 12000   true 16   570 120 timeout 900   1100 9500 true 19   660 150 timeout 900   200 12000
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .085 24 .81 error (42) 880     320   3500    error (42) 880     340   5600    true 3.7 290 34 out of memory 170    15000 2000   unknown .032 4.6 .19 unknown .026 4.6 .28  timeout 900     4800 4700    timeout 900    450 9800   true 3.9 290 41 out of memory 250    15000 3300   disqualified 880   540 7400 timeout (verification) 900    500 7600   true 13   570 99 timeout 900   1200 11000 true 13   570 110 timeout 900   200 13000
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .085 24 .71 error (42) 880     460   4500    error (42) 880     500   6700    timeout 900   1400 10000 out of memory 160    15000 2100   unknown .031 4.7 .21 unknown .037 4.7 .21  timeout 900     4800 8100    timeout 900    480 9900   timeout 900   1800 11000 out of memory 320    15000 4100   disqualified 880   350 8300 timeout (verification) 900    550 8100   true 15   550 130 timeout 900   1100 10000 true 16   570 140 timeout 900   200 11000
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c error (5) .089 24 .89 error (42) 870     860   5300    error (42) 880     690   10000    timeout 900   4100 11000 out of memory 170    15000 2700   unknown .029 4.6 .17 unknown .031 4.6 .19  timeout 900     6000 6000    timeout 900    2300 8400   timeout 900   4000 10000 timeout 900    4600 14000   disqualified 880   240 7800 timeout (verification) 900    4200 10000   true 13   490 120 timeout 900   1200 12000 true 13   500 110 timeout 900   430 13000
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c error (5) .092 24 .78 error (42) 880     4200   6800    error (42) 870     180   11000    timeout 910   4400 12000 out of memory 170    15000 2200   unknown .031 4.7 .19 unknown .027 4.8 .22  timeout 900     15000 8700    timeout 900    1100 11000   timeout 900   4100 11000 out of memory 290    15000 3600   disqualified 880   480 7900 timeout (verification) 900    1000 12000   true 17   520 160 timeout 900   5200 13000 true 36   750 330 timeout 900   150 13000
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true .10  24 1.2  error (42) 880     2300   10000    error (42) 880     880   6500    true 3.2 270 29 unknown .79 67 8.4 unknown .034 4.6 .20 unknown .027 4.7 .22  timeout 900     2200 13000    timeout 900    4500 9100   true 3.1 270 27 timeout 900    880 4400   disqualified 2.5 80 33 true .17 16 1.9 true 8.1 340 61 true 8.8 370 72 true 8.5 360 66 timeout 900   150 12000
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c true .098 24 .96 error (42) 880     4700   4800    error (42) 880     210   10000    true 3.0 270 28 unknown 1.0  66 11   unknown .045 4.6 .17 unknown .028 4.6 .21  timeout 900     190 10000    timeout 900    74 9200   true 3.1 270 26 timeout 900    3400 3400   disqualified 880   3100 9200 timeout (verification) 900    17 11000   true 9.1 370 72 true 8.7 380 80 true 9.0 370 71 timeout 900   150 11000
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true .13  24 .76 error (42) 880     1200   8500    error (42) 870     8200   13000    true 3.0 270 29 unknown .79 67 8.7 unknown .036 4.6 .17 unknown .032 4.6 .19  timeout 900     470 11000    timeout 900    75 9600   true 3.1 270 27 timeout 900    520 5000   disqualified 880   290 9600 timeout (verification) 900    3300 11000   true 8.5 360 70 true 9.1 380 65 true 7.9 350 58 timeout 900   150 11000
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true .10  24 .79 error (42) 880     1200   9700    out of memory 850     15000   13000    true 3.0 270 25 unknown .84 66 7.9 unknown .035 4.6 .29 unknown .033 4.6 .16  timeout 900     500 11000    timeout 900    75 10000   true 3.0 270 28 timeout 900    300 6300   disqualified 880   580 9600 timeout (verification) 900    440 7600   true 8.6 370 66 true 9.5 400 85 true 8.2 360 68 timeout 900   150 11000
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true .14  24 .85 error (42) 880     1800   9400    out of memory 520     15000   6900    true 3.0 270 29 unknown 1.3  66 18   unknown .054 4.6 .25 unknown .031 4.6 .22  timeout 900     240 12000    timeout 900    4500 14000   true 3.0 270 27 timeout 900    210 4500   disqualified 880   350 10000 timeout (verification) 900    280 11000   true 8.1 370 60 true 8.7 360 74 true 8.3 370 64 timeout 890   150 11000
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true .17  25 1.5  error (42) 880     4500   4000    error (42) 880     160   9800    true 3.0 270 29 unknown 28    41 360   unknown .028 4.8 .21 unknown .033 4.6 .20  timeout 900     870 11000    timeout 900    74 9700   true 3.0 270 28 timeout 900    380 4600   disqualified 880   760 12000 timeout (verification) 900    450 10000   true 7.7 360 65 true 8.2 330 61 true 8.4 380 67 error (1) 3.9 200 33
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true .099 24 .94 error (42) 880     2100   7200    out of memory 450     15000   5900    true 3.2 270 30 unknown .89 66 9.0 unknown .056 4.5 .16 unknown .032 4.6 .21  timeout 900     490 14000    timeout 900    5000 10000   true 3.2 270 31 timeout 900    300 7600   disqualified 880   410 10000 timeout (verification) 900    530 11000   true 9.0 360 76 true 9.7 400 85 true 8.7 380 67 timeout 900   150 12000
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true .095 24 .84 error (42) 880     4800   4300    error (42) 880     150   11000    true 3.0 270 25 unknown .78 67 9.3 unknown .031 4.6 .19 unknown .031 4.6 .19  timeout 900     890 11000    timeout 900    75 9400   true 3.1 270 28 timeout 900    350 4300   disqualified 880   640 9300 timeout (verification) 900    440 7300   true 7.6 350 69 true 8.1 370 69 true 8.0 370 59 timeout 900   150 11000
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true .092 23 .78 true .056 7.0 .26 witness invalid (true) .042 6.1 .29 true 2.9 270 29 unknown .81 68 8.6 unknown .030 4.7 .20 unknown .028 4.6 .25  true .082 26 .87 timeout 900    84 9800   true 2.9 270 25 true .34 59 3.5 disqualified 2.0 66 27 true .13 15 1.6 true 7.4 360 60 true 7.9 360 60 true 8.2 350 65 timeout 900   150 13000
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true .096 24 .81 true .053 6.8 .34 witness invalid (true) .047 6.1 .24 true 2.8 260 25 unknown .78 66 8.3 unknown .028 4.6 .19 unknown .024 4.6 .19  out of memory 280     15000 4100    timeout 900    75 7000   true 2.9 270 27 out of memory 60    15000 870   disqualified 2.4 74 30 true .17 16 1.6 true 7.7 370 62 true 7.2 360 56 true 7.3 340 63 error (1) 51   150 640
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true .098 24 .88 true 1.6   50   21    out of memory 180     15000   2800    true 3.0 270 29 unknown .83 66 8.9 unknown .027 4.6 .29 unknown .048 4.6 .21  true .60  26 9.3  timeout 900    2000 9200   true 3.0 270 33 true .38 59 4.5 disqualified 27   170 340 true .19 18 2.5 true 7.3 340 56 true 9.1 350 80 true 8.6 370 59 timeout 900   150 11000
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1700 10000    error (42) 880     2300   4300    error (42) 880     170   12000    timeout 910   13000 11000 unknown 58    49 750   unknown .034 4.6 .19 unknown .026 4.7 .22  timeout 900     1100 12000    timeout 900    75 11000   timeout 910   13000 10000 timeout 900    410 4900   disqualified 880   790 12000 timeout (verification) 900    410 7900   timeout 900   3100 12000 timeout 900   5700 7300 timeout 900   1800 12000 timeout 900   150 13000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .077 10   .63 false(no-overflow) .12  8.0 .33 false(no-overflow) 2.9 270 25 false(no-overflow) .19 33 1.8 unknown .034 4.8 .27 unknown .032 4.6 .18  false(no-overflow) .14  26 1.3  false(no-overflow) 380    4400 4300   false(no-overflow) 3.1 270 31 false(no-overflow) .35 59 4.4 disqualified 3.3 91 41 false(no-overflow) .26 18 2.9 false(no-overflow) 8.2 370 69 false(no-overflow) 7.8 340 70 false(no-overflow) 8.3 370 67 false(no-overflow) 110   150 1400
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .10  9.7 1.1  false(no-overflow) .067 9.0 .56 false(no-overflow) 3.1 270 28 false(no-overflow) .22 34 2.8 unknown .056 4.6 .13 unknown .028 4.6 .18  false(no-overflow) .14  26 1.6  false(no-overflow) 340    4200 3600   false(no-overflow) 3.2 260 32 false(no-overflow) .40 59 3.0 disqualified 3.4 98 42 false(no-overflow) .25 18 2.9 false(no-overflow) 8.4 370 69 false(no-overflow) 8.1 340 63 false(no-overflow) 8.6 360 77 false(no-overflow) 140   150 2100
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .079 9.3 .60 false(no-overflow) .067 9.2 .38 false(no-overflow) 3.0 270 28 false(no-overflow) .17 33 2.3 unknown .053 4.6 .14 unknown .033 4.7 .19  false(no-overflow) .11  26 1.3  timeout 900    4200 13000   false(no-overflow) 3.1 270 31 false(no-overflow) .35 59 4.1 disqualified 3.2 85 39 false(no-overflow) .24 18 3.7 false(no-overflow) 7.8 370 60 false(no-overflow) 7.5 360 55 false(no-overflow) 8.2 360 64 false(no-overflow) 200   150 2600
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .12  24 .97 false(no-overflow) .075 9.6 .51 false(no-overflow) .066 9.7 .59 false(no-overflow) 3.0 270 27 false(no-overflow) .15 33 1.9 unknown .046 4.7 .11 unknown .038 4.5 .095 false(no-overflow) .11  26 1.2  false(no-overflow) 770    4300 10000   false(no-overflow) 2.9 270 25 false(no-overflow) .37 59 3.5 disqualified 3.2 82 50 false(no-overflow) .25 19 2.9 false(no-overflow) 8.2 370 60 false(no-overflow) 7.8 370 64 false(no-overflow) 7.5 370 56 false(no-overflow) 3.4 150 35
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .13  24 .82 false(no-overflow) .084 9.1 .79 false(no-overflow) .072 9.2 .50 false(no-overflow) 3.1 270 31 false(no-overflow) .16 33 1.8 unknown .031 4.7 .21 unknown .054 4.5 .23  false(no-overflow) .10  26 1.1  timeout 900    82 8900   false(no-overflow) 3.1 270 28 false(no-overflow) .37 59 3.2 disqualified 3.4 88 42 false(no-overflow) .26 18 3.9 false(no-overflow) 9.2 380 70 false(no-overflow) 8.6 370 80 false(no-overflow) 8.8 350 77 false(no-overflow) 290   150 4200
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .13  9.4 .43 false(no-overflow) .12  8.5 .37 false(no-overflow) 3.1 270 27 false(no-overflow) .14 33 1.7 unknown .028 4.6 .27 unknown .035 4.5 .20  false(no-overflow) .088 26 .95 false(no-overflow) 220    4400 2500   false(no-overflow) 3.2 270 29 false(no-overflow) .36 59 4.4 disqualified 3.2 86 44 false(no-overflow) .27 18 3.1 false(no-overflow) 7.4 340 67 false(no-overflow) 7.6 370 68 false(no-overflow) 7.6 370 65 timeout 900   150 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .081 9.7 .68 out of memory 310     15000   4600    false(no-overflow) 3.1 270 32 false(no-overflow) .14 34 1.4 unknown .031 4.6 .21 unknown .029 4.6 .20  false(no-overflow) .086 26 .85 false(no-overflow) 640    4200 7300   false(no-overflow) 3.2 270 27 timeout 900    360 4900   disqualified 3.3 89 37 false(no-overflow) .41 18 5.0 false(no-overflow) 8.4 360 71 false(no-overflow) 9.6 380 73 false(no-overflow) 8.1 350 61 timeout 900   150 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 900     1700 10000    error (42) 880     2400   4300    error (42) 880     160   10000    timeout 910   13000 12000 unknown 58    48 810   unknown .033 4.6 .11 unknown .030 4.8 .23  timeout 900     1100 11000    timeout 900    74 9300   timeout 910   13000 11000 timeout 900    420 4500   disqualified 880   710 10000 timeout (verification) 900    430 11000   timeout 900   2500 12000 timeout 900   4400 6000 timeout 900   2400 14000 timeout 900   150 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .11  24 .97 false(no-overflow) .067 9.9 .70 false(no-overflow) .12  7.8 .45 false(no-overflow) 3.0 270 32 false(no-overflow) .14 34 2.0 unknown .054 4.6 .16 unknown .029 4.8 .22  false(no-overflow) .11  26 .80 timeout 900    84 11000   false(no-overflow) 3.2 270 30 false(no-overflow) .41 59 3.2 disqualified 3.2 84 36 false(no-overflow) .24 18 2.5 false(no-overflow) 7.6 360 63 false(no-overflow) 8.9 370 68 false(no-overflow) 7.6 350 65 false(no-overflow) 6.2 150 81
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .12  23 1.0  false(no-overflow) .062 9.3 .62 false(no-overflow) .067 9.0 .46 false(no-overflow) 3.0 270 27 false(no-overflow) .13 33 1.5 unknown .048 4.8 .19 unknown .032 4.6 .21  false(no-overflow) .10  26 .65 timeout 900    75 11000   false(no-overflow) 2.9 270 30 false(no-overflow) .37 59 3.3 disqualified 3.0 80 38 false(no-overflow) .23 18 2.6 false(no-overflow) 8.5 370 71 false(no-overflow) 8.3 370 67 false(no-overflow) 8.1 370 70 false(no-overflow) 54   150 720
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 900     2400 6000    error (42) 880     1500   5900    out of memory 210     15000   3400    timeout 910   6600 10000 unknown 900    710 11000   unknown .030 4.6 .19 unknown .046 4.7 .22  timeout 900     1100 10000    timeout 900    74 8400   timeout 910   6600 13000 timeout 900    410 3700   disqualified 880   440 9000 timeout (verification) 900    1200 12000   timeout 900   1300 12000 timeout 900   1800 6800 timeout 900   1300 12000 timeout 900   150 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 900     960 11000    error (42) 880     1300   9300    out of memory 330     15000   4200    timeout 910   620 12000 unknown 720    75 10000   unknown .043 4.6 .19 unknown .027 4.6 .24  timeout 900     130 13000    timeout 900    4200 7700   timeout 910   500 12000 timeout 900    540 8000   disqualified 880   180 11000 timeout (verification) 900    3100 9100   timeout 900   8200 11000 timeout 900   3300 5900 timeout 900   7500 9300 timeout 900   150 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .12  24 1.6  false(no-overflow) .069 9.8 .61 false(no-overflow) .061 9.3 .42 false(no-overflow) 3.3 280 32 false(no-overflow) .14 33 1.7 unknown .030 4.6 .19 unknown .027 4.6 .27  false(no-overflow) .088 26 .91 false(no-overflow) 110    5000 1300   false(no-overflow) 3.3 280 28 false(no-overflow) .37 59 3.0 disqualified 3.1 80 41 false(no-overflow) .22 19 2.5 false(no-overflow) 8.1 370 65 false(no-overflow) 8.1 360 60 false(no-overflow) 7.2 340 54 false(no-overflow) 13   150 170
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .12  24 .97 false(no-overflow) .071 9.6 .63 false(no-overflow) .068 8.9 .52 false(no-overflow) 3.1 270 32 false(no-overflow) .15 34 1.8 unknown .034 4.6 .22 unknown .046 4.6 .17  false(no-overflow) .11  26 1.5  timeout 900    83 9700   false(no-overflow) 3.2 270 31 false(no-overflow) .38 59 3.5 disqualified 3.1 83 38 false(no-overflow) .27 18 2.8 false(no-overflow) 7.5 360 61 false(no-overflow) 7.7 360 61 false(no-overflow) 8.1 360 59 timeout 900   150 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .11  24 1.0  false(no-overflow) .14  8.9 .48 false(no-overflow) .071 10   .47 false(no-overflow) 3.1 270 26 false(no-overflow) .15 33 1.5 unknown .033 4.6 .23 unknown .030 4.6 .26  false(no-overflow) .11  26 .87 timeout 900    83 10000   false(no-overflow) 3.1 270 31 false(no-overflow) .38 59 3.6 disqualified 3.1 84 37 false(no-overflow) .23 17 3.4 false(no-overflow) 8.2 360 61 false(no-overflow) 8.7 350 65 false(no-overflow) 7.9 340 58 false(no-overflow) 8.7 150 110
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .13  24 .99 false(no-overflow) .071 9.6 .64 error (42) 880     8100   12000    false(no-overflow) 3.0 270 33 false(no-overflow) .13 34 1.7 unknown .037 4.6 .15 unknown .033 4.6 .24  false(no-overflow) .083 26 .96 false(no-overflow) 340    4100 3700   false(no-overflow) 3.1 270 30 false(no-overflow) .37 58 3.7 disqualified 3.2 87 40 false(no-overflow) .27 19 2.8 false(no-overflow) 7.7 340 59 false(no-overflow) 7.6 340 59 false(no-overflow) 7.7 350 60 false(no-overflow) 3.5 200 36
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .15  24 1.2  false(no-overflow) .079 9.5 .73 false(no-overflow) .070 9.0 .44 false(no-overflow) 3.1 270 28 false(no-overflow) .16 34 1.9 unknown .055 4.6 .18 unknown .054 4.6 .16  false(no-overflow) .12  26 .97 false(no-overflow) 570    190 8500   false(no-overflow) 3.0 270 29 false(no-overflow) .37 59 3.2 disqualified 3.2 90 39 false(no-overflow) .23 18 3.1 false(no-overflow) 8.2 380 58 false(no-overflow) 7.9 370 69 false(no-overflow) 8.8 370 67 false(no-overflow) 3.8 150 37
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .14  24 1.4  false(no-overflow) .16  15   1.1  false(no-overflow) .071 9.1 .46 false(no-overflow) 3.1 280 26 false(no-overflow) .32 35 4.3 unknown .053 4.6 .14 unknown .050 4.6 .16  false(no-overflow) .25  27 2.9  false(no-overflow) .40 83 4.9 false(no-overflow) 3.0 270 27 false(no-overflow) .38 59 3.2 disqualified 3.5 90 43 false(no-overflow) .26 18 2.9 false(no-overflow) 6.8 360 60 false(no-overflow) 7.6 360 59 false(no-overflow) 7.4 370 61 false(no-overflow) 3.7 150 36
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .13  24 1.0  false(no-overflow) .091 9.4 .48 false(no-overflow) .10  8.6 .41 false(no-overflow) 3.1 270 26 false(no-overflow) .16 34 1.9 unknown .029 4.6 .18 unknown .031 4.6 .20  false(no-overflow) .11  26 1.1  false(no-overflow) 570    4200 8600   false(no-overflow) 3.1 270 30 false(no-overflow) .39 59 3.6 disqualified 3.3 87 42 false(no-overflow) .24 18 2.7 false(no-overflow) 8.0 360 58 false(no-overflow) 7.4 350 58 false(no-overflow) 7.6 330 64 timeout 900   150 13000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .16  24 1.1  false(no-overflow) .098 9.7 .41 false(no-overflow) .076 9.1 .48 false(no-overflow) 2.9 270 27 false(no-overflow) .17 33 1.9 unknown .029 4.6 .24 unknown .028 4.5 .19  false(no-overflow) .11  26 1.2  timeout 900    3900 14000   false(no-overflow) 3.0 270 27 false(no-overflow) .38 59 3.8 disqualified 3.2 85 38 false(no-overflow) .23 18 2.8 false(no-overflow) 7.6 350 65 false(no-overflow) 7.7 350 60 false(no-overflow) 8.4 370 66 false(no-overflow) 200   200 2900
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .12  24 .97 false(no-overflow) .080 9.5 .48 false(no-overflow) .055 9.4 .42 false(no-overflow) 3.0 270 31 false(no-overflow) .15 34 1.9 unknown .028 4.6 .20 unknown .028 4.6 .16  false(no-overflow) .10  26 1.1  false(no-overflow) 770    4100 11000   false(no-overflow) 2.9 270 26 false(no-overflow) .36 59 3.4 disqualified 3.2 86 39 false(no-overflow) .26 18 3.0 false(no-overflow) 7.1 340 53 false(no-overflow) 7.0 340 64 false(no-overflow) 6.8 330 53 false(no-overflow) 3.5 150 39
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .11  9.7 .66 false(no-overflow) .093 9.4 .36 false(no-overflow) 3.1 270 27 false(no-overflow) .19 34 1.9 unknown .056 4.7 .15 unknown .030 4.7 .20  false(no-overflow) .11  26 1.0  false(no-overflow) 190    79 2700   false(no-overflow) 3.1 270 29 false(no-overflow) .36 59 3.9 disqualified 3.3 86 45 false(no-overflow) .27 18 3.6 false(no-overflow) 8.3 380 61 false(no-overflow) 8.2 380 73 false(no-overflow) 7.3 340 55 false(no-overflow) 8.7 200 100
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .17  24 .91 false(no-overflow) .14  9.3 .56 false(no-overflow) .065 9.4 .67 false(no-overflow) 3.0 260 33 false(no-overflow) .16 34 2.1 unknown .029 4.6 .13 unknown .028 4.6 .15  false(no-overflow) .11  26 1.2  false(no-overflow) .41 82 4.5 false(no-overflow) 3.1 270 26 false(no-overflow) .37 59 3.0 disqualified 3.3 91 37 false(no-overflow) .24 18 3.4 false(no-overflow) 7.2 350 56 false(no-overflow) 6.9 330 54 false(no-overflow) 7.2 340 53 false(no-overflow) 3.7 150 41
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .12  24 .88 false(no-overflow) .13  8.7 .43 false(no-overflow) .068 8.9 .47 false(no-overflow) 3.1 270 33 false(no-overflow) .14 33 1.5 unknown .031 4.6 .16 unknown .036 4.6 .24  false(no-overflow) .080 26 .93 false(no-overflow) .43 80 5.2 false(no-overflow) 3.1 270 26 false(no-overflow) .36 59 3.9 disqualified 3.1 82 37 false(no-overflow) .23 18 3.0 false(no-overflow) 8.2 370 57 false(no-overflow) 8.3 370 60 false(no-overflow) 8.2 370 63 false(no-overflow) 3.5 150 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .13  23 1.0  false(no-overflow) .15  8.6 .39 false(no-overflow) .069 8.9 .43 false(no-overflow) 3.0 270 26 false(no-overflow) .15 33 2.2 unknown .031 4.8 .18 unknown .035 4.6 .19  false(no-overflow) .085 26 .96 false(no-overflow) 72    88 980   false(no-overflow) 3.1 270 25 false(no-overflow) .38 59 3.0 disqualified 3.1 83 38 false(no-overflow) .23 17 2.9 false(no-overflow) 7.6 360 57 false(no-overflow) 8.0 350 68 false(no-overflow) 8.2 360 57 false(no-overflow) 3.5 150 43
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .12  24 1.2  false(no-overflow) .082 9.4 .54 false(no-overflow) .071 9.2 .44 false(no-overflow) 3.2 280 33 false(no-overflow) .13 33 1.6 unknown .057 4.6 .11 unknown .047 4.6 .16  false(no-overflow) .11  26 .83 false(no-overflow) 15    81 210   false(no-overflow) 3.1 290 29 false(no-overflow) .36 59 3.7 disqualified 3.1 83 39 false(no-overflow) .23 17 2.7 false(no-overflow) 8.4 370 69 false(no-overflow) 7.4 350 61 false(no-overflow) 8.2 360 59 false(no-overflow) 3.4 150 41
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .12  24 .93 false(no-overflow) .080 9.7 .46 false(no-overflow) .075 9.6 .43 false(no-overflow) 3.4 280 29 false(no-overflow) .14 33 1.3 unknown .029 4.6 .12 unknown .030 4.6 .18  false(no-overflow) .079 26 .83 false(no-overflow) .41 83 4.3 false(no-overflow) 3.3 280 31 false(no-overflow) .37 59 3.1 disqualified 3.1 79 37 false(no-overflow) .22 18 2.5 false(no-overflow) 8.1 370 55 false(no-overflow) 7.5 360 64 false(no-overflow) 6.6 320 56 false(no-overflow) 3.6 150 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .13  24 .97 false(no-overflow) .096 8.6 .38 false(no-overflow) .067 9.2 .46 false(no-overflow) 3.3 280 30 false(no-overflow) .13 34 1.7 unknown .030 4.6 .14 unknown .027 4.6 .23  false(no-overflow) .080 26 .85 false(no-overflow) .42 84 4.4 false(no-overflow) 3.2 280 30 false(no-overflow) .37 59 3.1 disqualified 3.0 79 51 false(no-overflow) .22 18 2.5 false(no-overflow) 8.0 370 56 false(no-overflow) 7.4 350 61 false(no-overflow) 7.7 360 58 false(no-overflow) 3.5 150 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .064 9.5 .71 false(no-overflow) .085 8.9 .40 false(no-overflow) 3.0 270 26 false(no-overflow) .14 33 1.6 unknown .044 4.6 .24 unknown .029 4.6 .24  false(no-overflow) .082 26 .94 false(no-overflow) .39 83 4.8 false(no-overflow) 3.1 270 29 false(no-overflow) .35 59 3.3 disqualified 3.1 110 43 false(no-overflow) .23 18 2.6 false(no-overflow) 7.5 350 64 false(no-overflow) 6.7 330 56 false(no-overflow) 7.4 360 61 false(no-overflow) 3.5 150 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .072 10   .51 false(no-overflow) .15  7.8 .35 false(no-overflow) 3.0 270 28 false(no-overflow) .14 33 1.7 unknown .026 4.6 .21 unknown .029 4.7 .17  false(no-overflow) .078 26 .94 false(no-overflow) .41 79 5.6 false(no-overflow) 2.9 280 28 false(no-overflow) .37 59 3.1 disqualified 3.1 110 36 false(no-overflow) .24 23 3.0 false(no-overflow) 8.1 380 67 false(no-overflow) 7.4 330 56 false(no-overflow) 7.3 340 58 false(no-overflow) 3.5 150 41
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .068 9.1 .57 false(no-overflow) .077 8.3 .48 false(no-overflow) 3.0 270 26 false(no-overflow) .14 33 1.8 unknown .030 4.6 .18 unknown .048 4.7 .23  false(no-overflow) .089 26 .87 false(no-overflow) .39 79 5.2 false(no-overflow) 3.0 270 31 false(no-overflow) .36 59 3.5 disqualified 3.1 83 41 false(no-overflow) .23 18 3.2 false(no-overflow) 8.1 360 60 false(no-overflow) 7.6 350 49 false(no-overflow) 7.9 370 57 false(no-overflow) 6.3 150 82
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .13  24 1.2  false(no-overflow) .064 9.3 .56 false(no-overflow) .070 9.2 .51 false(no-overflow) 3.1 270 29 false(no-overflow) .14 33 2.0 unknown .050 4.6 .27 unknown .026 4.6 .28  false(no-overflow) .099 26 1.1  timeout 900    160 13000   false(no-overflow) 2.9 270 27 false(no-overflow) .36 58 3.6 disqualified 3.2 82 44 false(no-overflow) .23 18 3.0 false(no-overflow) 7.4 350 57 false(no-overflow) 7.8 360 61 false(no-overflow) 7.6 360 59 false(no-overflow) 9.5 150 100
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .13  23 .80 false(no-overflow) .071 9.3 .50 false(no-overflow) .064 8.6 .53 false(no-overflow) 3.0 270 32 false(no-overflow) .13 33 1.8 unknown .057 4.7 .17 unknown .028 4.6 .24  false(no-overflow) .095 26 .94 timeout 900    84 12000   false(no-overflow) 2.9 270 31 false(no-overflow) .37 59 2.9 disqualified 3.1 80 36 false(no-overflow) .23 18 2.7 false(no-overflow) 7.8 370 63 false(no-overflow) 8.2 370 60 false(no-overflow) 8.0 370 57 timeout 900   150 13000
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .13  24 1.0  false(no-overflow) .080 9.7 .89 false(no-overflow) .072 8.9 .43 false(no-overflow) 3.0 270 27 false(no-overflow) .16 33 2.0 unknown .045 4.6 .14 unknown .027 4.6 .27  false(no-overflow) .12  26 1.0  false(no-overflow) .41 82 4.8 false(no-overflow) 3.0 270 27 false(no-overflow) .37 58 3.1 disqualified 3.3 82 43 false(no-overflow) .22 17 2.6 false(no-overflow) 7.9 370 67 false(no-overflow) 7.4 330 53 false(no-overflow) 7.9 350 55 false(no-overflow) 3.5 150 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .13  24 .92 false(no-overflow) .074 9.6 .53 false(no-overflow) .067 9.1 .53 false(no-overflow) 3.3 280 31 false(no-overflow) .14 33 1.5 unknown .038 4.6 .17 unknown .043 4.7 .17  false(no-overflow) .085 26 .97 false(no-overflow) .43 85 5.6 false(no-overflow) 3.3 280 31 false(no-overflow) .34 58 4.2 disqualified 3.1 84 45 false(no-overflow) .23 18 2.8 false(no-overflow) 7.7 350 61 false(no-overflow) 6.8 340 57 false(no-overflow) 7.6 340 63 false(no-overflow) 3.5 150 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .13  24 .97 false(no-overflow) .070 8.9 .49 false(no-overflow) .087 8.8 .46 false(no-overflow) 3.2 260 31 false(no-overflow) .14 34 1.8 unknown .038 4.6 .17 unknown .030 4.8 .16  false(no-overflow) .10  26 .86 false(no-overflow) .43 83 5.1 false(no-overflow) 3.1 260 28 false(no-overflow) .38 59 3.2 disqualified 3.1 83 42 false(no-overflow) .23 17 2.5 false(no-overflow) 8.0 370 55 false(no-overflow) 8.0 370 68 false(no-overflow) 7.7 350 57 false(no-overflow) 3.6 150 44
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .072 9.3 .57 false(no-overflow) .071 9.3 .56 false(no-overflow) 3.1 270 29 false(no-overflow) .15 33 1.8 unknown .027 4.6 .23 unknown .029 4.6 .17  false(no-overflow) .095 26 1.3  false(no-overflow) .44 80 6.2 false(no-overflow) 3.0 270 32 false(no-overflow) .36 59 3.4 disqualified 3.2 86 44 false(no-overflow) .25 18 3.3 false(no-overflow) 8.7 360 67 false(no-overflow) 8.9 350 71 false(no-overflow) 8.7 370 68 false(no-overflow) 3.4 150 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .11  24 1.1  false(no-overflow) .068 9.3 .55 false(no-overflow) .065 9.6 .49 false(no-overflow) 3.1 260 27 false(no-overflow) .17 33 1.4 unknown .036 4.7 .16 unknown .030 4.6 .14  false(no-overflow) .084 26 .83 timeout 900    200 12000   false(no-overflow) 3.1 270 31 false(no-overflow) .36 59 3.5 disqualified 3.1 83 39 false(no-overflow) .27 18 2.7 false(no-overflow) 8.6 350 78 false(no-overflow) 9.7 410 81 false(no-overflow) 8.4 370 64 false(no-overflow) 3.5 150 32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .14  24 1.0  false(no-overflow) .092 9.7 .78 false(no-overflow) .074 9.1 .47 false(no-overflow) 3.0 270 27 false(no-overflow) .22 33 2.7 unknown .033 4.6 .19 unknown .031 4.6 .20  false(no-overflow) .16  26 1.9  false(no-overflow) .42 83 4.3 false(no-overflow) 3.0 270 31 false(no-overflow) .37 59 3.4 disqualified 3.3 82 34 false(no-overflow) .24 18 3.0 false(no-overflow) 7.8 370 61 false(no-overflow) 7.0 340 55 false(no-overflow) 7.9 370 60 false(no-overflow) 3.6 150 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .11  24 1.2  false(no-overflow) .066 9.3 .86 false(no-overflow) .069 9.3 .47 false(no-overflow) 3.0 270 27 false(no-overflow) .16 34 1.9 unknown .033 4.7 .29 unknown .051 4.7 .16  false(no-overflow) .10  26 1.2  timeout 900    75 9800   false(no-overflow) 3.0 270 31 false(no-overflow) .36 59 3.0 disqualified 3.1 81 40 false(no-overflow) .22 19 2.5 false(no-overflow) 6.8 340 61 false(no-overflow) 8.1 360 57 false(no-overflow) 7.9 370 57 false(no-overflow) 6.5 150 74
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .065 9.4 .50 false(no-overflow) .13  8.6 .35 false(no-overflow) 3.0 270 25 false(no-overflow) .17 33 2.1 unknown .031 4.7 .12 unknown .037 4.6 .23  false(no-overflow) .11  26 1.5  false(no-overflow) 110    83 1400   false(no-overflow) 3.0 270 29 false(no-overflow) .36 59 3.5 disqualified 3.1 83 39 false(no-overflow) .23 20 3.1 false(no-overflow) 7.7 340 59 false(no-overflow) 7.0 360 52 false(no-overflow) 7.7 360 55 false(no-overflow) 5.2 150 62
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .13  23 1.0  false(no-overflow) .12  9.8 .51 false(no-overflow) .070 9.8 .48 false(no-overflow) 3.1 270 30 false(no-overflow) .19 33 2.0 unknown .031 4.6 .15 unknown .035 4.6 .25  false(no-overflow) .11  26 1.1  false(no-overflow) .40 83 6.2 false(no-overflow) 3.0 270 29 false(no-overflow) .41 59 2.9 disqualified 3.1 82 38 false(no-overflow) .23 18 2.6 false(no-overflow) 7.9 350 59 false(no-overflow) 7.9 370 58 false(no-overflow) 7.3 340 57 false(no-overflow) 3.5 150 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .12  24 .89 false(no-overflow) .079 10   .45 false(no-overflow) .12  8.5 .32 false(no-overflow) 3.1 270 25 false(no-overflow) .14 34 1.5 unknown .028 4.6 .18 unknown .032 4.7 .28  false(no-overflow) .11  26 .83 false(no-overflow) .39 82 5.6 false(no-overflow) 3.0 270 28 false(no-overflow) .36 59 3.4 disqualified 3.1 76 39 false(no-overflow) .22 18 2.8 false(no-overflow) 7.7 370 61 false(no-overflow) 7.8 370 54 false(no-overflow) 7.9 370 63 false(no-overflow) 11   150 120
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .11  24 1.0  false(no-overflow) .11  9.3 .34 false(no-overflow) .064 9.7 .62 false(no-overflow) 3.0 270 28 false(no-overflow) .13 33 1.7 unknown .044 4.6 .15 unknown .030 4.8 .33  false(no-overflow) .081 26 .80 timeout 900    78 11000   false(no-overflow) 3.0 270 28 false(no-overflow) .35 59 4.8 disqualified 3.0 77 40 false(no-overflow) .22 17 2.5 false(no-overflow) 7.4 350 64 false(no-overflow) 7.1 340 57 false(no-overflow) 7.1 340 55 false(no-overflow) 55   150 650
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .15  23 .94 false(no-overflow) .061 10   .57 false(no-overflow) .060 9.6 .62 false(no-overflow) 3.0 270 29 false(no-overflow) .13 33 1.7 unknown .028 4.7 .18 unknown .036 4.6 .22  false(no-overflow) .083 26 .88 false(no-overflow) 250    77 2800   false(no-overflow) 2.9 270 28 false(no-overflow) .36 59 3.0 disqualified 3.1 110 38 false(no-overflow) .23 18 3.4 false(no-overflow) 7.0 360 55 false(no-overflow) 7.7 370 66 false(no-overflow) 7.2 340 59 error (1) 51   150 590
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .12  24 .89 false(no-overflow) .12  8.9 .37 false(no-overflow) .078 9.2 .43 false(no-overflow) 2.9 270 27 false(no-overflow) .14 33 1.7 unknown .027 4.6 .24 unknown .059 4.6 .25  false(no-overflow) .092 26 .91 false(no-overflow) 3.1  79 40   false(no-overflow) 2.9 270 30 false(no-overflow) .36 59 3.4 disqualified 3.1 84 46 false(no-overflow) .24 18 2.9 false(no-overflow) 7.5 340 58 false(no-overflow) 7.8 370 67 false(no-overflow) 7.0 340 55 false(no-overflow) 3.7 150 42
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .12  24 .96 false(no-overflow) .062 10   .68 false(no-overflow) .059 9.8 .57 false(no-overflow) 2.8 270 28 false(no-overflow) .17 34 1.7 unknown .034 4.6 .21 unknown .029 4.7 .19  false(no-overflow) .12  26 .98 false(no-overflow) .42 79 5.6 false(no-overflow) 2.9 270 28 false(no-overflow) .38 58 3.8 disqualified 3.2 81 41 false(no-overflow) .23 19 2.9 false(no-overflow) 7.8 360 60 false(no-overflow) 8.3 370 64 false(no-overflow) 7.9 360 58 false(no-overflow) 14   150 170
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .11  24 .99 false(no-overflow) .080 9.8 .38 false(no-overflow) .066 9.2 .46 false(no-overflow) 3.1 270 28 false(no-overflow) .15 34 1.5 unknown .034 4.6 .18 unknown .028 4.6 .21  false(no-overflow) .11  26 .96 timeout 900    78 11000   false(no-overflow) 3.0 270 27 false(no-overflow) .38 59 3.1 disqualified 3.1 82 37 false(no-overflow) .25 18 2.6 false(no-overflow) 7.2 330 52 false(no-overflow) 7.3 350 50 false(no-overflow) 6.8 340 57 false(no-overflow) 96   150 1200
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .12  24 .95 false(no-overflow) .071 9.5 .41 false(no-overflow) .073 9.1 .41 false(no-overflow) 3.1 270 27 false(no-overflow) .13 33 1.8 unknown .057 4.6 .18 unknown .036 4.8 .21  false(no-overflow) .084 26 .94 timeout 900    4300 9800   false(no-overflow) 2.9 260 29 false(no-overflow) .37 59 2.9 disqualified 3.1 82 40 false(no-overflow) .24 18 2.7 false(no-overflow) 7.6 350 60 false(no-overflow) 7.6 340 60 false(no-overflow) 8.3 370 63 timeout 900   150 11000
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .12  24 .97 false(no-overflow) .068 9.3 .59 false(no-overflow) .062 9.2 .47 false(no-overflow) 3.0 270 28 false(no-overflow) .14 33 1.6 unknown .036 4.6 .24 unknown .031 4.6 .21  false(no-overflow) .10  26 .80 false(no-overflow) .40 82 4.2 false(no-overflow) 3.0 270 31 false(no-overflow) .38 59 3.7 disqualified 3.1 82 34 false(no-overflow) .27 23 2.4 false(no-overflow) 6.6 330 57 false(no-overflow) 7.9 370 56 false(no-overflow) 7.6 360 60 false(no-overflow) 3.4 150 32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .12  24 .95 false(no-overflow) .072 9.5 .50 false(no-overflow) .080 9.0 .42 false(no-overflow) 3.0 270 31 false(no-overflow) .15 33 1.9 unknown .053 4.6 .15 unknown .028 4.6 .18  false(no-overflow) .11  26 .92 false(no-overflow) .39 83 4.2 false(no-overflow) 3.1 270 27 false(no-overflow) .37 58 3.7 disqualified 3.1 85 39 false(no-overflow) .25 18 2.9 false(no-overflow) 6.6 340 53 false(no-overflow) 8.4 360 61 false(no-overflow) 7.9 360 57 false(no-overflow) 3.6 150 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .13  24 .97 false(no-overflow) .077 9.5 .54 false(no-overflow) .072 9.1 .40 false(no-overflow) 3.0 270 25 false(no-overflow) .17 34 1.9 unknown .040 4.7 .27 unknown .029 4.6 .18  false(no-overflow) .10  26 1.4  false(no-overflow) .40 82 5.8 false(no-overflow) 2.9 280 27 false(no-overflow) .40 59 3.6 disqualified 3.2 87 42 false(no-overflow) .23 18 2.4 false(no-overflow) 7.7 370 64 false(no-overflow) 8.1 370 67 false(no-overflow) 8.1 370 57 false(no-overflow) 3.6 200 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .15  24 1.1  false(no-overflow) .11  8.2 .42 false(no-overflow) .11  9.6 .36 false(no-overflow) 3.1 270 29 false(no-overflow) .15 34 1.9 unknown .031 4.7 .13 unknown .027 4.6 .23  false(no-overflow) .087 26 .89 false(no-overflow) .40 79 5.4 false(no-overflow) 3.1 270 26 false(no-overflow) .37 59 2.7 disqualified 3.2 85 44 false(no-overflow) .23 18 3.0 false(no-overflow) 7.2 340 57 false(no-overflow) 7.6 350 55 false(no-overflow) 8.0 370 59 false(no-overflow) 3.7 150 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .11  24 1.0  false(no-overflow) .072 8.9 .54 false(no-overflow) .076 9.6 .40 false(no-overflow) 3.0 260 26 false(no-overflow) .15 34 1.5 unknown .047 4.6 .15 unknown .028 4.7 .17  false(no-overflow) .081 26 .87 false(no-overflow) .41 83 4.5 false(no-overflow) 2.9 260 28 false(no-overflow) .39 59 3.9 disqualified 3.2 85 37 false(no-overflow) .23 18 2.8 false(no-overflow) 8.4 360 62 false(no-overflow) 8.4 370 63 false(no-overflow) 8.0 370 69 false(no-overflow) 3.8 150 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .068 9.7 .57 false(no-overflow) .069 9.2 .44 false(no-overflow) 3.1 270 27 false(no-overflow) .14 33 2.0 unknown .047 4.5 .21 unknown .038 4.8 .24  false(no-overflow) .086 26 .94 false(no-overflow) 530    78 7100   false(no-overflow) 3.1 270 29 false(no-overflow) .40 59 3.0 disqualified 3.2 85 39 false(no-overflow) .23 18 2.5 false(no-overflow) 7.7 350 62 false(no-overflow) 6.6 330 53 false(no-overflow) 8.0 360 70 false(no-overflow) 180   150 2600
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .096 8.4 .42 false(no-overflow) .061 10   .59 false(no-overflow) 3.0 270 26 false(no-overflow) .14 33 1.4 unknown .036 4.7 .19 unknown .031 4.6 .16  false(no-overflow) .098 26 .87 false(no-overflow) 330    100 4800   false(no-overflow) 3.0 270 28 false(no-overflow) .37 59 3.4 disqualified 3.2 82 42 false(no-overflow) .22 17 2.6 false(no-overflow) 7.1 330 59 false(no-overflow) 7.8 360 70 false(no-overflow) 7.5 370 59 false(no-overflow) 12   150 130
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .12  24 .98 false(no-overflow) .097 9.3 .43 false(no-overflow) .13  8.9 .34 false(no-overflow) 3.3 290 29 false(no-overflow) .15 34 1.7 unknown .034 4.6 .18 unknown .033 4.5 .19  false(no-overflow) .11  26 .78 false(no-overflow) 270    630 2700   false(no-overflow) 3.3 290 27 false(no-overflow) .36 59 3.2 disqualified 3.1 83 40 false(no-overflow) .24 17 2.8 false(no-overflow) 7.8 370 55 false(no-overflow) 7.8 360 68 false(no-overflow) 8.0 360 60 false(no-overflow) 3.6 150 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .12  24 .95 false(no-overflow) .080 9.5 .54 false(no-overflow) .062 9.7 .49 false(no-overflow) 3.2 270 31 false(no-overflow) .16 33 1.9 unknown .033 4.8 .24 unknown .027 4.6 .20  false(no-overflow) .11  26 .89 false(no-overflow) 150    77 2200   false(no-overflow) 3.1 270 26 false(no-overflow) .38 59 3.3 disqualified 3.2 86 39 false(no-overflow) .24 19 3.0 false(no-overflow) 7.8 360 60 false(no-overflow) 8.1 360 61 false(no-overflow) 7.2 350 56 false(no-overflow) 180   150 2400
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .085 9.5 .57 false(no-overflow) .061 9.1 .56 false(no-overflow) 2.9 270 26 false(no-overflow) .14 34 1.8 unknown .039 4.6 .15 unknown .046 4.6 .18  false(no-overflow) .11  26 .87 false(no-overflow) .42 79 4.7 false(no-overflow) 3.0 280 27 false(no-overflow) .37 59 2.9 disqualified 3.2 87 44 false(no-overflow) .26 18 2.8 false(no-overflow) 7.8 360 56 false(no-overflow) 7.7 350 60 false(no-overflow) 7.9 370 59 false(no-overflow) 3.6 150 38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .16  24 .81 false(no-overflow) .068 9.6 .54 false(no-overflow) .064 9.6 .53 false(no-overflow) 3.1 270 28 false(no-overflow) .14 33 1.6 unknown .049 4.6 .21 unknown .033 4.6 .29  false(no-overflow) .16  26 2.6  false(no-overflow) 740    77 9600   false(no-overflow) 3.0 270 29 false(no-overflow) .36 59 3.3 disqualified 3.2 83 48 false(no-overflow) .23 18 2.6 false(no-overflow) 7.9 360 65 false(no-overflow) 8.4 370 56 false(no-overflow) 7.6 360 66 false(no-overflow) 180   150 2100
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .063 9.4 .60 false(no-overflow) .074 9.1 .46 false(no-overflow) 3.0 270 30 false(no-overflow) .17 33 1.7 unknown .048 4.6 .19 unknown .048 4.6 .16  false(no-overflow) .085 26 .89 timeout 900    83 9300   false(no-overflow) 3.0 270 29 false(no-overflow) .39 59 4.4 disqualified 3.1 84 42 false(no-overflow) .24 18 2.9 false(no-overflow) 8.4 370 62 false(no-overflow) 8.3 340 61 false(no-overflow) 8.3 360 64 false(no-overflow) 33   150 440
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .13  24 1.0  false(no-overflow) .073 8.8 .56 false(no-overflow) .064 9.0 .53 false(no-overflow) 3.1 270 26 false(no-overflow) .16 33 1.6 unknown .058 4.6 .15 unknown .041 4.7 .22  false(no-overflow) .090 26 .99 timeout 900    83 11000   false(no-overflow) 3.0 270 26 false(no-overflow) .37 58 3.2 disqualified 3.1 83 34 false(no-overflow) .25 18 2.6 false(no-overflow) 7.4 340 64 false(no-overflow) 7.2 350 61 false(no-overflow) 8.1 370 61 false(no-overflow) 490   150 5600
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .071 9.6 .53 false(no-overflow) .059 9.2 .62 false(no-overflow) 3.0 270 26 false(no-overflow) .14 33 1.7 unknown .031 4.6 .26 unknown .036 4.6 .12  false(no-overflow) .086 26 .98 timeout 900    82 12000   false(no-overflow) 3.0 270 34 false(no-overflow) .36 59 4.0 disqualified 3.2 90 44 false(no-overflow) .24 19 2.9 false(no-overflow) 8.0 360 57 false(no-overflow) 7.3 340 55 false(no-overflow) 8.2 370 63 false(no-overflow) 230   150 3000
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .12  8.9 .39 false(no-overflow) .077 8.7 .39 false(no-overflow) 3.0 260 27 false(no-overflow) .14 33 1.7 unknown .030 4.7 .23 unknown .036 4.6 .24  false(no-overflow) .10  26 .94 false(no-overflow) 250    670 3300   false(no-overflow) 3.1 270 30 false(no-overflow) .39 59 3.3 disqualified 3.1 83 36 false(no-overflow) .22 17 2.6 false(no-overflow) 7.5 350 62 false(no-overflow) 6.8 340 55 false(no-overflow) 6.9 330 62 false(no-overflow) 200   150 2200
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .12  24 .98 false(no-overflow) .14  9.4 .41 false(no-overflow) .076 9.1 .36 false(no-overflow) 3.2 270 27 false(no-overflow) .14 33 2.0 unknown .046 4.8 .16 unknown .036 4.6 .11  false(no-overflow) .084 26 .83 false(no-overflow) 330    4100 3800   false(no-overflow) 3.1 270 27 false(no-overflow) .38 59 3.2 disqualified 3.1 96 36 false(no-overflow) .27 18 3.3 false(no-overflow) 8.3 360 62 false(no-overflow) 7.9 340 67 false(no-overflow) 8.0 360 59 false(no-overflow) 480   150 7100
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .14  24 1.1  false(no-overflow) .080 9.5 .57 false(no-overflow) 110     4500   1300    false(no-overflow) 3.6 290 33 false(no-overflow) .14 34 1.6 unknown .055 4.8 .16 unknown .031 4.6 .23  false(no-overflow) .082 26 1.0  false(no-overflow) 180    78 2000   false(no-overflow) 3.6 290 33 false(no-overflow) .38 59 3.5 disqualified 3.3 86 37 false(no-overflow) .24 18 2.9 false(no-overflow) 10   390 78 false(no-overflow) 13   490 120 false(no-overflow) 9.0 380 77 timeout 900   150 12000
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .13  24 1.1  false(no-overflow) .088 10   .67 false(no-overflow) .075 9.6 .34 false(no-overflow) 3.0 270 31 false(no-overflow) .17 34 2.2 unknown .052 4.7 .12 unknown .031 4.6 .24  false(no-overflow) .10  26 1.4  false(no-overflow) 93    78 1200   false(no-overflow) 2.9 270 26 false(no-overflow) .37 58 3.8 disqualified 3.2 82 37 false(no-overflow) .22 18 3.0 false(no-overflow) 6.7 330 55 false(no-overflow) 7.6 360 63 false(no-overflow) 7.2 330 58 false(no-overflow) 3.6 150 36
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) .25  23 3.0  false(no-overflow) .078 9.5 .81 error (42) 880     1400   10000    false(no-overflow) 3.3 280 29 false(no-overflow) .16 33 1.7 unknown .034 4.7 .18 unknown .036 4.6 .26  false(no-overflow) .091 26 .78 timeout 900    77 12000   false(no-overflow) 3.3 270 31 timeout 900    8000 7000   disqualified 3.3 90 36 false(no-overflow) .29 18 3.4 false(no-overflow) 11   450 84 false(no-overflow) 11   520 95 false(no-overflow) 12   470 79 false(no-overflow) 4.2 150 43
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .11  24 1.2  false(no-overflow) .12  8.9 .42 false(no-overflow) .10  8.7 .44 false(no-overflow) 3.1 280 29 false(no-overflow) .14 34 1.8 unknown .052 4.7 .17 unknown .032 4.6 .18  false(no-overflow) .083 26 1.0  false(no-overflow) .41 82 5.9 false(no-overflow) 3.2 280 32 false(no-overflow) .40 59 3.0 disqualified 3.2 84 36 false(no-overflow) .23 17 2.6 false(no-overflow) 7.6 340 56 false(no-overflow) 7.9 360 67 false(no-overflow) 7.7 370 54 false(no-overflow) 12   150 140
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .13  24 .77 false(no-overflow) .069 9.1 .61 false(no-overflow) .060 9.5 .52 false(no-overflow) 3.2 280 32 false(no-overflow) .14 33 1.6 unknown .051 4.7 .22 unknown .058 4.6 .17  false(no-overflow) .11  26 .75 false(no-overflow) .40 79 4.9 false(no-overflow) 3.3 280 34 false(no-overflow) .36 59 3.1 disqualified 3.1 85 45 false(no-overflow) .22 17 2.8 false(no-overflow) 8.2 360 61 false(no-overflow) 7.3 350 59 false(no-overflow) 7.9 370 59 false(no-overflow) 13   150 150
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c error (5) .081 24 .77 false(no-overflow) .078 8.9 .54 false(no-overflow) .084 9.0 .34 false(no-overflow) 3.3 280 30 false(no-overflow) .15 34 1.7 unknown .027 4.6 .19 unknown .033 4.7 .16  false(no-overflow) .097 26 .83 false(no-overflow) .41 83 5.0 false(no-overflow) 3.4 290 30 false(no-overflow) .37 59 3.3 disqualified 2.7 74 36 false(no-overflow) .26 18 2.7 false(no-overflow) 8.7 380 69 false(no-overflow) 8.5 350 61 false(no-overflow) 8.1 340 62 false(no-overflow) 3.7 150 37
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c error (5) .083 24 .78 false(no-overflow) .083 10   .50 false(no-overflow) .066 9.1 .47 false(no-overflow) 3.4 290 34 false(no-overflow) .16 34 1.5 unknown .032 4.6 .21 unknown .029 4.6 .23  false(no-overflow) .083 26 .89 false(no-overflow) .39 83 6.4 false(no-overflow) 3.5 290 31 false(no-overflow) .35 59 4.1 disqualified 2.7 75 34 false(no-overflow) .24 18 2.9 false(no-overflow) 8.3 350 74 false(no-overflow) 8.0 350 63 false(no-overflow) 8.1 340 61 false(no-overflow) 3.7 150 40
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c error (5) .081 24 .82 false(no-overflow) .083 9.2 .76 false(no-overflow) .12  9.3 .30 error 3.8 290 35 false(no-overflow) .14 34 1.5 unknown .055 4.6 .18 unknown .031 4.7 .15  false(no-overflow) .10  26 .82 false(no-overflow) 48    120 620   error 3.9 290 36 false(no-overflow) .37 59 3.2 disqualified 2.7 76 37 false(no-overflow) .28 18 3.1 false(no-overflow) 7.3 350 64 false(no-overflow) 8.2 370 60 false(no-overflow) 7.5 350 49 timeout 900   150 11000
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c error (5) .091 23 .72 false(no-overflow) .075 9.7 .73 false(no-overflow) .066 9.2 .64 false(no-overflow) 3.3 290 28 false(no-overflow) .14 34 1.4 unknown .054 4.7 .17 unknown .030 4.7 .14  false(no-overflow) .10  26 .72 false(no-overflow) 59    140 690   false(no-overflow) 3.2 290 32 false(no-overflow) .37 59 3.2 disqualified 2.7 76 36 false(no-overflow) .23 18 2.9 false(no-overflow) 8.4 360 62 false(no-overflow) 7.5 350 54 false(no-overflow) 8.1 370 58 false(no-overflow) 4.0 150 40
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .11  24 1.2  false(no-overflow) .074 9.4 .61 false(no-overflow) .072 9.0 .45 false(no-overflow) 2.9 270 27 false(no-overflow) .15 34 1.7 unknown .057 4.6 .24 unknown .029 4.6 .19  false(no-overflow) .089 26 .99 timeout 900    78 11000   false(no-overflow) 3.0 270 26 false(no-overflow) .38 59 3.5 disqualified 3.1 83 35 false(no-overflow) .23 18 2.7 false(no-overflow) 7.2 340 63 false(no-overflow) 6.9 330 53 false(no-overflow) 7.4 350 53 false(no-overflow) 73   150 870
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .11  24 .93 false(no-overflow) .069 9.5 .46 false(no-overflow) .063 9.2 .48 false(no-overflow) 2.9 270 28 false(no-overflow) .14 34 1.4 unknown .055 4.6 .17 unknown .030 4.6 .25  false(no-overflow) .080 26 .86 timeout 900    74 11000   false(no-overflow) 3.0 260 28 timeout 900    410 4900   disqualified 3.1 83 39 false(no-overflow) .25 17 2.5 false(no-overflow) 7.9 340 54 false(no-overflow) 8.0 370 64 false(no-overflow) 7.7 340 62 false(no-overflow) 73   150 790
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .12  24 .93 false(no-overflow) .13  9.4 .53 false(no-overflow) .15  8.5 .36 false(no-overflow) 3.0 270 32 false(no-overflow) .15 33 1.5 unknown .026 4.6 .24 unknown .030 4.6 .19  false(no-overflow) .10  26 .84 false(no-overflow) .42 80 5.3 false(no-overflow) 3.1 270 25 false(no-overflow) .35 59 3.9 disqualified 3.1 110 36 false(no-overflow) .23 18 2.4 false(no-overflow) 7.8 360 62 false(no-overflow) 8.2 350 59 false(no-overflow) 7.5 330 63 false(no-overflow) 3.5 150 36
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .11  24 .93 false(no-overflow) .075 9.6 .45 false(no-overflow) .063 9.3 .67 false(no-overflow) 3.0 270 25 false(no-overflow) .13 33 2.4 unknown .033 4.8 .26 unknown .031 4.7 .19  false(no-overflow) .082 26 .89 false(no-overflow) 320    77 3700   false(no-overflow) 3.0 270 27 false(no-overflow) .36 59 2.7 disqualified 3.1 77 44 false(no-overflow) .22 19 3.3 false(no-overflow) 7.7 360 64 false(no-overflow) 6.7 320 56 false(no-overflow) 6.9 340 58 false(no-overflow) 6.5 150 68
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .13  24 .90 false(no-overflow) .14  9.8 .58 false(no-overflow) .075 9.1 .59 false(no-overflow) 3.2 280 34 false(no-overflow) .14 34 1.5 unknown .023 4.6 .28 unknown .052 4.7 .27  false(no-overflow) .11  26 .92 false(no-overflow) .41 82 4.9 false(no-overflow) 3.3 280 29 false(no-overflow) .37 58 3.4 disqualified 3.1 83 35 false(no-overflow) .27 22 2.8 false(no-overflow) 7.1 350 60 false(no-overflow) 8.0 370 62 false(no-overflow) 7.2 360 61 false(no-overflow) 3.5 150 33
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .12  24 .98 false(no-overflow) .064 9.5 .47 false(no-overflow) .13  8.0 .32 false(no-overflow) 3.0 260 28 false(no-overflow) .14 34 1.5 unknown .029 4.6 .19 unknown .031 4.6 .19  false(no-overflow) .12  26 .77 false(no-overflow) .39 83 4.5 false(no-overflow) 3.1 270 31 false(no-overflow) .36 59 3.0 disqualified 3.1 84 37 false(no-overflow) .23 18 2.8 false(no-overflow) 7.9 370 56 false(no-overflow) 7.1 340 53 false(no-overflow) 8.1 360 61 false(no-overflow) 14   200 180
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .12  24 1.1  false(no-overflow) .077 9.6 .49 false(no-overflow) .061 9.0 .47 false(no-overflow) 3.0 270 31 false(no-overflow) .14 33 1.6 unknown .031 4.7 .21 unknown .031 4.6 .21  false(no-overflow) .10  26 .84 timeout 900    78 11000   false(no-overflow) 3.0 270 28 false(no-overflow) .37 59 3.6 disqualified 3.1 84 50 false(no-overflow) .24 17 2.7 false(no-overflow) 7.6 370 66 false(no-overflow) 7.7 340 59 false(no-overflow) 8.0 360 63 false(no-overflow) 130   150 1600
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .077 9.4 .77 false(no-overflow) .066 9.6 .70 false(no-overflow) 3.0 270 30 false(no-overflow) .17 33 1.9 unknown .030 4.7 .22 unknown .033 4.6 .23  false(no-overflow) .12  26 1.3  false(no-overflow) .44 83 5.1 false(no-overflow) 3.2 280 30 false(no-overflow) .35 59 3.8 disqualified 3.3 90 40 false(no-overflow) .23 18 3.1 false(no-overflow) 7.7 350 59 false(no-overflow) 8.2 360 60 false(no-overflow) 7.5 370 57 false(no-overflow) 3.5 150 35
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .11  24 .95 false(no-overflow) .066 9.5 .56 false(no-overflow) .071 9.2 .45 false(no-overflow) 3.1 270 27 false(no-overflow) .15 33 1.6 unknown .031 4.6 .24 unknown .035 4.7 .21  false(no-overflow) .084 26 .95 timeout 900    83 10000   false(no-overflow) 3.1 270 32 false(no-overflow) .38 59 3.4 disqualified 3.1 83 38 false(no-overflow) .23 18 2.7 false(no-overflow) 7.6 360 58 false(no-overflow) 7.9 370 55 false(no-overflow) 7.9 360 67 false(no-overflow) 360   160 4600
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .13  24 .96 false(no-overflow) .080 9.4 .51 false(no-overflow) .087 8.9 .40 false(no-overflow) 3.1 270 27 false(no-overflow) .18 34 2.0 unknown .038 4.6 .15 unknown .054 4.6 .24  false(no-overflow) .10  26 1.6  false(no-overflow) .39 83 4.7 false(no-overflow) 3.1 270 28 false(no-overflow) .38 59 2.6 disqualified 3.2 83 44 false(no-overflow) .24 18 3.3 false(no-overflow) 8.9 360 74 false(no-overflow) 8.8 370 65 false(no-overflow) 8.0 360 66 false(no-overflow) 370   200 4300
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .11  24 1.1  false(no-overflow) .082 9.7 .42 error (42) 880     12000   11000    false(no-overflow) 3.1 270 29 false(no-overflow) .14 33 2.0 unknown .038 4.8 .25 unknown .051 4.6 .31  false(no-overflow) .10  26 .84 false(no-overflow) 140    4600 1400   false(no-overflow) 3.0 270 29 timeout 900    430 4800   disqualified 3.2 86 44 false(no-overflow) .27 18 3.0 false(no-overflow) 8.3 360 64 false(no-overflow) 10   380 78 false(no-overflow) 8.7 360 69 timeout 900   150 12000
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) .13  24 .89 false(no-overflow) .085 9.7 .72 error (42) 880     13000   12000    false(no-overflow) 3.1 270 29 false(no-overflow) .15 33 1.4 unknown .044 4.6 .14 unknown .043 4.6 .14  false(no-overflow) .083 26 .85 false(no-overflow) 140    4900 1600   false(no-overflow) 3.0 270 25 timeout 900    450 6100   disqualified 3.1 84 38 false(no-overflow) .26 18 3.1 false(no-overflow) 8.4 380 72 false(no-overflow) 9.9 380 86 false(no-overflow) 7.7 340 72 timeout 900   150 13000
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .12  9.6 .48 error (42) 880     13000   12000    false(no-overflow) 3.0 270 28 false(no-overflow) .13 34 1.8 unknown .059 4.7 .19 unknown .042 4.6 .17  false(no-overflow) .10  26 .70 false(no-overflow) 140    4100 1700   false(no-overflow) 3.1 270 28 timeout 900    460 5800   disqualified 3.1 84 39 false(no-overflow) .26 18 3.1 false(no-overflow) 8.3 360 66 false(no-overflow) 9.9 380 85 false(no-overflow) 7.6 350 58 timeout 900   150 12000
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .13  24 .99 false(no-overflow) .081 9.6 .60 false(no-overflow) .071 9.0 .41 false(no-overflow) 3.0 270 27 false(no-overflow) .19 33 2.2 unknown .029 4.6 .19 unknown .049 4.6 .13  false(no-overflow) .13  26 1.8  timeout 900    83 12000   false(no-overflow) 3.0 270 29 false(no-overflow) .36 59 3.2 disqualified 3.2 83 44 false(no-overflow) .27 23 2.5 false(no-overflow) 8.0 360 60 false(no-overflow) 7.9 370 63 false(no-overflow) 7.8 360 62 false(no-overflow) 3.7 150 38
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .12  24 1.0  false(no-overflow) .079 9.3 .50 false(no-overflow) .087 8.8 .32 false(no-overflow) 3.1 270 30 false(no-overflow) .14 34 1.6 unknown .034 4.6 .21 unknown .030 4.7 .15  false(no-overflow) .085 26 .82 false(no-overflow) .40 79 3.8 false(no-overflow) 3.2 280 29 false(no-overflow) .37 58 3.3 disqualified 3.1 82 35 false(no-overflow) .25 18 2.6 false(no-overflow) 6.7 330 61 false(no-overflow) 7.7 350 56 false(no-overflow) 7.7 350 61 false(no-overflow) 3.5 150 35
termination-crafted-lit/cstrncmp_false-no-overflow.c error (134) .20  24 1.4  false(no-overflow) .083 9.2 .69 error (134) .049 8.5 .37 false(no-overflow) 4.0 320 46 false(no-overflow) .17 34 2.2 unknown .023 4.6 .21 unknown .031 4.6 .20  false(no-overflow) .11  26 1.2  false(no-overflow) 28    760 330   false(no-overflow) 4.1 320 45 false(no-overflow) .70 61 6.4 disqualified 3.3 86 38 false(no-overflow) .80 18 12   false(no-overflow) 9.1 370 69 false(no-overflow) 8.7 360 68 false(no-overflow) 9.2 380 75 error (1) 4.3 200 36
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .12  23 1.0  false(no-overflow) .068 9.0 .61 false(no-overflow) .068 9.0 .39 false(no-overflow) 2.9 270 22 false(no-overflow) .16 33 2.0 unknown .047 4.8 .20 unknown .053 4.6 .15  false(no-overflow) .11  26 1.1  timeout 900    75 11000   false(no-overflow) 3.0 270 30 false(no-overflow) .38 59 3.0 disqualified 3.1 83 37 false(no-overflow) .27 18 3.7 false(no-overflow) 7.4 360 57 false(no-overflow) 8.7 380 72 false(no-overflow) 7.3 340 55 timeout 900   150 10000
termination-crafted-lit/joey_false-no-overflow.c error (5) .14  24 .72 false(no-overflow) .12  11   1.2  false(no-overflow) .065 9.4 .53 false(no-overflow) 3.1 270 29 false(no-overflow) .14 34 1.3 unknown .030 4.6 .17 unknown .030 4.5 .23  false(no-overflow) .077 26 .91 timeout 900    120 9700   false(no-overflow) 3.0 270 28 false(no-overflow) .37 58 3.8 disqualified 2.7 74 33 false(no-overflow) .25 18 3.3 false(no-overflow) 8.6 370 64 false(no-overflow) 8.7 370 67 false(no-overflow) 8.7 370 69 timeout 900   200 11000
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .12  24 1.2  false(no-overflow) .12  9.3 .51 false(no-overflow) .065 9.2 .55 false(no-overflow) 3.1 270 28 false(no-overflow) .18 34 1.9 unknown .030 4.6 .21 unknown .044 4.7 .21  false(no-overflow) .10  26 1.4  false(no-overflow) .40 82 4.6 false(no-overflow) 3.1 270 30 false(no-overflow) .37 59 3.5 disqualified 3.2 82 43 false(no-overflow) .24 18 2.5 false(no-overflow) 8.1 360 56 false(no-overflow) 8.0 370 64 false(no-overflow) 7.0 340 48 false(no-overflow) 3.4 150 42
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     830 9800    error (42) 880     1300   8900    out of memory 560     15000   8000    out of memory 870   15000 12000 unknown 900    290 11000   unknown .028 4.6 .16 unknown .046 4.6 .16  timeout 900     650 10000    timeout 900    4400 6900   out of memory 870   15000 13000 timeout 900    490 6400   disqualified 880   180 13000 timeout (verification) 900    3300 10000   timeout 900   1500 12000 timeout 900   5400 6900 timeout 900   1300 11000 timeout 900   150 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true .099 24 .65 error (42) 880     1200   8800    error (42) 880     15000   13000    true 3.2 270 27 unknown .81 67 8.8 unknown .031 4.7 .20 unknown .033 4.6 .20  timeout 900     730 9800    timeout 900    75 10000   true 3.0 270 27 timeout 900    320 4300   disqualified 880   370 11000 timeout (verification) 900    1400 12000   true 8.5 370 65 true 17   520 150 true 8.5 330 70 timeout 900   150 13000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true .11  24 .94 true 1.7   50   21    out of memory 190     15000   2900    true 3.0 270 29 unknown .83 66 9.2 unknown .032 4.7 .23 unknown .029 4.6 .21  true .63  26 6.9  timeout 900    2100 10000   true 3.0 270 28 true .41 59 3.6 disqualified 27   170 330 true .21 19 2.1 true 8.1 370 65 true 8.2 350 74 true 8.4 370 67 timeout 900   150 13000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 900     1700 10000    error (42) 880     2300   4000    error (42) 880     220   10000    timeout 900   13000 14000 unknown 58    48 650   unknown .033 4.6 .20 unknown .030 4.6 .20  timeout 900     1100 11000    timeout 900    75 9400   timeout 910   13000 12000 timeout 900    410 4500   disqualified 880   780 11000 timeout (verification) 900    420 7200   timeout 900   2500 12000 timeout 900   5700 9100 timeout 900   1800 14000 timeout 900   200 9800
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 25     580 260    error (42) 880     1300   5100    error (42) 870     8000   14000    true 110   1100 890 unknown 900    200 12000   unknown .028 4.5 .24 unknown .027 4.6 .18  timeout 900     340 11000    timeout 900    75 8600   true 110   1100 880 out of memory 38    15000 470   disqualified 880   170 12000 timeout (verification) 900    310 14000   true 8.2 340 65 true 11   560 98 true 8.1 360 64 timeout 900   150 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 900     2200 5600    error (42) 880     1500   5900    out of memory 340     15000   4600    timeout 910   6600 11000 unknown 900    590 11000   unknown .023 4.7 .22 unknown .028 4.6 .19  timeout 900     870 10000    timeout 900    75 8700   timeout 910   6600 12000 timeout 900    380 4000   disqualified 880   420 10000 timeout (verification) 900    1300 13000   true 19   550 150 timeout 900   2300 6700 true 17   680 130 timeout 900   150 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 900     920 9700    error (42) 880     1400   9300    out of memory 330     15000   3800    timeout 910   520 14000 unknown 680    69 8500   unknown .031 4.7 .19 unknown .051 4.6 .19  timeout 900     130 13000    timeout 900    4200 7400   timeout 910   520 14000 timeout 900    550 7100   disqualified 880   180 12000 timeout (verification) 900    3100 7500   timeout 900   5400 11000 timeout 900   5600 9200 timeout 900   3200 13000 timeout 900   150 13000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true .75  28 9.7  true .32  9.7 3.9  out of memory 340     15000   4800    true 59   550 760 unknown 4.7  68 63   unknown .036 4.6 .17 unknown .029 4.7 .18  true .16  26 1.7  timeout 900    4300 6400   true 59   530 820 out of memory 130    15000 1800   disqualified 97   120 1500 timeout (verification) 900    4000 6800   true 180   4700 2100 timeout 900   4100 6700 true 170   4700 2200 timeout 900   150 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true .10  24 .98 error (42) 880     1300   7700    out of memory 380     15000   4300    true 3.1 270 25 unknown .83 65 10   unknown .033 4.7 .25 unknown .028 4.6 .17  timeout 900     270 12000    timeout 900    75 9900   true 3.1 270 25 timeout 900    350 4800   disqualified 880   470 14000 timeout (verification) 900    480 8400   true 9.4 380 81 true 20   710 180 true 9.4 370 73 timeout 900   150 14000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true .10  24 .93 error (42) 880     1400   8300    out of memory 290     15000   4500    true 3.1 270 33 unknown .86 67 9.0 unknown .035 4.6 .32 unknown .051 4.7 .16  timeout 900     220 11000    timeout 900    75 9200   true 3.1 270 28 timeout 900    320 4900   disqualified 880   510 9400 timeout (verification) 900    1200 12000   true 10   420 77 timeout 900   2200 6000 true 9.7 440 83 timeout 900   150 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true .097 24 .93 error (42) 880     1500   9300    error (42) 880     8800   12000    true 3.2 270 31 unknown .85 67 9.5 unknown .038 4.6 .24 unknown .034 4.6 .18  timeout 900     310 11000    timeout 900    84 11000   true 3.2 270 34 timeout 900    400 4100   disqualified 880   380 11000 timeout (verification) 900    170 11000   true 8.7 360 70 true 12   570 110 true 9.4 370 72 timeout 900   150 9500
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true .093 24 1.1  error (42) 880     2600   12000    error (42) 870     5100   11000    true 4.8 290 46 unknown .91 67 10   unknown .059 4.6 .20 unknown .031 4.7 .23  timeout 900     1300 11000    timeout 900    83 10000   true 4.9 290 42 out of memory 40    15000 590   disqualified 880   460 10000 timeout (verification) 900    220 10000   true 7.6 360 63 true 11   540 95 true 7.9 350 60 timeout 900   150 9100
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true .091 24 .95 error (42) 880     5000   5100    error (42) 870     4400   13000    true 3.1 270 25 unknown 1.9  68 22   unknown .029 4.6 .21 unknown .034 4.7 .26  timeout 900     320 13000    timeout 900    75 10000   true 3.1 270 29 timeout 900    360 4100   disqualified 880   850 8500 timeout (verification) 900    1000 9600   true 7.4 330 65 true 11   520 88 true 7.8 350 63 timeout 900   150 13000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true .48  24 5.8  error (42) 880     1200   7800    error (42) 880     1900   13000    true 3.4 280 33 unknown 900    91 13000   unknown .044 4.6 .14 unknown .029 4.7 .17  timeout 900     130 13000    timeout 900    75 10000   true 3.3 270 31 timeout 900    520 5500   disqualified 880   770 9700 timeout (verification) 900    120 8100   true 10   410 75 true 23   800 230 true 10   420 73 timeout 900   150 12000
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 900     2100 11000    error (42) 880     1100   6900    error (42) 870     440   12000    timeout 910   7000 11000 unknown 250    58 3500   unknown .055 4.6 .15 unknown .032 4.7 .19  timeout 900     380 11000    timeout 900    75 9800   timeout 910   7100 13000 timeout 900    380 4500   disqualified 880   490 8900 timeout (verification) 900    380 9000   timeout 900   1800 12000 timeout 900   5400 9300 timeout 900   1400 13000 timeout 900   150 9500
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout 900     430 7200    error (42) 880     660   6700    error (42) 880     4000   12000    true 3.1 270 28 unknown 900    92 11000   unknown .036 4.7 .23 unknown .033 4.6 .14  timeout 900     100 12000    timeout 900    83 9400   true 3.2 270 32 timeout 900    420 5700   disqualified 880   180 11000 timeout (verification) 900    62 14000   true 11   510 83 true 15   700 130 true 13   550 110 timeout 900   200 12000
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout 900     440 7200    error (42) 880     660   8300    error (42) 880     4100   14000    true 3.2 270 30 unknown 900    93 13000   unknown .028 4.6 .18 unknown .029 4.6 .18  timeout 900     110 12000    timeout 900    86 9000   true 3.1 270 28 timeout 900    550 8300   disqualified 880   190 12000 timeout (verification) 900    62 11000   true 11   490 90 true 19   570 180 true 11   510 82 timeout 900   160 13000
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true .10  24 .84 error (42) 880     2200   5300    error (42) 870     4900   12000    timeout 910   8200 11000 unknown 1.8  66 24   unknown .031 4.7 .20 unknown .052 4.7 .16  timeout 900     380 14000    timeout 900    77 9600   timeout 900   8200 10000 timeout 900    390 4800   disqualified 880   490 9900 timeout (verification) 900    320 13000   true 9.7 380 72 true 95   1500 940 true 10   400 83 timeout 900   150 12000
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 900     1200 5500    error (42) 880     6400   7000    error (42) 870     2500   10000    timeout 900   15000 11000 unknown 900    220 13000   unknown .053 4.6 .23 unknown .035 4.6 .22  timeout 900     370 11000    timeout 900    75 9600   timeout 900   15000 12000 out of memory 38    15000 460   disqualified 880   590 11000 timeout (verification) 900    140 12000   timeout 900   2000 13000 timeout 900   2000 7300 timeout 900   1900 11000 timeout 900   150 9900
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 900     1100 9600    error (42) 880     3100   4400    error (42) 880     200   11000    timeout 900   4100 11000 unknown 380    64 3800   unknown .030 4.6 .16 unknown .028 4.6 .27  timeout 900     840 10000    timeout 900    250 8800   timeout 900   4100 9300 timeout 900    410 6100   disqualified 880   820 11000 timeout (verification) 900    420 8400   true 12   500 92 true 120   1600 1500 true 10   450 83 timeout 900   150 12000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true .10  24 .79 true 1.8   50   22    out of memory 190     15000   2200    true 2.9 270 28 unknown .83 66 8.8 unknown .026 4.7 .22 unknown .043 4.7 .15  true .60  26 8.1  timeout 900    2100 9900   true 3.1 260 28 true .39 59 4.1 disqualified 27   170 440 true .19 18 2.0 true 8.2 380 71 true 9.5 380 71 true 8.3 370 58 timeout 900   150 13000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 900     1700 12000    error (42) 880     2400   4800    error (42) 880     210   10000    timeout 910   13000 11000 unknown 58    49 750   unknown .029 4.8 .24 unknown .033 4.7 .24  timeout 900     1100 13000    timeout 900    75 9400   timeout 910   13000 12000 timeout 900    410 3800   disqualified 880   720 9600 timeout (verification) 900    430 7700   timeout 900   3200 14000 timeout 900   5700 7100 timeout 900   1800 14000 timeout 900   150 12000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 900     900 11000    error (42) 880     1400   10000    out of memory 330     15000   4200    timeout 910   620 13000 unknown 720    73 8700   unknown .034 4.6 .24 unknown .035 4.6 .11  timeout 900     130 14000    timeout 900    4000 7600   timeout 910   620 12000 timeout 900    470 8500   disqualified 880   180 11000 timeout (verification) 900    3200 9900   timeout 900   7800 8400 timeout 900   3900 6700 timeout 900   7400 9700 timeout 900   150 12000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true .84  29 10    true .33  10   3.6  out of memory 340     15000   4900    true 59   540 830 unknown 4.7  67 61   unknown .034 4.6 .28 unknown .035 4.7 .24  true .17  26 2.0  timeout 900    4300 6500   true 58   550 770 out of memory 120    15000 1400   disqualified 95   120 1400 timeout (verification) 900    4000 7700   true 180   4800 2000 timeout 900   2700 6000 true 170   4700 1800 timeout 900   150 13000
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true .11  24 .81 error (42) 880     7000   3600    error (42) 880     410   7000    true 3.1 270 30 unknown .77 66 8.3 unknown .036 4.6 .23 unknown .029 4.6 .26  timeout 900     1400 12000    killed by signal 9 890    4500 8700   true 3.1 270 32 timeout 900    510 8200   disqualified 2.4 74 30 true .16 15 2.3 true 7.6 350 55 true 7.8 360 58 true 6.9 340 53 timeout 900   150 13000
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true .14  24 .86 error (42) 880     2000   6800    error (42) 870     180   10000    true 3.1 260 27 unknown .80 67 8.9 unknown .024 4.8 .24 unknown .028 4.6 .23  timeout 900     280 11000    timeout 900    4300 9400   true 3.0 270 30 timeout 900    430 6400   disqualified 880   530 13000 timeout (verification) 900    480 5800   true 8.0 370 59 true 8.6 360 65 true 7.7 370 66 timeout 900   150 11000
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true .10  24 .81 error (42) 880     430   6500    error (42) 880     100   11000    true 2.9 270 26 unknown 1.0  67 11   unknown .030 4.6 .22 unknown .027 4.6 .25  timeout 900     220 11000    timeout 900    83 10000   true 3.1 270 32 timeout 900    330 5900   disqualified 880   810 11000 timeout (verification) 900    420 9200   true 8.6 380 69 true 8.9 380 63 true 8.6 370 73 timeout 900   150 10000
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true .12  24 1.0  error (42) 880     1300   8200    error (42) 880     14000   13000    true 3.0 260 26 unknown .79 66 7.7 unknown .027 4.6 .29 unknown .031 4.6 .22  timeout 900     610 11000    timeout 900    4100 8900   true 3.0 270 29 timeout 900    390 5000   disqualified 880   360 9800 timeout (verification) 900    2800 10000   true 8.5 360 67 true 10   410 77 true 8.2 370 71 timeout 900   150 11000
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true .095 24 1.1  error (42) 880     1600   8100    error (42) 880     11000   10000    true 3.1 270 28 unknown .87 67 9.0 unknown .029 4.6 .18 unknown .027 4.7 .18  timeout 900     540 11000    killed by signal 9 590    5000 6800   true 3.1 270 26 timeout 900    380 5100   disqualified 880   360 11000 timeout (verification) 900    2700 12000   true 8.2 350 66 true 12   550 110 true 8.8 380 69 timeout 900   150 11000
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true .098 24 1.3  error (42) 880     2200   10000    out of memory 540     15000   7200    true 3.1 270 30 unknown .86 66 11   unknown .028 4.6 .14 unknown .034 4.5 .23  timeout 900     770 12000    killed by signal 9 590    5300 7000   true 3.1 270 26 timeout 900    400 6800   disqualified 880   360 9000 timeout (verification) 900    2900 8500   true 8.8 370 65 true 12   490 93 true 7.8 340 70 timeout 900   150 11000
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true .10  24 .83 error (42) 880     550   6500    error (42) 880     9700   11000    true 3.2 270 26 unknown 1.3  67 15   unknown .031 4.6 .19 unknown .039 4.6 .24  timeout 900     140 12000    timeout 900    82 9600   true 3.0 270 26 timeout 900    300 5900   disqualified 880   640 9800 timeout (verification) 900    45 11000   true 8.7 370 69 true 11   570 98 true 8.9 370 76 timeout 900   150 11000
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true .10  24 .73 error (42) 880     1200   9200    error (42) 870     14000   11000    true 3.0 270 26 unknown 1.1  66 12   unknown .031 4.8 .24 unknown .030 4.6 .19  timeout 900     200 12000    timeout 900    75 10000   true 2.9 270 28 timeout 900    320 4500   disqualified 880   600 9000 timeout (verification) 900    600 12000   true 8.2 360 60 true 8.4 350 72 true 8.0 350 60 timeout 900   150 11000
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true .11  24 .72 error (42) 880     1000   7900    out of memory 300     15000   4800    true 3.0 260 28 unknown 1.0  67 13   unknown .031 4.6 .20 unknown .035 4.6 .23  timeout 900     180 11000    timeout 900    83 10000   true 3.0 270 28 out of memory 290    15000 2900   disqualified 880   610 11000 timeout (verification) 900    50 12000   true 8.3 340 70 true 9.3 400 79 true 8.9 390 71 timeout 900   150 13000
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 6.1   110 91    true .22  7.0 2.1  true .26  7.5 1.7  timeout 900   7200 10000 unknown 76    60 930   unknown .030 4.6 .14 unknown .032 4.6 .20  true .39  26 4.8  timeout 900    84 8700   timeout 910   7400 10000 true .44 59 3.7 disqualified 880   680 9100 true .15 15 1.8 true 120   1400 1300 timeout 900   2600 6900 true 190   1200 2300 timeout 900   150 11000
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     2600 10000    error (42) 880     1900   9000    error (42) 870     9800   14000    timeout 900   560 13000 unknown 900    100 12000   unknown .030 4.7 .19 unknown .055 4.5 .19  timeout 900     270 11000    timeout 900    5300 8300   timeout 900   460 13000 timeout 900    400 5300   disqualified 26   120 320 timeout (verification) 900    2800 12000   timeout 900   2900 12000 timeout 900   4900 6600 timeout 900   1600 12000 timeout 900   150 11000
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true .10  24 .81 error (42) 880     1200   7600    out of memory 790     15000   11000    true 3.2 270 28 unknown .79 67 8.8 unknown .031 4.6 .18 unknown .030 4.7 .26  timeout 900     1100 10000    timeout 900    4200 8300   true 3.1 270 31 timeout 900    350 5000   disqualified 890   330 11000 timeout (verification) 900    400 9500   true 8.5 360 68 true 9.0 370 74 true 8.3 360 63 error (1) 3.2 150 33
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 900     1200 11000    error (42) 880     3300   4000    error (42) 880     200   12000    timeout 900   4200 10000 unknown 340    58 4200   unknown .048 4.6 .16 unknown .028 4.6 .23  timeout 900     1200 10000    timeout 900    230 10000   timeout 900   4100 10000 timeout 900    440 4500   disqualified 880   900 10000 timeout (verification) 900    430 7900   true 10   490 78 true 140   1300 1400 true 11   470 100 timeout 900   150 12000
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true .088 24 1.0  error (42) 880     4500   4600    error (42) 870     170   9400    true 3.1 270 27 unknown .80 66 8.2 unknown .028 4.6 .18 unknown .036 4.6 .26  timeout 900     600 11000    timeout 900    75 10000   true 3.1 270 30 timeout 900    400 6000   disqualified 880   720 12000 timeout (verification) 900    460 9500   true 7.2 340 52 true 8.9 360 69 true 8.3 360 64 timeout 900   150 10000
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c true 1.2   45 13    error (42) 880     3200   2800    error (42) 880     200   10000    true 3.2 270 32 unknown 29    67 350   unknown .030 4.6 .17 unknown .027 4.6 .25  timeout 900     1200 11000    timeout 900    74 9100   true 3.2 270 27 timeout 900    380 4000   disqualified 880   8000 10000 timeout (verification) 900    430 6600   true 8.8 360 64 true 14   620 130 true 11   400 87 timeout 900   150 8500
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true .091 24 .98 error (42) 880     3500   5700    error (42) 870     200   11000    true 3.0 270 27 unknown .84 66 10   unknown .054 4.6 .16 unknown .055 4.6 .21  timeout 900     200 13000    timeout 900    4200 9900   true 3.0 270 24 timeout 900    620 6400   disqualified 880   310 12000 timeout (verification) 900    77 13000   true 8.4 370 59 true 8.3 340 63 true 7.8 370 66 timeout 900   150 13000
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 900     2300 13000    error (42) 880     2100   8900    error (42) 870     4800   11000    timeout 900   6700 12000 unknown 88    47 1200   unknown .031 4.6 .19 unknown .034 4.6 .18  timeout 900     880 11000    timeout 900    4700 8000   timeout 900   6900 11000 timeout 900    970 12000   disqualified 890   380 10000 timeout (verification) 900    57 11000   timeout 900   4100 10000 timeout 900   5400 10000 timeout 900   3700 13000 error (1) 3.2 150 30
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true .10  24 .76 error (42) 870     1400   10000    out of memory 830     15000   13000    true 3.0 260 28 unknown .98 65 11   unknown .049 4.6 .16 unknown .035 4.6 .26  timeout 900     210 11000    timeout 900    4800 7400   true 3.0 260 28 timeout 900    400 4300   disqualified 880   460 11000 timeout (verification) 900    2500 11000   true 6.8 340 58 true 8.4 360 64 true 7.1 340 58 timeout 900   150 15000
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c true .10  24 .95 error (42) 880     1700   8400    error (42) 880     4400   12000    true 3.1 270 31 unknown .95 67 10   unknown .027 4.6 .15 unknown .042 4.6 .20  timeout 900     230 11000    timeout 900    82 9500   true 3.0 270 25 out of memory 42    15000 520   disqualified 880   360 13000 timeout (verification) 900    390 8900   true 8.7 380 72 true 9.9 370 78 true 8.4 370 63 timeout 900   150 9800
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 900     830 7000    error (42) 880     910   9800    error (42) 880     3100   12000    timeout 900   560 13000 unknown 900    170 11000   unknown .028 4.6 .26 unknown .035 4.6 .13  timeout 900     260 14000    timeout 900    4300 9800   timeout 900   570 13000 timeout 900    540 5500   disqualified 880   290 13000 timeout (verification) 900    55 12000   timeout 900   990 12000 timeout 900   3600 8900 timeout 900   1900 13000 timeout 900   150 11000
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c error (5) .084 24 .80 out of memory 520     14000   6200    error (42) 880     13000   13000    true 3.6 280 31 out of memory 250    15000 3000   unknown .032 4.6 .16 unknown .027 4.6 .21  out of memory 620     15000 6300    timeout 900    2200 7200   true 3.5 290 32 timeout 900    4500 5400   disqualified 880   140 11000 timeout (verification) 900    380 12000   true 12   500 88 true 13   620 130 true 13   590 100 timeout 900   150 12000
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c error (5) .11  24 .59 out of memory 410     14000   4300    error (42) 880     13000   11000    timeout 900   4200 10000 out of memory 230    15000 2400   unknown .049 4.6 .15 unknown .035 4.6 .22  out of memory 530     15000 5000    timeout 900    2100 13000   timeout 900   5400 10000 out of memory 98    15000 1400   disqualified 890   210 11000 timeout (verification) 900    500 12000   true 19   730 150 timeout 900   2300 9000 true 17   550 130 timeout 900   150 13000
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true .10  24 .88 error (42) 880     1900   8100    error (42) 880     6300   11000    true 3.0 270 27 unknown 2.8  67 38   unknown .039 4.6 .13 unknown .051 4.6 .21  timeout 900     180 11000    timeout 900    76 11000   true 3.1 270 28 timeout 900    320 5800   disqualified 880   280 11000 timeout (verification) 900    100 10000   true 8.1 360 62 true 15   650 140 true 8.7 370 72 timeout 900   150 11000
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true .11  24 .74 error (42) 880     1700   9200    out of memory 500     15000   6500    true 3.0 270 30 unknown .84 66 8.3 unknown .033 4.6 .26 unknown .041 4.6 .22  timeout 900     660 11000    timeout 900    82 9900   true 3.0 260 29 timeout 900    410 4700   disqualified 880   630 10000 timeout (verification) 900    220 7300   true 8.6 380 61 true 8.5 360 76 true 7.6 350 60 timeout 900   150 11000
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true .15  24 .74 true .42  15   3.9  witness invalid (true) .39  15   5.1  true 3.0 270 28 unknown .85 67 9.4 unknown .045 4.6 .13 unknown .049 4.6 .19  true .21  26 2.5  timeout 900    2100 9700   true 2.9 270 26 true .66 130 7.0 disqualified 16   110 190 true .16 15 1.8 true 8.0 360 66 true 7.5 330 58 true 7.2 340 59 timeout 900   150 11000
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 20     600 170    error (42) 870     1300   4600    error (42) 870     4800   13000    true 110   1100 780 unknown 900    200 13000   unknown .035 4.6 .26 unknown .032 4.6 .17  timeout 900     330 12000    timeout 900    75 9700   true 110   1100 840 out of memory 38    15000 520   disqualified 880   250 10000 timeout (verification) 900    310 14000   true 8.1 340 64 true 10   450 84 true 9.4 380 76 timeout 900   150 12000
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true .092 24 .95 error (42) 880     4500   3900    error (42) 870     150   9800    true 3.0 270 28 unknown .79 66 9.1 unknown .037 4.8 .23 unknown .028 4.6 .29  timeout 900     890 10000    timeout 900    74 10000   true 2.9 270 30 timeout 900    360 6000   disqualified 880   650 9000 timeout (verification) 900    430 7100   true 8.2 370 74 true 8.2 360 74 true 8.1 370 62 timeout 900   150 11000
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true .10  24 .73 error (42) 880     2100   5500    error (42) 870     4800   13000    true 3.0 270 26 unknown 1.3  65 16   unknown .030 4.7 .19 unknown .031 4.6 .21  timeout 900     390 13000    timeout 900    74 9700   true 3.1 270 29 timeout 900    490 3600   disqualified 880   830 11000 timeout (verification) 900    980 12000   true 9.6 380 71 timeout 900   2200 8100 true 8.7 360 69 timeout 900   150 12000
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true .13  24 .78 error (42) 880     1300   11000    error (42) 880     14000   12000    true 3.0 270 28 unknown .84 67 7.7 unknown .031 4.7 .18 unknown .035 4.7 .29  timeout 900     550 12000    killed by signal 9 830    4500 11000   true 3.1 270 28 timeout 900    370 5200   disqualified 880   340 8800 timeout (verification) 900    2900 12000   true 8.0 360 63 true 9.0 360 76 true 8.0 350 70 timeout 900   150 11000
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true .10  24 .77 error (42) 880     1400   11000    out of memory 440     15000   5000    true 2.9 270 28 unknown .96 67 11   unknown .033 4.6 .29 unknown .042 4.7 .21  timeout 900     350 10000    timeout 900    75 9500   true 3.0 270 29 timeout 900    3200 4600   disqualified 890   1200 12000 true .22 18 2.6 true 8.4 360 63 true 7.5 340 61 true 7.9 350 57 error (1) 51   150 650
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true .092 24 1.1  error (42) 870     10000   12000    error (42) 880     1400   8800    timeout 910   5200 11000 unknown .82 66 8.3 unknown .032 4.6 .18 unknown .056 4.6 .19  timeout 900     3500 11000    timeout 900    75 8600   timeout 910   5300 12000 out of memory 770    15000 8100   disqualified 880   500 12000 timeout (verification) 900    410 12000   true 9.0 380 69 true 10   460 82 true 8.8 370 75 timeout 900   150 12000
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true .13  24 .78 error (42) 880     890   4900    error (42) 880     200   10000    true 4.8 290 46 unknown .88 67 12   unknown .031 4.6 .18 unknown .053 4.5 .22  timeout 900     810 13000    timeout 900    82 8700   true 4.6 290 44 timeout 900    730 4900   disqualified 880   790 9200 timeout (verification) 900    410 9700   true 9.0 370 75 true 10   460 88 true 9.1 380 72 timeout 900   150 10000
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true .10  24 .79 error (42) 880     2900   11000    out of memory 370     15000   4800    true 3.1 270 29 unknown 1.3  67 16   unknown .028 4.6 .22 unknown .035 4.6 .26  timeout 900     480 12000    timeout 900    4400 9100   true 3.2 270 27 timeout 900    370 5900   disqualified 880   340 12000 timeout (verification) 900    3000 12000   true 8.6 350 72 true 11   500 100 true 9.0 380 75 timeout 900   150 12000
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c true .15  23 .71 error (42) 880     2100   9700    error (42) 880     150   12000    true 3.1 270 28 unknown .82 68 9.1 unknown .031 4.6 .15 unknown .059 4.5 .23  timeout 900     450 13000    timeout 900    84 9800   true 3.0 270 27 out of memory 540    15000 7000   disqualified 2.5 81 33 probably out of memory (killed (signal 9, verification)) 170    15000 2700   true 8.4 370 58 true 7.8 360 61 true 8.1 370 70 timeout 900   150 9900
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 3.6   99 50    true 5.1   140   72    error (42) 880     3200   9300    timeout 910   8200 12000 unknown 34    68 450   unknown .053 4.6 .16 unknown .030 4.6 .19  true 5.3   33 61    timeout 900    2100 12000   timeout 900   8300 10000 out of memory 52    15000 830   disqualified 880   320 11000 timeout (verification) 900    370 12000   timeout 900   7100 7500 timeout 900   1600 6900 timeout 900   6400 9400 timeout 900   150 13000
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c error (134) .21  25 1.5  error (42) 880     5300   5800    error (134) .051 8.1 .30 true 3.7 310 35 unknown .95 68 10   unknown .053 4.6 .16 unknown .034 4.6 .17  timeout 900     5600 10000    true 73    5500 770   true 3.7 310 40 timeout 900    890 7400   disqualified 2.6 75 30 true .20 17 2.8 true 8.9 360 70 true 7.8 340 70 true 9.0 380 65 error (1) 4.1 200 39
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c error (134) .18  24 1.1  error (42) 880     1000   6100    error (134) .050 6.8 .25 true 3.6 300 34 unknown 1.1  67 13   unknown .052 4.6 .16 unknown .030 4.6 .22  timeout 900     1800 11000    true 62    5000 770   true 3.6 310 35 timeout 900    710 5500   disqualified 2.6 81 28 timeout (verification) 900    330 11000   true 8.7 370 72 true 8.7 360 69 true 8.7 370 63 error (1) 4.1 200 40
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c error (134) .16  24 1.7  error (42) 880     6300   3400    error (134) .050 7.2 .34 true 3.2 280 26 unknown .92 68 9.8 unknown .059 4.6 .22 unknown .050 4.5 .18  timeout 900     2600 11000    true 75    4500 720   true 3.2 280 33 timeout 900    1100 11000   disqualified 2.5 73 33 timeout (verification) 900    430 11000   true 7.9 350 61 true 7.6 350 61 true 8.0 350 67 error (1) 4.1 200 37
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c error (134) .16  25 1.4  error (42) 880     1000   5200    error (134) .047 8.2 .41 true 3.6 310 37 unknown 1.1  65 12   unknown .053 4.7 .25 unknown .030 4.6 .20  timeout 900     2100 9500    true 74    5800 790   true 3.6 310 30 timeout 900    690 5100   disqualified 2.5 79 28 true .21 17 2.5 true 8.6 340 70 true 9.3 360 72 true 8.8 370 67 error (1) 4.2 200 34
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c error (134) .17  25 1.4  error (42) 880     1000   6900    error (134) .055 8.1 .38 true 3.6 310 34 unknown 1.1  67 15   unknown .056 4.6 .18 unknown .029 4.6 .20  timeout 900     2000 8900    true 61    5700 790   true 3.5 310 35 timeout 900    700 5200   disqualified 2.5 81 36 timeout (verification) 900    450 12000   true 7.5 340 65 true 8.4 350 62 true 9.1 380 84 error (1) 4.1 200 35
termination-crafted-lit/genady_true-termination_true-no-overflow.c true .69  24 9.1  true 4.4   130   57    true 4.6   170   64    timeout 910   4400 10000 unknown 130    67 1400   unknown .030 4.6 .23 unknown .032 4.6 .18  out of memory 860     15000 8300    timeout 900    76 9400   timeout 910   4500 9500 true 2.6  85 30   disqualified 880   960 7800 true .22 15 2.9 true 11   510 86 true 48   930 490 true 11   480 97 timeout 900   150 11000
termination-crafted-lit/strchr_true-no-overflow_true-termination.c error (134) .16  24 1.4  error (42) 880     5500   5800    error (134) .050 7.9 .27 true 3.2 280 32 unknown .92 66 9.8 unknown .054 4.6 .15 unknown .035 4.7 .23  timeout 900     1800 12000    true 130    5000 1300   true 3.2 260 29 timeout 900    630 6300   disqualified 2.5 77 33 true .23 19 2.1 true 9.1 380 66 true 8.8 340 65 true 8.3 360 70 error (1) 4.3 210 35
termination-numeric/Addition01_false-no-overflow.c error (5) .097 24 .71 false(no-overflow) .096 9.1 .64 false(no-overflow) .093 8.7 .40 false(no-overflow) 3.2 280 28 false(no-overflow) .15 33 1.5 unknown .032 4.6 .17 unknown .030 4.6 .21  false(no-overflow) .080 26 .92 false(no-overflow) 21    91 250   false(no-overflow) 3.3 280 27 false(no-overflow) .35 59 3.5 disqualified 2.7 76 34 false(no-overflow) .24 18 2.8 false(no-overflow) 7.6 370 58 false(no-overflow) 8.1 360 71 false(no-overflow) 6.9 330 54 false(no-overflow) 4.8 150 52
termination-numeric/Avg_true_false-no-overflow.c error (5) .082 24 .87 false(no-overflow) .082 9.6 .77 false(no-overflow) .067 9.6 .58 false(no-overflow) 3.1 270 29 false(no-overflow) .17 34 1.9 unknown .035 4.6 .12 unknown .028 4.6 .21  false(no-overflow) .11  26 1.3  timeout 900    2100 7700   false(no-overflow) 3.1 270 28 false(no-overflow) .36 59 3.9 disqualified 2.8 80 32 false(no-overflow) .24 18 3.0 false(no-overflow) 7.3 340 59 false(no-overflow) 7.8 370 62 false(no-overflow) 7.7 370 58 false(no-overflow) 7.2 200 82
termination-numeric/Binomial_true-termination_false-no-overflow.c error (5) .086 24 .87 false(no-overflow) 25     210   240    out of memory 430     15000   5400    timeout 900   1400 9400 unknown 900    860 9400   unknown .029 4.6 .24 unknown .029 4.9 .20  false(no-overflow) 7.6   77 93    false(no-overflow) .42 83 5.2 timeout 900   1400 9700 false(no-overflow) .56 59 5.9 disqualified 880   200 13000 false(no-overflow) .36 18 4.8 timeout 900   930 11000 timeout 900   1500 10000 timeout 910   13000 8900 false(no-overflow) 4.5 200 42
termination-numeric/Et1_true_false-no-overflow.c error (5) .085 24 .73 false(no-overflow) .078 9.5 .54 false(no-overflow) .069 9.9 .45 false(no-overflow) 3.0 270 27 false(no-overflow) .17 33 1.9 unknown .027 4.6 .23 unknown .028 4.7 .25  false(no-overflow) .13  26 1.2  false(no-overflow) .41 83 4.9 false(no-overflow) 3.0 270 31 false(no-overflow) .38 59 4.0 disqualified 3.1 83 44 false(no-overflow) .24 19 3.2 false(no-overflow) 7.6 350 63 false(no-overflow) 7.9 360 63 false(no-overflow) 8.3 370 71 false(no-overflow) 3.6 160 36
termination-numeric/Et2_true_false-no-overflow.c error (5) .12  24 .77 false(no-overflow) .079 9.8 .84 false(no-overflow) .058 9.4 .59 false(no-overflow) 2.9 270 29 false(no-overflow) .18 34 1.7 unknown .028 4.8 .15 unknown .033 4.6 .26  false(no-overflow) .12  26 1.3  timeout 900    1500 8900   false(no-overflow) 3.1 270 28 false(no-overflow) .39 59 3.2 disqualified 3.1 82 36 false(no-overflow) .23 18 3.1 false(no-overflow) 7.4 350 58 false(no-overflow) 8.4 360 60 false(no-overflow) 8.0 370 69 false(no-overflow) 3.4 150 36
termination-numeric/Et3_true_false-no-overflow.c error (5) .083 24 .78 false(no-overflow) .079 9.5 .55 false(no-overflow) .068 9.4 .50 false(no-overflow) 3.0 270 29 false(no-overflow) .16 33 1.9 unknown .029 4.6 .25 unknown .033 4.6 .19  false(no-overflow) .10  26 1.3  false(no-overflow) .42 83 4.8 false(no-overflow) 3.0 270 30 false(no-overflow) .39 59 3.6 disqualified 3.1 100 39 false(no-overflow) .23 18 2.5 false(no-overflow) 7.9 370 69 false(no-overflow) 7.9 370 61 false(no-overflow) 6.8 330 60 false(no-overflow) 3.6 150 41
termination-numeric/Et4_true_false-no-overflow.c error (5) .13  24 .72 false(no-overflow) .13  9.1 .62 false(no-overflow) .066 9.0 .58 false(no-overflow) 3.1 260 27 false(no-overflow) .19 33 2.3 unknown .034 4.7 .29 unknown .028 4.8 .18  false(no-overflow) .14  26 1.6  timeout 900    1800 8300   false(no-overflow) 2.9 270 27 false(no-overflow) .36 59 3.6 disqualified 3.1 82 37 false(no-overflow) .23 18 2.7 false(no-overflow) 8.2 370 57 false(no-overflow) 8.5 370 67 false(no-overflow) 8.1 360 62 false(no-overflow) 3.4 150 33
termination-numeric/MultCommutative_false-no-overflow.c error (5) .092 24 .72 false(no-overflow) .081 9.8 1.1  error (42) 870     6500   13000    error 6.3 300 63 out of memory 200    15000 3100   unknown .032 4.6 .29 unknown .028 4.6 .25  false(no-overflow) .21  26 2.0  false(no-overflow) 49    200 570   error 5.9 310 51 false(no-overflow) .39 59 3.3 disqualified 2.9 79 38 false(no-overflow) .43 18 6.3 false(no-overflow) 11   510 85 false(no-overflow) 13   620 120 false(no-overflow) 12   540 95 false(no-overflow) 4.7 200 43
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c error (5) .092 24 .70 false(no-overflow) 1.0   63   12    false(no-overflow) 2.9   67   44    timeout 900   1300 7900 false(no-overflow) 6.5  84 89   unknown .029 4.6 .22 unknown .030 4.6 .19  false(no-overflow) 14     50 180    timeout 900    210 11000   timeout 900   1300 7700 timeout 900    3000 4300   disqualified 36   87 530 false(no-overflow) 9.8  50 140   timeout 900   1100 7000 timeout 900   1300 12000 timeout 900   2600 7600 false(no-overflow) 4.3 200 39
termination-numeric/Ackermann01_true-termination_true-no-overflow.c error (5) .086 24 .83 error (42) 870     240   3400    error (42) 870     10000   13000    timeout 910   6900 10000 out of memory 220    15000 3100   unknown .060 4.8 .13 unknown .031 4.6 .18  out of memory 460     15000 5800    timeout 900    150 9900   timeout 900   4000 11000 out of memory 55    15000 800   disqualified 890   230 9500 timeout (verification) 900    14000 14000   timeout 900   8900 7200 timeout 900   1000 9900 timeout 900   7600 7500 timeout 900   150 11000
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c error (5) .12  24 .69 error (42) 880     2800   9200    error (42) 880     280   11000    timeout 900   4300 10000 unknown .90 66 9.6 unknown .028 4.6 .24 unknown .057 4.7 .22  timeout 900     1100 9200    timeout 900    1900 11000   timeout 910   4100 11000 out of memory 100    15000 1500   disqualified 890   190 13000 timeout (verification) 900    1300 14000   true 13   530 110 timeout 900   4600 9100 true 13   550 110 timeout 900   150 11000
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c error (5) .094 24 .77 error (42) 880     180   3300    error (42) 880     12000   11000    true 6.1 320 54 out of memory 180    15000 2200   unknown .046 4.6 .14 unknown .030 4.6 .12  timeout 900     8800 7900    timeout 900    1300 10000   true 5.5 310 53 out of memory 45    15000 700   disqualified 890   290 9000 timeout (verification) 900    2900 12000   timeout 900   6600 11000 timeout 900   1100 11000 timeout 900   5400 10000 timeout 900   200 13000
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c error (5) .087 24 .71 out of memory 690     15000   4500    error (42) 880     350   9100    true 3.3 280 30 unknown .85 66 9.4 unknown .032 4.8 .22 unknown .031 4.6 .22  timeout 900     960 10000    timeout 900    770 8700   true 3.3 280 32 timeout 900    1800 7800   disqualified 890   200 11000 timeout (verification) 900    460 9100   true 8.6 360 67 true 10   490 82 true 8.1 340 59 timeout 900   150 12000
termination-numeric/LogRecursive_true-termination_true-no-overflow.c error (5) .089 24 .77 true 2.6   71   29    true 25     79   310    timeout 900   1300 10000 unknown 4.0  120 46   unknown .031 4.6 .20 unknown .056 4.6 .17  true 81     160 1100    timeout 900    4300 10000   timeout 900   1400 10000 true 4.9  620 67   disqualified 880   360 8900 true 23    160 220   timeout 900   770 12000 timeout 900   5400 11000 timeout 900   960 13000 timeout 900   200 12000
termination-numeric/Parts_true-termination_true-no-overflow.c error (5) .092 24 .70 error (42) 880     730   4500    error (42) 880     14000   11000    timeout 900   3000 10000 unknown 900    7700 11000   unknown .027 4.6 .21 unknown .037 4.6 .15  timeout 900     2800 11000    timeout 900    75 9000   timeout 900   3000 11000 timeout 900    680 5500   disqualified 890   390 7100 timeout (verification) 900    10000 13000   timeout 900   4600 13000 timeout 900   1400 10000 timeout 900   5600 13000 timeout 900   200 10000
termination-numeric/TwoWay_true-termination_true-no-overflow.c error (5) .083 24 .88 error (42) 880     5500   5700    error (42) 880     930   7900    timeout 900   640 8400 unknown 14    84 180   unknown .042 4.6 .19 unknown .053 4.6 .22  timeout 900     200 11000    timeout 900    680 11000   timeout 900   650 9700 out of memory 54    15000 770   disqualified 45   98 540 timeout (verification) 900    9000 11000   true 16   610 140 timeout 900   1100 8700 true 53   710 660 timeout 900   200 12000
termination-numeric/gcd01_true-termination_true-no-overflow.c error (5) .095 24 .79 error (42) 880     4800   5600    error (42) 880     12000   11000    true 3.6 280 32 out of memory 250    15000 3100   unknown .055 4.6 .17 unknown .034 4.7 .22  timeout 900     890 7800    timeout 900    93 13000   true 3.5 290 38 out of memory 180    15000 2600   disqualified 880   100 10000 timeout (verification) 900    59 11000   true 9.5 370 69 true 12   560 96 true 8.7 350 73 timeout 900   150 11000
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true .52  31 7.6  true .52  15   6.4  true 1.4   16   22    true 16   540 160 unknown 7.4  67 110   unknown .029 4.6 .16 unknown .033 4.6 .20  true .19  26 2.7  timeout 900    2000 9300   true 17   540 180 true .66 120 7.3 disqualified 32   130 470 true .42 18 5.4 true 49   990 490 true 220   1500 2800 true 73   1200 840 timeout 900   150 13000
termination-numeric/recHanoi02_true-termination_true-no-overflow.c error (5) .087 24 .86 true .47  12   4.3  true 2.5   16   38    timeout 910   4400 10000 unknown .87 66 9.7 unknown .055 4.5 .21 unknown .032 4.6 .16  true 1.8   27 27    timeout 900    2200 12000   timeout 900   4400 12000 true .59 62 7.4 disqualified 12   84 190 true .66 18 8.3 true 66   1100 650 timeout 900   1300 10000 error (7) 120   2900 1600 timeout 900   200 11000
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (5) .082 24 .84 error (42) 870     5000   6400    error (42) 880     500   11000    timeout 900   4100 10000 unknown 3.4  82 39   unknown .033 4.7 .15 unknown .029 4.7 .20  timeout 900     1200 12000    timeout 900    1100 10000   timeout 900   4300 13000 out of memory 840    15000 11000   disqualified 880   320 9000 timeout (verification) 900    2800 11000   timeout 900   4400 9600 timeout 900   2100 7300 timeout 900   3200 11000 timeout 900   200 9800
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (5) .090 24 .84 error (42) 880     5000   6900    error (42) 880     500   11000    timeout 900   4400 11000 unknown 3.4  82 51   unknown .056 4.6 .16 unknown .031 4.6 .18  timeout 900     1200 9700    timeout 900    1100 8600   timeout 910   4600 9100 out of memory 850    15000 12000   disqualified 880   330 10000 timeout (verification) 900    2800 11000   timeout 900   4600 9600 timeout 900   1800 7200 timeout 900   3600 11000 timeout 900   200 12000
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 900     24 9900    out of memory 290     14000   3600    error (42) 870     5100   11000    timeout 900   7900 13000 unknown 900    740 11000   unknown .030 4.6 .18 unknown .028 4.7 .22  timeout 900     1200 11000    timeout 900    78 11000   timeout 900   7900 10000 timeout 900    500 5100   disqualified 880   180 12000 timeout (verification) 900    1200 11000   timeout 900   1000 11000 timeout 900   1900 7400 timeout 900   990 13000 timeout 900   150 11000
recursive/Addition02WithOverflowBug_false-no-overflow.c error (5) .10  25 .68 false(no-overflow) .14  9.6 .62 false(no-overflow) .069 9.2 .52 false(no-overflow) 3.2 280 30 false(no-overflow) .19 33 1.7 unknown .034 4.6 .16 unknown .029 4.6 .20  false(no-overflow) .12  26 1.1  false(no-overflow) 150    190 2400   false(no-overflow) 3.2 280 30 false(no-overflow) .37 58 3.1 disqualified 2.7 77 37 false(no-overflow) .27 19 3.0 false(no-overflow) 8.5 360 67 false(no-overflow) 6.9 330 53 false(no-overflow) 8.4 370 57 false(no-overflow) 3.6 150 41
recursive/Addition03_false-no-overflow.c error (5) .10  24 .75 false(no-overflow) .083 9.7 .87 false(no-overflow) .066 9.5 .47 false(no-overflow) 3.3 280 28 false(no-overflow) .14 33 1.7 unknown .031 4.7 .21 unknown .031 4.6 .16  false(no-overflow) .091 26 .85 false(no-overflow) 44    140 530   false(no-overflow) 3.2 270 35 false(no-overflow) .36 58 3.4 disqualified 2.7 76 31 false(no-overflow) .26 18 2.8 false(no-overflow) 7.9 360 63 false(no-overflow) 8.6 350 60 false(no-overflow) 7.7 360 62 false(no-overflow) 3.5 160 35
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c error (5) .090 24 .86 false(no-overflow) .079 9.6 .62 false(no-overflow) .12  8.8 .31 false(no-overflow) 3.0 270 26 false(no-overflow) .14 34 1.6 unknown .027 4.6 .20 unknown .031 4.6 .16  false(no-overflow) .088 26 .91 false(no-overflow) 15    85 240   false(no-overflow) 2.9 270 26 false(no-overflow) .37 59 3.2 disqualified 2.7 73 35 false(no-overflow) .28 19 3.1 false(no-overflow) 8.3 370 62 false(no-overflow) 8.6 370 64 false(no-overflow) 8.4 370 69 false(no-overflow) 3.5 150 43
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (5) .090 24 .87 error (42) 880     240   4200    error (42) 880     10000   12000    timeout 910   3800 12000 out of memory 220    15000 2500   unknown .027 4.6 .18 unknown .033 4.6 .25  out of memory 460     15000 4800    timeout 900    130 11000   timeout 910   4200 12000 out of memory 55    15000 690   disqualified 890   230 9500 timeout (verification) 900    13000 12000   timeout 900   6800 10000 timeout 900   1300 11000 timeout 900   7800 7500 timeout 900   150 12000
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (5) .089 24 .87 error (42) 880     230   3200    error (42) 880     10000   11000    timeout 910   9400 12000 out of memory 220    15000 2800   unknown .023 4.6 .34 unknown .033 4.6 .19  out of memory 480     15000 5800    timeout 900    140 10000   timeout 910   4300 12000 out of memory 55    15000 770   disqualified 890   220 9100 timeout (verification) 900    15000 11000   timeout 900   8300 7100 timeout 900   1100 9600 timeout 900   7500 11000 timeout 900   150 13000
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (5) .086 24 1.4  error (42) 880     230   3200    error (42) 870     11000   12000    timeout 910   4400 11000 out of memory 220    15000 2700   unknown .051 4.6 .17 unknown .043 4.6 .15  out of memory 470     15000 5300    timeout 900    230 10000   timeout 910   3300 10000 out of memory 55    15000 760   disqualified 890   220 7600 timeout (verification) 900    13000 12000   timeout 900   8000 6800 timeout 900   1200 11000 timeout 900   7200 8500 timeout 900   150 13000
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (5) .12  24 .71 error (42) 880     230   3100    error (42) 880     11000   11000    timeout 900   5300 12000 out of memory 220    15000 2600   unknown .029 4.6 .22 unknown .034 4.5 .18  out of memory 470     15000 5300    timeout 900    280 11000   timeout 910   4000 11000 out of memory 55    15000 620   disqualified 890   230 9900 timeout (verification) 900    13000 14000   timeout 900   6600 8300 timeout 900   1000 10000 timeout 900   7500 7200 timeout 900   150 13000
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (5) .084 24 .88 out of memory 760     15000   9000    error (42) 880     3600   11000    timeout 900   5600 12000 out of memory 220    15000 3200   unknown .042 4.5 .11 unknown .034 4.6 .19  out of memory 840     15000 7900    timeout 900    1300 11000   timeout 910   5500 11000 out of memory 73    15000 850   disqualified 890   230 11000 timeout (verification) 900    250 12000   timeout 900   2800 11000 timeout 900   3200 8100 timeout 900   2000 11000 timeout 900   150 11000
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (5) .11  24 .70 out of memory 770     15000   7400    error (42) 870     3600   12000    timeout 900   5600 12000 out of memory 220    15000 2800   unknown .037 4.6 .21 unknown .028 4.7 .22  out of memory 840     15000 8200    timeout 900    2000 12000   timeout 900   5400 11000 out of memory 69    15000 830   disqualified 890   240 11000 timeout (verification) 900    250 13000   timeout 900   2600 13000 timeout 900   3700 10000 timeout 900   1800 13000 timeout 900   160 11000
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (5) .087 23 1.0  error (42) 880     15000   9800    error (42) 880     7100   11000    timeout 900   1900 9800 out of memory 220    15000 2800   unknown .050 4.7 .16 unknown .028 4.8 .22  out of memory 840     15000 9300    false(no-overflow) 45    140 530   timeout 900   1900 11000 out of memory 47    15000 640   disqualified 890   170 12000 timeout (verification) 900    440 11000   timeout 900   1500 13000 timeout 900   1800 6900 timeout 900   1400 12000 timeout 900   150 8800
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c error (5) .11  24 .75 true .092 6.2 .42 witness invalid (true) .054 6.7 .48 true 3.2 280 28 unknown .78 66 9.3 unknown .028 4.6 .20 unknown .032 4.6 .15  true .086 26 1.1  timeout 900    2200 11000   true 3.2 280 30 true .35 59 3.6 disqualified 2.0 70 24 true .20 16 2.4 true 8.2 360 59 true 7.1 340 59 true 7.8 350 60 error (1) 3.0 150 32
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (5) .10  23 .66 error (42) 880     2800   9300    error (42) 880     280   10000    timeout 910   4400 11000 unknown .90 65 8.5 unknown .029 4.6 .17 unknown .031 4.6 .21  timeout 900     1100 12000    timeout 900    1900 11000   timeout 900   4000 12000 out of memory 89    15000 1300   disqualified 890   190 11000 timeout (verification) 900    1300 11000   true 14   490 110 timeout 900   4800 10000 true 13   530 110 timeout 900   150 11000
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (5) .094 24 .74 error (42) 880     2800   7900    error (42) 880     280   12000    timeout 910   4700 9000 unknown .91 69 10   unknown .030 4.6 .18 unknown .032 4.6 .24  timeout 900     1100 13000    timeout 900    1900 11000   timeout 900   5700 12000 out of memory 90    15000 1200   disqualified 890   190 12000 timeout (verification) 900    1300 11000   true 14   520 120 timeout 900   5300 10000 true 14   520 130 timeout 900   150 11000
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (5) .095 24 .83 error (42) 880     200   7500    error (42) 880     13000   11000    true 4.8 300 44 out of memory 180    15000 2600   unknown .052 4.6 .16 unknown .036 4.6 .21  timeout 900     8800 10000    timeout 900    86 9600   true 5.8 310 60 out of memory 47    15000 670   disqualified 890   210 10000 probably out of memory (killed (signal 9, verification)) 770    15000 12000   timeout 900   5500 12000 timeout 900   960 11000 timeout 900   5500 14000 timeout 900   200 12000
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c error (5) .095 24 .68 true .12  7.6 1.2  true .19  8.1 1.1  true 680   760 6100 unknown .79 66 8.4 unknown .056 4.7 .16 unknown .027 4.7 .20  true .13  26 1.4  timeout 900    83 9100   true 670   770 6500 true .44 59 3.7 disqualified 160   150 2000 true .21 17 1.9 true 31   1100 300 timeout 900   1100 11000 true 140   6100 1400 timeout 900   200 11000
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (5) .083 24 .87 error (42) 880     190   5100    error (42) 880     13000   12000    true 7.6 400 78 out of memory 180    15000 2300   unknown .031 4.6 .14 unknown .039 4.9 .19  timeout 900     8800 6700    timeout 900    86 9800   true 5.4 300 46 out of memory 47    15000 620   disqualified 890   210 11000 probably out of memory (killed (signal 9, verification)) 710    15000 9800   timeout 900   5800 11000 timeout 900   930 10000 timeout 900   5200 11000 timeout 900   200 10000
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (5) .083 24 .85 error (42) 880     180   3500    error (42) 880     13000   11000    true 5.8 300 61 out of memory 180    15000 2500   unknown .031 4.6 .18 unknown .035 4.6 .28  timeout 900     8800 6200    timeout 900    1300 13000   true 4.8 300 43 out of memory 45    15000 730   disqualified 890   210 11000 timeout (verification) 900    2400 11000   timeout 900   5400 12000 timeout 900   900 11000 timeout 900   4900 10000 timeout 900   200 13000
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (5) .085 24 .80 error (42) 880     180   4000    error (42) 880     13000   12000    true 5.7 310 61 out of memory 180    15000 2200   unknown .028 4.6 .16 unknown .030 4.6 .23  timeout 900     8800 6700    timeout 900    1300 13000   true 4.8 310 40 out of memory 45    15000 680   disqualified 890   210 9400 timeout (verification) 900    3000 10000   timeout 900   5600 14000 timeout 900   900 9900 timeout 900   5200 10000 timeout 900   200 13000
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (5) .087 24 .88 error (42) 880     1600   4100    error (42) 870     6200   12000    true 3.6 280 38 out of memory 170    15000 2500   unknown .027 4.6 .21 unknown .032 4.6 .20  timeout 900     6400 8000    timeout 900    320 11000   true 3.6 280 35 out of memory 43    15000 660   disqualified 880   180 9200 timeout (verification) 900    260 12000   true 9.3 390 80 true 10   460 75 true 9.9 420 74 timeout 900   150 13000
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (5) .088 24 .97 error (42) 880     1600   3400    error (42) 880     6300   13000    true 3.7 280 32 out of memory 170    15000 2300   unknown .028 4.8 .22 unknown .055 4.7 .15  timeout 900     6400 7400    timeout 900    330 11000   true 3.7 290 34 out of memory 43    15000 620   disqualified 880   180 9600 timeout (verification) 900    260 11000   true 9.8 390 75 true 9.5 450 92 true 8.7 380 73 timeout 900   150 12000
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (5) .11  24 .80 error (42) 880     330   3500    error (42) 870     6100   10000    error 5.0 300 48 out of memory 200    15000 2500   unknown .034 4.6 .28 unknown .050 4.6 .23  out of memory 760     15000 7400    timeout 900    1600 11000   error 5.0 300 46 out of memory 43    15000 560   disqualified 890   220 12000 timeout (verification) 900    220 11000   timeout 900   960 6800 timeout 900   980 9600 timeout 910   14000 5200 timeout 900   200 13000
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (5) .11  24 .94 error (42) 880     200   3100    out of memory 860     15000   12000    error 11   330 110 out of memory 220    15000 2700   unknown .056 4.6 .22 unknown .032 4.6 .25  out of memory 230     15000 2600    timeout 900    1300 12000   error 11   410 98 out of memory 850    15000 5600   disqualified 890   210 10000 timeout (verification) 900    120 12000   timeout 900   950 8000 timeout 900   1100 10000 timeout 910   14000 5100 timeout 900   200 13000
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (5) .086 24 .86 error (42) 880     4800   8100    error (42) 880     12000   8100    true 3.5 280 33 out of memory 250    15000 3200   unknown .029 4.7 .15 unknown .028 4.6 .22  timeout 900     890 8100    timeout 900    99 14000   true 3.5 280 37 out of memory 180    15000 2500   disqualified 880   100 12000 timeout (verification) 900    63 12000   true 8.8 370 72 true 11   490 110 true 8.7 350 64 timeout 900   150 12000
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (5) .085 24 .88 error (42) 880     6800   9700    error (42) 870     6900   11000    true 4.0 290 42 out of memory 220    15000 2100   unknown .055 4.6 .16 unknown .031 4.6 .20  timeout 900     1200 7400    timeout 900    90 12000   true 4.0 300 35 out of memory 230    15000 3200   disqualified 880   120 11000 timeout (verification) 900    62 13000   true 15   610 120 timeout 900   990 11000 true 17   660 140 timeout 900   200 10000
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (5) .086 24 .81 error (42) 880     1400   3500    error (42) 880     14000   13000    timeout 910   6600 11000 out of memory 180    15000 2400   unknown .050 4.7 .26 unknown .047 4.7 .17  timeout 900     13000 9100    timeout 900    92 9300   timeout 900   6200 10000 timeout 900    4500 6300   disqualified 61   150 880 probably out of memory (killed (signal 9, verification)) 830    15000 14000   timeout 900   2000 10000 timeout 900   1700 11000 timeout 900   5200 9000 error (1) 4.2 200 39
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c error (5) .10  24 .63 true .37  12   4.3  true 2.5   16   35    timeout 910   4600 11000 unknown .91 66 9.8 unknown .030 4.7 .19 unknown .029 4.6 .17  true 1.8   27 28    timeout 900    2200 10000   timeout 900   4300 12000 true .62 62 6.3 disqualified 12   84 150 true .68 23 8.5 true 63   1200 620 timeout 900   1400 14000 error (7) 140   2300 2000 timeout 900   200 12000
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c error (5) .086 24 .76 true .44  12   4.2  true 2.6   16   32    timeout 910   4600 11000 unknown .87 66 10   unknown .052 4.6 .17 unknown .041 4.6 .22  true 1.8   27 24    timeout 900    2200 9800   timeout 900   4000 10000 true .67 68 6.6 disqualified 26   100 360 true .67 18 8.1 true 64   1000 660 timeout 900   1100 8500 error (7) 110   2400 1400 timeout 900   200 12000
recursive-simple/id_b3_o2_false-no-overflow.c error (5) .084 24 .81 false(no-overflow) .097 9.2 .39 false(no-overflow) .088 8.6 .38 false(no-overflow) 3.1 280 29 false(no-overflow) .14 34 1.5 unknown .052 4.6 .13 unknown .032 4.6 .29  false(no-overflow) .093 26 .93 false(no-overflow) 6.7  91 91   false(no-overflow) 3.2 280 32 false(no-overflow) .36 58 3.7 disqualified 2.7 74 31 false(no-overflow) .24 18 2.8 false(no-overflow) 7.2 330 57 false(no-overflow) 8.2 360 61 false(no-overflow) 7.8 360 56 false(no-overflow) 4.4 200 42
recursive-simple/id_b3_o5_false-no-overflow.c error (5) .094 24 .65 false(no-overflow) .073 9.0 .51 false(no-overflow) .066 9.6 .50 false(no-overflow) 3.1 280 28 false(no-overflow) .14 33 1.4 unknown .033 4.6 .29 unknown .028 4.5 .25  false(no-overflow) .11  26 .83 false(no-overflow) 6.7  91 92   false(no-overflow) 3.2 280 28 false(no-overflow) .38 59 3.4 disqualified 2.7 74 30 false(no-overflow) .29 18 3.2 false(no-overflow) 8.1 370 64 false(no-overflow) 8.4 380 60 false(no-overflow) 8.2 370 67 false(no-overflow) 4.4 200 39
recursive-simple/id_b5_o10_false-no-overflow.c error (5) .12  24 .77 false(no-overflow) .11  8.5 .37 false(no-overflow) .14  8.1 .31 false(no-overflow) 3.1 270 28 false(no-overflow) .14 33 1.5 unknown .034 4.6 .29 unknown .030 4.7 .19  false(no-overflow) .11  26 .77 false(no-overflow) 6.7  91 86   false(no-overflow) 3.2 280 27 false(no-overflow) .36 59 3.3 disqualified 2.6 74 35 false(no-overflow) .25 18 2.8 false(no-overflow) 8.1 370 59 false(no-overflow) 8.3 370 69 false(no-overflow) 8.0 380 56 false(no-overflow) 4.3 200 43
recursive-simple/sum_non_eq_false-no-overflow.c error (5) .085 24 .81 false(no-overflow) .15  9.1 .42 false(no-overflow) .068 9.1 .40 false(no-overflow) 3.1 280 31 false(no-overflow) .15 33 1.9 unknown .051 4.6 .14 unknown .029 4.7 .26  false(no-overflow) .092 26 1.4  false(no-overflow) 18    100 220   false(no-overflow) 3.2 280 31 false(no-overflow) .37 59 3.1 disqualified 2.7 74 31 false(no-overflow) .26 19 2.3 false(no-overflow) 8.6 360 63 false(no-overflow) 8.1 350 56 false(no-overflow) 8.2 370 72 false(no-overflow) 3.7 150 34
recursive-simple/sum_non_false-no-overflow.c error (5) .11  24 .71 false(no-overflow) .074 9.3 .63 false(no-overflow) .061 9.8 .64 false(no-overflow) 3.2 280 30 false(no-overflow) .14 33 1.6 unknown .027 4.6 .25 unknown .030 4.6 .17  false(no-overflow) .085 26 1.2  false(no-overflow) 56    120 800   false(no-overflow) 3.2 280 32 false(no-overflow) .37 59 3.1 disqualified 2.7 76 35 false(no-overflow) .26 19 3.2 false(no-overflow) 8.7 380 62 false(no-overflow) 9.2 360 75 false(no-overflow) 8.9 370 73 false(no-overflow) 3.8 150 33
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (5) .087 24 .74 error (42) 880     5000   4800    error (42) 880     550   10000    true 3.2 270 31 unknown .84 66 8.5 unknown .036 4.8 .24 unknown .033 4.6 .19  timeout 900     1100 11000    timeout 900    290 8700   true 3.1 280 31 out of memory 200    15000 2500   disqualified 2.0 73 27 true .20 17 2.9 true 7.1 350 54 true 7.9 350 60 true 7.9 370 60 timeout 900   200 13000
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (5) .10  24 .59 error (42) 880     5000   5400    error (42) 880     550   11000    true 3.1 270 32 unknown .81 67 9.1 unknown .031 4.7 .21 unknown .027 4.6 .27  timeout 900     1100 11000    timeout 900    290 9200   true 3.3 280 29 out of memory 200    15000 2500   disqualified 2.0 72 22 true .20 16 2.2 true 8.1 360 55 true 8.5 360 65 true 8.0 360 50 timeout 900   200 11000
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (5) .094 24 .75 error (42) 880     5000   6700    error (42) 870     550   10000    true 3.1 280 32 unknown .80 67 10   unknown .048 4.7 .14 unknown .044 4.7 .20  timeout 900     1100 9400    timeout 900    290 8900   true 3.4 280 30 out of memory 200    15000 2500   disqualified 2.1 73 25 true .19 15 2.6 true 7.7 350 68 true 7.7 370 58 true 7.7 350 57 timeout 900   200 11000
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (5) .091 24 .72 error (42) 880     5000   5900    error (42) 880     540   9700    true 3.2 270 29 unknown .82 66 8.8 unknown .036 4.6 .14 unknown .039 4.8 .24  timeout 900     1100 8900    timeout 900    290 8700   true 3.3 280 30 out of memory 200    15000 2800   disqualified 2.1 73 22 true .20 16 1.9 true 8.2 370 65 true 7.8 370 64 true 8.1 370 66 timeout 900   200 12000
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (5) .093 23 1.2  error (42) 880     9900   6100    error (42) 880     540   11000    true 3.1 270 30 unknown .79 67 9.2 unknown .030 4.6 .21 unknown .030 4.6 .21  timeout 900     1100 10000    timeout 900    290 10000   true 3.2 280 28 out of memory 190    15000 2400   disqualified 2.1 72 22 true .20 17 2.4 true 7.9 350 58 true 7.8 370 57 true 7.9 340 55 timeout 900   210 12000
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (5) .082 24 .79 error (42) 880     640   13000    error (42) 880     380   10000    true 4.3 300 41 unknown .98 66 10   unknown .028 4.6 .20 unknown .043 4.6 .18  timeout 900     520 12000    timeout 900    1300 8800   true 4.4 290 37 out of memory 480    15000 6600   disqualified 890   240 13000 timeout (verification) 900    1500 12000   true 8.3 370 62 true 9.7 380 80 true 9.9 390 81 timeout 900   200 12000
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (5) .091 24 .87 error (42) 880     640   13000    error (42) 880     380   12000    true 4.2 290 42 unknown .95 66 10   unknown .031 4.6 .20 unknown .026 4.7 .22  timeout 900     520 13000    timeout 900    1300 11000   true 4.4 300 37 out of memory 480    15000 6700   disqualified 890   240 14000 timeout (verification) 900    1500 8200   true 8.6 360 64 true 9.5 380 73 true 9.8 390 77 timeout 900   200 11000
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (5) .12  24 .64 error (42) 880     5000   6600    error (42) 870     390   10000    true 5.2 310 45 unknown .95 66 12   unknown .055 4.7 .16 unknown .028 4.7 .26  timeout 900     530 13000    timeout 900    1300 11000   true 5.1 310 48 out of memory 480    15000 6100   disqualified 890   240 11000 timeout (verification) 900    1500 9300   true 9.0 370 75 true 9.7 380 67 true 9.8 400 79 timeout 900   200 12000
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c error (5) .092 24 .72 out of memory 640     15000   4500    error (42) 870     790   10000    true 3.1 280 27 unknown .79 66 9.4 unknown .047 4.6 .11 unknown .056 4.6 .16  timeout 900     1000 9600    timeout 900    300 8300   true 3.2 280 29 out of memory 170    15000 2000   disqualified 2.0 72 25 true .19 17 2.4 true 6.9 320 50 true 8.0 360 59 true 8.2 370 58 timeout 900   200 12000
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c error (5) .089 24 .72 out of memory 700     15000   3900    error (42) 880     790   12000    true 3.2 270 27 unknown .77 65 9.2 unknown .028 4.6 .21 unknown .027 4.7 .30  timeout 900     1000 11000    timeout 900    300 8500   true 3.0 270 29 out of memory 170    15000 2000   disqualified 2.1 71 23 true .20 17 2.1 true 7.2 350 54 true 6.9 330 56 true 7.5 370 55 timeout 900   250 9800
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c error (5) .096 24 .85 out of memory 660     15000   4200    error (42) 880     780   10000    true 3.2 270 27 unknown .81 65 8.2 unknown .040 4.6 .26 unknown .031 4.6 .25  timeout 900     1000 11000    timeout 900    300 8200   true 3.1 270 30 out of memory 170    15000 2100   disqualified 2.0 72 26 true .19 16 2.1 true 7.4 350 57 true 7.4 360 62 true 7.7 360 56 timeout 900   200 12000
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c error (5) .095 24 .67 out of memory 690     15000   4100    error (42) 880     790   11000    true 3.1 280 32 unknown .80 66 8.6 unknown .029 4.6 .20 unknown .051 4.6 .14  timeout 900     1000 11000    timeout 900    300 7200   true 3.1 270 28 out of memory 170    15000 2000   disqualified 2.0 70 23 true .19 16 2.0 true 6.6 330 57 true 7.6 350 63 true 8.2 360 60 timeout 900   200 12000
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c error (5) .088 24 .75 out of memory 720     15000   3700    error (42) 880     800   9100    true 3.0 270 28 unknown .76 65 8.2 unknown .031 4.6 .18 unknown .033 4.6 .21  timeout 900     1000 9200    timeout 900    300 8600   true 3.1 270 29 out of memory 170    15000 2300   disqualified 2.0 72 24 true .19 17 2.3 true 7.2 350 60 true 8.2 370 71 true 7.0 340 56 timeout 900   200 13000
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c error (5) .092 23 .76 out of memory 710     15000   4700    error (42) 880     790   9800    true 3.1 270 27 unknown .80 67 8.9 unknown .028 4.7 .22 unknown .035 4.6 .24  timeout 900     990 11000    timeout 900    310 9400   true 3.1 270 29 out of memory 170    15000 2200   disqualified 2.0 72 25 true .20 17 2.6 true 7.1 330 62 true 8.2 350 58 true 8.1 370 60 timeout 900   200 10000
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c error (5) .091 24 .70 error (42) 880     11000   4700    error (42) 880     730   10000    true 3.0 270 28 unknown .80 66 8.6 unknown .053 4.6 .16 unknown .035 4.5 .28  timeout 900     980 9600    killed by signal 9 300    340 3300   true 3.2 280 28 out of memory 90    15000 1100   disqualified 2.1 72 25 true .19 16 2.4 true 8.0 360 60 true 7.8 370 57 true 7.9 370 61 timeout 900   150 11000
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c error (5) .087 23 .95 out of memory 820     15000   8000    error (42) 880     720   9000    true 3.1 270 29 unknown .79 66 10   unknown .054 4.6 .16 unknown .026 4.6 .24  timeout 900     980 11000    killed by signal 9 360    390 3700   true 3.1 280 27 out of memory 86    15000 1200   disqualified 2.1 72 26 true .20 16 2.1 true 8.4 370 67 true 7.5 360 57 true 7.7 360 60 timeout 900   150 11000
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) .36  24 3.8  false(no-overflow) .13  9.8 1.0  false(no-overflow) .30  12   3.1  false(no-overflow) 6.4 320 58 false(no-overflow) .42 35 5.6 unknown .047 4.6 .16 unknown .028 4.6 .22  false(no-overflow) .11  27 1.2  timeout 900    2000 11000   false(no-overflow) 6.6 320 56 false(no-overflow) .44 59 4.1 disqualified 69   310 550 false(no-overflow) .55 18 6.8 error 29   610 280 timeout 900   1200 8800 error (7) 12   490 97 false(no-overflow) 5.1 210 46
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) .37  24 4.0  false(no-overflow) .14  10   1.1  false(no-overflow) .29  12   3.3  false(no-overflow) 7.1 330 63 false(no-overflow) .40 36 4.9 unknown .029 4.6 .22 unknown .057 4.7 .22  false(no-overflow) .12  27 1.0  timeout 900    2000 9800   false(no-overflow) 6.8 330 66 false(no-overflow) .47 59 4.0 disqualified 65   330 610 false(no-overflow) .55 18 6.9 error 31   750 250 timeout 900   1100 6900 error (7) 13   510 110 false(no-overflow) 5.0 210 49
bitvector/byte_add_false-no-overflow.i false(no-overflow) .37  24 4.3  false(no-overflow) .13  9.5 1.5  false(no-overflow) .68  24   9.0  false(no-overflow) 7.4 310 74 false(no-overflow) .45 35 5.4 unknown .055 4.6 .17 unknown .053 4.6 .19  false(no-overflow) .14  27 2.2  timeout 900    3900 9300   false(no-overflow) 7.2 350 74 false(no-overflow) .41 59 4.2 disqualified 110   340 880 false(no-overflow) 1.0  18 14   error 42   630 400 timeout 900   1100 7800 error 64   850 540 false(no-overflow) 5.2 210 47
bitvector/jain_1_false-no-overflow.i false(no-overflow) .11  24 1.0  false(no-overflow) .070 9.3 .38 false(no-overflow) .065 9.0 .37 false(no-overflow) 3.4 310 34 false(no-overflow) .14 33 1.7 unknown .031 4.8 .16 unknown .055 4.6 .15  false(no-overflow) .086 26 .87 false(no-overflow) 130    4400 1300   false(no-overflow) 3.5 300 34 false(no-overflow) .36 58 3.3 disqualified 3.1 89 41 false(no-overflow) .25 19 3.6 false(no-overflow) 7.3 360 51 false(no-overflow) 7.4 350 64 false(no-overflow) 7.6 360 62 false(no-overflow) 3.5 160 35
bitvector/jain_2_false-no-overflow.i false(no-overflow) .11  24 1.4  false(no-overflow) .095 9.9 .78 false(no-overflow) .067 9.3 .48 false(no-overflow) 3.4 300 30 false(no-overflow) .16 33 1.6 unknown .029 4.7 .22 unknown .030 4.6 .19  false(no-overflow) .083 26 1.1  false(no-overflow) 110    4100 1100   false(no-overflow) 3.4 300 34 false(no-overflow) .35 58 3.1 disqualified 3.2 110 43 false(no-overflow) .27 18 3.1 false(no-overflow) 7.7 360 57 false(no-overflow) 8.1 370 61 false(no-overflow) 7.5 350 63 false(no-overflow) 3.5 150 35
bitvector/jain_4_false-no-overflow.i false(no-overflow) .12  24 1.1  false(no-overflow) .086 9.3 .72 false(no-overflow) .10  9.2 .46 false(no-overflow) 3.4 300 36 false(no-overflow) .14 34 1.7 unknown .038 4.7 .16 unknown .041 4.6 .21  false(no-overflow) .079 26 .84 false(no-overflow) 110    4200 1100   false(no-overflow) 3.5 300 36 false(no-overflow) .37 58 3.3 disqualified 3.4 110 43 false(no-overflow) .25 18 2.7 false(no-overflow) 8.0 360 57 false(no-overflow) 7.8 360 60 false(no-overflow) 7.1 330 57 false(no-overflow) 3.4 150 31
bitvector/jain_5_false-no-overflow.i timeout 900     1000 8800    out of memory 260     15000   3200    out of memory 190     15000   2800    timeout 910   4100 11000 unknown 87    55 1300   unknown .029 4.6 .20 unknown .028 4.6 .17  out of memory 830     15000 10000    false(no-overflow) .40 83 4.8 timeout 900   4000 11000 false(no-overflow) 67    1300 840   disqualified 890   530 8800 false(no-overflow) 1.2  50 15   timeout 900   1500 9300 timeout 900   3500 7800 error (7) 680   2400 8900 timeout 900   150 11000
bitvector/jain_6_false-no-overflow.i false(no-overflow) .14  24 .99 false(no-overflow) .084 9.4 .73 false(no-overflow) .084 9.4 .48 false(no-overflow) 3.4 300 30 false(no-overflow) .14 33 1.5 unknown .035 4.8 .23 unknown .057 4.6 .17  false(no-overflow) .088 26 .98 false(no-overflow) 110    4300 1200   false(no-overflow) 3.5 300 31 false(no-overflow) .36 58 3.2 disqualified 3.5 140 44 false(no-overflow) .25 17 2.5 false(no-overflow) 7.2 350 56 false(no-overflow) 8.1 370 70 false(no-overflow) 8.1 360 69 false(no-overflow) 3.4 150 37
bitvector/jain_7_false-no-overflow.i false(no-overflow) .16  23 .97 false(no-overflow) .081 9.2 .71 false(no-overflow) .075 9.1 .49 false(no-overflow) 3.4 300 31 false(no-overflow) .18 34 1.5 unknown .031 4.6 .24 unknown .029 4.7 .19  false(no-overflow) .090 26 1.0  false(no-overflow) 120    4500 1100   false(no-overflow) 3.3 300 31 false(no-overflow) .36 58 2.8 disqualified 3.6 140 50 false(no-overflow) .28 19 3.0 false(no-overflow) 7.3 340 60 false(no-overflow) 7.5 350 57 false(no-overflow) 7.7 370 61 false(no-overflow) 3.5 150 37
bitvector/modulus_false-no-overflow.i false(no-overflow) .13  24 1.2  false(no-overflow) .071 10   .56 false(no-overflow) .061 9.7 .69 false(no-overflow) 3.0 270 29 false(no-overflow) .16 33 1.3 unknown .047 4.6 .11 unknown .037 4.6 .16  false(no-overflow) .11  26 .79 timeout 900    920 11000   false(no-overflow) 2.9 270 30 false(no-overflow) .35 59 3.1 disqualified 3.3 83 53 false(no-overflow) .27 19 3.3 error 8.5 360 60 error 6.9 330 52 error 7.0 340 61 false(no-overflow) 4.5 200 42
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .12  24 1.0  true .12  6.3 1.2  true .34  12   5.1  true 4.0 280 38 unknown .86 66 9.4 unknown .031 4.6 .25 unknown .029 4.6 .15  true .13  27 1.6  timeout 900    2000 10000   true 3.8 270 34 true .54 60 5.6 disqualified 64   330 500 true .67 18 9.5 true 9.3 380 69 true 11   400 82 true 8.2 350 59 timeout 900   210 13000
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .11  25 1.7  true .12  6.5 1.1  true .35  14   4.3  true 3.9 280 41 unknown .87 66 9.7 unknown .028 4.6 .28 unknown .048 4.6 .19  true .13  27 1.4  timeout 900    2000 9300   true 4.0 290 34 true .57 59 6.1 disqualified 75   330 810 true .70 19 11   true 9.3 380 70 true 9.9 390 85 true 7.7 350 69 timeout 900   210 10000
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true .12  25 .90 true .12  6.8 1.7  true 1.5   42   21    true 3.9 280 37 unknown .89 67 11   unknown .037 4.6 .22 unknown .032 4.6 .18  true .17  27 2.1  timeout 900    3800 10000   true 4.0 280 40 true 1.3  96 17   disqualified 83   340 780 true 2.0  19 27   true 7.9 340 66 true 11   400 81 true 8.6 360 72 timeout 900   210 13000
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .11  24 1.0  true .25  8.3 2.1  true .24  8.4 2.4  true 3.1 280 32 unknown 1.0  66 11   unknown .028 4.6 .21 unknown .034 4.6 .30  true .52  28 7.9  true 900    4300 11000   true 3.2 270 29 true .47 60 4.3 disqualified 2.5 99 31 true .40 21 4.8 true 8.6 380 74 true 9.0 380 67 true 8.7 360 69 timeout 900   200 12000
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true .11  23 .87 true .49  21   6.2  true .72  21   9.0  true 3.2 270 26 unknown .95 67 11   unknown .037 4.6 .33 unknown .027 4.6 .23  true 9.2   42 140    timeout 900    4300 10000   true 3.1 270 28 true 6.0  680 83   disqualified 2.5 74 32 true 93    46 1200   true 8.9 370 76 true 9.2 380 65 true 8.9 380 66 timeout 900   200 9900
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true .11  24 .82 true .52  21   7.0  true .76  21   11    true 3.1 270 26 unknown .96 67 11   unknown .041 4.7 .11 unknown .027 4.6 .21  true 9.2   43 110    timeout 900    4300 10000   true 3.1 270 34 true 6.0  690 77   disqualified 2.5 74 31 true 100    44 1300   true 8.8 370 65 true 9.4 370 75 true 8.9 380 66 timeout 900   200 10000
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .37  23 4.1  true .062 6.9 .58 true .073 6.9 .48 true 4.5 300 43 unknown 2.2  66 25   unknown .029 4.5 .30 unknown .031 4.8 .26  true .084 26 .84 timeout 900    84 9700   true 4.4 300 40 true .37 58 3.2 disqualified 2.6 85 33 true .19 16 2.2 true 15   510 130 true 27   670 250 true 14   510 130 timeout 900   200 11000
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .098 24 1.2  true .16  6.4 .93 witness invalid (true) .11  6.4 .89 true 3.1 260 29 unknown .82 66 11   unknown .054 4.6 .16 unknown .028 4.7 .16  true .095 26 1.2  timeout 900    4300 9600   true 3.0 270 27 true .37 58 3.2 disqualified 2.4 83 37 true .19 16 2.2 true 7.6 370 63 true 8.0 350 55 true 8.5 370 57 timeout 900   150 12000
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true .10  23 1.2  error (42) 880     650   3500    out of memory 110     15000   1700    true 2.9 270 27 unknown .77 66 8.0 unknown .028 4.5 .17 unknown .048 4.6 .19  timeout 900     1400 11000    timeout 900    4200 7800   true 3.0 270 32 out of memory 32    15000 410   disqualified 2.4 71 33 true .20 17 2.1 true 8.0 370 59 true 7.9 370 62 true 6.9 330 59 timeout 900   160 12000
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true .11  24 .80 error (42) 880     960   4500    out of memory 120     15000   1700    true 2.9 260 30 unknown .78 66 9.1 unknown .025 4.6 .27 unknown .027 4.7 .23  timeout 900     870 9800    timeout 900    4000 8300   true 2.9 270 27 out of memory 32    15000 440   disqualified 2.4 72 28 true .22 17 2.1 true 7.3 340 55 true 8.1 370 65 true 8.8 370 68 timeout 900   150 11000
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true .10  24 .83 error (42) 880     1300   5000    out of memory 120     15000   1600    true 3.1 270 27 unknown .80 65 7.5 unknown .030 4.6 .15 unknown .045 4.6 .15  timeout 900     780 8500    timeout 900    4400 8400   true 3.1 270 25 out of memory 31    15000 410   disqualified 2.4 72 28 true .19 16 2.3 true 7.3 330 59 true 8.0 360 51 true 7.6 370 59 timeout 900   150 12000
bitvector/jain_5_true-unreach-call_true-no-overflow.i true .094 24 .91 out of memory 250     15000   2900    out of memory 190     15000   2800    true 3.0 270 26 unknown .80 65 7.3 unknown .066 4.7 .16 unknown .029 4.6 .20  timeout 900     13000 11000    timeout 900    74 8600   true 2.9 270 26 out of memory 600    15000 7700   disqualified 2.4 75 32 true .18 16 3.1 true 7.3 330 54 true 7.5 370 56 true 7.1 330 65 timeout 900   160 11000
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true .099 23 .82 error (42) 880     1300   3800    out of memory 130     15000   1800    true 3.0 270 26 unknown .81 67 9.8 unknown .029 4.6 .20 unknown .036 4.6 .23  timeout 900     800 10000    timeout 900    4200 9800   true 3.0 270 26 out of memory 32    15000 420   disqualified 2.4 72 31 true .18 15 2.2 true 7.4 350 62 true 7.8 360 59 true 7.1 330 57 timeout 900   150 11000
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true .10  24 .82 error (42) 880     1300   4300    out of memory 130     15000   1600    true 2.9 270 26 unknown .81 67 9.6 unknown .033 4.7 .25 unknown .033 4.6 .27  timeout 900     1200 9500    timeout 900    5400 11000   true 2.9 270 26 out of memory 39    15000 500   disqualified 2.4 72 29 true .21 16 2.1 true 8.3 360 58 true 8.2 350 60 true 7.4 330 54 timeout 900   150 13000
bitvector/modulus_true-unreach-call_true-no-overflow.i true .11  24 .99 true 45     1100   430    error (42) 880     12000   8800    true 3.2 270 26 unknown 1.3  66 16   unknown .056 4.8 .27 unknown .043 4.6 .15  true 76     280 960    timeout 900    4300 11000   true 3.1 270 30 out of memory 59    15000 970   disqualified 2.6 82 34 timeout (verification) 900    140 9900   error 7.7 360 66 error 8.2 360 54 error 7.3 340 57 timeout 900   200 9900
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .13  24 .73 true .099 6.7 .67 true .10  6.4 .77 true 3.1 270 26 unknown .80 67 9.3 unknown .029 4.6 .21 unknown .023 4.6 .22  true .12  26 .93 timeout 900    84 9600   true 3.1 270 31 true .40 58 2.4 disqualified 8.1 130 110 true .18 17 2.2 error 7.9 360 61 error 7.8 360 61 error 7.7 360 54 timeout 900   150 11000
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .13  23 .74 true .11  6.8 .78 true 1.4   71   22    true 3.2 270 32 unknown .78 66 9.1 unknown .034 4.6 .21 unknown .032 4.6 .22  true .13  26 1.6  timeout 900    2100 9400   true 3.2 270 29 true .96 61 13   disqualified 9.4 140 130 true 3.6  19 45   error 6.9 340 58 error 7.6 360 61 error 7.3 340 57 timeout 900   150 13000
bitvector/parity_true-unreach-call_true-no-overflow.i true .11  24 .81 true .22  7.2 2.2  witness invalid (true) .41  8.1 5.4  true 3.1 270 26 unknown .81 67 9.8 unknown .030 4.5 .20 unknown .036 4.6 .23  true .76  26 8.7  timeout 900    2100 10000   true 3.1 270 29 true 2.6  93 32   disqualified 2.5 74 30 true .19 17 2.2 true 7.7 330 50 true 7.8 360 54 true 7.9 370 66 timeout 900   160 12000
bitvector/sum02_false-unreach-call_true-no-overflow.i true .13  23 .67 error (42) 880     5200   3400    error (42) 880     250   6400    true 2.9 270 29 unknown .82 66 8.6 unknown .030 4.6 .22 unknown .028 4.6 .19  timeout 900     1600 10000    timeout 900    75 9000   true 3.0 270 27 timeout 900    510 5400   disqualified 2.5 71 33 true .21 16 3.1 true 7.8 360 68 true 7.8 360 54 true 7.2 330 59 timeout 900   200 10000
bitvector/sum02_true-unreach-call_true-no-overflow.i true .10  24 .99 error (42) 880     5300   3700    error (42) 870     260   8800    true 3.0 270 28 unknown .82 67 7.7 unknown .029 4.6 .20 unknown .029 4.7 .23  timeout 900     1600 10000    timeout 900    75 10000   true 2.9 270 26 timeout 900    490 6100   disqualified 2.4 72 36 true .21 16 2.0 true 7.7 370 60 true 7.7 350 63 true 7.6 340 56 timeout 900   150 11000
psyco/psyco_abp_1_false-no-overflow.c timeout 900     7000 8200    error (42) 880     1600   6000    out of memory 840     15000   9300    timeout 910   8000 11000 unknown 900    640 13000   unknown .036 4.7 .20 unknown .034 4.6 .21  timeout 900     3700 11000    timeout 900    4300 6700   timeout 910   8200 12000 out of memory 62    15000 810   disqualified 880   970 5800 timeout (verification) 900    2700 7200   timeout 900   5800 13000 timeout 900   5800 10000 timeout 900   5400 12000 error (1) 4.7 200 39
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
total 359 27000 54000 290000 359 130000 620000 920000 359 120000 1100000 1600000 359 57000 410000 710000 359 25000   510000 330000 359 13 1700 70 359 13 1700 73 359 140000     520000 1600000    359 220000 430000 2400000 359 57000 400000 700000 359 97000   1200000 690000 359 110000 96000 1300000 359 110000 270000 1300000 359 45000 300000 530000 359 71000 320000 720000 359 46000 340000 560000 359 180000 61000 2300000
    correct results 227 96 7100 980 200 56 2400 530 178 140 6400 1700 283 2100 81000 19000 17 3.4 570 38 0 0 198 68     5300 840    21 2300 58000 26000 283 2100 81000 20000 191 160   14000 1700 0 230 260 4200 3300 306 3400 130000 30000 279 3400 110000 28000 302 3400 130000 31000 148 5300 24000 67000
        correct true 87 77 3700 820 31 15 530 180 19 18 400 250 119 1400 35000 13000 0 0 0 30 30     820 390    7 1400 36000 16000 119 1400 35000 13000 29 30   3200 350 0 59 210 1000 2600 143 2100 70000 19000 116 1500 51000 13000 139 2100 72000 20000 0
        correct false 140 19 3400 160 169 40 1900 350 159 120 6000 1400 164 730 46000 6300 17 3.4 570 38 0 0 168 38     4400 440    14 890 23000 10000 164 730 46000 6500 162 130   11000 1400 0 171 54 3200 660 163 1300 59000 10000 163 1900 62000 15000 163 1300 60000 11000 148 5300 24000 67000
    correct-unconfimed results 5 11 440 140 6 53 1300 540 3 27 160 330 11 62 3500 600 150 44   5100 570 0 0 6 160     560 2100    112 13000 89000 170000 11 59 3400 580 3 6.2 740 83 0 3 27 190 260 0 1 220 1500 2800 0 0
        correct-unconfirmed true 5 11 440 140 6 53 1300 540 3 27 160 330 11 62 3500 600 0 0 0 5 160     530 2100    0 11 59 3400 580 3 6.2 740 83 0 3 27 190 260 0 1 220 1500 2800 0 0
        correct-unconfirmed false 0 0 0 0 150 44   5100 570 0 0 1 .091 26 .78 112 13000 89000 170000 0 0 0 0 0 0 0 0
    incorrect results 0 0 0 0 0 0 0 0 1 45 140 530 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 1 45 140 530 0 0 0 0 0 0 0 0
Run set 2ls.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] cbmc.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] cbmc-path.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] cpa-seq.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] depthk.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] divine-explicit.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] divine-smt.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] esbmc-kind.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] map2check.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] pesco.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] pinaka.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] smack.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] symbiotic.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] uautomizer.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] ukojak.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] utaipan.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other] verifuzz.[sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other]