Tool CPAchecker 1.4-svcomp16c
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 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]]
Run set sv-comp16.BitVectorsReach
Options -sv-comp16--k-induction -disable-java-assertions -heap 10000m -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-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.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) 16   3.6 590 wit false(reach) 8.6 4.8 380 error 31   19   500
bitvector/byte_add_1_true-unreach-call.i true 23   4.6 640 wit - -
bitvector/byte_add_2_true-unreach-call.i true 22   4.5 540 wit - -
bitvector/gcd_1_true-unreach-call.i true 19   4.3 730 wit - -
bitvector/gcd_2_true-unreach-call.i true 300   130   3800 wit - -
bitvector/gcd_3_true-unreach-call.i true 270   110   3700 wit - -
bitvector/gcd_4_true-unreach-call.i true 6.7 2.1 340 wit - -
bitvector/interleave_bits_true-unreach-call.i true 18   4.1 570 wit - -
bitvector/jain_1_true-unreach-call.i timeout 900   420   11000 wit - -
bitvector/jain_2_true-unreach-call.i timeout 900   420   13000 wit - -
bitvector/jain_4_true-unreach-call.i timeout 900   420   14000 wit - -
bitvector/jain_5_true-unreach-call.i timeout 900   440   7900 wit - -
bitvector/jain_6_true-unreach-call.i timeout 900   420   13000 wit - -
bitvector/jain_7_true-unreach-call.i timeout 900   420   10000 wit - -
bitvector/modulus_true-unreach-call.i true 45   18   3700 wit - -
bitvector/num_conversion_1_true-unreach-call.i true 6.2 2.2 280 wit - -
bitvector/num_conversion_2_true-unreach-call.i true 6.4 2.3 290 wit - -
bitvector/parity_true-unreach-call.i true 74   16   1300 wit - -
bitvector/sum02_true-unreach-call.i timeout 900   440   5900 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c false(reach) 44   10   1100 wit false(reach) 12   6.7 500 false(reach) 42   23   550
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c false(reach) 53   14   1400 wit false(reach) 13   7.1 490 false(reach) 42   23   540
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c false(reach) 31   6.4 900 wit false(reach) 14   7.6 500 unknown 39   22   520
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c true 48   11   1100 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 41   8.1 1000 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 35   7.0 930 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c timeout 900   430   4800 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c true 35   6.3 890 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c true 190   75   3400 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c true 200   78   4100 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c timeout 900   420   5900 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c timeout 900   420   5900 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c timeout 900   410   5200 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c true 21   4.5 540 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c timeout 900   380   7100 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c true 760   350   4200 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c true 22   4.5 540 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i false(reach) 4.1 1.8 230 wit false(reach) 4.4 2.5 230 error 9.8 5.7 310
bitvector-regression/implicitunsignedconversion_false-unreach-call.i false(reach) 4.0 1.9 230 wit false(reach) 4.3 2.6 220 false(reach) 11   6.3 330
bitvector-regression/integerpromotion_false-unreach-call.i false(reach) 5.2 2.2 240 wit false(reach) 7.2 4.0 330 false(reach) 20   11   360
bitvector-regression/signextension2_false-unreach-call.i false(reach) 5.1 2.2 240 wit false(reach) 7.4 4.1 340 false(reach) 12   6.8 340
bitvector-regression/signextension_false-unreach-call.i false(reach) 5.1 2.2 240 wit false(reach) 7.6 4.2 330 false(reach) 12   7.1 330
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true 3.5 1.6 200 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true 4.4 1.8 210 wit - -
bitvector-regression/signextension2_true-unreach-call.i true 4.3 1.8 200 wit - -
bitvector-regression/signextension_true-unreach-call.i true 3.7 1.5 200 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) 6.7 2.3 380 wit false(reach) 5.6 3.2 240 false(reach) 12   7.7 330
bitvector-loops/overflow_false-unreach-call1.i timeout 900   440   8300 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(reach) 23   7.9 1400 wit false(reach) 8.4 4.7 410 timeout 91   83   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 14000 6400 150000 48 93   51   4000   48 320   210   4500  
    correct results 35 2400 910 40000 11 93   51   4000   7 320   210   4500  
        correct true 24 2200 850 33000 0 0   0   0   0 0   0   0  
        correct false 11 200 54 7000 11 93   51   4000   7 320   210   4500  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 84) 59
Run set sv-comp16.BitVectorsReach