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