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-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.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) 0 wit inspect .15  .15  1.7  24 .84 0   true 18    9.3  350   650 timeout 97   84   1100 680 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i out of memory 0 wit inspect 250     240     3400    15000 .84 0   error (invalid witness file) .52 .32 13   40 error (invalid witness file) 6.0 3.2 110 300 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .43  .42  5.2  28 .99 0   - - true 8.7  4.7  110   340 true 390   340   5100 1300
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .47  .46  6.0  28 .84 0   - - true 8.9  4.8  120   350 true 400   350   4500 1400
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .46  .46  5.7  26 .84 0   - - true 9.0  7.1  150   320 timeout 960   950   13000 770
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 190     190     2100    200 .84 0   - - true 110    110    1600   470 timeout 960   950   15000 630
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 250     250     3100    200 .84 0   - - true 120    110    2300   470 timeout 960   950   13000 590
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect .16  .16  1.6  30 .84 0   - - true 6.9  4.7  140   320 timeout 960   940   11000 920
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .69  .67  8.7  74 .84 0   - - true 6.9  4.3  86   330 true 110   87   1100 700
bitvector/jain_1_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 280     280     3300    15000 .84 0   - - error (invalid witness file) .51 .33 6.4 39 error (invalid witness file) 6.4 3.4 96 310
bitvector/jain_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     900     7100    4600 .84 0   - - error (invalid witness file) .55 .36 5.7 40 error (invalid witness file) 6.1 3.2 93 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     900     7600    3100 .84 0   - - error (invalid witness file) .53 .34 10   39 error (invalid witness file) 6.0 3.2 120 310
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 140     130     1400    15000 .84 0   - - error (invalid witness file) .51 .33 4.0 40 error (invalid witness file) 5.5 3.0 120 290
bitvector/jain_6_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     900     7600    5700 .84 0   - - error (invalid witness file) .49 .33 12   40 error (invalid witness file) 6.3 3.3 120 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     900     8300    7500 .84 0   - - error (invalid witness file) .52 .34 9.0 40 error (invalid witness file) 6.2 3.3 110 300
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect .43  .43  5.4  25 .84 0   - - true 15    13    180   350 unknown 31   27   440 320
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .14  .13  1.7  23 .84 0   - - true 5.0  2.8  94   280 true 64   50   1100 490
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .21  .20  2.1  23 .84 0   - - true 4.8  2.7  62   280 timeout 960   930   12000 940
bitvector/parity_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     900     2600    200 .84 0   - - error (invalid witness file) .64 .41 8.2 40 error (invalid witness file) 6.2 3.3 110 300
bitvector/sum02_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 290     290     2600    15000 .84 0   - - error (invalid witness file) .66 .42 7.8 41 error (invalid witness file) 6.2 3.3 120 300
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 8.5   8.5   120    410 .84 0   false(unreach-call) 7.7  4.1  130   310 true 9.6 5.1 170 330 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 16     16     240    680 .84 0   false(unreach-call) 10    5.2  120   340 true 9.5 5.0 160 330 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 3.5   3.5   47    190 .84 0   false(unreach-call) 6.8  3.6  110   300 true 9.1 4.9 150 330 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 59     59     780    1900 .84 0   - - true 61    50    990   1000 true 47   25   420 870
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 43     43     590    1600 .84 0   - - true 22    13    290   630 true 57   31   510 1100
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 45     45     490    1600 .84 0   - - true 19    11    240   560 true 38   20   360 880
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     10000    1800 .84 0   - - error (invalid witness file) .56 .37 9.2 40 error (invalid witness file) 6.1 3.2 130 300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     10000    15000 .84 0   - - error (invalid witness file) .51 .32 9.4 41 error (invalid witness file) 6.2 3.3 120 300
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     11000    9700 .84 0   - - error (invalid witness file) .48 .32 9.6 40 error (invalid witness file) 5.8 3.1 100 290
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     12000    10000 .99 0   - - error (invalid witness file) .53 .33 13   41 error (invalid witness file) 6.6 3.5 130 300
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     9900    12000 .84 0   - - error (invalid witness file) .50 .32 6.7 39 error (invalid witness file) 5.3 2.8 110 290
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     10000    12000 .84 0   - - error (invalid witness file) .54 .39 11   41 error (invalid witness file) 5.9 3.1 120 290
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 1.0   1.0   15    26 .84 0   - - timeout 900    860    7300   6300 true 120   97   1400 860
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect .11  .11  1.2  24 .84 0   - - out of memory 830    760    12000   7000 true 73   62   1100 950
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c true 1 wit inspect 7.0   6.9   88    210 .84 0   - - out of memory 760    690    12000   7000 timeout 960   930   21000 2000
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 19     19     240    38 .84 0   - - true 270    260    3200   780 true 310   280   4100 1000
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect .13  .13  .97 24 .84 0   - - out of memory 810    740    10000   7000 true 21   11   340 550
bitvector-regression/implicitfloatconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .079 .080 .65 23 .84 0   false(unreach-call) 3.7  2.1  70   280 true 11   5.8 170 310 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  .74 23 .84 0   false(unreach-call) 3.4  1.9  61   270 true 6.5 3.5 98 310 - -
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  .66 23 .99 0   false(unreach-call) 3.5  2.0  54   270 false(unreach-call) 12   6.6 170 320 - -
bitvector-regression/recHanoi03_false-unreach-call.c false(unreach-call) 0 wit inspect 2.4   2.3   30    120 .84 0   timeout 96    78    960   3900 timeout 96   75   1900 2300 - -
bitvector-regression/signextension2_false-unreach-call.c false(unreach-call) 1 wit inspect .10  .10  .71 23 .84 0   false(unreach-call) 3.5  1.9  42   270 true 7.3 3.9 140 310 - -
bitvector-regression/signextension_false-unreach-call.c false(unreach-call) 1 wit inspect .098 .098 .83 23 .99 0   false(unreach-call) 3.5  2.0  62   270 true 6.6 3.6 130 310 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true 2 wit inspect .10  .10  .63 23 .84 0   - - true 3.7  2.1  68   260 true 7.3 3.9 140 320
bitvector-regression/integerpromotion_true-unreach-call.c true 2 wit inspect .11  .11  .58 23 .84 0   - - true 3.1  1.8  38   250 true 12   6.5 160 310
bitvector-regression/signextension2_true-unreach-call.c true 2 wit inspect .072 .073 .74 23 .84 0   - - true 3.9  2.2  54   280 true 7.1 3.8 140 310
bitvector-regression/signextension_true-unreach-call.c true 2 wit inspect .11  .10  .77 23 .84 0   - - true 4.5  2.6  46   270 true 7.6 4.0 150 310
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect .086 .086 .97 23 .84 0   false(unreach-call) 4.0  2.3  72   270 false(unreach-call) 8.2 4.4 140 340 - -
bitvector-loops/overflow_false-unreach-call1.i out of memory 0 wit inspect 200     200     2200    15000 .84 0   error (invalid witness file) .48 .31 7.3 40 error (invalid witness file) 5.7 3.1 110 300 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(unreach-call) 1 wit inspect 1.1   1.1   13    59 .84 0   false(unreach-call) 5.6  3.1  110   300 out of memory 82   52   590 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 53 12000   12000   120000 170000 43    0   50 170 120 2200 7500   50 370 260 5100 13000   50 4000 3700 51000 35000   50 7500 7100 110000 22000  
    correct results 31 52 640   640   7800 7400 26    0   10 52 28 840 2900   9 160 95 1900 9900   18 3200 3000 39000 28000   15 6500 6100 85000 16000  
        correct true 21 42 610   610   7400 6000 18    0   0 0 0 0 0   7 0 0 0 0   18 3200 3000 39000 28000   15 6500 6100 85000 16000  
        correct false 10 10 30   30   430 1500 8.7  0   10 52 28 840 2900   2 160 95 1900 9900   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 3 1 9.5 9.4 120 360 2.5  0   1 110 87 1300 4500   0 190 160 3000 3000   0 760 690 12000 7000   0 960 930 21000 2000  
        correct-unconfirmed true 1 1 7.0 6.9 88 210 .84 0   1 0 0 0 0   0 0 0 0 0   0 760 690 12000 7000   0 960 930 21000 2000  
        correct-unconfirmed false 2 0 2.5 2.5 32 140 1.7  0   0 110 87 1300 4500   0 190 160 3000 3000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (50 tasks, max score: 86) 53
Run set sv-comp17.ReachSafety-BitVectors