Tool SeaHorn-F16 0.1.0
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-13 15:22:34 CET [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]]
Run set sv-comp16.BitVectorsReach
Options --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.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 .64 .34  62 wit timeout 90   79   3700 true 12   7.1 320
bitvector/byte_add_1_true-unreach-call.i false(reach) .57 .31  47 wit - -
bitvector/byte_add_2_true-unreach-call.i false(reach) .58 .32  49 wit - -
bitvector/gcd_1_true-unreach-call.i false(reach) .29 .17  39 wit - -
bitvector/gcd_2_true-unreach-call.i false(reach) .33 .20  39 wit - -
bitvector/gcd_3_true-unreach-call.i false(reach) .30 .18  39 wit - -
bitvector/gcd_4_true-unreach-call.i false(reach) .49 .29  41 wit - -
bitvector/interleave_bits_true-unreach-call.i false(reach) .38 .23  42 wit - -
bitvector/jain_1_true-unreach-call.i true .28 .17  37 wit - -
bitvector/jain_2_true-unreach-call.i true .28 .17  37 wit - -
bitvector/jain_4_true-unreach-call.i true .19 .13  27 wit - -
bitvector/jain_5_true-unreach-call.i true .23 .16  28 wit - -
bitvector/jain_6_true-unreach-call.i true .22 .14  28 wit - -
bitvector/jain_7_true-unreach-call.i true .15 .096 28 wit - -
bitvector/modulus_true-unreach-call.i false(reach) .31 .19  40 wit - -
bitvector/num_conversion_1_true-unreach-call.i true .19 .12  30 wit - -
bitvector/num_conversion_2_true-unreach-call.i false(reach) .26 .16  38 wit - -
bitvector/parity_true-unreach-call.i false(reach) .27 .17  39 wit - -
bitvector/sum02_true-unreach-call.i false(reach) .31 .19  40 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c false(reach) 3.1  1.6   81 wit false(reach) 13   7.1 500 true 12   6.8 330
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c witness timeout 9.9  5.0   81 wit timeout 90   78   3500 true 13   7.3 340
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c false(reach) 1.4  .76  76 wit false(reach) 12   6.3 440 true 13   7.8 340
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c true 10    5.2   72 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 77    38     110 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 33    17     94 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c true 59    30     77 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c true 170    86     93 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c true 140    70     85 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c true 91    45     86 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c true 50    25     96 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c true 140    68     140 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c false(reach) .51 .29  59 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c true .47 .26  53 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c false(reach) .45 .24  54 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c false(reach) .55 .30  62 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c true .48 .27  52 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i witness unconfirmed .19 .12  34 wit true 4.2 2.5 210 error 9.2 5.3 300
bitvector-regression/implicitunsignedconversion_false-unreach-call.i witness unconfirmed .20 .13  34 wit true 4.0 2.4 210 true 10   6.4 320
bitvector-regression/integerpromotion_false-unreach-call.i witness unconfirmed .22 .14  35 wit true 7.0 4.0 260 true 11   6.8 310
bitvector-regression/signextension2_false-unreach-call.i witness unconfirmed .20 .13  34 wit true 8.7 4.9 290 true 9.7 5.5 330
bitvector-regression/signextension_false-unreach-call.i witness unconfirmed .23 .15  35 wit true 9.6 5.2 310 true 11   6.7 320
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true .17 .11  29 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true .19 .12  29 wit - -
bitvector-regression/signextension2_true-unreach-call.i true .25 .16  29 wit - -
bitvector-regression/signextension_true-unreach-call.i true .22 .14  29 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) .38 .22  39 wit false(reach) 6.0 3.5 250 true 11   7.6 330
bitvector-loops/overflow_false-unreach-call1.i witness timeout .20 .12  34 wit timeout 91   83   730 true 12   7.2 320
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i true .34 .21  38 wit - -
../../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 800    400    2500 48 340   280   10000   48 120   74   3600  
    correct results 25 780    390    1500 3 31   17   1200   3 37   22   1000  
        correct true 22 770    390    1300 0 0   0   0   3 0   0   0  
        correct false 3 4.9  2.6  200 3 31   17   1200   0 37   22   1000  
    incorrect results 15 6.0  3.4  660 0 0   0   0   0 0   0   0  
        incorrect true 1 .34 .21 38 0 0   0   0   0 0   0   0  
        incorrect false 14 5.6  3.2  630 0 0   0   0   0 0   0   0  
score (48 tasks, max score: 84) -209
Run set sv-comp16.BitVectorsReach