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:24:14 CET [[ 2017-01-15 01:24:24 CET ]] [[ 2017-01-15 01:40:44 CET ]] [[ 2017-01-15 01:25:54 CET ]] [[ 2017-01-15 01:44:51 CET ]]
Run set sv-comp17.Overflows-Other
Options -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0924.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0924.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0924.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0924.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 .076 .076 1.0  23 .99 0   error (recursion) 3.2  1.8  66   250 false(no-overflow) 9.0 4.8 98 310 - -
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .11  .11  .77 23 .99 0   error (recursion) 3.4  1.9  61   250 false(no-overflow) 8.5 4.4 130 320 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c unknown 0 wit inspect .076 .077 .85 23 .99 0   error (invalid witness file) .50 .33 9.0 40 error (invalid witness file) 7.3 3.9 80 300 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     10000    4700 .84 0   - - error (invalid witness file) .48 .33 7.4 39 error (invalid witness file) 7.1 3.8 76 300
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     8000    4700 .99 0   - - error (invalid witness file) .55 .36 13   39 error (invalid witness file) 7.0 3.7 80 300
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     9300    4800 .99 0   - - error (invalid witness file) .48 .30 10   39 error (invalid witness file) 6.1 3.3 100 290
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     8200    4800 .99 0   - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 5.7 3.0 93 300
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 370     360     3400    15000 .84 0   - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 5.6 3.0 110 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 340     340     3500    15000 .99 0   - - error (invalid witness file) .54 .37 13   40 error (invalid witness file) 6.7 3.5 88 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 350     350     3300    15000 .99 0   - - error (invalid witness file) .52 .33 11   43 error (invalid witness file) 6.7 3.5 86 300
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .11  .11  .72 23 .84 0   - - true 3.5  1.9  61   250 true 9.0 4.8 98 330
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .11  .11  .66 23 .99 0   - - error (invalid witness file) .53 .33 12   42 error (invalid witness file) 7.9 4.2 75 310
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .072 .072 .90 23 .99 0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 7.7 4.1 72 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     10000    1300 .99 0   - - error (invalid witness file) .51 .33 10   39 error (invalid witness file) 6.5 3.5 89 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .99  .98  13    32 .99 0   - - error (recursion) 3.3  1.9  45   250 true 38   22   650 1300
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     8100    1200 .99 0   - - error (invalid witness file) .53 .34 12   39 error (invalid witness file) 5.5 2.9 93 300
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     8700    1200 .99 0   - - error (invalid witness file) .52 .35 12   39 error (invalid witness file) 7.2 3.8 96 300
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     9500    2300 .84 0   - - error (invalid witness file) .50 .34 12   39 error (invalid witness file) 7.7 4.0 82 320
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     8400    5700 .84 0   - - error (invalid witness file) .52 .33 12   39 error (invalid witness file) 7.9 4.1 97 320
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     7700    5700 .84 0   - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 7.3 3.8 71 300
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     7100    4300 .99 0   - - error (invalid witness file) .54 .34 12   42 error (invalid witness file) 7.0 3.7 80 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 330     330     2500    15000 .99 0   - - error (invalid witness file) .48 .33 13   40 error (invalid witness file) 6.5 3.5 79 280
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     9500    980 .99 0   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.3 3.3 110 300
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     10000    930 .99 0   - - error (invalid witness file) .47 .32 9.4 39 error (invalid witness file) 7.2 3.7 97 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 600     600     5900    15000 .99 0   - - error (invalid witness file) .56 .36 12   44 error (invalid witness file) 6.5 3.4 130 310
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 9.1   9.1   120    170 .84 0   - - error (recursion) 3.1  1.8  32   240 timeout 960   790   14000 4300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 9.0   9.0   120    170 .84 0   - - error (recursion) 3.4  1.9  41   250 timeout 960   790   15000 4000
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .097 .096 .78 23 .99 0   true 3.1  1.7  61   230 false(no-overflow) 7.6 4.0 160 320 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .10  .10  .89 23 .99 0   true 3.0  1.7  65   230 false(no-overflow) 7.2 3.9 130 310 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .095 .094 .79 23 .99 0   true 3.1  1.7  65   230 false(no-overflow) 7.7 4.2 120 310 - -
bitvector/jain_5_false-no-overflow.i out of memory 0 wit inspect 97     93     1300    15000 .84 0   error (invalid witness file) .50 .31 11   40 error (invalid witness file) 6.7 3.6 75 290 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .083 .083 .89 23 .84 0   true 2.9  1.6  66   240 false(no-overflow) 9.6 5.1 92 320 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .079 .078 .76 23 .99 0   true 3.0  1.7  65   240 false(no-overflow) 7.7 4.1 140 320 - -
bitvector/modulus_false-no-overflow.i false(no-overflow) 0 wit inspect .091 .090 .78 23 .84 0   true 3.2  1.8  67   240 true 7.0 3.8 140 320 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .21  .21  3.0  25 .84 0   - - true 12    6.1  130   460 true 10   5.4 110 320
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .26  .25  2.7  26 .99 0   - - true 11    5.7  170   450 true 8.3 4.5 120 330
bitvector/byte_add_false-unreach-call_true-no-overflow.i true 2 wit inspect .30  .30  3.7  30 .99 0   - - true 20    10    230   620 true 9.5 5.1 140 320
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .11  .11  .67 23 .84 0   - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 6.8 3.6 110 300
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .076 .075 .84 23 .84 0   - - error (invalid witness file) .53 .34 13   41 error (invalid witness file) 7.4 3.9 97 310
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .098 .098 .79 23 .99 0   - - error (invalid witness file) .51 .34 12   40 error (invalid witness file) 5.7 3.0 85 300
bitvector/gcd_4_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .095 .093 .93 23 .84 0   - - error (invalid witness file) .51 .33 9.6 41 error (invalid witness file) 7.8 4.1 88 320
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .13  .13  1.3  23 .99 0   - - true 4.8  2.6  68   290 true 8.7 4.6 110 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 320     310     4300    15000 .84 0   - - error (invalid witness file) .50 .32 10   40 error (invalid witness file) 6.2 3.3 98 290
bitvector/jain_2_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 310     300     3700    15000 .84 0   - - error (invalid witness file) .50 .33 14   40 error (invalid witness file) 6.8 3.6 80 300
bitvector/jain_4_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 310     300     3800    15000 .84 0   - - error (invalid witness file) .52 .33 13   41 error (invalid witness file) 7.5 3.9 71 300
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 340     320     5000    15000 .99 0   - - error (invalid witness file) .50 .34 12   39 error (invalid witness file) 6.5 3.5 100 290
bitvector/jain_6_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 320     310     4100    15000 .99 0   - - error (invalid witness file) .49 .32 10   39 error (invalid witness file) 5.4 2.9 87 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 310     310     3600    15000 .99 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.6 3.5 78 300
bitvector/modulus_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     900     6500    2700 .99 0   - - error (invalid witness file) .51 .33 10   41 error (invalid witness file) 6.0 3.1 83 300
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .12  .12  1.2  23 .84 0   - - true 4.5  2.5  36   280 true 7.9 4.2 150 350
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .16  .16  1.5  23 .84 0   - - true 4.5  2.5  61   280 true 7.4 4.0 140 330
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.7   9.7   110    210 .99 0   - - true 5.1  2.8  43   280 true 8.1 4.4 100 310
bitvector/sum02_false-unreach-call_true-no-overflow.i out of memory 0 wit inspect 200     200     2800    15000 .99 0   - - error (invalid witness file) .48 .31 10   40 error (invalid witness file) 5.9 3.2 93 300
bitvector/sum02_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 210     210     2500    15000 .99 0   - - error (invalid witness file) .54 .35 12   41 error (invalid witness file) 5.9 3.1 130 290
../../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 27 17000     17000     170000    260000 50    0   54 26   15   530 2000   54 78   42   1200 3100   54 91   51   1300 5000   54 2200 1800 34000 22000  
    correct results 16 25 13     13     140    580 15    0   5 22   12   450 1700   7 57   30   870 2200   8 68   36   840 3200   9 110 58 1600 3900  
        correct true 9 18 12     12     140    410 8.3  0   5 0   0   0 0   0 0   0   0 0   8 68   36   840 3200   9 110 58 1600 3900  
        correct false 7 7 .64  .64  5.9  160 6.8  0   0 22   12   450 1700   7 57   30   870 2200   0 0   0   0 0   0 0 0 0 0  
    correct-unconfimed results 3 2 18     18     240    370 2.5  0   1 3.2 1.8 67 240   1 7.0 3.8 140 320   0 6.6 3.7 73 490   0 1900 1600 30000 8300  
        correct-unconfirmed true 2 2 18     18     240    350 1.7  0   1 0   0   0 0   1 0   0   0 0   0 6.6 3.7 73 490   0 1900 1600 30000 8300  
        correct-unconfirmed false 1 0 .091 .090 .78 23 .84 0   0 3.2 1.8 67 240   0 7.0 3.8 140 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) 27
Run set sv-comp17.Overflows-Other