Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-01 10:20:37 CET 2017-12-01 11:16:27 CET 2017-12-01 08:43:54 CET 2017-12-01 08:51:01 CET 2017-12-01 10:49:29 CET 2017-12-01 13:07:37 CET 2017-12-02 06:23:16 CET 2017-12-02 18:23:42 CET 2017-12-02 00:52:46 CET 2017-12-03 04:09:48 CET 2017-12-03 11:17:40 CET 2017-12-03 08:43:49 CET
Run set 2ls.sv-comp18.NoOverflows-BitVectors cbmc.sv-comp18.NoOverflows-BitVectors cpa-bam-bnb.sv-comp18.NoOverflows-BitVectors cpa-bam-slicing.sv-comp18.NoOverflows-BitVectors cpa-seq.sv-comp18.NoOverflows-BitVectors depthk.sv-comp18.NoOverflows-BitVectors esbmc-incr.sv-comp18.NoOverflows-BitVectors esbmc-kind.sv-comp18.NoOverflows-BitVectors map2check.sv-comp18.NoOverflows-BitVectors symbiotic.sv-comp18.NoOverflows-BitVectors uautomizer.sv-comp18.NoOverflows-BitVectors ukojak.sv-comp18.NoOverflows-BitVectors utaipan.sv-comp18.NoOverflows-BitVectors
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i .13  24 .86 1 .25 34 2.5 1 .48 41 3.9 0 .43 40 4.6 0 3.4 300 29 1 4.1  410 30   0 .12  28 .72 1 .11  28 .83 1 .32  11 3.7  1 .17  11 1.8  1 4.1 240 32 1 4.3 240 36 1 4.1 240 34 1
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i .14  24 .95 1 .26 34 2.5 1 .47 40 4.6 0 .44 40 4.1 0 3.5 280 32 1 3.8  420 33   0 .082 28 .93 1 .092 28 .97 1 .32  12 3.8  0 .17  11 1.5  1 4.8 260 40 1 4.4 260 38 1 4.7 270 41 1
signedintegeroverflow-regression/Division_false-no-overflow.c.i .10  24 1.0  1 .27 34 2.1 1 .47 41 4.4 0 .48 40 5.0 0 3.6 280 32 1 4.2  420 27   0 .082 28 .98 1 .079 28 1.1  1 .30  12 4.2  0 .16  11 1.7  1 4.1 240 38 1 4.4 250 35 1 4.1 240 34 1
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i .14  24 .85 1 .25 34 2.5 1 .45 41 4.4 0 .45 40 4.4 0 3.4 280 27 1 3.9  420 39   0 .097 28 .70 1 .11  28 .82 1 .31  11 2.7  1 .16  11 1.7  1 4.2 240 37 1 4.2 250 37 1 4.3 240 37 1
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i .10  24 .89 1 .25 34 2.4 1 .45 40 4.1 0 .43 40 3.8 0 3.4 280 34 1 4.2  420 29   0 .12  28 .81 1 .081 28 1.0  1 .30  11 3.5  1 .17  11 1.5  1 4.1 230 32 1 4.1 240 35 1 4.0 240 35 1
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i .12  24 .93 1 .26 34 2.1 1 .48 43 4.7 0 .44 41 3.9 0 3.5 280 31 1 4.0  410 32   0 .092 28 1.1  1 .083 28 .90 1 .32  11 3.4  0 .14  11 1.9  1 4.7 270 44 1 4.5 270 35 1 4.4 270 39 1
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i .10  24 1.3  1 .24 34 2.3 1 .46 41 4.5 0 .47 40 4.1 0 3.4 280 29 1 3.9  420 30   0 .11  28 .77 1 .11  28 .76 1 .32  12 3.2  0 .14  11 1.7  1 4.2 240 39 1 4.2 250 38 1 4.0 240 35 1
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i .13  24 .81 1 .24 34 2.0 1 .50 41 4.0 0 .46 40 4.3 0 3.7 280 32 1 4.1  420 30   0 .11  28 .77 1 .10  28 .97 1 .29  11 4.2  0 .15  11 1.7  1 4.5 270 38 1 4.4 250 34 1 4.4 260 34 1
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i .13  24 .92 1 .26 34 2.2 1 .46 40 4.5 0 .46 40 4.0 0 3.4 270 31 1 4.0  420 31   0 .083 28 .88 1 .12  28 .58 1 .30  12 4.0  0 .14  11 1.8  1 4.1 250 36 1 4.2 240 37 1 4.1 240 33 1
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i .14  24 .77 1 .27 34 2.2 1 .48 40 3.9 0 .45 41 4.6 0 3.5 280 31 1 4.0  420 32   0 .080 28 1.0  1 .082 28 .83 1 .32  11 3.5  0 .17  11 1.7  1 4.1 240 35 1 4.6 240 42 1 4.1 250 38 1
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i .12  24 .80 2 .44 34 5.1 2 .47 40 4.1 0 .41 40 4.0 0 3.0 270 24 2 1.3  48 15   0 .072 26 .92 2 .081 26 .77 2 .32  11 3.6  2 .15  11 1.4  2 4.0 240 34 2 4.0 240 35 2 4.3 240 33 2
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i .13  24 .80 2 .47 34 4.4 2 .51 43 3.8 0 .44 40 4.2 0 3.1 270 30 2 1.6  49 20   0 .088 27 .89 2 .089 27 .77 2 .30  11 4.5  2 .16  11 1.4  2 4.6 290 38 2 4.4 260 36 2 4.7 280 42 2
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i .11  24 .79 2 .44 34 4.1 2 .48 41 4.6 0 .45 40 4.1 0 3.1 280 28 2 1.7  48 21   0 .072 26 .96 2 .080 27 .76 2 .32  11 3.7  2 .15  11 1.3  2 4.0 230 34 2 3.9 240 31 2 4.3 250 34 2
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i .11  24 .91 2 .47 34 4.3 2 .46 40 4.4 0 .44 40 4.0 0 3.0 280 24 2 480    420 5400   -16 .079 26 .90 2 .088 26 .72 2 .29  11 3.9  2 .15  11 1.6  2 4.1 240 35 2 4.0 230 31 2 4.2 240 32 2
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i .11  24 .78 2 .46 34 4.3 2 .47 41 4.4 0 .47 41 4.0 0 2.9 270 29 2 480    110 6200   0 .073 26 1.0  2 .075 26 .84 2 .29  12 4.5  2 .15  11 1.5  2 4.4 240 34 2 4.0 240 36 2 4.1 240 31 2
termination-crafted/2Nested_false-no-overflow.c .11  22 .77 1 .24 33 2.0 1 .48 41 4.0 0 .44 40 4.7 0 2.6 270 26 1 .53 75 6.6 0 .15  28 2.1  1 .21  28 1.6  1 .69  12 8.0  1 .19  12 1.9  1 6.1 340 49 1 4.1 250 35 1 4.2 240 36 1
termination-crafted/4NestedWith3Variables_false-no-overflow.c .15  24 .98 1 .28 36 2.6 1 .50 40 4.5 0 .46 41 4.9 0 2.6 270 24 1 .60 75 6.7 0 .36  28 2.9  1 .41  28 4.0  1 1.1   13 13    1 .18  12 1.6  1 4.1 250 38 1 4.3 250 37 1 4.3 250 37 1
termination-crafted/Ackermann_false-no-overflow.c .098 22 .71 0 .25 33 2.5 1 .49 40 4.2 0 .46 40 5.0 0 900   3800 11000 0 .61 49 7.3 0 .16  28 1.6  1 .20  28 1.7  1 .50  12 5.7  1 .17  12 1.9  1 4.0 240 38 1 4.3 250 38 1 4.2 250 35 1
termination-crafted/Bangalore_false-no-overflow.c .14  22 .92 1 .24 33 2.8 1 .47 40 4.4 0 .45 40 3.9 0 2.6 270 26 1 .55 75 6.7 0 .15  28 1.9  1 .19  28 2.4  1 .60  13 7.4  1 .18  12 1.8  1 4.0 240 37 1 4.2 240 38 1 4.3 250 38 1
termination-crafted/Bangalore_v3_false-no-overflow.c .11  22 .95 1 .24 33 2.3 1 .47 40 4.5 0 .43 40 3.8 0 2.6 270 24 1 .54 75 6.0 0 .19  28 1.8  1 .17  28 2.2  1 .75  13 9.3  1 .18  12 2.7  1 4.2 240 36 1 4.0 240 35 1 4.1 240 32 1
termination-crafted/Benghazi_nondet_false-no-overflow.c .13  23 .87 1 .27 33 2.2 1 .47 41 4.4 0 .48 41 4.2 0 2.7 280 27 1 .56 75 6.9 0 .23  28 2.0  1 .24  28 3.2  1 .68  12 9.7  1 .16  12 1.9  1 4.0 230 36 1 4.2 250 37 1 4.6 250 34 1
termination-crafted/Binary_Search_false-no-overflow.c .10  22 .65 0 .28 34 2.6 1 .50 40 4.3 0 .46 40 3.8 0 2.9 290 25 1 .40 48 5.0 0 .22  28 2.1  1 .35  28 3.3  1 .58  12 6.8  1 .17  12 2.1  1 4.2 250 34 1 4.3 260 38 1 4.1 240 34 1
termination-crafted/Cairo_nondet_false-no-overflow.c .13  23 .98 1 .26 33 2.1 1 .47 40 4.2 0 .45 40 4.1 0 2.7 270 22 1 .85 75 12   0 .17  28 1.8  1 .18  28 1.5  1 .67  12 8.9  1 .17  12 2.1  1 4.4 280 36 1 5.3 290 40 1 4.6 290 35 1
termination-crafted/Cairo_step2_false-no-overflow.c 900     1300 11000    0 870    5100 5000   0 .49 41 4.4 0 .45 38 4.0 0 900   2600 13000 0 77    75 1000   0 900     390 10000    0 900     390 11000    0 900     1100 11000    0 900     170 13000    0 900   4400 14000 0 900   5200 12000 0 900   2400 13000 0
termination-crafted/Collatz_unknown-termination_false-no-overflow.c .11  23 .98 1 .26 33 2.3 1 .43 41 4.8 0 .44 41 4.1 0 2.8 280 28 1 21    75 260   0 .14  28 1.4  1 .24  28 2.3  1 .43  12 5.1  1 .17  12 2.0  1 5.0 290 40 1 4.2 250 36 1 5.2 290 41 1
termination-crafted/Copenhagen_disj_false-no-overflow.c .13  23 .75 1 .27 33 2.0 1 .46 40 4.5 0 .48 40 4.7 0 2.7 270 24 1 .40 75 4.7 0 .22  28 1.9  1 .24  28 1.9  1 .49  12 5.7  1 .18  12 1.6  1 4.4 270 36 1 4.3 250 37 1 4.5 280 35 1
termination-crafted/Gothenburg_false-no-overflow.c .13  25 1.2  1 .26 35 2.0 1 .49 41 4.2 0 .45 38 3.9 0 2.7 270 24 1 .61 75 7.4 0 .32  28 2.6  1 .42  28 3.4  1 3.6   14 43    1 .19  12 1.7  1 4.2 250 37 1 4.2 250 33 1 4.2 250 36 1
termination-crafted/Gothenburg_v2_false-no-overflow.c .13  25 .97 1 .29 33 2.4 1 .47 41 4.6 0 .44 40 4.0 0 2.7 270 22 1 .57 75 7.7 0 .32  28 3.1  1 .37  28 4.0  1 .41  12 4.5  1 .18  12 1.6  1 4.3 250 38 1 4.4 250 33 1 4.1 250 34 1
termination-crafted/Hanoi_2vars_false-no-overflow.c .12  22 1.0  1 .26 33 2.0 1 .50 41 4.2 0 .46 40 4.0 0 2.6 270 24 1 .53 75 6.4 0 .18  28 1.7  1 .20  28 1.8  1 26     15000 390    0 .16  12 1.9  1 4.0 240 35 1 4.1 250 35 1 4.0 240 35 1
termination-crafted/Hanoi_3vars_false-no-overflow.c .11  23 .80 1 .23 33 2.2 1 .48 40 4.1 0 .44 39 4.4 0 2.7 270 22 1 .54 75 6.9 0 .23  28 2.1  1 .41  28 3.9  1 .68  13 8.4  1 .18  12 1.8  1 4.2 240 36 1 4.3 250 38 1 4.2 250 33 1
termination-crafted/Hanoi_plus_false-no-overflow.c .13  23 .86 1 .25 33 2.3 1 .46 40 3.8 0 .45 40 4.0 0 2.7 270 25 1 .55 75 6.0 0 .32  28 2.4  1 .24  28 3.3  1 .99  13 12    1 .18  12 1.7  1 4.3 230 39 1 4.3 250 41 1 4.3 240 32 1
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c .12  22 .86 1 .25 33 2.1 1 .49 43 4.7 0 .43 40 3.4 0 2.5 270 24 1 .37 75 4.3 0 .17  28 1.7  1 .15  28 1.9  1 .42  12 5.6  1 .18  12 1.7  1 4.4 270 35 1 6.9 370 51 1 4.7 280 38 1
termination-crafted/Mysore_false-no-overflow.c .12  23 .81 1 .24 33 2.3 1 .48 42 4.3 0 .47 40 4.1 0 2.7 270 23 1 .56 75 6.6 0 .24  28 1.6  1 .23  28 2.4  1 .83  12 10    1 .16  12 2.1  1 6.3 340 47 1 4.2 250 39 1 4.0 240 37 1
termination-crafted/NestedRecursion_1a_false-no-overflow.c .12  22 .68 0 .25 33 2.6 1 .48 40 4.8 0 .45 40 4.2 0 2.7 270 26 1 .57 49 6.5 0 .13  28 1.3  1 .18  28 1.9  1 .35  12 4.3  1 .16  12 1.8  1 4.2 250 35 1 4.4 250 39 1 4.2 250 33 1
termination-crafted/NestedRecursion_2a_false-no-overflow.c .12  22 .75 0 .24 33 2.1 1 .49 43 4.6 0 .43 40 4.4 0 2.7 270 26 1 .52 48 5.6 0 .12  28 1.5  1 .14  28 1.2  1 .38  11 3.4  1 .15  12 2.1  1 4.5 280 44 1 4.3 250 36 1 4.7 280 38 1
termination-crafted/NonTermination1_false-no-overflow.c .12  23 .87 1 .27 33 2.1 1 .50 43 4.5 0 .45 38 4.1 0 2.7 280 24 1 .55 75 6.2 0 .13  28 1.4  1 .15  28 1.1  1 .39  12 4.8  1 .18  12 1.8  1 3.9 240 34 1 4.2 240 38 1 4.1 250 37 1
termination-crafted/NonTermination2_false-no-overflow.c .14  23 .86 1 .24 33 2.2 1 .52 43 4.4 0 .46 40 4.3 0 3.0 280 27 1 .38 75 4.3 0 .13  28 1.1  1 .26  28 1.7  1 .48  12 5.3  1 .16  12 1.9  1 4.1 240 37 1 4.1 250 38 1 6.8 350 44 1
termination-crafted/NonTermination4_false-no-overflow.c .53  41 5.7  1 1.8  35 20   1 .50 43 4.5 0 .45 40 4.4 0 190   1300 1500 1 12    75 140   0 .12  28 1.2  1 .12  28 1.2  1 .30  11 3.8  0 .16  11 2.0  1 23   780 200 1 350   4900 4900 1 250   2200 2700 1
termination-crafted/NonTerminationSimple2_false-no-overflow.c .14  22 .77 1 .23 33 2.5 1 .45 40 4.0 0 .45 40 4.5 0 2.8 270 23 1 .55 75 5.6 0 .13  28 1.3  1 .16  28 1.2  1 .41  12 5.5  1 .15  11 1.7  1 4.0 230 36 1 4.3 240 34 1 4.2 240 33 1
termination-crafted/NonTerminationSimple3_false-no-overflow.c .099 23 1.0  1 .27 33 2.0 1 .47 40 4.7 0 .47 40 3.7 0 2.7 270 21 1 .55 75 6.4 0 .16  28 1.8  1 .22  28 2.1  1 .58  13 8.0  1 .15  12 1.7  1 4.2 240 38 1 4.0 240 35 1 4.0 240 37 1
termination-crafted/NonTerminationSimple4_false-no-overflow.c 900     1200 13000    0 880    5100 4300   0 .49 41 4.0 0 .45 40 3.8 0 900   2200 12000 0 76    75 950   0 900     400 12000    0 900     390 12000    0 900     83 4200    0 .099 11 1.2  0 900   3900 15000 0 900   5200 13000 0 900   2500 15000 0
termination-crafted/NonTerminationSimple5_false-no-overflow.c .13  22 .82 1 .25 33 2.1 1 .50 41 4.1 0 .44 40 4.2 0 2.7 270 23 1 .55 75 6.3 0 .13  28 1.1  1 .12  28 1.5  1 .42  12 4.8  1 .17  11 1.7  1 4.5 280 37 1 4.3 250 37 1 4.6 290 37 1
termination-crafted/NonTerminationSimple6_false-no-overflow.c .14  22 .91 1 .23 33 1.9 1 .48 41 5.2 0 .41 38 3.8 0 2.6 270 23 1 .54 75 6.5 0 .13  28 1.6  1 .20  28 1.6  1 26     15000 370    0 .18  12 1.9  1 4.0 240 36 1 4.1 240 36 1 4.1 230 36 1
termination-crafted/NonTerminationSimple8_false-no-overflow.c .13  22 1.1  1 .28 33 2.0 1 .52 43 4.8 0 .45 41 4.4 0 2.7 280 26 1 .57 75 7.2 0 .15  28 1.2  1 .16  28 1.7  1 .44  12 5.3  1 .18  11 1.7  1 6.1 330 45 1 4.1 250 39 1 4.0 250 39 1
termination-crafted/NonTerminationSimple9_false-no-overflow.c .14  22 .80 1 .23 33 2.4 1 .51 40 3.8 0 .47 41 3.9 0 2.7 280 26 1 .53 75 7.7 0 .12  28 1.3  1 .13  28 1.3  1 26     15000 360    0 .18  12 1.8  1 4.3 240 36 1 4.1 240 36 1 4.2 250 35 1
termination-crafted/Pure2Phase_false-no-overflow.c .13  22 .87 1 .26 33 2.0 1 .50 41 4.3 0 .41 40 4.3 0 2.6 270 23 1 .55 75 6.0 0 .19  28 1.9  1 .27  28 2.1  1 .43  12 5.5  1 .19  12 1.4  1 4.7 280 36 1 4.5 250 39 1 4.8 280 37 1
termination-crafted/Pure3Phase_false-no-overflow.c .14  23 .85 1 .25 35 2.4 1 .45 41 4.2 0 .50 40 4.5 0 2.7 270 25 1 .58 75 6.6 0 .26  28 2.2  1 .27  28 2.8  1 1.6   13 22    1 .16  12 2.6  1 4.2 240 33 1 4.5 250 34 1 4.2 250 33 1
termination-crafted/RecursiveMultiplication_false-no-overflow.c .10  22 .65 0 .25 33 2.2 0 .48 40 4.8 0 .46 40 4.3 0 3.5 300 30 1 .57 49 7.7 0 .16  28 1.7  1 .19  28 1.9  1 .80  12 12    0 .17  12 1.9  1 4.4 250 34 1 4.2 250 38 1 4.3 250 38 1
termination-crafted/RecursiveNonterminating_false-no-overflow.c .12  22 .71 0 .27 33 2.2 1 .49 41 4.2 0 .41 40 3.4 0 2.6 270 21 1 .56 49 7.0 0 .13  28 1.6  1 .11  28 1.5  1 .33  11 3.6  1 .16  14 1.8  1 4.3 240 34 1 4.0 250 32 1 4.0 250 37 1
termination-crafted/Rotation180_false-no-overflow.c .11  24 .68 1 .26 33 2.1 1 .48 42 4.1 0 .46 40 4.1 0 2.6 260 23 1 .36 75 4.1 0 .12  28 1.2  1 .21  28 2.2  1 890     11 14000    0 .18  12 1.7  1 4.1 240 34 1 4.2 250 36 1 4.0 240 33 1
termination-crafted/Singapore_false-no-overflow.c .12  23 .81 1 .25 33 2.1 1 .52 44 4.6 0 .42 40 4.3 0 2.6 270 22 1 .56 75 6.7 0 .17  28 2.5  1 .21  28 1.9  1 .60  13 7.8  1 .19  12 1.8  1 4.0 240 36 1 4.3 250 34 1 4.4 240 36 1
termination-crafted/Singapore_plus_false-no-overflow.c .11  23 1.0  1 .28 35 2.1 1 .46 42 4.9 0 .44 40 4.2 0 2.8 270 23 1 .56 75 6.5 0 .20  28 2.0  1 .29  28 2.9  1 .64  12 7.6  1 .19  12 1.8  1 4.1 240 34 1 4.4 250 38 1 4.2 240 32 1
termination-crafted/Singapore_v1_false-no-overflow.c .12  23 1.0  1 .27 33 2.3 1 .47 40 4.8 0 .44 40 4.1 0 2.5 260 23 1 .54 75 8.1 0 .19  28 2.0  1 .20  28 1.9  1 .68  12 8.4  1 .17  12 2.1  1 4.2 240 35 1 4.3 250 36 1 4.2 240 38 1
termination-crafted/Singapore_v2_false-no-overflow.c .12  23 .83 1 .27 33 2.2 1 .46 43 4.3 0 .43 40 4.6 0 2.6 270 26 1 .55 75 7.0 0 .17  28 1.9  1 .21  28 1.9  1 .69  12 8.1  1 .16  12 1.9  1 4.1 240 36 1 4.2 250 34 1 4.3 250 35 1
termination-crafted/Stockholm_false-no-overflow.c .12  23 .89 1 .24 33 2.0 1 .44 40 4.6 0 .47 40 4.0 0 2.7 270 22 1 .57 75 7.5 0 .29  28 2.2  1 .32  28 2.5  1 1.8   13 22    1 .18  12 1.7  1 4.3 240 39 1 4.2 250 41 1 4.4 250 35 1
termination-crafted/Thun_false-no-overflow.c .13  23 .76 1 .27 33 2.0 1 .47 43 4.5 0 .44 40 3.9 0 2.7 270 23 1 .54 75 6.2 0 .18  28 1.6  1 .27  28 2.4  1 1.1   13 16    1 .18  12 1.7  1 4.0 240 33 1 4.3 250 33 1 4.0 250 33 1
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c .12  23 1.1  1 .27 33 2.1 1 .49 40 4.7 0 .42 40 4.3 0 2.7 270 22 1 .57 75 6.9 0 .17  28 1.5  1 .28  28 1.8  1 .95  12 13    1 .16  12 1.8  1 4.9 280 41 1 4.5 250 41 1 4.8 290 38 1
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c .12  24 1.1  1 .27 33 2.5 1 .48 43 4.9 0 .46 40 4.0 0 3.1 280 28 1 .62 77 7.9 0 .55  28 4.4  1 .57  28 5.7  1 1.4   12 19    0 .20  12 1.9  1 13   660 120 1 12   540 120 1 13   610 100 1
termination-crafted/aaron2_false-no-overflow.c .14  25 .85 1 .24 35 2.5 1 .50 41 4.7 0 .43 40 3.9 0 2.7 280 28 1 .41 75 4.6 0 .25  28 2.3  1 .34  28 3.3  1 .93  13 12    1 .16  12 2.3  1 4.7 280 43 1 4.1 250 36 1 4.6 280 38 1
termination-crafted/aaron3_false-no-overflow.c .14  23 .76 1 .26 33 2.2 1 .47 41 4.1 0 .48 40 4.6 0 2.7 270 23 1 .39 75 4.6 0 .26  28 2.5  1 .33  28 2.9  1 .79  13 10    1 .19  12 2.4  1 6.0 320 40 1 4.2 250 39 1 4.3 250 40 1
termination-crafted/easy2_false-no-overflow.c 900     1700 12000    0 870    2200 3100   0 .48 42 4.2 0 .43 40 4.3 0 900   13000 10000 0 160    390 2300   0 900     890 11000    0 900     880 11000    0 900     300 11000    0 900     210 13000    0 900   5300 14000 0 900   7000 13000 0 900   5300 13000 0
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c .19  24 1.4  2 2.2  34 28   2 .50 40 4.4 0 .44 40 3.9 0 2.6 270 24 2 1.2  76 14   0 .087 26 .89 2 .074 26 .79 2 .34  11 3.5  2 .13  11 1.5  2 7.3 360 56 2 4.6 260 42 2 4.5 260 36 2
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c 5.9   200 66    2 870    3000 3200   0 .49 41 4.3 0 .43 40 4.1 0 2.9 270 25 2 60    100 790   0 900     1600 11000    0 .12  26 .57 2 890     100 12000    0 900     250 11000    0 30   940 320 2 900   5200 14000 0 900   1500 11000 0
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c 3.0   100 31    2 870    3900 4200   0 .48 41 4.8 0 .42 40 4.2 0 2.7 270 24 2 1.3  75 14   0 900     1500 14000    0 .072 26 .78 2 900     32 11000    0 900     70 11000    0 4.6 280 36 2 4.5 260 42 2 4.8 280 40 2
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c 3.3   170 37    2 870    3800 3000   0 .47 43 4.3 0 .46 40 4.1 0 900   6200 11000 0 1.4  100 18   0 900     1100 11000    0 .089 26 .78 2 3.0   140 33    0 900     180 12000    0 5.7 300 51 2 7.0 470 63 2 6.8 330 60 2
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c .10  22 .73 2 870    5300 4700   0 .47 41 4.4 0 .47 40 4.2 0 2.7 270 25 2 7.6  75 92   0 900     130 10000    0 .10  26 .85 2 900     60 10000    0 900     52 12000    0 5.2 300 44 2 7.0 460 58 2 5.5 290 49 2
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c .087 23 .86 2 870    5500 5800   0 .47 40 3.7 0 .45 38 3.6 0 2.7 270 28 2 7.2  75 89   0 900     190 12000    0 .089 26 1.1  2 900     58 12000    0 900     55 14000    0 5.3 300 42 2 6.2 420 59 2 5.5 300 42 2
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c .17  24 1.2  2 .45 33 3.8 2 .48 40 4.5 0 .45 40 4.8 0 2.6 270 25 2 1.5  75 15   0 .12  26 1.2  2 .096 26 .95 2 .49  12 5.2  2 .20  12 2.0  2 5.0 300 43 2 5.3 290 40 2 5.8 300 50 2
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c 900     310 8400    0 870    2200 3200   0 .49 41 4.3 0 .44 40 3.8 0 900   4900 11000 0 380    560 4700   0 900     1300 9700    0 900     1300 11000    0 900     930 12000    0 900     100 13000    0 17   720 150 2 900   5700 12000 0 24   800 220 2
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c .12  22 .68 2 870    8400 3400   0 .47 41 4.1 0 .45 41 4.0 0 2.6 270 21 2 1.2  75 18   0 .056 15 .25 0 .033 15 .31 0 900     1200 11000    0 .080 11 .63 0 4.1 230 38 2 4.0 240 32 2 4.1 240 37 2
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c 900     1300 12000    0 870    4600 5900   0 .50 40 4.3 0 .47 41 4.4 0 900   2600 10000 0 68    75 850   0 900     440 11000    0 900     450 12000    0 900     1100 11000    0 900     270 13000    0 4.9 300 40 2 4.9 270 44 2 5.3 300 43 2
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c 900     1400 13000    0 870    4500 4000   0 .45 41 4.6 0 .44 40 4.5 0 2.8 270 23 2 1.4  75 20   0 900     400 9700    0 900     400 11000    0 900     1200 12000    0 900     170 11000    0 4.6 290 46 2 5.1 270 41 2 5.1 280 43 2
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c .11  23 .87 2 870    3200 4900   0 .48 41 4.6 0 .43 38 3.7 0 2.7 270 22 2 1.3  75 16   0 900     760 11000    0 .075 26 .77 2 900     1100 9900    0 900     230 13000    0 5.5 310 53 2 6.8 420 51 2 6.4 300 51 2
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c .11  23 .83 2 870    3900 3500   0 .51 43 4.3 0 .45 40 4.0 0 2.9 290 23 2 1.5  75 17   0 900     630 13000    0 .082 26 .86 2 900     26 12000    0 900     15 14000    0 4.7 290 39 2 5.8 310 45 2 7.6 390 50 2
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c 6.3   280 63    1 50    14000 600   0 .49 43 4.8 0 .46 40 3.8 0 2.7 270 25 1 38    100 500   0 750     15000 11000    0 .11  26 .96 1 900     1900 11000    0 300     2900 2500    0 900   4900 13000 0 900   5300 15000 0 900   1600 11000 0
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c .16  24 1.7  0 58    14000 730   0 .48 40 4.1 0 .44 40 4.2 0 900   6300 9900 0 120    160 1500   0 900     5900 11000    0 900     5900 11000    0 900     1900 12000    0 900     3800 7900    0 900   2000 11000 0 900   6200 11000 0 900   1300 12000 0
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c .13  22 .69 2 210    15000 2800   0 .45 41 3.9 0 .44 40 4.5 0 2.5 270 24 2 1.2  75 12   0 900     11000 9700    0 .082 26 .66 2 890     11 12000    0 .13  11 1.3  2 3.8 240 37 2 3.9 230 35 2 4.3 240 34 2
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c 900     1500 10000    0 870    1200 8200   0 .50 41 4.3 0 .45 40 3.8 0 900   600 12000 0 900    120 9700   0 900     150 12000    0 900     150 11000    0 900     110 13000    0 900     76 12000    0 900   5200 11000 0 900   5300 14000 0 900   3900 13000 0
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c .10  22 .64 0 870    2000 2900   0 .47 41 4.2 0 .42 40 4.4 0 2.9 280 27 2 510    15000 7100   0 900     6400 7300    0 900     9000 9500    0 900     140 11000    0 900     72 12000    0 6.3 310 53 2 6.6 400 52 2 6.4 310 51 2
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c 900     750 7700    0 870    3200 4100   0 .48 43 3.8 0 .46 40 4.0 0 2.9 270 25 2 1.4  75 16   0 900     1000 11000    0 900     1000 10000    0 900     940 12000    0 900     100 12000    0 9.8 540 79 2 18   670 170 2 7.2 320 55 2
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c .12  22 .69 0 870    310 3700   0 .46 41 4.8 0 .47 40 4.2 0 3.9 290 33 2 450    15000 6300   0 900     12000 6500    0 720     15000 7600    0 900     600 12000    0 900     92 12000    0 8.5 450 66 2 900   1200 14000 0 16   640 140 2
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c .12  22 .66 0 870    290 2400   0 .48 40 4.3 0 .44 40 4.8 0 4.0 290 40 2 440    15000 6000   0 900     12000 6200    0 670     15000 7800    0 900     260 11000    0 900     130 11000    0 19   790 170 2 900   1200 12000 0 44   1100 390 2
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c .12  22 .64 0 870    710 3800   0 .47 40 4.2 0 .45 40 4.6 0 900   1200 13000 0 440    15000 5900   0 900     4900 6300    0 900     4800 12000    0 900     460 12000    0 900     360 13000    0 12   560 93 2 900   1500 13000 0 23   670 180 2
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c .11  22 .67 0 870    480 3200   0 .45 40 4.0 0 .41 40 4.8 0 3.3 280 30 2 390    15000 4400   0 900     4900 6800    0 770     15000 6700    0 900     460 10000    0 900     290 14000    0 8.4 480 71 2 900   1600 14000 0 13   580 110 2
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c .10  22 .84 0 870    700 3600   0 .50 43 5.0 0 .41 40 3.7 0 900   1400 9800 0 440    15000 6000   0 900     4800 5200    0 680     15000 6600    0 900     490 13000    0 900     400 12000    0 12   530 99 2 900   1800 11000 0 15   610 110 2
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c .086 22 .64 0 870    810 6200   0 .49 43 4.2 0 .47 40 4.6 0 900   5100 9900 0 500    15000 5300   0 900     6100 6000    0 900     12000 7200    0 900     2400 9200    0 900     980 11000    0 11   550 83 2 900   2000 11000 0 9.5 520 76 2
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c .097 22 .64 0 870    4100 5400   0 .45 41 4.2 0 .44 40 4.3 0 900   4300 11000 0 500    15000 7300   0 890     15000 7700    0 900     12000 10000    0 900     1600 10000    0 900     270 10000    0 14   610 120 2 900   5000 12000 0 14   610 120 2
termination-crafted/NonTermination3_true-no-overflow_false-termination.c .11  23 .80 2 870    2700 5600   0 .46 41 4.2 0 .45 41 3.9 0 2.6 270 22 2 1.2  75 13   0 900     2100 11000    0 .079 26 .74 2 .41  12 5.0  2 .13  11 1.6  2 4.1 240 33 2 4.0 240 40 2 3.9 230 31 2
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c .12  22 .84 2 870    5300 4400   0 .52 40 4.4 0 .44 40 4.3 0 2.7 270 26 2 1.4  75 16   0 900     170 11000    0 .072 26 .89 2 890     11 12000    0 .16  11 1.6  2 5.3 300 45 2 6.4 380 52 2 5.8 300 46 2
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c .11  25 .81 2 870    2200 6500   0 .48 40 4.2 0 .44 41 3.9 0 2.7 270 23 2 1.4  75 17   0 900     380 12000    0 .10  26 .62 2 900     650 13000    0 900     4000 10000    0 4.9 280 44 2 6.3 390 55 2 6.8 360 60 2
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c .11  23 .83 2 870    2100 6800   0 .44 40 4.3 0 .44 40 4.8 0 2.6 270 24 2 1.3  75 17   0 900     400 9700    0 .076 26 .86 2 900     250 11000    0 900     250 12000    0 4.9 280 42 2 6.1 380 52 2 4.9 290 38 2
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c .14  23 .75 2 870    830 9100   0 .46 40 4.3 0 .45 40 3.8 0 2.7 270 26 2 1.2  75 16   0 900     220 12000    0 .12  26 1.1  2 900     140 11000    0 900     170 12000    0 5.0 290 41 2 6.0 340 50 2 4.9 300 44 2
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c .15  23 1.7  2 870    4500 4000   0 .46 40 4.3 0 .43 40 4.5 0 2.6 270 26 2 72    75 1000   0 900     720 11000    0 900     720 11000    0 900     460 11000    0 900     250 12000    0 5.5 300 46 2 5.8 320 50 2 5.0 280 41 2
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c .11  23 .72 2 870    1300 9500   0 .42 40 4.4 0 .45 40 4.1 0 2.7 260 23 2 1.3  75 15   0 900     410 14000    0 .12  26 .86 2 900     440 12000    0 900     330 11000    0 5.7 300 45 2 6.5 380 62 2 5.6 300 46 2
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c .10  22 .74 2 870    5100 4100   0 .49 43 4.2 0 .43 40 3.7 0 2.6 270 23 2 1.4  75 14   0 900     740 11000    0 .11  26 .72 2 900     260 11000    0 900     210 13000    0 4.8 290 38 2 5.1 260 47 2 4.7 280 36 2
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c .10  22 .84 2 .39 33 5.0 2 .47 41 4.5 0 .46 40 4.2 0 2.7 290 25 2 1.2  48 12   0 .069 26 .84 2 .093 26 .73 2 .29  11 3.5  2 .14  11 1.3  2 4.1 240 33 2 3.8 240 31 2 4.0 240 35 2
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c .10  22 .72 2 .41 33 4.3 1 .48 41 4.1 0 .44 40 3.6 0 2.6 270 24 2 1.2  75 13   0 290     15000 4400    0 .10  26 .68 2 890     11 12000    0 .13  11 1.4  2 4.1 240 37 2 3.8 230 33 2 4.2 240 31 2
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c .11  22 .92 2 4.2  61 55   2 .46 40 3.6 0 .46 40 4.4 0 2.7 270 22 2 1.4  75 17   0 .61  26 8.6  2 .11  26 .66 2 .38  11 4.3  2 .15  11 1.5  2 4.8 290 37 2 5.7 310 45 2 4.8 290 39 2
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c 900     1700 9900    0 870    2400 4200   0 .50 42 4.4 0 .43 41 4.0 0 900   13000 11000 0 120    240 1600   0 900     900 12000    0 900     890 10000    0 900     310 9900    0 900     180 12000    0 900   5300 13000 0 900   7100 11000 0 7.4 350 60 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c .15  23 .84 1 .27 33 1.9 1 .49 40 4.0 0 .44 41 4.0 0 2.8 270 24 1 .58 100 6.9 0 .29  28 2.3  1 .41  29 4.6  1 .41  12 6.0  1 .19  12 1.9  1 4.7 300 43 1 4.7 260 36 1 4.7 290 40 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c .13  26 1.1  1 .28 36 2.6 1 .43 40 3.6 0 .44 41 4.6 0 2.7 280 26 1 .60 130 6.5 0 .29  28 3.0  1 .56  30 6.8  1 .43  12 6.0  1 .19  12 1.9  1 5.1 280 46 1 4.9 260 42 1 5.1 290 38 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c .11  23 .93 1 .25 33 2.1 1 .48 40 4.3 0 .44 41 4.1 0 2.6 270 24 1 .40 75 4.7 0 .24  28 2.8  1 .26  28 3.2  1 .92  13 13    1 .20  12 1.8  1 4.6 280 38 1 4.3 250 42 1 4.8 280 40 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c .14  23 .88 1 .24 33 2.5 1 .48 42 4.6 0 .42 41 4.2 0 2.8 270 24 1 .39 75 4.4 0 .27  28 2.9  1 .35  28 2.8  1 .82  13 10    0 .22  12 2.4  1 4.4 240 36 1 4.3 250 37 1 4.4 250 36 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c .13  23 .98 1 .29 33 2.6 1 .48 41 4.0 0 .46 40 3.7 0 2.6 270 21 1 .63 100 6.9 0 .23  28 1.8  1 .38  28 3.7  1 .68  13 7.9  1 .21  12 2.0  1 5.9 300 49 1 6.2 380 59 1 6.3 290 47 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c .14  25 .96 1 .28 33 2.3 1 .48 41 4.8 0 .45 42 4.6 0 2.8 270 26 1 .38 75 4.8 0 .25  28 2.2  1 .38  28 2.9  1 .72  12 7.8  1 .17  12 2.1  1 4.0 240 37 1 4.6 250 44 1 4.3 250 35 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c .13  23 1.1  1 .26 33 2.7 1 .48 41 4.6 0 .44 41 4.5 0 2.8 270 26 1 .58 130 6.7 0 .20  28 1.8  1 .36  28 3.8  1 1.2   13 16    1 .25  12 2.7  1 7.1 370 56 1 5.9 340 51 1 5.2 290 42 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c 900     1700 12000    0 870    2400 3400   0 .44 40 3.8 0 .45 40 3.8 0 900   13000 11000 0 160    390 2100   0 900     890 12000    0 900     890 11000    0 900     270 11000    0 900     200 10000    0 900   5300 15000 0 900   7000 10000 0 900   5300 12000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c .14  23 .90 1 .26 33 1.5 1 .48 41 4.5 0 .42 40 3.5 0 2.6 270 23 1 .39 75 4.5 0 .27  28 2.4  1 .36  28 3.8  1 .53  13 6.5  1 .16  12 1.9  1 5.0 290 42 1 5.9 320 52 1 4.7 280 40 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c .12  22 .87 1 .25 33 1.9 1 .49 41 4.7 0 .44 40 3.7 0 2.6 270 24 1 .54 75 6.0 0 .13  28 1.4  1 .14  28 1.1  1 .30  11 3.6  1 .19  12 1.7  1 4.5 280 38 1 4.5 250 37 1 4.7 290 36 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c 900     3000 5800    0 870    1500 5000   0 .47 41 4.1 0 .46 40 4.5 0 900   6200 10000 0 900    710 6100   0 900     1100 11000    0 900     1000 9700    0 890     620 12000    0 900     1900 9800    0 900   5000 13000 0 900   6000 12000 0 900   3000 15000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c 900     1000 9500    0 870    590 9400   0 .45 41 3.9 0 .45 41 4.2 0 910   620 13000 0 900    140 12000   0 900     120 12000    0 900     120 9600    0 900     350 14000    0 900     4000 8700    0 900   8500 9900 0 900   6700 12000 0 900   3800 12000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c .14  23 .84 1 .25 33 2.0 1 .42 40 3.8 0 .46 41 4.1 0 2.9 280 27 1 .56 75 6.5 0 .15  28 1.3  1 .13  28 1.5  1 .40  12 5.0  1 .18  12 1.9  1 4.1 250 35 1 4.3 250 35 1 4.4 250 34 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c .14  25 .85 1 .25 33 2.2 1 .45 41 4.0 0 .45 40 3.8 0 2.7 280 24 1 .55 75 6.6 0 .22  28 2.5  1 .26  28 2.3  1 31     15000 470    0 .19  12 1.8  1 4.4 240 39 1 4.1 250 36 1 4.2 250 32 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c .13  22 .80 1 .27 33 2.0 1 .45 42 4.3 0 .46 40 4.2 0 2.7 270 23 1 .39 75 4.8 0 .27  28 2.4  1 .35  28 3.7  1 .50  13 6.5  1 .19  12 2.0  1 4.9 290 41 1 5.5 310 48 1 4.9 280 42 1
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c .14  23 .83 1 .25 33 2.3 1 .45 40 4.1 0 .42 40 4.2 0 2.8 270 23 1 .38 75 4.7 0 .28  28 2.2  1 .45  28 3.7  1 .61  12 8.0  1 .19  12 1.9  1 4.9 300 39 1 4.7 270 39 1 4.7 290 37 1
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c .13  23 .86 1 .25 33 2.6 1 .46 41 4.0 0 .45 40 4.2 0 2.7 270 25 1 .61 76 7.1 0 .24  28 2.2  1 .26  28 2.5  1 25     15000 310    0 .20  12 1.9  1 4.8 280 37 1 4.6 250 36 1 4.7 290 40 1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c .15  29 1.5  1 .35 38 2.6 1 .45 41 3.8 0 .45 40 3.8 0 2.7 270 23 1 480    130 6900   0 .42  29 4.2  1 .69  32 6.7  1 1.9   20 22    1 .17  12 2.3  1 4.4 250 37 1 4.3 250 36 1 4.3 250 39 1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c .11  23 .82 1 .28 35 2.4 1 .49 40 5.1 0 .43 40 4.6 0 2.8 270 22 1 .40 75 4.7 0 .27  28 2.6  1 .31  28 2.9  1 .68  12 8.2  1 .21  12 2.1  1 4.5 250 36 1 4.6 250 35 1 4.4 250 32 1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c .11  23 1.0  1 .27 33 2.2 1 .46 41 3.8 0 .41 40 3.7 0 2.7 270 23 1 .41 75 4.5 0 .25  28 2.7  1 .29  28 3.4  1 .98  13 11    1 .20  12 1.8  1 4.5 280 38 1 4.3 240 37 1 4.5 290 34 1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c .13  23 .82 1 .25 33 2.2 1 .47 40 4.6 0 .47 41 4.1 0 2.6 270 23 1 .39 75 4.8 0 .30  28 2.6  1 .33  28 2.9  1 .81  13 9.6  1 .20  12 2.3  1 4.2 240 40 1 4.2 260 36 1 4.3 250 37 1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c .14  23 .94 1 .28 33 2.2 1 .48 43 4.5 0 .44 40 3.8 0 2.7 270 25 1 .44 76 4.8 0 .37  28 4.0  1 .47  29 4.2  1 .82  12 11    1 .21  12 2.0  1 4.2 240 36 1 4.3 260 34 1 4.5 260 38 1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c .13  24 .81 1 .27 33 2.3 1 .50 42 4.4 0 .44 40 3.8 0 2.6 270 26 1 .42 76 4.6 0 .31  28 3.4  1 .42  28 4.3  1 26     15000 360    0 .20  12 1.9  1 4.3 250 39 1 4.4 260 42 1 4.2 250 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c .11  23 .95 1 .25 33 1.9 1 .50 41 4.1 0 .45 40 4.6 0 2.7 270 24 1 .55 75 6.4 0 .12  28 1.2  1 .14  28 1.4  1 .48  12 6.3  1 .17  12 1.7  1 4.5 280 41 1 4.3 250 36 1 4.5 280 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c .12  23 .86 1 .24 33 2.7 1 .46 40 3.9 0 .43 40 4.8 0 2.7 270 23 1 .37 75 5.1 0 .11  28 1.3  1 .13  28 1.2  1 1.1   12 16    -32 .17  12 2.2  1 4.3 240 35 1 4.3 240 34 1 4.3 240 37 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c .10  23 1.1  1 .23 33 2.8 1 .48 41 4.6 0 .45 41 3.8 0 2.6 280 22 1 .39 75 4.4 0 .12  28 1.5  1 .12  28 1.3  1 .37  11 4.8  1 .17  12 2.0  1 4.4 280 37 1 4.4 250 35 1 4.4 290 37 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c .10  23 .75 1 .24 33 1.8 1 .46 40 4.4 0 .40 40 4.4 0 2.7 290 28 1 .39 75 4.3 0 .11  28 1.5  1 .16  28 1.1  1 .38  12 4.5  1 .17  12 1.9  1 4.2 240 32 1 4.2 250 39 1 4.1 240 36 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c .14  23 .88 1 .26 33 2.1 1 .49 40 4.2 0 .45 40 4.0 0 2.8 280 26 1 .38 75 5.0 0 .13  28 1.2  1 .14  28 1.2  1 .36  12 4.4  1 .20  12 2.0  1 4.1 230 34 1 4.2 250 35 1 4.1 240 36 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c .13  22 .81 1 .27 33 1.9 1 .48 43 5.0 0 .42 40 3.9 0 2.6 270 24 1 .54 75 7.4 0 .18  28 1.5  1 .19  28 1.9  1 .54  13 7.6  1 .17  12 1.8  1 3.9 230 31 1 4.2 250 34 1 4.3 240 39 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c .14  23 .83 1 .24 33 2.3 1 .49 41 4.8 0 .47 41 3.9 0 2.6 270 23 1 .54 75 6.8 0 .17  28 1.7  1 .29  28 3.1  1 .58  12 7.9  1 .17  12 2.0  1 4.5 280 39 1 4.3 250 40 1 4.6 280 38 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c .14  23 .82 1 .26 33 2.2 1 .50 44 4.4 0 .45 40 4.0 0 2.6 280 23 1 .56 75 6.6 0 .17  28 1.8  1 .30  28 2.8  1 .52  12 7.0  0 .17  12 2.1  1 4.2 240 39 1 4.3 250 37 1 4.1 240 37 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c .10  23 1.1  1 .25 33 2.2 1 .44 40 3.9 0 .47 40 4.2 0 2.6 270 23 1 .56 75 6.3 0 .17  28 2.1  1 .21  28 1.9  1 .93  13 13    1 .17  12 1.6  1 4.2 240 32 1 4.2 250 41 1 4.2 240 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c .11  23 .84 1 .26 33 2.0 1 .51 43 4.8 0 .42 40 4.1 0 2.6 270 22 1 .56 75 7.4 0 .16  28 1.6  1 .22  28 2.3  1 27     15000 360    0 .18  12 1.9  1 4.1 250 41 1 4.3 240 35 1 4.2 240 33 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c .15  24 1.1  1 .27 34 2.2 1 .46 41 4.3 0 .41 39 4.3 0 2.6 270 26 1 .40 75 4.5 0 .20  28 2.1  1 .24  28 2.5  1 1.1   12 14    1 .16  12 1.7  1 4.3 240 35 1 4.1 250 35 1 4.1 240 32 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c .13  23 .98 1 .27 33 2.2 1 .46 41 4.6 0 .49 41 3.9 0 2.8 290 29 1 .37 75 4.7 0 .18  28 1.5  1 .27  28 2.6  1 .58  12 7.8  1 .16  12 2.1  1 4.0 240 36 1 4.0 250 34 1 4.3 240 36 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c .14  23 .85 1 .26 33 2.2 1 .49 41 4.6 0 .46 40 4.2 0 2.7 270 22 1 .55 75 6.1 0 .20  28 1.5  1 .21  28 2.2  1 .72  12 9.7  1 .19  12 1.8  1 4.2 240 34 1 4.2 250 34 1 4.3 240 38 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c .14  23 .88 1 .26 33 2.0 1 .48 41 4.8 0 .45 40 4.2 0 2.6 260 22 1 .39 75 5.7 0 .21  28 2.1  1 .24  28 3.1  1 1.0   13 12    1 .17  12 1.9  1 4.9 290 43 1 5.2 290 42 1 5.3 290 43 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c .10  23 .87 1 .25 33 2.4 1 .44 40 4.5 0 .44 41 5.1 0 2.7 270 23 1 .39 75 4.2 0 .18  28 1.5  1 .25  28 2.1  1 .49  12 6.1  1 .16  12 1.9  1 4.7 300 39 1 5.7 330 45 1 4.9 290 38 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c .15  24 .77 1 .27 34 2.9 1 .48 40 4.0 0 .42 40 3.9 0 2.7 280 21 1 .40 75 4.4 0 .29  28 3.2  1 .37  29 4.5  1 .87  12 10    1 .19  12 1.6  1 6.2 330 45 1 4.3 250 36 1 4.1 240 31 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c .14  23 .83 1 .25 33 2.0 1 .47 43 4.4 0 .43 40 4.0 0 2.6 270 25 1 .55 75 6.3 0 .26  28 2.4  1 .31  28 2.7  1 1.3   13 19    1 .16  12 2.2  1 4.0 250 34 1 4.3 250 37 1 4.1 240 35 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c .12  23 .89 1 .28 33 2.0 1 .50 43 4.3 0 .44 40 4.3 0 2.6 270 22 1 .39 75 4.9 0 .19  28 2.7  1 .25  28 2.5  1 .73  12 9.6  1 .16  12 1.9  1 4.1 240 34 1 4.4 250 39 1 4.4 250 31 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c .14  23 .88 1 .26 33 2.0 1 .51 41 4.1 0 .43 40 4.4 0 2.6 270 22 1 .40 75 4.3 0 .19  28 2.5  1 .25  28 2.0  1 .58  12 6.3  1 .16  12 1.8  1 4.2 240 38 1 4.2 250 38 1 4.4 250 33 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c .13  22 .89 1 .26 33 1.8 1 .44 40 3.5 0 .46 41 4.0 0 2.8 270 22 1 .54 75 5.5 0 .17  28 1.8  1 .17  28 1.9  1 .54  12 6.4  0 .18  12 1.8  1 4.2 240 37 1 4.2 240 35 1 4.0 240 32 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c .11  23 .81 1 .27 33 2.1 1 .48 40 4.0 0 .45 40 4.3 0 2.6 260 23 1 .38 75 4.0 0 .16  28 1.5  1 .23  28 1.7  1 .40  12 5.3  1 .18  12 2.0  1 4.4 270 36 1 4.4 250 37 1 4.6 280 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c .13  22 .84 1 .24 33 2.5 1 .47 41 4.4 0 .43 40 4.1 0 2.6 260 25 1 .36 75 4.7 0 .18  28 1.6  1 .16  28 2.1  1 .44  11 6.0  1 .15  12 1.7  1 4.1 230 33 1 4.3 250 39 1 4.3 240 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c .11  23 .97 1 .25 33 2.8 1 .47 40 4.6 0 .42 40 4.6 0 2.8 270 24 1 .54 75 6.8 0 .18  28 1.9  1 .27  28 2.6  1 .69  12 9.4  1 .16  12 1.7  1 4.0 240 33 1 4.2 240 33 1 6.3 340 55 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c .13  23 .84 1 .23 33 2.9 1 .48 42 4.0 0 .42 40 4.0 0 2.6 260 22 1 .36 75 4.3 0 .18  28 1.7  1 .22  28 3.0  1 .86  12 9.9  0 .17  12 2.1  1 4.2 240 31 1 4.4 250 39 1 4.2 250 38 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c .11  23 1.0  1 .28 33 2.1 1 .50 43 4.2 0 .47 40 4.1 0 2.8 270 23 1 .56 75 7.3 0 .17  28 1.7  1 .22  28 1.7  1 .51  12 6.9  1 .16  12 1.9  1 4.1 250 33 1 4.2 250 35 1 4.3 240 37 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c .12  22 .92 1 .24 33 2.7 1 .50 43 3.7 0 .44 40 3.7 0 2.6 270 23 1 .37 75 4.7 0 .17  28 1.9  1 .20  28 1.6  1 .44  12 6.1  -32 .17  12 2.1  1 4.0 250 37 1 4.2 250 35 1 4.0 240 32 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c .12  23 .73 1 .23 33 2.3 1 .51 41 4.3 0 .44 40 4.1 0 2.7 270 23 1 .55 75 6.8 0 .25  28 2.1  1 .34  28 3.2  1 1.1   13 13    1 .16  12 2.1  1 4.4 250 33 1 4.3 250 38 1 4.2 250 32 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c .12  22 .80 1 .26 33 1.9 1 .53 43 3.8 0 .43 40 3.8 0 2.6 270 26 1 .55 75 5.7 0 .25  28 1.6  1 .37  28 4.9  1 .70  15 8.5  0 .18  12 1.7  1 6.5 340 48 1 4.1 250 40 1 6.1 340 45 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c .12  23 .99 1 .25 33 2.1 1 .47 43 4.2 0 .44 40 3.8 0 2.7 270 24 1 .37 75 4.3 0 .26  28 2.1  1 .35  28 3.0  1 .96  13 13    1 .17  12 1.8  1 4.3 250 37 1 4.7 260 33 1 4.1 240 37 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c .12  23 .89 1 .27 33 2.1 1 .49 40 4.5 0 .46 42 4.3 0 2.6 270 22 1 .38 75 5.2 0 .24  28 1.9  1 .27  28 2.4  1 .81  13 9.6  1 .17  12 2.3  1 4.2 240 34 1 4.2 250 39 1 3.9 230 31 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c .12  23 1.1  1 .27 33 2.4 1 .49 41 4.5 0 .49 41 4.0 0 2.7 270 25 1 .54 75 7.0 0 .23  28 1.9  1 .22  28 2.1  1 .68  12 9.5  1 .16  12 1.9  1 4.6 280 35 1 4.5 260 35 1 4.8 280 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c .11  23 1.1  1 .25 33 2.3 1 .47 40 3.8 0 .44 40 4.6 0 2.7 270 25 1 .56 75 7.5 0 .20  28 2.2  1 .23  28 2.2  1 1.7   13 23    0 .16  12 2.0  1 4.3 240 38 1 4.5 250 35 1 4.1 250 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c .12  23 .84 1 .24 33 2.2 1 .45 41 4.2 0 .43 38 3.6 0 2.7 260 23 1 .39 75 4.6 0 .23  28 2.0  1 .29  28 2.6  1 .85  14 10    1 .20  12 1.8  1 4.1 240 34 1 4.2 250 36 1 4.1 240 34 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c .12  23 .82 1 .24 35 2.3 1 .46 40 4.4 0 .43 40 3.8 0 3.2 310 29 1 .39 75 4.6 0 .20  28 1.4  1 .25  28 2.0  1 .78  12 8.4  1 .17  12 1.9  1 4.2 240 38 1 4.4 250 36 1 4.1 250 37 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c .13  23 .91 1 .25 33 1.9 1 .47 41 4.2 0 .44 41 4.1 0 2.7 270 25 1 .37 75 5.3 0 .22  28 2.2  1 .26  28 2.4  1 1.6   14 19    1 .21  12 2.0  1 4.2 250 37 1 4.2 250 35 1 4.3 250 35 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c .13  23 1.1  1 .25 33 2.1 1 .45 40 4.1 0 .46 40 4.2 0 2.7 270 26 1 .38 75 3.9 0 .31  28 2.8  1 .32  28 3.1  1 1.1   13 13    1 .18  12 2.0  1 4.2 250 36 1 4.2 250 35 1 4.2 250 32 1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c .11  22 .84 1 .25 33 2.1 1 .48 40 4.5 0 .44 40 4.7 0 2.8 270 22 1 .55 75 6.6 0 .23  28 2.1  1 .23  28 2.5  1 .49  13 5.8  0 .16  12 2.2  1 4.3 250 32 1 4.2 260 35 1 4.4 250 36 1
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c .13  23 .80 1 .28 33 2.2 1 .47 41 4.5 0 .45 40 4.1 0 2.7 260 25 1 .39 75 4.8 0 .28  28 2.2  1 .41  28 3.3  1 .48  13 5.6  1 .19  12 1.8  1 4.9 290 39 1 5.6 300 48 1 4.7 290 40 1
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c .12  23 .80 1 .27 33 2.1 1 .47 42 3.9 0 .41 40 4.0 0 2.8 270 21 1 .56 75 6.8 0 .28  28 2.7  1 .30  28 3.1  1 .46  12 4.9  1 .18  12 1.8  1 4.1 240 33 1 4.2 250 34 1 4.2 250 37 1
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c .11  23 .99 1 .24 33 2.1 1 .49 41 4.1 0 .44 40 4.3 0 2.8 270 26 1 .56 100 6.6 0 .28  28 2.3  1 .49  28 4.5  1 .49  12 7.0  1 .16  12 2.1  1 4.2 240 37 1 4.2 250 33 1 4.3 250 34 1
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c .10  23 1.0  1 .24 33 2.1 1 .45 41 4.0 0 .46 40 4.1 0 2.6 270 23 1 .55 75 6.6 0 .24  28 2.0  1 .22  28 2.6  1 26     15000 330    0 .18  12 1.8  1 4.1 240 38 1 4.3 250 35 1 4.2 240 40 1
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c .11  23 .95 1 .28 33 2.1 1 .48 41 3.9 0 .46 40 4.1 0 2.7 280 24 1 .57 75 7.6 0 .21  28 1.9  1 .25  28 2.2  1 .57  12 7.9  1 .18  12 2.4  1 4.8 280 42 1 4.9 270 42 1 5.0 290 43 1
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c .13  23 1.2  1 .28 33 2.0 1 .45 40 5.0 0 .43 40 4.2 0 3.2 290 26 1 .65 79 8.1 0 .19  28 1.5  1 .16  28 1.7  1 3.4   15 46    1 .18  12 2.0  1 6.1 300 56 1 9.9 480 81 1 5.8 290 48 1
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c .14  23 .82 1 .29 33 2.0 1 .50 41 4.0 0 .47 41 4.0 0 2.7 270 26 1 .55 75 7.2 0 .20  28 1.9  1 .25  28 2.5  1 .46  12 5.2  1 .18  12 2.0  1 4.2 240 32 1 4.2 250 40 1 4.2 250 36 1
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c .13  22 .90 1 .24 33 2.6 1 .57 43 5.1 0 .44 40 3.9 0 2.8 270 24 1 .58 75 6.4 0 .18  28 1.5  1 .18  28 1.8  1 .052 11 .34 0 2.4   4300 25    0 4.9 290 43 1 4.9 260 38 1 4.7 280 38 1
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c .14  23 .96 1 .24 33 2.4 1 .47 40 4.5 0 .45 40 4.6 0 2.7 280 26 1 .56 75 6.4 0 .19  28 1.6  1 .18  28 2.1  1 .52  12 6.5  1 .18  12 1.6  1 4.1 240 32 1 4.3 250 36 1 4.4 250 36 1
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c .14  23 1.0  1 .27 33 2.0 1 .48 40 4.7 0 .45 40 4.5 0 2.8 280 24 1 .57 75 6.8 0 .22  28 1.9  1 .25  28 2.3  1 .54  12 7.7  1 .16  12 1.7  1 4.1 240 37 1 4.3 240 38 1 4.3 240 34 1
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c .098 22 .66 0 .26 33 2.3 1 .47 40 4.3 0 .42 40 3.4 0 3.0 280 26 1 .56 49 6.5 0 .14  28 1.3  1 .12  28 1.7  1 .41  12 5.9  1 .16  12 2.1  1 5.7 310 53 1 5.7 320 46 1 5.3 290 46 1
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c .10  22 .62 0 .24 33 2.6 1 .47 40 3.9 0 .44 41 4.3 0 3.2 280 27 1 .56 49 7.7 0 .18  28 1.6  1 .19  28 2.2  1 .62  12 6.6  1 .18  12 2.0  1 5.1 290 42 1 5.5 320 43 1 5.2 290 41 1
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c .11  22 .86 0 .29 33 2.4 1 .49 41 4.5 0 .48 38 3.4 0 900   2500 8200 0 .57 49 6.3 0 .18  28 1.6  1 .20  28 1.5  1 .47  12 5.5  1 .18  12 2.0  1 4.3 240 34 1 4.3 250 39 1 4.3 240 32 1
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c .11  22 .59 0 .28 33 2.1 1 .45 40 4.6 0 .45 40 4.5 0 3.1 310 28 1 .56 51 7.4 0 .17  28 1.6  1 .21  28 1.8  1 .48  12 6.4  1 .16  12 1.6  1 4.0 240 35 1 4.4 250 38 1 4.4 240 37 1
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c .12  22 .94 1 .24 33 2.3 1 .49 41 4.6 0 .45 41 4.2 0 2.5 260 23 1 .55 75 6.1 0 .20  28 1.5  1 .19  28 2.4  1 .53  12 6.1  1 .18  12 1.8  1 4.2 240 37 1 4.2 250 33 1 4.3 250 32 1
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c .11  23 .91 1 .23 33 2.5 1 .48 40 4.5 0 .52 40 3.9 0 2.6 270 26 1 .56 75 5.9 0 .17  28 1.8  1 .20  28 1.9  1 .44  12 4.8  1 .16  12 1.8  1 4.5 280 39 1 4.5 250 36 1 4.6 280 40 1
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c .11  23 .72 1 .24 33 2.6 1 .49 43 4.2 0 .41 40 4.1 0 2.8 270 26 1 .55 75 7.0 0 .17  28 1.7  1 .23  28 3.1  1 .56  13 6.4  1 .18  12 1.7  1 4.3 240 33 1 4.1 250 32 1 4.1 240 32 1
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c .11  22 .94 1 .25 33 2.1 1 .49 43 4.7 0 .48 40 4.1 0 2.6 270 22 1 .55 75 6.4 0 .15  28 1.9  1 .26  28 2.9  1 26     15000 350    0 .16  12 1.9  1 4.0 240 34 1 4.0 250 31 1 3.9 240 30 1
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c .10  23 1.3  1 .27 33 2.1 1 .49 41 4.6 0 .43 40 3.8 0 2.9 290 24 1 .36 75 4.5 0 .19  28 1.7  1 .21  28 1.8  1 .54  12 7.3  1 .18  12 2.0  1 4.2 240 35 1 6.1 340 46 1 4.2 240 35 1
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c .13  22 .74 1 .27 33 2.0 1 .48 41 4.2 0 .44 40 4.0 0 2.6 270 26 1 .54 75 7.2 0 .19  28 1.5  1 .22  28 1.7  1 .58  12 7.3  1 .19  12 1.7  1 4.0 240 32 1 4.1 250 38 1 4.2 240 34 1
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c .14  23 .82 1 .25 35 2.0 1 .51 41 4.6 0 .44 40 3.9 0 2.7 270 26 1 .53 75 6.5 0 .19  28 1.8  1 .21  28 1.7  1 .55  12 7.2  1 .16  12 2.0  1 4.0 250 36 1 4.1 250 32 1 4.2 250 32 1
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c .14  23 .88 1 .26 33 2.1 1 .47 41 4.9 0 .43 40 4.4 0 2.7 270 27 1 .55 75 8.4 0 .19  28 1.9  1 .25  28 2.2  1 .71  12 8.3  1 .16  12 1.8  1 4.2 250 36 1 4.2 250 38 1 4.4 250 37 1
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c .12  23 .81 1 .28 33 1.9 1 .46 40 4.5 0 .44 40 4.3 0 2.9 270 25 1 .56 76 6.5 0 .27  28 2.5  1 .43  28 3.6  1 .57  12 6.9  1 .19  12 1.9  1 4.2 250 37 1 4.3 250 37 1 4.1 250 35 1
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c .13  23 .90 1 .25 33 2.7 1 .48 43 4.9 0 .44 40 4.6 0 2.9 270 25 1 .56 75 7.7 0 .28  28 2.6  1 .24  28 2.5  1 .82  13 10    1 .18  12 1.9  1 4.8 290 37 1 5.4 270 43 1 4.9 280 36 1
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c .12  23 .90 1 .25 33 2.2 1 .46 40 4.1 0 .41 40 4.1 0 2.8 270 24 1 .40 75 4.3 0 .24  28 2.5  1 .30  28 2.9  1 .52  12 5.1  1 .19  12 2.1  1 5.1 290 40 1 6.2 350 51 1 5.3 300 41 1
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c .14  22 .76 1 .28 33 2.2 1 .47 40 4.5 0 .43 40 3.6 0 2.7 270 25 1 .37 75 4.7 0 .29  28 2.4  1 .34  28 3.0  1 .48  12 5.5  1 .21  12 2.0  1 5.3 280 45 1 6.1 340 52 1 5.2 280 40 1
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c .12  24 1.1  1 .23 33 2.4 1 .48 40 4.5 0 .44 37 4.1 0 2.7 270 23 1 .40 75 4.6 0 .25  28 2.1  1 .34  28 2.9  1 .50  12 5.5  1 .20  12 2.0  1 5.2 300 48 1 6.1 340 44 1 4.8 290 39 1
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c .13  23 .90 1 .26 33 2.0 1 .47 40 4.1 0 .45 40 4.0 0 2.7 270 23 1 .41 75 4.7 0 .24  28 2.3  1 .32  29 3.0  1 .55  12 6.1  0 .19  12 1.9  1 4.3 250 39 1 4.3 250 37 1 6.5 340 56 1
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c .11  23 1.2  1 .25 33 2.6 1 .50 42 4.4 0 .46 40 4.2 0 2.7 280 24 1 .55 75 7.2 0 .15  28 1.3  1 .15  28 1.4  1 .48  14 5.7  1 .16  12 2.1  1 4.5 280 40 1 4.3 250 33 1 4.5 270 37 1
termination-crafted-lit/cstrncmp_false-no-overflow.c .16  23 1.4  0 .44 34 4.6 1 .48 41 3.9 0 .46 40 4.1 0 3.7 330 34 1 .68 76 8.3 0 .34  29 2.8  1 .37  29 4.5  1 .064 11 .48 0 .24  13 2.6  1 8.0 370 61 1 6.4 350 54 1 5.8 290 51 1
termination-crafted-lit/gcd1_false-no-overflow.c .15  23 .86 1 .25 35 2.3 1 .48 41 4.2 0 .43 40 4.5 0 2.6 270 20 1 .57 100 6.5 0 .29  28 2.2  1 .26  28 3.7  1 900     120 12000    0 .20  12 2.2  1 4.4 250 37 1 4.2 250 37 1 4.0 250 31 1
termination-crafted-lit/joey_false-no-overflow.c .091 22 .78 0 .30 34 3.1 1 .48 43 5.1 0 .44 40 3.6 0 2.7 270 22 1 630    15000 8800   0 .13  28 1.3  1 .14  28 1.3  1 .43  12 5.1  1 .19  12 1.8  1 5.0 290 48 1 5.3 300 48 1 5.3 300 44 1
termination-crafted-lit/min_rf_false-no-overflow.c .10  23 .90 1 .27 35 2.1 1 .43 40 4.4 0 .47 40 4.1 0 2.8 270 26 1 .42 75 4.8 0 .27  28 2.9  1 .29  28 3.5  1 1.1   13 16    1 .18  12 1.7  1 4.4 250 37 1 4.4 250 40 1 4.3 250 34 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 900     900 7600    0 870    590 8400   0 .46 40 3.8 0 .45 41 3.9 0 850   15000 12000 0 890    120 9800   0 900     620 9300    0 900     590 11000    0 900     650 11000    0 900     4000 9000    0 900   5100 15000 0 900   6300 12000 0 900   3800 12000 0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c .11  22 .87 2 870    1800 6000   0 .48 41 4.9 0 .46 40 5.0 0 2.7 270 23 2 1.4  75 15   0 900     600 9700    0 .12  26 .65 2 900     340 11000    0 900     360 13000    0 5.3 300 42 2 6.8 470 61 2 8.6 400 75 2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c .13  23 .81 2 4.3  61 44   2 .48 41 4.2 0 .47 41 4.1 0 2.7 260 23 2 1.4  75 18   0 .62  26 7.3  2 .074 26 .91 2 .39  11 4.3  2 .15  11 1.4  2 4.6 280 37 2 5.6 310 45 2 5.0 290 40 2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 900     1700 9800    0 870    2300 3900   0 .46 41 4.5 0 .48 40 3.6 0 900   13000 11000 0 120    240 1700   0 900     900 12000    0 900     900 11000    0 900     300 10000    0 900     210 12000    0 900   5300 12000 0 900   7100 14000 0 7.0 370 57 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c 20     610 180    2 870    1700 5400   0 .48 41 4.0 0 .43 37 3.6 0 100   1100 860 2 900    710 12000   0 900     310 11000    0 900     310 12000    0 900     160 12000    0 900     350 8700    0 5.6 290 45 2 7.6 490 68 2 8.1 380 61 2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 900     2500 5800    0 870    1500 4800   0 .48 43 3.7 0 .46 40 3.7 0 900   6200 10000 0 900    1200 8000   0 900     870 9800    0 .23  27 2.6  2 900     640 12000    0 900     1900 11000    0 15   640 130 2 120   2300 1700 2 46   1400 450 2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 900     990 10000    0 870    610 8700   0 .50 41 3.9 0 .43 40 4.0 0 900   540 12000 0 890    130 11000   0 900     130 12000    0 900     130 10000    0 900     370 10000    0 900     4300 11000    0 900   4700 14000 0 900   6600 15000 0 10   490 76 1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c .79  40 9.2  2 1.4  34 15   2 .47 43 4.3 0 .43 40 3.8 0 59   480 780 2 7.3  76 89   0 .18  26 1.7  2 .25  26 3.0  2 900     1800 10000    0 900     3200 8000    0 160   4700 1900 2 900   6400 11000 0 51   1700 470 2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c .14  23 .72 2 870    1400 7400   0 .46 41 4.4 0 .45 40 4.2 0 2.8 270 24 2 1.5  75 17   0 900     240 10000    0 .077 26 .86 2 900     250 9900    0 900     200 12000    0 5.9 300 45 2 7.5 470 69 2 7.0 340 53 2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c .11  23 .69 2 870    1200 8500   0 .45 40 4.3 0 .43 40 4.4 0 2.8 270 23 2 1.5  75 17   0 900     190 12000    0 .12  26 1.3  2 900     660 13000    0 900     1800 10000    0 7.0 330 52 2 16   700 160 2 8.9 490 67 2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c .13  23 .78 2 870    1300 5500   0 .47 41 4.0 0 .41 40 4.1 0 2.9 280 27 2 1.4  75 14   0 900     250 12000    0 .14  26 1.0  2 900     120 10000    0 900     31 12000    0 5.9 300 50 2 8.5 530 83 2 6.9 320 53 2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c .11  23 .80 2 870    2700 7200   0 .46 43 4.2 0 .47 40 4.8 0 3.9 280 36 2 1.5  100 17   0 900     1100 11000    0 .12  26 .78 2 900     230 11000    0 900     190 12000    0 4.9 290 37 2 7.2 440 60 2 5.0 290 44 2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c .12  22 .76 2 870    5500 5100   0 .48 43 3.6 0 .44 40 3.7 0 2.8 260 25 2 1.8  100 25   0 900     280 13000    0 .091 26 .71 2 900     310 11000    0 900     320 10000    0 6.6 320 56 2 7.6 480 68 2 6.6 320 53 2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c .22  25 1.9  2 870    1100 7300   0 .50 44 4.5 0 .47 40 3.9 0 2.8 270 25 2 890    110 13000   0 900     120 12000    0 900     120 13000    0 900     210 12000    0 900     68 12000    0 8.4 380 65 2 14   630 120 2 6.5 330 56 2
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 900     2100 12000    0 870    1400 5700   0 .47 40 4.5 0 .46 40 4.1 0 900   6900 11000 0 200    270 2800   0 900     310 13000    0 900     310 11000    0 900     240 11000    0 900     210 12000    0 900   5300 12000 0 900   6700 11000 0 10   520 84 1
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 900     480 7000    0 870    360 7500   0 .48 40 4.4 0 .44 40 3.7 0 2.8 270 25 2 43    75 540   0 900     110 12000    0 900     99 10000    0 900     75 11000    0 900     66 12000    0 8.0 450 70 2 13   590 130 2 10   500 92 2
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 900     510 6800    0 870    360 6900   0 .47 40 4.0 0 .48 40 4.2 0 2.8 270 24 2 30    75 340   0 900     110 11000    0 900     99 11000    0 900     72 12000    0 900     65 11000    0 7.8 420 63 2 19   690 190 2 7.6 360 60 2
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c .097 25 .88 2 870    2400 4400   0 .49 40 4.4 0 .42 40 4.2 0 900   8000 11000 0 1.9  100 24   0 900     340 12000    0 .16  26 1.5  2 900     500 10000    0 900     430 10000    0 6.0 310 51 2 14   580 120 2 6.4 300 50 2
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 900     1200 7000    0 870    7000 3600   0 .46 40 4.3 0 .42 40 4.6 0 890   15000 11000 0 900    5300 13000   0 900     350 11000    0 900     350 11000    0 900     130 10000    0 900     170 11000    0 900   2500 12000 0 900   6100 13000 0 900   4900 14000 0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 900     1200 9700    0 870    3100 4400   0 .48 43 5.0 0 .47 41 3.9 0 900   4000 9100 0 130    230 1800   0 900     670 9900    0 900     670 11000    0 900     300 9900    0 900     130 11000    0 8.0 440 63 2 93   2000 1000 2 8.8 480 68 2
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c .11  22 .75 2 4.3  62 47   2 .45 40 4.3 0 .45 40 4.2 0 2.8 270 24 2 1.4  75 16   0 .63  26 7.4  2 .11  26 .68 2 .36  11 4.5  2 .14  11 1.6  2 4.8 290 42 2 5.6 310 46 2 4.6 290 39 2
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 900     1700 9400    0 870    2300 3900   0 .49 41 4.0 0 .45 41 4.2 0 900   13000 11000 0 160    390 2000   0 900     900 13000    0 900     900 11000    0 900     270 11000    0 900     190 12000    0 900   5400 13000 0 900   7100 14000 0 900   5300 11000 0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 900     970 10000    0 870    610 10000   0 .48 41 4.3 0 .43 40 4.5 0 910   610 11000 0 900    130 12000   0 900     130 10000    0 900     120 11000    0 900     440 10000    0 900     4200 9700    0 900   8100 8900 0 900   6700 14000 0 900   3800 12000 0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c .75  39 10    2 1.4  35 18   2 .46 43 4.2 0 .42 40 4.3 0 59   460 710 2 13    76 150   0 .16  26 2.2  2 .28  26 3.6  2 900     1900 13000    0 900     3100 7200    0 160   4900 1800 2 900   6400 12000 0 50   1500 500 2
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c .10  22 .76 2 880    8400 3900   0 .49 43 4.4 0 .49 40 4.2 0 2.7 270 26 2 1.2  75 13   0 900     1200 12000    0 .077 26 .80 2 890     31 12000    0 .13  11 1.5  2 4.3 230 33 2 4.1 230 35 2 4.0 240 32 2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c .11  22 .60 2 870    1100 7600   0 .48 42 4.7 0 .41 38 3.6 0 2.9 300 23 2 1.5  75 20   0 900     220 11000    0 .11  26 .75 2 900     100 11000    0 900     230 11000    0 4.8 280 44 2 5.1 280 46 2 4.8 290 37 2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c .11  22 .67 2 870    1200 5600   0 .48 41 4.8 0 .46 40 4.0 0 3.0 290 26 2 1.2  75 16   0 900     190 12000    0 .11  26 1.1  2 900     160 13000    0 900     210 11000    0 4.8 290 49 2 5.8 320 50 2 5.7 300 46 2
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c .11  22 .80 2 870    1200 7100   0 .45 40 4.3 0 .45 40 3.7 0 2.6 270 25 2 1.2  75 13   0 900     520 12000    0 .11  26 .74 2 900     360 11000    0 900     3900 11000    0 5.0 290 40 2 6.5 380 57 2 5.0 280 43 2
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c .11  23 .80 2 870    1600 7700   0 .46 42 4.7 0 .46 40 4.0 0 2.7 270 24 2 1.3  75 16   0 900     460 11000    0 .098 26 .90 2 900     240 11000    0 900     3400 13000    0 5.1 300 39 2 8.5 470 78 2 5.2 300 47 2
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c .094 23 .87 2 870    2000 5700   0 .47 41 4.7 0 .46 40 4.1 0 2.7 270 27 2 1.3  75 17   0 900     680 9900    0 .092 26 .96 2 900     480 11000    0 900     3800 8000    0 5.1 290 44 2 7.5 470 64 2 5.2 290 38 2
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c .10  22 .70 2 870    520 6500   0 .46 41 4.5 0 .47 41 3.9 0 2.8 290 27 2 2.0  75 25   0 900     140 11000    0 .18  26 1.7  2 900     27 11000    0 900     23 13000    0 5.4 300 42 2 6.8 460 57 2 5.7 300 45 2
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c .11  22 .68 2 870    1100 6900   0 .48 43 4.7 0 .44 41 4.4 0 2.7 270 25 2 1.2  75 14   0 900     180 11000    0 .11  26 .95 2 900     670 9500    0 900     81 12000    0 5.5 300 51 2 6.0 310 47 2 5.7 310 44 2
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c .10  22 .94 2 870    1300 7200   0 .48 41 4.4 0 .45 40 4.0 0 2.6 280 23 2 1.5  75 18   0 900     160 12000    0 .11  26 1.1  2 900     31 12000    0 900     51 11000    0 6.0 300 53 2 6.7 450 57 2 6.0 300 53 2
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 6.7   110 77    2 2.7  35 32   2 .47 40 4.1 0 .42 40 4.0 0 900   7100 10000 0 1.4  75 16   0 .41  26 4.8  2 .46  26 6.3  2 .33  11 3.9  2 .17  11 1.6  2 110   3500 1400 2 900   6300 13000 0 120   4000 1500 2
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 900     2700 9500    0 870    1600 8700   0 .50 42 4.8 0 .46 40 3.9 0 900   560 11000 0 900    160 11000   0 900     230 10000    0 900     240 11000    0 900     520 11000    0 900     3900 13000    0 900   5100 12000 0 900   6400 12000 0 900   4800 13000 0
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c .10  22 .79 2 870    1000 5700   0 .45 40 4.0 0 .42 38 4.1 0 2.6 270 23 2 1.3  75 14   0 900     900 10000    0 .079 26 .74 2 900     290 12000    0 900     190 12000    0 5.0 290 40 2 5.7 310 47 2 4.9 290 40 2
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 900     1300 9200    0 870    3100 4400   0 .51 41 4.5 0 .46 40 3.7 0 900   4000 9700 0 270    190 3600   0 900     990 12000    0 900     990 11000    0 900     660 13000    0 900     120 12000    0 8.0 450 69 2 100   2300 1300 2 8.6 470 76 2
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c .11  22 .71 2 880    4500 3700   0 .49 40 4.4 0 .45 40 3.8 0 2.6 270 22 2 1.4  75 17   0 900     490 11000    0 .087 26 .93 2 900     260 11000    0 900     190 13000    0 4.6 280 38 2 5.1 280 41 2 4.7 290 34 2
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c .15  24 1.2  2 870    3400 4500   0 .47 41 4.3 0 .44 40 3.7 0 2.8 270 23 2 1.4  75 18   0 900     950 11000    0 900     940 11000    0 900     940 11000    0 900     250 13000    0 6.1 310 52 2 13   570 120 2 7.4 330 53 2
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c .089 23 .90 2 870    770 4900   0 .45 41 4.1 0 .40 40 4.8 0 2.6 270 25 2 890    320 11000   0 900     190 10000    0 .078 26 .88 2 890     84 12000    0 900     75 12000    0 4.8 280 43 2 5.3 290 45 2 4.6 290 38 2
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 900     2400 11000    0 870    3000 7900   0 .47 41 4.6 0 .43 40 4.6 0 900   6800 13000 0 140    100 1700   0 900     800 9500    0 900     760 11000    0 890     180 10000    0 900     67 11000    0 900   5300 13000 0 900   5200 13000 0 900   5400 11000 0
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c .13  22 .69 2 870    1300 7400   0 .47 43 4.3 0 .44 40 3.9 0 2.5 270 20 2 1.5  75 19   0 900     190 11000    0 .10  26 1.1  2 900     480 11000    0 900     230 10000    0 4.7 270 38 2 4.7 260 39 2 4.6 290 35 2
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c .13  23 .74 2 870    1700 6300   0 .48 40 4.7 0 .44 40 4.7 0 2.7 270 24 2 500    110 6300   0 900     200 11000    0 .11  26 1.3  2 900     360 9800    0 900     210 11000    0 5.0 300 40 2 6.2 380 50 2 7.0 360 45 2
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 900     1000 7100    0 870    640 8300   0 .48 43 4.7 0 .47 40 4.0 0 900   510 13000 0 890    130 9500   0 900     250 14000    0 900     230 12000    0 900     51 14000    0 900     45 14000    0 900   1200 12000 0 900   6000 12000 0 900   990 12000 0
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c .12  22 .67 0 870    7400 6500   0 .49 40 4.0 0 .42 40 4.0 0 3.0 270 24 2 580    15000 7300   0 590     15000 7100    0 690     15000 7100    0 900     500 11000    0 900     240 14000    0 9.0 510 67 2 9.3 520 86 2 11   540 99 2
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c .12  22 .65 0 490    15000 5000   0 .47 41 4.4 0 .44 40 4.5 0 900   5300 10000 0 450    15000 6000   0 510     15000 5600    0 890     15000 7600    0 900     710 9400    0 900     160 12000    0 17   700 160 2 900   5600 14000 0 8.7 450 70 2
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c .090 23 .81 2 870    980 5900   0 .46 40 4.4 0 .43 40 4.0 0 2.6 270 26 2 2.1  75 25   0 900     180 13000    0 .29  26 3.3  2 900     71 11000    0 900     44 11000    0 5.4 300 45 2 11   520 100 2 5.6 320 48 2
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c .10  25 .82 2 870    1800 5700   0 .47 41 4.1 0 .44 40 4.4 0 2.7 270 24 2 1.3  75 14   0 900     560 13000    0 .12  26 .70 2 900     190 11000    0 900     40 12000    0 4.9 290 38 2 6.8 470 56 2 4.9 290 43 2
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c .11  22 .78 2 2.5  37 27   2 .49 41 4.3 0 .44 40 3.7 0 2.6 260 23 2 1.4  75 15   0 .20  26 2.5  2 .11  26 .59 2 1.8   12 24    2 .15  11 1.7  2 4.8 280 43 2 4.9 270 42 2 4.5 280 37 2
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c 18     610 170    2 870    1700 4300   0 .48 43 4.4 0 .44 40 4.3 0 110   1000 790 2 1.8  100 20   0 900     320 11000    0 900     310 13000    0 900     170 10000    0 900     190 11000    0 5.5 290 50 2 7.0 470 63 2 6.2 300 52 2
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c .12  22 .69 2 870    4400 3300   0 .49 43 4.4 0 .45 40 4.2 0 2.5 270 21 2 1.4  75 15   0 900     740 9600    0 .075 26 .86 2 900     280 11000    0 900     240 12000    0 4.5 280 41 2 4.6 260 39 2 4.8 280 35 2
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c .12  22 .78 2 870    2400 3400   0 .44 41 4.1 0 .42 40 4.1 0 2.6 270 25 2 1.7  100 18   0 900     350 12000    0 .12  26 1.2  2 890     480 9800    0 900     680 12000    0 6.0 300 53 2 7.0 480 64 2 6.4 300 49 2
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c .11  22 .94 2 870    1300 5700   0 .50 40 4.7 0 .46 40 4.6 0 2.7 270 23 2 1.2  75 14   0 900     470 10000    0 .083 26 .95 2 900     370 12000    0 900     3900 8100    0 4.9 290 40 2 6.0 340 52 2 4.9 290 35 2
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c .10  22 .76 2 870    2800 5700   0 .48 41 4.3 0 .43 39 4.0 0 2.6 260 23 2 1.4  75 17   0 900     300 9900    0 .096 26 .98 2 900     12 12000    0 .16  12 2.0  2 4.5 290 37 2 4.4 260 39 2 4.6 280 36 2
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c .10  23 .78 2 870    13000 12000   0 .45 40 4.3 0 .45 40 3.9 0 900   4900 12000 0 1.4  100 16   0 900     3600 12000    0 .085 26 .75 2 890     330 9100    0 900     190 11000    0 5.4 300 46 2 6.6 420 51 2 5.9 300 48 2
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c .13  23 .75 2 870    780 4400   0 .47 41 4.1 0 .46 40 4.1 0 4.1 290 39 2 1.4  100 20   0 900     670 10000    0 .11  26 .65 2 900     760 13000    0 900     210 12000    0 5.5 300 50 2 6.9 430 57 2 5.9 300 46 2
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c .12  23 .82 2 870    2600 7900   0 .43 40 4.3 0 .41 40 3.7 0 2.8 270 26 2 1.3  75 17   0 900     420 12000    0 .14  26 1.0  2 900     370 11000    0 900     3700 11000    0 5.8 300 46 2 7.8 470 68 2 6.9 310 58 2
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c .11  22 .88 2 870    2900 5600   0 .48 41 4.8 0 .43 40 4.4 0 2.6 270 24 2 1.3  75 14   0 900     400 9900    0 .10  26 1.0  2 .30  11 3.4  2 900     15000 12000    0 4.8 280 39 2 4.8 260 37 2 4.8 290 37 2
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 3.6   94 42    2 8.1  180 93   2 .52 42 4.1 0 .46 41 4.3 0 900   8100 11000 0 22    75 260   0 5.7   32 72    2 6.1   33 77    2 900     290 10000    0 900     330 8500    0 350   5700 4500 2 900   5800 12000 0 7.7 380 63 2
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c .16  24 1.6  0 870    8400 3400   0 .45 40 4.0 0 .44 41 4.9 0 3.4 310 31 2 1.4  75 20   0 900     5700 10000    0 .19  27 1.7  2 .074 11 .37 0 .22  13 2.3  0 5.1 280 41 2 5.4 300 50 2 5.1 290 47 2
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c .16  24 1.3  0 870    1200 3900   0 .48 40 4.2 0 .41 40 4.3 0 3.4 310 29 2 900    590 11000   0 900     1400 9900    0 .14  27 1.9  2 .073 11 .34 0 .22  13 2.6  0 5.2 280 45 2 5.7 310 54 2 5.4 290 42 2
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c .17  23 1.4  0 870    7500 3700   0 .48 43 4.7 0 .46 41 4.5 0 2.8 280 25 2 1.4  75 14   0 900     2900 9000    0 .15  27 1.3  2 .074 11 .37 0 .18  12 2.1  0 4.9 290 40 2 5.5 300 40 2 5.3 280 45 2
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c .17  24 1.6  0 870    1200 3400   0 .48 40 4.1 0 .44 40 4.1 0 3.3 310 32 2 900    530 11000   0 900     1900 11000    0 .16  27 1.5  2 .061 11 .50 0 .22  13 2.0  0 5.2 280 42 2 5.5 310 47 2 5.1 290 37 2
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c .19  24 1.2  0 870    1200 4400   0 .48 41 3.8 0 .45 40 4.0 0 3.3 310 31 2 900    560 11000   0 900     1800 8300    0 .16  27 1.7  2 .071 11 .40 0 .22  13 2.4  0 5.2 290 41 2 5.6 300 45 2 5.2 290 43 2
termination-crafted-lit/genady_true-termination_true-no-overflow.c .98  30 11    2 9.4  160 110   2 .48 40 4.3 0 .45 40 4.4 0 900   4500 11000 0 54    75 780   0 900     12000 8100    0 900     11000 10000    0 .40  11 4.7  2 .19  12 2.5  2 8.1 420 71 2 36   1000 410 2 6.5 310 49 2
termination-crafted-lit/strchr_true-no-overflow_true-termination.c .20  24 1.4  0 730    8500 3800   0 .46 41 4.6 0 .44 39 3.7 0 2.8 290 23 2 .54 75 5.6 -16 900     1800 11000    0 .12  27 1.4  2 .067 11 .45 0 .19  12 2.2  0 5.1 290 40 2 5.7 320 48 2 5.4 290 41 2
termination-numeric/Addition01_false-no-overflow.c .099 22 .71 0 .27 33 2.4 1 .48 40 4.7 0 .44 37 3.6 0 3.1 310 28 1 .54 49 6.3 0 .17  28 1.6  1 .20  28 1.5  1 .45  12 5.9  1 .16  12 2.0  1 4.3 250 37 1 4.4 260 37 1 4.3 250 35 1
termination-numeric/Avg_true_false-no-overflow.c .12  22 .69 0 .27 35 2.2 1 .47 40 4.2 0 .43 40 4.1 0 2.6 270 24 1 .59 49 6.6 0 .18  28 1.8  1 .17  28 1.8  1 .65  12 7.4  1 .19  12 1.7  1 4.2 250 35 1 4.4 260 38 1 4.3 250 32 1
termination-numeric/Binomial_true-termination_false-no-overflow.c .10  22 .83 0 23    250 280   0 .48 40 4.7 0 .43 41 4.4 0 900   2000 8300 0 27    140 330   0 8.0   80 110    1 5.5   64 71    1 1.1   12 13    0 .24  12 3.1  1 900   1100 6600 0 900   2300 8700 0 900   4800 12000 0
termination-numeric/Et1_true_false-no-overflow.c .12  22 .66 0 .27 33 1.8 1 .48 40 4.6 0 .45 40 4.0 0 2.6 270 21 1 .45 49 5.3 0 .20  28 2.0  1 .24  28 2.0  1 1.3   13 16    1 .18  12 1.7  1 4.1 240 38 1 4.2 250 35 1 4.3 250 33 1
termination-numeric/Et2_true_false-no-overflow.c .099 22 .67 0 .28 33 2.3 1 .49 41 4.2 0 .46 40 4.1 0 2.7 260 27 1 .58 49 8.0 0 .22  28 2.2  1 .27  28 2.7  1 1.1   13 15    1 .19  12 1.8  1 4.3 240 35 1 4.2 250 36 1 4.4 250 36 1
termination-numeric/Et3_true_false-no-overflow.c .12  22 .60 0 .25 33 2.1 1 .45 43 4.5 0 .44 40 3.9 0 2.6 270 21 1 .54 49 7.3 0 .19  28 1.9  1 .22  28 2.1  1 1.2   13 17    1 .16  12 1.9  1 4.2 250 37 1 4.4 250 36 1 4.2 250 33 1
termination-numeric/Et4_true_false-no-overflow.c .12  22 .61 0 .27 34 2.5 1 .48 41 3.9 0 .46 41 4.1 0 2.7 270 23 1 .49 49 5.3 0 .39  28 3.6  1 .44  28 3.5  1 .98  13 12    1 .19  12 1.7  1 4.5 250 38 1 4.4 250 36 1 4.4 250 41 1
termination-numeric/MultCommutative_false-no-overflow.c .11  22 .77 0 .30 34 2.5 0 .48 40 4.8 0 .45 40 4.0 0 900   1600 11000 0 480    15000 5900   0 .30  28 2.8  1 .43  29 4.7  1 .65  12 6.9  0 .27  12 2.8  1 8.1 450 74 1 11   600 120 1 9.2 450 80 1
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c .10  22 .69 0 2.0  78 25   1 .46 41 4.5 0 .45 41 4.0 0 900   1600 7500 0 1.7  140 21   0 16     51 180    1 23     57 310    1 41     39 580    0 12     39 160    1 900   740 6400 0 900   2100 10000 0 60   690 750 -32
termination-numeric/Ackermann01_true-termination_true-no-overflow.c .10  22 .67 0 870    330 2600   0 .48 40 4.6 0 .47 40 4.1 0 900   6500 10000 0 460    15000 6400   0 460     15000 4900    0 620     15000 6600    0 890     17 13000    0 900     2000 11000    0 900   13000 9900 0 900   1700 11000 0 900   13000 5700 0
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c .097 22 .65 0 870    2800 6600   0 .49 41 4.5 0 .43 40 4.0 0 900   4300 11000 0 1.6  49 21   0 900     1100 11000    0 900     1100 12000    0 900     770 10000    0 900     300 14000    0 10   540 86 2 900   5000 12000 0 7.3 370 64 2
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c .10  22 .80 0 870    260 3000   0 .50 42 4.7 0 .47 40 3.7 0 5.3 310 57 1 380    15000 4700   0 900     8800 6500    0 900     11000 11000    0 900     1400 11000    0 900     250 13000    0 900   4700 11000 0 900   1500 10000 0 58   1600 420 1
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c .098 22 .74 0 730    15000 5200   0 .49 42 4.8 0 .43 40 4.1 0 3.0 280 24 2 1.3  49 14   0 900     900 10000    0 900     900 9800    0 890     380 12000    0 900     230 12000    0 5.6 290 43 2 7.6 490 65 2 5.1 290 45 2
termination-numeric/LogRecursive_true-termination_true-no-overflow.c .093 22 .68 0 5.0  91 55   1 .47 41 4.3 0 .44 40 4.0 0 900   1900 9300 0 2.0  77 24   0 84     160 1000    1 110     170 1200    1 35     170 440    1 20     170 290    1 900   490 11000 0 900   5300 12000 0 900   1400 11000 0
termination-numeric/Parts_true-termination_true-no-overflow.c .12  22 .72 0 870    840 5700   0 .46 40 4.3 0 .42 38 4.0 0 900   2900 10000 0 900    430 8100   0 900     2900 13000    0 900     3700 13000    0 900     350 12000    0 900     3200 11000    0 900   5300 13000 0 900   1900 11000 0 900   13000 6200 0
termination-numeric/TwoWay_true-termination_true-no-overflow.c .12  22 .61 0 870    2500 4600   0 .51 41 4.8 0 .45 40 4.1 0 900   740 11000 0 5.8  150 52   0 900     190 9600    0 900     190 10000    0 900     790 8500    0 900     350 9700    0 12   530 120 2 900   2500 9500 0 33   700 390 0
termination-numeric/gcd01_true-termination_true-no-overflow.c .098 22 .85 0 880    5000 4800   0 .46 40 4.1 0 .44 40 4.5 0 3.5 310 33 2 430    15000 5400   0 900     890 8600    0 900     1600 8300    0 900     89 11000    0 900     49 12000    0 5.7 300 50 2 8.4 470 73 2 5.3 310 42 2
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c .55  39 6.7  2 2.7  38 29   2 .50 42 4.3 0 .45 40 3.6 0 15   460 160 2 1.4  75 17   0 .22  26 2.2  2 .22  26 2.8  2 1.9   12 26    2 .31  12 4.1  2 44   1200 460 2 170   4700 2200 2 70   1300 690 2
termination-numeric/recHanoi02_true-termination_true-no-overflow.c .099 22 .76 0 2.6  36 25   1 .49 43 5.1 0 .46 40 3.8 0 900   4400 9800 0 1.8  49 20   0 1.9   28 24    1 2.0   27 27    1 2.1   13 27    1 .65  16 7.7  1 59   1500 640 1 900   4600 13000 0 900   2500 11000 0
termination-numeric/rec_counter1_true-termination_true-no-overflow.c .10  22 .71 0 870    5800 4000   0 .46 41 4.0 0 .43 40 4.6 0 900   4500 12000 0 2.5  97 30   0 900     1100 10000    0 900     1100 9900    0 900     2100 9600    0 900     500 12000    0 900   5600 14000 0 900   5700 15000 0 900   5500 14000 0
termination-numeric/rec_counter3_true-termination_true-no-overflow.c .12  22 .70 0 870    5800 4600   0 .46 40 3.8 0 .46 40 4.6 0 900   5700 11000 0 2.4  99 28   0 900     1200 12000    0 900     1100 9700    0 900     1900 9300    0 900     480 13000    0 900   5600 13000 0 900   5800 12000 0 900   5500 11000 0
termination-numeric/twisted_true-termination_true-no-overflow.c 900     24 9800    0 170    13000 1900   0 .47 41 4.3 0 .45 41 3.9 0 900   7800 11000 0 900    6600 13000   0 900     1200 12000    0 900     1000 9000    0 900     670 11000    0 900     1800 9700    0 900   1300 11000 0 900   5600 12000 0 900   1300 13000 0
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 280 25000   46000 270000 274 280 90000   370000 560000 188 280 130 11000 1200 0 280 120 11000 1200 0 280 45000   320000 540000 313 280 28000 270000 350000 -32 280 96000   250000 1100000 188 280 47000 210000 550000 297 280 94000   190000 1200000 88 280 87000   110000 1100000 195 280 28000 230000 370000 351 280 44000 310000 580000 318 280 25000 190000 320000 319
    correct results 202 87   6400 820 273 167 88   6000 900 185 0 0 229 1200   66000 10000 311 0 169 64   4800 700 186 223 81 6200 910 294 133 94   1600 1200 150 172 42   2100 490 193 250 2200 93000 21000 350 234 2100 87000 22000 318 248 1900 83000 17000 346
        correct true 71 71   3400 700 142 18 46   980 530 36 0 0 82 560   25000 5300 164 0 17 9.3 450 120 34 71 15 1900 160 142 17 9.0 190 110 34 21 3.3 230 36 42 100 1500 53000 16000 200 84 1100 42000 11000 168 98 990 42000 8900 196
        correct false 131 17   3000 120 131 149 42   5000 380 149 0 0 147 600   41000 5100 147 0 152 55   4300 580 152 152 66 4300 750 152 116 85   1400 1100 116 151 39   1800 450 151 150 700 40000 6000 150 150 1000 45000 11000 150 150 920 41000 8200 150
    correct-unconfimed results 1 6.3 280 63 1 3 8.1 160 84 3 0 0 2 8.0 580 82 2 149 630 15000 8500 0 2 86   190 1000 2 3 110 220 1300 3 17 86   390 1100 2 2 21   180 300 2 1 59 1500 640 1 0 5 93 3300 700 5
        correct-unconfirmed true 1 6.3 280 63 1 3 8.1 160 84 3 0 0 2 8.0 580 82 2 0 2 86   190 1000 2 3 110 220 1300 3 2 38   180 470 2 2 21   180 300 2 1 59 1500 640 1 0 5 93 3300 700 5
        correct-unconfirmed false 0 0 0 0 0 149 630 15000 8500 0 0 0 15 49   210 670 0 0 0 0 0
    incorrect results 0 0 0 0 0 2 480 500 5400 -32 0 0 2 1.6 24 22 -64 0 0 0 1 60 690 750 -32
        incorrect true 0 0 0 0 0 0 0 0 2 1.6 24 22 -64 0 0 0 1 60 690 750 -32
        incorrect false 0 0 0 0 0 2 480 500 5400 -32 0 0 0 0 0 0 0
score (280 tasks, max score: 402) 274 188 0 0 313 -32 188 297 88 195 351 318 319
Run set 2ls.sv-comp18.NoOverflows-BitVectors cbmc.sv-comp18.NoOverflows-BitVectors cpa-bam-bnb.sv-comp18.NoOverflows-BitVectors cpa-bam-slicing.sv-comp18.NoOverflows-BitVectors cpa-seq.sv-comp18.NoOverflows-BitVectors depthk.sv-comp18.NoOverflows-BitVectors esbmc-incr.sv-comp18.NoOverflows-BitVectors esbmc-kind.sv-comp18.NoOverflows-BitVectors map2check.sv-comp18.NoOverflows-BitVectors symbiotic.sv-comp18.NoOverflows-BitVectors uautomizer.sv-comp18.NoOverflows-BitVectors ukojak.sv-comp18.NoOverflows-BitVectors utaipan.sv-comp18.NoOverflows-BitVectors