Tool skink
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:20 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 01:53:26 CET ]] [[ 2017-01-15 01:38:17 CET ]] [[ 2017-01-15 01:54:04 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/skink.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/skink.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/skink.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/skink.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 unknown 0 wit inspect 11   3.8 87 680 .037  0   error (invalid witness file) .50 .31 9.2 39 error (invalid witness file) 6.4 3.4 100 300 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 wit inspect 4.9 1.7 39 340 .037  0   error (invalid witness file) .49 .33 11   39 error (invalid witness file) 6.3 3.3 88 300 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 11   3.9 81 680 .037  0   - - error (invalid witness file) .57 .37 13   45 error (invalid witness file) 6.0 3.2 72 290
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 11   3.9 95 680 .037  0   - - error (invalid witness file) .47 .30 11   40 error (invalid witness file) 7.4 3.9 72 300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 6.0 1.9 49 350 .037  0   - - error (invalid witness file) .51 .32 8.9 39 error (invalid witness file) 5.8 3.1 58 310
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 6.4 2.0 54 350 .037  0   - - error (invalid witness file) .48 .32 12   40 error (invalid witness file) 6.9 3.6 84 300
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 5.7 1.8 46 340 .037  0   - - error (invalid witness file) .58 .38 7.5 41 error (invalid witness file) 6.7 3.6 90 300
bitvector/gcd_4_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 6.0 1.9 50 350 .037  0   - - error (invalid witness file) .53 .34 12   41 error (invalid witness file) 6.2 3.3 64 300
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 5.9 1.9 43 340 .037  0   - - error (invalid witness file) .49 .32 9.8 40 error (invalid witness file) 7.1 3.7 86 300
bitvector/jain_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 4.6 1.5 37 330 .037  0   - - error (invalid witness file) .52 .33 10   41 error (invalid witness file) 6.5 3.4 73 300
bitvector/jain_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 4.7 1.6 43 330 .037  0   - - error (invalid witness file) .51 .33 9.6 40 error (invalid witness file) 7.1 3.7 75 300
bitvector/jain_4_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 4.8 1.6 42 330 .037  0   - - error (invalid witness file) .53 .39 8.5 40 error (invalid witness file) 7.9 4.1 78 310
bitvector/jain_5_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 4.6 1.6 35 330 .037  0   - - error (invalid witness file) .51 .33 11   39 error (invalid witness file) 6.5 3.4 86 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 4.9 1.7 44 330 .037  0   - - error (invalid witness file) .49 .33 11   39 error (invalid witness file) 8.3 4.4 76 310
bitvector/jain_7_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 4.9 1.7 42 340 .037  0   - - error (invalid witness file) .51 .32 9.1 39 error (invalid witness file) 6.0 3.1 110 300
bitvector/modulus_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 5.7 1.8 45 340 .037  0   - - error (invalid witness file) .54 .35 8.7 39 error (invalid witness file) 5.6 3.0 74 290
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 5.1 1.7 39 340 .037  0   - - error (invalid witness file) .61 .39 7.8 40 error (invalid witness file) 7.4 3.9 79 300
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 5.3 1.7 43 320 .037  0   - - error (invalid witness file) .57 .37 11   42 error (invalid witness file) 5.8 3.1 110 300
bitvector/parity_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 5.2 1.7 42 340 .037  0   - - error (invalid witness file) .52 .33 12   39 error (invalid witness file) 8.7 4.5 95 310
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 4.6 1.6 36 330 .037  0   - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 7.1 3.8 75 300
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 17   8.0 140 750 .037  0   error (invalid witness file) .54 .34 9.5 40 error (invalid witness file) 6.5 3.4 95 290 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 17   7.9 140 780 .037  0   error (invalid witness file) .53 .33 12   40 error (invalid witness file) 5.5 2.9 100 290 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 17   8.0 140 760 .0041 0   error (invalid witness file) .52 .34 13   41 error (invalid witness file) 7.4 3.9 81 290 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 17   8.0 150 740 .037  0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.4 3.4 60 290
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 17   7.8 160 780 .037  0   - - error (invalid witness file) .52 .32 10   41 error (invalid witness file) 6.4 3.4 84 300
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 17   8.0 140 750 .037  0   - - error (invalid witness file) .63 .40 8.8 42 error (invalid witness file) 5.9 3.1 92 300
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 20   9.2 180 840 .037  0   - - error (invalid witness file) .54 .35 12   43 error (invalid witness file) 5.8 3.1 80 300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 20   8.9 180 820 .037  0   - - error (invalid witness file) .51 .34 11   40 error (invalid witness file) 7.5 3.9 83 300
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 18   8.2 140 820 .037  0   - - error (invalid witness file) .55 .35 11   44 error (invalid witness file) 6.1 3.2 61 300
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 18   8.4 160 820 .037  0   - - error (invalid witness file) .53 .34 11   39 error (invalid witness file) 5.6 2.9 99 290
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 19   8.4 170 830 .037  0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.3 3.3 81 300
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 19   8.3 150 800 .037  0   - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 7.2 3.8 70 300
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c unknown 0 wit inspect 14   5.4 100 710 .037  0   - - error (invalid witness file) .50 .31 8.9 40 error (invalid witness file) 7.2 3.8 65 300
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c unknown 0 wit inspect 12   4.7 100 700 .037  0   - - error (invalid witness file) .54 .36 11   44 error (invalid witness file) 6.1 3.3 110 300
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c unknown 0 wit inspect 13   4.8 110 710 .037  0   - - error (invalid witness file) .69 .43 7.3 41 error (invalid witness file) 6.4 3.4 110 310
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c unknown 0 wit inspect 13   5.3 110 710 .037  0   - - error (invalid witness file) .53 .35 13   43 error (invalid witness file) 6.0 3.2 100 300
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c unknown 0 wit inspect 12   4.8 93 730 .037  0   - - error (invalid witness file) .51 .31 11   40 error (invalid witness file) 7.0 3.7 84 300
bitvector-regression/implicitfloatconversion_false-unreach-call.c unknown 0 wit inspect 4.3 1.5 35 300 .037  0   error (invalid witness file) .50 .32 9.6 41 error (invalid witness file) 5.7 3.0 98 290 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c false(unreach-call) 1 wit inspect 4.4 1.5 36 320 .037  0   false(unreach-call) 3.4  1.9  69   260 false(unreach-call) 9.6 5.1 100 330 - -
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) 1 wit inspect 4.6 1.6 40 340 .037  0   false(unreach-call) 4.0  2.3  41   270 false(unreach-call) 13   7.2 220 320 - -
bitvector-regression/recHanoi03_false-unreach-call.c unknown 0 wit inspect 3.9 1.5 34 300 .037  0   error (invalid witness file) .53 .34 11   40 error (invalid witness file) 8.1 4.3 90 320 - -
bitvector-regression/signextension2_false-unreach-call.c false(unreach-call) 1 wit inspect 4.9 1.7 45 310 .037  0   false(unreach-call) 3.5  1.9  67   270 true 7.6 4.0 100 310 - -
bitvector-regression/signextension_false-unreach-call.c false(unreach-call) 1 wit inspect 4.9 1.7 35 310 .037  0   false(unreach-call) 3.6  2.0  65   260 true 9.2 4.9 85 320 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true 2 wit inspect 4.5 1.5 35 320 .037  0   - - true 3.3  1.9  75   260 true 7.5 4.0 120 310
bitvector-regression/integerpromotion_true-unreach-call.c true 2 wit inspect 5.0 1.6 42 340 .037  0   - - true 3.4  2.0  43   250 true 14   7.4 170 310
bitvector-regression/signextension2_true-unreach-call.c true 2 wit inspect 5.3 1.7 40 330 .037  0   - - true 3.5  1.9  81   260 true 8.9 4.7 99 310
bitvector-regression/signextension_true-unreach-call.c true 2 wit inspect 5.5 1.8 45 340 .037  0   - - true 3.4  1.9  58   260 true 10   5.4 84 320
bitvector-loops/diamond_false-unreach-call2.i unknown 0 wit inspect 5.7 1.9 48 350 .037  0   error (invalid witness file) .51 .33 11   41 error (invalid witness file) 7.1 3.8 73 290 - -
bitvector-loops/overflow_false-unreach-call1.i unknown 0 wit inspect 4.7 1.6 38 330 .0041 0   error (invalid witness file) .64 .41 7.2 44 error (invalid witness file) 7.4 3.9 74 310 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i unknown 0 wit inspect 5.5 1.7 47 340 .037  0   error (invalid witness file) .48 .30 8.4 39 error (invalid witness file) 7.4 3.9 86 290 - -
../../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 12 460 190   3900 25000 1.8  0   50 20 12   340 1500   50 110 57 1400 4300   50 31 19   590 2300   50 250 130 3100 11000  
    correct results 8 12 39 13   320 2600 .29 0   4 15 8.2 240 1100   4 40 21 510 1300   4 14 7.7 260 1000   4 40 21 470 1300  
        correct true 4 8 20 6.6 160 1300 .15 0   0 0 0   0 0   2 0 0 0 0   4 14 7.7 260 1000   4 40 21 470 1300  
        correct false 4 4 19 6.5 160 1300 .15 0   4 15 8.2 240 1100   2 40 21 510 1300   0 0 0   0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (50 tasks, max score: 86) 12
Run set sv-comp17.ReachSafety-BitVectors