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-Other
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)
recursive/Addition02WithOverflowBug_false-no-overflow.c out of memory 0 wit inspect 110    110    1300   15000 .99 0   error (invalid witness file) .51 .33 8.1 42 error (invalid witness file) 6.9 3.6 110 320 - -
recursive/Addition03_false-no-overflow.c out of memory 0 wit inspect 110    110    1400   15000 .99 0   error (invalid witness file) .50 .33 9.8 40 error (invalid witness file) 5.9 3.1 110 300 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect 2.2  2.2  28   160 1.7  0   true 6.5  3.5  110   320 false(no-overflow) 61   33   490 4700 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 150    140    2000   15000 .99 0   - - error (invalid witness file) .49 .32 9.4 40 error (invalid witness file) 6.1 3.3 130 300
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 150    140    2000   15000 .84 0   - - error (invalid witness file) .53 .34 4.7 40 error (invalid witness file) 6.2 3.3 120 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 150    150    2100   15000 .99 0   - - error (invalid witness file) .53 .33 9.7 42 error (invalid witness file) 6.1 3.2 120 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 150    150    1900   15000 .99 0   - - error (invalid witness file) .51 .32 7.2 40 error (invalid witness file) 5.9 3.1 130 300
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 120    110    1600   15000 .99 0   - - error (invalid witness file) .51 .33 4.3 40 error (invalid witness file) 6.1 3.2 120 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 120    110    1300   15000 .99 0   - - error (invalid witness file) .52 .34 3.6 42 error (invalid witness file) 5.7 3.1 91 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 120    110    1600   15000 .99 0   - - error (invalid witness file) .51 .34 5.7 40 error (invalid witness file) 6.5 3.4 130 320
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .49 .48 5.9 44 1.7  0   - - true 4.2  2.3  70   260 true 8.0 4.2 160 320
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 2.4  2.4  29   160 1.7  0   - - error (recursion) 4.2  2.3  88   260 timeout 960   800   12000 4100
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 2.4  2.4  28   160 2.0  0   - - error (recursion) 3.8  2.2  46   250 timeout 960   800   14000 4800
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 92    89    1000   15000 .84 0   - - error (invalid witness file) .48 .30 6.5 39 error (invalid witness file) 6.0 3.2 120 290
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .14 .14 1.8 23 2.0  0   - - error (recursion) 3.4  1.9  63   250 true 37   21   540 940
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 94    92    1100   15000 .99 0   - - error (invalid witness file) .56 .37 4.5 42 error (invalid witness file) 6.6 3.5 130 320
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 97    94    1100   15000 .99 0   - - error (invalid witness file) .48 .32 7.0 41 error (invalid witness file) 5.9 3.2 120 300
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 96    94    1400   15000 .84 0   - - error (invalid witness file) .53 .34 4.5 43 error (invalid witness file) 5.6 2.9 110 300
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 130    120    1700   15000 .84 0   - - error (invalid witness file) .50 .31 9.6 39 error (invalid witness file) 5.8 3.1 120 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 130    120    1800   15000 .84 0   - - error (invalid witness file) .61 .38 6.7 42 error (invalid witness file) 6.7 3.5 140 320
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 150    150    1900   15000 .99 0   - - error (invalid witness file) .54 .33 13   40 error (invalid witness file) 5.8 3.1 110 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 190    180    2400   15000 .99 0   - - error (invalid witness file) .50 .33 6.4 40 error (invalid witness file) 6.4 3.4 130 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 120    120    1400   15000 .99 0   - - error (invalid witness file) .51 .33 5.4 40 error (invalid witness file) 6.1 3.2 110 300
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 110    110    1500   15000 .84 0   - - error (invalid witness file) .50 .32 9.1 40 error (invalid witness file) 6.0 3.2 130 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 110    110    1500   15000 .99 0   - - error (invalid witness file) .47 .31 3.8 40 error (invalid witness file) 6.0 3.2 120 300
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 1.3  1.3  17   50 2.0  0   - - error (recursion) 4.1  2.3  82   270 timeout 960   800   17000 3800
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 1.3  1.3  15   50 2.0  0   - - error (recursion) 3.7  2.1  43   250 timeout 960   800   11000 3900
bitvector/jain_1_false-no-overflow.i out of memory 0 wit inspect 52    52    530   15000 5.4  0   true 13    6.9  130   720 false(no-overflow) 52   29   520 3600 - -
bitvector/jain_2_false-no-overflow.i out of memory 0 wit inspect 56    55    680   15000 5.6  0   true 14    7.5  160   900 timeout 97   55   850 6400 - -
bitvector/jain_4_false-no-overflow.i out of memory 0 wit inspect 67    67    690   15000 5.1  0   true 26    13    280   1200 out of memory 90   51   700 7000 - -
bitvector/jain_5_false-no-overflow.i false(no-overflow) 0 wit inspect 3.3  3.3  40   350 5.3  0   timeout 93    82    1400   3700 true 7.1 3.8 110 320 - -
bitvector/jain_6_false-no-overflow.i out of memory 0 wit inspect 70    70    670   15000 5.9  0   true 23    12    250   1200 false(no-overflow) 68   44   580 3300 - -
bitvector/jain_7_false-no-overflow.i out of memory 0 wit inspect 65    65    720   15000 5.9  0   true 23    12    260   1200 false(no-overflow) 73   47   1100 3100 - -
bitvector/modulus_false-no-overflow.i out of memory 0 wit inspect 880    880    10000   15000 4.0  0   true 3.1  1.7  56   240 true 7.1 3.8 110 310 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 140    140    1700   15000 8.7  0   - - true 16    8.3  180   580 true 10   5.3 130 420
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 140    140    1800   15000 8.7  0   - - true 16    8.4  200   580 true 10   5.4 160 420
bitvector/byte_add_false-unreach-call_true-no-overflow.i out of memory 0 wit inspect 200    200    2200   15000 9.2  0   - - true 24    12    190   870 true 11   5.7 180 430
bitvector/gcd_1_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 35    35    400   15000 5.9  0   - - true 7.2  3.9  120   330 true 9.5 5.1 170 330
bitvector/gcd_2_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 36    35    430   15000 5.1  0   - - true 8.0  4.3  150   330 true 9.3 4.9 170 330
bitvector/gcd_3_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 36    35    390   15000 5.1  0   - - true 7.5  4.1  100   320 true 9.5 5.0 150 330
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect .77 .77 8.2 100 5.0  0   - - true 4.7  2.6  100   280 true 14   7.5 200 450
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .70 .70 8.6 100 4.2  0   - - true 4.6  2.6  84   280 true 7.4 3.9 150 320
bitvector/jain_1_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 74    73    790   15000 5.7  0   - - true 13    7.8  230   450 true 8.2 4.3 160 310
bitvector/jain_2_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 66    66    690   15000 5.9  0   - - true 17    12    230   450 true 7.6 4.0 150 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 61    61    590   15000 6.2  0   - - true 19    14    210   440 true 7.3 3.9 150 300
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.1  5.1  59   1200 16    0   - - true 440    430    4400   1600 true 11   5.7 210 560
bitvector/jain_6_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 60    60    660   15000 5.6  0   - - true 17    12    190   450 true 7.9 4.2 140 320
bitvector/jain_7_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 60    60    720   15000 6.0  0   - - true 16    10    200   450 true 7.3 3.9 150 300
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 900    900    10000   15000 6.3  0   - - true 8.5  4.5  81   360 error (1) 9.0 4.8 170 330
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.7  1.7  18   170 5.0  0   - - true 5.0  2.7  100   280 true 7.2 3.9 140 320
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.5  1.5  16   190 5.0  0   - - true 4.4  2.5  54   280 true 7.3 3.9 130 310
bitvector/parity_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 47    47    520   15000 4.9  0   - - true 7.2  3.9  120   290 true 8.5 4.4 160 330
bitvector/sum02_false-unreach-call_true-no-overflow.i out of memory 0 wit inspect 50    49    540   15000 5.6  0   - - true 16    10    190   450 true 7.7 4.1 150 310
bitvector/sum02_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 50    50    500   15000 4.8  0   - - true 18    13    240   450 true 8.2 4.3 150 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 21 5600   5600   68000 620000 200   0   54 200   140   2600 9500   54 470   270   4700 29000   54 700 580   7900 12000   54 4200 3400 60000 30000  
    correct results 9 17 910   910   10000 17000 47   0   1 6.5 3.5 110 320   1 61   33   490 4700   7 470 450   4900 3600   7 100 55 1700 3600  
        correct true 8 16 910   910   10000 17000 46   0   1 0   0   0 0   0 0   0   0 0   7 470 450   4900 3600   7 100 55 1700 3600  
        correct false 1 1 2.2 2.2 28 160 1.7 0   0 6.5 3.5 110 320   1 61   33   490 4700   0 0 0   0 0   0 0 0 0 0  
    correct-unconfimed results 5 4 11   11   130 770 13   0   0 93   82   1400 3700   1 7.1 3.8 110 320   0 16 8.8 260 1000   0 3800 3200 54000 17000  
        correct-unconfirmed true 4 4 7.4 7.4 89 420 7.6 0   0 0   0   0 0   1 0   0   0 0   0 16 8.8 260 1000   0 3800 3200 54000 17000  
        correct-unconfirmed false 1 0 3.3 3.3 40 350 5.3 0   0 93   82   1400 3700   0 7.1 3.8 110 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) 21
Run set sv-comp17.Overflows-Other