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 16:16:17 CET [[ 2017-01-14 22:37:08 CET ]] [[ 2017-01-15 00:13:18 CET ]] [[ 2017-01-14 22:52:42 CET ]] [[ 2017-01-15 00:24:59 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.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 .14  .14  1.9  24 .84 0   true 17    9.0  230   660 timeout 97   86   1800 610 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i out of memory 0 wit inspect 300     300     3900    15000 .84 0   error (invalid witness file) .51 .35 4.7 40 error (invalid witness file) 6.2 3.3 110 300 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .32  .31  4.1  24 .84 0   - - true 11    5.7  150   340 true 390   340   8700 1300
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .33  .32  4.4  24 .84 0   - - true 9.1  4.9  88   350 true 400   350   7700 1400
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .47  .47  5.7  26 .84 0   - - true 8.9  6.9  150   310 timeout 960   950   12000 560
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 180     180     2000    150 .84 0   - - true 110    110    1900   470 timeout 960   950   13000 590
bitvector/gcd_3_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     900     2300    150 .84 0   - - error (invalid witness file) .52 .35 7.3 40 error (invalid witness file) 5.4 2.9 70 300
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect .079 .078 .99 23 .84 0   - - true 7.2  5.0  150   310 timeout 960   940   16000 830
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .15  .15  1.3  23 .84 0   - - true 7.2  4.5  77   340 true 83   64   1100 650
bitvector/jain_1_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 180     180     1500    15000 .84 0   - - error (invalid witness file) .53 .33 11   40 error (invalid witness file) 6.5 3.4 130 300
bitvector/jain_2_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 150     150     1700    15000 .84 0   - - error (invalid witness file) .48 .32 11   40 error (invalid witness file) 6.0 3.2 110 300
bitvector/jain_4_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 260     260     2000    15000 .84 0   - - error (invalid witness file) .49 .32 5.7 40 error (invalid witness file) 5.5 2.9 110 290
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 340     320     4900    15000 .84 0   - - error (invalid witness file) .54 .34 14   40 error (invalid witness file) 6.1 3.3 120 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 170     170     1400    15000 .84 0   - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 5.9 3.1 93 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 580     570     1400    15000 .84 0   - - error (invalid witness file) .49 .31 8.8 39 error (invalid witness file) 6.0 3.1 98 290
bitvector/modulus_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     900     6300    1400 .84 0   - - error (invalid witness file) .52 .34 14   41 error (invalid witness file) 6.2 3.3 120 300
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .10  .10  1.1  23 .84 0   - - true 4.9  2.7  91   280 true 59   47   670 490
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .17  .17  1.4  23 .84 0   - - true 4.8  2.7  86   290 timeout 960   930   12000 910
bitvector/parity_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     900     12000    340 .84 0   - - error (invalid witness file) .49 .32 8.4 40 error (invalid witness file) 5.9 3.1 100 290
bitvector/sum02_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 390     390     5300    15000 .84 0   - - error (invalid witness file) .53 .36 12   42 error (invalid witness file) 5.6 3.0 100 300
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 5.0   5.0   80    240 .84 0   false(unreach-call) 8.0  4.2  160   300 true 8.9 4.8 160 330 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 9.8   9.8   110    390 .84 0   false(unreach-call) 8.6  4.5  180   350 true 8.5 4.6 150 320 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 2.2   2.2   33    120 .84 0   false(unreach-call) 6.8  3.7  110   300 true 9.1 4.9 190 330 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 34     34     470    1200 .84 0   - - true 59    49    830   1100 true 45   25   410 870
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 28     28     300    1000 .84 0   - - true 19    11    300   590 true 53   29   440 1000
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 29     29     360    1000 .84 0   - - true 19    11    180   600 true 38   20   330 900
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     11000    1000 .84 0   - - error (invalid witness file) .62 .40 7.0 39 error (invalid witness file) 6.2 3.3 110 300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     11000    11000 .84 0   - - error (invalid witness file) .51 .32 6.9 39 error (invalid witness file) 6.0 3.2 89 300
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     11000    6500 .84 0   - - error (invalid witness file) .49 .32 8.8 40 error (invalid witness file) 6.6 3.4 120 310
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     10000    6700 .84 0   - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 5.9 3.2 80 300
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     9600    9200 .84 0   - - error (invalid witness file) .54 .35 9.2 40 error (invalid witness file) 5.7 3.1 100 300
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     900     2000    3600 .84 0   - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 5.7 3.1 110 290
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c true 1 wit inspect 19     19     260    280 .84 0   - - timeout 900    860    12000   6200 error 110   93   1100 820
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect .66  .65  8.8  51 .84 0   - - out of memory 820    750    9100   7000 true 75   64   890 840
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c true 1 wit inspect 2.0   1.9   23    53 .84 0   - - out of memory 890    810    11000   7000 timeout 960   930   17000 2000
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 220     220     3200    360 .84 0   - - true 300    300    10000   810 true 290   270   4400 1100
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect .65  .65  7.9  47 .84 0   - - out of memory 720    660    12000   7000 true 22   12   260 550
bitvector-regression/implicitfloatconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .071 .071 .79 23 .84 0   false(unreach-call) 3.7  2.1  53   280 true 12   6.4 180 310 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .071 .072 .90 23 .84 0   false(unreach-call) 3.6  2.0  55   270 true 6.9 3.7 130 310 - -
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) 1 wit inspect .10  .10  .75 23 .84 0   false(unreach-call) 3.8  2.1  79   280 false(unreach-call) 12   6.2 220 310 - -
bitvector-regression/recHanoi03_false-unreach-call.c false(unreach-call) 0 wit inspect 2.0   2.0   28    83 .84 0   timeout 96    77    1200   3600 timeout 96   73   1800 2600 - -
bitvector-regression/signextension2_false-unreach-call.c false(unreach-call) 1 wit inspect .073 .073 .66 23 .84 0   false(unreach-call) 3.6  2.0  83   280 true 6.3 3.4 120 300 - -
bitvector-regression/signextension_false-unreach-call.c false(unreach-call) 1 wit inspect .088 .087 .83 23 .84 0   false(unreach-call) 3.5  2.0  67   270 true 6.9 3.6 120 310 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true 2 wit inspect .27  .27  .83 23 .84 0   - - true 4.2  2.4  44   250 true 7.1 3.8 150 320
bitvector-regression/integerpromotion_true-unreach-call.c true 2 wit inspect .075 .075 .74 23 .84 0   - - true 3.3  1.9  56   260 true 11   6.0 160 300
bitvector-regression/signextension2_true-unreach-call.c true 2 wit inspect .10  .10  .87 23 .84 0   - - true 3.6  2.0  51   250 true 8.6 4.5 160 320
bitvector-regression/signextension_true-unreach-call.c true 2 wit inspect .072 .072 .82 23 .84 0   - - true 3.2  1.8  41   250 true 7.3 4.0 130 310
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect .11  .11  .81 23 .84 0   false(unreach-call) 4.0  2.2  68   270 false(unreach-call) 9.0 4.7 170 350 - -
bitvector-loops/overflow_false-unreach-call1.i out of memory 0 wit inspect 310     250     3600    15000 .84 0   error (invalid witness file) .50 .33 7.0 41 error (invalid witness file) 5.8 3.1 110 300 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(unreach-call) 1 wit inspect .18  .18  1.9  25 .84 0   false(unreach-call) 5.5  3.1  84   300 out of memory 82   52   690 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 48 11000   11000   110000 180000 42   0   50 170 120 2400 7200   50 370 260 5900 14000   50 3900 3600 58000 35000   50 6500 6100 98000 21000  
    correct results 28 46 510   510   6600 5100 24   0   10 51 28 940 2900   9 160 95 2100 9900   16 2100 1900 35000 21000   14 5300 5000 78000 13000  
        correct true 18 36 490   490   6400 4200 15   0   0 0 0 0 0   7 0 0 0 0   16 2100 1900 35000 21000   14 5300 5000 78000 13000  
        correct false 10 10 18   18   230 920 8.4 0   10 51 28 940 2900   2 160 95 2100 9900   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 4 2 23   23   320 440 3.4 0   1 110 86 1400 4200   0 190 160 3500 3200   0 1800 1700 23000 13000   0 1100 1000 18000 2800  
        correct-unconfirmed true 2 2 21   21   290 330 1.7 0   1 0 0 0 0   0 0 0 0 0   0 1800 1700 23000 13000   0 1100 1000 18000 2800  
        correct-unconfirmed false 2 0 2.1 2.1 30 110 1.7 0   0 110 86 1400 4200   0 190 160 3500 3200   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) 48
Run set sv-comp17.ReachSafety-BitVectors