Tool CPAchecker 1.6.1-svn 24048
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 07:44:08 CET [[ 2017-01-15 00:24:53 CET ]] [[ 2017-01-15 00:50:42 CET ]] [[ 2017-01-15 00:30:44 CET ]] [[ 2017-01-15 00:56:39 CET ]]
Run set sv-comp17.Overflows-BitVectors
Options -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0744.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) 1 wit inspect 3.2 1.2  27 270 0      0   false(no-overflow) 4.0 2.2 73 250 false(no-overflow) 6.9 3.6 83 310 - -
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.0 1.2  23 250 0      0   false(no-overflow) 4.0 2.2 72 240 false(no-overflow) 6.9 3.7 120 320 - -
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 1 wit inspect 2.9 1.2  28 270 0      0   false(no-overflow) 3.9 2.2 60 260 false(no-overflow) 6.9 3.7 86 320 - -
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 1 wit inspect 2.9 1.1  25 270 0      0   false(no-overflow) 4.3 2.3 65 260 false(no-overflow) 6.8 3.6 95 300 - -
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.0 1.2  29 260 0      0   false(no-overflow) 3.9 2.2 65 250 false(no-overflow) 6.6 3.6 120 310 - -
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 2.9 1.1  25 260 0      0   false(no-overflow) 4.1 2.3 65 260 false(no-overflow) 7.2 3.9 130 320 - -
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.0 1.2  24 270 0      0   false(no-overflow) 3.8 2.1 55 260 false(no-overflow) 7.1 3.8 140 320 - -
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.0 1.2  28 260 0      0   false(no-overflow) 4.0 2.2 67 240 false(no-overflow) 6.7 3.6 100 310 - -
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 2.9 1.2  25 260 0      0   false(no-overflow) 3.9 2.2 73 250 false(no-overflow) 8.2 4.3 96 340 - -
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.0 1.2  26 260 0      0   false(no-overflow) 3.9 2.2 58 240 false(no-overflow) 7.3 3.9 92 320 - -
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow.c.i true 2 wit inspect 2.8 1.1  23 260 0      0   - - true 4.0  2.2  58 260 true 6.9 3.7 130 310
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow.c.i true 2 wit inspect 2.7 1.1  26 250 0      0   - - true 4.2  2.3  83 270 true 7.4 3.9 140 320
signedintegeroverflow-regression/Multiplication_true-no-overflow.c.i true 2 wit inspect 2.9 1.2  26 250 0      0   - - true 3.9  2.2  64 250 true 7.0 3.8 140 310
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow.c.i true 2 wit inspect 2.9 1.1  24 260 0      0   - - true 3.8  2.1  67 250 true 6.9 3.7 130 310
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow.c.i true 2 wit inspect 2.9 1.1  24 260 0      0   - - true 3.9  2.2  65 270 true 7.5 4.0 130 310
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  21 250 0      0   false(no-overflow) 3.1 1.8 57 240 false(no-overflow) 6.8 3.7 110 320 - -
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  19 250 0      0   false(no-overflow) 3.2 1.8 57 240 false(no-overflow) 7.0 3.7 140 310 - -
termination-crafted/Ackermann_false-no-overflow.c error (recursion) 0 wit inspect 2.4 1.0  24 240 0      0   error (recursion) 3.3 1.9 60 240 false(no-overflow) 6.7 3.6 100 310 - -
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  22 250 0      0   true 2.9 1.6 46 240 false(no-overflow) 6.8 3.6 97 310 - -
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  24 260 0      0   true 2.9 1.6 47 230 false(no-overflow) 7.2 3.8 150 320 - -
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  19 250 0      0   false(no-overflow) 3.3 1.8 55 240 false(no-overflow) 7.2 3.8 140 310 - -
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  19 250 0      0   false(no-overflow) 3.4 1.9 72 240 false(no-overflow) 7.1 3.8 88 320 - -
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect 2.9 1.2  24 270 0      0   true 3.3 1.8 59 250 false(no-overflow) 8.3 4.3 170 330 - -
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  24 250 0      0   true 2.9 1.6 42 240 false(no-overflow) 6.7 3.7 87 310 - -
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  22 250 .0082 0   true 3.3 1.9 73 240 false(no-overflow) 7.6 4.1 140 320 - -
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  22 260 .0082 0   false(no-overflow) 3.1 1.8 49 240 false(no-overflow) 7.3 3.9 85 330 - -
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  24 260 .0082 0   false(no-overflow) 3.2 1.8 50 230 false(no-overflow) 7.5 4.0 150 310 - -
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  20 240 0      0   false(no-overflow) 3.1 1.8 49 240 false(no-overflow) 6.6 3.5 80 310 - -
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  20 240 0      0   false(no-overflow) 3.5 2.0 65 250 false(no-overflow) 7.2 3.8 130 320 - -
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  20 250 0      0   false(no-overflow) 3.2 1.8 53 240 false(no-overflow) 6.7 3.6 79 310 - -
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  24 260 0      0   false(no-overflow) 3.3 1.8 64 240 false(no-overflow) 7.2 3.8 82 320 - -
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  23 260 .0082 0   false(no-overflow) 3.3 1.8 54 230 false(no-overflow) 7.1 3.8 100 310 - -
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  23 260 0      0   false(no-overflow) 3.4 1.9 53 240 false(no-overflow) 7.6 4.1 150 330 - -
termination-crafted/NestedRecursion_2a_false-no-overflow.c error (recursion) 0 wit inspect 2.4 1.0  20 250 0      0   false(no-overflow) 3.4 1.9 57 250 false(no-overflow) 7.6 4.1 150 320 - -
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  21 250 0      0   true 2.9 1.7 58 240 false(no-overflow) 6.6 3.5 79 310 - -
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  21 250 .0082 0   false(no-overflow) 3.0 1.7 41 240 false(no-overflow) 6.9 3.7 110 320 - -
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 1 wit inspect 3.8 1.4  30 270 0      0   true 3.7 2.1 40 250 false(no-overflow) 7.6 4.1 95 310 - -
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  21 250 0      0   true 2.9 1.7 33 240 false(no-overflow) 7.7 4.0 140 330 - -
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  19 250 0      0   true 2.9 1.6 65 240 false(no-overflow) 6.9 3.7 110 320 - -
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 0 wit inspect 900   850    12000 760 0      0   true 3.7 2.1 62 280 timeout 97   62   810 1600 - -
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  20 260 0      0   true 3.1 1.8 54 250 false(no-overflow) 6.7 3.6 110 320 - -
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  22 250 0      0   true 2.9 1.7 40 240 false(no-overflow) 6.8 3.6 86 320 - -
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 1.2  24 260 .025  0   true 2.9 1.7 55 230 false(no-overflow) 7.6 4.0 150 330 - -
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  22 250 0      0   true 3.2 1.8 69 250 false(no-overflow) 6.6 3.6 88 310 - -
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  24 260 0      0   false(no-overflow) 3.1 1.8 46 240 false(no-overflow) 7.7 4.1 130 320 - -
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  22 260 .0082 0   false(no-overflow) 3.6 2.0 78 250 false(no-overflow) 7.1 3.8 130 320 - -
termination-crafted/RecursiveMultiplication_false-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  19 250 0      0   error (recursion) 3.3 1.9 54 250 false(no-overflow) 7.5 4.0 110 330 - -
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  24 240 0      0   false(no-overflow) 3.2 1.8 61 250 false(no-overflow) 7.3 3.8 110 320 - -
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  19 240 0      0   false(no-overflow) 3.0 1.7 50 240 false(no-overflow) 6.6 3.6 100 310 - -
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.0  23 250 .0082 0   false(no-overflow) 3.1 1.8 46 240 false(no-overflow) 7.0 3.7 86 330 - -
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  20 250 .0082 0   false(no-overflow) 3.1 1.8 55 230 false(no-overflow) 7.5 4.0 120 320 - -
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  25 260 .0082 0   false(no-overflow) 3.3 1.9 57 230 false(no-overflow) 7.1 3.8 120 320 - -
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  23 260 .0082 0   false(no-overflow) 3.1 1.8 50 240 false(no-overflow) 7.1 3.8 120 320 - -
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  21 260 0      0   true 3.0 1.7 66 230 false(no-overflow) 7.1 3.8 100 310 - -
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  19 250 0      0   false(no-overflow) 3.2 1.9 58 240 false(no-overflow) 7.3 3.9 120 320 - -
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  21 260 .0082 0   true 3.4 1.9 54 250 false(no-overflow) 7.3 3.9 120 310 - -
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 1.2  27 270 .012  0   true 3.6 2.1 62 250 false(no-overflow) 9.3 5.0 120 350 - -
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 1.1  22 280 .0082 0   true 3.1 1.8 50 250 false(no-overflow) 7.9 4.2 110 330 - -
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 1.1  24 270 .0082 0   false(no-overflow) 3.2 1.8 53 240 false(no-overflow) 8.3 4.3 140 330 - -
termination-crafted/4BitCounterPointer_true-no-overflow.c timeout 0 wit inspect 910   880    8900 8900 0      0   - - true 4.5  2.5  96 280 true 7.0 3.8 140 310
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow.c error 0 wit inspect 2.4 1.1  23 260 0      0   - - out of memory 250    230    3000 7000 timeout 960   800   12000 4600
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow.c error 0 wit inspect 2.3 1.0  22 240 0      0   - - false(no-overflow) 3.9  2.2  84 290 true 9.2 4.8 160 330
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow.c error 0 wit inspect 2.5 1.0  22 250 0      0   - - timeout 900    860    13000 5100 true 8.8 4.7 140 330
termination-crafted/Bangalore_true-no-overflow.c timeout 0 wit inspect 900   890    9800 2400 0      0   - - true 3.8  2.2  73 280 true 8.5 4.5 150 330
termination-crafted/Bangalore_v2_true-no-overflow.c false(no-overflow) -16 wit inspect 2.5 1.1  23 250 0      0   - - true 2.9  1.7  50 230 true 8.4 4.5 150 310
termination-crafted/Bangalore_v4_true-no-overflow.c false(no-overflow) -16 wit inspect 2.6 1.1  22 260 0      0   - - true 2.9  1.7  30 240 true 8.1 4.4 160 320
termination-crafted/Benghazi_true-no-overflow.c timeout 0 wit inspect 900   850    12000 5700 0      0   - - true 4.0  2.3  88 280 true 89   56   780 1200
termination-crafted/Cairo_step2_true-no-overflow.c timeout 0 wit inspect 900   860    12000 4200 0      0   - - true 3.9  2.2  90 280 timeout 960   810   13000 4000
termination-crafted/Cairo_true-no-overflow.c timeout 0 wit inspect 900   850    11000 3200 0      0   - - true 3.8  2.2  86 280 true 7.7 4.1 140 330
termination-crafted/Copenhagen_true-no-overflow.c timeout 0 wit inspect 910   860    10000 8700 0      0   - - true 4.0  2.2  66 280 true 8.6 4.6 160 330
termination-crafted/Division_true-no-overflow.c timeout 0 wit inspect 900   890    11000 2400 0      0   - - true 3.9  2.2  66 280 true 7.0 3.8 130 320
termination-crafted/LexIndexValue-Array_true-no-overflow.c error 0 wit inspect 2.5 1.0  20 260 0      0   - - out of memory 500    470    5200 7000 timeout 960   790   11000 4800
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c false(no-overflow) -16 wit inspect 2.5 1.1  22 250 0      0   - - timeout 900    880    21000 3700 true 9.2 4.9 150 350
termination-crafted/Madrid_true-no-overflow.c timeout 0 wit inspect 900   860    12000 1900 0      0   - - true 3.5  2.0  58 280 true 6.9 3.7 130 310
termination-crafted/McCarthy91_Iteration_true-no-overflow.c timeout 0 wit inspect 900   850    12000 4800 0      0   - - true 4.1  2.3  89 280 timeout 960   850   11000 4600
termination-crafted/McCarthy91_Recursion_true-no-overflow.c error (recursion) 0 wit inspect 2.5 1.0  23 250 0      0   - - error (recursion) 3.4  1.9  53 250 true 9.4 5.1 170 340
termination-crafted/MenloPark_true-no-overflow.c timeout 0 wit inspect 910   860    12000 8900 0      0   - - error (invalid witness file) .55 .35 11 44 error (invalid witness file) 7.4 3.8 140 330
termination-crafted/MutualRecursion_1a_true-no-overflow.c error (recursion) 0 wit inspect 2.5 1.0  23 250 0      0   - - error (recursion) 3.5  2.0  67 240 true 12   6.9 210 390
termination-crafted/MutualRecursion_1b_true-no-overflow.c error (recursion) 0 wit inspect 2.5 1.1  23 260 0      0   - - error (recursion) 3.5  1.9  46 260 true 19   11   290 580
termination-crafted/NestedRecursion_1b_true-no-overflow.c error (recursion) 0 wit inspect 2.4 1.0  22 250 0      0   - - error (recursion) 3.5  1.9  59 260 true 18   9.7 310 530
termination-crafted/NestedRecursion_1c_true-no-overflow.c error (recursion) 0 wit inspect 2.3 .99 19 240 0      0   - - error (recursion) 3.4  1.9  57 250 true 15   8.0 200 400
termination-crafted/NestedRecursion_1d_true-no-overflow.c error (recursion) 0 wit inspect 2.4 1.0  23 250 0      0   - - error (recursion) 3.4  1.9  58 250 true 18   9.7 310 580
termination-crafted/NestedRecursion_2b_true-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  19 250 0      0   - - error (recursion) 3.2  1.8  59 240 timeout 960   800   13000 4000
termination-crafted/NestedRecursion_2c_true-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  19 250 0      0   - - error (recursion) 3.3  1.9  63 240 timeout 960   800   12000 4000
termination-crafted/NonTermination3_true-no-overflow.c error 0 wit inspect 2.4 1.0  21 240 0      0   - - true 4.0  2.3  66 280 true 6.5 3.5 120 310
termination-crafted/NonTerminationSimple7_true-no-overflow.c timeout 0 wit inspect 900   850    13000 780 0      0   - - true 3.9  2.2  73 300 true 7.9 4.2 130 330
termination-crafted/Nyala-2lex_true-no-overflow.c timeout 0 wit inspect 910   890    8800 11000 0      0   - - true 4.3  2.4  95 270 true 7.8 4.1 140 320
termination-crafted/Parallel_true-no-overflow.c timeout 0 wit inspect 900   870    12000 4000 0      0   - - true 4.2  2.4  67 280 true 7.4 4.0 160 320
termination-crafted/Piecewise_true-no-overflow.c timeout 0 wit inspect 900   890    11000 1500 0      0   - - true 4.8  2.6  77 280 true 8.1 4.3 150 320
termination-crafted/SyntaxSupportPointer01_true-no-overflow.c timeout 0 wit inspect 910   870    9900 11000 0      0   - - true 3.9  2.2  61 300 true 8.5 4.6 160 330
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow.c timeout 0 wit inspect 900   880    9400 1700 0      0   - - true 4.8  2.6  70 280 true 8.2 4.4 170 310
termination-crafted/Waldkirch_true-no-overflow.c timeout 0 wit inspect 910   860    10000 9500 0      0   - - true 3.9  2.2  80 270 true 7.2 3.9 140 320
termination-crafted/WhileFalse_true-no-overflow.c true 1 wit inspect 2.3 1.0  19 240 0      0   - - error (invalid witness file) 2.8  1.5  35 190 unknown 5.8 3.1 110 300
termination-crafted/WhileTrue_true-no-overflow.c timeout 0 wit inspect 900   860    12000 850 0      0   - - error (invalid witness file) 2.5  1.4  48 190 unknown 6.1 3.2 130 300
termination-crafted/easy1_true-no-overflow.c true 2 wit inspect 7.9 2.6  60 330 0      0   - - true 4.1  2.3  71 280 true 7.6 4.2 140 320
termination-crafted/easy2_true-no-overflow.c timeout 0 wit inspect 910   870    10000 9000 0      0   - - true 3.9  2.2  82 270 timeout 960   820   11000 4700
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.1  19 250 0      0   true 2.9 1.7 57 240 false(no-overflow) 6.8 3.7 140 310 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  23 250 0      0   true 3.1 1.8 52 230 false(no-overflow) 7.4 4.0 110 310 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  22 250 .0082 0   true 3.0 1.7 63 230 false(no-overflow) 7.3 3.9 110 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  21 250 .0082 0   false(no-overflow) 3.3 1.9 57 240 false(no-overflow) 6.8 3.7 79 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  23 250 0      0   true 3.1 1.8 52 240 false(no-overflow) 7.8 4.2 120 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  24 250 0      0   false(no-overflow) 3.3 1.8 58 240 false(no-overflow) 7.4 3.9 140 310 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  23 250 0      0   true 3.4 2.0 63 250 false(no-overflow) 8.4 4.5 150 330 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  22 250 0      0   true 3.3 1.8 67 230 false(no-overflow) 7.5 4.0 93 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_false-no-overflow.c false(no-overflow) 0 wit inspect 18   5.8  130 510 0      0   true 4.1 2.3 77 260 out of memory 73   43   500 7000 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) 1 wit inspect 2.2 1.0  19 240 0      0   true 3.0 1.7 57 240 false(no-overflow) 8.2 4.3 96 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  19 250 0      0   false(no-overflow) 3.3 1.9 75 240 false(no-overflow) 7.9 4.2 91 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  24 260 .0082 0   true 3.1 1.7 49 240 false(no-overflow) 7.2 3.8 120 310 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  21 250 0      0   true 3.1 1.7 34 240 false(no-overflow) 7.4 3.9 91 320 - -
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  21 260 .0082 0   true 3.3 1.8 52 240 false(no-overflow) 7.8 4.1 91 320 - -
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  24 240 .0082 0   false(no-overflow) 3.3 1.9 54 240 false(no-overflow) 8.0 4.2 120 330 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 1.1  21 270 .0082 0   false(no-overflow) 3.7 2.0 83 260 false(no-overflow) 7.0 3.8 83 310 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 1 wit inspect 3.0 1.2  28 270 .025  0   true 3.3 1.9 63 240 false(no-overflow) 7.4 3.9 110 320 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  25 250 .0082 0   true 2.9 1.7 51 230 false(no-overflow) 7.1 3.8 85 310 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  21 250 .0082 0   false(no-overflow) 3.2 1.8 57 240 false(no-overflow) 7.5 4.0 74 310 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 1.2  28 280 .0082 0   false(no-overflow) 3.7 2.0 86 240 false(no-overflow) 8.0 4.2 110 310 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.1  21 250 .0082 0   false(no-overflow) 3.5 1.9 72 240 false(no-overflow) 7.6 4.0 92 350 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.0  22 260 0      0   true 3.1 1.8 63 240 false(no-overflow) 7.9 4.2 150 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.1  20 250 .0082 0   false(no-overflow) 3.2 1.8 52 240 false(no-overflow) 7.3 3.9 120 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 1.1  22 260 .0082 0   false(no-overflow) 3.5 1.9 47 240 false(no-overflow) 8.5 4.5 160 340 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  23 250 .0082 0   false(no-overflow) 3.1 1.8 48 230 false(no-overflow) 7.0 3.7 110 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  21 250 .0082 0   false(no-overflow) 3.1 1.8 51 230 false(no-overflow) 7.2 3.8 110 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  23 250 0      0   false(no-overflow) 3.2 1.8 60 240 false(no-overflow) 6.7 3.6 120 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  19 250 0      0   false(no-overflow) 3.0 1.7 52 230 false(no-overflow) 7.2 3.9 88 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  21 250 0      0   false(no-overflow) 3.4 1.9 67 230 false(no-overflow) 6.7 3.6 120 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 1.1  22 270 0      0   false(no-overflow) 3.1 1.7 53 240 false(no-overflow) 7.1 3.8 140 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.0  22 250 0      0   false(no-overflow) 3.2 1.8 51 240 false(no-overflow) 6.9 3.7 79 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  26 260 .0082 0   false(no-overflow) 3.2 1.8 59 230 false(no-overflow) 7.1 3.8 100 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  19 240 0      0   false(no-overflow) 3.1 1.8 54 240 false(no-overflow) 6.4 3.4 77 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  19 240 0      0   false(no-overflow) 3.2 1.8 50 230 false(no-overflow) 7.0 3.7 81 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  21 260 0      0   false(no-overflow) 3.2 1.8 63 240 false(no-overflow) 8.3 4.5 100 340 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  22 250 0      0   true 3.0 1.7 49 230 false(no-overflow) 6.9 3.7 120 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  21 250 .0082 0   false(no-overflow) 3.1 1.8 48 230 false(no-overflow) 7.0 3.8 88 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  19 250 0      0   false(no-overflow) 3.1 1.8 41 240 false(no-overflow) 7.1 3.8 120 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  21 240 .0082 0   false(no-overflow) 3.1 1.7 48 230 false(no-overflow) 6.6 3.6 140 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.1  20 240 0      0   true 3.0 1.7 49 240 false(no-overflow) 7.1 3.8 88 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.1  21 250 0      0   true 2.8 1.6 38 240 false(no-overflow) 6.8 3.7 140 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  22 250 0      0   true 3.0 1.7 50 240 false(no-overflow) 7.6 4.1 120 340 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  23 250 0      0   false(no-overflow) 3.2 1.8 59 240 false(no-overflow) 6.6 3.6 110 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  23 250 0      0   false(no-overflow) 3.2 1.8 52 240 false(no-overflow) 7.0 3.7 100 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  21 250 .0082 0   false(no-overflow) 3.2 1.8 57 230 false(no-overflow) 7.2 3.9 110 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  20 250 0      0   false(no-overflow) 3.1 1.8 55 240 false(no-overflow) 6.5 3.5 110 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  23 250 .0082 0   false(no-overflow) 3.1 1.8 48 240 false(no-overflow) 7.4 3.9 100 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  19 240 0      0   false(no-overflow) 3.2 1.8 47 240 false(no-overflow) 7.2 3.9 88 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  22 250 0      0   false(no-overflow) 3.2 1.8 52 230 false(no-overflow) 7.3 3.9 120 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  23 250 .0082 0   false(no-overflow) 3.2 1.8 45 240 false(no-overflow) 6.9 3.7 82 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  19 250 0      0   false(no-overflow) 3.5 2.0 78 240 false(no-overflow) 6.9 3.7 120 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  20 250 0      0   false(no-overflow) 3.3 1.8 54 240 false(no-overflow) 7.7 4.1 120 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  20 250 0      0   false(no-overflow) 3.2 1.8 54 230 false(no-overflow) 7.4 3.9 130 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  20 250 .0082 0   false(no-overflow) 3.1 1.8 62 240 false(no-overflow) 7.1 3.8 110 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  24 250 .0082 0   false(no-overflow) 3.2 1.8 53 230 false(no-overflow) 6.6 3.5 120 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.0  21 250 .0082 0   false(no-overflow) 3.5 2.0 77 240 false(no-overflow) 7.6 4.0 85 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  22 250 .0082 0   false(no-overflow) 3.3 1.8 51 230 false(no-overflow) 6.7 3.6 80 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  21 250 0      0   false(no-overflow) 3.2 1.8 52 240 false(no-overflow) 6.5 3.5 110 320 - -
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  25 250 0      0   true 3.3 1.9 69 230 false(no-overflow) 7.5 4.0 110 320 - -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  23 260 0      0   false(no-overflow) 3.3 1.9 60 230 false(no-overflow) 7.2 3.8 89 320 - -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  23 240 .0082 0   false(no-overflow) 3.1 1.8 56 230 false(no-overflow) 6.7 3.6 80 320 - -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  20 250 0      0   false(no-overflow) 3.1 1.8 53 230 false(no-overflow) 7.5 4.0 160 320 - -
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  23 260 0      0   true 3.4 1.9 59 250 false(no-overflow) 7.9 4.2 130 330 - -
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 12   3.9  110 430 .23   0   true 3.8 2.1 63 240 false(no-overflow) 8.5 4.5 91 330 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  21 240 0      0   true 2.9 1.6 54 240 false(no-overflow) 7.8 4.1 96 340 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c error 0 wit inspect 2.5 1.1  24 260 0      0   false(no-overflow) 3.8 2.1 69 290 false(no-overflow) 7.1 3.9 140 310 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.0  20 250 0      0   true 3.1 1.7 66 230 false(no-overflow) 7.2 3.8 85 310 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  22 260 .0082 0   false(no-overflow) 3.3 1.9 58 250 false(no-overflow) 7.2 3.8 130 310 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  19 250 0      0   false(no-overflow) 3.7 2.0 53 260 false(no-overflow) 8.8 4.8 170 330 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c error (recursion) 0 wit inspect 2.4 1.0  22 240 0      0   false(no-overflow) 3.2 1.9 56 250 false(no-overflow) 7.7 4.1 88 310 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c error (recursion) 0 wit inspect 2.3 1.1  19 250 0      0   error (recursion) 3.2 1.8 61 250 false(no-overflow) 7.2 3.8 130 320 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  20 240 0      0   error (recursion) 3.3 1.9 53 240 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 2.4 1.1  21 240 0      0   false(no-overflow) 3.1 1.8 60 240 false(no-overflow) 7.1 3.8 130 320 - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.0  20 260 0      0   false(no-overflow) 3.1 1.8 47 240 false(no-overflow) 7.8 4.1 120 310 - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  20 250 0      0   false(no-overflow) 3.2 1.8 57 240 false(no-overflow) 6.5 3.5 97 320 - -
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  19 250 0      0   true 3.0 1.7 50 230 false(no-overflow) 6.8 3.6 90 310 - -
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.1  24 250 0      0   false(no-overflow) 3.4 1.9 71 250 false(no-overflow) 7.2 3.8 110 330 - -
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  23 250 0      0   false(no-overflow) 3.1 1.7 38 240 false(no-overflow) 6.9 3.7 81 320 - -
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  20 260 0      0   false(no-overflow) 3.3 1.9 67 240 false(no-overflow) 7.4 3.9 120 320 - -
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  21 260 .0082 0   true 3.3 1.9 52 250 false(no-overflow) 7.2 3.8 140 310 - -
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  23 250 .0082 0   false(no-overflow) 3.4 1.9 37 240 false(no-overflow) 7.0 3.7 110 310 - -
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  21 260 .0082 0   true 3.0 1.7 38 240 false(no-overflow) 7.4 4.0 130 320 - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_false-no-overflow.c false(no-overflow) 0 wit inspect 17   5.4  150 510 0      0   true 4.0 2.3 50 260 out of memory 78   46   510 7000 - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  25 260 0      0   true 3.4 1.9 56 250 false(no-overflow) 7.6 4.1 110 320 - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.1  22 240 0      0   true 3.2 1.9 58 260 false(no-overflow) 7.0 3.7 92 320 - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.4 1.1  22 250 0      0   true 3.4 1.9 54 250 false(no-overflow) 7.3 3.9 120 320 - -
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  23 250 .0082 0   false(no-overflow) 3.2 1.8 61 230 false(no-overflow) 6.6 3.5 91 310 - -
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.3 1.0  21 240 0      0   true 3.0 1.7 66 230 false(no-overflow) 7.3 3.9 140 320 - -
termination-crafted-lit/cstrncmp_false-no-overflow.c error 0 wit inspect 2.6 1.1  25 260 0      0   false(no-overflow) 4.6 2.6 82 300 false(no-overflow) 9.0 4.9 120 350 - -
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  25 260 .0082 0   true 3.0 1.7 37 240 false(no-overflow) 6.9 3.7 94 310 - -
termination-crafted-lit/joey_false-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  20 250 0      0   error (recursion) 3.2 1.8 58 240 false(no-overflow) 7.4 4.1 99 310 - -
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  22 250 .025  0   false(no-overflow) 3.5 2.0 73 240 false(no-overflow) 6.8 3.6 80 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   860    12000 4900 0      0   - - timeout 900    880    13000 5300 timeout 960   870   15000 4000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c timeout 0 wit inspect 900   870    12000 4200 0      0   - - true 4.4  2.4  86 280 true 8.6 4.6 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect 8.0 2.6  62 330 0      0   - - true 4.1  2.3  84 280 true 7.8 4.2 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 910   870    10000 9000 0      0   - - true 4.0  2.2  76 270 timeout 960   820   16000 4700
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 0 wit inspect 900   790    13000 5600 0      0   - - timeout 900    880    21000 4700 timeout 960   790   12000 3100
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900   850    11000 4500 0      0   - - true 4.0  2.3  72 280 out of memory 450   360   4300 7000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect 230   210    2800 2800 0      0   - - timeout 900    880    12000 3900 true 48   28   640 2600
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c timeout 0 wit inspect 900   840    10000 3500 0      0   - - true 4.5  2.5  91 280 true 8.7 4.7 150 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c timeout 0 wit inspect 900   860    11000 4300 0      0   - - true 4.3  2.4  80 280 true 9.0 4.9 160 340
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c timeout 0 wit inspect 900   880    7400 2600 0      0   - - true 4.1  2.3  70 280 true 8.6 4.7 140 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c timeout 0 wit inspect 900   850    13000 5900 0      0   - - timeout 900    870    12000 4600 true 7.8 4.2 150 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c timeout 0 wit inspect 900   850    10000 4600 0      0   - - timeout 900    860    10000 4800 true 8.6 4.6 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout 0 wit inspect 900   890    6500 4700 0      0   - - true 4.1  2.3  72 270 true 10   5.5 170 370
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   810    13000 5800 0      0   - - timeout 900    840    13000 6100 timeout 960   840   18000 4900
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c false(no-overflow) -16 wit inspect 2.8 1.2  24 270 .025  0   - - true 2.9  1.6  47 230 true 15   8.9 260 380
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c false(no-overflow) -16 wit inspect 2.8 1.1  21 250 .0082 0   - - true 3.1  1.8  54 240 true 12   6.5 210 420
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 910   860    9500 13000 0      0   - - true 4.4  2.4  70 280 true 9.7 5.2 150 340
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 0 wit inspect 910   870    8000 11000 0      0   - - timeout 900    840    9800 5600 timeout 960   820   17000 4800
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 0 wit inspect 910   870    10000 8900 0      0   - - true 3.8  2.1  83 280 true 23   13   260 590
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect 8.5 2.7  67 340 0      0   - - true 4.3  2.4  90 280 true 7.1 3.9 130 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 910   870    8500 9000 0      0   - - true 3.8  2.1  70 270 timeout 960   820   11000 4700
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900   850    13000 4500 0      0   - - true 4.1  2.3  68 270 out of memory 430   330   4400 7000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect 230   210    3200 2700 0      0   - - timeout 900    880    19000 3800 true 45   27   390 2400
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c timeout 0 wit inspect 900   860    10000 7700 0      0   - - true 3.8  2.1  53 280 true 6.7 3.6 120 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c false(no-overflow) -16 wit inspect 2.4 1.1  22 250 0      0   - - false(no-overflow) 3.2  1.8  54 240 true 7.4 4.0 130 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c timeout 0 wit inspect 910   880    10000 9100 0      0   - - true 3.9  2.2  65 270 true 7.8 4.2 140 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   860    13000 4500 0      0   - - true 4.4  2.4  72 280 true 8.5 4.5 160 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c timeout 0 wit inspect 900   860    10000 4600 0      0   - - true 4.6  2.6  84 280 true 8.1 4.3 150 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c timeout 0 wit inspect 900   870    13000 4500 0      0   - - true 5.2  2.9  77 300 true 7.9 4.2 130 310
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c false(no-overflow) -16 wit inspect 2.4 1.1  21 250 .0082 0   - - true 3.0  1.7  51 230 true 8.3 4.5 140 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout 0 wit inspect 910   880    7600 5900 0      0   - - true 4.2  2.3  85 270 true 8.3 4.4 160 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c false(no-overflow) -16 wit inspect 2.5 1.1  21 260 0      0   - - true 3.1  1.8  59 230 true 8.7 4.7 150 350
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2 wit inspect 16   5.3  140 440 0      0   - - true 4.1  2.3  87 280 true 120   78   1200 3100
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   830    11000 4900 0      0   - - timeout 900    870    14000 5000 timeout 960   850   18000 4800
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c timeout 0 wit inspect 900   870    12000 5000 0      0   - - true 4.7  2.6  89 280 true 7.5 4.0 130 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 910   860    12000 8900 0      0   - - true 3.8  2.2  77 270 true 20   12   270 590
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c timeout 0 wit inspect 910   870    8600 9000 0      0   - - true 3.8  2.1  62 270 true 8.6 4.5 180 340
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout 0 wit inspect 910   860    13000 8700 0      0   - - true 3.8  2.2  71 280 true 9.1 4.9 170 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c timeout 0 wit inspect 900   880    11000 2500 0      0   - - true 4.0  2.2  70 280 true 7.2 3.9 140 320
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 0 wit inspect 910   790    9000 6900 0      0   - - timeout 900    850    14000 6700 timeout 960   800   11000 4700
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c timeout 0 wit inspect 900   860    11000 4500 0      0   - - true 4.3  2.4  65 270 true 7.6 4.0 150 320
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c false(no-overflow) -16 wit inspect 2.4 1.1  21 260 .0082 0   - - false(no-overflow) 3.1  1.8  53 240 true 8.1 4.3 150 320
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   880    8900 2200 0      0   - - true 4.2  2.3  66 280 timeout 960   820   12000 2600
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.4 1.0  21 250 0      0   - - error (recursion) 3.4  1.9  61 240 true 12   6.4 200 420
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.2 1.0  20 240 0      0   - - error (recursion) 3.4  1.9  75 250 timeout 960   800   11000 3400
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   890    5600 1200 0      0   - - true 4.0  2.2  60 280 true 8.7 4.7 170 320
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c timeout 0 wit inspect 900   880    8100 4700 0      0   - - true 4.7  2.6  83 280 true 7.9 4.2 140 320
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 5.9 2.3  47 290 0      0   - - true 3.8  2.1  87 270 true 8.4 4.4 150 330
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 910   860    11000 9500 0      0   - - true 3.9  2.2  73 280 true 8.1 4.3 140 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c timeout 0 wit inspect 900   850    10000 6200 0      0   - - true 4.1  2.3  66 280 true 9.0 4.8 170 330
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c timeout 0 wit inspect 900   870    10000 5900 0      0   - - true 4.4  2.5  76 280 true 8.3 4.4 150 340
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c timeout 0 wit inspect 900   860    11000 700 0      0   - - true 4.0  2.2  76 280 true 7.2 3.9 150 310
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c timeout 0 wit inspect 900   850    11000 800 0      0   - - out of memory 330    320    4400 7000 true 8.2 4.5 150 320
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c timeout 0 wit inspect 900   850    12000 2800 0      0   - - out of memory 350    330    4000 7000 true 8.1 4.4 140 320
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout 0 wit inspect 900   870    13000 5100 0      0   - - true 5.6  3.0  93 290 true 7.8 4.2 140 310
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c timeout 0 wit inspect 910   860    10000 8500 0      0   - - true 4.4  2.5  75 280 true 7.5 4.0 87 330
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 2 wit inspect 45   31    430 670 0      0   - - true 4.4  2.4  73 280 timeout 960   810   19000 5000
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c error 0 wit inspect 2.6 1.1  22 260 0      0   - - true 5.6  3.1  78 290 true 8.3 4.5 150 330
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c error 0 wit inspect 2.6 1.1  22 260 0      0   - - false(no-overflow) 4.5  2.6  60 300 true 8.2 4.3 160 330
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c error 0 wit inspect 2.5 1.1  23 250 0      0   - - false(no-overflow) 4.4  2.4  95 290 true 8.3 4.5 130 330
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c error 0 wit inspect 2.5 1.1  22 240 0      0   - - true 6.8  3.7  110 320 true 7.8 4.3 150 330
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c error 0 wit inspect 2.5 1.1  24 250 0      0   - - false(no-overflow) 4.8  2.8  91 300 true 8.3 4.5 150 330
termination-crafted-lit/genady_true-termination_true-no-overflow.c timeout 0 wit inspect 900   860    12000 740 0      0   - - true 3.7  2.1  63 270 true 12   6.7 170 450
termination-crafted-lit/strchr_true-no-overflow.c error 0 wit inspect 2.5 1.1  21 260 0      0   - - true 5.1  2.8  86 290 true 8.0 4.3 160 320
termination-numeric/Addition01_false-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  20 240 0      0   false(no-overflow) 3.4 1.9 49 250 false(no-overflow) 7.2 3.8 86 320 - -
termination-numeric/Avg_true_false-no-overflow.c error (recursion) 0 wit inspect 2.4 1.1  21 240 0      0   error (recursion) 3.3 1.9 62 240 false(no-overflow) 7.1 3.8 140 310 - -
termination-numeric/Binomial_true-termination_false-no-overflow.c error (recursion) 0 wit inspect 2.7 1.1  25 250 0      0   error (recursion) 3.1 1.7 61 220 timeout 96   64   1900 1200 - -
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  22 250 .016  0   false(no-overflow) 3.3 1.9 60 240 false(no-overflow) 8.6 4.7 160 340 - -
termination-numeric/Et2_true_false-no-overflow.c error (recursion) 0 wit inspect 2.4 1.1  21 240 0      0   false(no-overflow) 3.8 2.1 66 250 false(no-overflow) 6.9 3.7 87 320 - -
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  22 250 .016  0   false(no-overflow) 3.5 2.0 73 240 false(no-overflow) 7.3 3.9 94 320 - -
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 1.1  26 250 .041  0   false(no-overflow) 3.5 2.0 77 240 false(no-overflow) 8.9 4.8 160 340 - -
termination-numeric/MultCommutative_false-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  21 240 0      0   error (recursion) 3.4 1.9 73 240 false(no-overflow) 12   7.0 170 400 - -
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c error (recursion) 0 wit inspect 2.4 1.0  23 250 0      0   error (recursion) 3.5 1.9 53 260 timeout 97   87   1100 1100 - -
termination-numeric/Ackermann01_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.4 1.1  21 240 0      0   - - error (recursion) 3.6  2.0  69 250 out of memory 800   640   8800 7000
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  22 250 0      0   - - error (recursion) 3.4  1.9  60 250 timeout 960   800   19000 4400
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.2 1.0  18 250 0      0   - - error (recursion) 3.4  1.9  80 240 timeout 960   890   15000 5700
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.4 1.1  22 240 0      0   - - error (recursion) 3.3  1.9  53 250 true 7.8 4.3 130 330
termination-numeric/LogRecursive_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  18 240 0      0   - - error (recursion) 3.2  1.8  43 250 timeout 960   790   17000 4800
termination-numeric/Parts_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 3.2 1.3  30 260 0      0   - - error (recursion) 2.8  1.6  50 190 timeout 960   800   17000 4800
termination-numeric/TwoWay_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.4 1.1  23 250 0      0   - - error (recursion) 3.3  1.9  76 240 unknown 19   12   270 480
termination-numeric/gcd01_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  20 250 0      0   - - error (recursion) 3.2  1.8  48 240 true 8.2 4.5 140 330
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect 7.0 2.8  61 300 0      0   - - true 3.9  2.2  69 280 true 63   38   590 1100
termination-numeric/recHanoi02_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  23 250 0      0   - - error (recursion) 3.3  1.9  66 240 timeout 960   800   13000 4400
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.2 .99 20 250 0      0   - - error (recursion) 2.7  1.5  53 190 timeout 960   810   11000 5200
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  21 240 0      0   - - error (recursion) 2.9  1.6  62 200 timeout 960   810   12000 4900
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 0 wit inspect 900   830    10000 5100 0      0   - - true 6.0  3.2  97 300 timeout 960   800   12000 2800
../../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 21 59000   56000   690000 410000 .80  0   274 510   290   8900 37000   274 1500 890 22000 66000   274 13000   12000   200000 110000   274 28000   23000   390000 180000  
    correct results 150 164 920   620   10000 44000 .75  0   136 440   250   7700 33000   136 990 530 15000 44000   12 1900   1800   32000 11000   13 1300   1000   23000 17000  
        correct true 14 28 570   470   7000 9500 0     0   47 0   0   0 0   0 0 0 0 0   12 1900   1800   32000 11000   13 1300   1000   23000 17000  
        correct false 136 136 350   150   3100 35000 .75  0   89 440   250   7700 33000   136 990 530 15000 44000   0 0   0   0 0   0 0   0   0 0  
    correct-unconfimed results 3 1 38   12   290 1300 0     0   2 8.2 4.6 130 510   0 150 89 1000 14000   0 2.8 1.5 35 190   0 5.8 3.1 110 300  
        correct-unconfirmed true 1 1 2.3 1.0 19 240 0     0   2 0   0   0 0   0 0 0 0 0   0 2.8 1.5 35 190   0 5.8 3.1 110 300  
        correct-unconfirmed false 2 0 35   11   270 1000 0     0   0 8.2 4.6 130 510   0 150 89 1000 14000   0 0   0   0 0   0 0   0   0 0  
    incorrect results 9 -144 23   9.9 200 2300 .049 0   0 0   0   0 0   0 0 0 0 0   8 930   890   21000 5600   9 85   47   1500 3100  
        incorrect true 0
        incorrect false 9 -144 23   9.9 200 2300 .049 0   0 0   0   0 0   0 0 0 0 0   2 930   890   21000 5600   0 85   47   1500 3100  
score (274 tasks, max score: 393) 21
Run set sv-comp17.Overflows-BitVectors