Benchmark ESBMC-falsif TBF Test-Suite Validator
Tool ESBMC version 6.0.0 64-bit x86_64 linux 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-05 21:11:17 CET 2019-02-06 06:16:01 CET
Run set esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Floats tbf-testsuite-validator-esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Floats
Options -s falsi --verbose --sequence-file cov-seq.txt -r --stop-after-found-violation --test-suite ../../results-verified/esbmc-falsi.2019-02-05_2111.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 false(unreach-call) prog tests 1 inspect 25     25     93 330    1.0 0   unknown prog tests 0 inspect
.00 18.2  .12  .12  16   .094 0  
floats-cdfpl/newton_1_5.yml false(unreach-call) prog tests 1 inspect 33     33     93 420    1.0 0   unknown prog tests 0 inspect
.00 18.2  .12  .12  16   .094 0  
floats-cdfpl/newton_1_6.yml false(unreach-call) prog tests 1 inspect 41     41     92 530    1.0 0   unknown prog tests 0 inspect
.00 18.2  .12  .12  16   .094 0  
floats-cdfpl/newton_1_7.yml false(unreach-call) prog tests 1 inspect 8.9   8.9   92 110    1.0 0   unknown prog tests 0 inspect
.00 18.2  .12  .13  16   .094 0  
floats-cdfpl/newton_1_8.yml false(unreach-call) prog tests 1 inspect 39     39     93 500    1.0 0   unknown prog tests 0 inspect
.00 18.2  .12  .12  16   .094 0  
floats-cdfpl/newton_2_6.yml false(unreach-call) prog tests 1 inspect 130     130     190 1900    1.0 0   unknown prog tests 0 inspect
.00 16.7  .12  .12  16   .094 0  
floats-cdfpl/newton_2_7.yml false(unreach-call) prog tests 1 inspect 120     120     190 1400    1.0 0   unknown prog tests 0 inspect
.00 16.7  .12  .12  16   .094 0  
floats-cdfpl/newton_2_8.yml false(unreach-call) prog tests 1 inspect 60     60     190 770    1.0 0   unknown prog tests 0 inspect
.00 16.7  .13  .14  16   .053 0  
floats-cdfpl/newton_3_6.yml false(unreach-call) prog tests 1 inspect 100     100     290 1200    1.0 0   unknown prog tests 0 inspect
.00 15.4  .12  .12  16   .098 0  
floats-cdfpl/newton_3_7.yml false(unreach-call) prog tests 1 inspect 120     120     280 1400    1.0 0   unknown prog tests 0 inspect
.00 15.4  .13  .13  16   .098 0  
floats-cdfpl/newton_3_8.yml false(unreach-call) prog tests 1 inspect 130     130     300 1600    1.0 0   unknown prog tests 0 inspect
.00 15.4  .12  .12  17   .098 0  
floats-cdfpl/sine_1.yml false(unreach-call) prog tests 1 inspect 20     20     65 240    1.0 0   unknown prog tests 0 inspect
.00 25.0  .12  .12  16   .094 0  
floats-cdfpl/sine_2.yml false(unreach-call) prog tests 1 inspect 20     20     64 260    1.0 0   unknown prog tests 0 inspect
.00 25.0  .12  .12  17   .094 0  
floats-cdfpl/sine_3.yml false(unreach-call) prog tests 1 inspect 19     19     64 250    1.0 0   unknown prog tests 0 inspect
.00 25.0  .12  .12  16   .094 0  
floats-cdfpl/square_1.yml false(unreach-call) prog tests 1 inspect 4.7   4.7   54 59    1.0 0   unknown prog tests 0 inspect
.00 22.2  .11  .11  16   .094 0  
floats-cdfpl/square_2.yml false(unreach-call) prog tests 1 inspect 6.8   6.8   60 81    1.0 0   unknown prog tests 0 inspect
.00 22.2  .12  .12  16   .094 0  
floats-cdfpl/square_3.yml false(unreach-call) prog tests 1 inspect 7.5   7.5   54 92    1.0 0   unknown prog tests 0 inspect
.00 22.2  .12  .12  16   .094 0  
float-benchs/cast_float_ptr.yml false(unreach-call) 1 prog tests 1 inspect .10  .10  26 1.2  1.0 0   true prog tests 1 inspect
41.7  68.8  .12  .12  16   .094 0  
float-benchs/cast_union_loose.yml false(unreach-call) 1 prog tests 1 inspect .15  .15  26 1.8  1.0 0   true prog tests 1 inspect
40.0  92.3  .12  .12  16   .094 0  
float-benchs/cast_union_tight.yml false(unreach-call) 1 prog tests 1 inspect .16  .17  27 1.5  1.0 0   true prog tests 1 inspect
50.0  91.7  .12  .12  16   .078 0  
float-benchs/float_int_inv_square.yml false(unreach-call) 1 prog tests 1 inspect .36  .37  28 4.9  1.0 0   true prog tests 1 inspect
50.0  75.0  .12  .13  16   .078 0  
float-benchs/inv_Newton-2.yml timeout prog tests 0 inspect 900     900     300 10000    1.0 0   error (0) prog tests 0 inspect
0    0    .061 .062 9.0 0     0  
float-benchs/inv_Newton.c.p+cfa-reducer.yml timeout prog tests 0 inspect 900     900     1300 8700    1.0 0   error (0) prog tests 0 inspect
0    0    .060 .061 8.9 0     0  
float-benchs/inv_square-1.yml false(unreach-call) prog tests 1 inspect .33  .34  28 4.4  1.0 0   unknown prog tests 0 inspect
.00 22.2  .12  .14  17   .094 0  
float-benchs/nan_double.yml false(unreach-call) 1 prog tests 1 inspect .082 .082 26 .95 1.0 0   true prog tests 1 inspect
50.0  80.0  .12  .14  16   .094 0  
float-benchs/nan_float.yml false(unreach-call) 1 prog tests 1 inspect .085 .086 26 1.0  1.0 0   true prog tests 1 inspect
50.0  80.0  .12  .12  16   .094 0  
float-benchs/sin_interpolated_index-1.yml false(unreach-call) prog tests 1 inspect 9.1   9.1   100 110    1.0 0   unknown prog tests 0 inspect
.00 8.70 .13  .15  17   .13  0  
float-benchs/sqrt_poly2.yml false(unreach-call) prog tests 1 inspect 58     58     150 800    1.0 0   unknown prog tests 0 inspect
.00 10.5  .12  .14  16   .078 0  
float-newlib/double_req_bl_0870a.yml false(unreach-call) prog tests 1 inspect .25  .25  40 3.0  1.0 0   unknown prog tests 0 inspect
.00 .60 .15  .15  17   .19  0  
float-newlib/float_req_bl_0870a.yml false(unreach-call) prog tests 1 inspect .20  .20  32 2.1  1.0 0   unknown prog tests 0 inspect
.00 .60 .15  .15  17   .18  0  
loop-floats-scientific-comp/loop1-2.yml false(unreach-call) prog tests 1 inspect 1.6   1.6   46 22    1.0 0   unknown prog tests 0 inspect
.00 14.3  .12  .12  16   .094 0  
loop-floats-scientific-comp/loop2-1.yml false(unreach-call) prog tests 1 inspect 1.3   1.3   42 16    1.0 0   unknown prog tests 0 inspect
.00 9.52 .12  .12  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 6 2800    2800    4400 31000 33   0   32 282 883 3.8 3.9 510 3.0 0  
Run set esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Floats tbf-testsuite-validator-esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Floats