Benchmark Symbiotic TBF Test-Suite Validator
Tool symbiotic 6.0.3-dev-fd3f777b Tbf Test-suite Validator v1.2
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 10800 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-45-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2019-02-06 07:07:32 CET 2019-02-06 14:52:39 CET
Run set symbiotic.test-comp19_prop-coverage-branches.ReachSafety-BitVectors tbf-testsuite-validator-symbiotic.test-comp19_prop-coverage-branches.ReachSafety-BitVectors
Options --test-comp --verifier klee-testcomp --verbose --sequence-file cov-seq.txt -r --test-suite ../../results-verified/symbiotic.2019-02-06_0707.logfiles/${rundefinition_name}.${inputfile_name}.files/test-suite.zip
sv-benchmarks/c/ status score program test-suite TS size inspect test-suite cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status program test-suite TS size inspect test-suite cov branch cov (%) line cov (%) cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
bitvector/byte_add-1.yml done .85  prog tests 3 inspect 1.7  1.7  20 21   0   0   true prog tests 1 inspect
85.0  100    .13 .13 16 .13  0  
bitvector/byte_add_1-1.yml done .733 prog tests 5 inspect .71 .71 20 8.8 0   0   unknown prog tests 0 inspect
73.3  82.8  .14 .14 17 .17  0  
bitvector/byte_add_2-2.yml done .75  prog tests 5 inspect .72 .71 20 10   0   0   unknown prog tests 0 inspect
75.0  82.8  .13 .18 17 .14  0  
bitvector/gcd_1.yml done .75  prog tests 3 inspect .72 .72 24 10   0   0   unknown prog tests 0 inspect
75.0  94.7  .12 .12 17 .11  0  
bitvector/gcd_2.yml done .7   prog tests 2 inspect 29    29    45 380   0   0   unknown prog tests 0 inspect
70.0  94.7  .12 .12 16 .094 0  
bitvector/gcd_3.yml done .7   prog tests 3 inspect 35    35    44 420   0   0   unknown prog tests 0 inspect
70.0  94.7  .14 .13 16 .11  0  
bitvector/interleave_bits.yml done .75  prog tests 1 inspect .37 .37 19 5.0 0   0   unknown prog tests 0 inspect
75.0  95.8  .11 .11 16 .078 0  
bitvector/modulus-2.yml done .8   prog tests 3 inspect 870    870    210 11000   0   0   unknown prog tests 0 inspect
80.0  90.5  .12 .12 16 .11  0  
bitvector/num_conversion_2.yml done .667 prog tests 1 inspect .34 .34 19 4.2 0   0   unknown prog tests 0 inspect
66.7  87.5  .12 .12 16 .078 0  
bitvector/parity.yml done .75  prog tests 2 inspect 26    26    27 350   0   0   unknown prog tests 0 inspect
75.0  91.3  .12 .12 16 .094 0  
bitvector/s3_clnt_1.BV.c.cil-1.yml done .698 prog tests 29 inspect 1.8  1.8  21 24   0   0   unknown prog tests 0 inspect
69.8  83.5  .32 .31 17 2.0   0  
bitvector/s3_clnt_1.BV.c.cil-2.yml done .722 prog tests 35 inspect 840    840    490 12000   0   0   true prog tests 1 inspect
72.2  85.5  .41 .43 17 2.3   0  
bitvector/s3_clnt_2.BV.c.cil-1.yml done .688 prog tests 24 inspect 1.7  1.7  20 28   0   0   unknown prog tests 0 inspect
68.8  83.0  .31 .30 17 1.6   0  
bitvector/s3_clnt_2.BV.c.cil-2.yml done .762 prog tests 30 inspect 840    840    120 8800   0   0   true prog tests 1 inspect
76.2  86.8  .41 .40 17 2.0   0  
bitvector/s3_clnt_3.BV.c.cil-1.yml done .691 prog tests 27 inspect 1.7  1.7  21 27   0   0   unknown prog tests 0 inspect
69.1  83.1  .30 .29 17 1.8   0  
bitvector/s3_clnt_3.BV.c.cil-2.yml done .568 prog tests 19 inspect 1.1  1.1  20 13   0   0   true prog tests 1 inspect
56.8  67.7  .36 .39 17 1.3   0  
bitvector/s3_srvr_1.BV.c.cil.yml done .718 prog tests 33 inspect 840    840    970 10000   0   0   unknown prog tests 0 inspect
71.8  77.6  .37 .35 17 2.6   0  
bitvector/s3_srvr_1_alt.BV.c.cil.yml done .0   prog tests 56 inspect 840    840    330 9200   0   0   unknown prog tests 0 inspect
.00 7.03 .47 .45 17 4.4   0  
bitvector/s3_srvr_3.BV.c.cil.yml done .724 prog tests 32 inspect 840    840    130 9800   0   0   unknown prog tests 0 inspect
72.4  79.8  .36 .36 17 2.4   0  
bitvector/s3_srvr_3_alt.BV.c.cil.yml done .736 prog tests 36 inspect 840    840    130 10000   0   0   unknown prog tests 0 inspect
73.6  80.4  .36 .35 17 2.7   0  
bitvector/soft_float_1-2.c.cil.yml done .608 prog tests 11 inspect 840    840    120 14000   0   0   unknown prog tests 0 inspect
60.8  65.1  .16 .16 17 .39  0  
bitvector/soft_float_1-3.c.cil.yml done .622 prog tests 13 inspect 840    840    130 11000   0   0   true prog tests 1 inspect
62.2  65.7  .17 .16 17 .44  0  
bitvector/soft_float_2.c.cil.yml done .458 prog tests 7 inspect 3.6  3.6  25 51   0   0   unknown prog tests 0 inspect
45.8  46.6  .15 .14 16 .24  0  
bitvector/soft_float_3.c.cil.yml done .562 prog tests 7 inspect 10    10    31 150   0   0   unknown prog tests 0 inspect
56.2  62.6  .14 .14 16 .24  0  
bitvector/soft_float_4-2.c.cil.yml done .595 prog tests 13 inspect 850    850    43 13000   0   0   unknown prog tests 0 inspect
59.5  64.6  .18 .17 17 .39  0  
bitvector/soft_float_4-3.c.cil.yml done .619 prog tests 13 inspect 850    850    49 12000   0   0   true prog tests 1 inspect
61.9  65.3  .17 .16 16 .39  0  
bitvector/soft_float_5.c.cil.yml done .479 prog tests 7 inspect 3.5  3.5  25 54   0   0   unknown prog tests 0 inspect
47.9  48.9  .15 .15 17 .24  0  
bitvector/sum02-1.yml done .5   prog tests 1 inspect 840    840    350 10000   0   0   unknown prog tests 0 inspect
50.0  88.9  .11 .12 16 .078 0  
bitvector/sum02-2.yml done .5   prog tests 1 inspect 840    840    360 12000   0   0   unknown prog tests 0 inspect
50.0  92.3  .11 .11 16 .078 0  
bitvector-regression/recHanoi03-1.yml done .875 prog tests 5 inspect 840    840    730 12000   0   0   true prog tests 1 inspect
87.5  100    .13 .13 16 .14  0  
bitvector-loops/diamond_2-1.yml done 1.0   prog tests 2 inspect .40 .40 18 5.0 0   0   true prog tests 1 inspect
100    100    .12 .12 16 .094 0  
bitvector-loops/verisec_sendmail_tTflag_arr_one_loop.yml done .875 prog tests 2 inspect .77 .77 20 11   0   0   true prog tests 1 inspect
87.5  100    .12 .14 16 .094 0  
sv-benchmarks/c/ status score program test-suite TS size inspect test-suite cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status program test-suite TS size inspect test-suite cov branch cov (%) line cov (%) cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 32 21.5 12000 12000 4600 160000 0   0   32 2150 2550 6.6 6.6 530 27 0  
Run set symbiotic.test-comp19_prop-coverage-branches.ReachSafety-BitVectors tbf-testsuite-validator-symbiotic.test-comp19_prop-coverage-branches.ReachSafety-BitVectors