Tool CBMC 5.6
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-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-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.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)
bitvector/byte_add_false-unreach-call_true-no-overflow.i false(unreach-call) 1 wit inspect .28 .27 3.0  18 .053  0     false(unreach-call) 5.2  2.8  62 290 false(unreach-call) 44   24   540 540 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i error (42) 0 wit inspect 850    850    4000    7900 4.3    0     error (invalid witness file) .55 .37 12 42 error (invalid witness file) 5.7 3.0 120 300 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .35 .35 3.9  18 .074  0     - - true 13    7.1  160   430 true 460   400   11000 1500
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .36 .36 3.9  18 .074  0     - - true 15    8.0  160   430 true 400   350   8700 1600
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .32 .32 3.7  21 0      0     - - true 8.8  6.9  210   320 timeout 960   950   24000 780
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.2  1.2  17    31 .049  0     - - true 140    140    2300   480 timeout 960   950   16000 630
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.2  1.2  13    31 .049  0     - - true 130    130    2200   470 timeout 960   950   23000 650
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect .30 .29 3.1  17 .016  0     - - true 6.6  4.4  120   320 timeout 960   940   21000 840
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .56 .55 6.9  17 .074  0     - - true 10    6.1  120   350 true 93   74   1900 640
bitvector/jain_1_true-unreach-call_true-no-overflow.i error (134) 0 wit inspect 94    94    1200    14000 10      0     - - error (invalid witness file) .58 .35 14   43 error (invalid witness file) 6.3 3.3 110 300
bitvector/jain_2_true-unreach-call_true-no-overflow.i error (134) 0 wit inspect 58    58    790    14000 4.4    0     - - error (invalid witness file) .55 .37 4.9 40 error (invalid witness file) 7.5 4.0 92 290
bitvector/jain_4_true-unreach-call_true-no-overflow.i error (134) 0 wit inspect 69    69    730    14000 6.4    .070 - - error (invalid witness file) .52 .37 12   44 error (invalid witness file) 5.3 2.8 93 290
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 250    250    3600    15000 5.9    0     - - error (invalid witness file) .49 .33 10   40 error (invalid witness file) 6.5 3.4 130 320
bitvector/jain_6_true-unreach-call_true-no-overflow.i error (134) 0 wit inspect 150    150    1600    14000 29      0     - - error (invalid witness file) .64 .40 9.6 41 error (invalid witness file) 5.5 2.9 80 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i error (134) 0 wit inspect 110    110    1300    14000 33      0     - - error (invalid witness file) .53 .34 12   41 error (invalid witness file) 6.9 3.6 130 310
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 380    380    2100    1100 3.2    0     - - true 50    34    620   650 unknown 44   37   1200 560
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .40 .40 5.9  17 .041  0     - - true 6.1  3.3  66   290 true 60   48   1000 490
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .47 .47 3.9  17 .045  0     - - true 7.1  4.0  71   290 timeout 960   930   16000 960
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.5  2.5  32    22 .18   0     - - true 27    21    590   430 timeout 960   940   23000 1000
bitvector/sum02_true-unreach-call_true-no-overflow.i error (42) 0 wit inspect 850    850    3500    7300 4.4    0     - - error (invalid witness file) .56 .36 11   41 error (invalid witness file) 7.0 3.7 130 310
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 4.3  4.3  58    220 .40   0     true 8.2  4.4  120 300 false(unreach-call) 25   13   420 510 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 3.7  3.7  47    180 .42   .16  true 8.0  4.2  140 300 false(unreach-call) 32   17   590 610 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect .91 .93 12    75 .11   10     true 6.4  3.4  55 290 false(unreach-call) 23   12   460 480 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 16    16    170    360 1.9    .16  - - true 70    58    1700   1000 true 52   29   1100 810
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 14    14    160    290 1.8    0     - - true 26    15    480   760 true 68   37   1100 970
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 14    14    150    270 1.8    0     - - true 26    14    320   670 true 49   26   1000 910
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c error (42) 0 wit inspect 850    850    11000    430 1.2    0     - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 8.0 4.3 85 300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c error (42) 0 wit inspect 850    850    3600    910 7.6    0     - - error (invalid witness file) .72 .45 9.9 44 error (invalid witness file) 6.2 3.2 120 300
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c error (42) 0 wit inspect 850    850    4600    790 8.3    0     - - error (invalid witness file) .59 .37 10   40 error (invalid witness file) 7.1 3.7 110 290
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c error (42) 0 wit inspect 850    850    3600    820 8.2    0     - - error (invalid witness file) .52 .34 13   40 error (invalid witness file) 6.0 3.2 110 290
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c error (42) 0 wit inspect 850    850    3400    850 7.1    0     - - error (invalid witness file) .70 .45 7.0 40 error (invalid witness file) 5.6 3.0 110 290
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c error (42) 0 wit inspect 850    850    4000    830 7.6    0     - - error (invalid witness file) .59 .37 7.0 41 error (invalid witness file) 5.8 3.1 99 300
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 4.2  4.2  47    41 1.0    0     - - timeout 900    860    18000   6200 true 230   200   3400 1100
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 2.8  2.8  30    43 1.0    0     - - out of memory 800    720    19000   7000 true 78   66   1800 850
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c true 1 wit inspect 2.8  2.8  41    42 1.0    0     - - out of memory 850    770    14000   7000 timeout 960   920   17000 2000
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 9.9  9.9  130    44 .98   0     - - true 350    340    9100   790 true 330   290   8000 1400
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 2.8  2.9  36    52 1.0    11     - - out of memory 880    800    15000   7000 true 24   13   420 570
bitvector-regression/implicitfloatconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .14 .13 .86 17 .0041 0     false(unreach-call) 3.4  1.9  36 270 false(unreach-call) 13   6.9 240 320 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .14 .13 .95 17 .0041 0     false(unreach-call) 3.4  2.0  46 270 false(unreach-call) 6.8 3.6 120 320 - -
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) 1 wit inspect .12 .11 .85 17 .0041 0     false(unreach-call) 3.5  2.0  81 270 false(unreach-call) 12   6.6 220 310 - -
bitvector-regression/recHanoi03_false-unreach-call.c false(unreach-call) 1 wit inspect .97 .96 11    23 .16   0     false(unreach-call) 15    7.7  300 580 true 8.3 4.4 150 340 - -
bitvector-regression/signextension2_false-unreach-call.c false(unreach-call) 1 wit inspect .12 .11 .84 17 .0041 0     false(unreach-call) 3.6  2.0  77 280 false(unreach-call) 7.2 3.8 140 310 - -
bitvector-regression/signextension_false-unreach-call.c false(unreach-call) 1 wit inspect .13 .13 .97 17 .0041 0     false(unreach-call) 3.9  2.2  81 270 false(unreach-call) 8.5 4.5 110 310 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true 2 wit inspect .19 .19 1.6  17 .0082 0     - - true 3.2  1.8  69   260 true 7.1 3.8 140 330
bitvector-regression/integerpromotion_true-unreach-call.c true 2 wit inspect .19 .18 1.6  17 .0082 0     - - true 3.8  2.1  57   250 true 12   6.5 230 310
bitvector-regression/signextension2_true-unreach-call.c true 2 wit inspect .18 .17 1.9  17 .0082 0     - - true 3.8  2.1  61   270 true 8.3 4.4 150 320
bitvector-regression/signextension_true-unreach-call.c true 2 wit inspect .19 .18 2.0  17 .0082 0     - - true 4.3  2.4  48   250 true 7.7 4.1 150 320
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect .14 .13 .93 18 0      0     false(unreach-call) 4.1  2.2  54 290 false(unreach-call) 7.9 4.2 170 350 - -
bitvector-loops/overflow_false-unreach-call1.i error (1) 0 wit inspect 280    280    3300    15000 2.1    710     error (invalid witness file) .50 .32 12 39 error (invalid witness file) 6.0 3.2 91 290 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(unreach-call) 1 wit inspect .40 .40 3.7  21 .086  0     false(unreach-call) 6.0  3.3  70 300 out of memory 63   39   920 7000 - -
../../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 50 57 8300   8300   53000 120000 150   730   50 72 39 1100 3800   50 260 150 4300 12000   50 4300 3900 85000 36000   50 8700 8200 180000 23000  
    correct results 34 56 460   460   3000 3100 15   21   12 71 38 1100 3700   11 250 140 4100 11000   19 3500 3200 70000 29000   15 7700 7300 160000 18000  
        correct true 22 44 450   450   2900 2400 13   11   3 0 0 0 0   1 0 0 0 0   19 3500 3200 70000 29000   15 7700 7300 160000 18000  
        correct false 12 12 11   11   140 640 1.3 10   9 71 38 1100 3700   10 250 140 4100 11000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 1 1 2.8 2.8 41 42 1.0 0   0 0 0 0 0   0 0 0 0 0   0 850 770 14000 7000   0 960 920 17000 2000  
        correct-unconfirmed true 1 1 2.8 2.8 41 42 1.0 0   0 0 0 0 0   0 0 0 0 0   0 850 770 14000 7000   0 960 920 17000 2000  
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (50 tasks, max score: 86) 57
Run set sv-comp17.ReachSafety-BitVectors