Tool impara 0.45
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 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]]
Run set sv-comp16.BitVectorsReach
Options --eager --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/impara.2016-01-13_0741.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) 3.5   3.5   24 wit false(reach) 9.0 5.0 380 false(reach) 47   28   520
bitvector/byte_add_1_true-unreach-call.i true 7.7   7.7   24 wit - -
bitvector/byte_add_2_true-unreach-call.i true 8.2   8.2   24 wit - -
bitvector/gcd_1_true-unreach-call.i true 1.1   1.1   29 wit - -
bitvector/gcd_2_true-unreach-call.i true 2.2   2.2   27 wit - -
bitvector/gcd_3_true-unreach-call.i timeout 900     900     4000 wit - -
bitvector/gcd_4_true-unreach-call.i true .15  .16  23 wit - -
bitvector/interleave_bits_true-unreach-call.i true .22  .22  23 wit - -
bitvector/jain_1_true-unreach-call.i timeout 900     900     290 wit - -
bitvector/jain_2_true-unreach-call.i timeout 900     900     280 wit - -
bitvector/jain_4_true-unreach-call.i timeout 900     900     250 wit - -
bitvector/jain_5_true-unreach-call.i timeout 900     900     77 wit - -
bitvector/jain_6_true-unreach-call.i timeout 900     900     200 wit - -
bitvector/jain_7_true-unreach-call.i timeout 900     900     110 wit - -
bitvector/modulus_true-unreach-call.i timeout 900     900     350 wit - -
bitvector/num_conversion_1_true-unreach-call.i true .16  .16  23 wit - -
bitvector/num_conversion_2_true-unreach-call.i true 170     170     43 wit - -
bitvector/parity_true-unreach-call.i timeout 900     900     11000 wit - -
bitvector/sum02_true-unreach-call.i timeout 900     900     80 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c witness timeout 4.7   4.7   27 wit timeout 91   71   3800 true 15   8.7 360
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c witness timeout 9.9   9.9   29 wit timeout 91   70   3800 true 16   8.8 350
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c witness timeout .93  .93  26 wit timeout 90   73   3800 true 16   10   340
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c true 69     69     33 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 33     33     29 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 41     41     31 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c timeout 900     900     390 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c timeout 900     900     130 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c timeout 900     900     250 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c timeout 900     900     250 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c timeout 900     900     130 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c timeout 900     900     130 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c true 16     17     34 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c timeout 900     900     160 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c timeout 900     900     110 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c true 9.3   9.3   28 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c true 1.7   1.7   31 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i false(reach) .12  .12  23 wit false(reach) 4.3 2.6 230 error 9.6 5.4 310
bitvector-regression/implicitunsignedconversion_false-unreach-call.i false(reach) .087 .089 23 wit false(reach) 4.5 2.6 220 false(reach) 11   7.7 320
bitvector-regression/integerpromotion_false-unreach-call.i false(reach) .12  .12  25 wit false(reach) 7.2 4.1 340 false(reach) 21   13   380
bitvector-regression/signextension2_false-unreach-call.i false(reach) .092 .095 25 wit false(reach) 6.4 3.6 340 false(reach) 12   6.7 340
bitvector-regression/signextension_false-unreach-call.i false(reach) .12  .12  25 wit false(reach) 7.6 4.3 330 false(reach) 11   6.7 350
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true .11  .11  22 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true .11  .11  25 wit - -
bitvector-regression/signextension2_true-unreach-call.i true .15  .15  25 wit - -
bitvector-regression/signextension_true-unreach-call.i true .092 .095 25 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) .68  .69  23 wit false(reach) 6.0 3.4 250 false(reach) 13   7.1 340
bitvector-loops/overflow_false-unreach-call1.i timeout 900     900     29 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(reach) 3.2   3.2   32 wit false(reach) 9.4 5.2 410 timeout 91   84   380
../../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 17000   17000   19000 48 330   250   14000   48 260   190   4000  
    correct results 26 360   360   700 8 54   31   2500   6 220   160   2900  
        correct true 18 360   360   500 0 0   0   0   0 0   0   0  
        correct false 8 7.9 7.9 200 8 54   31   2500   6 220   160   2900  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 84) 44
Run set sv-comp16.BitVectorsReach