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-Floats tbf-testsuite-validator-symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Floats
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)
floats-cdfpl/newton_1_4.yml .42 .42 18 5.0 0     0   0   0   .065 .065 9.0 0     0  
floats-cdfpl/newton_1_5.yml .44 .44 18 4.6 0     0   0   0   .070 .073 8.9 0     0  
floats-cdfpl/newton_1_6.yml .42 .42 19 5.2 0     0   0   0   .060 .061 9.0 0     0  
floats-cdfpl/newton_1_7.yml .44 .44 18 5.2 0     0   0   0   .059 .059 9.0 0     0  
floats-cdfpl/newton_1_8.yml .43 .43 18 4.9 0     0   0   0   .059 .064 9.0 0     0  
floats-cdfpl/newton_2_6.yml .42 .42 18 5.5 0     0   0   0   .058 .072 8.9 0     0  
floats-cdfpl/newton_2_7.yml .45 .45 19 5.2 0     0   0   0   .056 .059 9.0 0     0  
floats-cdfpl/newton_2_8.yml .43 .43 18 5.0 0     0   0   0   .058 .059 9.0 0     0  
floats-cdfpl/newton_3_6.yml .43 .42 19 5.3 0     0   0   0   .061 .062 9.0 0     0  
floats-cdfpl/newton_3_7.yml .44 .43 18 6.3 0     0   0   0   .057 .058 9.0 0     0  
floats-cdfpl/newton_3_8.yml .43 .43 19 6.1 0     0   0   0   .061 .062 8.9 0     0  
floats-cdfpl/sine_1.yml .42 .42 19 5.0 0     0   0   0   .061 .061 9.0 0     0  
floats-cdfpl/sine_2.yml .41 .41 19 4.5 0     0   0   0   .055 .056 9.0 0     0  
floats-cdfpl/sine_3.yml .41 .41 19 5.1 0     0   0   0   .059 .060 9.0 0     0  
floats-cdfpl/square_1.yml .41 .41 19 5.5 0     0   0   0   .057 .058 9.0 0     0  
floats-cdfpl/square_2.yml .40 .39 19 4.5 0     0   0   0   .062 .062 9.0 0     0  
floats-cdfpl/square_3.yml .39 .39 18 4.9 0     0   0   0   .066 .067 9.0 0     0  
float-benchs/cast_float_ptr.yml .39 .39 19 4.9 0     0   0   0   .058 .059 9.0 0     0  
float-benchs/cast_union_loose.yml .45 .45 19 5.7 0     0   0   0   .060 .061 9.0 0     0  
float-benchs/cast_union_tight.yml .41 .40 18 5.8 0     0   0   0   .058 .059 9.0 0     0  
float-benchs/float_int_inv_square.yml 1 .54 .53 21 7.4 0     0   50.0 75.0 .11  .11  16   .078 0  
float-benchs/inv_Newton-2.yml .44 .44 19 5.7 0     0   0   0   .070 .071 9.0 0     0  
float-benchs/inv_Newton.c.p+cfa-reducer.yml .41 .41 18 5.1 0     0   0   0   .061 .094 9.0 0     0  
float-benchs/inv_square-1.yml .41 .41 18 5.8 0     0   0   0   .057 .058 8.9 0     0  
float-benchs/nan_double.yml .36 .35 18 5.0 0     0   0   0   .057 .058 9.0 0     0  
float-benchs/nan_float.yml .36 .36 18 4.6 0     0   0   0   .060 .061 9.0 0     0  
float-benchs/sin_interpolated_index-1.yml .51 .51 18 5.5 0     0   0   0   .060 .061 9.0 0     0  
float-benchs/sqrt_poly2.yml .46 .46 18 7.5 0     0   0   0   .059 .060 9.0 0     0  
float-newlib/double_req_bl_0870a.yml 1.4  1.4  20 19   0     0   0   0   .090 .091 8.8 0     0  
float-newlib/float_req_bl_0870a.yml 1.3  1.3  19 18   0     0   0   0   .057 .057 8.9 0     0  
loop-floats-scientific-comp/loop1-2.yml 900    900    61 9500   .016 0   0   0   .061 .061 9.0 0     0  
loop-floats-scientific-comp/loop2-1.yml .49 .49 19 6.1 0     0   0   0   .061 .062 9.0 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 32 1 920 920 640 9700 .016 0   32 50.0 75.0 2.0 2.1 290 .078 0  
Run set symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Floats tbf-testsuite-validator-symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Floats