Tool ULTIMATE Automizer 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 12:41:58 CET [[ 2017-01-15 02:09:41 CET ]] [[ 2017-01-15 04:03:21 CET ]] [[ 2017-01-15 02:31:54 CET ]] [[ 2017-01-15 04:27:36 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.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 55   24   540 750 2.6 0      true 26    14    250   930 false(unreach-call) 35   19   300 530 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   900   11000 340 2.3 0      error (invalid witness file) .53 .35 13   39 error (invalid witness file) 6.0 3.2 120 310 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   800   11000 4100 2.5 0      - - error (invalid witness file) .66 .42 9.2 41 error (invalid witness file) 5.9 3.2 120 300
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 580   510   6800 1400 2.6 0      - - true 9.2  5.0  190   340 true 400   350   5100 1600
bitvector/gcd_1_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   890   11000 530 2.3 0      - - error (invalid witness file) .54 .36 8.6 39 error (invalid witness file) 6.5 3.4 130 300
bitvector/gcd_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   890   11000 730 2.3 0      - - error (invalid witness file) .54 .34 9.2 40 error (invalid witness file) 5.4 2.9 100 290
bitvector/gcd_3_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   890   11000 560 2.3 0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 5.6 3.0 87 290
bitvector/gcd_4_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   880   11000 670 2.3 0      - - error (invalid witness file) .65 .41 9.1 40 error (invalid witness file) 6.6 3.5 130 300
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 120   98   1200 1700 2.6 0      - - true 8.1  5.0  150   350 true 80   63   990 640
bitvector/jain_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.7 2.0 55 340 2.5 0      - - timeout 900    900    17000   2500 true 8.3 4.5 150 330
bitvector/jain_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.2 2.0 56 340 2.5 0      - - timeout 900    900    24000   3800 true 7.8 4.2 100 320
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.7 1.9 49 330 2.5 0      - - timeout 900    900    19000   1600 true 12   7.4 150 360
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   760   13000 2200 2.3 0      - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 5.6 3.0 83 310
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.9 2.0 48 330 2.5 0      - - timeout 900    900    26000   1700 true 8.6 4.7 170 320
bitvector/jain_7_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.9 2.0 50 320 2.5 0      - - timeout 900    900    19000   690 true 43   38   640 370
bitvector/modulus_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 29   25   420 330 2.5 0      - - error (invalid witness file) .76 .48 9.1 44 error (invalid witness file) 6.0 3.2 110 290
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 270   250   3800 2300 2.5 0      - - true 4.6  2.6  89   280 true 60   48   960 530
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   860   11000 880 2.5 0      - - error (invalid witness file) .47 .30 9.3 39 error (invalid witness file) 5.6 3.0 100 290
bitvector/parity_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   880   11000 1000 2.5 0      - - error (invalid witness file) .56 .37 9.1 39 error (invalid witness file) 6.0 3.2 130 300
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   890   12000 510 2.3 0      - - error (invalid witness file) .71 .44 8.8 42 error (invalid witness file) 6.2 3.2 120 290
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 24   6.9 200 570 2.9 0      true 6.5  3.4  80   300 false(unreach-call) 22   12   190 520 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 28   7.7 220 720 3.0 0      true 7.0  3.7  120   300 false(unreach-call) 36   19   380 600 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 22   6.4 170 560 2.8 0      true 6.4  3.4  68   290 false(unreach-call) 25   13   400 510 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 35   9.8 280 840 2.8 0      - - true 63    53    1100   950 true 45   25   430 810
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 42   13   360 1100 2.7 0      - - true 18    11    280   600 true 53   29   600 1000
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 25   6.4 190 1100 2.7 0      - - true 21    12    270   570 out of memory 120   75   1300 7000
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   870   13000 2400 2.3 0      - - error (invalid witness file) .65 .41 8.0 39 error (invalid witness file) 6.8 3.5 100 310
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 47   17   460 1900 2.7 0      - - timeout 910    900    16000   4900 true 52   28   670 1100
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 39   12   340 1500 2.7 0      - - timeout 910    890    15000   4200 true 41   22   460 1100
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 38   12   290 1600 2.7 0      - - timeout 910    890    14000   4100 true 42   22   420 1100
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 36   11   300 1400 2.7 0      - - timeout 910    900    20000   5300 true 44   24   430 1100
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 36   11   310 1500 2.7 0      - - timeout 910    900    16000   5400 true 46   24   570 1000
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c witness invalid (true) 0 wit inspect 160   130   1900 890 2.5 0      - - error (invalid witness file) .58 .37 13   42 error (invalid witness file) 5.5 3.0 95 290
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 220   200   2500 1000 2.5 0      - - out of memory 800    730    20000   7000 true 80   66   1200 950
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c timeout 0 wit inspect 900   870   10000 1600 2.5 0      - - error (invalid witness file) .63 .41 7.5 40 error (invalid witness file) 7.3 3.8 90 300
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 510   470   5400 1000 2.6 0      - - true 380    370    7900   770 true 290   260   3500 1000
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 15   4.4 110 610 2.6 0      - - out of memory 750    670    24000   7000 true 20   11   260 540
bitvector-regression/implicitfloatconversion_false-unreach-call.c false(unreach-call) 1 wit inspect 9.1 3.0 69 320 2.6 0      false(unreach-call) 4.4  2.5  50   270 false(unreach-call) 11   5.8 150 310 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c false(unreach-call) 1 wit inspect 5.4 1.8 45 320 2.5 0      false(unreach-call) 3.4  1.9  47   270 false(unreach-call) 6.8 3.6 100 310 - -
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) 1 wit inspect 8.9 3.0 74 320 2.6 0      false(unreach-call) 3.5  2.0  51   270 false(unreach-call) 12   6.2 170 330 - -
bitvector-regression/recHanoi03_false-unreach-call.c false(unreach-call) 0 wit inspect 87   62   1200 880 2.6 0      timeout 95    81    1500   3800 true 7.9 4.2 110 340 - -
bitvector-regression/signextension2_false-unreach-call.c false(unreach-call) 1 wit inspect 5.8 1.9 43 320 2.5 0      false(unreach-call) 3.6  2.0  61   270 false(unreach-call) 6.9 3.7 120 310 - -
bitvector-regression/signextension_false-unreach-call.c false(unreach-call) 1 wit inspect 6.7 1.9 51 330 2.5 0      false(unreach-call) 3.6  2.0  59   260 false(unreach-call) 7.1 3.8 140 320 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true 2 wit inspect 5.6 1.9 44 330 2.5 0      - - true 4.2  2.4  44   260 true 7.9 4.2 160 330
bitvector-regression/integerpromotion_true-unreach-call.c true 2 wit inspect 9.0 3.1 75 310 2.6 0      - - true 4.1  2.3  39   260 true 12   6.3 170 310
bitvector-regression/signextension2_true-unreach-call.c true 2 wit inspect 5.7 1.8 49 320 2.5 0      - - true 4.0  2.3  51   250 true 7.5 4.0 150 320
bitvector-regression/signextension_true-unreach-call.c true 2 wit inspect 6.1 1.9 43 330 2.5 0      - - true 4.0  2.2  63   270 true 7.7 4.1 120 320
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 8.1 2.7 61 370 2.5 0      false(unreach-call) 4.2  2.3  53   290 false(unreach-call) 8.2 4.4 150 360 - -
bitvector-loops/overflow_false-unreach-call1.i timeout 0 wit inspect 900   750   15000 1500 2.3 0      error (invalid witness file) .50 .31 9.2 43 error (invalid witness file) 5.4 2.9 100 290 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(unreach-call) 0 wit inspect 160   150   2000 740 2.5 .0082 true 4.2  2.3  67   280 out of memory 72   43   850 7000 - -
../../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 56 14000 13000 180000 46000 130   .0082 50 170 120 2500 7600   50 260 140 3300 12000   50 11000 11000 240000 54000   50 1600 1200 20000 26000  
    correct results 33 56 2200 1700 24000 26000 86   0      10 69 38 840 3500   10 170 90 2100 4100   11 11000 11000 240000 53000   22 1500 1100 19000 23000  
        correct true 23 46 2100 1600 23000 22000 60   0      4 0 0 0 0   0 0 0 0 0   11 11000 11000 240000 53000   22 1500 1100 19000 23000  
        correct false 10 10 170 60 1500 4600 26   0      6 69 38 840 3500   10 170 90 2100 4100   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 2 0 250 210 3200 1600 5.1 .0082 1 99 84 1600 4100   1 79 47 960 7300   0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 2 0 250 210 3200 1600 5.1 .0082 0 99 84 1600 4100   0 79 47 960 7300   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) 56
Run set sv-comp17.ReachSafety-BitVectors