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-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-11 11:18:39 CET [[ 2017-01-14 21:32:33 CET ]] [[ 2017-01-14 22:21:46 CET ]] [[ 2017-01-14 21:35:07 CET ]] [[ 2017-01-14 22:35:09 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.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 1 76   65    1000 1700 .041  0   5.8 3.2 100 290 52   29   560 560
bitvector/sum02_false-unreach-call_true-no-overflow.i 0 900   530    7600 4000 .0082 0   92   85   2100 1100 24   20   410 340
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 2 70   60    770 1700 .016  0   9.0 4.9 180 340 380   340   4400 1400
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 2 25   16    260 920 .037  0   11   5.7 130 350 400   350   8100 1400
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 2 6.5 4.7  87 280 .0082 0   10   8.3 190 310 960   950   14000 560
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 7.1 5.2  77 280 .0082 0   140   140   2700 470 960   950   13000 590
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 2 150   150    2000 310 .0082 0   110   100   3500 470 960   950   20000 570
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 2 2.3 .97 20 240 0      0   8.3 5.6 120 320 960   940   16000 910
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2 6.9 2.8  58 400 .025  0   7.4 4.7 140 330 90   71   1500 670
bitvector/jain_1_true-unreach-call_true-no-overflow.i 2 2.8 1.2  28 270 .0082 0   270   260   6900 7000 7.9 4.3 99 320
bitvector/jain_2_true-unreach-call_true-no-overflow.i 2 2.7 1.2  26 260 .0082 0   250   240   3200 7000 7.5 4.0 110 320
bitvector/jain_4_true-unreach-call_true-no-overflow.i 2 2.8 1.2  25 270 .0082 0   200   190   4200 7000 7.4 4.0 130 310
bitvector/jain_5_true-unreach-call_true-no-overflow.i 0 900   610    8900 7200 0      0   350   340   7600 7000 960   820   19000 3000
bitvector/jain_6_true-unreach-call_true-no-overflow.i 2 2.9 1.2  24 270 .0082 0   200   190   5100 7000 7.7 4.1 150 330
bitvector/jain_7_true-unreach-call_true-no-overflow.i 2 4.4 2.8  48 270 .0082 0   260   260   7900 7000 8.1 4.3 170 320
bitvector/modulus_true-unreach-call_true-no-overflow.i 2 230   210    3100 1700 .020  0   16   14   380 350 43   35   450 530
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 2 2.3 .98 20 240 0      0   5.3 3.0 77 280 59   47   560 510
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 2 17   11    160 540 .016  0   5.8 3.3 74 280 960   920   19000 900
bitvector/parity_true-unreach-call_true-no-overflow.i 2 120   110    1600 730 .0082 0   29   23   430 370 960   950   19000 950
bitvector/sum02_true-unreach-call_true-no-overflow.i 0 900   530    9800 6300 .0082 0   910   900   15000 6100 960   950   21000 540
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 1 8.3 2.5  62 440 .037  0   7.6 4.0 150 300 29   15   270 500
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 1 11   3.8  100 510 .045  0   7.2 3.9 110 300 36   18   380 560
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 1 6.7 2.0  53 330 .033  0   7.1 3.8 140 310 27   14   280 460
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 2 21   14    220 1600 0      0   66   56   1100 970 43   24   610 760
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 2 19   13    210 1500 0      0   19   11   280 580 50   27   670 910
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 2 22   15    210 2100 0      0   18   10   280 560 35   18   470 890
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 910   550    11000 4200 .16   0   900   890   21000 1800 960   900   12000 4300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 2 27   19    270 2300 0      0   910   900   19000 5000 61   33   910 1100
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 2 94   84    1200 2300 0      0   900   890   18000 4200 41   22   600 1200
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c 2 93   84    1100 2300 0      0   900   890   18000 4200 42   23   670 1100
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 2 25   19    250 2300 0      0   910   900   20000 5400 45   24   540 1100
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 2 26   19    270 2300 0      0   910   900   18000 5400 44   24   560 1100
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c 1 11   5.9  110 390 .025  0   910   860   15000 6100 85   68   1400 690
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c 2 110   100    1500 1300 .070  0   880   820   16000 7000 77   64   1400 820
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c 1 100   87    1500 1300 .070  0   840   770   21000 7000 960   930   15000 1800
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c 2 200   200    2500 370 .025  0   390   380   7600 790 56   37   970 610
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c 2 110   98    1200 1300 .070  0   770   700   19000 7000 19   11   280 560
bitvector-regression/implicitfloatconversion_false-unreach-call.c 1 2.3 1.0  21 250 .0041 0   3.9 2.2 45 270 13   6.9 160 300
bitvector-regression/implicitunsignedconversion_false-unreach-call.c 1 2.5 1.0  20 270 .0041 0   3.3 1.9 33 270 8.6 4.6 100 320
bitvector-regression/integerpromotion_false-unreach-call.c 1 2.5 1.0  21 260 .0041 0   3.5 2.0 73 270 15   7.8 140 310
bitvector-regression/recHanoi03_false-unreach-call.c 0 3.2 1.3  25 300 0      0   3.4 1.9 59 260 97   73   1400 1100
bitvector-regression/signextension2_false-unreach-call.c 1 2.5 1.1  25 240 .0041 0   3.8 2.1 61 270 7.8 4.1 74 320
bitvector-regression/signextension_false-unreach-call.c 1 2.4 1.0  20 250 .0041 0   3.9 2.2 66 270 8.1 4.3 110 310
bitvector-regression/implicitunsignedconversion_true-unreach-call.c 2 2.1 .92 19 220 0      0   3.4 1.9 70 250 7.3 3.8 100 320
bitvector-regression/integerpromotion_true-unreach-call.c 2 2.3 .95 20 250 0      0   3.7 2.1 57 260 14   7.3 210 320
bitvector-regression/signextension2_true-unreach-call.c 2 2.2 .95 19 240 0      0   3.9 2.1 65 260 8.2 4.3 120 320
bitvector-regression/signextension_true-unreach-call.c 2 2.2 .96 19 240 0      0   3.3 1.9 70 260 9.6 5.1 100 320
bitvector-loops/diamond_false-unreach-call2.i 1 3.0 1.2  26 260 .0082 0   4.7 2.6 47 280 10   5.5 120 340
bitvector-loops/overflow_false-unreach-call1.i 0 910   610    9700 7800 0      0   94   84   1600 1700 97   68   1300 1100
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 1 210   200    2500 890 .27   0   6.1 3.3 130 310 98   59   1100 6100
../../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 75 6400   4500   69000 66000 1.1   0   50 250   200   4800 6200   50 520 330 6400 13000   50 12000 12000 250000 110000   50 11000 11000 190000 32000  
    correct results 42 73 1700   1500   21000 35000 .81  0   11 57   31   950 3200   10 300 170 3300 10000   19 8200 7900 170000 81000   24 7300 6900 130000 22000  
        correct true 31 62 1400   1200   17000 29000 .35  0   0 0   0   0 0   0 0 0 0 0   19 8200 7900 170000 81000   24 7300 6900 130000 22000  
        correct false 11 11 330   280   3900 5400 .46  0   11 57   31   950 3200   10 300 170 3300 10000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 3 2 120   95   1600 2000 .094 0   0 3.4 1.9 59 260   0 97 73 1400 1100   0 1800 1600 37000 13000   0 1000 990 17000 2500  
        correct-unconfirmed true 2 2 110   93   1600 1700 .094 0   0 0   0   0 0   0 0 0 0 0   0 1800 1600 37000 13000   0 1000 990 17000 2500  
        correct-unconfirmed false 1 0 3.2 1.3 25 300 0     0   0 3.4 1.9 59 260   0 97 73 1400 1100   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (50 tasks, max score: 86) 75
Run set sv-comp17.ReachSafety-BitVectors