Tool Ceagle Ceagle 1.3 @ 53cfa89
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-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-01-11 10:43:25 CET [[ 2017-01-14 21:26:44 CET ]] [[ 2017-01-14 21:28:35 CET ]] [[ 2017-01-14 21:27:51 CET ]] [[ 2017-01-14 21:29:04 CET ]]
Run set [sv-comp17.Overflows-BitVectors; sv-comp17.Overflows-Other]
Options --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i .028  .029  .22   8.5  0   .38  2.5  1.4  51   150 7.5 4.0 130 320
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i .12   .13   1.2    8.6  0   .27  2.5  1.4  42   160 7.3 3.9 99 320
signedintegeroverflow-regression/Division_false-no-overflow.c.i .11   .11   1.2    8.1  0   0     2.4  1.3  45   150 7.6 4.0 150 310
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i .042  .044  .20   8.5  0   .38  2.3  1.3  44   150 6.9 3.7 110 310
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i .030  .030  .18   8.4  0   .20  2.6  1.4  34   160 8.5 4.4 160 330
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i .10   .10   1.3    8.4  0   .057 2.6  1.5  46   160 7.9 4.2 120 320
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i .11   .11   1.2    8.4  0   .14  2.5  1.4  32   160 7.6 4.1 110 320
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i .11   .11   1.2    8.2  0   .070 3.8  2.2  34   150 7.3 3.9 120 320
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i .11   .11   1.0    8.5  0   .22  2.5  1.4  41   150 7.1 3.8 130 310
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i .11   .11   1.2    8.3  0   .10  2.5  1.4  53   150 7.4 3.9 150 320
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow.c.i .042  .043  .20   8.3  0   .10  4.3  2.4  72   270 7.0 3.8 120 310
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow.c.i .032  .034  .19   8.2  0   .033 5.1  2.8  54   260 7.8 4.1 160 310
signedintegeroverflow-regression/Multiplication_true-no-overflow.c.i .029  .030  .16   8.3  0   .27  3.9  2.1  50   270 6.5 3.5 130 310
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow.c.i .033  .033  .17   8.2  0   .070 5.4  3.0  27   270 7.1 3.8 120 310
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow.c.i .048  .050  .20   8.6  0   .23  4.0  2.2  55   270 7.2 3.8 150 330
termination-crafted/2Nested_false-no-overflow.c .0078 .0082 .020  .92 0   0     .49 .32 11   40 5.7 3.1 120 300
termination-crafted/4NestedWith3Variables_false-no-overflow.c .0096 .0098 .019  .92 0   0     .52 .33 13   39 6.6 3.5 130 300
termination-crafted/Ackermann_false-no-overflow.c .11   .11   1.1    8.1  0   .12  .56 .36 9.6 41 6.8 3.6 86 290
termination-crafted/Bangalore_false-no-overflow.c .0081 .0095 .027  .99 0   0     .62 .39 8.6 39 6.0 3.2 110 290
termination-crafted/Bangalore_v3_false-no-overflow.c .0092 .0096 .027  .74 0   0     .50 .33 11   40 5.8 3.1 82 290
termination-crafted/Benghazi_nondet_false-no-overflow.c .0090 .0092 .025  .89 0   0     .51 .33 11   39 7.2 3.8 110 300
termination-crafted/Binary_Search_false-no-overflow.c .16   .16   1.0    8.0  0   .033 .63 .38 6.3 39 6.0 3.2 110 290
termination-crafted/Cairo_nondet_false-no-overflow.c .0093 .0096 .016  1.0  0   0     .62 .41 7.5 39 6.4 3.4 130 290
termination-crafted/Collatz_unknown-termination_false-no-overflow.c .010  .011  .022  .88 0   0     .75 .47 8.4 41 5.9 3.1 120 300
termination-crafted/Copenhagen_disj_false-no-overflow.c .0083 .010  .026  .86 0   0     .51 .32 10   39 6.6 3.5 110 300
termination-crafted/Gothenburg_false-no-overflow.c .0092 .0095 .019  .78 0   0     .54 .34 12   43 6.1 3.2 110 300
termination-crafted/Gothenburg_v2_false-no-overflow.c .0083 .0086 .019  .76 0   0     .52 .35 13   39 5.7 3.0 110 290
termination-crafted/Hanoi_2vars_false-no-overflow.c .0092 .0094 .016  1.0  0   0     .50 .32 11   39 5.7 3.1 110 300
termination-crafted/Hanoi_3vars_false-no-overflow.c .0093 .0096 .018  .72 0   0     .51 .34 12   41 6.4 3.4 94 300
termination-crafted/Hanoi_plus_false-no-overflow.c .0063 .0080 .033  .92 0   0     .52 .33 10   40 6.2 3.3 81 290
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c .0081 .0084 .025  .84 0   0     .48 .31 11   40 6.3 3.3 120 300
termination-crafted/Mysore_false-no-overflow.c .010  .012  .026  1.0  0   0     .65 .42 7.3 39 7.1 3.7 130 300
termination-crafted/NestedRecursion_1a_false-no-overflow.c .12   .12   1.0    8.0  0   .16  .57 .38 8.3 40 6.3 3.3 110 310
termination-crafted/NestedRecursion_2a_false-no-overflow.c .11   .11   1.1    7.9  0   .033 .55 .35 10   43 7.0 3.7 84 290
termination-crafted/NonTermination1_false-no-overflow.c .0071 .0074 .024  .88 0   0     .63 .40 8.4 40 6.1 3.3 110 300
termination-crafted/NonTermination2_false-no-overflow.c .0073 .0074 .019  .92 0   0     .56 .35 12   42 7.6 4.0 80 320
termination-crafted/NonTermination4_false-no-overflow.c .0095 .011  .027  1.1  0   0     .62 .39 12   45 6.3 3.3 120 300
termination-crafted/NonTerminationSimple2_false-no-overflow.c .0073 .0075 .022  .87 0   0     .48 .32 9.3 39 5.5 2.9 120 300
termination-crafted/NonTerminationSimple3_false-no-overflow.c .0065 .0077 .020  1.0  0   0     .49 .32 9.2 40 6.3 3.3 99 300
termination-crafted/NonTerminationSimple4_false-no-overflow.c .0088 .0090 .026  .95 0   0     .56 .36 11   39 6.5 3.5 140 310
termination-crafted/NonTerminationSimple5_false-no-overflow.c .0082 .0084 .019  .81 0   0     .50 .32 8.4 43 7.2 3.8 72 290
termination-crafted/NonTerminationSimple6_false-no-overflow.c .011  .011  .015  .66 0   0     .63 .41 8.0 39 5.8 3.1 100 300
termination-crafted/NonTerminationSimple8_false-no-overflow.c .0063 .0064 .0    .89 0   0     .54 .34 13   40 6.3 3.3 120 300
termination-crafted/NonTerminationSimple9_false-no-overflow.c .0090 .0098 .028  .89 0   0     .65 .41 8.3 40 5.9 3.1 120 300
termination-crafted/Pure2Phase_false-no-overflow.c .010  .011  .028  .92 0   0     .63 .40 7.2 40 8.3 4.3 92 320
termination-crafted/Pure3Phase_false-no-overflow.c .010  .011  .019  .77 0   0     .51 .33 13   40 6.3 3.4 97 300
termination-crafted/RecursiveMultiplication_false-no-overflow.c .12   .12   1.0    8.2  0   .25  .46 .31 9.6 40 7.4 3.9 84 300
termination-crafted/RecursiveNonterminating_false-no-overflow.c .11   .11   1.3    8.0  0   0     .58 .38 8.1 40 6.7 3.6 75 290
termination-crafted/Rotation180_false-no-overflow.c .0092 .010  .020  1.0  0   0     .50 .32 11   39 6.4 3.5 89 290
termination-crafted/Singapore_false-no-overflow.c .0065 .0088 .027  1.1  0   0     .51 .32 12   39 6.3 3.3 130 300
termination-crafted/Singapore_plus_false-no-overflow.c .0088 .0094 .025  1.1  0   0     .50 .32 9.6 42 6.1 3.2 110 300
termination-crafted/Singapore_v1_false-no-overflow.c .0096 .0099 .021  .88 0   0     .51 .33 10   42 6.7 3.5 96 300
termination-crafted/Singapore_v2_false-no-overflow.c .0091 .0095 .018  .93 0   0     .57 .36 11   42 6.5 3.4 120 300
termination-crafted/Stockholm_false-no-overflow.c .0094 .011  .025  .87 0   0     .52 .34 12   39 6.1 3.2 110 300
termination-crafted/Thun_false-no-overflow.c .0092 .0095 .022  .87 0   0     .57 .36 8.4 40 6.2 3.3 110 300
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c .0081 .0083 .021  .98 0   0     .60 .40 10   42 7.6 4.0 74 290
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c .0094 .0097 .015  .80 0   0     .52 .32 12   39 7.1 3.7 110 310
termination-crafted/aaron2_false-no-overflow.c .0093 .0096 .017  .98 0   0     .60 .37 13   42 7.5 3.9 100 310
termination-crafted/aaron3_false-no-overflow.c .0092 .0095 .022  .90 0   0     .63 .39 14   43 6.2 3.3 81 300
termination-crafted/4BitCounterPointer_true-no-overflow.c .010  .011  .020  .86 0   0     .52 .33 8.9 40 5.5 2.9 100 290
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow.c .011  .012  .013  1.0  0   0     .49 .32 7.4 42 7.3 3.8 120 310
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow.c .010  .011  .016  .85 0   0     .56 .36 9.9 40 5.6 3.1 120 290
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow.c .010  .013  .019  .93 0   0     .48 .30 8.7 39 5.5 3.0 120 290
termination-crafted/Bangalore_true-no-overflow.c .0064 .0068 .028  .62 0   0     .59 .37 10   41 5.8 3.1 120 290
termination-crafted/Bangalore_v2_true-no-overflow.c .0094 .011  .022  .78 0   0     .57 .36 12   44 7.8 4.1 84 300
termination-crafted/Bangalore_v4_true-no-overflow.c .0088 .0090 .021  .85 0   0     .54 .34 13   43 5.3 2.8 110 290
termination-crafted/Benghazi_true-no-overflow.c .0082 .0083 .024  .91 0   0     .55 .36 10   40 6.0 3.2 110 300
termination-crafted/Cairo_step2_true-no-overflow.c .0075 .0077 .036  .94 0   0     .51 .31 11   40 6.3 3.3 120 300
termination-crafted/Cairo_true-no-overflow.c .0060 .0062 .014  .76 0   0     .51 .33 11   43 6.8 3.6 78 300
termination-crafted/Copenhagen_true-no-overflow.c .010  .011  .021  1.0  0   0     .54 .35 13   42 5.9 3.1 110 300
termination-crafted/Division_true-no-overflow.c .011  .013  .025  1.1  0   0     .53 .34 13   41 5.9 3.2 99 290
termination-crafted/LexIndexValue-Array_true-no-overflow.c .0091 .0094 .020  .93 0   0     .51 .33 12   40 7.1 3.7 130 330
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c .0088 .0092 .024  .81 0   0     .47 .31 7.6 40 5.8 3.1 110 300
termination-crafted/Madrid_true-no-overflow.c .0093 .0096 .018  .95 0   0     .51 .33 11   39 6.1 3.3 93 290
termination-crafted/McCarthy91_Iteration_true-no-overflow.c .0071 .0074 .025  .63 0   0     .50 .33 9.7 39 7.0 3.7 120 310
termination-crafted/McCarthy91_Recursion_true-no-overflow.c .11   .11   1.0    7.8  0   .033 .50 .33 11   41 6.7 3.6 85 300
termination-crafted/MenloPark_true-no-overflow.c .0068 .0069 .017  .86 0   0     .49 .32 11   41 6.4 3.3 110 300
termination-crafted/MutualRecursion_1a_true-no-overflow.c .12   .12   1.2    8.0  0   0     .50 .33 10   40 5.8 3.1 110 290
termination-crafted/MutualRecursion_1b_true-no-overflow.c .12   .13   1.2    8.2  0   .25  .52 .34 12   40 4.9 2.7 97 280
termination-crafted/NestedRecursion_1b_true-no-overflow.c .12   .12   1.5    8.0  0   0     .50 .33 9.7 40 6.4 3.4 110 310
termination-crafted/NestedRecursion_1c_true-no-overflow.c .11   .11   1.2    8.1  0   0     .57 .36 12   44 6.2 3.3 120 310
termination-crafted/NestedRecursion_1d_true-no-overflow.c .13   .13   1.4    8.4  0   .25  .49 .32 12   40 6.1 3.2 110 300
termination-crafted/NestedRecursion_2b_true-no-overflow.c .031  .032  .15   8.1  0   .12  .55 .34 12   39 5.9 3.1 110 300
termination-crafted/NestedRecursion_2c_true-no-overflow.c .029  .030  .19   8.1  0   .033 .58 .36 10   42 7.5 3.9 92 310
termination-crafted/NonTermination3_true-no-overflow.c .0084 .0091 .028  .97 0   0     .55 .35 12   40 6.5 3.4 110 310
termination-crafted/NonTerminationSimple7_true-no-overflow.c .0091 .0093 .024  .92 0   0     .53 .34 11   42 5.8 3.1 120 290
termination-crafted/Nyala-2lex_true-no-overflow.c .0072 .0076 .024  1.0  0   0     .49 .32 11   40 5.4 2.8 97 300
termination-crafted/Parallel_true-no-overflow.c .010  .010  .026  .71 0   0     .59 .36 9.2 40 6.0 3.1 110 300
termination-crafted/Piecewise_true-no-overflow.c .0095 .0098 .024  .70 0   0     .70 .46 10   40 6.2 3.3 120 300
termination-crafted/SyntaxSupportPointer01_true-no-overflow.c .0078 .0090 .031  .94 0   0     .54 .35 12   43 6.6 3.5 76 300
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow.c .0075 .0076 .020  .78 0   0     .63 .40 13   43 6.4 3.4 79 290
termination-crafted/Waldkirch_true-no-overflow.c .0097 .010  .022  .63 0   0     .67 .42 8.9 41 5.5 2.9 100 290
termination-crafted/WhileFalse_true-no-overflow.c .0091 .010  .021  .88 0   0     .49 .32 9.7 39 6.4 3.4 130 300
termination-crafted/WhileTrue_true-no-overflow.c .0085 .0099 .031  .92 0   0     .53 .33 9.5 40 6.6 3.5 120 300
termination-crafted/easy1_true-no-overflow.c .010  .010  .017  .93 0   0     .47 .31 11   39 5.3 2.8 95 290
termination-crafted/easy2_true-no-overflow.c .0051 .0053 .010  1.0  0   0     .51 .33 11   39 10   5.3 95 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c .010  .012  .018  .88 0   0     .53 .34 12   41 6.1 3.3 95 290
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c .010  .011  .021  .84 0   0     .50 .31 6.7 40 6.2 3.4 84 290
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c .0090 .0093 .017  .79 0   0     .58 .36 9.7 41 6.7 3.5 100 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c .0095 .0097 .023  .91 0   0     .62 .39 13   46 6.9 3.7 110 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c .0074 .0075 .018  .91 0   0     .55 .35 12   40 6.3 3.4 100 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c .0068 .0081 .019  .88 0   0     .50 .32 12   39 7.0 3.7 90 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c .0077 .0081 .025  .79 0   0     .52 .34 12   41 6.1 3.2 120 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c .0096 .0098 .023  .88 0   0     .49 .32 10   40 6.3 3.3 120 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_false-no-overflow.c .0088 .0090 .031  1.0  0   0     .50 .32 9.3 39 6.6 3.5 110 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c .0093 .0096 .025  1.0  0   0     .51 .32 11   39 7.9 4.1 85 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c .0033 .0035 .017  .76 0   0     .57 .36 13   43 6.1 3.3 110 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c .010  .013  .033  1.0  0   0     .53 .34 10   43 6.6 3.4 130 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c .0073 .0079 .016  1.1  0   0     .55 .35 12   43 6.7 3.5 130 310
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c .0071 .0075 .022  .99 0   0     .54 .34 12   40 6.4 3.4 130 300
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c .0091 .0094 .021  .81 0   0     .48 .31 9.6 40 6.4 3.4 110 300
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c .0095 .0098 .021  1.0  0   0     .50 .32 11   39 6.8 3.6 83 300
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c .010  .011  .015  .86 0   0     .59 .37 8.9 40 7.4 3.9 96 300
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c .012  .014  .032  .91 0   0     .52 .33 11   39 6.6 3.5 140 300
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c .0094 .0097 .0075 .98 0   0     .48 .31 11   40 8.9 4.7 97 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c .010  .011  .020  .88 0   0     .50 .32 10   40 5.8 3.1 120 300
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c .0068 .0068 .0078 .82 0   0     .56 .36 12   43 6.1 3.2 94 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c .0094 .0097 .022  1.1  0   0     .52 .34 9.0 44 6.0 3.2 110 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c .0098 .010  .016  .84 0   0     .51 .33 12   40 6.2 3.3 120 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c .0099 .011  .040  1.0  0   0     .53 .33 12   39 5.8 3.0 86 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c .0094 .010  .021  1.0  0   0     .65 .42 7.4 39 6.3 3.3 97 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c .010  .011  .021  .94 0   0     .54 .34 10   40 6.0 3.2 98 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c .0093 .0095 .020  .97 0   0     .55 .34 12   40 6.1 3.2 100 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c .010  .011  .016  .88 0   0     .57 .35 9.9 39 5.8 3.1 110 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c .0075 .0077 .026  .88 0   0     .53 .34 11   40 8.1 4.3 79 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c .0096 .0099 .024  .92 0   0     .62 .41 7.8 39 6.0 3.2 120 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c .0094 .011  .018  .93 0   0     .49 .32 8.7 40 6.4 3.4 79 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c .0096 .0099 .019  1.1  0   0     .52 .33 12   41 5.3 2.9 89 290
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c .010  .011  .019  .72 0   0     .52 .33 13   40 6.2 3.2 99 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c .0091 .0093 .013  .66 0   0     .52 .33 8.9 40 6.8 3.6 82 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c .0090 .0092 .025  .63 0   0     .67 .43 7.8 42 6.6 3.5 110 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c .010  .011  .018  1.1  0   0     .50 .31 12   40 8.2 4.3 120 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c .0091 .0094 .020  .98 0   0     .51 .32 13   40 5.4 2.9 120 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c .010  .012  .021  1.0  0   0     .54 .36 12   40 7.4 3.9 94 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c .0092 .0094 .021  1.0  0   0     .50 .31 9.3 39 7.7 4.1 83 290
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c .0089 .0092 .018  .90 0   0     .74 .47 8.6 44 5.8 3.1 120 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c .010  .010  .024  .73 0   0     .56 .36 12   40 6.9 3.6 100 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c .011  .011  .023  .88 0   0     .50 .32 11   40 6.0 3.2 120 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c .010  .010  .023  1.1  0   0     .51 .33 12   41 6.8 3.5 120 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c .0094 .0097 .025  1.1  0   0     .54 .36 11   44 5.6 3.0 120 290
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c .0090 .0093 .034  .89 0   0     .54 .34 12   43 6.1 3.2 130 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c .0076 .0078 .018  1.1  0   0     .58 .38 11   40 5.4 2.9 99 290
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c .0094 .0097 .021  1.1  0   0     .54 .35 9.1 40 7.0 3.7 83 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c .010  .011  .024  .99 0   0     .55 .35 12   43 5.7 3.1 100 290
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c .011  .012  .024  1.1  0   0     .52 .32 12   40 5.2 2.8 88 290
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c .0070 .0082 .025  .92 0   0     .56 .36 11   42 6.4 3.4 88 290
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c .0094 .0098 .020  .85 0   0     .49 .32 8.9 40 7.4 4.0 74 290
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c .011  .011  .018  .75 0   0     .52 .32 13   40 6.3 3.3 99 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c .011  .011  .027  .89 0   0     .52 .34 12   40 6.1 3.2 120 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c .0097 .0099 .020  .94 0   0     .51 .31 12   40 6.2 3.3 82 290
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c .0060 .0067 .019  .91 0   0     .51 .33 12   40 6.0 3.2 110 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c .0094 .0096 .019  .76 0   0     .57 .37 8.3 40 6.2 3.2 100 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c .010  .011  .020  .90 0   0     .58 .38 8.5 40 6.2 3.3 130 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c .0053 .0055 .014  .76 0   0     .53 .33 12   40 8.4 4.4 81 310
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c .010  .011  .013  .77 0   0     .50 .33 12   40 5.2 2.8 95 290
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c .0092 .0095 .022  1.1  0   0     .49 .31 11   40 6.2 3.3 100 290
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c .010  .010  .021  .92 0   0     .66 .42 7.7 40 6.4 3.3 53 300
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c .0092 .0095 .014  .85 0   0     .73 .46 9.0 45 6.1 3.2 110 290
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c .0083 .0087 .021  1.1  0   0     .67 .42 7.0 41 6.1 3.2 130 300
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c .0075 .0076 .019  .99 0   0     .54 .34 10   40 7.2 3.8 130 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c .0087 .0090 .029  .92 0   0     .53 .34 9.1 39 5.9 3.1 110 300
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c .010  .010  .024  .88 0   0     .54 .33 11   41 6.0 3.2 120 300
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c .010  .012  .031  1.0  0   0     .49 .32 8.4 40 6.9 3.7 91 300
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c .0070 .0072 .017  .89 0   0     .49 .32 9.4 39 6.8 3.6 79 290
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c .033  .033  .19   8.3  0   0     .54 .34 12   41 6.3 3.3 110 300
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c .12   .12   1.1    8.2  0   .12  .60 .39 9.0 39 5.9 3.1 110 290
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c .12   .12   1.3    8.5  0   .25  .58 .37 9.9 42 6.2 3.3 110 300
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c .11   .11   1.3    7.9  0   0     .58 .38 9.7 42 7.3 3.9 87 290
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c .012  .013  .027  1.0  0   0     .62 .39 6.9 39 5.9 3.1 110 290
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c .0093 .0096 .016  1.1  0   0     .52 .32 11   40 6.3 3.4 91 300
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c .0091 .0094 .026  .76 0   0     .59 .36 12   39 5.8 3.1 110 300
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c .010  .011  .020  .72 0   0     .53 .34 13   43 5.9 3.1 110 300
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c .0099 .010  .024  .88 0   0     .69 .43 8.0 41 5.7 3.1 110 290
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c .0097 .011  .027  .97 0   0     .48 .31 8.6 40 6.0 3.2 120 300
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c .010  .011  .028  1.1  0   0     .56 .37 11   44 6.2 3.3 130 310
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c .010  .011  .024  .82 0   0     .57 .35 10   41 5.7 3.0 100 290
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c .011  .012  .029  1.0  0   0     .58 .37 12   40 7.5 4.0 92 300
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c .0093 .0097 .021  .93 0   0     .49 .31 12   40 7.1 3.7 77 310
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_false-no-overflow.c .0094 .011  .026  .92 0   0     .51 .33 12   39 6.0 3.2 110 300
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c .0078 .0080 .032  .79 0   0     .52 .31 10   40 6.9 3.7 87 300
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c .0098 .010  .024  .88 0   0     .59 .37 8.3 42 7.0 3.7 120 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c .0080 .0082 .026  1.0  0   0     .61 .39 9.1 41 6.0 3.2 110 300
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c .0099 .010  .016  1.0  0   0     .48 .31 12   40 5.9 3.2 110 290
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c .0094 .0098 .018  .92 0   0     .66 .41 8.6 40 6.2 3.3 110 300
termination-crafted-lit/cstrncmp_false-no-overflow.c .0094 .0099 .023  .91 0   0     .47 .31 11   40 6.8 3.6 83 290
termination-crafted-lit/gcd1_false-no-overflow.c .0088 .011  .029  .91 0   0     .56 .36 7.9 39 5.9 3.1 120 300
termination-crafted-lit/joey_false-no-overflow.c .11   .11   1.3    8.4  0   .18  .53 .33 11   40 6.8 3.5 100 310
termination-crafted-lit/min_rf_false-no-overflow.c .0092 .0095 .025  .76 0   0     .53 .34 12   40 5.6 3.0 100 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c .011  .011  .020  .90 0   0     .48 .30 8.6 39 6.2 3.2 130 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c .011  .011  .019  .89 0   0     .53 .34 12   41 6.3 3.4 95 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c .0083 .0086 .023  .92 0   0     .67 .43 9.0 42 6.4 3.3 110 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c .0092 .0094 .021  1.1  0   0     .50 .32 9.7 40 5.4 2.9 110 290
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c .0098 .010  .022  1.0  0   0     .51 .33 13   40 7.2 3.8 100 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c .0067 .0069 .020  1.0  0   0     .49 .32 12   40 6.9 3.6 110 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c .0079 .0094 .028  .85 0   0     .54 .34 9.7 40 6.1 3.2 130 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c .010  .012  .019  1.0  0   0     .50 .32 8.7 41 6.0 3.2 110 290
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c .0094 .0097 .021  .97 0   0     .50 .32 12   39 5.9 3.2 130 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c .010  .010  .025  .78 0   0     .49 .31 9.6 40 5.9 3.1 130 290
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c .0098 .010  .028  .88 0   0     .51 .32 11   40 6.3 3.3 89 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c .0097 .010  .023  .89 0   0     .52 .32 9.8 39 5.6 3.0 110 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c .010  .012  .021  .90 0   0     .51 .33 12   43 6.2 3.3 100 300
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c .0087 .0090 .021  .94 0   0     .53 .34 12   40 5.9 3.1 120 300
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c .0095 .0097 .018  1.0  0   0     .56 .37 11   44 6.1 3.2 120 290
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c .010  .010  .023  .86 0   0     .52 .32 10   39 6.0 3.2 120 290
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c .0074 .0075 .022  .91 0   0     .53 .33 10   41 6.4 3.4 93 300
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c .0043 .0044 .018  .78 0   0     .50 .32 12   42 6.3 3.3 100 300
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c .010  .011  .020  .76 0   0     .59 .37 10   41 6.1 3.2 120 290
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c .0091 .0094 .016  .93 0   0     .65 .41 11   44 6.1 3.2 120 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c .0093 .0095 .019  .93 0   0     .52 .33 10   41 5.6 3.0 91 300
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c .0094 .0097 .027  .92 0   0     .50 .33 11   40 5.7 3.0 110 300
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c .0087 .0090 .033  .92 0   0     .69 .44 9.2 43 6.2 3.3 130 300
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c .010  .010  .017  1.1  0   0     .49 .32 10   40 6.1 3.2 120 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c .0063 .0079 .021  .80 0   0     .52 .33 13   40 5.4 2.9 110 290
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c .0073 .0074 .014  .88 0   0     .71 .46 8.1 40 6.4 3.4 93 290
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c .0092 .011  .022  .93 0   0     .50 .33 11   40 6.4 3.4 100 300
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c .0089 .0092 .028  1.0  0   0     .59 .38 9.3 41 7.4 3.9 110 300
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c .0092 .011  .030  .79 0   0     .52 .35 13   39 6.3 3.4 130 300
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c .011  .013  .029  1.1  0   0     .49 .32 7.9 40 6.1 3.2 120 300
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c .0043 .0045 .018  .93 0   0     .53 .35 11   41 6.2 3.4 76 290
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c .0085 .0095 .023  .78 0   0     .49 .31 9.2 39 6.2 3.3 120 290
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c .0096 .0099 .023  .76 0   0     .52 .33 11   41 6.0 3.2 120 300
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c .0093 .010  .016  .92 0   0     .52 .32 11   40 5.9 3.1 130 300
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c .0092 .0094 .026  .85 0   0     .48 .32 8.5 40 5.5 3.0 110 290
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c .010  .012  .026  1.0  0   0     .56 .36 12   42 6.4 3.4 130 300
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c .0091 .0094 .024  .76 0   0     .51 .32 9.6 40 5.9 3.1 130 290
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c .010  .010  .031  .85 0   0     .52 .34 7.7 39 6.4 3.3 98 290
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c .010  .010  .020  1.0  0   0     .54 .35 12   41 6.8 3.6 96 300
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c .0095 .011  .026  .96 0   0     .48 .32 12   39 6.3 3.3 120 300
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c .010  .010  .015  .83 0   0     .47 .30 11   39 5.8 3.1 120 290
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c .0091 .0094 .033  .77 0   0     .50 .31 9.8 39 6.4 3.4 110 300
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c .010  .012  .018  1.1  0   0     .53 .35 13   41 7.1 3.7 130 300
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c .11   .11   1.1    8.0  0   0     .59 .38 8.4 39 6.2 3.3 110 300
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c .11   .11   1.4    7.9  0   .033 .50 .32 10   39 6.5 3.4 140 320
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c .0065 .0067 .029  .90 0   0     .54 .33 12   41 7.1 3.7 140 310
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c .0092 .011  .028  1.1  0   0     .58 .37 14   43 6.8 3.6 110 300
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c .0073 .0075 .024  1.0  0   0     .52 .33 8.5 39 6.2 3.3 110 300
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c .0094 .0097 .027  1.0  0   0     .51 .33 8.4 39 6.1 3.2 110 300
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c .010  .011  .017  .72 0   0     .58 .36 11   41 6.0 3.2 110 290
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c .0079 .0080 .024  1.0  0   0     .71 .44 8.8 43 6.1 3.2 86 290
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c .011  .011  .015  .92 0   0     .59 .37 10   39 7.1 3.7 90 290
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c .0085 .010  .036  1.1  0   0     .51 .33 11   39 5.8 3.1 100 310
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c .0087 .0090 .022  .89 0   0     .49 .31 11   39 8.4 4.4 81 300
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c .0093 .0095 .022  .82 0   0     .50 .32 9.7 39 6.4 3.4 110 300
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c .0071 .0075 .024  1.0  0   0     .53 .34 11   40 6.4 3.4 98 310
termination-crafted-lit/aviad_true-termination_true-no-overflow.c .0091 .0093 .026  1.1  0   0     .49 .32 10   40 5.9 3.1 110 310
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c .0093 .0096 .021  .72 0   0     .49 .32 11   42 6.0 3.2 110 290
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c .010  .011  .013  1.1  0   0     .50 .32 10   41 6.0 3.2 120 300
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c .010  .012  .023  1.0  0   0     .68 .44 7.7 40 6.9 3.6 120 320
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c .010  .011  .020  .82 0   0     .47 .31 8.8 39 5.6 3.0 100 290
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c .0072 .0073 .022  .89 0   0     .57 .36 9.6 43 6.3 3.3 120 290
termination-crafted-lit/genady_true-termination_true-no-overflow.c .012  .013  .025  .95 0   0     .47 .32 8.5 40 6.8 3.6 110 300
termination-crafted-lit/strchr_true-no-overflow.c .011  .011  .021  .85 0   0     .49 .32 11   40 5.5 2.9 110 280
termination-numeric/Addition01_false-no-overflow.c .13   .13   1.2    8.1  0   .10  .52 .34 12   41 6.5 3.4 99 300
termination-numeric/Avg_true_false-no-overflow.c .11   .11   1.1    8.0  0   .033 .65 .42 7.6 40 5.8 3.1 110 290
termination-numeric/Binomial_true-termination_false-no-overflow.c .010  .010  .018  .92 0   0     .48 .32 12   39 7.6 4.0 75 300
termination-numeric/Et1_true_false-no-overflow.c .11   .11   1.1    8.1  0   .033 .57 .36 13   42 6.0 3.2 85 300
termination-numeric/Et2_true_false-no-overflow.c .12   .12   1.0    8.2  0   .25  .49 .32 12   40 6.2 3.3 100 300
termination-numeric/Et3_true_false-no-overflow.c .11   .11   1.2    8.1  0   .033 .49 .31 9.2 39 5.6 3.0 120 290
termination-numeric/Et4_true_false-no-overflow.c .12   .13   1.2    8.3  0   .25  .63 .41 11   44 6.4 3.3 120 310
termination-numeric/MultCommutative_false-no-overflow.c .11   .11   1.2    8.4  0   .25  .49 .32 11   39 5.8 3.1 110 290
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c .13   .24   1.8    44    0   36     .65 .42 7.4 40 5.8 3.1 110 300
termination-numeric/Ackermann01_true-termination_true-no-overflow.c .11   .11   1.2    8.2  0   .033 .55 .37 8.8 39 5.9 3.1 120 300
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c .11   .11   1.1    8.4  0   .25  .54 .35 9.8 39 5.9 3.1 110 300
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c .11   .12   1.1    8.3  0   .25  .49 .32 12   40 6.7 3.5 110 310
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c .16   .16   1.1    8.1  0   .14  .55 .36 9.7 39 5.4 2.9 100 290
termination-numeric/LogRecursive_true-termination_true-no-overflow.c .11   .11   1.1    8.1  0   .25  .52 .33 10   40 5.7 3.0 100 300
termination-numeric/Parts_true-termination_true-no-overflow.c .010  .012  .021  .95 0   0     .50 .33 9.7 41 7.0 3.7 70 290
termination-numeric/TwoWay_true-termination_true-no-overflow.c .11   .11   1.3    8.0  0   .12  .53 .35 9.8 39 6.8 3.6 110 320
termination-numeric/gcd01_true-termination_true-no-overflow.c .11   .11   1.3    8.0  0   .033 .54 .34 10   44 6.1 3.2 110 310
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c .010  .011  .022  .70 0   0     .50 .33 9.6 40 6.5 3.5 120 300
termination-numeric/recHanoi02_true-termination_true-no-overflow.c .12   .12   .97   8.0  0   .033 .51 .33 11   41 6.9 3.6 110 310
termination-numeric/rec_counter1_true-termination_true-no-overflow.c .010  .010  .023  .97 0   0     .47 .31 8.5 39 6.3 3.3 110 290
termination-numeric/rec_counter3_true-termination_true-no-overflow.c .0085 .0088 .029  1.0  0   0     .50 .33 10   39 8.7 4.5 93 320
termination-numeric/twisted_true-termination_true-no-overflow.c .0081 .0093 .027  .74 0   0     .52 .34 11   40 5.4 2.9 97 280
recursive/Addition02WithOverflowBug_false-no-overflow.c .18   .29   1.3    44    0   36     .50 .31 8.0 39 5.4 2.9 90 290
recursive/Addition03_false-no-overflow.c .11   .11   1.4    8.2  0   .32  .53 .34 13   40 7.1 3.7 85 300
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c .11   .11   1.2    8.4  0   .25  .62 .41 7.8 39 5.8 3.1 120 300
recursive/Ackermann01_true-unreach-call_true-no-overflow.c .11   .11   1.4    8.6  0   .25  .57 .36 13   43 6.0 3.2 110 300
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c .12   .13   1.2    8.5  0   .25  .50 .32 8.9 40 7.1 3.8 130 320
recursive/Ackermann03_true-unreach-call_true-no-overflow.c .11   .11   1.2    8.3  0   .12  .62 .40 8.3 40 6.5 3.4 120 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c .11   .11   1.3    8.4  0   .25  .49 .32 10   40 6.8 3.6 110 310
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c .13   .24   1.6    44    0   36     .52 .32 10   40 6.5 3.5 110 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c .11   .11   1.2    8.0  0   .10  .50 .32 9.8 40 5.6 3.0 120 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c .074  .21   .71   44    0   36     .53 .34 13   40 5.7 3.1 110 290
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c .11   .11   1.2    8.3  0   .14  .57 .36 10   43 6.3 3.3 100 300
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c .11   .11   1.0    7.9  0   .033 .57 .36 13   39 7.3 3.9 87 300
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c .11   .11   1.2    7.9  0   0     .65 .41 13   43 5.5 3.0 100 290
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c .13   .13   1.1    8.4  0   .25  .55 .36 13   43 5.5 3.0 110 280
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c .12   .13   1.3    8.1  0   .25  .52 .34 11   41 5.6 3.0 110 300
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c .12   .12   1.1    8.2  0   .033 .55 .35 10   43 7.5 3.9 74 300
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c .11   .12   1.1    8.0  0   0     .69 .44 8.1 41 5.4 2.9 110 290
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c .11   .11   1.2    8.2  0   .25  .55 .35 8.7 39 6.1 3.2 120 300
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c .11   .11   1.1    8.5  0   .42  .57 .35 9.1 41 7.2 3.8 90 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c .095  .096  1.2    7.9  0   .17  .57 .36 9.5 39 6.4 3.4 130 300
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c .11   .12   1.3    8.3  0   .25  .53 .34 13   43 5.9 3.2 100 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c .12   .13   1.5    8.3  0   .090 .60 .38 12   41 6.7 3.5 100 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c .11   .11   1.2    8.4  0   .25  .50 .33 7.5 42 5.8 3.1 100 290
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c .13   .13   1.2    8.5  0   .25  .51 .33 12   41 5.7 3.1 110 290
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c .12   .12   1.2    8.1  0   0     .71 .45 5.4 43 6.0 3.1 130 290
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c .11   .11   1.4    8.0  0   0     .62 .40 8.5 40 6.9 3.6 130 310
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c .11   .11   1.1    8.0  0   0     .49 .32 12   40 6.6 3.5 140 300
bitvector/jain_1_false-no-overflow.i .0092 .010  .020  .92 0   0     .54 .34 12   40 6.7 3.6 93 300
bitvector/jain_2_false-no-overflow.i .0044 .0045 .021  1.0  0   0     .54 .34 8.6 39 7.0 3.7 79 290
bitvector/jain_4_false-no-overflow.i .0086 .0089 .021  .86 0   0     .56 .35 9.7 39 6.9 3.6 100 300
bitvector/jain_5_false-no-overflow.i .0071 .0072 .020  .88 0   0     .51 .33 12   40 5.8 3.1 110 300
bitvector/jain_6_false-no-overflow.i .010  .011  .018  .82 0   0     .50 .32 11   40 7.0 3.7 88 300
bitvector/jain_7_false-no-overflow.i .010  .011  .021  .72 0   0     .61 .40 8.0 40 6.1 3.2 110 300
bitvector/modulus_false-no-overflow.i .0076 .0078 .025  .88 0   0     .63 .40 7.8 39 6.0 3.2 110 300
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i .0050 .0054 .021  .79 0   0     .49 .31 12   39 6.3 3.3 110 300
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i .0091 .0094 .022  .76 0   0     .50 .32 10   40 7.7 4.0 140 350
bitvector/byte_add_false-unreach-call_true-no-overflow.i .011  .011  .020  .93 0   0     .63 .40 8.3 40 5.7 3.0 120 300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i .011  .013  .025  1.0  0   0     .52 .34 11   39 6.1 3.2 110 290
bitvector/gcd_2_true-unreach-call_true-no-overflow.i .0095 .0098 .019  1.0  0   0     .56 .36 12   44 6.6 3.5 77 300
bitvector/gcd_3_true-unreach-call_true-no-overflow.i .011  .011  .019  .90 0   0     .50 .31 12   40 6.0 3.2 130 300
bitvector/gcd_4_true-unreach-call_true-no-overflow.i .0098 .010  .020  1.0  0   0     .50 .32 12   40 6.1 3.2 110 300
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i .0068 .0069 .029  .77 0   0     .48 .31 11   39 6.3 3.3 110 300
bitvector/jain_1_true-unreach-call_true-no-overflow.i .0090 .0096 .017  .99 0   0     .56 .35 12   43 5.9 3.1 82 290
bitvector/jain_2_true-unreach-call_true-no-overflow.i .010  .012  .030  1.1  0   0     .48 .32 8.7 39 5.9 3.2 110 300
bitvector/jain_4_true-unreach-call_true-no-overflow.i .010  .012  .027  .96 0   0     .49 .32 9.7 40 5.9 3.1 97 300
bitvector/jain_5_true-unreach-call_true-no-overflow.i .010  .011  .024  1.0  0   0     .51 .33 12   40 5.9 3.1 110 290
bitvector/jain_6_true-unreach-call_true-no-overflow.i .0097 .010  .024  1.0  0   0     .51 .33 13   40 6.7 3.6 130 320
bitvector/jain_7_true-unreach-call_true-no-overflow.i .010  .011  .020  .87 0   0     .51 .33 8.4 40 7.7 4.1 95 320
bitvector/modulus_true-unreach-call_true-no-overflow.i .011  .012  .028  1.0  0   0     .51 .33 11   39 6.9 3.7 86 300
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i .010  .011  .015  .88 0   0     .48 .31 9.3 39 7.6 4.0 110 320
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i .010  .011  .018  .88 0   0     .49 .32 10   40 6.1 3.2 120 300
bitvector/parity_true-unreach-call_true-no-overflow.i .0093 .0097 .016  .93 0   0     .47 .30 11   39 7.3 3.9 90 300
bitvector/sum02_false-unreach-call_true-no-overflow.i .010  .010  .019  .88 0   0     .50 .33 11   40 6.9 3.7 81 300
bitvector/sum02_true-unreach-call_true-no-overflow.i .0092 .0095 .027  .89 0   0     .50 .32 10   39 5.6 2.9 79 300
../../sv-benchmarks/c/ verifier status cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 328 11    11    89    1000 0   150    328 110 69 2000 7800   328 1100 570 17000 49000   328 110 67 1900 7700   328 1000 550 18000 49000  
    correct results 15 1.1  1.1  9.7  130 0   2.5  0 26 15 420 1500   10 75 40 1300 3200   5 23 12 260 1300   5 36 19 660 1600  
        correct true 5 .18 .19 .92 42 0   .71 0 0 0 0 0   0 0 0 0 0   5 23 12 260 1300   5 36 19 660 1600  
        correct false 10 .88 .89 8.7  84 0   1.8  0 26 15 420 1500   10 75 40 1300 3200   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (328 tasks, max score: 491) 20
Run set [sv-comp17.Overflows-BitVectors; sv-comp17.Overflows-Other]