Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
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 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.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 2.2  2.2  28   110 6.8  0      true 24    12    210   640 false(unreach-call) 70   48   640 520 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 wit inspect 69    69    840   76 260    0      error (invalid witness file) .62 .39 8.3 40 error (invalid witness file) 7.4 3.9 95 310 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 74    64    870   1800 14    0      - - true 11    6.0  92   330 true 470   420   6100 1200
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 28    20    300   840 14    0      - - true 10    5.7  110   330 true 450   400   9500 1200
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 490    490    6000   280 3.4  0      - - true 10    8.0  130   310 timeout 960   950   13000 550
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 240    240    2400   290 26    0      - - true 120    120    1600   480 timeout 960   950   17000 560
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 460    450    5000   320 26    0      - - true 140    130    2100   470 timeout 960   950   23000 590
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 490    480    6400   260 14    .0041 - - true 6.9  4.8  180   310 timeout 960   940   12000 890
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 17    12    210   410 42    0      - - true 6.9  4.3  150   340 true 110   87   1300 630
bitvector/jain_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 300    300    3400   290 260    0      - - error (invalid witness file) .67 .42 7.2 40 error (invalid witness file) 5.8 3.1 64 300
bitvector/jain_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 900    900    7700   290 150    0      - - error (invalid witness file) .58 .37 9.8 42 error (invalid witness file) 6.0 3.2 90 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 890    900    7000   240 120    0      - - error (invalid witness file) .53 .33 11   40 error (invalid witness file) 6.7 3.5 110 320
bitvector/jain_5_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 59    58    680   75 260    0      - - error (invalid witness file) .71 .45 9.3 45 error (invalid witness file) 6.1 3.2 93 310
bitvector/jain_6_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 890    900    8400   270 130    0      - - error (invalid witness file) .56 .35 10   39 error (invalid witness file) 5.7 3.0 100 290
bitvector/jain_7_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 900    900    6700   290 230    0      - - error (invalid witness file) .51 .33 14   39 error (invalid witness file) 5.8 3.1 120 310
bitvector/modulus_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 890    900    7500   380 34    0      - - error (invalid witness file) .59 .37 12   44 error (invalid witness file) 6.1 3.2 68 310
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.0  5.5  77   260 22    0      - - true 4.8  2.6  91   280 true 60   48   1000 490
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 22    15    230   600 22    0      - - true 5.0  2.8  76   300 timeout 960   920   13000 1000
bitvector/parity_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 890    900    10000   150 73    0      - - error (invalid witness file) .59 .38 8.7 42 error (invalid witness file) 5.5 2.9 96 300
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 170    170    1800   490 260    .020  - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.0 3.1 92 300
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 33    33    470   100 20    0      false(unreach-call) 8.0  4.3  160   330 true 9.6 5.1 130 340 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 56    56    830   110 27    .10   false(unreach-call) 9.6  5.1  120   320 true 9.4 5.0 120 340 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 18    18    210   85 14    0      false(unreach-call) 9.3  5.0  93   300 true 9.9 5.2 200 340 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 170    170    2100   1300 37    0      - - true 64    55    1000   970 true 44   24   530 770
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 140    140    1800   1600 37    .21   - - true 20    12    230   580 true 59   32   760 870
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 140    140    1800   2200 37    .10   - - true 15    8.8  280   560 true 40   21   460 900
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 890    900    9900   390 4.3  0      - - timeout 900    890    12000   1400 timeout 960   930   13000 1300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 46    38    520   2300 4.3  0      - - timeout 910    900    16000   4900 true 50   27   740 1100
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 890    900    11000   370 62    0      - - error (invalid witness file) .59 .38 8.3 42 error (invalid witness file) 5.6 3.0 100 300
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 890    900    11000   380 61    0      - - error (invalid witness file) .63 .40 9.4 44 error (invalid witness file) 5.7 3.0 43 310
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 890    900    13000   310 62    0      - - error (invalid witness file) .63 .42 9.5 40 error (invalid witness file) 6.7 3.5 110 300
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 890    900    12000   300 62    0      - - error (invalid witness file) .56 .37 11   39 error (invalid witness file) 5.5 2.9 66 290
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 15    8.9  140   400 4.3  .025  - - timeout 900    860    21000   6100 true 120   100   2000 860
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 120    100    1300   1200 3.5  .21   - - out of memory 830    760    11000   7000 true 83   68   830 830
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c true 1 wit inspect 120    110    1500   1400 60    0      - - out of memory 790    710    18000   7000 timeout 960   930   17000 1900
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 230    220    2600   360 4.3  0      - - true 380    370    4900   780 true 300   270   3600 980
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 110    99    1500   1200 3.5  .049  - - out of memory 870    790    14000   7000 true 20   11   230 520
bitvector-regression/implicitfloatconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .38 .37 3.8 48 .85 0      false(unreach-call) 4.1  2.3  51   280 false(unreach-call) 10   5.6 230 290 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .37 .37 3.9 48 .85 .10   false(unreach-call) 4.2  2.3  51   270 false(unreach-call) 6.6 3.6 140 300 - -
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) 1 wit inspect .35 .34 4.1 48 .85 0      false(unreach-call) 3.7  2.1  86   280 false(unreach-call) 12   6.3 210 320 - -
bitvector-regression/recHanoi03_false-unreach-call.c unknown 0 wit inspect 4.6  2.5  49   300 4.3  0      error (recursion) 3.3  1.9  63   250 timeout 97   74   1400 1100 - -
bitvector-regression/signextension2_false-unreach-call.c false(unreach-call) 1 wit inspect 480    480    6200   70 .85 0      false(unreach-call) 4.0  2.2  74   270 false(unreach-call) 7.2 3.8 130 320 - -
bitvector-regression/signextension_false-unreach-call.c false(unreach-call) 1 wit inspect .37 .37 4.1 48 .85 0      false(unreach-call) 3.6  2.0  68   270 false(unreach-call) 8.5 4.5 100 310 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true 2 wit inspect 3.2  1.7  29   260 3.4  0      - - true 3.8  2.1  54   250 true 7.0 3.8 120 320
bitvector-regression/integerpromotion_true-unreach-call.c true 2 wit inspect 3.2  1.7  28   260 3.4  0      - - true 4.4  2.5  44   260 true 12   6.2 150 310
bitvector-regression/signextension2_true-unreach-call.c true 2 wit inspect 480    480    5800   270 3.4  0      - - true 3.6  2.0  66   260 true 7.6 4.0 130 320
bitvector-regression/signextension_true-unreach-call.c true 2 wit inspect 3.1  1.7  29   260 3.4  0      - - true 3.5  2.0  65   260 true 7.6 4.0 89 320
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 1.2  1.2  17   78 4.2  0      false(unreach-call) 4.4  2.4  71   280 false(unreach-call) 7.3 4.0 92 350 - -
bitvector-loops/overflow_false-unreach-call1.i unknown 0 wit inspect 54    54    780   75 260    0      error (invalid witness file) .53 .34 11   39 error (invalid witness file) 6.4 3.4 100 310 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(unreach-call) 1 wit inspect 7.9  7.8  97   100 30    0      false(unreach-call) 6.5  3.6  100   310 false(unreach-call) 28   15   430 730 - -
../../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 54 15000 14000 160000 24000 2800 .83 50 86 46 1200 3900   50 290 190 4000 5800   50 6000 5700 100000 41000   50 8600 8100 140000 22000  
    correct results 32 53 3900 3800 47000 17000 440 .81 11 81 44 1100 3500   11 180 110 2400 4200   17 4300 4000 74000 32000   16 6600 6200 110000 15000  
        correct true 21 42 3300 3200 39000 17000 330 .61 1 0 0 0 0   3 0 0 0 0   17 4300 4000 74000 32000   16 6600 6200 110000 15000  
        correct false 11 11 600 600 7900 850 110 .20 10 81 44 1100 3500   8 180 110 2400 4200   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 1 1 120 110 1500 1400 60 0    0 0 0 0 0   0 0 0 0 0   0 790 710 18000 7000   0 960 930 17000 1900  
        correct-unconfirmed true 1 1 120 110 1500 1400 60 0    0 0 0 0 0   0 0 0 0 0   0 790 710 18000 7000   0 960 930 17000 1900  
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (50 tasks, max score: 86) 54
Run set sv-comp17.ReachSafety-BitVectors