| Benchmark | CPA/CoVeriTest | CPA/Tiger-MGP | ESBMC-bkind | ESBMC-falsif | FairFuzz | KLEE | PRtest | Symbiotic | VeriFuzz | ||||||||||||||||||||||||||||||||||||
| Tool | CPAchecker 1.8-svn 30375 | CPAchecker 1.8-svn 30541M | ESBMC version 6.0.0 64-bit x86_64 linux | FairFuzz TC-0.0.2 | KLEE 2.0.0-pre-test-comp | tbf v0.3.0-testcomp19 | symbiotic 6.0.3-dev-fd3f777b | VeriFuzz 1.0.1 | |||||||||||||||||||||||||||||||||||||
| Limits | timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 | ||||||||||||||||||||||||||||||||||||||||||||
| 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:05:56 CET | 2019-02-05 21:13:54 CET | 2019-02-05 21:13:25 CET | 2019-02-05 21:11:17 CET | 2019-02-08 09:39:09 CET | 2019-02-05 21:09:47 CET | 2019-02-06 06:02:44 CET | 2019-02-06 07:07:32 CET | 2019-02-06 07:17:17 CET | ||||||||||||||||||||||||||||||||||||
| Run set | coveritest.test-comp19_prop-coverage-error-call.ReachSafety-Floats | cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Floats | esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Floats | esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Floats | fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Floats | klee.test-comp19_prop-coverage-error-call.ReachSafety-Floats | prtest.test-comp19_prop-coverage-error-call.ReachSafety-Floats | symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Floats | verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Floats | ||||||||||||||||||||||||||||||||||||
| Options | -benchmark -heap 10000M -testcomp19 | -benchmark -heap 10000M -tigertestcomp19 | -s kinduction | -s falsi | --stats -i random --write-xml --svcomp-nondets | --test-comp --verifier klee-testcomp | --testcomp | ||||||||||||||||||||||||||||||||||||||
| ../sv-benchmarks/c/ | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) |
| floats-cdfpl/newton_1_4.yml | done | 1 | 94 | 380 | 610 | unknown | 1 | 76 | 370 | 580 | false(unreach-call) | 25 | 92 | 310 | false(unreach-call) | 25 | 93 | 330 | timeout | 900 | 11 | 12000 | done | .11 | 21 | 1.3 | unknown | 1 | .27 | 31 | 2.7 | unknown | .42 | 18 | 5.0 | done | 1 | 10 | 150 | 120 | |||||
| floats-cdfpl/newton_1_5.yml | done | 1 | 77 | 370 | 540 | unknown | 1 | 56 | 370 | 560 | false(unreach-call) | 33 | 92 | 400 | false(unreach-call) | 33 | 93 | 420 | timeout | 900 | 10 | 12000 | done | .11 | 21 | 1.4 | unknown | 1 | .25 | 31 | 3.0 | unknown | .44 | 18 | 4.6 | done | 1 | 7.3 | 150 | 71 | |||||
| floats-cdfpl/newton_1_6.yml | done | 1 | 64 | 370 | 630 | unknown | 1 | 45 | 370 | 340 | false(unreach-call) | 41 | 94 | 570 | false(unreach-call) | 41 | 92 | 530 | timeout | 900 | 10 | 12000 | done | .12 | 21 | 1.0 | unknown | 1 | .24 | 31 | 3.5 | unknown | .42 | 19 | 5.2 | done | 1 | 7.9 | 150 | 79 | |||||
| floats-cdfpl/newton_1_7.yml | done | 1 | 41 | 370 | 330 | unknown | 1 | 22 | 380 | 180 | false(unreach-call) | 8.8 | 93 | 120 | false(unreach-call) | 8.9 | 92 | 110 | timeout | 900 | 10 | 10000 | done | .13 | 21 | 1.4 | unknown | 1 | .27 | 30 | 4.7 | unknown | .44 | 18 | 5.2 | done | 1 | 6.9 | 150 | 89 | |||||
| floats-cdfpl/newton_1_8.yml | done | 1 | 36 | 380 | 290 | unknown | 1 | 16 | 360 | 120 | false(unreach-call) | 39 | 92 | 490 | false(unreach-call) | 39 | 93 | 500 | timeout | 900 | 10 | 12000 | done | .12 | 21 | 2.0 | unknown | 1 | .26 | 31 | 3.0 | unknown | .43 | 18 | 4.9 | done | 1 | 6.9 | 150 | 83 | |||||
| floats-cdfpl/newton_2_6.yml | done | 1 | 160 | 480 | 1100 | unknown | 1 | 130 | 470 | 970 | false(unreach-call) | 130 | 190 | 1700 | false(unreach-call) | 130 | 190 | 1900 | timeout | 900 | 10 | 14000 | done | .15 | 21 | 1.0 | unknown | 1 | .24 | 30 | 3.2 | unknown | .42 | 18 | 5.5 | done | 1 | 42 | 150 | 370 | |||||
| floats-cdfpl/newton_2_7.yml | done | 1 | 100 | 480 | 760 | unknown | 1 | 84 | 460 | 600 | false(unreach-call) | 130 | 190 | 1500 | false(unreach-call) | 120 | 190 | 1400 | timeout | 900 | 10 | 13000 | done | .12 | 21 | 1.2 | unknown | 1 | .24 | 31 | 3.5 | unknown | .45 | 19 | 5.2 | done | 1 | 26 | 150 | 270 | |||||
| floats-cdfpl/newton_2_8.yml | done | 1 | 62 | 470 | 600 | unknown | 1 | 43 | 460 | 360 | false(unreach-call) | 60 | 190 | 830 | false(unreach-call) | 60 | 190 | 770 | timeout | 1 | 900 | 11 | 12000 | done | .12 | 21 | 1.4 | unknown | 1 | .26 | 31 | 2.8 | unknown | .43 | 18 | 5.0 | done | 1 | 19 | 150 | 190 | ||||
| floats-cdfpl/newton_3_6.yml | done | 1 | 310 | 600 | 2300 | unknown | 1 | 290 | 570 | 2500 | false(unreach-call) | 100 | 290 | 1200 | false(unreach-call) | 100 | 290 | 1200 | timeout | 900 | 10 | 14000 | done | .12 | 21 | 1.2 | unknown | 1 | .27 | 31 | 3.2 | unknown | .43 | 19 | 5.3 | done | 1 | 320 | 220 | 3900 | |||||
| floats-cdfpl/newton_3_7.yml | done | 1 | 220 | 600 | 1900 | unknown | 1 | 200 | 570 | 1300 | false(unreach-call) | 120 | 280 | 1400 | false(unreach-call) | 120 | 280 | 1400 | timeout | 900 | 10 | 14000 | done | .13 | 21 | 1.1 | unknown | 1 | .26 | 31 | 3.2 | unknown | .44 | 18 | 6.3 | done | 1 | 74 | 230 | 940 | |||||
| floats-cdfpl/newton_3_8.yml | done | 1 | 190 | 600 | 1300 | unknown | 1 | 160 | 570 | 1400 | false(unreach-call) | 130 | 300 | 1600 | false(unreach-call) | 130 | 300 | 1600 | timeout | 900 | 10 | 12000 | done | .12 | 21 | 1.4 | unknown | 1 | .26 | 31 | 5.0 | unknown | .43 | 19 | 6.1 | done | 1 | 36 | 200 | 360 | |||||
| floats-cdfpl/sine_1.yml | done | 1 | 29 | 340 | 290 | unknown | 1 | 8.7 | 330 | 91 | false(unreach-call) | 20 | 65 | 230 | false(unreach-call) | 20 | 65 | 240 | timeout | 1 | 900 | 10 | 12000 | done | .14 | 21 | 1.1 | unknown | 1 | .25 | 30 | 3.1 | unknown | .42 | 19 | 5.0 | done | 1 | 5.2 | 150 | 51 | ||||
| floats-cdfpl/sine_2.yml | done | 1 | 66 | 350 | 590 | unknown | 1 | 44 | 360 | 360 | false(unreach-call) | 20 | 63 | 270 | false(unreach-call) | 20 | 64 | 260 | timeout | 1 | 900 | 10 | 13000 | done | .12 | 21 | 1.8 | unknown | 1 | .28 | 31 | 3.1 | unknown | .41 | 19 | 4.5 | done | 1 | 4.6 | 150 | 59 | ||||
| floats-cdfpl/sine_3.yml | done | 1 | 300 | 450 | 2800 | unknown | 1 | 280 | 440 | 2700 | false(unreach-call) | 19 | 64 | 260 | false(unreach-call) | 19 | 64 | 250 | timeout | 900 | 10 | 11000 | done | .14 | 21 | 1.2 | unknown | 1 | .25 | 31 | 2.5 | unknown | .41 | 19 | 5.1 | done | 1 | 5.6 | 150 | 63 | |||||
| floats-cdfpl/square_1.yml | done | 1 | 37 | 1500 | 400 | unknown | 1 | 18 | 350 | 150 | false(unreach-call) | 4.7 | 57 | 60 | false(unreach-call) | 4.7 | 54 | 59 | timeout | 900 | 10 | 13000 | done | .13 | 21 | 1.1 | unknown | 1 | .31 | 31 | 3.3 | unknown | .41 | 19 | 5.5 | done | 1 | 9.6 | 150 | 120 | |||||
| floats-cdfpl/square_2.yml | done | 1 | 200 | 1600 | 2100 | unknown | 1 | 180 | 510 | 1500 | false(unreach-call) | 6.8 | 55 | 85 | false(unreach-call) | 6.8 | 60 | 81 | timeout | 900 | 11 | 11000 | done | .12 | 21 | 1.1 | unknown | 1 | 1.3 | 31 | 15 | unknown | .40 | 19 | 4.5 | done | 1 | 22 | 150 | 250 | |||||
| floats-cdfpl/square_3.yml | done | 1 | 82 | 1500 | 750 | unknown | 1 | 61 | 360 | 440 | false(unreach-call) | 7.5 | 55 | 99 | false(unreach-call) | 7.5 | 54 | 92 | timeout | 900 | 10 | 13000 | done | .14 | 21 | .98 | unknown | 1 | 8.0 | 31 | 91 | unknown | .39 | 18 | 4.9 | done | 1 | 12 | 150 | 170 | |||||
| float-benchs/cast_float_ptr.yml | done | 3.4 | 270 | 33 | unknown | 2.8 | 270 | 27 | false(unreach-call) | 1 | .11 | 26 | 1.0 | false(unreach-call) | 1 | .10 | 26 | 1.2 | false(unreach-call) | 1 | 13 | 15 | 60 | done | .13 | 21 | 1.5 | unknown | .25 | 31 | 3.6 | unknown | .39 | 19 | 4.9 | done | 1 | 3.8 | 150 | 43 | |||||
| float-benchs/cast_union_loose.yml | done | 3.7 | 280 | 40 | unknown | 3.2 | 280 | 29 | false(unreach-call) | 1 | .15 | 26 | 1.9 | false(unreach-call) | 1 | .15 | 26 | 1.8 | timeout | 1 | 900 | 11 | 14000 | done | .13 | 21 | 1.4 | unknown | 1 | 3.3 | 31 | 40 | unknown | .45 | 19 | 5.7 | done | 1 | 3.7 | 150 | 39 | ||||
| float-benchs/cast_union_tight.yml | done | 3.8 | 270 | 40 | unknown | 3.2 | 290 | 30 | false(unreach-call) | 1 | .17 | 27 | 1.7 | false(unreach-call) | 1 | .16 | 27 | 1.5 | false(unreach-call) | 1 | 9.4 | 16 | 27 | done | .13 | 21 | 1.2 | unknown | 1 | .25 | 30 | 3.1 | unknown | .41 | 18 | 5.8 | done | 1 | 3.6 | 150 | 30 | ||||
| float-benchs/float_int_inv_square.yml | done | 1 | 3.6 | 280 | 35 | unknown | 1 | 2.9 | 280 | 28 | false(unreach-call) | 1 | .36 | 28 | 4.4 | false(unreach-call) | 1 | .36 | 28 | 4.9 | timeout | 1 | 900 | 11 | 11000 | done | .16 | 21 | 1.4 | timeout | 900 | 31 | 9900 | done | 1 | .54 | 21 | 7.4 | done | 1 | 3.7 | 150 | 39 | ||
| float-benchs/inv_Newton-2.yml | done | 6.1 | 350 | 63 | unknown | 3.0 | 270 | 30 | timeout | 900 | 300 | 12000 | timeout | 900 | 300 | 10000 | couldn't run: all seeds time out or crash | 3.1 | 11 | 42 | done | .11 | 21 | 2.3 | unknown | .25 | 31 | 3.0 | unknown | .44 | 19 | 5.7 | done | 1 | 5.0 | 150 | 55 | ||||||||
| float-benchs/inv_Newton.c.p+cfa-reducer.yml | done | 1 | 6.8 | 350 | 74 | unknown | 4.4 | 350 | 47 | done | 470 | 530 | 4100 | timeout | 900 | 1300 | 8700 | done | 16 | 15 | 56 | done | .11 | 21 | 1.3 | unknown | .27 | 31 | 3.2 | unknown | .41 | 18 | 5.1 | done | 1 | 4.5 | 150 | 47 | |||||||
| float-benchs/inv_square-1.yml | done | 1 | 3.4 | 270 | 34 | unknown | 1 | 3.0 | 280 | 31 | false(unreach-call) | .30 | 28 | 3.9 | false(unreach-call) | .33 | 28 | 4.4 | false(unreach-call) | 740 | 11 | 9200 | done | .13 | 21 | 1.3 | unknown | 1 | .26 | 31 | 2.6 | unknown | .41 | 18 | 5.8 | timeout | 900 | 150 | 11000 | ||||||
| float-benchs/nan_double.yml | done | 3.4 | 270 | 31 | unknown | 2.8 | 270 | 23 | false(unreach-call) | 1 | .085 | 26 | 1.1 | false(unreach-call) | 1 | .082 | 26 | .95 | false(unreach-call) | 1 | 20 | 16 | 120 | done | .13 | 21 | 1.1 | unknown | .25 | 31 | 3.5 | unknown | .36 | 18 | 5.0 | done | 1 | 3.4 | 150 | 36 | |||||
| float-benchs/nan_float.yml | done | 3.2 | 260 | 31 | unknown | 3.1 | 280 | 31 | false(unreach-call) | 1 | .088 | 26 | .98 | false(unreach-call) | 1 | .085 | 26 | 1.0 | false(unreach-call) | 1 | 19 | 16 | 89 | done | .12 | 21 | 2.4 | unknown | 1 | .26 | 31 | 2.9 | unknown | .36 | 18 | 4.6 | done | 1 | 3.6 | 150 | 36 | ||||
| float-benchs/sin_interpolated_index-1.yml | done | 1 | 25 | 570 | 220 | unknown | 1 | 4.8 | 360 | 44 | false(unreach-call) | 9.1 | 100 | 110 | false(unreach-call) | 9.1 | 100 | 110 | done | 890 | 10 | 11000 | done | .12 | 21 | 1.4 | timeout | 900 | 31 | 12000 | unknown | .51 | 18 | 5.5 | done | 1 | 6.9 | 280 | 82 | ||||||
| float-benchs/sqrt_poly2.yml | done | 1 | 15 | 440 | 120 | unknown | 1 | 11 | 430 | 100 | false(unreach-call) | 58 | 150 | 580 | false(unreach-call) | 58 | 150 | 800 | couldn't run: all seeds time out or crash | 3.1 | 11 | 48 | done | .14 | 21 | 1.2 | unknown | .24 | 31 | 3.6 | unknown | .46 | 18 | 7.5 | done | 1 | 4.0 | 150 | 44 | ||||||
| float-newlib/double_req_bl_0870a.yml | exception | 6.9 | 460 | 63 | unknown | 5.4 | 360 | 47 | false(unreach-call) | .24 | 40 | 2.6 | false(unreach-call) | .25 | 40 | 3.0 | false(unreach-call) | 1 | 44 | 17 | 110 | done | .15 | 21 | 1.6 | timeout | 900 | 31 | 13000 | unknown | 1.4 | 20 | 19 | done | 1 | 590 | 170 | 7600 | |||||||
| float-newlib/float_req_bl_0870a.yml | done | 1 | 350 | 2700 | 3200 | unknown | 4.9 | 300 | 42 | false(unreach-call) | .20 | 32 | 2.4 | false(unreach-call) | .20 | 32 | 2.1 | done | 11 | 15 | 41 | done | .15 | 21 | 1.4 | unknown | 1 | 350 | 31 | 5300 | unknown | 1.3 | 19 | 18 | done | 1 | 130 | 170 | 1700 | ||||||
| loop-floats-scientific-comp/loop1-2.yml | done | 1 | 4.2 | 300 | 40 | unknown | 1 | 3.5 | 300 | 36 | false(unreach-call) | 1.6 | 46 | 18 | false(unreach-call) | 1.6 | 46 | 22 | false(unreach-call) | 1 | 70 | 18 | 340 | timeout | 900 | 75 | 11000 | unknown | 1 | 680 | 47 | 9800 | timeout (verification) | 900 | 61 | 9500 | done | 1 | 3.4 | 150 | 40 | ||||
| loop-floats-scientific-comp/loop2-1.yml | done | 1 | 4.6 | 300 | 51 | unknown | 1 | 3.7 | 300 | 37 | false(unreach-call) | 1.3 | 42 | 17 | false(unreach-call) | 1.3 | 42 | 16 | couldn't run: all seeds time out or crash | 3.1 | 10 | 42 | done | .13 | 21 | 1.2 | unknown | 1 | 710 | 42 | 11000 | unknown | .49 | 19 | 6.1 | done | 3.7 | 150 | 38 | ||||||
| ../sv-benchmarks/c/ | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) | status | score | cpu (s) | mem (MB) | energy (J) |
| total | 32 | 25 | 2500 | 18000 | 21000 | 32 | 23 | 1800 | 12000 | 15000 | 32 | 6 | 2300 | 3700 | 28000 | 32 | 6 | 2800 | 4400 | 31000 | 32 | 11 | 19000 | 380 | 260000 | 32 | 900 | 730 | 11000 | 32 | 24 | 4500 | 1000 | 61000 | 32 | 1 | 920 | 640 | 9700 | 32 | 30 | 2300 | 5200 | 28000 | |
| Run set | coveritest.test-comp19_prop-coverage-error-call.ReachSafety-Floats | cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Floats | esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Floats | esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Floats | fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Floats | klee.test-comp19_prop-coverage-error-call.ReachSafety-Floats | prtest.test-comp19_prop-coverage-error-call.ReachSafety-Floats | symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Floats | verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Floats | ||||||||||||||||||||||||||||||||||||