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