Tool symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a
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-13 11:10:58 CET [[ 2017-01-15 02:01:54 CET ]] [[ 2017-01-15 02:34:25 CET ]] [[ 2017-01-15 02:04:28 CET ]] [[ 2017-01-15 03:02:21 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.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 0 .20 .20 2.3 11   .012 0    95    85    3100   700 7.5 4.0 150 320
bitvector/sum02_false-unreach-call_true-no-overflow.i 0 900    900    10000   800   .012 0    .52 .33 11   40 7.1 3.8 66 300
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 2 .22 .22 2.2 10   .012 0    9.9  5.4  150   330 420   370   14000 1400
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 2 .31 .42 2.5 18   .012 8.2  9.7  5.3  84   340 470   410   11000 1300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 2 .21 .21 2.1 11   .012 0    13    11    170   310 960   950   14000 570
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 2.0  2.0  25   14   .012 0    120    120    3200   470 960   950   18000 580
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 2 2.1  2.1  27   14   .012 0    130    120    2300   470 960   950   20000 850
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 2 .13 .13 1.9 9.4 .012 0    7.4  5.1  120   310 960   940   27000 900
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2 .18 .18 2.0 10   .012 0    8.1  5.1  64   330 120   91   1600 650
bitvector/jain_1_true-unreach-call_true-no-overflow.i 0 900    900    9100   75   .012 0    .50 .31 7.6 40 7.2 3.8 79 300
bitvector/jain_2_true-unreach-call_true-no-overflow.i 0 900    900    8300   93   .012 0    .54 .35 9.1 40 6.1 3.2 120 300
bitvector/jain_4_true-unreach-call_true-no-overflow.i 0 900    920    12000   15000   .012 0    .64 .41 10   41 5.6 3.0 89 300
bitvector/jain_5_true-unreach-call_true-no-overflow.i 0 890    930    13000   15000   .012 0    .50 .32 12   41 5.6 3.1 120 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i 0 890    930    12000   15000   .012 0    .52 .34 11   40 6.7 3.5 89 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i 0 890    930    12000   15000   .012 0    .51 .33 11   42 7.9 4.1 81 300
bitvector/modulus_true-unreach-call_true-no-overflow.i 2 270    270    3400   56   .012 0    15    13    350   330 32   29   880 330
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 2 .15 .15 1.4 9.4 .012 0    4.9  2.7  100   280 66   51   1500 510
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 2 .15 .15 1.7 9.8 .012 0    5.7  3.2  75   280 960   930   14000 1100
bitvector/parity_true-unreach-call_true-no-overflow.i 2 1.4  1.4  20   11   .012 0    25    21    560   340 960   940   27000 1000
bitvector/sum02_true-unreach-call_true-no-overflow.i 0 900    900    12000   800   .012 0    .49 .31 11   39 6.1 3.2 120 300
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 0 .37 .36 4.6 11   .12  0    7.6  4.1  93   280 8.3 4.4 180 310
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 0 .48 .48 5.7 12   .12  0    6.0  3.3  110   290 9.1 5.0 110 310
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 1 .29 .28 2.8 11   .12  .32 7.7  4.1  150   310 8.0 4.3 130 310
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 2 .62 .74 7.2 20   .12  8.5  59    50    1200   950 43   23   380 800
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 2 .52 .51 6.3 11   .12  0    17    10    320   590 57   31   1000 1000
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 2 .52 .52 6.7 12   .12  0    15    8.5  220   570 44   23   580 890
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900    900    9700   370   .14  0    .48 .31 8.0 39 5.9 3.1 110 300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900    900    10000   580   .14  0    .53 .35 12   39 5.8 3.1 70 290
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900    900    12000   190   .14  0    .50 .33 12   41 6.2 3.3 120 300
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900    900    9300   160   .14  0    .50 .32 8.0 41 7.4 3.9 85 300
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900    900    9800   270   .14  0    .51 .34 8.5 39 5.5 3.0 110 290
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900    900    10000   270   .14  0    .51 .33 11   40 6.5 3.5 110 300
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c 2 500    500    6200   190   .025 0    900    850    14000   6300 130   110   1800 870
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c 2 2.6  2.6  32   15   .025 0    760    680    11000   7000 79   66   1300 920
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c 1 4.4  4.4  66   17   .025 0    780    700    14000   7000 960   920   21000 1900
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c 0 900    900    13000   150   .025 0    .58 .39 7.7 40 5.6 3.0 88 300
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c 2 2.6  2.7  28   23   .025 7.8  870    790    11000   7000 24   13   400 540
bitvector-regression/implicitfloatconversion_false-unreach-call.c 1 .13 .13 1.5 9.2 .012 0    3.9  2.2  57   280 14   7.3 190 310
bitvector-regression/implicitunsignedconversion_false-unreach-call.c 1 .16 .16 1.4 9.1 .012 0    4.2  2.4  39   280 6.8 3.6 130 310
bitvector-regression/integerpromotion_false-unreach-call.c 1 .13 .13 1.7 9.2 .012 0    4.5  2.5  51   280 6.6 3.6 130 310
bitvector-regression/recHanoi03_false-unreach-call.c 0 900    900    12000   2800   .012 0    .67 .42 7.5 40 5.5 2.9 110 290
bitvector-regression/signextension2_false-unreach-call.c 1 .16 .16 1.6 9.4 .012 0    3.5  2.0  68   270 8.4 4.5 96 320
bitvector-regression/signextension_false-unreach-call.c 1 .16 .15 1.4 9.3 .012 .32 3.4  1.9  63   270 7.7 4.1 83 310
bitvector-regression/implicitunsignedconversion_true-unreach-call.c 2 .16 .16 1.3 9.4 .012 0    3.9  2.2  51   260 6.9 3.7 110 310
bitvector-regression/integerpromotion_true-unreach-call.c 2 .13 .12 1.3 9.3 .012 0    3.5  2.0  44   250 11   6.2 240 300
bitvector-regression/signextension2_true-unreach-call.c 2 .16 .16 1.4 9.2 .012 0    4.0  2.2  64   260 7.5 4.0 86 320
bitvector-regression/signextension_true-unreach-call.c 2 .13 .13 1.6 9.3 .012 0    3.4  1.9  69   270 9.2 4.9 97 320
bitvector-loops/diamond_false-unreach-call2.i 1 .16 .16 1.6 9.3 .012 0    4.6  2.6  57   270 9.9 5.4 120 350
bitvector-loops/overflow_false-unreach-call1.i 0 .13 .13 1.7 9.3 .012 0    96    87    2500   1900 7.4 3.9 140 320
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 0 .23 .22 2.8 12   .012 0    91    87    2100   1000 7.0 3.7 97 310
../../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 50 15000   15000   180000 67000 2.1   25    50 330 280 8400 6300   50 110 61 1700 4400   50 3800 3400 59000 35000   50 8300 7900 180000 22000  
    correct results 28 49 780   780   9700 550 .82  25    7 32 18 480 2000   7 61 33 880 2200   18 3000 2700 45000 27000   14 7300 6900 150000 15000  
        correct true 21 42 780   780   9700 480 .63  25    0 0 0 0 0   6 0 0 0 0   18 3000 2700 45000 27000   14 7300 6900 150000 15000  
        correct false 7 7 1.2 1.2 12 66 .20  .63 7 32 18 480 2000   1 61 33 880 2200   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 6 1 5.8 5.8 83 72 .31  0    2 300 270 7900 4200   5 39 21 680 1600   0 780 700 14000 7000   0 960 920 21000 1900  
        correct-unconfirmed true 1 1 4.4 4.4 66 17 .025 0    2 0 0 0 0   5 0 0 0 0   0 780 700 14000 7000   0 960 920 21000 1900  
        correct-unconfirmed false 5 0 1.4 1.4 17 55 .28  0    0 300 270 7900 4200   0 39 21 680 1600   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) 50
Run set sv-comp17.ReachSafety-BitVectors