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