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-Heap tbf-testsuite-validator-symbiotic.test-comp19_prop-coverage-branches.ReachSafety-Heap
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/ldv-regression/ 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)
alias_of_return_2.c_1.yml .25  .29 .29 16 3.8 0   0   25.0 45.5 .14 .14 16 .078 0  
alias_of_return_2.yml .5   .30 .30 16 3.9 0   0   50.0 72.7 .12 .12 16 .078 0  
fo_test.yml 1.0   .37 .37 18 5.2 0   0   100   100   .15 .15 16 .14  0  
rule60_list2.c_1.yml .857 .49 .49 19 5.4 0   0   85.7 100   .15 .16 17 .22  0  
rule60_list2.yml .786 .44 .44 18 5.7 0   0   78.6 92.9 .14 .14 17 .22  0  
sizeofparameters_test.yml .5   .32 .32 16 4.1 0   0   50.0 80.0 .13 .14 17 .078 0  
test10.yml .5   .31 .30 16 2.7 0   0   50.0 95.5 .11 .14 16 .078 0  
test11.yml .5   .34 .34 17 3.7 0   0   50.0 86.7 .12 .13 16 .078 0  
test14.yml .5   .33 .33 17 3.7 0   0   50.0 91.7 .12 .12 16 .078 0  
test15.yml .5   .30 .30 16 3.3 0   0   50.0 80.0 .11 .11 17 .078 0  
test19.yml .5   .33 .33 17 3.3 0   0   50.0 85.7 .12 .12 17 .078 0  
test21-1.yml .75  .57 .56 19 6.7 0   0   75.0 88.9 .12 .12 16 .11  0  
test21-2.yml .875 .59 .59 19 8.9 0   0   87.5 100   .14 .15 17 .11  0  
test22-1.yml .833 .63 .63 19 7.2 0   0   83.3 91.3 .13 .12 16 .13  0  
test22-2.yml .917 .88 .88 19 12   0   0   91.7 100   .16 .19 16 .15  0  
test23-1.yml .714 1.1  1.1  27 18   0   0   71.4 100   .13 .13 16 .098 0  
test23-2.yml .714 .62 .62 20 8.1 0   0   71.4 91.7 .12 .12 17 .11  0  
test24-1.yml .75  .34 .34 19 3.8 0   0   75.0 86.7 .12 .12 16 .094 0  
test24-2.yml .8   .41 .41 23 5.0 0   0   80.0 94.4 .13 .13 16 .11  0  
test25-1.yml .917 .41 .41 22 5.3 0   0   91.7 100   .12 .12 16 .13  0  
test25-2.yml .833 .37 .37 21 4.4 0   0   83.3 88.9 .12 .12 16 .11  0  
test28-1.yml .875 .46 .46 19 5.8 0   0   87.5 100   .11 .11 16 .086 0  
test28-2.yml .875 .46 .46 19 5.2 0   0   87.5 80.0 .12 .12 16 .086 0  
test29-1.yml 1.0   .32 .32 18 3.9 0   0   100   100   .12 .12 16 .11  0  
test29-2.yml .875 .34 .34 18 4.0 0   0   87.5 80.0 .11 .13 16 .086 0  
sv-benchmarks/c/ldv-regression/ 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 25 18.1 11 11 470 140 0   0   25 1810 2230 3.2 3.3 410 2.7 0  
Run set symbiotic.test-comp19_prop-coverage-branches.ReachSafety-Heap tbf-testsuite-validator-symbiotic.test-comp19_prop-coverage-branches.ReachSafety-Heap