Tool DepthK ESBMC+DepthK version 2.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-22-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-05 14:06:34 CET [[ 2016-01-15 09:00:06 CET ]] [[ 2016-01-15 22:17:52 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/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmcdepthk.2016-01-05_1406.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 4.2  2.6  170 wit timeout 91   70   2200 true 12   6.6 320
bitvector/byte_add_1_true-unreach-call.i true 1.4  1.4  26 wit - -
bitvector/byte_add_2_true-unreach-call.i true 1.3  1.4  26 wit - -
bitvector/gcd_1_true-unreach-call.i true 3.9  4.0  110 wit - -
bitvector/gcd_2_true-unreach-call.i true 85    85    110 wit - -
bitvector/gcd_3_true-unreach-call.i true 200    200    120 wit - -
bitvector/gcd_4_true-unreach-call.i true .69 .72 22 wit - -
bitvector/interleave_bits_true-unreach-call.i true 4.9  5.1  31 wit - -
bitvector/jain_1_true-unreach-call.i true .54 .57 41 wit - -
bitvector/jain_2_true-unreach-call.i true 11    11    79 wit - -
bitvector/jain_4_true-unreach-call.i true 150    150    170 wit - -
bitvector/jain_5_true-unreach-call.i true .41 .44 21 wit - -
bitvector/jain_6_true-unreach-call.i true 140    140    170 wit - -
bitvector/jain_7_true-unreach-call.i true 12    12    55 wit - -
bitvector/modulus_true-unreach-call.i true 130    130    720 wit - -
bitvector/num_conversion_1_true-unreach-call.i true 1.7  1.8  22 wit - -
bitvector/num_conversion_2_true-unreach-call.i true 2.4  2.5  22 wit - -
bitvector/parity_true-unreach-call.i unknown 890    900    240 wit - -
bitvector/sum02_true-unreach-call.i unknown 47    48    27 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c witness timeout 64    63    290 wit timeout 91   69   3800 true 14   8.2 340
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c false(reach) 54    52    230 wit false(reach) 15   7.8 570 true 14   7.6 350
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c false(reach) 53    51    230 wit false(reach) 13   7.0 500 true 13   7.3 350
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c true 7.5  7.5  280 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 5.2  5.2  220 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 6.8  6.8  210 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c unknown 890    900    430 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c true 6.1  6.1  280 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c true 11    11    240 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c true 13    13    250 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c true 9.6  9.6  300 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c true 11    11    300 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c true 1.9  1.9  43 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c true .71 .73 41 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c true 17    18    45 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c true 25    25    49 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c true .75 .78 41 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i false(reach) 3.1  1.5  170 wit false(reach) 4.7 2.8 230 error 8.3 4.8 320
bitvector-regression/implicitunsignedconversion_false-unreach-call.i false(reach) 2.9  1.4  160 wit false(reach) 4.5 2.7 220 true 9.7 6.0 310
bitvector-regression/integerpromotion_false-unreach-call.i false(reach) 4.7  2.9  170 wit false(reach) 7.6 4.2 340 true 10   7.0 310
bitvector-regression/signextension2_false-unreach-call.i false(reach) 4.3  2.4  180 wit false(reach) 8.3 4.5 340 true 10   6.2 310
bitvector-regression/signextension_false-unreach-call.i false(reach) 4.9  3.1  170 wit false(reach) 8.4 4.6 360 true 12   7.3 340
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true .33 .36 21 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true .70 .73 28 wit - -
bitvector-regression/signextension2_true-unreach-call.i true .54 .57 27 wit - -
bitvector-regression/signextension_true-unreach-call.i true .51 .54 27 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) 3.5  2.0  160 wit false(reach) 6.3 3.6 250 true 11   6.3 330
bitvector-loops/overflow_false-unreach-call1.i unknown 31    32    22 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(reach) 3.5  1.9  160 wit false(reach) 8.7 5.1 380 true 11   6.5 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 2900 2900 6900 48 260   180   9200   48 130   74   3600  
    correct results 42 1000 990 5800 9 76   42   3200   8 100   59   2900  
        correct true 33 870 870 4100 0 0   0   0   8 0   0   0  
        correct false 9 130 120 1600 9 76   42   3200   0 100   59   2900  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 84) 75
Run set sv-comp16.BitVectorsReach