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
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 score witness inspect witness 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) 0 wit inspect 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) 1 wit inspect 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) 1 wit inspect 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) 0 wit inspect 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) 0 wit inspect 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) 1 wit inspect 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) 1 wit inspect 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) 1 wit inspect 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) 1 wit inspect 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) 1 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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) -16 wit inspect 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 0 wit inspect 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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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 0 wit inspect 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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 0 wit inspect 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) 1 wit inspect .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) 1 wit inspect .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 0 wit inspect 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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 0 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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)) 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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)) 0 wit inspect 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)) 0 wit inspect 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)) 0 wit inspect 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)) 0 wit inspect 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)) 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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) 0 wit inspect .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) 0 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 0 wit inspect 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) 1 wit inspect .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) 0 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 0 wit inspect .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) 0 wit inspect 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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 0 wit inspect 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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 0 wit inspect .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) 0 wit inspect .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)) 0 wit inspect 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) 1 wit inspect .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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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) -16 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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) 0 wit inspect 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) 1 wit inspect .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) 0 wit inspect .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) 1 wit inspect .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) 1 wit inspect .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 0 wit inspect 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) 0 wit inspect 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)) 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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 0 wit inspect 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)) 0 wit inspect 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
../../sv-benchmarks/c/ verifier status score witness inspect witness 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 274 102 26000 25000 310000 270000 7000   .21 274 340 190 6900 22000   274 1500 840 22000 74000   274 270   160   5600 20000   274 10000 8500   180000 91000  
    correct results 134 134 91 91 970 12000 210   0    0 290 170 6000 19000   134 1000 540 17000 43000   0 0   0   0 0   0 0 0   0 0  
        correct true 0
        correct false 134 134 91 91 970 12000 210   0    0 290 170 6000 19000   134 1000 540 17000 43000   0 0   0   0 0   0 0 0   0 0  
    correct-unconfimed results 17 0 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 0 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 -32 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 -32 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 (274 tasks, max score: 393) 102
Run set sv-comp17.Overflows-BitVectors