Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-13 08:09:41 CET [[ 2017-01-15 00:46:31 CET ]] [[ 2017-01-15 01:12:25 CET ]] [[ 2017-01-15 00:52:40 CET ]] [[ 2017-01-15 01:18:42 CET ]]
Run set sv-comp17.Overflows-BitVectors
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i false(no-overflow) 1 wit inspect .65 .65 7.6 110 4.2  0   false(no-overflow) 4.0  2.3  66   250 true 6.7 3.6 120 310 - -
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 1 wit inspect .65 .65 7.5 110 5.0  0   false(no-overflow) 4.3  2.4  86   260 true 7.7 4.1 150 310 - -
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 1 wit inspect .63 .63 6.6 110 4.2  0   false(no-overflow) 4.2  2.3  86   250 true 7.2 3.8 120 310 - -
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 1 wit inspect .63 .63 5.7 110 5.0  0   false(no-overflow) 4.1  2.3  83   250 true 9.3 4.8 79 310 - -
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 1 wit inspect .63 .63 6.0 110 4.2  0   false(no-overflow) 4.2  2.3  79   250 true 7.1 3.8 120 320 - -
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .61 .61 8.0 110 4.9  0   false(no-overflow) 4.2  2.3  85   260 true 6.9 3.7 99 300 - -
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .64 .63 5.8 110 5.0  0   false(no-overflow) 4.4  2.4  86   260 true 7.0 3.7 120 310 - -
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .65 .65 5.4 110 5.0  0   false(no-overflow) 4.3  2.4  79   260 true 7.0 3.7 140 300 - -
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .63 .63 5.8 110 5.0  0   false(no-overflow) 4.3  2.4  89   260 true 6.7 3.6 110 320 - -
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 1 wit inspect .69 .69 6.9 110 5.0  0   false(no-overflow) 4.0  2.3  77   240 true 6.7 3.6 110 320 - -
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow.c.i true 2 wit inspect .59 .58 5.3 110 5.0  0   - - true 4.0  2.2  87   250 true 7.2 3.8 130 320
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow.c.i true 2 wit inspect .58 .58 6.4 110 5.0  0   - - true 4.1  2.2  80   260 true 7.8 4.2 150 320
signedintegeroverflow-regression/Multiplication_true-no-overflow.c.i true 2 wit inspect .56 .55 6.2 110 5.0  0   - - true 3.9  2.2  83   250 true 7.4 3.9 150 310
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow.c.i true 2 wit inspect .58 .58 5.4 110 5.0  0   - - true 4.2  2.3  85   260 true 7.1 3.8 140 310
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow.c.i true 2 wit inspect .57 .57 5.3 110 5.0  0   - - true 4.3  2.4  90   270 true 6.6 3.6 140 310
termination-crafted/2Nested_false-no-overflow.c out of memory 0 wit inspect 46    45    520   15000 4.2  0   true 3.0  1.7  58   240 false(no-overflow) 7.1 3.8 130 330 - -
termination-crafted/4NestedWith3Variables_false-no-overflow.c out of memory 0 wit inspect 86    86    940   15000 5.0  0   true 3.3  1.8  57   230 false(no-overflow) 7.4 4.0 110 320 - -
termination-crafted/Ackermann_false-no-overflow.c out of memory 0 wit inspect 140    130    1900   15000 .99 0   error (invalid witness file) .52 .32 7.3 40 error (invalid witness file) 5.7 3.0 98 290 - -
termination-crafted/Bangalore_false-no-overflow.c out of memory 0 wit inspect 40    39    500   15000 5.0  0   true 3.1  1.8  67   240 false(no-overflow) 7.2 3.8 120 320 - -
termination-crafted/Bangalore_v3_false-no-overflow.c out of memory 0 wit inspect 40    39    420   15000 5.0  0   true 3.2  1.8  70   240 false(no-overflow) 7.3 3.9 140 320 - -
termination-crafted/Benghazi_nondet_false-no-overflow.c out of memory 0 wit inspect 55    54    710   15000 4.2  0   true 3.2  1.8  68   240 false(no-overflow) 6.9 3.7 110 310 - -
termination-crafted/Binary_Search_false-no-overflow.c out of memory 0 wit inspect 140    140    1900   15000 .84 0   error (invalid witness file) .51 .34 10   40 error (invalid witness file) 5.7 3.0 99 290 - -
termination-crafted/Cairo_nondet_false-no-overflow.c out of memory 0 wit inspect 36    35    390   15000 4.4  0   true 8.0  4.2  92   550 timeout 97   63   1500 6300 - -
termination-crafted/Collatz_unknown-termination_false-no-overflow.c out of memory 0 wit inspect 74    74    900   15000 4.2  0   true 3.0  1.7  62   240 false(no-overflow) 7.1 3.8 130 320 - -
termination-crafted/Copenhagen_disj_false-no-overflow.c out of memory 0 wit inspect 37    36    380   15000 5.7  0   true 15    7.7  200   890 out of memory 79   51   610 7000 - -
termination-crafted/Gothenburg_false-no-overflow.c out of memory 0 wit inspect 52    52    560   15000 5.3  0   true 13    7.0  190   730 timeout 98   68   1300 6400 - -
termination-crafted/Gothenburg_v2_false-no-overflow.c out of memory 0 wit inspect 52    52    580   15000 5.2  0   true 14    7.4  190   730 timeout 96   79   1200 5100 - -
termination-crafted/Hanoi_2vars_false-no-overflow.c out of memory 0 wit inspect 43    43    560   15000 5.0  0   true 3.2  1.8  62   240 false(no-overflow) 8.2 4.4 130 330 - -
termination-crafted/Hanoi_3vars_false-no-overflow.c out of memory 0 wit inspect 53    53    660   15000 5.0  0   true 3.4  1.9  59   240 false(no-overflow) 15   8.7 190 400 - -
termination-crafted/Hanoi_plus_false-no-overflow.c out of memory 0 wit inspect 66    65    670   15000 5.0  0   true 3.2  1.8  55   240 false(no-overflow) 7.2 3.8 130 310 - -
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c out of memory 0 wit inspect 52    52    690   15000 5.4  0   true 13    6.7  150   720 out of memory 67   43   620 7000 - -
termination-crafted/Mysore_false-no-overflow.c out of memory 0 wit inspect 49    49    510   15000 5.0  0   false(no-overflow) 3.3  1.9  68   240 false(no-overflow) 6.8 3.6 93 310 - -
termination-crafted/NestedRecursion_1a_false-no-overflow.c out of memory 0 wit inspect 99    94    1100   15000 .97 0   error (invalid witness file) .51 .32 11   39 error (invalid witness file) 6.0 3.2 100 300 - -
termination-crafted/NestedRecursion_2a_false-no-overflow.c out of memory 0 wit inspect 150    140    2000   15000 .99 0   error (invalid witness file) .49 .32 9.7 40 error (invalid witness file) 6.6 3.5 120 310 - -
termination-crafted/NonTermination1_false-no-overflow.c out of memory 0 wit inspect 34    34    360   15000 5.0  0   true 3.0  1.7  65   230 false(no-overflow) 7.0 3.7 120 320 - -
termination-crafted/NonTermination2_false-no-overflow.c out of memory 0 wit inspect 42    42    430   15000 5.1  0   true 9.5  5.0  160   460 false(no-overflow) 34   22   470 2900 - -
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 1 wit inspect 900    900    3400   420 5.0  0   false(no-overflow) 3.9  2.2  78   250 true 7.2 3.8 120 310 - -
termination-crafted/NonTerminationSimple2_false-no-overflow.c out of memory 0 wit inspect 36    36    440   15000 5.0  0   true 4.7  2.6  82   290 false(no-overflow) 13   6.8 140 870 - -
termination-crafted/NonTerminationSimple3_false-no-overflow.c out of memory 0 wit inspect 41    41    470   15000 5.2  0   true 7.1  3.8  120   520 false(no-overflow) 51   33   590 5100 - -
termination-crafted/NonTerminationSimple4_false-no-overflow.c out of memory 0 wit inspect 36    35    480   15000 5.3  0   true 10    5.9  160   720 timeout 97   62   770 1700 - -
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 1 wit inspect 890    900    9400   1100 4.0  0   true 3.1  1.7  66   230 false(no-overflow) 7.3 3.9 120 320 - -
termination-crafted/NonTerminationSimple6_false-no-overflow.c out of memory 0 wit inspect 36    36    380   15000 5.2  0   true 9.4  4.9  130   460 false(no-overflow) 40   24   400 3900 - -
termination-crafted/NonTerminationSimple8_false-no-overflow.c out of memory 0 wit inspect 80    80    830   15000 4.4  0   true 6.6  3.6  100   370 false(no-overflow) 21   12   290 1900 - -
termination-crafted/NonTerminationSimple9_false-no-overflow.c out of memory 0 wit inspect 45    44    510   15000 5.1  0   true 7.6  4.0  120   390 false(no-overflow) 26   16   300 3100 - -
termination-crafted/Pure2Phase_false-no-overflow.c out of memory 0 wit inspect 53    53    560   15000 5.0  0   true 3.4  1.9  70   230 true 7.7 4.2 130 320 - -
termination-crafted/Pure3Phase_false-no-overflow.c out of memory 0 wit inspect 160    160    1500   15000 4.0  0   true 3.9  2.2  65   250 false(no-overflow) 13   7.4 150 400 - -
termination-crafted/RecursiveMultiplication_false-no-overflow.c out of memory 0 wit inspect 120    120    1600   15000 .99 0   error (invalid witness file) .51 .35 9.1 39 error (invalid witness file) 6.4 3.4 120 310 - -
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 1 wit inspect .49 .48 4.5 41 2.0  0   true 3.2  1.8  59   240 false(no-overflow) 7.0 3.8 130 320 - -
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 0 wit inspect 570    570    4000   3300 27    0   timeout 98    51    670   5200 out of memory 80   45   930 7000 - -
termination-crafted/Singapore_false-no-overflow.c out of memory 0 wit inspect 40    40    440   15000 5.0  0   true 3.0  1.7  63   230 false(no-overflow) 8.5 4.6 91 310 - -
termination-crafted/Singapore_plus_false-no-overflow.c out of memory 0 wit inspect 41    40    480   15000 5.0  0   true 3.8  2.1  82   260 out of memory 44   29   350 7000 - -
termination-crafted/Singapore_v1_false-no-overflow.c out of memory 0 wit inspect 41    41    510   15000 5.0  0   true 3.6  2.0  72   260 out of memory 78   48   550 7000 - -
termination-crafted/Singapore_v2_false-no-overflow.c out of memory 0 wit inspect 42    42    440   15000 4.3  0   true 3.5  2.0  71   260 out of memory 71   44   550 7000 - -
termination-crafted/Stockholm_false-no-overflow.c out of memory 0 wit inspect 44    44    560   15000 5.2  0   true 8.2  4.3  140   550 out of memory 80   53   990 7000 - -
termination-crafted/Thun_false-no-overflow.c out of memory 0 wit inspect 37    36    410   15000 4.8  0   true 3.2  1.8  66   240 false(no-overflow) 8.3 4.3 120 330 - -
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c out of memory 0 wit inspect 39    39    390   15000 5.0  0   true 4.6  2.5  66   290 timeout 95   58   960 7000 - -
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c out of memory 0 wit inspect 40    40    420   15000 4.9  0   true 3.9  2.2  78   250 out of memory 89   55   610 7000 - -
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 0 wit inspect 900    900    8300   1300 4.0  0   true 3.3  1.9  53   240 true 11   6.0 160 360 - -
termination-crafted/aaron3_false-no-overflow.c out of memory 0 wit inspect 71    70    770   15000 5.0  0   true 3.2  1.8  69   240 false(no-overflow) 7.6 4.0 140 310 - -
termination-crafted/4BitCounterPointer_true-no-overflow.c true 2 wit inspect 2.5  2.5  24   320 5.0  0   - - true 4.5  2.5  92   280 true 6.8 3.7 130 310
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow.c out of memory 0 wit inspect 33    33    350   15000 5.6  0   - - out of memory 340    320    3100   7000 timeout 960   800   20000 4300
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow.c out of memory 0 wit inspect 34    33    340   15000 5.5  0   - - false(no-overflow) 12    7.8  160   320 true 9.1 4.7 160 330
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow.c out of memory 0 wit inspect 36    35    470   15000 4.8  0   - - timeout 900    860    16000   5100 true 9.0 4.9 160 340
termination-crafted/Bangalore_true-no-overflow.c out of memory 0 wit inspect 35    34    380   15000 4.9  0   - - true 11    6.5  190   720 true 8.3 4.5 180 330
termination-crafted/Bangalore_v2_true-no-overflow.c out of memory 0 wit inspect 35    35    440   15000 5.3  0   - - true 11    6.9  170   410 true 8.7 4.6 160 330
termination-crafted/Bangalore_v4_true-no-overflow.c out of memory 0 wit inspect 35    35    370   15000 5.3  0   - - false(no-overflow) 9.8  5.5  100   320 true 8.9 4.7 160 330
termination-crafted/Benghazi_true-no-overflow.c out of memory 0 wit inspect 35    35    430   15000 6.1  0   - - true 13    8.1  210   320 true 87   55   780 1400
termination-crafted/Cairo_step2_true-no-overflow.c out of memory 0 wit inspect 36    35    420   15000 4.6  0   - - true 9.8  5.8  140   300 timeout 960   810   16000 4100
termination-crafted/Cairo_true-no-overflow.c out of memory 0 wit inspect 36    36    480   15000 5.3  0   - - true 11    6.1  110   370 true 8.7 4.6 160 320
termination-crafted/Copenhagen_true-no-overflow.c out of memory 0 wit inspect 35    35    410   15000 5.8  0   - - true 12    7.1  190   330 true 10   5.5 160 360
termination-crafted/Division_true-no-overflow.c out of memory 0 wit inspect 33    33    400   15000 4.7  0   - - true 5.3  2.9  65   300 true 9.2 4.8 170 330
termination-crafted/LexIndexValue-Array_true-no-overflow.c out of memory 0 wit inspect 78    78    860   15000 5.9  0   - - out of memory 540    510    6300   7000 timeout 960   800   11000 4600
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c out of memory 0 wit inspect 62    61    650   15000 6.6  0   - - false(no-overflow) 7.5  4.1  130   350 timeout 960   800   14000 4800
termination-crafted/Madrid_true-no-overflow.c true 2 wit inspect 1.4  1.4  18   420 9.0  0   - - true 370    370    4300   3000 true 9.6 5.0 160 360
termination-crafted/McCarthy91_Iteration_true-no-overflow.c true 2 wit inspect 900    900    9000   1400 5.7  0   - - true 47    41    410   1300 timeout 960   850   21000 4700
termination-crafted/McCarthy91_Recursion_true-no-overflow.c out of memory 0 wit inspect 120    120    1600   15000 .99 0   - - error (invalid witness file) .51 .32 6.8 40 error (invalid witness file) 5.9 3.1 120 290
termination-crafted/MenloPark_true-no-overflow.c out of memory 0 wit inspect 34    34    430   15000 5.9  0   - - true 12    7.3  200   450 true 18   9.8 250 500
termination-crafted/MutualRecursion_1a_true-no-overflow.c out of memory 0 wit inspect 110    110    1600   15000 .99 0   - - error (invalid witness file) .49 .31 4.7 40 error (invalid witness file) 6.2 3.3 120 300
termination-crafted/MutualRecursion_1b_true-no-overflow.c out of memory 0 wit inspect 120    110    1400   15000 .99 0   - - error (invalid witness file) .50 .32 9.7 40 error (invalid witness file) 6.1 3.2 140 300
termination-crafted/NestedRecursion_1b_true-no-overflow.c out of memory 0 wit inspect 96    91    1200   15000 .84 0   - - error (invalid witness file) .56 .37 14   43 error (invalid witness file) 6.2 3.3 130 300
termination-crafted/NestedRecursion_1c_true-no-overflow.c out of memory 0 wit inspect 93    89    1200   15000 .99 0   - - error (invalid witness file) .52 .34 10   42 error (invalid witness file) 5.5 2.9 110 290
termination-crafted/NestedRecursion_1d_true-no-overflow.c out of memory 0 wit inspect 96    91    1300   15000 .99 0   - - error (invalid witness file) .50 .34 10   40 error (invalid witness file) 5.7 3.1 100 290
termination-crafted/NestedRecursion_2b_true-no-overflow.c out of memory 0 wit inspect 120    110    1400   15000 .99 0   - - error (invalid witness file) .50 .32 7.2 41 error (invalid witness file) 6.2 3.3 130 300
termination-crafted/NestedRecursion_2c_true-no-overflow.c out of memory 0 wit inspect 120    110    1800   15000 .99 0   - - error (invalid witness file) .57 .35 6.9 42 error (invalid witness file) 5.9 3.2 140 300
termination-crafted/NonTermination3_true-no-overflow.c out of memory 0 wit inspect 51    50    540   15000 5.6  0   - - true 6.2  3.3  110   290 true 7.3 3.9 140 310
termination-crafted/NonTerminationSimple7_true-no-overflow.c out of memory 0 wit inspect 41    40    450   15000 5.1  0   - - true 12    7.1  170   300 true 8.6 4.6 170 330
termination-crafted/Nyala-2lex_true-no-overflow.c out of memory 0 wit inspect 51    50    520   15000 5.6  0   - - true 20    15    180   770 true 9.2 4.8 170 320
termination-crafted/Parallel_true-no-overflow.c out of memory 0 wit inspect 51    51    680   15000 6.1  0   - - true 49    44    530   490 true 9.3 4.9 170 340
termination-crafted/Piecewise_true-no-overflow.c out of memory 0 wit inspect 190    190    2500   15000 6.1  0   - - true 89    82    700   1600 true 9.1 4.8 130 330
termination-crafted/SyntaxSupportPointer01_true-no-overflow.c out of memory 0 wit inspect 34    34    360   15000 5.3  0   - - true 5.8  3.1  75   300 true 8.6 4.6 150 330
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow.c out of memory 0 wit inspect 64    64    790   15000 7.8  0   - - true 350    340    6700   2700 true 9.9 5.2 180 370
termination-crafted/Waldkirch_true-no-overflow.c out of memory 0 wit inspect 34    34    380   15000 5.3  0   - - true 5.3  2.9  86   280 true 8.0 4.2 180 320
termination-crafted/WhileFalse_true-no-overflow.c true 2 wit inspect .36 .36 4.4 32 5.0  0   - - true 3.6  2.0  81   290 true 7.6 4.0 140 320
termination-crafted/WhileTrue_true-no-overflow.c true 2 wit inspect .38 .38 4.5 32 5.0  0   - - true 3.5  2.0  71   270 true 7.2 3.8 140 320
termination-crafted/easy1_true-no-overflow.c out of memory 0 wit inspect 50    49    530   15000 5.7  0   - - true 22    18    260   640 true 10   5.3 190 330
termination-crafted/easy2_true-no-overflow.c out of memory 0 wit inspect 34    34    370   15000 5.9  0   - - true 11    6.7  160   310 timeout 960   820   18000 4700
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c timeout 0 wit inspect 900    900    11000   4600 .99 0   error (invalid witness file) .54 .35 9.9 40 error (invalid witness file) 5.7 3.1 110 300 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c out of memory 0 wit inspect 26    26    230   15000 .99 0   error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.9 3.1 110 290 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 0 wit inspect 890    900    9300   1400 3.4  0   true 3.3  1.8  73   240 true 12   6.6 180 390 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c out of memory 0 wit inspect 80    80    930   15000 5.0  0   true 3.3  1.8  67   240 false(no-overflow) 8.1 4.3 150 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c timeout 0 wit inspect 900    900    7600   10000 .99 0   error (invalid witness file) .51 .35 5.1 39 error (invalid witness file) 6.0 3.1 120 300 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 1 wit inspect 890    890    10000   2400 4.0  0   true 3.1  1.7  59   230 false(no-overflow) 7.3 3.9 120 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c timeout 0 wit inspect 900    900    8300   11000 .99 0   error (invalid witness file) .51 .33 9.9 39 error (invalid witness file) 7.3 3.8 120 320 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c out of memory 0 wit inspect 67    67    740   15000 6.0  0   true 23    12    290   1200 timeout 92   59   1100 7000 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_false-no-overflow.c timeout 0 wit inspect 900    900    9000   2600 .99 0   error (invalid witness file) .52 .34 11   42 error (invalid witness file) 5.9 3.2 110 300 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c out of memory 0 wit inspect 35    35    370   15000 5.2  0   true 11    5.6  200   560 timeout 97   69   1000 5900 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c out of memory 0 wit inspect 200    200    2600   15000 4.4  0   true 3.1  1.8  68   230 true 9.5 5.1 130 340 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c out of memory 0 wit inspect 57    57    690   15000 5.0  0   true 9.1  4.8  150   550 false(no-overflow) 48   31   510 5100 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c out of memory 0 wit inspect 67    66    930   15000 6.0  0   true 24    12    250   1200 timeout 96   56   790 6300 - -
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c out of memory 0 wit inspect 140    140    1400   15000 4.9  0   true 3.2  1.8  64   240 false(no-overflow) 7.8 4.2 130 320 - -
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c out of memory 0 wit inspect 330    330    3500   15000 5.0  0   true 3.4  1.9  74   240 true 11   5.9 150 360 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) 0 wit inspect 890    890    11000   4200 4.0  0   true 3.8  2.1  54   260 timeout 93   66   1100 7000 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c out of memory 0 wit inspect 320    320    3500   15000 5.1  0   true 8.3  4.4  110   540 false(no-overflow) 53   33   730 5000 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 0 wit inspect 890    900    8000   1400 4.0  0   true 3.1  1.7  48   240 true 11   6.1 150 380 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c out of memory 0 wit inspect 80    79    930   15000 5.0  0   true 3.2  1.8  64   230 false(no-overflow) 7.8 4.1 140 330 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c out of memory 0 wit inspect 530    530    6500   15000 5.0  0   true 3.4  1.9  68   240 false(no-overflow) 8.1 4.3 150 320 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c out of memory 0 wit inspect 68    68    860   15000 5.0  0   false(no-overflow) 3.6  2.0  74   240 false(no-overflow) 7.0 3.7 130 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c out of memory 0 wit inspect 33    32    330   15000 5.0  0   true 2.9  1.7  51   240 false(no-overflow) 6.8 3.6 91 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c out of memory 0 wit inspect 50    49    580   15000 4.2  0   true 3.0  1.7  66   240 true 9.6 5.2 140 350 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c out of memory 0 wit inspect 44    44    470   15000 5.0  0   true 3.4  1.9  69   250 false(no-overflow) 8.2 4.4 140 350 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c out of memory 0 wit inspect 42    42    520   15000 5.0  0   true 4.1  2.3  82   260 false(no-overflow) 11   5.8 150 450 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c out of memory 0 wit inspect 43    42    500   15000 5.1  0   true 11    5.5  180   490 false(no-overflow) 33   22   380 3400 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c out of memory 0 wit inspect 42    42    490   15000 5.1  0   true 5.9  3.2  68   360 out of memory 80   49   590 7000 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c out of memory 0 wit inspect 43    42    400   15000 5.0  0   true 2.9  1.7  63   240 false(no-overflow) 9.0 4.8 170 360 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c out of memory 0 wit inspect 33    33    370   15000 5.0  0   true 3.1  1.8  63   240 false(no-overflow) 7.3 3.9 130 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c out of memory 0 wit inspect 34    33    420   15000 5.0  0   true 2.9  1.7  62   240 false(no-overflow) 8.3 4.4 130 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c out of memory 0 wit inspect 48    48    560   15000 5.4  0   true 13    6.8  150   720 timeout 98   63   780 6000 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c out of memory 0 wit inspect 39    39    490   15000 5.0  0   false(no-overflow) 3.1  1.8  69   230 false(no-overflow) 8.0 4.2 130 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c out of memory 0 wit inspect 34    34    350   15000 5.0  0   true 3.3  1.8  50   240 false(no-overflow) 7.4 4.0 130 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c out of memory 0 wit inspect 42    42    510   15000 4.8  0   true 3.1  1.8  48   240 false(no-overflow) 9.5 5.1 140 340 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c out of memory 0 wit inspect 39    39    410   15000 4.2  0   true 3.3  1.8  64   250 false(no-overflow) 7.4 3.9 130 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c out of memory 0 wit inspect 42    42    460   15000 4.2  0   true 3.1  1.8  76   240 false(no-overflow) 7.5 4.0 130 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c out of memory 0 wit inspect 41    41    450   15000 5.0  0   false(no-overflow) 3.3  1.8  66   240 false(no-overflow) 7.6 4.0 150 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c out of memory 0 wit inspect 40    39    430   15000 5.0  0   true 3.1  1.8  68   240 false(no-overflow) 8.7 4.7 120 340 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c out of memory 0 wit inspect 52    51    500   15000 5.0  0   false(no-overflow) 3.2  1.8  58   240 false(no-overflow) 10   5.4 120 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c out of memory 0 wit inspect 35    35    370   15000 4.9  0   true 3.1  1.7  61   240 false(no-overflow) 6.8 3.7 130 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 1 wit inspect 890    900    11000   560 4.0  0   true 3.2  1.8  59   240 false(no-overflow) 7.4 3.9 120 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c out of memory 0 wit inspect 38    38    360   15000 5.0  0   true 3.1  1.7  57   240 false(no-overflow) 6.9 3.7 110 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c out of memory 0 wit inspect 38    37    430   15000 5.3  0   true 8.5  4.5  130   630 false(no-overflow) 23   12   260 910 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c out of memory 0 wit inspect 36    35    450   15000 4.2  0   true 3.4  1.9  72   260 false(no-overflow) 9.5 4.9 160 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c out of memory 0 wit inspect 35    35    380   15000 5.0  0   true 3.5  1.9  73   250 false(no-overflow) 8.1 4.3 140 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c out of memory 0 wit inspect 46    45    490   15000 5.0  0   true 3.0  1.7  70   230 false(no-overflow) 7.4 4.0 100 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c out of memory 0 wit inspect 35    35    380   15000 5.0  0   false(no-overflow) 3.2  1.8  71   230 false(no-overflow) 7.3 3.8 120 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c out of memory 0 wit inspect 46    46    610   15000 5.4  0   true 14    7.1  170   720 timeout 97   75   1000 5200 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c out of memory 0 wit inspect 52    52    530   15000 5.0  0   true 3.2  1.8  67   230 false(no-overflow) 7.6 4.1 130 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c out of memory 0 wit inspect 45    45    560   15000 5.0  0   false(no-overflow) 3.3  1.9  71   240 false(no-overflow) 6.6 3.6 110 310 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c out of memory 0 wit inspect 42    41    510   15000 4.8  0   true 3.2  1.8  68   240 false(no-overflow) 8.3 4.5 130 340 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c out of memory 0 wit inspect 46    46    500   15000 5.0  0   true 3.1  1.8  55   250 false(no-overflow) 8.6 4.6 140 350 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c out of memory 0 wit inspect 44    44    460   15000 5.0  0   true 3.0  1.7  47   230 false(no-overflow) 7.2 3.8 120 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c out of memory 0 wit inspect 48    48    540   15000 5.7  0   true 23    12    250   1200 timeout 97   72   950 6200 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c out of memory 0 wit inspect 42    42    460   15000 5.0  0   true 3.2  1.8  61   230 false(no-overflow) 7.6 4.0 120 330 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c out of memory 0 wit inspect 67    67    790   15000 4.8  0   true 3.1  1.7  46   240 false(no-overflow) 7.9 4.2 150 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c out of memory 0 wit inspect 47    46    480   15000 5.0  0   false(no-overflow) 3.2  1.8  64   240 false(no-overflow) 7.2 3.9 130 320 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c out of memory 0 wit inspect 41    41    480   15000 5.0  0   true 3.1  1.7  63   240 true 10   5.6 150 360 - -
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c out of memory 0 wit inspect 67    67    790   15000 5.1  0   true 23    12    270   1200 out of memory 84   53   870 7000 - -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c out of memory 0 wit inspect 71    71    770   15000 4.7  0   true 14    7.3  160   730 timeout 98   68   1500 5500 - -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c out of memory 0 wit inspect 54    54    520   15000 5.7  0   true 15    8.0  210   1200 timeout 97   67   1100 5800 - -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c out of memory 0 wit inspect 39    39    430   15000 5.3  0   true 14    7.3  210   720 timeout 97   69   1400 5600 - -
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c out of memory 0 wit inspect 69    69    770   15000 5.0  0   true 3.9  2.2  81   260 false(no-overflow) 9.7 5.1 140 370 - -
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c out of memory 0 wit inspect 40    39    490   15000 5.1  0   true 13    6.7  170   510 false(no-overflow) 22   13   320 1800 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c out of memory 0 wit inspect 120    120    1400   15000 4.8  0   true 2.9  1.6  44   240 true 22   16   260 390 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c timeout 0 wit inspect 900    900    11000   420 .99 0   error (invalid witness file) .52 .34 5.6 40 error (invalid witness file) 6.1 3.2 110 300 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c out of memory 0 wit inspect 43    42    460   15000 5.0  0   true 2.8  1.6  47   240 false(no-overflow) 7.5 4.0 140 320 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c out of memory 0 wit inspect 41    41    500   15000 4.7  0   false(no-overflow) 3.2  1.8  70   240 false(no-overflow) 7.1 3.8 110 310 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 0 wit inspect 3.8  3.8  45   70 2.0  0   error (recursion) 6.0  3.2  110   320 timeout 97   59   750 6400 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect 3.2  3.2  35   88 2.0  0   error (recursion) 4.0  2.2  74   270 false(no-overflow) 15   7.9 190 750 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c out of memory 0 wit inspect 140    140    1600   15000 .84 0   error (invalid witness file) .47 .30 6.6 39 error (invalid witness file) 6.0 3.2 110 300 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 0 wit inspect 78    77    1200   5100 2.0  0   error (recursion) 5.9  3.2  110   320 timeout 97   69   1100 6400 - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c out of memory 0 wit inspect 46    46    490   15000 4.8  0   true 3.0  1.7  60   230 false(no-overflow) 6.7 3.6 110 310 - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c out of memory 0 wit inspect 60    60    760   15000 5.4  0   true 13    6.8  220   720 true 43   27   470 4700 - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c out of memory 0 wit inspect 47    46    520   15000 5.0  0   true 3.5  2.0  64   250 timeout 97   90   1300 470 - -
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c out of memory 0 wit inspect 38    38    500   15000 5.6  0   true 15    7.8  190   900 false(no-overflow) 34   18   300 2300 - -
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c out of memory 0 wit inspect 42    42    470   15000 5.0  0   true 3.0  1.7  49   240 false(no-overflow) 7.1 3.8 110 330 - -
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c out of memory 0 wit inspect 60    60    720   15000 5.0  0   true 3.2  1.8  50   240 false(no-overflow) 8.1 4.3 130 340 - -
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c out of memory 0 wit inspect 83    82    1000   15000 5.0  0   true 3.3  1.9  44   240 false(no-overflow) 9.2 4.9 150 350 - -
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c out of memory 0 wit inspect 61    61    660   15000 5.0  0   true 3.0  1.7  57   230 false(no-overflow) 9.3 4.9 110 330 - -
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c out of memory 0 wit inspect 43    42    400   15000 5.4  0   true 14    7.1  140   720 false(no-overflow) 54   32   480 3500 - -
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c out of memory 0 wit inspect 70    70    860   15000 4.4  0   true 11    5.7  160   580 timeout 97   73   1500 5300 - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_false-no-overflow.c timeout 0 wit inspect 900    900    8900   2500 .84 0   error (invalid witness file) .53 .34 12   43 error (invalid witness file) 5.7 3.1 130 300 - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c out of memory 0 wit inspect 210    210    2500   15000 5.0  0   true 3.2  1.8  68   240 false(no-overflow) 7.4 4.0 140 320 - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c out of memory 0 wit inspect 280    280    3000   15000 5.0  0   true 3.2  1.8  65   240 false(no-overflow) 6.8 3.7 100 320 - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c out of memory 0 wit inspect 290    290    2900   15000 4.2  0   true 3.2  1.8  51   230 false(no-overflow) 7.0 3.7 130 310 - -
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c out of memory 0 wit inspect 200    200    2200   15000 5.0  0   true 4.7  2.6  89   290 false(no-overflow) 11   5.9 190 480 - -
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c out of memory 0 wit inspect 33    32    360   15000 5.0  0   true 2.9  1.7  64   230 false(no-overflow) 7.4 3.9 140 320 - -
termination-crafted-lit/cstrncmp_false-no-overflow.c out of memory 0 wit inspect 67    67    720   15000 5.0  0   true 3.5  2.0  64   240 true 6.9 3.7 120 310 - -
termination-crafted-lit/gcd1_false-no-overflow.c timeout 0 wit inspect 900    900    13000   2600 .99 0   error (invalid witness file) .51 .33 13   40 error (invalid witness file) 5.9 3.1 110 290 - -
termination-crafted-lit/joey_false-no-overflow.c out of memory 0 wit inspect 70    67    950   15000 .99 0   error (invalid witness file) .46 .30 6.8 39 error (invalid witness file) 6.1 3.2 110 310 - -
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 1 wit inspect 890    900    11000   2300 4.0  0   true 3.4  1.9  73   240 false(no-overflow) 8.9 4.8 160 340 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900    900    8200   4700 .84 0   - - error (invalid witness file) .50 .32 7.5 40 error (invalid witness file) 6.0 3.2 120 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c out of memory 0 wit inspect 59    59    750   15000 6.2  0   - - true 46    40    630   520 true 9.5 5.1 170 340
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c out of memory 0 wit inspect 49    49    530   15000 5.9  0   - - true 6.3  3.4  120   290 true 9.0 4.7 140 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c out of memory 0 wit inspect 34    34    460   15000 5.9  0   - - true 5.9  3.2  99   280 timeout 960   820   21000 4800
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c out of memory 0 wit inspect 33    32    340   15000 .99 0   - - error (invalid witness file) .52 .34 12   41 error (invalid witness file) 5.9 3.1 120 290
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c true 2 wit inspect 890    890    9700   1200 3.5  0   - - true 5.4  2.9  100   290 out of memory 460   360   8200 7000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect 2.4  2.4  25   340 4.3  0   - - timeout 900    880    12000   4100 true 44   26   440 1900
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c out of memory 0 wit inspect 110    110    1100   15000 6.4  0   - - true 7.2  3.9  140   290 true 10   5.5 170 350
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c out of memory 0 wit inspect 160    160    1800   15000 6.3  0   - - true 6.8  3.7  47   290 true 11   5.7 210 370
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c out of memory 0 wit inspect 52    52    620   15000 5.1  0   - - true 7.3  3.9  130   310 true 12   6.2 210 380
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c out of memory 0 wit inspect 240    230    2700   15000 9.5  0   - - timeout 900    900    11000   1000 true 10   5.4 170 420
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c timeout 0 wit inspect 900    900    11000   2600 .99 0   - - error (invalid witness file) .58 .37 12   44 error (invalid witness file) 5.7 3.0 120 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 2 wit inspect 890    890    9500   1600 4.0  0   - - true 6.7  3.6  97   310 true 9.9 5.5 140 370
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c out of memory 0 wit inspect 110    110    1300   15000 6.2  0   - - timeout 900    840    13000   6100 timeout 960   840   19000 4600
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c true 2 wit inspect 890    890    8700   940 4.0  0   - - true 6.1  3.3  100   310 true 14   7.9 270 390
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 890    890    10000   980 3.9  0   - - true 6.3  3.4  120   310 true 14   7.5 220 460
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900    900    8500   2600 .99 0   - - error (invalid witness file) .49 .33 7.0 39 error (invalid witness file) 6.2 3.3 130 300
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 0 wit inspect 900    900    7900   2600 .99 0   - - error (invalid witness file) .57 .34 7.9 39 error (invalid witness file) 6.1 3.2 120 300
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c out of memory 0 wit inspect 34    33    310   15000 5.6  0   - - true 11    7.2  170   320 true 22   12   270 590
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c out of memory 0 wit inspect 51    50    510   15000 5.9  0   - - true 6.0  3.3  72   290 true 8.2 4.4 140 330
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c out of memory 0 wit inspect 34    34    400   15000 5.9  0   - - true 6.1  3.3  98   290 timeout 960   820   17000 4800
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c true 2 wit inspect 890    890    10000   1200 4.1  0   - - true 5.2  2.9  91   300 out of memory 450   350   5200 7000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect 2.4  2.4  27   340 5.1  0   - - timeout 900    880    13000   3900 true 45   26   410 1900
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c out of memory 0 wit inspect 58    58    680   15000 5.0  0   - - true 10    5.9  150   420 true 7.4 3.9 160 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c out of memory 0 wit inspect 37    36    370   15000 5.6  0   - - false(no-overflow) 12    7.7  180   430 true 8.8 4.6 160 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c out of memory 0 wit inspect 42    41    510   15000 5.6  0   - - true 10    6.2  140   300 true 8.8 4.7 150 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c out of memory 0 wit inspect 52    51    560   15000 6.5  0   - - true 35    30    390   930 true 9.4 4.9 190 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c out of memory 0 wit inspect 63    63    700   15000 6.4  0   - - true 84    78    510   630 true 10   5.4 200 360
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c out of memory 0 wit inspect 62    62    730   15000 8.2  0   - - true 280    270    1800   950 true 10   5.4 180 380
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 2 wit inspect 900    900    9000   860 4.0  0   - - false(no-overflow) 5.2  2.8  96   290 true 9.1 4.9 160 350
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c out of memory 0 wit inspect 130    130    1600   15000 5.8  0   - - true 31    27    260   430 true 9.0 4.8 170 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c out of memory 0 wit inspect 340    340    4600   15000 5.9  0   - - false(no-overflow) 36    31    430   490 true 8.7 4.7 160 330
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2 wit inspect .83 .82 11   120 4.3  0   - - true 4.7  2.7  95   280 true 120   79   1600 3400
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c true 1 wit inspect 890    890    9400   2800 4.3  0   - - timeout 900    860    18000   4800 timeout 960   850   19000 4900
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c out of memory 0 wit inspect 52    51    630   15000 6.5  0   - - true 22    16    260   450 true 8.8 4.7 170 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c out of memory 0 wit inspect 34    33    370   15000 5.6  0   - - true 11    6.3  130   360 true 24   14   310 690
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c out of memory 0 wit inspect 35    34    410   15000 5.3  0   - - true 11    6.3  160   420 true 8.5 4.4 160 330
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c out of memory 0 wit inspect 33    33    320   15000 5.6  0   - - true 6.4  3.4  91   300 true 9.4 5.2 180 340
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c out of memory 0 wit inspect 37    36    470   15000 5.6  0   - - true 11    6.6  160   320 true 8.9 4.7 160 330
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c out of memory 0 wit inspect 170    170    2000   15000 10    0   - - timeout 900    840    13000   6600 timeout 960   800   14000 4600
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c out of memory 0 wit inspect 130    130    1500   15000 6.1  0   - - true 39    33    280   490 true 8.8 4.7 140 330
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c out of memory 0 wit inspect 110    110    1300   15000 5.1  0   - - false(no-overflow) 6.5  3.4  120   290 true 9.3 4.9 170 320
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900    900    12000   5100 .84 0   - - error (invalid witness file) .52 .36 6.9 41 error (invalid witness file) 5.9 3.1 110 300
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c out of memory 0 wit inspect 200    200    2300   15000 .99 0   - - error (invalid witness file) .53 .34 12   41 error (invalid witness file) 6.2 3.3 120 300
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c out of memory 0 wit inspect 130    130    1500   15000 .99 0   - - error (invalid witness file) .50 .32 12   41 error (invalid witness file) 5.6 3.0 100 300
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 2 wit inspect 890    890    7500   1800 4.0  0   - - true 5.2  2.9  87   280 true 8.7 4.7 150 320
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c out of memory 0 wit inspect 70    70    770   15000 5.6  0   - - true 47    42    480   1100 true 8.9 4.7 160 330
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c out of memory 0 wit inspect 34    34    360   15000 5.3  0   - - true 6.1  3.3  120   310 true 8.0 4.3 150 330
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c out of memory 0 wit inspect 34    34    340   15000 5.3  0   - - true 9.7  5.8  160   300 true 7.6 4.1 150 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c timeout 0 wit inspect 900    900    7600   2500 .99 0   - - error (invalid witness file) .51 .32 7.8 39 error (invalid witness file) 6.1 3.3 130 300
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c out of memory 0 wit inspect 52    52    560   15000 6.0  0   - - true 57    52    460   560 true 9.4 5.0 180 330
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c out of memory 0 wit inspect 61    60    780   15000 5.6  0   - - true 14    9.3  220   320 true 8.5 4.5 180 320
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c out of memory 0 wit inspect 33    33    370   15000 3.9  0   - - out of memory 360    340    4800   7000 true 9.4 5.0 160 330
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c out of memory 0 wit inspect 35    35    470   15000 6.6  0   - - out of memory 490    470    7600   7000 true 9.8 5.2 170 350
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c out of memory 0 wit inspect 90    90    980   15000 8.7  0   - - true 560    560    4200   1100 true 11   5.7 140 420
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c out of memory 0 wit inspect 91    91    960   15000 7.1  0   - - true 170    160    1300   2100 true 10   5.2 170 340
termination-crafted-lit/aviad_true-termination_true-no-overflow.c out of memory 0 wit inspect 46    46    510   15000 5.9  0   - - true 7.7  4.1  99   310 timeout 960   810   15000 4700
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c out of memory 0 wit inspect 51    50    560   15000 5.6  0   - - true 13    7.4  140   380 true 9.4 5.0 160 330
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c out of memory 0 wit inspect 570    570    6400   15000 5.5  0   - - false(no-overflow) 8.9  4.7  130   370 true 9.2 4.9 160 330
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c out of memory 0 wit inspect 49    49    490   15000 5.3  0   - - false(no-overflow) 8.7  4.6  120   340 true 8.4 4.5 160 330
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c out of memory 0 wit inspect 550    550    6400   15000 5.0  0   - - true 12    6.2  190   430 true 9.3 5.0 130 340
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c out of memory 0 wit inspect 570    570    4800   15000 5.5  0   - - false(no-overflow) 9.7  5.1  160   370 true 9.7 5.2 180 350
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2 wit inspect 1.4  1.4  15   220 6.4  0   - - true 21    16    380   730 true 14   7.5 260 470
termination-crafted-lit/strchr_true-no-overflow.c out of memory 0 wit inspect 46    45    470   15000 5.3  0   - - true 12    6.3  140   340 true 8.2 4.5 130 320
termination-numeric/Addition01_false-no-overflow.c out of memory 0 wit inspect 110    110    1400   15000 .84 0   error (invalid witness file) .54 .34 4.5 41 error (invalid witness file) 6.0 3.2 120 290 - -
termination-numeric/Avg_true_false-no-overflow.c out of memory 0 wit inspect 120    110    1600   15000 .99 0   error (invalid witness file) .52 .33 9.0 41 error (invalid witness file) 6.1 3.2 120 290 - -
termination-numeric/Binomial_true-termination_false-no-overflow.c out of memory 0 wit inspect 61    59    720   15000 .84 0   error (invalid witness file) .56 .37 14   43 error (invalid witness file) 6.0 3.2 110 300 - -
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 1 wit inspect 3.6  3.6  45   78 1.7  0   true 3.7  2.1  82   260 false(no-overflow) 13   7.0 200 410 - -
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) 1 wit inspect 8.6  8.6  110   140 1.8  0   error (recursion) 3.5  2.0  63   260 false(no-overflow) 7.6 4.0 150 320 - -
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6  2.6  32   65 2.0  0   true 3.6  2.0  75   260 false(no-overflow) 9.3 4.8 140 350 - -
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 0 wit inspect 5.3  5.3  72   140 2.0  0   true 4.1  2.3  70   270 true 60   38   610 1300 - -
termination-numeric/MultCommutative_false-no-overflow.c out of memory 0 wit inspect 150    140    1700   15000 .84 0   error (invalid witness file) .55 .35 13   39 error (invalid witness file) 6.0 3.2 100 300 - -
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 0 wit inspect 8.5  8.5  88   340 2.0  0   error (recursion) 5.5  3.0  58   300 timeout 97   68   970 5800 - -
termination-numeric/Ackermann01_true-termination_true-no-overflow.c out of memory 0 wit inspect 140    140    1800   15000 .99 0   - - error (invalid witness file) .49 .33 9.0 41 error (invalid witness file) 6.2 3.3 130 300
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c true 1 wit inspect 2.4  2.4  27   160 2.0  0   - - error (recursion) 4.2  2.3  65   250 timeout 960   800   14000 4100
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c out of memory 0 wit inspect 95    92    1200   15000 .84 0   - - error (invalid witness file) .50 .33 13   39 error (invalid witness file) 6.0 3.2 130 300
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c true 2 wit inspect .73 .72 8.5 45 2.0  0   - - error (recursion) 4.0  2.2  89   260 true 9.2 4.9 160 320
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 1 wit inspect 17    17    180   510 2.0  0   - - error (recursion) 3.9  2.2  81   250 timeout 960   790   19000 4800
termination-numeric/Parts_true-termination_true-no-overflow.c out of memory 0 wit inspect 67    62    800   15000 .84 0   - - error (invalid witness file) .53 .35 7.2 43 error (invalid witness file) 6.2 3.3 130 310
termination-numeric/TwoWay_true-termination_true-no-overflow.c true 1 wit inspect 22    22    260   340 2.0  0   - - error (recursion) 3.7  2.1  65   250 unknown 19   12   220 570
termination-numeric/gcd01_true-termination_true-no-overflow.c out of memory 0 wit inspect 110    110    1500   15000 .99 0   - - error (invalid witness file) .50 .32 6.8 40 error (invalid witness file) 5.7 3.0 130 290
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c out of memory 0 wit inspect 33    33    310   15000 5.6  0   - - true 14    9.9  220   340 true 62   37   1100 1100
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 1 wit inspect 1.3  1.3  16   49 1.7  0   - - error (recursion) 3.7  2.1  44   260 timeout 960   800   18000 4300
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 0 wit inspect 900    900    12000   1800 .99 0   - - error (invalid witness file) .50 .32 6.6 40 error (invalid witness file) 5.4 2.9 100 290
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 0 wit inspect 900    900    8600   1800 .84 0   - - error (invalid witness file) .49 .32 6.7 41 error (invalid witness file) 5.6 3.0 110 300
termination-numeric/twisted_true-termination_true-no-overflow.c out of memory 0 wit inspect 32    32    270   15000 .99 0   - - error (invalid witness file) .51 .33 4.8 41 error (invalid witness file) 5.7 3.0 85 300
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 274 69 47000 47000 500000 3100000 1200 0   274 870 470 13000 54000   274 4100 2600 49000 260000   274 11000 10000 150000 100000   274 17000 14000 290000 130000  
    correct results 42 64 12000 12000 120000 21000 180 0   18 77 43 1500 5000   20 160 86 2600 6900   19 2300 2200 32000 18000   19 2200 1800 40000 31000  
        correct true 22 44 7200 7200 74000 12000 100 0   7 0 0 0 0   11 0 0 0 0   18 2300 2200 32000 18000   19 2200 1800 40000 31000  
        correct false 20 20 4500 4500 46000 8300 78 0   11 77 43 1500 5000   9 160 86 2600 6900   1 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 14 5 5200 5200 52000 21000 62 0   5 130 70 1200 7400   4 560 360 5900 35000   0 920 870 18000 5900   0 3900 3300 70000 19000  
        correct-unconfirmed true 5 5 940 940 9900 3900 12 0   5 0 0 0 0   4 0 0 0 0   0 920 870 18000 5900   0 3900 3300 70000 19000  
        correct-unconfirmed false 9 0 4200 4200 42000 17000 50 0   0 130 70 1200 7400   0 560 360 5900 35000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (274 tasks, max score: 393) 69
Run set sv-comp17.Overflows-BitVectors