Tool ULTIMATE Kojak f7c3ed31
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 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.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 29   15   270 480 2.6 0     true 35    19    440   1300 false(unreach-call) 33   18   360 560 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   870   13000 660 2.5 0     error (invalid witness file) .59 .37 9.2 41 error (invalid witness file) 6.2 3.3 64 310 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   820   12000 3500 2.5 0     - - error (invalid witness file) .63 .39 7.6 40 error (invalid witness file) 5.2 2.8 79 290
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   840   11000 4500 2.5 0     - - error (invalid witness file) .66 .41 7.0 41 error (invalid witness file) 7.5 3.9 95 310
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 110   100   950 480 2.5 0     - - true 12    9.3  190   320 timeout 960   950   14000 620
bitvector/gcd_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   890   11000 720 2.3 0     - - error (invalid witness file) .59 .37 11   43 error (invalid witness file) 6.1 3.2 110 290
bitvector/gcd_3_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   890   11000 640 2.3 0     - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 5.5 3.0 120 290
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 13   4.3 110 480 2.5 0     - - true 4.9  2.8  89   320 timeout 960   940   13000 790
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 91   74   1100 1800 2.6 0     - - true 9.3  5.7  120   350 true 84   66   1400 640
bitvector/jain_1_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   570   9500 890 2.3 0     - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.1 3.2 110 290
bitvector/jain_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   560   11000 850 2.3 0     - - error (invalid witness file) .51 .34 11   40 error (invalid witness file) 5.9 3.1 110 300
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.4 2.1 46 320 2.5 0     - - timeout 900    900    17000   2100 true 7.6 4.1 110 320
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   830   14000 800 2.3 0     - - error (invalid witness file) .51 .33 6.4 41 error (invalid witness file) 5.9 3.1 120 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.7 5.2 96 330 2.5 0     - - timeout 900    900    18000   2100 true 7.2 3.9 160 310
bitvector/jain_7_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   540   10000 770 2.3 0     - - error (invalid witness file) .56 .34 9.3 40 error (invalid witness file) 5.8 3.1 100 290
bitvector/modulus_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   890   8600 830 2.5 0     - - error (invalid witness file) .52 .33 12   42 error (invalid witness file) 6.2 3.2 100 310
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 300   280   3800 2600 2.5 0     - - true 6.1  3.4  73   290 true 61   48   1100 510
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   860   12000 840 2.5 0     - - error (invalid witness file) .52 .32 13   40 error (invalid witness file) 5.8 3.0 100 300
bitvector/parity_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   870   12000 1400 2.5 0     - - error (invalid witness file) .61 .39 9.0 40 error (invalid witness file) 6.0 3.2 100 310
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   880   8900 800 2.5 0     - - error (invalid witness file) .69 .43 9.5 43 error (invalid witness file) 6.3 3.3 120 290
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   770   15000 4900 2.3 0     error (invalid witness file) .54 .34 8.7 41 error (invalid witness file) 5.9 3.2 110 300 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   770   13000 4200 2.3 0     error (invalid witness file) .48 .31 10   40 error (invalid witness file) 6.2 3.3 120 290 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 87   59   960 860 2.7 0     true 10    5.4  130   440 false(unreach-call) 24   13   410 510 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   780   14000 4700 2.3 .057 - - error (invalid witness file) .59 .38 8.5 40 error (invalid witness file) 6.1 3.3 110 290
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   770   12000 4400 2.3 0     - - error (invalid witness file) .59 .38 11   41 error (invalid witness file) 6.3 3.4 140 310
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   780   12000 1700 2.3 0     - - error (invalid witness file) .53 .35 11   44 error (invalid witness file) 6.3 3.3 97 300
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   810   14000 4500 2.3 0     - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 6.7 3.5 130 310
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   780   13000 1300 2.3 0     - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.0 3.2 120 290
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   790   12000 1300 2.3 0     - - error (invalid witness file) .70 .44 8.0 42 error (invalid witness file) 6.1 3.3 120 300
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   780   14000 1100 2.3 0     - - error (invalid witness file) .53 .34 10   40 error (invalid witness file) 6.1 3.2 120 300
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   780   13000 4800 2.3 0     - - error (invalid witness file) .65 .41 9.9 43 error (invalid witness file) 5.8 3.1 85 300
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   780   13000 4700 2.3 0     - - error (invalid witness file) .61 .40 8.5 41 error (invalid witness file) 6.0 3.2 96 290
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c timeout 0 wit inspect 900   530   11000 1900 2.3 0     - - error (invalid witness file) .57 .35 13   44 error (invalid witness file) 6.0 3.2 79 290
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c timeout 0 wit inspect 900   710   12000 1300 2.3 0     - - error (invalid witness file) .59 .38 9.3 45 error (invalid witness file) 5.9 3.1 87 310
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c timeout 0 wit inspect 900   710   13000 1300 2.3 0     - - error (invalid witness file) .66 .43 8.5 41 error (invalid witness file) 6.3 3.3 110 300
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c timeout 0 wit inspect 900   550   9900 2200 2.3 0     - - error (invalid witness file) .50 .31 12   40 error (invalid witness file) 5.8 3.1 110 300
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c timeout 0 wit inspect 900   710   13000 1400 2.3 0     - - error (invalid witness file) .54 .34 13   40 error (invalid witness file) 5.6 3.0 100 300
bitvector-regression/implicitfloatconversion_false-unreach-call.c error 0 wit inspect 4.8 1.5 38 310 2.5 0     error (invalid witness file) .57 .37 9.0 42 error (invalid witness file) 5.7 3.0 100 300 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c false(unreach-call) 1 wit inspect 5.9 1.8 48 330 2.5 0     false(unreach-call) 4.4  2.5  45   270 false(unreach-call) 7.0 3.7 130 310 - -
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) 1 wit inspect 9.8 3.1 70 340 2.6 0     false(unreach-call) 3.4  2.0  60   270 false(unreach-call) 11   6.0 130 320 - -
bitvector-regression/recHanoi03_false-unreach-call.c false(unreach-call) 0 wit inspect 110   87   1500 840 2.6 0     timeout 95    81    1200   3800 true 8.9 4.6 190 340 - -
bitvector-regression/signextension2_false-unreach-call.c false(unreach-call) 1 wit inspect 5.6 1.9 43 320 2.5 0     false(unreach-call) 3.5  2.0  54   270 false(unreach-call) 6.5 3.6 140 320 - -
bitvector-regression/signextension_false-unreach-call.c false(unreach-call) 1 wit inspect 5.6 1.8 43 320 2.5 0     false(unreach-call) 3.6  2.0  47   270 false(unreach-call) 7.3 3.9 150 320 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true 2 wit inspect 6.4 1.9 53 330 2.5 0     - - true 3.3  1.9  51   250 true 7.2 3.8 110 320
bitvector-regression/integerpromotion_true-unreach-call.c true 2 wit inspect 8.9 3.0 70 320 2.6 0     - - true 3.3  1.9  66   250 true 12   6.5 190 320
bitvector-regression/signextension2_true-unreach-call.c true 2 wit inspect 5.6 1.8 44 320 2.5 0     - - true 4.7  2.6  50   260 true 6.9 3.8 110 310
bitvector-regression/signextension_true-unreach-call.c true 2 wit inspect 6.6 2.0 49 340 2.5 0     - - true 4.2  2.3  47   270 true 7.0 3.7 85 310
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 6.4 2.1 50 330 2.5 0     true 7.4  4.1  82   300 false(unreach-call) 8.3 4.4 150 340 - -
bitvector-loops/overflow_false-unreach-call1.i timeout 0 wit inspect 900   800   13000 980 2.3 0     error (invalid witness file) .58 .36 8.3 41 error (invalid witness file) 6.0 3.2 110 300 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i error 0 wit inspect 670   650   7500 650 2.5 0     error (invalid witness file) .51 .33 8.1 40 error (invalid witness file) 5.6 3.0 110 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 27 29000 24000 380000 76000 120   .057 50 170 120 2100 7200   50 140   76   2300 4800   50 1900 1800 36000 7600   50 2300 2100 34000 12000  
    correct results 17 27 710 570 7800 10000 43   0     7 67 37 860 3200   7 98   52   1500 2700   8 1900 1800 36000 6500   8 2100 2000 31000 4500  
        correct true 10 20 560 480 6300 7300 25   0     3 0 0 0 0   0 0   0   0 0   8 1900 1800 36000 6500   8 2100 2000 31000 4500  
        correct false 7 7 150 85 1500 3000 18   0     4 67 37 860 3200   7 98   52   1500 2700   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 1 0 110 87 1500 840 2.6 0     0 95 81 1200 3800   1 8.9 4.6 190 340   0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 1 0 110 87 1500 840 2.6 0     0 95 81 1200 3800   0 8.9 4.6 190 340   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) 27
Run set sv-comp17.ReachSafety-BitVectors