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 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]]
Run set sv-comp16.BitVectorsReach
Options -sv-comp16 -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-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.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 87   57   3700 8.9 4.9 380 70   41   540
bitvector/byte_add_1_true-unreach-call.i 38   17   1500
bitvector/byte_add_2_true-unreach-call.i 92   60   3800
bitvector/gcd_1_true-unreach-call.i 21   4.7 790
bitvector/gcd_2_true-unreach-call.i 270   110   3000
bitvector/gcd_3_true-unreach-call.i 280   120   2800
bitvector/gcd_4_true-unreach-call.i 2.9 1.3 180
bitvector/interleave_bits_true-unreach-call.i 22   5.2 700
bitvector/jain_1_true-unreach-call.i 310   130   6200
bitvector/jain_2_true-unreach-call.i 310   130   6000
bitvector/jain_4_true-unreach-call.i 310   140   7000
bitvector/jain_5_true-unreach-call.i 900   710   5500
bitvector/jain_6_true-unreach-call.i 310   130   7000
bitvector/jain_7_true-unreach-call.i 310   130   5500
bitvector/modulus_true-unreach-call.i 46   19   3700
bitvector/num_conversion_1_true-unreach-call.i 3.3 1.5 190
bitvector/num_conversion_2_true-unreach-call.i 13   3.8 660
bitvector/parity_true-unreach-call.i 67   15   1000
bitvector/sum02_true-unreach-call.i 900   710   4900
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c 13   3.9 660 13   6.8 490 38   23   530
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c 17   5.7 710 14   7.5 480 41   23   550
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c 9.9 2.9 390 13   6.7 460 34   22   500
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c 28   18   1200
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c 27   17   1300
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c 30   19   1500
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c 900   700   3900
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c 38   24   2400
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c 100   82   3700
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c 100   82   3600
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c 35   23   2300
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c 34   23   2300
bitvector/soft_float_1_true-unreach-call.c.cil.c 320   130   4300
bitvector/soft_float_2_true-unreach-call.c.cil.c 21   5.2 610
bitvector/soft_float_3_true-unreach-call.c.cil.c 900   690   7600
bitvector/soft_float_4_true-unreach-call.c.cil.c 510   330   4100
bitvector/soft_float_5_true-unreach-call.c.cil.c 24   5.6 680
bitvector-regression/implicitfloatconversion_false-unreach-call.i 3.6 1.6 200 4.3 2.5 220 9.5 5.4 320
bitvector-regression/implicitunsignedconversion_false-unreach-call.i 3.0 1.4 200 4.6 2.8 220 11   6.1 320
bitvector-regression/integerpromotion_false-unreach-call.i 5.1 2.0 240 6.9 3.9 340 20   14   370
bitvector-regression/signextension2_false-unreach-call.i 4.9 2.0 230 7.4 4.1 330 11   6.5 330
bitvector-regression/signextension_false-unreach-call.i 4.3 1.7 240 7.2 4.0 340 11   9.0 330
bitvector-regression/implicitunsignedconversion_true-unreach-call.i 3.0 1.4 180
bitvector-regression/integerpromotion_true-unreach-call.i 4.0 1.7 190
bitvector-regression/signextension2_true-unreach-call.i 3.2 1.4 190
bitvector-regression/signextension_true-unreach-call.i 3.7 1.7 190
bitvector-loops/diamond_false-unreach-call2.i 4.4 1.7 230 5.8 3.4 250 14   7.7 340
bitvector-loops/overflow_false-unreach-call1.i 900   700   4900
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 26   8.7 1100 9.1 5.1 420 91   84   400
../../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 8400 5400 110000 48 94   52   3900   48 350   240   4500  
    correct results 43 3900 1900 87000 11 94   52   3900   8 350   240   4500  
        correct true 32 3700 1800 79000 0 0   0   0   0 0   0   0  
        correct false 11 180 89 7900 11 94   52   3900   8 350   240   4500  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 84) 75
Run set sv-comp16.BitVectorsReach