Tool CPAchecker 1.6.1-svn 23987
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS [Linux 4.4.0-57-generic; Linux 4.4.0-59-generic]
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-10 20:44:08 CET [[ 2017-01-14 18:01:01 CET ]] [[ 2017-01-14 20:09:29 CET ]] [[ 2017-01-14 18:26:00 CET ]] [[ 2017-01-14 20:41:28 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
bitvector/byte_add_false-unreach-call_true-no-overflow.i 0 13   3.6 95 530 .016  0      .57 .37 8.2 40 6.1 3.2 100 300
bitvector/sum02_false-unreach-call_true-no-overflow.i 0 3.5 1.5 30 300 .0041 0      .51 .32 10   40 5.7 3.0 110 290
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 0 10   3.2 82 470 .020  0      .64 .40 8.6 39 5.9 3.1 110 290
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 0 15   4.1 100 540 .020  .0082 .59 .39 8.0 39 6.7 3.5 130 300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 0 8.3 6.1 95 310 .0041 0      .54 .36 10   39 6.4 3.4 100 300
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 3.6 1.4 31 290 0      0      130    130    2400   470 960   950   26000 600
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 0 4.8 3.0 50 300 .0041 0      .61 .40 8.2 40 5.7 3.0 120 290
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 2 2.9 1.3 30 270 0      0      7.5  5.0  93   320 960   940   18000 880
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 0 5.6 2.2 47 350 .012  0      .68 .44 9.1 42 7.0 3.7 120 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i 2 2.9 1.3 27 270 0      0      310    300    5000   7000 7.3 3.9 110 330
bitvector/jain_2_true-unreach-call_true-no-overflow.i 2 2.8 1.3 27 270 0      0      270    260    4900   7000 7.4 4.0 140 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i 2 2.9 1.3 29 270 0      0      260    260    5300   7000 8.6 4.6 180 320
bitvector/jain_5_true-unreach-call_true-no-overflow.i 0 900   860   12000 3900 0      0      .64 .40 7.9 40 6.5 3.4 80 290
bitvector/jain_6_true-unreach-call_true-no-overflow.i 2 2.9 1.3 25 270 0      .0082 220    220    6300   7000 7.1 3.9 140 310
bitvector/jain_7_true-unreach-call_true-no-overflow.i 2 3.0 1.3 28 270 0      0      260    250    6700   7000 7.8 4.1 150 320
bitvector/modulus_true-unreach-call_true-no-overflow.i 0 21   19   240 310 .0041 0      .62 .39 11   43 6.0 3.2 120 300
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 2 3.2 1.3 31 290 0      0      6.2  3.4  56   280 60   47   700 500
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 0 14   9.9 130 490 .0082 0      .52 .33 9.1 39 5.9 3.1 110 300
bitvector/parity_true-unreach-call_true-no-overflow.i 0 3.0 1.3 29 280 .0041 0      .67 .42 8.4 41 5.7 3.1 110 310
bitvector/sum02_true-unreach-call_true-no-overflow.i 0 3.3 1.4 32 300 .0041 0      .62 .40 8.3 39 6.1 3.2 120 290
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 0 18   4.8 140 740 .041  .0082 10    5.4  110   430 13   7.0 190 520
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 1 23   6.3 170 1000 .049  .029  10    5.4  190   430 29   15   360 560
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 1 8.8 2.6 64 460 .037  0      11    6.0  120   420 29   15   470 510
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 18   4.7 130 740 .041  0      .65 .41 8.6 42 5.7 3.0 110 290
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 2 39   9.9 260 1600 0      0      21    12    310   630 60   33   710 1000
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 2 21   5.5 160 890 0      0      20    12    240   560 35   19   580 920
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900   700   11000 6400 0      0      .52 .33 9.0 41 6.1 3.3 78 300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 2 56   15   340 2300 0      2.3    910    890    20000   4600 48   26   680 1100
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 2 26   6.9 180 970 0      0      900    890    14000   4100 39   21   400 1200
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c 2 25   6.5 200 970 0      0      910    890    25000   4200 49   26   840 1100
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 2 46   12   350 2200 0      0      910    890    17000   5300 60   32   610 1100
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 2 40   12   320 2200 0      0      910    900    14000   5000 49   26   600 1000
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c 0 4.1 1.6 36 300 .016  0      .72 .46 8.5 41 5.4 2.9 100 300
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c 0 13   3.9 96 500 .037  0      .50 .31 9.2 40 6.2 3.3 120 300
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c 0 7.7 2.5 59 450 .033  0      .56 .36 12   43 6.8 3.6 110 290
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c 0 3.5 1.5 35 290 .012  0      .58 .37 8.9 39 6.0 3.2 120 300
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c 0 22   5.8 170 720 .037  0      .60 .38 11   40 7.2 3.7 110 310
bitvector-regression/implicitfloatconversion_false-unreach-call.c 1 3.1 1.3 28 280 .0041 .025  3.5  1.9  45   270 11   6.2 210 290
bitvector-regression/implicitunsignedconversion_false-unreach-call.c -32 2.6 1.1 22 270 0      0      3.9  2.2  46   260 6.3 3.4 140 300
bitvector-regression/integerpromotion_false-unreach-call.c 1 2.8 1.2 24 270 .0041 0      3.6  2.0  61   270 13   6.7 240 340
bitvector-regression/recHanoi03_false-unreach-call.c 0 3.0 1.3 26 280 .0041 0      .51 .34 6.9 42 5.7 3.0 120 290
bitvector-regression/signextension2_false-unreach-call.c -32 2.6 1.1 22 270 0      0      4.0  2.3  73   260 7.5 4.0 140 310
bitvector-regression/signextension_false-unreach-call.c -32 2.5 1.2 21 270 0      0      3.8  2.2  86   260 7.2 3.8 140 320
bitvector-regression/implicitunsignedconversion_true-unreach-call.c 2 2.6 1.1 25 260 0      0      3.3  1.9  64   260 7.3 3.9 140 320
bitvector-regression/integerpromotion_true-unreach-call.c 2 2.6 1.1 20 270 0      0      4.1  2.3  49   260 13   7.1 230 310
bitvector-regression/signextension2_true-unreach-call.c 2 2.6 1.2 26 270 0      0      4.3  2.4  43   250 7.4 4.0 120 310
bitvector-regression/signextension_true-unreach-call.c 2 2.7 1.2 21 260 0      0      3.5  2.0  68   250 7.8 4.2 130 310
bitvector-loops/diamond_false-unreach-call2.i -32 13   3.7 110 580 0      0      5.7  3.2  110   290 11   6.1 160 380
bitvector-loops/overflow_false-unreach-call1.i -32 3.0 1.3 28 270 0      .0041 92    87    1700   2500 97   67   1600 1300
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i -32 3.2 1.4 29 290 0      0      4.5  2.5  50   280 97   86   2000 680
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 50 -150 2300 1700   28000 37000 .42  2.4    50 150 120   2600 5800   50 340 230   6000 6300   50 6100 5900 120000 62000   50 2500 2200 53000 17000  
    correct results 23 42 330 94   2400 17000 .094 2.3    4 28 15   410 1400   4 82 43   1300 1700   9 6100 5900 120000 62000   17 2400 2200 51000 12000  
        correct true 19 38 290 82   2100 14000 0     2.3    2 0 0   0 0   0 0 0   0 0   9 6100 5900 120000 62000   17 2400 2200 51000 12000  
        correct false 4 4 38 11   290 2000 .094 .053  2 28 15   410 1400   4 82 43   1300 1700   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 1 0 18 4.8 140 740 .041 .0082 1 10 5.4 110 430   1 13 7.0 190 520   0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 1 0 18 4.8 140 740 .041 .0082 0 10 5.4 110 430   0 13 7.0 190 520   0 0 0 0 0   0 0 0 0 0  
    incorrect results 6 -192 27 9.7 230 1900 0     .0041 4 110 99   2100 3900   4 230 170   4200 3200   0 0 0 0 0   0 0 0 0 0  
        incorrect true 6 -192 27 9.7 230 1900 0     .0041 1 110 99   2100 3900   0 230 170   4200 3200   0 0 0 0 0   0 0 0 0 0  
        incorrect false 0
score (50 tasks, max score: 86) -150
Run set sv-comp17.ReachSafety-BitVectors