Tool symbiotic 3.0.1
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-23-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-07 09:04:54 CET [[ 2016-01-15 09:39:10 CET ]] [[ 2016-01-15 22:39:28 CET ]]
Run set sv-comp16.BitVectorsReach
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
bitvector/byte_add_false-unreach-call.i witness timeout 35     35    9.1 wit timeout 90   71   1400 unknown 9.6 5.4 310
bitvector/byte_add_1_true-unreach-call.i true 250     250    8.2 wit - -
bitvector/byte_add_2_true-unreach-call.i true 460     460    8.4 wit - -
bitvector/gcd_1_true-unreach-call.i true 36     36    7.9 wit - -
bitvector/gcd_2_true-unreach-call.i unknown .51  .56 8.2 wit - -
bitvector/gcd_3_true-unreach-call.i unknown .60  .64 8.2 wit - -
bitvector/gcd_4_true-unreach-call.i true 18     18    5.8 wit - -
bitvector/interleave_bits_true-unreach-call.i true 8.0   8.0  6.5 wit - -
bitvector/jain_1_true-unreach-call.i timeout 870     930    110   wit - -
bitvector/jain_2_true-unreach-call.i timeout 900     910    61   wit - -
bitvector/jain_4_true-unreach-call.i timeout 900     910    79   wit - -
bitvector/jain_5_true-unreach-call.i timeout 900     900    5.7 wit - -
bitvector/jain_6_true-unreach-call.i timeout 900     910    80   wit - -
bitvector/jain_7_true-unreach-call.i timeout 900     910    73   wit - -
bitvector/modulus_true-unreach-call.i timeout 900     900    54   wit - -
bitvector/num_conversion_1_true-unreach-call.i true 18     18    5.6 wit - -
bitvector/num_conversion_2_true-unreach-call.i true 460     460    10   wit - -
bitvector/parity_true-unreach-call.i true 130     130    8.9 wit - -
bitvector/sum02_true-unreach-call.i timeout 900     900    17   wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c witness unconfirmed 5.3   5.4  21   wit true 32   16   810 unknown 11   6.3 320
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c timeout 900     900    19   wit - -
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c true 500     500    20   wit - -
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c timeout 900     900    38   wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 93     93    43   wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 510     510    20   wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c timeout 900     900    22   wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c timeout 900     900    21   wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c timeout 900     900    20   wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c timeout 900     900    20   wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c timeout 900     900    20   wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c timeout 900     900    19   wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c timeout 900     920    140   wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c timeout 900     900    9.5 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c timeout 900     900    9.1 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c timeout 900     900    22   wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c timeout 900     900    9.4 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i witness unconfirmed .18  .21 6.5 wit true 4.1 2.5 210 unknown 9.1 5.2 320
bitvector-regression/implicitunsignedconversion_false-unreach-call.i witness unconfirmed .13  .15 6.7 wit true 4.3 2.6 210 unknown 10   7.7 310
bitvector-regression/integerpromotion_false-unreach-call.i witness unconfirmed .18  .20 6.8 wit true 5.6 3.2 230 unknown 9.1 5.3 310
bitvector-regression/signextension2_false-unreach-call.i witness unconfirmed .22  .24 6.7 wit true 5.4 3.1 230 unknown 8.5 4.8 310
bitvector-regression/signextension_false-unreach-call.i witness unconfirmed .23  .24 6.7 wit true 5.7 3.3 230 unknown 9.9 5.8 330
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true .17  .19 5.9 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true .076 .10 5.7 wit - -
bitvector-regression/signextension2_true-unreach-call.i true .10  .12 5.6 wit - -
bitvector-regression/signextension_true-unreach-call.i true .11  .12 5.7 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) .13  .16 6.5 wit false(reach) 5.6 3.2 250 unknown 8.8 5.1 330
bitvector-loops/overflow_false-unreach-call1.i witness timeout .20  .22 6.8 wit timeout 91   82   740 unknown 9.1 5.2 300
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i witness timeout 210     210    8.8 wit timeout 90   83   2600 unknown 10   5.8 320
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 48 22000    22000    1100   48 330   270   6800   48 95   56   3200  
    correct results 15 2000    2000    150   1 5.6 3.2 250   0 8.8 5.1 330  
        correct true 14 2000    2000    150   0 0   0   0   0 0   0   0  
        correct false 1 .13 .16 6.5 1 5.6 3.2 250   0 8.8 5.1 330  
    incorrect results 1 500    500    20   0 0   0   0   0 0   0   0  
        incorrect true 1 500    500    20   0 0   0   0   0 0   0   0  
        incorrect false 0
score (48 tasks, max score: 84) -3
Run set sv-comp16.BitVectorsReach