Tool CPAchecker 1.6.1-svn 24048
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 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.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 false(unreach-call) 1 wit inspect 8.6 1.9  53 480 .020  0      false(unreach-call) 5.2  2.9  66 290 false(unreach-call) 39   21   560 560 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i segmentation fault 0 wit inspect 71   18    570 2800 0      .012  error (invalid witness file) .50 .33 13 39 error (invalid witness file) 5.6 3.1 120 300 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 14   2.9  87 590 .016  0      - - true 15    7.6  200   400 true 460   420   9700 1800
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 15   3.1  110 640 .016  .020  - - true 12    6.3  160   390 true 400   350   8800 1800
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.5 3.6  80 330 .0041 0      - - true 11    9.1  230   320 false(unreach-call) 9.8 5.3 130 330
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 240   120    1500 660 .0041 0      - - true 160    160    2800   470 false(unreach-call) 7.5 4.0 150 320
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 220   110    1500 630 .0041 0      - - true 160    150    3000   470 false(unreach-call) 9.0 4.8 74 320
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.9 1.0  25 270 .0041 0      - - true 8.0  5.5  130   320 timeout 960   940   18000 910
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.4 2.5  79 450 .012  .0041 - - true 8.2  4.8  89   350 true 160   130   1700 770
bitvector/jain_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 4.3 1.2  29 310 .012  0      - - out of memory 280    270    7100   7000 true 7.8 4.2 140 320
bitvector/jain_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 4.3 1.3  31 300 .012  0      - - out of memory 210    200    4500   7000 true 8.3 4.4 180 330
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.0 1.3  32 320 .012  .020  - - out of memory 200    200    4400   7000 true 7.5 4.1 160 320
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 910   300    8500 7500 0      0      - - out of memory 370    360    6200   7000 timeout 960   820   21000 3000
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect 4.6 1.3  36 300 .012  .76   - - out of memory 180    170    5000   7000 true 7.7 4.2 150 330
bitvector/jain_7_true-unreach-call_true-no-overflow.i true 2 wit inspect 8.8 3.0  73 400 .012  0      - - out of memory 280    280    7400   7000 true 7.5 4.1 150 320
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 21   5.4  160 1500 .012  0      - - true 17    15    270   340 unknown 30   27   510 330
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.9 1.0  25 270 .0041 0      - - true 6.1  3.4  65   280 true 61   48   1300 510
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.7 1.4  39 340 0      0      - - true 6.2  3.5  61   280 timeout 960   930   22000 980
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 25   9.5  210 650 .0082 0      - - true 29    23    500   380 false(unreach-call) 7.5 4.1 160 320
bitvector/sum02_true-unreach-call_true-no-overflow.i segmentation fault 0 wit inspect 140   40    1200 3800 0      .012  - - error (invalid witness file) .49 .31 11   39 error (invalid witness file) 6.2 3.3 120 300
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 47   9.6  290 1700 .35   0      false(unreach-call) 8.2  4.3  94 320 false(unreach-call) 29   15   390 570 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 70   17    490 3000 .82   0      false(unreach-call) 11    5.7  96 320 false(unreach-call) 36   19   290 600 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 25   4.6  160 920 .070  0      false(unreach-call) 8.0  4.2  140 310 false(unreach-call) 23   12   250 500 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 57   12    350 1800 0      .79   - - true 20    11    360   610 out of memory 300   250   5700 7000
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 1 wit inspect 36   6.8  240 1300 0      0      - - unknown 15    7.8  150   460 false(unreach-call) 15   7.7 200 370
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 1 wit inspect 28   5.4  180 970 0      0      - - unknown 14    7.2  190   440 false(unreach-call) 13   7.0 270 400
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   290    4600 3600 0      0      - - timeout 900    890    17000   1600 timeout 960   850   15000 6900
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 130   36    1100 3800 .053  1.6    - - timeout 910    900    21000   5100 true 54   29   880 1100
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c segmentation fault 0 wit inspect 39   7.5  250 1300 0      .012  - - error (invalid witness file) .61 .39 8.4 39 error (invalid witness file) 7.2 3.8 82 310
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 160   46    1400 4400 .053  0      - - timeout 900    890    19000   4300 true 58   30   590 1200
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 190   55    1600 4900 .053  0      - - timeout 910    890    17000   5200 true 47   25   900 1100
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 910   290    7100 5700 0      .77   - - timeout 910    890    18000   5600 true 470   420   5700 4600
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 87   40    750 2300 .66   .82   - - timeout 900    850    19000   6200 true 170   150   2600 880
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c true 1 wit inspect 13   3.6  100 610 .13   .0041 - - out of memory 800    730    19000   7000 false(unreach-call) 97   71   1800 960
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c segmentation fault 0 wit inspect 36   7.6  270 1100 .13   0      - - error (invalid witness file) .47 .31 6.6 40 error (invalid witness file) 7.4 3.9 87 290
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 380   180    3800 2500 .39   0      - - true 350    340    8700   790 false(unreach-call) 23   15   460 400
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c true 1 wit inspect 8.4 1.9  59 430 .066  0      - - out of memory 880    790    14000   7000 false(unreach-call) 98   72   2000 980
bitvector-regression/implicitfloatconversion_false-unreach-call.c false(unreach-call) 1 wit inspect 3.4 1.1  31 290 .0082 .020  false(unreach-call) 3.6  2.1  47 260 false(unreach-call) 10   5.7 160 310 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c false(unreach-call) 1 wit inspect 3.1 1.1  26 280 .0082 3.1    false(unreach-call) 3.9  2.2  40 260 false(unreach-call) 8.0 4.2 110 310 - -
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) 1 wit inspect 3.1 1.1  27 270 .0082 0      false(unreach-call) 3.9  2.2  45 270 false(unreach-call) 12   6.2 210 310 - -
bitvector-regression/recHanoi03_false-unreach-call.c error 0 wit inspect 3.1 1.1  22 290 0      0      error (recursion) 3.5  1.9  59 260 timeout 97   74   1400 1100 - -
bitvector-regression/signextension2_false-unreach-call.c false(unreach-call) 1 wit inspect 3.3 1.1  28 280 .0082 0      false(unreach-call) 3.8  2.2  36 260 false(unreach-call) 7.2 3.9 150 320 - -
bitvector-regression/signextension_false-unreach-call.c false(unreach-call) 1 wit inspect 3.3 1.1  26 270 .0082 0      false(unreach-call) 4.7  2.6  40 260 false(unreach-call) 7.5 4.0 140 320 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true 2 wit inspect 2.7 .95 21 270 .0041 0      - - true 3.6  2.0  43   260 true 7.7 4.1 150 310
bitvector-regression/integerpromotion_true-unreach-call.c true 2 wit inspect 2.7 .98 26 270 .0041 0      - - true 3.2  1.8  66   250 true 13   7.2 260 320
bitvector-regression/signextension2_true-unreach-call.c true 2 wit inspect 2.7 .97 23 260 .0041 0      - - true 4.3  2.4  43   260 true 8.2 4.3 170 330
bitvector-regression/signextension_true-unreach-call.c true 2 wit inspect 2.8 1.0  23 270 .0041 3.1    - - true 3.4  1.9  61   260 true 8.2 4.4 150 320
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 6.3 1.7  42 370 .0041 .020  false(unreach-call) 4.4  2.5  86 280 false(unreach-call) 8.6 4.6 160 350 - -
bitvector-loops/overflow_false-unreach-call1.i timeout 0 wit inspect 910   300    7500 7100 0      0      timeout 92    85    1900 1700 timeout 97   67   1100 1200 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(unreach-call) 1 wit inspect 13   3.1  91 500 .31   0      true 5.5  3.1  98 300 false(unreach-call) 7.4 4.0 140 310 - -
../../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 67 5800 2000 45000 73000 3.3  11      50 160 120 2700 5100   50 390 240 5200 7100   50 9500 9100 200000 91000   50 6400 5700 120000 41000  
    correct results 37 63 1800 680 14000 37000 3.0  10      11 62 34 790 3100   11 190 100 2500 4500   17 5600 5400 120000 62000   22 3800 3400 75000 23000  
        correct true 26 52 1600 640 13000 29000 1.4  7.0    1 0 0 0 0   0 0 0 0 0   17 5600 5400 120000 62000   17 3800 3400 75000 23000  
        correct false 11 11 190 43 1300 8300 1.6  3.1    10 62 34 790 3100   11 190 100 2500 4500   0 0 0 0 0   5 0 0 0 0  
    correct-unconfimed results 4 4 86 18 580 3300 .20 .0041 0 0 0 0 0   0 0 0 0 0   0 1700 1500 34000 15000   4 220 160 4300 2700  
        correct-unconfirmed true 4 4 86 18 580 3300 .20 .0041 0 0 0 0 0   0 0 0 0 0   0 1700 1500 34000 15000   0 220 160 4300 2700  
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (50 tasks, max score: 86) 67
Run set sv-comp17.ReachSafety-BitVectors