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