Tool Forest svc_16_20151108
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]
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-09 23:49:59 CET [[ 2016-01-15 09:05:13 CET ]] [[ 2016-01-15 22:20:31 CET ]]
Run set sv-comp16.BitVectorsReach
Options -svcomp [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/forest.2016-01-09_2349.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/forest.2016-01-09_2349.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 true 2.5  2.9  39 wit - -
bitvector/byte_add_1_true-unreach-call.i true .69 .78 38 wit - -
bitvector/byte_add_2_true-unreach-call.i true 130    130    1800 wit - -
bitvector/gcd_1_true-unreach-call.i true .48 .57 39 wit - -
bitvector/gcd_2_true-unreach-call.i true 1.6  1.9  38 wit - -
bitvector/gcd_3_true-unreach-call.i true 1.7  2.1  38 wit - -
bitvector/gcd_4_true-unreach-call.i true 1.0  1.2  39 wit - -
bitvector/interleave_bits_true-unreach-call.i true .55 .64 38 wit - -
bitvector/jain_1_true-unreach-call.i false(reach) 56    58    38 wit - -
bitvector/jain_2_true-unreach-call.i true 110    120    84 wit - -
bitvector/jain_4_true-unreach-call.i unknown .53 .62 38 wit - -
bitvector/jain_5_true-unreach-call.i true 16    16    38 wit - -
bitvector/jain_6_true-unreach-call.i true .50 .58 38 wit - -
bitvector/jain_7_true-unreach-call.i unknown .59 .69 38 wit - -
bitvector/modulus_true-unreach-call.i true .64 .74 39 wit - -
bitvector/num_conversion_1_true-unreach-call.i true 1.4  1.7  38 wit - -
bitvector/num_conversion_2_true-unreach-call.i unknown .50 .59 38 wit - -
bitvector/parity_true-unreach-call.i true 3.0  3.5  38 wit - -
bitvector/sum02_true-unreach-call.i unknown .61 .69 38 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c true 3.2  3.5  39 wit - -
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c unknown .81 .90 39 wit - -
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c true 11    12    39 wit - -
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c true 2.9  3.2  39 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true .43 .53 17 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c unknown .75 .85 39 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c true .98 1.1  39 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c true .90 1.0  39 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c true 1.3  1.5  39 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c true 600    640    110 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c true 3.0  3.4  40 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c unknown .83 .92 39 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c true 410    450    39 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c true 1.6  1.9  39 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c true 2.4  2.8  39 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c true .74 .84 39 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c unknown .66 .76 39 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i false(reach) .51 .60 38 wit false(reach) 4.3 2.6 220 error 11 7.1 310
bitvector-regression/implicitunsignedconversion_false-unreach-call.i false(reach) .61 .71 38 wit false(reach) 4.5 2.6 220 true 10 7.1 320
bitvector-regression/integerpromotion_false-unreach-call.i true .62 .72 38 wit - -
bitvector-regression/signextension2_false-unreach-call.i unknown .50 .59 38 wit - -
bitvector-regression/signextension_false-unreach-call.i unknown .55 .65 39 wit - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true .55 .67 38 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true .72 .85 39 wit - -
bitvector-regression/signextension2_true-unreach-call.i unknown .60 .69 39 wit - -
bitvector-regression/signextension_true-unreach-call.i true .71 .82 39 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) 1.8  2.1  39 wit false(reach) 5.7 3.3 250 true 11 6.9 330
bitvector-loops/overflow_false-unreach-call1.i true .56 .66 38 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i true .68 .78 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 1400   1500   3700 48 14   8.5 700   48 32   21   950  
    correct results 30 1300   1400   3000 3 14   8.5 700   2 32   21   950  
        correct true 27 1300   1400   2900 0 0   0   0   2 0   0   0  
        correct false 3 2.9 3.4 110 3 14   8.5 700   0 32   21   950  
    incorrect results 7 74   78   270 0 0   0   0   0 0   0   0  
        incorrect true 6 18   20   230 0 0   0   0   0 0   0   0  
        incorrect false 1 56   58   38 0 0   0   0   0 0   0   0  
score (48 tasks, max score: 84) -151
Run set sv-comp16.BitVectorsReach