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