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