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-error-call.ReachSafety-BitVectors tbf-testsuite-validator-symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors
Options --test-comp --verifier klee-testcomp --verbose --sequence-file cov-seq.txt -r --stop-after-found-violation --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 1 1.1  1.1  20 13   0     0   60.0  73.4  .14  .14  16   .086 0  
bitvector/s3_clnt_1.BV.c.cil-2.yml 2.9  2.9  22 44   0     0   .62 10.9  .19  .19  17   .12  0  
bitvector/s3_clnt_2.BV.c.cil-2.yml 3.3  3.3  22 46   0     0   .00 8.68 .20  .21  17   .074 0  
bitvector/s3_clnt_3.BV.c.cil-2.yml 1.8  1.8  20 25   0     0   .00 6.53 .19  .19  17   .12  0  
bitvector/soft_float_1-3.c.cil.yml 1 1.8  1.8  21 28   0     0   20.3  33.7  .16  .22  17   .098 0  
bitvector/soft_float_4-3.c.cil.yml 1 1.7  1.7  21 24   0     0   19.1  30.7  .13  .13  16   .090 0  
bitvector/sum02-1.yml 900    900    400 13000   .025 0   0    0    .057 .058 9.0 0     0  
bitvector-regression/recHanoi03-1.yml 900    900    730 13000   .020 0   0    0    .061 .061 9.0 0     0  
bitvector-loops/diamond_2-1.yml 1 .63 .62 19 7.6 0     0   54.2  96.5  .12  .12  16   .078 0  
bitvector-loops/verisec_sendmail_tTflag_arr_one_loop.yml 1 .97 .97 20 13   0     0   75.0  89.5  .12  .13  16   .078 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 10 5 1800 1800 1300 27000 .045 0   10 229 350 1.4 1.5 150 .74 0  
Run set symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors tbf-testsuite-validator-symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors