Tool CBMC 5.6
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-11 13:54:34 CET [[ 2017-01-14 21:55:46 CET ]] [[ 2017-01-14 22:15:53 CET ]] [[ 2017-01-14 21:57:58 CET ]] [[ 2017-01-14 22:18:07 CET ]]
Run set sv-comp17.Overflows-Other
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1354.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1354.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1354.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1354.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 .12 .12  1.4  19 .0041 0      exception 3.6  2.0  38 210 false(no-overflow) 8.4 4.5 160 330 - -
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .16 .15  1.2  19 .0041 0      exception 3.5  2.0  42 220 false(no-overflow) 11   5.7 160 370 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .12 .11  .96 17 .0041 0      exception 3.5  1.9  53 220 false(no-overflow) 11   5.8 110 330 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 850    850     2400    300 .95   0      - - error (invalid witness file) .68 .43 8.1 40 error (invalid witness file) 6.2 3.3 100 300
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     4200    320 .93   0      - - error (invalid witness file) .53 .34 10   39 error (invalid witness file) 5.8 3.1 110 300
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 850    850     3500    320 .98   0      - - error (invalid witness file) .60 .38 13   43 error (invalid witness file) 5.9 3.2 86 290
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 850    850     3200    320 1.0    0      - - error (invalid witness file) .50 .32 11   41 error (invalid witness file) 6.3 3.4 110 310
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (134) 0 wit inspect 680    680     6300    15000 20      .074  - - error (invalid witness file) .52 .34 9.5 40 error (invalid witness file) 7.5 4.0 68 290
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (134) 0 wit inspect 740    740     7300    15000 20      .074  - - error (invalid witness file) .62 .39 7.9 39 error (invalid witness file) 7.0 3.7 85 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     7600    6800 20      .0041 - - error (invalid witness file) .50 .32 13   40 error (invalid witness file) 6.7 3.5 71 290
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .21 .21  1.6  17 .0082 0      - - true 3.5  1.9  70   240 true 7.8 4.2 68 320
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     6400    3800 4.5    0      - - error (invalid witness file) .68 .44 8.5 43 error (invalid witness file) 6.5 3.4 100 300
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     5700    3400 4.6    0      - - error (invalid witness file) .51 .32 13   40 error (invalid witness file) 7.8 4.0 95 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 850    850     2900    240 .21   0      - - error (invalid witness file) .58 .37 11   42 error (invalid witness file) 5.7 3.0 99 290
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .52 .52  4.7  18 .17   0      - - error (recursion) 4.6  2.5  57   260 true 50   28   470 1200
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     2200    220 .22   0      - - error (invalid witness file) .64 .41 7.5 39 error (invalid witness file) 6.5 3.4 120 310
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     2300    220 .22   0      - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 5.9 3.1 110 310
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     2500    230 .22   0      - - error (invalid witness file) .58 .36 10   41 error (invalid witness file) 6.3 3.4 99 300
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     3800    1900 10      0      - - error (invalid witness file) .51 .33 11   39 error (invalid witness file) 6.4 3.5 71 290
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     4200    2000 10      0      - - error (invalid witness file) .56 .35 10   39 error (invalid witness file) 7.2 3.7 90 300
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     3300    400 .46   0      - - error (invalid witness file) .62 .39 8.0 39 error (invalid witness file) 6.9 3.6 91 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (42) 0 wit inspect 850    850     2600    280 .012  0      - - error (invalid witness file) .53 .35 9.2 40 error (invalid witness file) 7.6 4.0 93 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     4100    5000 .26   0      - - error (invalid witness file) .71 .44 8.1 42 error (invalid witness file) 5.9 3.1 110 300
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     3500    7100 .27   0      - - error (invalid witness file) .53 .34 13   43 error (invalid witness file) 5.5 2.9 100 290
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 850    850     2100    1400 15      0      - - error (invalid witness file) .64 .42 7.9 41 error (invalid witness file) 5.7 3.0 99 290
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 1.1  1.1   14    22 .25   0      - - error (recursion) 3.5  2.0  64   250 timeout 960   800   19000 4000
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 1.2  1.2   11    24 .25   0      - - error (recursion) 4.2  2.3  55   240 timeout 960   800   22000 4400
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .12 .11  1.1  17 0      0      false(no-overflow) 3.0  1.7  60 240 false(no-overflow) 7.3 3.9 100 320 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .11 .10  1.2  18 0      0      true 3.6  2.0  47 230 false(no-overflow) 8.5 4.5 110 320 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .13 .13  1.3  20 0      0      true 3.0  1.7  55 240 false(no-overflow) 9.4 5.0 81 310 - -
bitvector/jain_5_false-no-overflow.i out of memory 0 wit inspect 260    260     3600    15000 6.8    .0041 error (invalid witness file) .53 .33 11 40 error (invalid witness file) 7.3 3.8 84 290 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .13 .12  1.3  22 0      0      false(no-overflow) 3.8  2.2  50 230 false(no-overflow) 9.4 4.9 110 320 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .15 .14  1.1  19 0      0      false(no-overflow) 3.5  1.9  57 240 false(no-overflow) 9.3 4.9 97 320 - -
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .10 .099 .84 17 0      0      false(no-overflow) 3.4  1.9  67 240 error (1) 9.2 4.9 100 330 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .37 .36  3.6  18 .078  .0041 - - true 13    6.7  200   460 true 9.5 5.1 98 320
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .34 .33  4.3  18 .078  0      - - true 12    6.3  240   460 true 8.7 4.6 85 330
bitvector/byte_add_false-unreach-call_true-no-overflow.i true 2 wit inspect .35 .35  4.3  18 .086  0      - - true 23    12    300   630 true 9.1 4.9 140 330
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .27 .27  2.8  22 0      0      - - true 5.4  3.1  110   320 true 9.6 5.2 150 340
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .80 .80  9.6  31 .049  0      - - true 5.7  3.2  98   320 true 9.8 5.3 110 330
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect .83 .82  8.8  31 .049  0      - - true 7.3  4.1  80   320 true 9.6 5.2 130 330
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect .30 .29  2.7  17 .016  0      - - true 5.5  3.1  82   290 true 17   9.2 160 420
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .55 .55  6.4  17 .074  0      - - true 6.0  3.2  120   300 true 7.5 4.0 130 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i error (42) 0 wit inspect 850    850     6500    14000 250      .074  - - error (invalid witness file) .60 .39 7.8 39 error (invalid witness file) 5.4 2.9 120 290
bitvector/jain_2_true-unreach-call_true-no-overflow.i error (42) 0 wit inspect 850    850     6900    14000 500      .074  - - error (invalid witness file) .58 .37 11   43 error (invalid witness file) 7.1 3.8 85 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i error (42) 0 wit inspect 850    850     8900    14000 740      .020  - - error (invalid witness file) .59 .38 10   40 error (invalid witness file) 7.0 3.7 78 290
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 260    260     2900    15000 5.6    .020  - - error (invalid witness file) .63 .40 7.9 40 error (invalid witness file) 7.0 3.7 76 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i error (42) 0 wit inspect 850    850     6300    14000 740      .078  - - error (invalid witness file) .57 .38 8.5 39 error (invalid witness file) 5.9 3.1 84 310
bitvector/jain_7_true-unreach-call_true-no-overflow.i error (42) 0 wit inspect 850    850     7800    15000 840      .025  - - error (invalid witness file) .64 .42 10   41 error (invalid witness file) 6.7 3.5 110 320
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 160    160     850    1000 2.8    0      - - true 20    11    210   520 error (1) 23   16   410 550
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .43 .43  4.0  17 .045  0      - - true 6.8  3.7  77   300 true 7.9 4.3 100 330
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .44 .43  4.8  17 .053  0      - - true 5.9  3.2  97   300 true 10   5.4 110 340
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect .86 .86  11    21 .18   0      - - true 9.1  4.8  120   330 true 9.5 5.0 110 350
bitvector/sum02_false-unreach-call_true-no-overflow.i error (42) 0 wit inspect 850    850     4000    8400 4.0    0      - - error (invalid witness file) .61 .38 10   40 error (invalid witness file) 8.1 4.3 84 310
bitvector/sum02_true-unreach-call_true-no-overflow.i error (42) 0 wit inspect 850    850     2600    7000 4.3    0      - - error (invalid witness file) .65 .41 7.5 40 error (invalid witness file) 7.0 3.7 80 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 54 39 23000   23000   130000 180000 3200     .45   54 31 18 480 2100   54 90 48 1100 3200   54 150   83   2300 6700   54 2300 1800 46000 23000  
    correct results 23 37 160   160   930 1500 3.7   .0041 6 31 17 470 2100   8 83 44 1000 2900   13 130   68   1900 5100   13 190 110 2300 5800  
        correct true 14 28 160   160   920 1300 3.7   .0041 2 0 0 0 0   0 0 0 0 0   13 130   68   1900 5100   13 190 110 2300 5800  
        correct false 9 9 1.1 1.1 10 170 .012 0      4 31 17 470 2100   8 83 44 1000 2900   0 0   0   0 0   0 0 0 0 0  
    correct-unconfimed results 2 2 2.3 2.3 25 46 .49  0      0 0 0 0 0   0 0 0 0 0   0 7.7 4.3 120 500   0 1900 1600 41000 8400  
        correct-unconfirmed true 2 2 2.3 2.3 25 46 .49  0      0 0 0 0 0   0 0 0 0 0   0 7.7 4.3 120 500   0 1900 1600 41000 8400  
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (54 tasks, max score: 98) 39
Run set sv-comp17.Overflows-Other