Tool Ceagle AbsRef 1.0.0
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-04 05:59:47 CET [[ 2016-01-15 08:28:20 CET ]] [[ 2016-01-15 21:58:46 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/ceagle-absref.2016-01-04_0559.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ceagle-absref.2016-01-04_0559.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 unknown .32  .35  5.9 wit - -
bitvector/byte_add_1_true-unreach-call.i unknown .21  .24  5.9 wit - -
bitvector/byte_add_2_true-unreach-call.i unknown .21  .24  5.7 wit - -
bitvector/gcd_1_true-unreach-call.i true .30  .32  5.9 wit - -
bitvector/gcd_2_true-unreach-call.i unknown .43  .46  6.0 wit - -
bitvector/gcd_3_true-unreach-call.i unknown .54  .57  6.1 wit - -
bitvector/gcd_4_true-unreach-call.i unknown .21  .24  9.1 wit - -
bitvector/interleave_bits_true-unreach-call.i unknown .084 .11  5.6 wit - -
bitvector/jain_1_true-unreach-call.i unknown .080 .11  5.5 wit - -
bitvector/jain_2_true-unreach-call.i unknown .11  .14  5.8 wit - -
bitvector/jain_4_true-unreach-call.i unknown .070 .093 6.0 wit - -
bitvector/jain_5_true-unreach-call.i unknown .13  .15  5.7 wit - -
bitvector/jain_6_true-unreach-call.i unknown .12  .14  5.9 wit - -
bitvector/jain_7_true-unreach-call.i unknown .069 .094 5.6 wit - -
bitvector/modulus_true-unreach-call.i unknown .15  .17  5.8 wit - -
bitvector/num_conversion_1_true-unreach-call.i unknown .12  .15  5.7 wit - -
bitvector/num_conversion_2_true-unreach-call.i unknown .098 .12  5.6 wit - -
bitvector/parity_true-unreach-call.i unknown .12  .14  5.9 wit - -
bitvector/sum02_true-unreach-call.i unknown .087 .11  5.7 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c unknown .26  .28  6.3 wit - -
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c unknown .46  .49  6.3 wit - -
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c unknown .50  .53  6.3 wit - -
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c unknown .27  .29  6.3 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c unknown .45  .49  6.3 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c unknown .45  .49  6.4 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c unknown .38  .41  6.3 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c unknown .43  .46  6.3 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c unknown .57  .59  6.3 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c unknown .38  .41  6.4 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c unknown .40  .42  6.3 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c unknown .51  .54  6.3 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c unknown .23  .25  5.9 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c unknown .22  .25  5.9 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c unknown .29  .31  6.0 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c false(reach) .29  .32  5.8 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c unknown .15  .18  5.7 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i witness unconfirmed .096 .12  5.9 wit true 4.1 2.4 210 error 10 6.7 310
bitvector-regression/implicitunsignedconversion_false-unreach-call.i true .085 .11  5.6 wit - -
bitvector-regression/integerpromotion_false-unreach-call.i unknown .095 .12  6.1 wit - -
bitvector-regression/signextension2_false-unreach-call.i unknown .090 .12  6.0 wit - -
bitvector-regression/signextension_false-unreach-call.i unknown .11  .15  6.0 wit - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.i false(reach) .075 .098 5.6 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i unknown .088 .12  6.0 wit - -
bitvector-regression/signextension2_true-unreach-call.i unknown .074 .10  6.0 wit - -
bitvector-regression/signextension_true-unreach-call.i unknown .056 .079 6.0 wit - -
bitvector-loops/diamond_false-unreach-call2.i unknown .19  .21  5.7 wit - -
bitvector-loops/overflow_false-unreach-call1.i unknown .098 .12  5.6 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i unknown .082 .10  5.9 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 11     12    290   48 4.1 2.4 210   48 10   6.7 310  
    correct results 1 .30  .32 5.9 0 0   0   0   0 0   0   0  
        correct true 1 .30  .32 5.9 0 0   0   0   0 0   0   0  
        correct false 0
    incorrect results 3 .45  .53 17   0 0   0   0   0 0   0   0  
        incorrect true 1 .085 .11 5.6 0 0   0   0   0 0   0   0  
        incorrect false 2 .36  .42 11   0 0   0   0   0 0   0   0  
score (48 tasks, max score: 84) -62
Run set sv-comp16.BitVectorsReach