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:59:26 CET [[ 2017-01-15 01:13:08 CET ]] [[ 2017-01-15 01:19:20 CET ]] [[ 2017-01-15 01:18:26 CET ]] [[ 2017-01-15 01:22:10 CET ]]
Run set sv-comp17.Overflows-Other
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0859.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 .11  .11  .73 23 .84 0   error (recursion) 3.3  1.8  71 250 false(no-overflow) 7.6 4.0 83 330 - -
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .080 .080 .83 23 .84 0   error (recursion) 3.5  1.9  78 260 false(no-overflow) 7.7 4.1 110 330 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c unknown 0 wit inspect .085 .085 .87 23 .99 0   error (invalid witness file) .54 .33 12 39 error (invalid witness file) 9.2 4.8 70 310 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     8100    5600 .84 0   - - error (invalid witness file) .55 .35 11   42 error (invalid witness file) 6.0 3.2 120 300
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     7000    5700 .99 0   - - error (invalid witness file) .67 .43 12   40 error (invalid witness file) 5.8 3.1 110 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     6900    5700 .84 0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 6.4 3.4 140 310
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     7100    5700 .99 0   - - error (invalid witness file) .59 .38 12   42 error (invalid witness file) 6.9 3.6 120 310
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 570     570     3500    15000 .99 0   - - error (invalid witness file) .54 .34 13   43 error (invalid witness file) 5.8 3.1 120 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 560     560     4000    15000 .84 0   - - error (invalid witness file) .52 .32 10   40 error (invalid witness file) 5.7 3.0 120 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 570     570     4100    15000 .99 0   - - error (invalid witness file) .51 .32 11   41 error (invalid witness file) 5.8 3.1 130 290
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     890     9100    920 .99 0   - - error (invalid witness file) .49 .33 11   39 error (invalid witness file) 5.9 3.1 110 300
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .11  .11  .65 23 .99 0   - - error (invalid witness file) .47 .31 9.7 40 error (invalid witness file) 5.5 2.9 64 300
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .11  .11  .64 23 .99 0   - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 5.7 3.0 120 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     10000    9700 .84 0   - - error (invalid witness file) .48 .30 11   39 error (invalid witness file) 5.8 3.1 130 290
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 300     290     4500    15000 .99 0   - - error (invalid witness file) .61 .39 7.8 40 error (invalid witness file) 6.3 3.3 68 310
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     9600    3900 .99 0   - - error (invalid witness file) .50 .34 11   41 error (invalid witness file) 6.3 3.3 120 300
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     9200    9700 .84 0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 5.9 3.2 110 300
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     9700    9700 .84 0   - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 5.8 3.1 110 300
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     10000    9900 .99 0   - - error (invalid witness file) .51 .34 11   42 error (invalid witness file) 6.1 3.3 120 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     8800    10000 .84 0   - - error (invalid witness file) .59 .38 12   42 error (invalid witness file) 5.8 3.1 110 300
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     7600    11000 .99 0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.1 3.2 120 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 250     250     1700    15000 .99 0   - - error (invalid witness file) .52 .33 13   42 error (invalid witness file) 6.0 3.2 120 290
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     10000    960 .99 0   - - error (invalid witness file) .50 .34 10   39 error (invalid witness file) 6.0 3.2 130 300
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     10000    500 .99 0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.1 3.2 130 290
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 610     610     4800    15000 .99 0   - - error (invalid witness file) .52 .34 11   41 error (invalid witness file) 5.5 2.9 110 290
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     9400    3300 .99 0   - - error (invalid witness file) .52 .35 13   39 error (invalid witness file) 6.2 3.3 120 290
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     13000    3300 .99 0   - - error (invalid witness file) .48 .31 11   40 error (invalid witness file) 5.2 2.8 110 280
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .074 .076 .75 23 .99 0   true 3.1  1.8  64 240 false(no-overflow) 7.2 3.8 93 320 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .11  .11  .84 23 .99 0   true 3.0  1.7  64 240 false(no-overflow) 7.8 4.2 170 320 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .080 .081 .86 23 .99 0   true 3.2  1.8  70 240 false(no-overflow) 7.2 3.9 130 320 - -
bitvector/jain_5_false-no-overflow.i out of memory 0 wit inspect 110     110     1500    15000 .84 0   error (invalid witness file) .48 .32 12 40 error (invalid witness file) 5.9 3.1 74 310 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .11  .11  .98 23 .84 0   true 3.1  1.8  76 240 false(no-overflow) 7.3 3.9 110 320 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .10  .10  .86 23 .99 0   true 3.0  1.7  62 240 false(no-overflow) 7.2 3.8 130 310 - -
bitvector/modulus_false-no-overflow.i false(no-overflow) 0 wit inspect .10  .10  .82 23 .84 0   true 3.2  1.8  74 240 true 7.3 3.9 110 320 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 450     440     5000    15000 .99 0   - - error (invalid witness file) .49 .33 13   40 error (invalid witness file) 6.0 3.2 130 300
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 380     380     5100    15000 .99 0   - - error (invalid witness file) .51 .32 9.5 39 error (invalid witness file) 5.8 3.1 110 300
bitvector/byte_add_false-unreach-call_true-no-overflow.i out of memory 0 wit inspect 450     440     5300    15000 .84 0   - - error (invalid witness file) .48 .32 11   40 error (invalid witness file) 6.1 3.2 130 300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .089 .089 .83 23 .99 0   - - error (invalid witness file) .52 .31 9.2 40 error (invalid witness file) 5.8 3.1 120 290
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .086 .086 .67 23 .99 0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 5.9 3.1 130 300
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .071 .071 1.0  23 .99 0   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.1 3.2 110 300
bitvector/gcd_4_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .083 .082 .70 23 .99 0   - - error (invalid witness file) .47 .31 7.8 40 error (invalid witness file) 6.6 3.5 120 300
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     870     14000    2600 .99 0   - - error (invalid witness file) .51 .34 12   39 error (invalid witness file) 6.0 3.1 120 300
bitvector/jain_1_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     890     9900    790 .84 0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.8 3.1 120 290
bitvector/jain_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     890     11000    780 .99 0   - - error (invalid witness file) .54 .35 12   40 error (invalid witness file) 5.9 3.2 120 290
bitvector/jain_4_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     890     11000    780 .99 0   - - error (invalid witness file) .51 .33 11   42 error (invalid witness file) 6.5 3.4 120 300
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     850     13000    12000 .99 0   - - error (invalid witness file) .54 .36 13   43 error (invalid witness file) 6.2 3.3 120 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     890     9500    760 .99 0   - - error (invalid witness file) .51 .33 11   42 error (invalid witness file) 6.5 3.4 120 310
bitvector/jain_7_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     890     10000    760 .84 0   - - error (invalid witness file) .55 .37 12   41 error (invalid witness file) 6.0 3.2 110 290
bitvector/modulus_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     900     12000    4800 .99 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.0 3.2 130 310
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 140     130     1800    15000 .99 0   - - error (invalid witness file) .54 .36 13   40 error (invalid witness file) 6.4 3.4 120 300
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 140     130     1800    15000 .97 0   - - error (invalid witness file) .53 .35 11   40 error (invalid witness file) 6.6 3.5 120 320
bitvector/parity_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     880     6900    700 .84 0   - - error (invalid witness file) .60 .39 8.0 40 error (invalid witness file) 5.9 3.2 110 300
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     880     9000    770 .99 0   - - error (invalid witness file) .57 .38 13   41 error (invalid witness file) 5.8 3.1 120 300
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     880     9100    750 .99 0   - - error (invalid witness file) .55 .36 9.4 44 error (invalid witness file) 5.6 3.0 110 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 7 29000    29000    300000    300000 51    0   54 26   15   580 2000 54 74   39   1100 3200 54 23 15 490 1800   54 260 140 5100 13000  
    correct results 7 7 .67 .67 5.9  160 6.5  0   5 22   13   480 1700 7 52   28   830 2200 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 7 7 .67 .67 5.9  160 6.5  0   0 22   13   480 1700 7 52   28   830 2200 0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 1 0 .10 .10 .82 23 .84 0   1 3.2 1.8 74 240 1 7.3 3.9 110 320 0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 1 0 .10 .10 .82 23 .84 0   0 3.2 1.8 74 240 0 7.3 3.9 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) 7
Run set sv-comp17.Overflows-Other