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