| 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-Recursive | cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | klee.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | prtest.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | ||||||||||||||||||||||||||||||||||||
| 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) |
| recursive/Ackermann02.yml | out of memory | 100 | 15000 | 930 | error (recursion) | 3.0 | 260 | 29 | false(unreach-call) | 1 | .22 | 29 | 2.7 | false(unreach-call) | 1 | .18 | 28 | 2.4 | false(unreach-call) | 1 | 110 | 20 | 660 | false(unreach-call) | 1 | .12 | 21 | 1.4 | timeout | 900 | 30 | 15000 | done | 1 | .58 | 19 | 7.6 | done | 1 | 3.5 | 150 | 38 | |||
| recursive/Addition02.yml | out of memory | 100 | 15000 | 970 | error (recursion) | 2.9 | 260 | 22 | false(unreach-call) | 1 | .13 | 26 | 2.2 | false(unreach-call) | 1 | .13 | 26 | 1.5 | false(unreach-call) | 1 | 16 | 16 | 82 | false(unreach-call) | 1 | .15 | 20 | 1.1 | error (0) | .24 | 31 | 3.4 | done | 1 | .56 | 19 | 7.1 | done | 1 | 3.5 | 150 | 37 | |||
| recursive/BallRajamani-SPIN2000-Fig1.yml | out of memory | 120 | 15000 | 1100 | error (recursion) | 2.9 | 260 | 25 | false(unreach-call) | 1 | .11 | 26 | .87 | false(unreach-call) | 1 | .085 | 26 | .85 | false(unreach-call) | 1 | 9.8 | 17 | 23 | false(unreach-call) | 1 | .13 | 21 | 1.0 | unknown | 1 | .23 | 30 | 3.3 | done | 1 | .48 | 19 | 6.6 | done | 1 | 3.5 | 150 | 37 | ||
| recursive/EvenOdd03.yml | done | 1 | 3.5 | 260 | 33 | error (recursion) | 2.8 | 260 | 26 | false(unreach-call) | 1 | .089 | 26 | .88 | false(unreach-call) | 1 | .13 | 26 | .85 | timeout | 1 | 900 | 10 | 12000 | false(unreach-call) | 1 | .13 | 21 | 1.1 | error (0) | .27 | 31 | 3.2 | done | 1 | .56 | 19 | 7.6 | done | 1 | 3.4 | 150 | 34 | ||
| recursive/Fibonacci04.yml | out of memory | 200 | 15000 | 2200 | error (recursion) | 2.9 | 270 | 23 | false(unreach-call) | 1 | .12 | 26 | 1.3 | false(unreach-call) | 1 | .11 | 26 | 1.3 | timeout | 1 | 900 | 17 | 12000 | false(unreach-call) | 1 | .16 | 21 | 1.0 | error (0) | .25 | 31 | 4.1 | done | 1 | .68 | 19 | 9.0 | done | 1 | 3.4 | 150 | 39 | |||
| recursive/Fibonacci05.yml | out of memory | 210 | 15000 | 2000 | error (recursion) | 3.0 | 270 | 26 | false(unreach-call) | 1 | 3.5 | 96 | 39 | false(unreach-call) | 1 | 3.3 | 95 | 41 | timeout | 1 | 900 | 17 | 11000 | false(unreach-call) | 1 | .18 | 21 | 2.1 | error (0) | .27 | 31 | 2.8 | done | 1 | .93 | 19 | 13 | done | 1 | 46 | 150 | 600 | |||
| recursive/McCarthy91-1.yml | done | 1 | 3.6 | 270 | 32 | error (recursion) | 2.9 | 260 | 25 | false(unreach-call) | 1 | .099 | 26 | .72 | false(unreach-call) | 1 | .085 | 26 | .95 | false(unreach-call) | 1 | 810 | 19 | 11000 | false(unreach-call) | 1 | .12 | 21 | 1.3 | error (0) | .25 | 31 | 3.1 | done | 1 | .54 | 19 | 7.3 | done | 1 | 3.6 | 150 | 36 | ||
| recursive-simple/id2_b3_o2.yml | out of memory | 34 | 15000 | 320 | error (recursion) | 2.9 | 270 | 30 | false(unreach-call) | 1 | .087 | 26 | .94 | false(unreach-call) | 1 | .094 | 26 | 1.0 | false(unreach-call) | 1 | 67 | 17 | 550 | false(unreach-call) | 1 | .13 | 21 | 1.1 | error (0) | .26 | 31 | 3.1 | done | 1 | .56 | 19 | 6.9 | done | 1 | 3.2 | 150 | 37 | |||
| recursive-simple/id_b3_o2-2.yml | out of memory | 35 | 15000 | 350 | error (recursion) | 2.9 | 260 | 25 | false(unreach-call) | 1 | .087 | 26 | .94 | false(unreach-call) | 1 | .090 | 26 | 1.2 | false(unreach-call) | 1 | 70 | 17 | 410 | false(unreach-call) | 1 | .12 | 21 | 1.3 | error (0) | .26 | 31 | 3.0 | done | 1 | .53 | 19 | 6.2 | done | 1 | 3.7 | 150 | 37 | |||
| recursive-simple/id_o10.yml | out of memory | 34 | 15000 | 360 | error (recursion) | 2.9 | 260 | 27 | false(unreach-call) | 1 | .10 | 26 | 1.4 | false(unreach-call) | 1 | .12 | 26 | 1.1 | false(unreach-call) | 1 | 19 | 18 | 100 | false(unreach-call) | 1 | .15 | 21 | .94 | error (0) | .26 | 31 | 3.0 | done | 1 | .48 | 19 | 5.3 | done | 1 | 53 | 160 | 630 | |||
| recursive-simple/id_o100.yml | out of memory | 35 | 15000 | 370 | error (recursion) | 2.8 | 260 | 26 | false(unreach-call) | 1 | 2.1 | 33 | 29 | false(unreach-call) | 1 | 1.0 | 27 | 12 | false(unreach-call) | 1 | 29 | 16 | 85 | false(unreach-call) | 1 | .44 | 21 | 5.5 | error (0) | .26 | 31 | 3.0 | done | 1 | .48 | 18 | 5.3 | done | 1 | 590 | 150 | 6200 | |||
| recursive-simple/id_o1000.yml | out of memory | 35 | 15000 | 350 | error (recursion) | 2.8 | 260 | 25 | timeout | 900 | 1200 | 11000 | false(unreach-call) | 1 | 760 | 1000 | 9700 | false(unreach-call) | 1 | 29 | 17 | 75 | false(unreach-call) | 1 | 31 | 79 | 440 | error (0) | .25 | 30 | 3.0 | done | 1 | .50 | 19 | 5.9 | done | 1 | 600 | 150 | 7300 | ||||
| recursive-simple/id_o20.yml | out of memory | 34 | 15000 | 400 | error (recursion) | 2.8 | 260 | 29 | false(unreach-call) | 1 | .16 | 26 | 1.8 | false(unreach-call) | 1 | .13 | 26 | 1.1 | false(unreach-call) | 1 | 28 | 17 | 78 | false(unreach-call) | 1 | .13 | 21 | 1.4 | error (0) | .27 | 31 | 3.1 | done | 1 | .49 | 19 | 8.0 | done | 1 | 53 | 150 | 720 | |||
| recursive-simple/id_o200.yml | out of memory | 34 | 15000 | 340 | error (recursion) | 2.8 | 260 | 25 | false(unreach-call) | 1 | 12 | 84 | 150 | false(unreach-call) | 1 | 6.1 | 58 | 78 | false(unreach-call) | 1 | 28 | 17 | 72 | false(unreach-call) | 1 | 1.1 | 22 | 15 | error (0) | .26 | 30 | 3.2 | done | 1 | .47 | 19 | 5.7 | timeout | 900 | 150 | 10000 | ||||
| recursive-simple/id_o3.yml | out of memory | 34 | 15000 | 320 | error (recursion) | 2.7 | 260 | 21 | false(unreach-call) | 1 | .090 | 26 | 1.0 | false(unreach-call) | 1 | .085 | 26 | 1.1 | false(unreach-call) | 1 | 27 | 18 | 96 | false(unreach-call) | 1 | .12 | 21 | 1.1 | error (0) | .26 | 30 | 3.6 | done | 1 | .47 | 18 | 5.8 | done | 1 | 3.3 | 150 | 33 | |||
| recursive-simple/sum_non_eq-3.yml | done | 1 | 3.7 | 270 | 28 | error (recursion) | 2.7 | 260 | 27 | false(unreach-call) | 1 | .087 | 26 | .90 | false(unreach-call) | 1 | .083 | 26 | .90 | couldn't run: all seeds time out or crash | .14 | 10 | 1.9 | false(unreach-call) | 1 | .12 | 21 | 1.3 | error (0) | .26 | 30 | 2.8 | done | 1 | .49 | 16 | 5.7 | done | 1 | 3.3 | 150 | 30 | |||
| ../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 | 16 | 3 | 1000 | 200000 | 10000 | 16 | 46 | 4200 | 410 | 16 | 15 | 920 | 1700 | 11000 | 16 | 16 | 770 | 1500 | 9800 | 16 | 15 | 3900 | 260 | 49000 | 16 | 16 | 34 | 390 | 480 | 16 | 1 | 900 | 490 | 16000 | 16 | 16 | 8.8 | 300 | 110 | 16 | 15 | 2300 | 2400 | 26000 | |
| Run set | coveritest.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | klee.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | prtest.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Recursive | ||||||||||||||||||||||||||||||||||||