Tool CPAchecker 1.4-svn 18373
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 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]]
Run set sv-comp16.BitVectorsReach
Options -sv-comp16--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.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 timeout 900   850   1300 wit - -
bitvector/byte_add_1_true-unreach-call.i timeout 900   870   810 wit - -
bitvector/byte_add_2_true-unreach-call.i timeout 900   870   810 wit - -
bitvector/gcd_1_true-unreach-call.i true 9.9 7.4 230 wit - -
bitvector/gcd_2_true-unreach-call.i true 11   7.6 250 wit - -
bitvector/gcd_3_true-unreach-call.i true 380   380   340 wit - -
bitvector/gcd_4_true-unreach-call.i true 3.7 1.7 210 wit - -
bitvector/interleave_bits_true-unreach-call.i true 8.2 3.9 400 wit - -
bitvector/jain_1_true-unreach-call.i true 3.9 1.8 220 wit - -
bitvector/jain_2_true-unreach-call.i true 4.0 1.9 220 wit - -
bitvector/jain_4_true-unreach-call.i true 4.2 2.0 220 wit - -
bitvector/jain_5_true-unreach-call.i timeout 900   860   4600 wit - -
bitvector/jain_6_true-unreach-call.i true 4.0 1.9 220 wit - -
bitvector/jain_7_true-unreach-call.i true 14   12   230 wit - -
bitvector/modulus_true-unreach-call.i timeout 900   900   480 wit - -
bitvector/num_conversion_1_true-unreach-call.i true 3.7 1.7 210 wit - -
bitvector/num_conversion_2_true-unreach-call.i timeout 900   850   1700 wit - -
bitvector/parity_true-unreach-call.i timeout 900   860   2000 wit - -
bitvector/sum02_true-unreach-call.i timeout 900   870   860 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c false(reach) 19   4.8 690 wit false(reach) 13   7.2 500 false(reach) 36 20   510
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c false(reach) 33   8.6 900 wit false(reach) 12   6.5 520 false(reach) 43 23   530
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c false(reach) 10   3.2 490 wit false(reach) 12   6.3 470 unknown 35 19   480
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c true 34   9.3 830 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 32   10   840 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 32   9.0 870 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c timeout 900   870   1200 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c timeout 900   840   1900 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c true 720   670   2000 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c true 700   640   1900 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c true 32   9.7 880 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c true 31   9.5 860 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c timeout 900   870   750 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c true 42   26   800 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c timeout 900   890   490 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c timeout 900   870   740 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c true 7.9 3.5 290 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i false(reach) 3.8 1.8 230 wit false(reach) 4.4 2.6 230 error 10 6.6 340
bitvector-regression/implicitunsignedconversion_false-unreach-call.i false(reach) 3.2 1.5 220 wit false(reach) 3.9 2.3 220 false(reach) 11 6.4 310
bitvector-regression/integerpromotion_false-unreach-call.i false(reach) 5.6 2.2 270 wit false(reach) 6.3 3.6 330 false(reach) 17 11   380
bitvector-regression/signextension2_false-unreach-call.i false(reach) 5.6 2.1 260 wit false(reach) 6.3 3.5 330 false(reach) 12 8.2 330
bitvector-regression/signextension_false-unreach-call.i false(reach) 4.7 1.8 260 wit false(reach) 6.9 3.9 340 false(reach) 11 6.5 320
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true 2.8 1.4 200 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true 4.2 1.8 220 wit - -
bitvector-regression/signextension2_true-unreach-call.i true 4.2 1.8 210 wit - -
bitvector-regression/signextension_true-unreach-call.i true 3.9 1.7 210 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) 5.1 2.2 250 wit false(reach) 5.8 3.4 250 false(reach) 13 6.9 330
bitvector-loops/overflow_false-unreach-call1.i timeout 900   850   4600 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i timeout 900   880   14000 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 16000 15000 52000 48 71   39   3200   48 190   110   3500  
    correct results 33 2200 1800 16000 9 71   39   3200   7 190   110   3500  
        correct true 24 2100 1800 13000 0 0   0   0   0 0   0   0  
        correct false 9 90 28 3600 9 71   39   3200   7 190   110   3500  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 84) 57
Run set sv-comp16.BitVectorsReach