Tool SMACK+Corral 1.7.2
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-13 11:09:55 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 02:12:47 CET ]] [[ 2017-01-15 01:38:53 CET ]] [[ 2017-01-15 02:35:07 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.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 4.7 4.6 59 130 1.0  0      5.3  2.9  110 290 32   18   500 480
bitvector/sum02_false-unreach-call_true-no-overflow.i 0 880   880   11000 450 .86 2.4    .59 .38 11 44 5.8 3.1 77 320
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 2 12   12   130 150 1.1  0      9.0  4.9  170   340 500   450   9000 1200
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 2 15   15   180 150 1.1  0      9.2  5.0  180   340 520   460   13000 1300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 2 1.7 1.8 20 77 .87 0      10    8.4  260   310 960   950   25000 540
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 860   860   13000 300 .87 0      120    110    2700   470 960   940   22000 730
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 0 880   930   11000 190 .87 0      .56 .37 9.7 40 8.3 4.4 75 310
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 2 1.5 1.6 18 70 .86 0      7.5  5.2  130   310 960   940   29000 910
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2 1.3 1.3 18 68 .97 0      7.2  4.5  160   340 110   87   1800 680
bitvector/jain_1_true-unreach-call_true-no-overflow.i 2 890   880   11000 240 .84 0      310    300    5000   7000 10   5.3 110 340
bitvector/jain_2_true-unreach-call_true-no-overflow.i 2 890   880   8500 250 .84 0      220    210    3800   7000 9.0 4.8 120 330
bitvector/jain_4_true-unreach-call_true-no-overflow.i 2 880   880   9300 260 .84 0      220    210    4200   7000 9.3 4.9 82 330
bitvector/jain_5_true-unreach-call_true-no-overflow.i 1 880   880   8900 200 .83 0      340    330    7400   7000 960   820   18000 3100
bitvector/jain_6_true-unreach-call_true-no-overflow.i 2 880   880   7900 270 .85 0      180    180    5100   7000 11   6.0 120 350
bitvector/jain_7_true-unreach-call_true-no-overflow.i 2 890   880   8700 290 .85 0      300    290    6600   7000 7.8 4.2 100 320
bitvector/modulus_true-unreach-call_true-no-overflow.i 2 340   340   2200 260 .87 0      15    13    300   340 32   28   610 340
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 2 1.2 1.3 16 68 .87 0      5.7  3.2  65   280 60   48   1600 500
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 2 1.3 1.3 16 65 .92 0      5.6  3.1  81   280 960   920   18000 950
bitvector/parity_true-unreach-call_true-no-overflow.i 2 880   880   12000 280 .86 .21   24    20    460   350 960   950   21000 930
bitvector/sum02_true-unreach-call_true-no-overflow.i 1 880   880   11000 330 .86 0      910    900    19000   6400 960   950   24000 510
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 1 16   16   170 220 1.2  0      7.4  4.0  130 310 8.4 4.5 110 320
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 1 38   37   420 240 1.2  0      9.0  4.8  110 320 9.1 4.9 90 340
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 1 9.1 8.8 100 190 1.2  0      6.7  3.6  140 290 7.8 4.2 67 310
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 2 150   150   1400 380 1.2  0      72    61    1200   970 45   24   930 740
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 2 120   110   1000 340 1.2  0      20    12    270   590 61   33   920 1100
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 2 130   130   1200 360 1.2  0      15    8.5  340   540 39   21   560 840
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 1 880   880   6900 580 1.3  0      900    900    18000   1400 960   930   29000 1400
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 2 880   880   6100 630 1.3  0      910    900    15000   4700 59   31   1200 1100
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 2 880   880   6400 540 1.3  0      910    900    15000   4200 43   23   930 1100
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c 2 880   880   6800 640 1.3  0      900    890    22000   4300 50   27   800 1100
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 2 880   880   6200 710 1.3  0      910    900    18000   5400 53   28   810 1100
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 2 880   880   6400 720 1.3  0      910    890    13000   5400 44   24   760 1000
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c 2 1.7 1.6 20 83 1.0  0      900    850    15000   6100 150   120   2200 880
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c 2 1.5 1.5 20 87 .96 0      760    690    22000   7000 84   69   1000 850
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c 1 11   11   140 120 .96 0      780    710    25000   7000 960   920   20000 1900
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c 2 16   16   200 95 .95 0      320    320    11000   800 420   370   5600 930
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c 2 1.5 1.5 22 86 .96 0      840    770    16000   7000 28   15   280 560
bitvector-regression/implicitfloatconversion_false-unreach-call.c 1 1.5 1.5 16 71 .82 0      3.6  2.0  68 270 12   6.2 150 300
bitvector-regression/implicitunsignedconversion_false-unreach-call.c 1 1.4 1.5 22 73 .82 .0041 3.5  2.0  69 270 6.9 3.7 51 330
bitvector-regression/integerpromotion_false-unreach-call.c 1 1.5 1.6 18 69 .83 0      3.5  2.0  46 270 14   7.6 87 320
bitvector-regression/recHanoi03_false-unreach-call.c 1 8.6 8.4 130 78 .84 .090  4.9  2.7  52 280 13   6.8 160 320
bitvector-regression/signextension2_false-unreach-call.c 1 1.5 1.6 19 72 .83 0      3.6  2.0  71 280 6.6 3.5 53 310
bitvector-regression/signextension_false-unreach-call.c 1 1.5 1.5 18 70 .83 0      3.7  2.1  76 270 6.7 3.6 81 300
bitvector-regression/implicitunsignedconversion_true-unreach-call.c 2 1.2 1.2 17 75 .82 0      3.3  1.9  62   250 7.3 3.9 100 310
bitvector-regression/integerpromotion_true-unreach-call.c 2 1.1 1.2 15 68 .83 0      4.0  2.2  51   250 12   6.5 240 320
bitvector-regression/signextension2_true-unreach-call.c 2 1.2 1.3 15 72 .83 0      3.8  2.1  45   260 8.7 4.6 120 320
bitvector-regression/signextension_true-unreach-call.c 2 1.2 1.3 13 81 .83 16      3.5  2.0  61   250 8.3 4.5 110 310
bitvector-loops/diamond_false-unreach-call2.i 1 1.9 1.8 29 93 .89 0      3.9  2.2  55 280 8.6 4.5 110 350
bitvector-loops/overflow_false-unreach-call1.i 0 880   930   12000 930 .83 0      .53 .34 13 42 5.7 3.0 99 290
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 1 4.7 4.5 62 110 .87 0      3.9  2.2  74 280 27   14   270 710
../../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 78 17000 17000 170000 12000 49   18     50 60 33 1000 3500   50 160 88 1900 5000   50 12000 11000 250000 110000   50 11000 10000 250000 30000  
    correct results 43 74 11000 11000 110000 9200 42   16     12 59 32 1000 3400   12 150 81 1700 4400   18 8900 8600 180000 86000   25 7200 6600 160000 22000  
        correct true 31 62 11000 11000 110000 7800 31   16     1 0 0 0 0   4 0 0 0 0   18 8900 8600 180000 86000   25 7200 6600 160000 22000  
        correct false 12 12 90 89 1100 1400 11   .094 11 59 32 1000 3400   8 150 81 1700 4400   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 4 4 2700 2700 27000 1200 3.9 0     0 0 0 0 0   0 0 0 0 0   0 2900 2800 70000 22000   0 3800 3600 91000 6900  
        correct-unconfirmed true 4 4 2700 2700 27000 1200 3.9 0     0 0 0 0 0   0 0 0 0 0   0 2900 2800 70000 22000   0 3800 3600 91000 6900  
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (50 tasks, max score: 86) 78
Run set sv-comp17.ReachSafety-BitVectors