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 error 0 wit inspect 13   3.6 95 530 .016  0      error (invalid witness file) .57 .37 8.2 40 error (invalid witness file) 6.1 3.2 100 300 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i error 0 wit inspect 3.5 1.5 30 300 .0041 0      error (invalid witness file) .51 .32 10   40 error (invalid witness file) 5.7 3.0 110 290 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i error 0 wit inspect 10   3.2 82 470 .020  0      - - error (invalid witness file) .64 .40 8.6 39 error (invalid witness file) 5.9 3.1 110 290
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i error 0 wit inspect 15   4.1 100 540 .020  .0082 - - error (invalid witness file) .59 .39 8.0 39 error (invalid witness file) 6.7 3.5 130 300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i error 0 wit inspect 8.3 6.1 95 310 .0041 0      - - error (invalid witness file) .54 .36 10   39 error (invalid witness file) 6.4 3.4 100 300
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.6 1.4 31 290 0      0      - - true 130    130    2400   470 timeout 960   950   26000 600
bitvector/gcd_3_true-unreach-call_true-no-overflow.i error 0 wit inspect 4.8 3.0 50 300 .0041 0      - - error (invalid witness file) .61 .40 8.2 40 error (invalid witness file) 5.7 3.0 120 290
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.9 1.3 30 270 0      0      - - true 7.5  5.0  93   320 timeout 960   940   18000 880
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i error 0 wit inspect 5.6 2.2 47 350 .012  0      - - error (invalid witness file) .68 .44 9.1 42 error (invalid witness file) 7.0 3.7 120 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.9 1.3 27 270 0      0      - - out of memory 310    300    5000   7000 true 7.3 3.9 110 330
bitvector/jain_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.8 1.3 27 270 0      0      - - out of memory 270    260    4900   7000 true 7.4 4.0 140 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.9 1.3 29 270 0      0      - - out of memory 260    260    5300   7000 true 8.6 4.6 180 320
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   860   12000 3900 0      0      - - error (invalid witness file) .64 .40 7.9 40 error (invalid witness file) 6.5 3.4 80 290
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.9 1.3 25 270 0      .0082 - - out of memory 220    220    6300   7000 true 7.1 3.9 140 310
bitvector/jain_7_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.0 1.3 28 270 0      0      - - out of memory 260    250    6700   7000 true 7.8 4.1 150 320
bitvector/modulus_true-unreach-call_true-no-overflow.i error 0 wit inspect 21   19   240 310 .0041 0      - - error (invalid witness file) .62 .39 11   43 error (invalid witness file) 6.0 3.2 120 300
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.2 1.3 31 290 0      0      - - true 6.2  3.4  56   280 true 60   47   700 500
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i error 0 wit inspect 14   9.9 130 490 .0082 0      - - error (invalid witness file) .52 .33 9.1 39 error (invalid witness file) 5.9 3.1 110 300
bitvector/parity_true-unreach-call_true-no-overflow.i error 0 wit inspect 3.0 1.3 29 280 .0041 0      - - error (invalid witness file) .67 .42 8.4 41 error (invalid witness file) 5.7 3.1 110 310
bitvector/sum02_true-unreach-call_true-no-overflow.i error 0 wit inspect 3.3 1.4 32 300 .0041 0      - - error (invalid witness file) .62 .40 8.3 39 error (invalid witness file) 6.1 3.2 120 290
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 0 wit inspect 18   4.8 140 740 .041  .0082 true 10    5.4  110   430 true 13   7.0 190 520 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 23   6.3 170 1000 .049  .029  true 10    5.4  190   430 false(unreach-call) 29   15   360 560 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 8.8 2.6 64 460 .037  0      true 11    6.0  120   420 false(unreach-call) 29   15   470 510 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c error 0 wit inspect 18   4.7 130 740 .041  0      - - error (invalid witness file) .65 .41 8.6 42 error (invalid witness file) 5.7 3.0 110 290
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 39   9.9 260 1600 0      0      - - true 21    12    310   630 true 60   33   710 1000
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 21   5.5 160 890 0      0      - - true 20    12    240   560 true 35   19   580 920
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   700   11000 6400 0      0      - - error (invalid witness file) .52 .33 9.0 41 error (invalid witness file) 6.1 3.3 78 300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 56   15   340 2300 0      2.3    - - timeout 910    890    20000   4600 true 48   26   680 1100
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 26   6.9 180 970 0      0      - - timeout 900    890    14000   4100 true 39   21   400 1200
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 25   6.5 200 970 0      0      - - timeout 910    890    25000   4200 true 49   26   840 1100
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 46   12   350 2200 0      0      - - timeout 910    890    17000   5300 true 60   32   610 1100
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 40   12   320 2200 0      0      - - timeout 910    900    14000   5000 true 49   26   600 1000
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c error 0 wit inspect 4.1 1.6 36 300 .016  0      - - error (invalid witness file) .72 .46 8.5 41 error (invalid witness file) 5.4 2.9 100 300
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c error 0 wit inspect 13   3.9 96 500 .037  0      - - error (invalid witness file) .50 .31 9.2 40 error (invalid witness file) 6.2 3.3 120 300
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c error 0 wit inspect 7.7 2.5 59 450 .033  0      - - error (invalid witness file) .56 .36 12   43 error (invalid witness file) 6.8 3.6 110 290
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c error 0 wit inspect 3.5 1.5 35 290 .012  0      - - error (invalid witness file) .58 .37 8.9 39 error (invalid witness file) 6.0 3.2 120 300
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c error 0 wit inspect 22   5.8 170 720 .037  0      - - error (invalid witness file) .60 .38 11   40 error (invalid witness file) 7.2 3.7 110 310
bitvector-regression/implicitfloatconversion_false-unreach-call.c false(unreach-call) 1 wit inspect 3.1 1.3 28 280 .0041 .025  false(unreach-call) 3.5  1.9  45   270 false(unreach-call) 11   6.2 210 290 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c true -32 wit inspect 2.6 1.1 22 270 0      0      false(unreach-call) 3.9  2.2  46   260 false(unreach-call) 6.3 3.4 140 300 - -
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) 1 wit inspect 2.8 1.2 24 270 .0041 0      false(unreach-call) 3.6  2.0  61   270 false(unreach-call) 13   6.7 240 340 - -
bitvector-regression/recHanoi03_false-unreach-call.c error 0 wit inspect 3.0 1.3 26 280 .0041 0      error (invalid witness file) .51 .34 6.9 42 error (invalid witness file) 5.7 3.0 120 290 - -
bitvector-regression/signextension2_false-unreach-call.c true -32 wit inspect 2.6 1.1 22 270 0      0      false(unreach-call) 4.0  2.3  73   260 false(unreach-call) 7.5 4.0 140 310 - -
bitvector-regression/signextension_false-unreach-call.c true -32 wit inspect 2.5 1.2 21 270 0      0      false(unreach-call) 3.8  2.2  86   260 false(unreach-call) 7.2 3.8 140 320 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true 2 wit inspect 2.6 1.1 25 260 0      0      - - true 3.3  1.9  64   260 true 7.3 3.9 140 320
bitvector-regression/integerpromotion_true-unreach-call.c true 2 wit inspect 2.6 1.1 20 270 0      0      - - true 4.1  2.3  49   260 true 13   7.1 230 310
bitvector-regression/signextension2_true-unreach-call.c true 2 wit inspect 2.6 1.2 26 270 0      0      - - true 4.3  2.4  43   250 true 7.4 4.0 120 310
bitvector-regression/signextension_true-unreach-call.c true 2 wit inspect 2.7 1.2 21 260 0      0      - - true 3.5  2.0  68   250 true 7.8 4.2 130 310
bitvector-loops/diamond_false-unreach-call2.i true -32 wit inspect 13   3.7 110 580 0      0      unknown 5.7  3.2  110   290 false(unreach-call) 11   6.1 160 380 - -
bitvector-loops/overflow_false-unreach-call1.i true -32 wit inspect 3.0 1.3 28 270 0      .0041 timeout 92    87    1700   2500 timeout 97   67   1600 1300 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i true -32 wit inspect 3.2 1.4 29 290 0      0      true 4.5  2.5  50   280 timeout 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