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-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.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 51    51    620   2200 1.7  0     true 19   9.9 280 640 false(unreach-call) 56   31   320 570 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i false(unreach-call) 0 wit inspect 2.2  2.2  24   150 1.9  0     timeout 95   83   2900 980 timeout 97   82   2500 3700 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 41    42    540   2200 5.1  0     - - true 15    7.8  180   540 true 400   350   5800 1500
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 42    42    530   2200 5.1  0     - - true 16    8.5  170   540 true 410   350   8400 1500
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 120    120    1200   1200 2.3  0     - - true 14    11    210   330 timeout 960   950   16000 570
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 360    360    3800   1300 2.3  0     - - true 140    130    1400   480 timeout 960   950   13000 620
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 230    230    2500   1400 2.3  0     - - true 140    130    2400   500 timeout 960   950   20000 630
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect .16 .16 1.4 23 1.7  0     - - true 7.5  5.2  150   310 timeout 960   940   20000 900
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .16 .16 2.0 23 1.7  0     - - true 8.8  5.5  100   340 true 100   86   1300 710
bitvector/jain_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.3  5.3  70   510 2.2  0     - - out of memory 300    290    6300   7000 true 9.6 5.1 92 330
bitvector/jain_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.8  6.8  91   730 2.4  0     - - out of memory 240    230    4100   7000 true 9.2 4.9 110 360
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 8.6  8.6  110   890 2.6  0     - - out of memory 200    190    4100   7000 true 7.5 4.0 90 320
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 1 wit inspect .25 .25 3.3 40 2.0  0     - - out of memory 370    360    6600   7000 timeout 960   820   13000 2900
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect 8.8  8.8  96   890 2.6  0     - - out of memory 230    220    3900   7000 true 9.9 5.1 140 340
bitvector/jain_7_true-unreach-call_true-no-overflow.i true 2 wit inspect 8.2  8.2  88   760 2.6  0     - - out of memory 310    300    6300   7000 true 8.5 4.5 180 340
bitvector/modulus_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900    900    8700   5600 .84 0     - - error (invalid witness file) .65 .41 9.7 42 error (invalid witness file) 6.4 3.4 91 290
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .16 .16 1.8 23 1.7  0     - - true 5.4  2.9  97   300 true 72   55   900 520
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .18 .17 2.0 23 1.7  0     - - true 6.7  3.8  65   290 timeout 960   930   18000 950
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.3  2.3  25   160 2.2  0     - - true 29    23    380   370 timeout 960   950   16000 1100
bitvector/sum02_true-unreach-call_true-no-overflow.i false(unreach-call) -16 wit inspect 2.6  2.6  34   150 1.9  .094 - - timeout 910    890    19000   1100 out of memory 320   280   4400 7000
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c out of memory 0 wit inspect 310    310    3900   15000 1.7  0     false(unreach-call) 9.6 5.2 110 330 true 9.4 5.0 160 330 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 890    890    12000   15000 1.7  0     false(unreach-call) 8.6 4.5 190 350 true 8.1 4.4 98 310 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 890    890    8200   15000 1.7  0     false(unreach-call) 7.4 3.9 140 310 true 8.9 4.8 130 330 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c out of memory 0 wit inspect 330    330    3600   15000 1.7  0     - - true 110    82    1300   2800 true 59   32   770 1900
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 900    900    7100   15000 1.7  0     - - true 46    26    480   2400 true 68   37   600 1900
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 900    900    7500   15000 1.7  0     - - true 33    19    670   2200 true 43   23   490 1900
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900    900    8500   2800 .84 0     - - error (invalid witness file) .59 .37 8.0 40 error (invalid witness file) 6.2 3.3 80 300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c out of memory 0 wit inspect 410    410    4400   15000 1.7  0     - - timeout 920    890    15000   6700 true 77   41   560 2400
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c out of memory 0 wit inspect 420    420    4500   15000 1.7  0     - - timeout 920    890    16000   5800 true 52   28   610 2100
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c out of memory 0 wit inspect 450    450    4800   15000 1.7  0     - - timeout 920    890    16000   5800 true 51   27   640 2100
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c out of memory 0 wit inspect 430    430    5100   15000 1.7  0     - - timeout 920    890    12000   6900 true 62   33   670 2000
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c out of memory 0 wit inspect 410    400    4300   15000 1.7  0     - - out of memory 830    810    14000   7000 true 54   29   690 2000
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 900    900    12000   2900 1.7  0     - - timeout 910    850    15000   6000 true 220   200   4700 1000
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 890    900    12000   2900 1.7  0     - - out of memory 790    720    18000   7000 true 76   65   970 980
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c true 1 wit inspect 890    900    11000   2900 1.7  0     - - timeout 900    820    16000   7000 timeout 960   920   21000 2100
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 890    890    13000   2900 1.7  0     - - true 340    330    11000   690 error 48   34   500 650
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 900    900    12000   2900 1.7  0     - - out of memory 840    770    16000   7000 true 22   12   300 590
bitvector-regression/implicitfloatconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .13 .13 1.3 23 1.7  0     false(unreach-call) 3.7 2.1 68 270 true 9.9 5.4 120 300 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .14 .14 1.4 23 1.7  .094 false(unreach-call) 4.3 2.4 39 270 true 6.4 3.4 89 310 - -
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) 1 wit inspect .13 .13 1.4 24 1.7  .65  false(unreach-call) 3.6 2.0 78 270 false(unreach-call) 12   6.2 200 310 - -
bitvector-regression/recHanoi03_false-unreach-call.c false(unreach-call) 0 wit inspect 4.1  4.0  51   300 1.8  0     timeout 97   75   2100 4100 timeout 98   70   1600 6100 - -
bitvector-regression/signextension2_false-unreach-call.c false(unreach-call) 1 wit inspect .13 .13 1.5 23 1.7  0     false(unreach-call) 3.5 2.0 58 270 true 6.6 3.5 140 310 - -
bitvector-regression/signextension_false-unreach-call.c false(unreach-call) 1 wit inspect .15 .15 1.4 23 1.7  .094 false(unreach-call) 3.7 2.0 87 280 true 7.6 4.0 130 310 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true 2 wit inspect .17 .17 1.3 23 1.7  0     - - true 4.1  2.3  45   250 true 7.0 3.7 81 320
bitvector-regression/integerpromotion_true-unreach-call.c true 2 wit inspect .15 .15 1.4 23 1.7  0     - - true 4.2  2.4  54   250 true 12   6.6 170 320
bitvector-regression/signextension2_true-unreach-call.c true 2 wit inspect .15 .15 1.4 23 1.7  0     - - true 3.4  1.9  41   260 true 6.8 3.6 58 310
bitvector-regression/signextension_true-unreach-call.c true 2 wit inspect .16 .16 1.5 23 1.7  0     - - true 3.5  1.9  68   270 true 9.0 4.8 71 310
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 16    16    190   1000 1.7  0     true 3.9 2.2 96 280 false(unreach-call) 7.9 4.2 91 350 - -
bitvector-loops/overflow_false-unreach-call1.i false(unreach-call) 0 wit inspect .15 .15 1.5 23 1.7  0     timeout 97   86   2800 1900 true 6.8 3.7 130 310 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(unreach-call) 1 wit inspect 2.1  2.1  24   220 1.7  0     false(unreach-call) 6.0 3.3 98 300 timeout 98   60   860 6300 - -
../../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 46 14000   14000   150000 200000 97   .93  50 360 280 9000 11000   50 430 290 6600 20000   50 11000 11000 210000 120000   50 9900 9100 170000 44000  
    correct results 35 60 8100   8100   94000 87000 72   .84  10 64 34 1100 3300   9 220 130 2200 9400   17 4600 4300 91000 65000   18 7300 6900 130000 19000  
        correct true 25 50 6200   6200   73000 54000 55   0     2 0 0 0 0   6 0 0 0 0   17 4600 4300 91000 65000   18 7300 6900 130000 19000  
        correct false 10 10 1900   1900   21000 33000 17   .84  8 64 34 1100 3300   3 220 130 2200 9400   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 5 2 900   900   11000 3400 9.0 0     0 290 240 7800 7000   1 200 160 4300 10000   0 1300 1200 23000 14000   0 1900 1700 34000 5000  
        correct-unconfirmed true 2 2 890   900   11000 2900 3.6 0     0 0 0 0 0   1 0 0 0 0   0 1300 1200 23000 14000   0 1900 1700 34000 5000  
        correct-unconfirmed false 3 0 6.5 6.4 76 470 5.3 0     0 290 240 7800 7000   0 200 160 4300 10000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 1 -16 2.6 2.6 34 150 1.9 .094 0 0 0 0 0   0 0 0 0 0   0 910 890 19000 1100   0 320 280 4400 7000  
        incorrect true 0
        incorrect false 1 -16 2.6 2.6 34 150 1.9 .094 0 0 0 0 0   0 0 0 0 0   0 910 890 19000 1100   0 320 280 4400 7000  
score (50 tasks, max score: 86) 46
Run set sv-comp17.ReachSafety-BitVectors