Tool ULTIMATE Taipan 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-14 09:46:18 CET [[ 2017-01-15 02:18:39 CET ]] [[ 2017-01-15 04:12:25 CET ]] [[ 2017-01-15 02:37:40 CET ]] [[ 2017-01-15 04:38:18 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.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 92   45   1000 940 2.6 0     24    13    290   900 34   18   350 520
bitvector/sum02_false-unreach-call_true-no-overflow.i 0 180   180   2200 370 2.5 0     .54 .34 9.9 42 6.2 3.3 130 300
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 0 900   830   11000 1200 2.5 0     .54 .34 12   41 5.9 3.1 110 300
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 0 900   830   13000 1200 2.5 0     .63 .41 8.4 40 5.5 3.0 100 300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 0 900   890   12000 460 2.3 0     .53 .35 8.1 40 7.3 3.8 110 340
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 0 900   890   11000 560 2.3 0     .62 .40 7.3 40 5.7 3.0 81 300
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 0 900   890   11000 610 2.3 0     .61 .39 7.8 39 5.6 3.0 100 290
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 0 900   890   11000 1100 2.3 0     .72 .46 7.8 44 5.7 3.0 120 290
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2 340   320   3400 1600 2.6 0     8.2  5.1  110   340 83   66   1500 610
bitvector/jain_1_true-unreach-call_true-no-overflow.i 2 6.2 1.9 48 340 2.5 0     900    900    23000   2600 7.4 4.1 140 310
bitvector/jain_2_true-unreach-call_true-no-overflow.i 2 6.7 1.9 51 350 2.5 0     900    900    15000   3600 8.0 4.3 120 320
bitvector/jain_4_true-unreach-call_true-no-overflow.i 2 6.2 1.9 43 320 2.5 0     900    900    21000   1600 11   7.1 170 340
bitvector/jain_5_true-unreach-call_true-no-overflow.i 1 7.2 2.3 59 360 2.5 0     360    350    8800   7000 960   860   17000 2900
bitvector/jain_6_true-unreach-call_true-no-overflow.i 2 6.3 2.0 51 330 2.5 0     900    900    20000   1700 9.0 4.9 170 360
bitvector/jain_7_true-unreach-call_true-no-overflow.i 2 6.6 2.0 56 340 2.5 0     900    900    15000   780 25   20   570 380
bitvector/modulus_true-unreach-call_true-no-overflow.i 0 9.7 5.8 99 330 2.5 0     .65 .41 8.5 40 5.7 3.1 100 290
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 2 110   94   1300 2400 2.5 0     4.7  2.6  60   280 58   46   580 490
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 0 900   870   12000 740 2.5 0     .66 .42 8.1 41 5.6 3.0 110 290
bitvector/parity_true-unreach-call_true-no-overflow.i 0 900   890   13000 940 2.5 0     .53 .34 12   40 6.0 3.2 110 300
bitvector/sum02_true-unreach-call_true-no-overflow.i 0 37   32   450 370 2.5 0     .63 .38 9.0 42 5.5 3.0 72 300
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 1 24   6.7 170 580 2.9 0     7.5  4.0  120   330 23   12   210 520
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 1 28   7.8 210 630 3.0 0     6.9  3.6  60   300 29   15   330 580
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 1 22   6.6 160 560 2.8 0     6.0  3.2  70   290 24   13   380 510
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 2 36   12   280 850 2.8 0     70    59    1200   990 46   25   400 770
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 2 42   13   320 1000 2.8 0     19    11    390   600 53   29   670 1100
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 2 130   93   1500 4800 2.7 0     22    13    220   550 130   77   1100 7000
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900   720   12000 2700 2.3 0     .57 .36 9.0 39 5.9 3.1 100 290
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900   720   12000 4500 2.3 .012 .62 .41 10   40 7.1 3.7 100 300
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900   720   12000 4700 2.3 0     .62 .39 5.9 40 6.0 3.2 120 300
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900   720   12000 4700 2.3 0     .68 .44 7.4 45 5.5 3.0 83 290
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900   730   12000 3600 2.3 0     .70 .44 7.6 42 5.9 3.2 93 300
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900   730   12000 4100 2.3 0     .57 .37 7.0 39 5.7 3.1 110 290
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c 0 130   96   1700 830 2.5 0     .58 .38 6.7 39 5.9 3.1 140 300
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c 2 110   61   1100 1500 2.5 0     760    700    23000   7000 78   66   1500 890
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c 0 900   860   12000 840 2.7 0     .62 .39 8.9 40 5.4 2.9 81 290
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c 0 610   560   7500 1900 2.5 0     .47 .31 8.1 40 5.8 3.1 100 290
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c 2 46   19   470 910 2.6 0     740    670    18000   7000 21   12   240 540
bitvector-regression/implicitfloatconversion_false-unreach-call.c 1 8.7 3.0 63 310 2.9 0     3.2  1.8  40   270 11   6.1 210 310
bitvector-regression/implicitunsignedconversion_false-unreach-call.c 1 6.4 1.9 52 350 2.5 0     3.5  2.0  69   270 7.1 3.8 160 310
bitvector-regression/integerpromotion_false-unreach-call.c 1 9.0 3.1 75 330 2.6 0     3.8  2.1  51   270 12   6.2 180 310
bitvector-regression/recHanoi03_false-unreach-call.c 0 220   190   2600 810 2.7 0     95    81    1100   3100 9.4 4.9 150 350
bitvector-regression/signextension2_false-unreach-call.c 1 5.4 1.8 41 320 2.5 0     4.0  2.3  53   260 7.1 3.8 120 320
bitvector-regression/signextension_false-unreach-call.c 1 5.3 1.8 43 310 2.5 0     4.1  2.3  35   270 7.2 3.8 110 310
bitvector-regression/implicitunsignedconversion_true-unreach-call.c 2 5.8 1.9 46 330 2.5 0     4.0  2.3  48   260 7.1 3.8 120 320
bitvector-regression/integerpromotion_true-unreach-call.c 2 9.7 3.2 83 320 2.6 0     3.4  1.9  67   260 12   6.5 190 300
bitvector-regression/signextension2_true-unreach-call.c 2 6.0 1.9 46 330 2.5 0     4.1  2.3  63   270 7.4 4.0 140 310
bitvector-regression/signextension_true-unreach-call.c 2 5.6 1.8 44 330 2.9 0     4.4  2.5  43   250 7.7 4.2 130 310
bitvector-loops/diamond_false-unreach-call2.i 1 12   3.7 98 450 2.5 0     5.1  2.8  39   280 7.7 4.1 95 340
bitvector-loops/overflow_false-unreach-call1.i 0 900   790   14000 870 2.3 0     .52 .35 12   40 5.9 3.1 99 300
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 0 190   170   2300 740 2.5 0     4.1  2.3  62   270 55   34   470 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 43 17000   15000   220000 59000 130   .012 50 170 120 2000 6900   50 240 130 3000 12000   50 6500 6300 150000 36000   50 1600 1300 27000 23000  
    correct results 26 42 1100   710   11000 21000 68   0     10 68 37 820 3500   10 160 86 2200 4000   9 6100 6000 140000 28000   15 560 380 7700 14000  
        correct true 16 32 880   630   8800 16000 42   0     4 0 0 0 0   0 0 0 0 0   9 6100 6000 140000 28000   15 560 380 7700 14000  
        correct false 10 10 210   81   2000 4800 27   0     6 68 37 820 3500   10 160 86 2200 4000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 3 1 420   360   5000 1900 7.8 0     1 99 83 1100 3300   1 64 39 620 7400   0 360 350 8800 7000   0 960 860 17000 2900  
        correct-unconfirmed true 1 1 7.2 2.3 59 360 2.5 0     1 0 0 0 0   1 0 0 0 0   0 360 350 8800 7000   0 960 860 17000 2900  
        correct-unconfirmed false 2 0 410   360   4900 1500 5.2 0     0 99 83 1100 3300   0 64 39 620 7400   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) 43
Run set sv-comp17.ReachSafety-BitVectors