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 09:57:49 CET [[ 2017-01-15 01:31:06 CET ]] [[ 2017-01-15 01:47:27 CET ]] [[ 2017-01-15 01:32:35 CET ]] [[ 2017-01-15 01:49:35 CET ]]
Run set sv-comp17.Overflows-Other
Options -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0957.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0957.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0957.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0957.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)
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .10  .10  .94 23 .84 0   error (recursion) 3.6  2.0  58 250 false(no-overflow) 8.7 4.6 96 310 - -
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .081 .080 .96 23 .84 0   error (recursion) 3.1  1.8  53 250 false(no-overflow) 7.0 3.8 140 330 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c unknown 0 wit inspect .080 .081 .74 23 .99 0   error (invalid witness file) .51 .32 13 40 error (invalid witness file) 5.9 3.2 99 300 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     11000    5300 .99 0   - - error (invalid witness file) .72 .45 9.0 44 error (invalid witness file) 5.2 2.8 96 300
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     9200    5300 .84 0   - - error (invalid witness file) .53 .35 13   39 error (invalid witness file) 5.9 3.1 120 310
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     11000    5500 .99 0   - - error (invalid witness file) .52 .32 12   39 error (invalid witness file) 6.3 3.4 82 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     8400    5500 .99 0   - - error (invalid witness file) .63 .40 7.4 43 error (invalid witness file) 5.6 3.0 84 290
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 330     320     2900    15000 .99 0   - - error (invalid witness file) .51 .34 11   39 error (invalid witness file) 7.8 4.1 80 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 320     310     3700    15000 .99 0   - - error (invalid witness file) .51 .32 10   40 error (invalid witness file) 6.5 3.4 82 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 340     330     3300    15000 .84 0   - - error (invalid witness file) .51 .33 8.3 42 error (invalid witness file) 7.8 4.1 93 300
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .12  .12  .70 23 .84 0   - - true 3.2  1.8  36   240 true 9.1 4.9 83 320
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .10  .10  .84 23 .99 0   - - error (invalid witness file) .52 .34 11   41 error (invalid witness file) 7.2 3.9 71 300
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .095 .094 .82 23 .96 0   - - error (invalid witness file) .52 .32 13   41 error (invalid witness file) 7.2 3.8 89 290
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     10000    1500 .99 0   - - error (invalid witness file) .52 .35 13   40 error (invalid witness file) 6.9 3.6 67 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 1.8   1.8   22    46 .99 0   - - error (recursion) 3.2  1.8  39   240 true 49   28   520 1300
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     8200    1400 .84 0   - - error (invalid witness file) .49 .33 12   41 error (invalid witness file) 6.4 3.4 86 290
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     8500    1400 .99 0   - - error (invalid witness file) .52 .32 11   39 error (invalid witness file) 6.5 3.5 82 290
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     7900    1400 .84 0   - - error (invalid witness file) .59 .37 13   44 error (invalid witness file) 5.7 3.1 87 290
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     10000    6500 .84 0   - - error (invalid witness file) .52 .35 11   40 error (invalid witness file) 7.0 3.8 78 290
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     8400    6100 .99 0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.2 2.8 110 300
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     7400    4100 .99 0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 5.8 3.1 120 290
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 410     410     3400    15000 .99 0   - - error (invalid witness file) .55 .35 14   44 error (invalid witness file) 6.1 3.2 100 310
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     9300    1000 .99 0   - - error (invalid witness file) .54 .37 12   41 error (invalid witness file) 5.6 3.0 120 300
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     9500    950 .99 0   - - error (invalid witness file) .54 .35 11   41 error (invalid witness file) 6.2 3.3 76 280
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 560     560     4800    15000 .99 0   - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.2 3.3 120 310
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 12     12     170    250 .99 0   - - error (recursion) 4.2  2.4  28   250 timeout 960   790   17000 3600
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 12     12     140    250 .98 0   - - error (recursion) 3.3  1.9  62   240 timeout 960   790   15000 3900
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .081 .082 .84 23 .99 0   true 3.2  1.9  46 230 false(no-overflow) 8.7 4.6 110 310 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .096 .095 .90 23 .99 0   true 3.1  1.7  64 240 false(no-overflow) 9.8 5.2 98 320 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .12  .12  .78 23 .99 0   true 3.2  1.8  72 240 false(no-overflow) 8.6 4.6 100 320 - -
bitvector/jain_5_false-no-overflow.i out of memory 0 wit inspect 150     150     2100    15000 .99 0   error (invalid witness file) .51 .33 12 40 error (invalid witness file) 6.8 3.6 73 300 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .095 .094 .74 23 .99 0   true 3.1  1.7  64 240 false(no-overflow) 8.7 4.6 95 310 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .10  .10  .86 23 .84 0   true 3.2  1.8  66 230 false(no-overflow) 9.7 5.1 89 320 - -
bitvector/modulus_false-no-overflow.i false(no-overflow) 0 wit inspect .077 .077 .83 23 .99 0   true 3.1  1.8  58 240 true 8.6 4.6 80 320 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .12  .12  1.5  24 .99 0   - - true 14    7.5  120   450 true 9.0 4.9 130 330
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .13  .13  1.4  24 .84 0   - - true 13    6.7  110   440 true 8.1 4.4 180 330
bitvector/byte_add_false-unreach-call_true-no-overflow.i true 2 wit inspect .14  .14  1.9  24 .84 0   - - true 19    9.7  220   460 true 8.9 4.8 120 320
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .073 .073 .88 23 .99 0   - - error (invalid witness file) .60 .39 8.3 41 error (invalid witness file) 5.7 3.0 97 300
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .094 .094 .72 23 .99 0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.5 3.4 100 310
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .10  .11  .68 23 .99 0   - - error (invalid witness file) .52 .34 12   43 error (invalid witness file) 7.2 3.8 79 300
bitvector/gcd_4_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .091 .090 1.0  23 .84 0   - - error (invalid witness file) .52 .35 10   40 error (invalid witness file) 6.4 3.4 70 280
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .078 .077 1.1  23 .99 0   - - true 4.6  2.5  58   290 true 7.0 3.7 150 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .080 .080 .90 23 .99 0   - - true 4.6  2.5  86   280 true 6.7 3.6 140 310
bitvector/jain_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .099 .098 .75 23 .99 0   - - true 4.3  2.4  82   280 true 6.4 3.4 140 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect .094 .093 .74 23 .99 0   - - true 4.4  2.5  92   280 true 8.2 4.4 95 320
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect .099 .098 .71 23 .99 0   - - true 4.1  2.3  81   270 true 8.1 4.3 85 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect .10  .10  .78 23 .84 0   - - true 4.9  2.7  47   290 true 6.8 3.6 130 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i true 2 wit inspect .079 .078 .76 23 .99 0   - - true 4.4  2.5  76   300 true 7.4 4.0 95 310
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect .095 .094 .96 23 .99 0   - - true 5.5  3.0  88   280 error (1) 7.5 4.0 160 310
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .081 .080 .91 23 .99 0   - - true 4.5  2.5  32   280 true 7.7 4.1 120 320
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .12  .12  .79 23 .99 0   - - true 4.4  2.4  39   280 true 7.5 4.0 120 330
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect .087 .086 .96 23 .99 0   - - true 5.1  2.8  66   280 true 8.4 4.5 93 320
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect .091 .091 1.0  23 .99 0   - - true 5.4  3.0  52   280 true 8.4 4.4 92 320
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect .076 .076 1.1  23 .99 0   - - true 4.6  2.6  84   280 true 8.5 4.5 99 320
../../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 54 45 14000     14000     140000    140000 52    0   54 27   15   510 2000   54 82   44   980 3100   54 130   74   1800 7000   54 2300 1800 36000 21000  
    correct results 25 43 4.2   4.2   44    610 24    0   5 22   13   420 1700   7 61   32   730 2200   17 110   61   1400 5500   17 180 99 2600 6700  
        correct true 18 36 3.5   3.5   38    440 17    0   5 0   0   0 0   0 0   0   0 0   17 110   61   1400 5500   17 180 99 2600 6700  
        correct false 7 7 .68  .67  6.0  160 6.5  0   0 22   13   420 1700   7 61   32   730 2200   0 0   0   0 0   0 0 0 0 0  
    correct-unconfimed results 3 2 24     24     310    520 3.0  0   1 3.1 1.8 58 240   1 8.6 4.6 80 320   0 7.5 4.2 90 490   0 1900 1600 32000 7500  
        correct-unconfirmed true 2 2 24     24     310    500 2.0  0   1 0   0   0 0   1 0   0   0 0   0 7.5 4.2 90 490   0 1900 1600 32000 7500  
        correct-unconfirmed false 1 0 .077 .077 .83 23 .99 0   0 3.1 1.8 58 240   0 8.6 4.6 80 320   0 0   0   0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (54 tasks, max score: 98) 45
Run set sv-comp17.Overflows-Other