Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]]
Run set sv-comp17.ReachSafety-BitVectors
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.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 0 .14  .13  1.5  24 .84 0   22    11    240   650 96   80   1300 570
bitvector/sum02_false-unreach-call_true-no-overflow.i 0 900     890     1700    6700 .84 0   .61 .39 9.5 40 5.7 3.0 78 300
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 0 750     750     8200    15000 .84 0   .50 .33 6.7 39 6.5 3.5 120 320
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 0 750     750     9400    15000 .84 0   .56 .35 11   40 6.3 3.3 120 300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 0 900     900     2100    6900 .84 0   .48 .31 6.2 41 6.1 3.2 120 300
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 0 900     900     10000    310 .84 0   .54 .34 11   39 6.0 3.2 120 310
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 0 900     900     11000    250 .84 0   .51 .34 5.2 40 5.8 3.1 110 300
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 0 900     850     13000    9900 .84 0   .48 .30 11   39 5.2 2.8 84 290
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 0 92     89     1400    15000 .84 0   .53 .34 8.5 41 5.4 2.9 99 290
bitvector/jain_1_true-unreach-call_true-no-overflow.i 0 230     230     2300    15000 .84 0   .52 .34 9.6 43 5.8 3.1 100 300
bitvector/jain_2_true-unreach-call_true-no-overflow.i 0 170     170     1300    15000 .84 0   .52 .34 8.0 40 6.3 3.3 120 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i 0 270     270     2100    15000 .84 0   .55 .35 14   44 6.3 3.3 120 320
bitvector/jain_5_true-unreach-call_true-no-overflow.i 0 900     850     13000    12000 .84 0   .51 .35 7.9 40 6.2 3.3 120 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i 0 200     200     1600    15000 .84 0   .50 .31 12   40 5.9 3.1 110 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i 0 230     230     2500    15000 .84 0   .51 .33 11   40 5.9 3.1 120 290
bitvector/modulus_true-unreach-call_true-no-overflow.i 0 900     900     7900    1000 .84 0   .48 .31 9.5 39 5.8 3.1 120 290
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 0 900     880     14000    1700 .84 0   .61 .41 5.2 39 6.0 3.2 110 300
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 0 530     520     6700    15000 .84 0   .51 .32 8.9 42 6.2 3.2 120 300
bitvector/parity_true-unreach-call_true-no-overflow.i 0 900     900     11000    280 .99 0   .48 .32 9.7 39 6.0 3.2 110 300
bitvector/sum02_true-unreach-call_true-no-overflow.i 0 690     680     7600    15000 .84 0   .51 .34 9.9 40 5.3 2.9 93 290
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 1 3.0   3.0   35    110 .84 0   7.8  4.1  140   310 8.8 4.8 180 320
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 1 5.8   5.7   68    150 .84 0   10    5.4  99   330 9.1 4.8 160 320
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 1 5.7   5.7   14    66 .84 0   8.1  4.4  98   300 8.7 4.6 130 330
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     8500    5500 .84 0   .53 .35 10   42 6.4 3.4 130 300
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     13000    5300 .84 0   .50 .32 10   40 5.8 3.1 130 300
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     9800    4800 .84 0   .49 .33 7.9 41 6.4 3.4 130 300
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     11000    400 .84 0   .49 .32 9.6 40 5.6 3.0 110 290
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     9800    4000 .84 0   .49 .32 11   40 5.9 3.2 120 290
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     11000    2400 .84 0   .49 .31 9.5 40 6.4 3.4 130 290
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     9700    2600 .84 0   .65 .41 8.3 40 6.0 3.2 99 310
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     8800    3700 .84 0   .63 .39 9.9 40 6.7 3.5 140 300
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900     900     11000    3700 .84 0   .54 .33 12   41 6.0 3.2 100 290
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c 0 900     900     11000    3800 .84 0   .49 .32 9.0 40 5.8 3.1 100 300
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c 0 900     900     12000    4200 .84 0   .50 .33 11   39 6.0 3.1 120 300
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c 0 900     900     11000    4100 .84 0   .55 .35 9.9 40 6.0 3.2 120 300
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c 0 900     900     12000    1400 .84 0   .52 .33 5.0 42 6.0 3.2 110 300
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c 0 900     900     8700    3100 .84 0   .53 .35 9.6 42 6.0 3.2 120 300
bitvector-regression/implicitfloatconversion_false-unreach-call.c 1 .086 .085 .76 23 .84 0   3.8  2.1  70   270 11   5.8 160 300
bitvector-regression/implicitunsignedconversion_false-unreach-call.c 1 .27  .27  .72 23 .84 0   4.3  2.4  48   270 6.6 3.5 68 310
bitvector-regression/integerpromotion_false-unreach-call.c 1 .071 .071 .86 23 .84 0   4.2  2.4  48   270 14   7.2 170 330
bitvector-regression/recHanoi03_false-unreach-call.c 0 1.6   1.6   22    46 .84 0   97    76    1400   3500 96   76   2300 2900
bitvector-regression/signextension2_false-unreach-call.c 1 .11  .11  .62 23 .84 0   3.8  2.1  75   270 6.7 3.6 150 300
bitvector-regression/signextension_false-unreach-call.c 1 .086 .086 .91 23 .84 0   3.8  2.1  66   270 6.3 3.4 91 300
bitvector-regression/implicitunsignedconversion_true-unreach-call.c 0 900     820     10000    10000 .84 0   .48 .31 11   40 6.6 3.5 140 310
bitvector-regression/integerpromotion_true-unreach-call.c 0 50     48     690    15000 .99 0   .51 .33 7.2 41 5.9 3.1 110 300
bitvector-regression/signextension2_true-unreach-call.c 0 900     850     14000    6800 .84 0   .50 .31 10   40 5.8 3.1 110 300
bitvector-regression/signextension_true-unreach-call.c 0 900     810     12000    4900 .84 0   .49 .32 9.7 40 5.8 3.1 110 290
bitvector-loops/diamond_false-unreach-call2.i 1 .085 .084 .90 23 .84 0   4.5  2.5  68   280 7.6 4.1 93 330
bitvector-loops/overflow_false-unreach-call1.i 0 900     720     11000    9100 .84 0   .51 .32 11   40 6.2 3.2 120 300
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 1 .16  .16  1.4  24 .84 0   5.9  3.2  120   310 97   58   1500 5800
../../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 10 28000   28000   320000 280000 42   0   50 180 120 2500 7100 50 380 260 6600 13000 50 19 12 340 1500   50 220 110 4200 11000  
    correct results 10 10 15   15   120 490 8.4 0   10 56 31 840 2900 9 170 100 2700 8600 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 10 10 15   15   120 490 8.4 0   10 56 31 840 2900 2 170 100 2700 8600 0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 2 0 1.7 1.7 23 70 1.7 0   1 120 87 1600 4100 0 190 160 3700 3400 0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 2 0 1.7 1.7 23 70 1.7 0   0 120 87 1600 4100 0 190 160 3700 3400 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) 10
Run set sv-comp17.ReachSafety-BitVectors