Tool CBMC
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-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.BitVectorsReach
Options --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.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) .30  .31 25 wit false(reach) 9.0 5.0 400 false(reach) 75   46   570
bitvector/byte_add_1_true-unreach-call.i true 5.8   5.8  100 wit - -
bitvector/byte_add_2_true-unreach-call.i true 6.0   6.0  110 wit - -
bitvector/gcd_1_true-unreach-call.i true 12     12    570 wit - -
bitvector/gcd_2_true-unreach-call.i true 12     12    580 wit - -
bitvector/gcd_3_true-unreach-call.i true 13     13    570 wit - -
bitvector/gcd_4_true-unreach-call.i true .88  .91 24 wit - -
bitvector/interleave_bits_true-unreach-call.i true 1.1   1.1  24 wit - -
bitvector/jain_1_true-unreach-call.i true 29     29    5800 wit - -
bitvector/jain_2_true-unreach-call.i true 59     59    12000 wit - -
bitvector/jain_4_true-unreach-call.i true 74     74    14000 wit - -
bitvector/jain_5_true-unreach-call.i true 1.1   1.1  24 wit - -
bitvector/jain_6_true-unreach-call.i true 58     58    11000 wit - -
bitvector/jain_7_true-unreach-call.i true 30     31    4200 wit - -
bitvector/modulus_true-unreach-call.i true 220     220    14000 wit - -
bitvector/num_conversion_1_true-unreach-call.i true 1.1   1.1  24 wit - -
bitvector/num_conversion_2_true-unreach-call.i true 1.1   1.2  24 wit - -
bitvector/parity_true-unreach-call.i true 7.5   7.5  42 wit - -
bitvector/sum02_true-unreach-call.i true 2.5   2.5  40 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c false(reach) 5.1   5.2  180 wit timeout 91   67   3800 false(reach) 43   24   530
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c false(reach) 4.6   4.7  150 wit timeout 91   70   3800 false(reach) 40   22   550
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c witness timeout 1.0   1.0  55 wit timeout 91   69   3700 unknown 34   18   500
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c true 850     850    1100 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 850     850    1100 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 850     850    3000 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c true 850     850    600 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c true 850     850    770 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c true 850     850    670 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c true 850     850    700 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c true 850     850    700 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c true 850     850    710 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c true 850     850    190 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c true 850     850    190 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c true 850     850    170 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c true 850     850    190 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c true 850     850    180 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i false(reach) .16  .18 24 wit false(reach) 3.9 2.3 230 error 8.9 4.9 310
bitvector-regression/implicitunsignedconversion_false-unreach-call.i false(reach) .11  .12 24 wit false(reach) 4.2 2.6 220 false(reach) 11   6.6 330
bitvector-regression/integerpromotion_false-unreach-call.i false(reach) .13  .14 26 wit false(reach) 5.8 3.3 260 false(reach) 18   10   380
bitvector-regression/signextension2_false-unreach-call.i false(reach) .12  .13 26 wit false(reach) 7.4 4.1 340 false(reach) 12   6.8 330
bitvector-regression/signextension_false-unreach-call.i false(reach) .10  .11 26 wit false(reach) 7.0 3.9 340 false(reach) 11   7.6 320
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true 1.1   1.1  24 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true 1.2   1.2  26 wit - -
bitvector-regression/signextension2_true-unreach-call.i true 1.0   1.1  26 wit - -
bitvector-regression/signextension_true-unreach-call.i true 1.2   1.3  26 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) .19  .20 25 wit false(reach) 6.0 3.4 260 false(reach) 12   7.8 330
bitvector-loops/overflow_false-unreach-call1.i true 1.2   1.2  24 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(reach) .47  .48 25 wit false(reach) 8.4 4.7 420 timeout 91   81   400
../../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 12000   12000   74000 48 320   240   14000   48 360   240   4600  
    correct results 46 12000   12000   74000 8 230   170   10000   8 320   220   4100  
        correct true 36 12000   12000   74000 0 0   0   0   0 0   0   0  
        correct false 10 11   11   540 8 230   170   10000   8 320   220   4100  
    incorrect results 1 1.2 1.2 24 0 0   0   0   0 0   0   0  
        incorrect true 1 1.2 1.2 24 0 0   0   0   0 0   0   0  
        incorrect false 0
score (48 tasks, max score: 84) 50
Run set sv-comp16.BitVectorsReach