Tool 2LS 0.5.0
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 11:02:28 CET [[ 2017-01-14 22:09:21 CET ]] [[ 2017-01-14 22:27:59 CET ]] [[ 2017-01-14 22:12:16 CET ]] [[ 2017-01-14 22:31:32 CET ]]
Run set [sv-comp17.Overflows-BitVectors; sv-comp17.Overflows-Other]
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_1102.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 false(no-overflow) .14  .13  .85 24 0      0    false(no-overflow) 4.9  2.7  73   250 false(no-overflow) 7.7 4.1 110 310 - -
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .097 .091 .98 24 0      0    false(no-overflow) 5.1  2.8  56   240 false(no-overflow) 9.4 5.0 98 310 - -
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .12  .11  .82 24 0      0    false(no-overflow) 4.0  2.2  90   250 false(no-overflow) 8.0 4.3 110 320 - -
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .11  .10  1.1  24 0      0    false(no-overflow) 5.2  2.9  57   250 false(no-overflow) 7.6 4.1 120 320 - -
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .14  .13  .89 24 0      .16 false(no-overflow) 4.1  2.3  88   250 false(no-overflow) 8.2 4.4 90 310 - -
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .13  .12  .87 24 0      0    false(no-overflow) 4.1  2.2  93   240 false(no-overflow) 8.0 4.2 110 310 - -
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .11  .10  .91 24 0      0    false(no-overflow) 4.7  2.6  57   240 false(no-overflow) 9.3 4.9 110 320 - -
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .11  .10  .93 24 0      0    false(no-overflow) 4.0  2.2  67   270 false(no-overflow) 7.9 4.2 100 300 - -
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .11  .11  .84 24 0      0    false(no-overflow) 5.1  2.8  56   250 false(no-overflow) 7.7 4.1 150 310 - -
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .11  .10  1.1  24 0      0    false(no-overflow) 5.2  2.8  57   250 false(no-overflow) 8.7 4.6 100 310 - -
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow.c.i true .12  .12  .78 24 0      0    - - true 4.3  2.4  76   250 true 6.3 3.4 130 300
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow.c.i true .10  .095 .92 24 0      0    - - true 4.0  2.2  59   260 true 9.0 4.8 110 320
signedintegeroverflow-regression/Multiplication_true-no-overflow.c.i true .098 .094 .90 24 0      0    - - true 4.8  2.6  49   260 true 9.4 4.9 80 310
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow.c.i true .13  .12  .85 24 0      0    - - true 5.1  2.8  62   270 true 7.5 4.0 91 300
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow.c.i true .13  .12  .81 24 0      0    - - true 4.2  2.3  67   260 true 8.5 4.6 93 310
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .13  .12  .86 22 .0041 0    false(no-overflow) 4.1  2.3  43   240 false(no-overflow) 9.2 4.9 86 310 - -
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .16  .15  1.0  24 .0041 0    true 3.1  1.7  63   240 false(no-overflow) 8.9 4.7 99 310 - -
termination-crafted/Ackermann_false-no-overflow.c error (5) .10  .096 .76 22 .0041 0    error (invalid witness file) .53 .34 11   42 error (invalid witness file) 7.2 3.8 82 290 - -
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .13  .12  .83 22 .0041 0    false(no-overflow) 3.6  2.0  56   230 false(no-overflow) 8.4 4.4 91 310 - -
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .11  .10  .88 22 .0041 0    false(no-overflow) 3.5  1.9  61   250 false(no-overflow) 8.5 4.5 71 320 - -
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .11  .11  .70 22 .0041 0    true 3.1  1.7  68   240 false(no-overflow) 7.3 3.9 120 320 - -
termination-crafted/Binary_Search_false-no-overflow.c error (5) .088 .088 .73 22 .0041 0    error (invalid witness file) .74 .46 7.9 43 error (invalid witness file) 7.5 4.0 63 290 - -
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .11  .10  .96 23 .0041 0    false(no-overflow) 3.7  2.1  51   240 false(no-overflow) 8.3 4.4 130 330 - -
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .11  .10  .99 23 .0041 0    false(no-overflow) 3.2  1.8  52   240 false(no-overflow) 8.9 4.8 89 320 - -
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .12  .12  .98 22 .0041 0    false(no-overflow) 3.2  1.8  63   240 false(no-overflow) 7.5 4.1 100 310 - -
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .12  .11  .96 23 .0041 .10 false(no-overflow) 3.3  1.9  67   240 false(no-overflow) 9.2 4.9 95 320 - -
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .10  .098 1.1  23 .0041 0    true 3.4  1.9  56   230 false(no-overflow) 9.0 4.8 120 330 - -
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .15  .14  .82 22 .0041 .17 false(no-overflow) 3.3  1.9  74   230 false(no-overflow) 6.7 3.6 120 310 - -
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .14  .14  .79 23 .0041 0    true 3.3  1.9  51   240 false(no-overflow) 8.3 4.4 130 320 - -
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .13  .13  .76 23 .0041 .12 true 3.8  2.1  39   240 false(no-overflow) 8.1 4.3 110 310 - -
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .13  .12  .80 22 .0041 .16 false(no-overflow) 4.2  2.4  45   250 false(no-overflow) 7.8 4.2 150 330 - -
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .14  .13  .81 22 .0041 0    true 3.9  2.2  39   230 false(no-overflow) 10   5.5 100 330 - -
termination-crafted/NestedRecursion_1a_false-no-overflow.c error (5) .094 .092 .80 22 .0041 0    error (invalid witness file) .58 .36 9.3 41 error (invalid witness file) 6.6 3.4 63 300 - -
termination-crafted/NestedRecursion_2a_false-no-overflow.c error (5) .081 .080 .78 22 .0041 0    error (invalid witness file) .60 .38 8.6 41 error (invalid witness file) 6.5 3.4 77 300 - -
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .14  .13  .77 22 .0041 0    false(no-overflow) 4.3  2.4  37   230 false(no-overflow) 8.7 4.6 93 310 - -
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .13  .12  1.0  22 .0041 0    false(no-overflow) 3.1  1.8  54   230 false(no-overflow) 9.8 5.2 63 310 - -
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) .77  .76  10    36 .0041 .16 false(no-overflow) 5.1  2.8  70   260 out of memory 77   47   940 7000 - -
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .12  .11  .83 22 .0041 0    false(no-overflow) 3.2  1.8  78   240 false(no-overflow) 9.1 4.8 78 310 - -
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .13  .12  .85 22 .0041 0    false(no-overflow) 3.4  1.9  62   240 false(no-overflow) 8.4 4.5 76 300 - -
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 900     900     10000    1200 .0041 0    error (invalid witness file) .65 .41 7.3 40 error (invalid witness file) 5.9 3.1 96 290 - -
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) .12  .12  .85 22 .0041 0    false(no-overflow) 3.8  2.1  59   240 false(no-overflow) 9.4 5.0 82 320 - -
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .11  .10  .82 22 .0041 0    false(no-overflow) 3.3  1.9  51   230 false(no-overflow) 8.2 4.4 94 310 - -
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .15  .14  .91 23 .0041 0    false(no-overflow) 3.1  1.8  65   240 false(no-overflow) 11   5.5 100 350 - -
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .12  .11  .86 22 .0041 0    false(no-overflow) 3.1  1.8  61   240 false(no-overflow) 9.1 4.8 93 320 - -
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .13  .13  .81 22 .0041 0    false(no-overflow) 3.3  1.9  55   230 false(no-overflow) 8.4 4.6 100 310 - -
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .14  .13  .95 23 .0041 0    true 3.1  1.8  64   240 false(no-overflow) 9.4 4.9 100 320 - -
termination-crafted/RecursiveMultiplication_false-no-overflow.c error (5) .096 .093 .67 22 .0041 0    error (invalid witness file) .52 .32 13   41 error (invalid witness file) 6.9 3.7 89 310 - -
termination-crafted/RecursiveNonterminating_false-no-overflow.c error (5) .081 .080 .61 22 .0041 0    error (invalid witness file) .49 .32 9.9 39 error (invalid witness file) 7.0 3.7 78 300 - -
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .11  .10  .93 22 .0041 0    false(no-overflow) 3.9  2.2  43   230 false(no-overflow) 10   5.4 84 320 - -
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .14  .14  .82 22 .0041 0    false(no-overflow) 3.9  2.2  44   230 false(no-overflow) 7.2 3.8 140 320 - -
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .13  .12  1.1  22 .0041 0    false(no-overflow) 3.4  1.9  56   240 false(no-overflow) 7.4 4.0 140 320 - -
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .14  .13  .86 22 .0041 0    false(no-overflow) 3.3  1.9  55   240 false(no-overflow) 8.6 4.6 110 310 - -
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .10  .099 .99 23 .0041 .16 false(no-overflow) 3.1  1.9  58   230 false(no-overflow) 8.9 4.7 120 310 - -
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .12  .11  .94 23 .0041 0    false(no-overflow) 3.2  1.8  69   240 false(no-overflow) 9.3 4.9 81 320 - -
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .14  .13  1.0  22 .0041 0    false(no-overflow) 3.4  1.9  42   240 false(no-overflow) 9.0 4.8 110 310 - -
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .13  .13  .79 23 .0041 .16 false(no-overflow) 3.4  1.9  52   240 false(no-overflow) 9.2 5.0 97 320 - -
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .14  .13  .95 25 .0041 0    false(no-overflow) 4.5  2.5  53   240 false(no-overflow) 13   7.3 160 370 - -
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .15  .14  .88 23 .0041 0    false(no-overflow) 3.9  2.2  37   240 false(no-overflow) 10   5.5 120 330 - -
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .11  .10  .92 23 .0041 0    true 3.2  1.8  59   240 false(no-overflow) 9.0 4.8 92 320 - -
termination-crafted/4BitCounterPointer_true-no-overflow.c true .21  .20  1.4  24 .012  .12 - - true 6.1  3.4  66   290 true 9.0 4.8 99 310
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow.c true 5.4   5.4   55    160 .0041 0    - - out of memory 230    220    4600   7000 timeout 960   790   18000 4500
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow.c true 2.7   2.7   32    75 .0041 0    - - false(no-overflow) 3.7  2.1  62   290 true 7.0 3.7 120 320
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow.c true 3.0   3.0   34    130 .0041 .16 - - timeout 900    860    20000   4900 true 9.4 5.1 150 320
termination-crafted/Bangalore_true-no-overflow.c true .10  .096 .79 22 .0041 0    - - true 3.9  2.2  74   280 true 11   5.6 93 330
termination-crafted/Bangalore_v2_true-no-overflow.c true .12  .11  .81 22 .0041 .16 - - true 4.3  2.4  71   280 true 8.0 4.3 140 330
termination-crafted/Bangalore_v4_true-no-overflow.c true .13  .12  1.4  23 .0041 0    - - false(no-overflow) 4.3  2.4  56   280 true 8.8 4.7 140 340
termination-crafted/Benghazi_true-no-overflow.c timeout 900     900     8300    260 .0041 0    - - error (invalid witness file) .57 .37 12   41 error (invalid witness file) 5.6 3.0 100 290
termination-crafted/Cairo_step2_true-no-overflow.c timeout 900     900     10000    1300 .0041 0    - - error (invalid witness file) .60 .38 8.1 41 error (invalid witness file) 7.0 3.7 70 310
termination-crafted/Cairo_true-no-overflow.c timeout 900     900     12000    1500 .0041 0    - - error (invalid witness file) .51 .32 11   39 error (invalid witness file) 8.4 4.4 94 320
termination-crafted/Copenhagen_true-no-overflow.c true .12  .11  .76 22 .0041 0    - - true 4.9  2.8  57   280 true 8.3 4.5 140 310
termination-crafted/Division_true-no-overflow.c true .11  .10  .85 22 .0041 0    - - true 3.7  2.1  56   270 true 9.0 4.8 110 340
termination-crafted/LexIndexValue-Array_true-no-overflow.c true 5.8   5.8   65    220 .0041 0    - - out of memory 570    550    11000   7000 timeout 960   790   16000 4300
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout 900     900     5400    11000 .012  0    - - error (invalid witness file) .55 .35 14   42 error (invalid witness file) 6.9 3.7 67 280
termination-crafted/Madrid_true-no-overflow.c true .12  .12  .80 22 .0041 0    - - true 4.1  2.3  53   280 true 8.0 4.3 86 310
termination-crafted/McCarthy91_Iteration_true-no-overflow.c timeout 900     900     12000    1500 .0041 .13 - - error (invalid witness file) .60 .37 9.0 40 error (invalid witness file) 6.0 3.2 84 310
termination-crafted/McCarthy91_Recursion_true-no-overflow.c error (5) .11  .11  .70 22 .0041 0    - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 7.1 3.7 91 300
termination-crafted/MenloPark_true-no-overflow.c timeout 900     900     7900    860 .0041 0    - - error (invalid witness file) .69 .43 7.0 40 error (invalid witness file) 7.1 3.7 80 300
termination-crafted/MutualRecursion_1a_true-no-overflow.c error (5) .12  .11  .73 22 .0041 0    - - error (invalid witness file) .50 .32 9.3 41 error (invalid witness file) 5.6 3.0 110 290
termination-crafted/MutualRecursion_1b_true-no-overflow.c error (5) .097 .093 .75 22 .0041 0    - - error (invalid witness file) .48 .30 12   40 error (invalid witness file) 7.6 4.0 79 310
termination-crafted/NestedRecursion_1b_true-no-overflow.c error (5) .12  .12  .74 22 .0041 0    - - error (invalid witness file) .64 .41 7.7 40 error (invalid witness file) 6.4 3.4 99 300
termination-crafted/NestedRecursion_1c_true-no-overflow.c error (5) .13  .12  .66 22 .0041 0    - - error (invalid witness file) .65 .41 9.4 43 error (invalid witness file) 7.4 3.9 68 300
termination-crafted/NestedRecursion_1d_true-no-overflow.c error (5) .12  .12  .70 22 .0041 0    - - error (invalid witness file) .54 .33 13   42 error (invalid witness file) 6.7 3.5 87 300
termination-crafted/NestedRecursion_2b_true-no-overflow.c error (5) .082 .078 .78 22 .0041 0    - - error (invalid witness file) .51 .33 8.2 45 error (invalid witness file) 6.7 3.5 97 300
termination-crafted/NestedRecursion_2c_true-no-overflow.c error (5) .12  .12  .61 22 .0041 0    - - error (invalid witness file) .49 .30 8.1 40 error (invalid witness file) 5.6 3.0 82 300
termination-crafted/NonTermination3_true-no-overflow.c true .13  .13  .73 23 .0041 0    - - true 4.9  2.8  64   280 true 7.7 4.1 110 310
termination-crafted/NonTerminationSimple7_true-no-overflow.c true .10  .10  .74 22 .0041 0    - - true 4.2  2.4  72   280 true 7.6 4.0 130 330
termination-crafted/Nyala-2lex_true-no-overflow.c true .13  .13  .76 22 .0041 0    - - true 5.0  2.8  56   280 true 8.0 4.3 140 320
termination-crafted/Parallel_true-no-overflow.c true .12  .12  .83 22 .0041 0    - - true 4.1  2.3  62   280 true 8.6 4.6 96 330
termination-crafted/Piecewise_true-no-overflow.c true .14  .13  .79 23 .0041 .16 - - true 4.9  2.7  92   280 true 8.1 4.3 150 330
termination-crafted/SyntaxSupportPointer01_true-no-overflow.c true .20  .19  1.4  23 .012  0    - - true 4.7  2.6  68   280 true 9.3 5.1 130 330
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow.c true .13  .13  .91 22 .0041 .16 - - true 4.7  2.6  77   280 true 9.0 4.8 140 320
termination-crafted/Waldkirch_true-no-overflow.c true .11  .10  .80 22 .0041 0    - - true 4.4  2.5  46   280 true 9.2 4.9 96 320
termination-crafted/WhileFalse_true-no-overflow.c true .11  .10  .73 22 .0041 0    - - true 4.5  2.5  45   270 true 7.2 3.9 120 310
termination-crafted/WhileTrue_true-no-overflow.c true .10  .096 .78 22 .0041 .17 - - true 3.7  2.0  70   270 true 8.6 4.6 93 310
termination-crafted/easy1_true-no-overflow.c true .10  .097 .87 22 .0041 0    - - true 3.9  2.2  45   280 true 8.4 4.5 110 320
termination-crafted/easy2_true-no-overflow.c timeout 900     900     10000    1700 .0041 0    - - error (invalid witness file) .53 .32 12   40 error (invalid witness file) 5.4 2.9 100 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .13  .12  1.1  23 .0041 0    false(no-overflow) 4.0  2.3  45   250 false(no-overflow) 10   5.3 89 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .12  .11  1.1  23 .0041 0    false(no-overflow) 3.4  1.9  64   240 false(no-overflow) 8.7 4.6 130 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .12  .12  .91 23 .0041 0    false(no-overflow) 3.7  2.1  50   240 false(no-overflow) 10   5.3 100 330 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .13  .12  .95 25 .0041 0    true 3.0  1.7  46   240 false(no-overflow) 8.2 4.4 120 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .096 .092 1.0  23 .0041 0    false(no-overflow) 3.5  2.0  61   230 false(no-overflow) 9.8 5.2 120 340 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .13  .12  .87 23 .0041 0    false(no-overflow) 4.0  2.3  45   240 false(no-overflow) 8.7 4.6 110 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) .13  .13  .78 23 .0041 0    timeout 93    77    1500   2700 false(no-overflow) 8.2 4.4 120 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .14  .13  .89 23 .0041 0    false(no-overflow) 3.7  2.0  65   240 false(no-overflow) 10   5.3 110 340 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_false-no-overflow.c false(no-overflow) 17     17     150    430 .0041 .29 timeout 93    82    1700   3600 timeout 92   54   970 7000 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .11  .10  .89 22 .0041 0    false(no-overflow) 4.0  2.3  42   230 false(no-overflow) 9.6 5.1 75 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .15  .14  .91 23 .0041 0    false(no-overflow) 3.2  1.8  60   240 false(no-overflow) 6.9 3.7 140 310 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .15  .15  .81 22 .0041 0    false(no-overflow) 4.1  2.3  47   240 false(no-overflow) 9.9 5.3 85 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .12  .11  .92 22 .0041 0    false(no-overflow) 3.8  2.2  55   240 false(no-overflow) 9.0 4.9 95 320 - -
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .13  .12  1.1  23 .0041 0    false(no-overflow) 4.3  2.4  45   240 false(no-overflow) 11   5.8 110 340 - -
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .16  .15  .91 23 .0041 0    false(no-overflow) 3.4  1.9  60   240 false(no-overflow) 9.7 5.1 100 310 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .15  .14  1.2  27 .0041 0    false(no-overflow) 3.2  1.8  70   230 false(no-overflow) 9.3 4.9 110 310 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .12  .11  .84 22 .0041 .16 false(no-overflow) 3.4  1.9  54   240 false(no-overflow) 8.3 4.4 100 320 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .12  .11  .83 23 .0041 0    false(no-overflow) 3.2  1.8  71   240 false(no-overflow) 8.3 4.4 130 320 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .12  .11  .94 23 .0041 0    true 3.2  1.8  60   240 false(no-overflow) 9.4 5.0 90 320 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .12  .11  1.1  23 .0041 0    true 3.7  2.1  55   240 false(no-overflow) 9.3 4.9 120 320 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .12  .12  1.0  23 .0041 0    false(no-overflow) 3.3  1.9  49   240 false(no-overflow) 9.4 5.0 90 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .11  .10  .87 22 .0041 0    false(no-overflow) 3.1  1.8  69   240 false(no-overflow) 9.4 5.0 110 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .12  .11  .89 22 .0041 0    false(no-overflow) 4.3  2.4  44   240 false(no-overflow) 8.6 4.6 100 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .12  .12  .86 22 .0041 .16 false(no-overflow) 3.5  2.0  60   250 false(no-overflow) 8.1 4.3 130 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .14  .13  .86 22 .0041 .17 false(no-overflow) 3.6  2.0  53   240 false(no-overflow) 7.7 4.1 110 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .12  .11  .89 22 .0041 0    false(no-overflow) 3.1  1.8  74   230 false(no-overflow) 8.3 4.5 100 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .12  .11  .80 22 .0041 0    false(no-overflow) 3.0  1.7  63   240 false(no-overflow) 8.8 4.6 93 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .10  .098 1.1  22 .0041 0    false(no-overflow) 4.0  2.2  44   240 false(no-overflow) 8.4 4.5 140 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .10  .096 .87 23 .0041 0    false(no-overflow) 3.2  1.8  46   240 false(no-overflow) 8.5 4.5 82 300 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .11  .11  .80 22 .0041 0    false(no-overflow) 4.1  2.3  42   240 false(no-overflow) 7.0 3.7 120 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .14  .13  .88 22 .0041 .17 false(no-overflow) 4.0  2.2  44   250 false(no-overflow) 8.2 4.5 110 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .15  .14  .96 23 .0041 0    false(no-overflow) 3.8  2.2  57   230 false(no-overflow) 8.7 4.6 110 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .10  .096 .86 22 .0041 0    false(no-overflow) 3.6  2.0  40   230 false(no-overflow) 8.9 4.7 95 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .12  .11  1.2  23 .0041 0    false(no-overflow) 3.7  2.1  59   240 false(no-overflow) 8.9 4.7 90 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .10  .096 .86 23 .0041 0    false(no-overflow) 4.2  2.3  49   240 false(no-overflow) 9.8 5.2 94 340 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .14  .13  .90 22 .0041 0    false(no-overflow) 3.7  2.1  56   240 false(no-overflow) 8.0 4.3 160 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .12  .12  .97 24 .0041 0    false(no-overflow) 3.1  1.8  62   240 false(no-overflow) 7.8 4.1 140 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .12  .11  .87 23 .0041 0    false(no-overflow) 3.7  2.1  40   230 false(no-overflow) 9.0 4.9 94 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .15  .14  .86 22 .0041 0    false(no-overflow) 4.1  2.3  47   240 false(no-overflow) 9.2 4.9 84 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .11  .11  .91 23 .0041 .17 false(no-overflow) 3.9  2.2  41   230 false(no-overflow) 7.7 4.1 130 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .11  .10  .91 24 .0041 0    false(no-overflow) 3.8  2.2  43   230 false(no-overflow) 7.3 3.9 95 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .10  .091 .88 22 .0041 0    false(no-overflow) 4.1  2.3  45   230 false(no-overflow) 7.9 4.2 110 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .11  .10  .92 22 .0041 0    false(no-overflow) 3.3  1.9  60   240 false(no-overflow) 8.6 4.6 89 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .12  .11  1.1  23 .0041 0    false(no-overflow) 3.2  1.8  64   240 false(no-overflow) 9.7 5.1 85 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .11  .11  .81 23 .0041 0    true 3.2  1.8  49   230 false(no-overflow) 8.6 4.6 140 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .10  .095 .85 22 .0041 0    false(no-overflow) 3.9  2.2  45   230 false(no-overflow) 7.8 4.1 100 300 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .13  .12  .81 22 .0041 0    false(no-overflow) 4.2  2.4  41   240 false(no-overflow) 8.6 4.5 120 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .099 .093 .96 22 .0041 0    false(no-overflow) 3.4  1.9  48   240 false(no-overflow) 9.7 5.1 98 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .14  .13  .79 22 .0041 0    true 3.1  1.7  47   240 false(no-overflow) 9.8 5.1 90 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .15  .14  .70 23 .0041 0    true 3.0  1.7  66   240 false(no-overflow) 8.5 4.5 130 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .13  .12  .91 23 .0041 0    false(no-overflow) 3.2  1.8  77   240 false(no-overflow) 8.3 4.5 110 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .13  .12  .88 25 .0041 0    false(no-overflow) 3.4  1.9  73   250 false(no-overflow) 9.4 5.1 91 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .11  .11  .88 22 .0041 .16 true 3.2  1.8  67   240 false(no-overflow) 8.3 4.5 99 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .14  .13  .80 23 .0041 0    true 3.2  1.8  62   230 false(no-overflow) 7.8 4.2 140 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .12  .11  1.1  23 .0041 .16 false(no-overflow) 3.9  2.2  46   240 false(no-overflow) 9.7 5.1 120 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .12  .11  .81 23 .0041 0    true 3.3  1.9  53   240 false(no-overflow) 8.0 4.3 120 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .15  .14  .85 23 .0041 0    true 3.4  1.9  54   240 false(no-overflow) 7.6 4.1 100 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .11  .10  .90 22 .0041 0    true 3.0  1.7  59   240 false(no-overflow) 9.0 4.8 120 330 - -
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .12  .11  .81 22 .0041 .16 false(no-overflow) 3.5  2.0  58   240 false(no-overflow) 8.3 4.5 110 320 - -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .12  .11  .84 22 .0041 .16 false(no-overflow) 3.2  1.8  61   240 false(no-overflow) 9.0 4.8 86 320 - -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .14  .13  .88 23 .0041 0    false(no-overflow) 3.5  2.0  59   240 false(no-overflow) 8.0 4.2 160 330 - -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .14  .13  .88 22 .0041 .16 false(no-overflow) 3.3  1.8  73   240 false(no-overflow) 7.9 4.2 120 320 - -
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .12  .12  1.0  24 .0041 0    false(no-overflow) 3.7  2.1  48   240 false(no-overflow) 8.6 4.6 120 310 - -
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .15  .15  .93 23 .0041 0    true 11    6.0  160   300 false(no-overflow) 12   6.3 120 340 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .15  .14  .88 23 .0041 0    false(no-overflow) 3.0  1.7  50   230 false(no-overflow) 10   5.4 88 330 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) .13  .12  .85 22 .0041 0    false(no-overflow) 3.2  1.9  60   230 false(no-overflow) 9.8 5.1 110 320 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .12  .11  .85 22 .0041 0    true 3.6  2.1  39   230 false(no-overflow) 9.5 5.1 85 320 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .12  .11  .88 23 .0041 0    false(no-overflow) 3.7  2.1  48   240 false(no-overflow) 9.5 5.1 78 320 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c error (5) .081 .080 .73 22 .0041 0    error (invalid witness file) .54 .35 9.7 39 error (invalid witness file) 6.8 3.6 87 300 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c error (5) .11  .10  .83 22 .0041 0    error (invalid witness file) .50 .32 9.9 39 error (invalid witness file) 8.5 4.5 94 340 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c error (5) .11  .11  .69 22 .0041 0    error (invalid witness file) .53 .34 13   42 error (invalid witness file) 7.0 3.7 81 300 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c error (5) .12  .12  .76 22 .0041 0    error (invalid witness file) .56 .35 13   41 error (invalid witness file) 6.8 3.6 77 300 - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .14  .14  .78 22 .0041 0    false(no-overflow) 3.6  2.0  60   240 false(no-overflow) 10   5.3 100 330 - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .11  .10  .93 22 .0041 0    false(no-overflow) 3.0  1.7  48   240 false(no-overflow) 9.0 4.8 110 330 - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .10  .095 1.2  22 .0041 0    false(no-overflow) 3.8  2.2  51   240 false(no-overflow) 8.8 4.7 83 310 - -
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .094 .088 1.2  22 .0041 0    false(no-overflow) 3.4  1.9  50   230 false(no-overflow) 8.4 4.5 90 310 - -
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .14  .14  .98 23 .0041 0    false(no-overflow) 3.9  2.2  47   240 false(no-overflow) 9.1 4.8 110 320 - -
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .11  .11  .85 22 .0041 0    false(no-overflow) 3.3  1.8  62   230 false(no-overflow) 9.5 5.0 89 320 - -
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .093 .087 .95 22 .0041 .17 true 3.3  1.9  50   230 false(no-overflow) 9.4 5.0 93 320 - -
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .11  .099 .86 23 .0041 0    false(no-overflow) 3.9  2.2  45   240 false(no-overflow) 9.0 4.7 110 310 - -
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .13  .13  .86 22 .0041 .17 false(no-overflow) 4.7  2.6  43   240 false(no-overflow) 9.1 4.8 120 330 - -
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .11  .11  1.0  23 .0041 0    false(no-overflow) 3.7  2.4  61   240 false(no-overflow) 9.0 4.8 76 320 - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_false-no-overflow.c false(no-overflow) 17     17     130    430 .0041 0    timeout 93    83    1800   2100 timeout 98   56   960 6400 - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .11  .099 .90 23 .0041 .16 false(no-overflow) 3.3  1.9  63   240 false(no-overflow) 9.1 4.8 120 320 - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) .11  .10  1.1  22 .0041 0    false(no-overflow) 4.2  2.4  48   240 false(no-overflow) 8.2 4.4 120 350 - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .14  .13  .82 22 .0041 0    false(no-overflow) 3.6  2.1  55   240 false(no-overflow) 9.5 5.0 94 320 - -
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .12  .11  1.1  23 .0041 0    true 3.8  2.1  43   240 false(no-overflow) 7.9 4.2 130 310 - -
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .10  .098 .91 22 .0041 0    false(no-overflow) 3.5  1.9  50   240 false(no-overflow) 7.1 3.9 130 320 - -
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) .12  .11  1.1  23 .0041 0    false(no-overflow) 4.5  2.5  50   250 true 10   5.3 120 330 - -
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .13  .12  .94 23 .0041 .16 false(no-overflow) 3.4  2.0  70   240 false(no-overflow) 7.8 4.2 90 310 - -
termination-crafted-lit/joey_false-no-overflow.c error (5) .085 .084 .73 22 .0041 0    error (invalid witness file) .52 .33 8.9 39 error (invalid witness file) 6.7 3.6 72 290 - -
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .13  .12  1.1  22 .0041 .16 true 3.3  1.8  60   240 false(no-overflow) 10   5.5 120 340 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     900     11000    1600 .0041 .10 - - error (invalid witness file) .49 .31 8.6 39 error (invalid witness file) 6.6 3.5 86 290
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true .10  .10  .70 22 .0041 0    - - true 4.6  2.6  79   280 true 9.5 5.1 120 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true .13  .13  .77 22 .0041 0    - - true 5.0  2.8  64   270 true 7.7 4.2 87 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 900     900     10000    1700 .0041 0    - - error (invalid witness file) .58 .38 11   40 error (invalid witness file) 8.2 4.3 84 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 900     900     5700    2800 .0041 0    - - error (invalid witness file) .52 .33 13   42 error (invalid witness file) 7.0 3.7 74 290
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 900     900     9100    470 .0041 0    - - error (invalid witness file) .52 .33 13   41 error (invalid witness file) 7.5 4.0 86 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 1.4   1.4   16    37 .0041 0    - - timeout 900    880    16000   3700 true 49   29   560 1900
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true .10  .10  1.1  22 .0041 0    - - true 5.4  3.0  59   280 true 10   5.4 120 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true .11  .11  .94 23 .0041 0    - - true 5.6  3.1  57   290 true 9.2 5.0 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true .13  .13  .83 22 .0041 0    - - true 3.8  2.2  53   280 true 8.5 4.6 100 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true .091 .089 .76 22 .0041 0    - - timeout 900    870    21000   4700 true 8.1 4.3 130 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true .11  .10  .80 25 .0041 .16 - - timeout 900    860    24000   4200 true 9.4 5.1 87 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true .19  .18  2.0  24 .0041 0    - - true 4.2  2.3  85   280 true 12   6.6 130 360
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 900     900     11000    2200 .0041 .13 - - error (invalid witness file) .66 .41 8.6 43 error (invalid witness file) 5.7 3.0 110 290
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout 900     900     6600    570 .0041 .20 - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.0 3.2 97 300
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout 900     900     8000    580 .0041 0    - - error (invalid witness file) .58 .38 9.6 40 error (invalid witness file) 7.3 3.8 77 300
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true .13  .13  .86 23 .0041 .17 - - true 4.8  2.6  74   270 true 12   6.2 130 350
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 900     900     13000    170 .0041 0    - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 5.7 3.1 110 300
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c true .22  .22  2.1  25 .0041 0    - - true 3.8  2.1  48   280 true 31   17   530 620
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true .13  .13  .81 22 .0041 .16 - - true 4.9  2.8  59   270 true 9.2 4.9 140 330
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 900     900     12000    1700 .0041 0    - - error (invalid witness file) .54 .34 9.7 43 error (invalid witness file) 6.4 3.3 110 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 900     900     10000    480 .0041 .13 - - error (invalid witness file) .53 .34 13   42 error (invalid witness file) 7.3 3.8 75 290
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 1.4   1.4   16    37 .0041 0    - - timeout 900    880    20000   4100 true 62   36   520 2200
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true .13  .12  .72 22 .0041 0    - - true 4.2  2.4  72   280 true 6.6 3.5 130 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true .12  .12  .84 23 .0041 0    - - false(no-overflow) 5.1  2.8  45   280 true 7.3 3.9 150 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true .096 .092 1.0  22 .0041 0    - - true 4.6  2.6  61   270 true 7.3 4.0 130 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true .13  .13  .72 23 .0041 0    - - true 5.0  2.7  60   280 true 9.0 4.8 82 320
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true .13  .13  .83 22 .0041 .12 - - true 5.3  3.0  61   280 true 8.4 4.5 120 320
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true .13  .13  .81 23 .0041 0    - - true 6.4  3.5  78   280 true 9.7 5.1 100 320
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true .090 .088 .90 22 .0041 .16 - - false(no-overflow) 4.4  2.5  64   280 true 9.3 5.1 110 350
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true .10  .097 .82 22 .0041 .16 - - true 4.1  2.3  56   290 true 11   5.7 120 350
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true .10  .095 .78 22 .0041 0    - - false(no-overflow) 4.4  2.5  53   280 true 8.8 4.8 100 330
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 6.4   6.4   70    96 .0041 0    - - true 6.5  3.5  71   300 true 140   90   1500 3500
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     900     9000    2600 .0041 .20 - - error (invalid witness file) .53 .34 12   39 error (invalid witness file) 7.1 3.7 81 310
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true .13  .12  .66 22 .0041 0    - - true 4.6  2.5  73   280 true 9.3 5.0 110 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c true .26  .26  2.8  26 .0041 0    - - true 4.4  2.5  61   280 true 24   14   250 560
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true .13  .12  .64 22 .0041 0    - - true 4.0  2.2  50   270 true 7.9 4.2 130 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c true .14  .13  1.1  23 .0041 0    - - true 4.7  2.7  40   270 true 14   7.3 150 370
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true .10  .098 .84 22 .0041 0    - - true 4.0  2.3  77   280 true 9.3 4.9 100 320
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 900     900     9500    2500 .0041 .31 - - error (invalid witness file) .67 .41 7.7 40 error (invalid witness file) 6.6 3.5 110 300
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true .086 .083 .96 22 .0041 0    - - true 4.0  2.3  52   280 true 8.2 4.4 110 320
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c true .095 .092 1.1  22 .0041 0    - - false(no-overflow) 4.5  2.5  46   280 true 10   5.4 97 330
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 900     900     13000    450 .0041 .20 - - error (invalid witness file) .50 .31 10   40 error (invalid witness file) 5.6 3.0 91 300
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c error (5) .092 .088 .94 22 .0041 0    - - error (invalid witness file) .59 .38 7.1 41 error (invalid witness file) 8.9 4.6 94 330
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c error (5) .11  .11  .70 22 .0041 0    - - error (invalid witness file) .62 .39 8.9 41 error (invalid witness file) 6.9 3.7 89 300
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true .13  .12  .93 23 .0041 0    - - true 5.2  2.9  57   270 true 9.3 5.0 130 310
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true .12  .12  .76 22 .0041 0    - - true 5.7  3.1  71   280 true 8.0 4.2 160 320
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true .097 .096 .69 22 .0041 0    - - true 5.0  2.7  55   270 true 9.8 5.2 94 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true .11  .10  .90 22 .0041 0    - - true 3.9  2.2  61   280 true 7.1 3.8 120 310
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true .095 .091 .94 22 .0041 0    - - true 4.0  2.2  70   280 true 11   5.8 120 340
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true .13  .13  .69 22 .0041 0    - - true 4.2  2.3  67   280 true 9.8 5.2 99 320
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true .11  .11  .88 22 .0041 .12 - - true 4.1  2.3  56   270 true 7.7 4.1 140 320
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true .096 .093 .78 22 .0041 0    - - out of memory 600    570    10000   7000 true 7.8 4.3 150 320
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true .12  .12  .71 23 .0041 0    - - out of memory 420    400    7300   7000 true 9.8 5.2 120 320
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true .14  .13  .73 23 .0041 0    - - true 6.5  3.6  69   280 true 8.3 4.5 100 320
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c true .13  .13  .84 22 .0041 0    - - true 5.2  2.9  49   280 true 7.5 4.0 130 320
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 3.4   3.4   40    78 .0041 0    - - true 6.4  3.5  73   300 timeout 960   800   14000 4800
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true .090 .089 .84 22 .0041 0    - - true 5.2  2.9  98   290 true 9.4 5.1 130 320
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c true .14  .13  .83 23 .0041 0    - - false(no-overflow) 6.0  3.3  76   320 true 8.7 4.7 140 320
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c true .11  .10  .96 22 .0041 0    - - false(no-overflow) 4.8  2.7  63   280 true 7.8 4.3 120 330
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true .11  .11  .79 23 .0041 0    - - true 7.9  4.3  70   310 true 12   6.2 110 330
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c true .12  .11  .79 23 .0041 0    - - false(no-overflow) 5.8  3.3  73   310 true 8.0 4.3 130 320
termination-crafted-lit/genady_true-termination_true-no-overflow.c true .20  .20  2.4  24 .0041 0    - - true 4.7  2.6  62   270 timeout 960   810   20000 2800
termination-crafted-lit/strchr_true-no-overflow.c true .11  .10  .78 22 .0041 0    - - true 4.9  2.7  86   280 true 9.8 5.3 110 330
termination-numeric/Addition01_false-no-overflow.c error (5) .12  .12  .72 22 .0041 0    error (invalid witness file) .65 .43 8.0 40 error (invalid witness file) 6.8 3.6 88 290 - -
termination-numeric/Avg_true_false-no-overflow.c error (5) .094 .093 .82 22 .0041 0    error (invalid witness file) .55 .34 15   40 error (invalid witness file) 5.8 3.1 110 300 - -
termination-numeric/Binomial_true-termination_false-no-overflow.c error (5) .092 .090 .68 22 .0041 0    error (invalid witness file) .53 .34 12   42 error (invalid witness file) 6.3 3.4 87 290 - -
termination-numeric/Et1_true_false-no-overflow.c error (5) .10  .10  .71 22 .0041 0    error (invalid witness file) .57 .36 14   44 error (invalid witness file) 7.2 3.8 61 300 - -
termination-numeric/Et2_true_false-no-overflow.c error (5) .12  .11  .74 22 .0041 0    error (invalid witness file) .51 .33 13   43 error (invalid witness file) 5.7 3.0 120 300 - -
termination-numeric/Et3_true_false-no-overflow.c error (5) .10  .10  .71 22 .0041 0    error (invalid witness file) .52 .32 9.1 40 error (invalid witness file) 6.5 3.4 92 300 - -
termination-numeric/Et4_true_false-no-overflow.c error (5) .098 .095 .85 22 .0041 0    error (invalid witness file) .62 .40 9.4 42 error (invalid witness file) 5.6 3.0 91 290 - -
termination-numeric/MultCommutative_false-no-overflow.c error (5) .12  .12  .62 22 .0041 0    error (invalid witness file) .62 .39 8.2 39 error (invalid witness file) 6.8 3.6 100 300 - -
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c error (5) .083 .084 .73 22 .0041 0    error (invalid witness file) .64 .41 7.9 40 error (invalid witness file) 7.3 3.9 76 300 - -
termination-numeric/Ackermann01_true-termination_true-no-overflow.c error (5) .12  .12  .77 22 .0041 0    - - error (invalid witness file) .48 .32 12   39 error (invalid witness file) 7.7 4.0 84 290
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c error (5) .11  .10  .85 22 .0041 0    - - error (invalid witness file) .58 .37 9.5 40 error (invalid witness file) 7.5 3.9 97 300
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c error (5) .096 .093 .80 22 .0041 0    - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 7.3 3.8 110 310
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c error (5) .082 .081 .82 22 .0041 0    - - error (invalid witness file) .67 .43 8.2 40 error (invalid witness file) 7.1 3.8 75 290
termination-numeric/LogRecursive_true-termination_true-no-overflow.c error (5) .12  .11  .72 22 .0041 0    - - error (invalid witness file) .65 .42 7.8 40 error (invalid witness file) 7.0 3.7 91 300
termination-numeric/Parts_true-termination_true-no-overflow.c error (5) .094 .092 .77 22 .0041 0    - - error (invalid witness file) .65 .41 8.1 41 error (invalid witness file) 6.5 3.5 92 300
termination-numeric/TwoWay_true-termination_true-no-overflow.c error (5) .11  .11  .79 22 .0041 0    - - error (invalid witness file) .56 .36 10   40 error (invalid witness file) 6.2 3.3 110 300
termination-numeric/gcd01_true-termination_true-no-overflow.c error (5) .099 .097 .78 22 .0041 0    - - error (invalid witness file) .51 .32 11   41 error (invalid witness file) 7.2 3.8 82 300
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true .60  .60  6.2  34 .0041 0    - - true 5.4  3.0  69   290 true 67   40   720 1100
termination-numeric/recHanoi02_true-termination_true-no-overflow.c error (5) .081 .080 .73 22 .0041 0    - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 7.8 4.1 84 300
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (5) .099 .095 .75 22 .0041 0    - - error (invalid witness file) .53 .34 8.5 40 error (invalid witness file) 7.9 4.1 78 300
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (5) .097 .092 .74 22 .0041 0    - - error (invalid witness file) .57 .37 9.3 40 error (invalid witness file) 6.7 3.5 100 300
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 900     900     10000    24 .0041 0    - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 6.5 3.4 83 300
recursive/Addition02WithOverflowBug_false-no-overflow.c error (5) .096 .092 .87 22 .0041 0    error (invalid witness file) .55 .35 13   42 error (invalid witness file) 6.5 3.4 91 300 - -
recursive/Addition03_false-no-overflow.c error (5) .13  .12  .73 22 .0041 0    error (invalid witness file) .50 .31 8.2 40 error (invalid witness file) 7.4 3.9 62 300 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c error (5) .11  .10  .84 22 .0041 0    error (invalid witness file) .61 .38 11   45 error (invalid witness file) 6.5 3.4 88 300 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (5) .094 .092 .71 22 .0041 0    - - error (invalid witness file) .54 .34 14   40 error (invalid witness file) 6.7 3.5 140 320
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (5) .094 .093 .64 22 .0041 0    - - error (invalid witness file) .52 .33 10   42 error (invalid witness file) 5.2 2.8 84 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (5) .12  .12  .78 22 .0041 0    - - error (invalid witness file) .58 .36 9.3 39 error (invalid witness file) 6.4 3.4 97 310
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (5) .095 .091 .77 22 .0041 0    - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.0 3.3 110 290
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (5) .12  .12  .70 22 .0041 0    - - error (invalid witness file) .52 .32 12   40 error (invalid witness file) 5.8 3.1 100 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (5) .11  .11  .89 22 .0041 0    - - error (invalid witness file) .59 .37 11   41 error (invalid witness file) 6.5 3.4 120 320
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (5) .081 .080 .81 22 .0041 0    - - error (invalid witness file) .67 .42 7.2 40 error (invalid witness file) 6.0 3.1 66 300
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c error (5) .089 .086 .90 22 .0041 0    - - error (invalid witness file) .65 .41 7.4 41 error (invalid witness file) 8.1 4.2 76 300
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (5) .11  .10  .83 22 .0041 0    - - error (invalid witness file) .51 .32 9.3 41 error (invalid witness file) 6.3 3.3 93 310
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (5) .098 .097 .87 22 .0041 0    - - error (invalid witness file) .52 .34 10   40 error (invalid witness file) 5.9 3.2 95 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (5) .10  .097 .76 22 .0041 0    - - error (invalid witness file) .66 .41 7.9 40 error (invalid witness file) 6.9 3.7 110 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c error (5) .11  .10  .76 22 .0041 0    - - error (invalid witness file) .69 .44 8.2 44 error (invalid witness file) 6.0 3.2 110 300
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (5) .10  .098 .75 22 .0041 0    - - error (invalid witness file) .56 .36 8.9 39 error (invalid witness file) 5.6 3.0 120 290
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (5) .10  .10  .97 22 .0041 0    - - error (invalid witness file) .58 .37 9.6 39 error (invalid witness file) 7.4 3.9 86 300
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (5) .094 .090 1.0  22 .0041 0    - - error (invalid witness file) .65 .42 7.3 42 error (invalid witness file) 8.6 4.5 74 310
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (5) .084 .084 .68 22 .0041 0    - - error (invalid witness file) .50 .34 10   41 error (invalid witness file) 5.7 3.1 110 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (5) .11  .11  .67 22 .0041 0    - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 7.9 4.1 90 290
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (5) .097 .097 .85 22 .0041 0    - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.6 3.5 91 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (5) .13  .12  .63 22 .0041 0    - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.9 3.7 92 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (5) .084 .081 1.0  22 .0041 0    - - error (invalid witness file) .51 .33 10   39 error (invalid witness file) 6.8 3.6 95 310
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (5) .095 .092 .92 22 .0041 0    - - error (invalid witness file) .53 .34 9.9 39 error (invalid witness file) 7.6 4.0 71 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (5) .12  .11  .67 22 .0041 0    - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 7.9 4.1 74 300
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c error (5) .12  .12  .72 22 .0041 0    - - error (invalid witness file) .67 .43 8.4 40 error (invalid witness file) 5.7 3.1 110 300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c error (5) .098 .095 .77 22 .0041 0    - - error (invalid witness file) .52 .33 10   40 error (invalid witness file) 7.2 3.8 81 300
bitvector/jain_1_false-no-overflow.i false(no-overflow) .095 .091 .86 22 0      0    false(no-overflow) 3.7  2.1  52   240 false(no-overflow) 9.4 5.0 100 340 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) .11  .10  .88 23 0      0    true 3.2  1.8  53   240 false(no-overflow) 7.8 4.2 110 310 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) .10  .10  .93 23 0      0    true 4.2  2.3  43   240 false(no-overflow) 9.9 5.2 110 330 - -
bitvector/jain_5_false-no-overflow.i timeout 900     900     8800    1300 0      0    error (invalid witness file) .51 .33 11   42 error (invalid witness file) 7.6 4.0 66 300 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) .12  .11  1.1  26 0      .16 false(no-overflow) 3.1  1.8  77   240 false(no-overflow) 7.6 4.0 130 310 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) .11  .11  1.0  24 0      0    true 3.7  2.1  51   240 false(no-overflow) 9.4 5.0 100 320 - -
bitvector/modulus_false-no-overflow.i false(no-overflow) .12  .11  1.0  25 0      0    false(no-overflow) 3.7  2.1  65   240 error (1) 9.8 5.1 120 330 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true .14  .13  .94 24 0      0    - - true 14    7.5  120   340 true 8.3 4.5 110 320
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true .14  .13  .93 23 0      0    - - true 11    6.0  190   450 true 7.9 4.3 130 320
bitvector/byte_add_false-unreach-call_true-no-overflow.i true .13  .13  .92 23 0      0    - - true 20    10    300   650 true 9.1 4.9 110 330
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .12  .11  1.1  24 0      0    - - true 5.5  3.1  69   310 true 11   5.9 110 330
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true .10  .098 .97 23 0      0    - - true 6.1  3.5  73   300 true 10   5.6 98 310
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true .10  .098 .96 23 0      0    - - true 6.4  3.6  51   300 true 9.6 5.1 100 330
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 1.2   1.2   14    39 0      0    - - true 5.4  3.0  75   280 true 15   8.3 150 440
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .13  .13  .85 24 0      0    - - true 6.3  3.4  64   290 true 7.3 4.0 120 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i true .11  .11  .68 22 0      0    - - true 5.6  3.1  47   300 true 7.2 3.8 120 310
bitvector/jain_2_true-unreach-call_true-no-overflow.i true .088 .084 .72 22 0      0    - - true 5.5  3.0  58   280 true 7.2 3.8 110 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i true .11  .11  .73 22 0      0    - - true 4.3  2.4  44   280 true 7.9 4.1 150 330
bitvector/jain_5_true-unreach-call_true-no-overflow.i true .083 .082 .78 22 0      .16 - - true 4.5  2.5  58   270 true 8.7 4.6 68 310
bitvector/jain_6_true-unreach-call_true-no-overflow.i true .10  .098 .74 23 0      0    - - true 5.8  3.2  48   280 true 7.7 4.1 120 320
bitvector/jain_7_true-unreach-call_true-no-overflow.i true .12  .11  .82 22 0      0    - - true 5.2  2.9  81   280 true 8.2 4.3 110 320
bitvector/modulus_true-unreach-call_true-no-overflow.i true .13  .12  .92 24 0      0    - - true 5.3  2.9  65   290 error (1) 7.2 3.9 91 330
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .089 .086 .94 22 0      0    - - true 5.7  3.1  60   300 true 9.3 4.9 110 320
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .098 .093 .89 22 0      0    - - true 4.6  2.5  66   280 true 8.8 4.7 99 320
bitvector/parity_true-unreach-call_true-no-overflow.i true .097 .092 .86 23 0      0    - - true 5.6  3.0  77   280 true 10   5.3 91 330
bitvector/sum02_false-unreach-call_true-no-overflow.i true .081 .080 .84 23 0      0    - - true 5.5  3.0  71   270 true 8.6 4.6 81 300
bitvector/sum02_true-unreach-call_true-no-overflow.i true .11  .11  .91 24 0      .16 - - true 6.1  3.4  66   280 true 7.5 4.0 130 320
../../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 21000 21000 220000 47000 1.2    7.9  328 800 540 13000 42000   328 1600 890 20000 72000   328 6800 6400 140000 78000   328 5400 4100 88000 74000  
    correct results 233 48 47 440 5700 .80   6.2  137 600 360 9200 36000   136 1300 690 16000 51000   88 6000 5600 120000 61000   92 3100 2200 48000 46000  
        correct true 95 30 30 310 2500 .30   2.3  27 0 0 0 0   1 0 0 0 0   79 6000 5600 120000 61000   92 3100 2200 48000 46000  
        correct false 138 18 17 140 3200 .50   3.9  110 600 360 9200 36000   135 1300 690 16000 51000   9 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 4 45 45 400 1200 .016  .29 0 190 170 3600 5800   0 190 110 1900 13000   0 810 770 16000 14000   0 1900 1600 35000 8800  
        correct-unconfirmed true 2 11 11 120 370 .0082 0    0 0 0 0 0   0 0 0 0 0   0 810 770 16000 14000   0 1900 1600 35000 8800  
        correct-unconfirmed false 2 34 34 290 860 .0082 .29 0 190 170 3600 5800   0 190 110 1900 13000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (328 tasks, max score: 491) 330
Run set [sv-comp17.Overflows-BitVectors; sv-comp17.Overflows-Other]