Tool 2LS 0.5.0
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 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 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/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.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/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.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 1 .33  .33  4.2  27 0      0     5.0  2.7  43   290 18   9.9 290 520
bitvector/sum02_false-unreach-call_true-no-overflow.i 0 900     900     10000    1500 0      0     .51 .34 6.2 39 6.4 3.4 100 300
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 2 .40  .40  5.8  28 0      0     11    5.9  160   350 390   340   6800 1600
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 2 .42  .41  4.5  28 0      0     9.3  5.0  140   350 520   460   7800 1300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 2 .29  .29  3.4  25 0      0     10    8.5  220   310 8.5 4.6 150 330
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 .69  .68  9.9  32 0      0     120    120    3800   480 960   950   19000 600
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 2 .64  .64  8.9  32 0      0     130    130    2500   470 960   950   20000 660
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 2 .81  .81  10    33 0      .16  6.6  4.4  85   310 960   940   25000 790
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2 .58  .57  7.3  44 0      0     7.4  4.6  120   330 89   70   1600 650
bitvector/jain_1_true-unreach-call_true-no-overflow.i 0 900     900     11000    1400 0      0     .54 .35 12   40 6.1 3.3 130 300
bitvector/jain_2_true-unreach-call_true-no-overflow.i 0 900     900     9900    1500 0      0     .63 .40 7.4 39 5.6 3.0 100 300
bitvector/jain_4_true-unreach-call_true-no-overflow.i 0 900     900     10000    2000 0      0     .50 .32 12   39 6.1 3.2 110 300
bitvector/jain_5_true-unreach-call_true-no-overflow.i 0 900     900     9900    1500 0      0     .64 .41 8.6 41 6.0 3.2 110 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i 0 900     900     12000    1900 0      0     .52 .34 12   42 5.8 3.1 95 290
bitvector/jain_7_true-unreach-call_true-no-overflow.i 0 900     900     9600    1700 0      0     .69 .45 8.1 41 5.5 2.9 98 290
bitvector/modulus_true-unreach-call_true-no-overflow.i 2 .77  .77  11    36 0      .082 16    14    280   340 31   28   880 330
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 2 .17  .16  1.3  24 0      0     6.6  3.7  75   280 59   47   1300 520
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 2 .15  .15  1.4  24 0      0     5.8  3.2  82   280 960   930   17000 1000
bitvector/parity_true-unreach-call_true-no-overflow.i 2 2.5   2.5   30    33 0      0     23    19    690   360 960   950   17000 940
bitvector/sum02_true-unreach-call_true-no-overflow.i 0 900     900     11000    1500 0      0     .52 .32 9.1 40 6.0 3.1 120 310
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 1 26     26     220    240 .0041 0     8.0  4.2  98   340 23   12   390 520
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 1 16     16     150    240 .0041 0     8.1  4.3  98   350 32   17   400 570
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 1 21     21     190    170 .0041 0     7.4  3.9  130   300 27   14   330 500
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     9000    760 .0041 0     .54 .34 9.8 39 6.0 3.2 120 300
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 2 17     17     160    280 .0041 0     21    12    380   600 53   29   710 1000
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 2 21     21     170    250 .0041 0     19    10    340   560 37   20   500 910
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     7600    1400 .0041 0     .50 .32 10   40 6.0 3.2 130 290
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     9900    8700 .0041 0     .68 .42 8.1 42 6.3 3.3 120 290
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     11000    7400 .0041 0     .63 .41 8.0 40 6.1 3.2 100 300
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     9200    7600 .0041 0     .55 .36 12   40 6.3 3.3 130 300
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     9700    8000 .0041 0     .60 .38 11   43 7.4 3.8 110 320
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     11000    8300 .0041 0     .51 .33 11   40 6.0 3.2 120 290
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c 2 .22  .25  1.7  38 .0041 10     910    860    21000   6200 130   110   2600 890
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c 2 .15  .15  1.6  26 .0041 0     890    810    18000   7000 76   64   1700 900
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c 1 6.7   6.7   80    150 .0041 0     840    770    18000   7000 960   920   16000 2100
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c 2 .79  .79  9.2  32 .0041 0     370    360    8700   790 560   520   8800 940
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c 2 .13  .13  1.6  26 .0041 .12  850    770    16000   7000 22   12   420 550
bitvector-regression/implicitfloatconversion_false-unreach-call.c 1 .14  .12  .78 22 .0041 0     3.4  1.9  55   270 11   6.0 190 300
bitvector-regression/implicitunsignedconversion_false-unreach-call.c 1 .12  .12  .99 24 .0041 2.2   3.7  2.1  73   270 7.1 3.8 150 310
bitvector-regression/integerpromotion_false-unreach-call.c 1 .12  .11  .82 22 .0041 0     3.5  2.0  70   280 11   5.9 140 310
bitvector-regression/recHanoi03_false-unreach-call.c 0 .12  .12  .69 22 .0041 0     .50 .34 4.6 40 5.9 3.1 120 300
bitvector-regression/signextension2_false-unreach-call.c 1 .12  .12  .97 22 .0041 0     3.7  2.0  76   270 7.3 3.8 140 320
bitvector-regression/signextension_false-unreach-call.c 1 .11  .11  .75 22 .0041 0     3.8  2.1  78   270 7.0 3.7 140 320
bitvector-regression/implicitunsignedconversion_true-unreach-call.c 2 .097 .094 .77 22 .0041 0     3.4  1.9  62   250 7.5 3.9 140 310
bitvector-regression/integerpromotion_true-unreach-call.c 2 .11  .10  .76 22 .0041 .12  3.3  1.9  58   260 13   6.9 230 340
bitvector-regression/signextension2_true-unreach-call.c 2 .095 .094 .74 22 .0041 0     3.3  1.8  59   260 7.7 4.1 160 320
bitvector-regression/signextension_true-unreach-call.c 2 .11  .10  .68 22 .0041 0     3.9  2.2  48   260 7.8 4.2 130 320
bitvector-loops/diamond_false-unreach-call2.i 1 .13  .13  1.1  24 0      .16  4.3  2.4  91   290 7.4 4.0 130 340
bitvector-loops/overflow_false-unreach-call1.i 0 900     900     11000    1400 0      0     .48 .31 12   40 6.1 3.2 120 310
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 1 .94  .93  12    37 0      0     5.9  3.3  100   300 92   56   720 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 54 15000   15000   160000 59000 .11   13   50 58 32 940 3400   50 260 150 3300 12000   50 4300 3900 90000 35000   50 7900 7400 150000 22000  
    correct results 32 53 110   110   1000 1900 .074  13   11 57 31 920 3200   10 240 140 3000 11000   18 3400 3100 72000 27000   15 6800 6400 130000 15000  
        correct true 21 42 47   47   440 1100 .041  11   0 0 0 0 0   1 0 0 0 0   18 3400 3100 72000 27000   14 6800 6400 130000 15000  
        correct false 11 11 64   64   580 850 .033  2.4 11 57 31 920 3200   9 240 140 3000 11000   0 0 0 0 0   1 0 0 0 0  
    correct-unconfimed results 1 1 6.7 6.7 80 150 .0041 0   0 0 0 0 0   0 0 0 0 0   0 840 770 18000 7000   0 960 920 16000 2100  
        correct-unconfirmed true 1 1 6.7 6.7 80 150 .0041 0   0 0 0 0 0   0 0 0 0 0   0 840 770 18000 7000   0 960 920 16000 2100  
        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