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-ControlFlow tbf-testsuite-validator-symbiotic.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow
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)
ntdrivers-simplified/cdaudio_simpl1.cil-1.yml done .688 prog tests 79 inspect 2.4  2.4  25 31   0   0   true prog tests 1 inspect
68.8  85.9 .70 .74 21 11    0  
ntdrivers-simplified/cdaudio_simpl1.cil-2.yml done .686 prog tests 75 inspect 2.4  2.4  24 31   0   0   unknown prog tests 0 inspect
68.6  85.7 .62 .64 20 10    0  
ntdrivers-simplified/diskperf_simpl1.cil.yml done .630 prog tests 27 inspect 1.5  1.5  22 19   0   0   unknown prog tests 0 inspect
63.0  82.6 .29 .27 18 2.0  0  
ntdrivers-simplified/floppy_simpl3.cil-1.yml done .716 prog tests 25 inspect 1.4  1.4  21 19   0   0   true prog tests 1 inspect
71.6  87.6 .30 .30 18 1.9  0  
ntdrivers-simplified/floppy_simpl3.cil-2.yml done .716 prog tests 26 inspect 1.4  1.4  21 19   0   0   unknown prog tests 0 inspect
71.6  86.0 .28 .26 18 1.9  0  
ntdrivers-simplified/floppy_simpl4.cil-1.yml done .740 prog tests 48 inspect 2.1  2.1  23 27   0   0   true prog tests 1 inspect
74.0  88.0 .47 .49 20 5.1  0  
ntdrivers-simplified/floppy_simpl4.cil-2.yml done .744 prog tests 45 inspect 2.1  2.1  23 29   0   0   unknown prog tests 0 inspect
74.4  88.2 .42 .47 20 4.7  0  
ntdrivers-simplified/kbfiltr_simpl1.cil.yml done .55  prog tests 7 inspect .70 .69 19 9.7 0   0   unknown prog tests 0 inspect
55.0  79.4 .17 .18 17 .40 0  
ntdrivers-simplified/kbfiltr_simpl2.cil-1.yml done .563 prog tests 17 inspect 1.1  1.1  20 15   0   0   unknown prog tests 0 inspect
56.3  78.3 .23 .24 17 1.3  0  
ntdrivers-simplified/kbfiltr_simpl2.cil-2.yml done .568 prog tests 18 inspect 1.1  1.1  20 13   0   0   true prog tests 1 inspect
56.8  78.8 .27 .27 18 1.4  0  
ssh-simplified/s3_clnt_1.cil-1.yml done .704 prog tests 22 inspect 1.7  1.7  20 22   0   0   unknown prog tests 0 inspect
70.4  83.7 .29 .28 17 1.5  0  
ssh-simplified/s3_clnt_1.cil-2.yml done .710 prog tests 23 inspect 1.7  1.7  20 22   0   0   true prog tests 1 inspect
71.0  84.3 .36 .36 17 1.6  0  
ssh-simplified/s3_clnt_2.cil-1.yml done .710 prog tests 24 inspect 1.6  1.6  20 21   0   0   true prog tests 1 inspect
71.0  85.2 .36 .34 17 1.6  0  
ssh-simplified/s3_clnt_2.cil-2.yml done .704 prog tests 24 inspect 1.7  1.7  20 25   0   0   unknown prog tests 0 inspect
70.4  84.6 .30 .32 17 1.6  0  
ssh-simplified/s3_clnt_3.cil-1.yml done .025 prog tests 1 inspect .56 .56 16 7.1 0   0   unknown prog tests 0 inspect
2.50 13.5 .20 .20 17 .11 0  
ssh-simplified/s3_clnt_3.cil-2.yml done .759 prog tests 30 inspect 2.1  2.1  21 30   0   0   true prog tests 1 inspect
75.9  88.8 .43 .46 17 2.0  0  
ssh-simplified/s3_clnt_3.cil-3.yml done .704 prog tests 22 inspect 1.7  1.7  20 25   0   0   unknown prog tests 0 inspect
70.4  84.1 .31 .30 17 1.5  0  
ssh-simplified/s3_clnt_4.cil-1.yml done .704 prog tests 24 inspect 1.6  1.6  20 20   0   0   unknown prog tests 0 inspect
70.4  84.6 .30 .29 17 1.6  0  
ssh-simplified/s3_clnt_4.cil-2.yml done .759 prog tests 30 inspect 2.0  2.0  20 29   0   0   true prog tests 1 inspect
75.9  88.4 .39 .44 17 2.0  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 19 12.4 31 31 400 410 0   0   19 1240 1540 6.7 6.8 340 53 0  
Run set symbiotic.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow tbf-testsuite-validator-symbiotic.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow