Tool ESBMC ESBMC version 2.0.0 64-bit x86_64 linux
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-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 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/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.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 false(reach) 810     620     5100 wit false(reach) 9.3 5.1 370 true 13   7.2 350
bitvector/byte_add_1_true-unreach-call.i true .81  .82  69 wit - -
bitvector/byte_add_2_true-unreach-call.i true .78  .80  70 wit - -
bitvector/gcd_1_true-unreach-call.i true 2.3   2.3   160 wit - -
bitvector/gcd_2_true-unreach-call.i true 54     54     240 wit - -
bitvector/gcd_3_true-unreach-call.i true 49     49     240 wit - -
bitvector/gcd_4_true-unreach-call.i true .067 .078 13 wit - -
bitvector/interleave_bits_true-unreach-call.i true .12  .13  13 wit - -
bitvector/jain_1_true-unreach-call.i true .23  .24  19 wit - -
bitvector/jain_2_true-unreach-call.i true .27  .29  27 wit - -
bitvector/jain_4_true-unreach-call.i true .33  .34  33 wit - -
bitvector/jain_5_true-unreach-call.i true .098 .11  12 wit - -
bitvector/jain_6_true-unreach-call.i true .42  .43  34 wit - -
bitvector/jain_7_true-unreach-call.i true .36  .38  28 wit - -
bitvector/modulus_true-unreach-call.i unknown 900     900     3400 wit - -
bitvector/num_conversion_1_true-unreach-call.i true .075 .084 13 wit - -
bitvector/num_conversion_2_true-unreach-call.i true .075 .086 13 wit - -
bitvector/parity_true-unreach-call.i true 1.3   1.3   15 wit - -
bitvector/sum02_true-unreach-call.i error (1) 14     10     490 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c false(reach) 810     570     6200 wit false(reach) 15   7.7 520 true 11   6.9 320
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c timeout 910     520     7300 wit - -
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c witness timeout 810     560     7000 wit timeout 91   70   3800 true 11   6.2 340
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c true 70     70     1800 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 61     61     1500 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 73     73     1600 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c unknown 890     900     2800 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c true 70     70     1900 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c unknown 890     900     1600 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c unknown 890     900     1700 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c true 70     70     1900 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c true 65     65     1900 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c true 1.2   1.2   120 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c true .77  .77  120 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c true .98  .99  120 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c true 8.4   8.4   130 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c true 1.0   1.0   120 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i false(reach) 3.2   10     220 wit false(reach) 4.6 2.8 230 error 9.5 5.4 310
bitvector-regression/implicitunsignedconversion_false-unreach-call.i false(reach) 3.7   10     210 wit false(reach) 4.5 2.6 220 true 12   7.1 340
bitvector-regression/integerpromotion_false-unreach-call.i false(reach) 7.8   12     280 wit false(reach) 7.8 4.4 340 true 11   6.8 310
bitvector-regression/signextension2_false-unreach-call.i false(reach) 8.5   11     300 wit false(reach) 8.2 4.7 340 true 11   5.9 320
bitvector-regression/signextension_false-unreach-call.i false(reach) 11     12     340 wit false(reach) 7.9 4.4 300 true 11   6.9 320
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true .064 .073 13 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true .096 .11  17 wit - -
bitvector-regression/signextension2_true-unreach-call.i true .081 .090 17 wit - -
bitvector-regression/signextension_true-unreach-call.i true .086 .097 17 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) 13     15     360 wit false(reach) 6.4 3.7 250 true 11   6.4 330
bitvector-loops/overflow_false-unreach-call1.i error (1) 78     50     3900 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i error (1) 30     10     720 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 7600 6500 54000 48 150   110   6400   48 99   59   2900  
    correct results 39 2200 1800 25000 8 63   35   2600   7 88   53   2600  
        correct true 31 530 530 12000 0 0   0   0   7 0   0   0  
        correct false 8 1700 1300 13000 8 63   35   2600   0 88   53   2600  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 84) 70
Run set sv-comp16.BitVectorsReach