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-branches.ReachSafety-Heap cpa-tiger.test-comp19_prop-coverage-branches.ReachSafety-Heap esbmc-kind.test-comp19_prop-coverage-branches.ReachSafety-Heap esbmc-falsi.test-comp19_prop-coverage-branches.ReachSafety-Heap fairfuzz.test-comp19_prop-coverage-branches.ReachSafety-Heap klee.test-comp19_prop-coverage-branches.ReachSafety-Heap prtest.test-comp19_prop-coverage-branches.ReachSafety-Heap symbiotic.test-comp19_prop-coverage-branches.ReachSafety-Heap verifuzz.test-comp19_prop-coverage-branches.ReachSafety-Heap
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/ldv-regression/ 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)
alias_of_return_2.c_1.yml .25  23   1500 250 .25  3.0 270 29 .0  .023 5.7 .10  .0  .028 5.7 .17  .0   12    25 57   .25  .13 21 1.3  .25  900    31 13000   .25  .29 16 3.8 .25  900 150 13000
alias_of_return_2.yml .75  23   1500 280 .75  3.2 270 26 .0  .032 5.6 .20  .0  .022 5.7 .081 .5   19    17 100   .75  .11 21 1.6  .75  900    31 12000   .5   .30 16 3.9 .5   900 150 13000
fo_test.yml 1.0   5.7 280 52 .5   3.8 270 39 .0  .029 5.7 .15  .0  .022 5.6 .15  1.0   8.7  16 32   1.0   .12 21 1.3  .0   .24 31 3.4 1.0   .37 18 5.2 1.0   890 170 11000
rule60_list2.c_1.yml .929 9.1 430 75 .929 4.4 280 44 .0  .023 5.7 .061 .0  .025 5.7 .11  .929 14    14 64   .929 .12 21 1.7  .714 900    31 13000   .857 .49 19 5.4 .929 890 170 11000
rule60_list2.yml .857 8.6 330 70 .857 4.3 280 43 .0  .027 5.7 .12  .0  .021 5.7 .043 .857 18    15 54   .857 .11 21 1.4  .571 900    31 13000   .786 .44 18 5.7 .857 900 170 13000
sizeofparameters_test.yml .5   4.0 270 37 .5   3.6 270 37 .0  .053 5.6 .14  .0  .019 5.7 .084 .0   .16 11 1.6 .5   .11 21 1.8  .5   900    31 12000   .5   .32 16 4.1 .5   900 170 13000
test10.yml .5   23   1700 260 .5   3.1 260 30 .0  .031 5.7 .15  .0  .029 5.7 .064 .5   29    16 87   .5   .12 21 1.2  .5   900    31 13000   .5   .31 16 2.7 .5   900 150 13000
test11.yml .6   3.5 270 29 .6   3.3 270 35 .0  .025 5.7 .11  .0  .021 5.7 .081 .5   29    15 85   .6   .13 22 1.3  .5   900    31 13000   .5   .34 17 3.7 .6   900 150 12000
test14.yml .625 3.8 270 36 .625 3.1 260 32 .0  .023 5.7 .059 .0  .023 5.7 .20  .5   29    15 91   .625 .13 21 1.1  .5   900    31 14000   .5   .33 17 3.7 .5   900 150 12000
test15.yml .5   23   1500 290 .5   2.9 270 28 .0  .029 5.7 .097 .0  .023 5.6 .14  .5   19    16 91   .5   .12 21 1.1  .5   900    31 15000   .5   .30 16 3.3 .5   900 150 13000
test19.yml .5   23   1500 280 .5   2.9 260 26 .0  .050 5.6 .080 .0  .025 5.7 .11  .5   19    16 88   .5   .13 21 1.1  .5   900    31 13000   .5   .33 17 3.3 .5   900 150 11000
test21-1.yml .75  24   700 200 .75  3.3 270 31 .0  .028 5.7 .17  .0  .027 5.7 .18  .5   31    17 110   .75  .12 21 1.5  .5   900    30 13000   .75  .57 19 6.7 .75  900 150 11000
test21-2.yml .875 24   690 190 .875 3.4 270 34 .0  .022 5.7 .15  .0  .027 5.7 .14  .875 16    16 76   .875 .11 21 1.6  .0   .25 31 3.1 .875 .59 19 8.9 .875 890 150 13000
test22-1.yml .833 32   680 320 .833 12   290 150 .0  .023 5.7 .090 .0  .025 5.7 .14  .333 32    16 110   .833 .14 21 1.5  .667 900    31 12000   .833 .63 19 7.2 .75  900 150 11000
test22-2.yml .917 25   680 200 .917 3.6 280 38 .0  .024 5.7 .15  .0  .030 5.7 .17  .917 19    15 52   .917 900    250 9900    .667 10    31 150   .917 .88 19 12   .833 900 150 12000
test23-1.yml .857 900   830 11000 .857 21   340 250 .0  .029 5.7 .17  .0  .047 5.6 .091 .857 31    16 71   .857 .33 23 4.1  .429 580    31 8400   .714 1.1  27 18   .714 880 150 13000
test23-2.yml .857 34   690 300 .857 12   300 110 .0  .024 5.7 .36  .0  .019 5.7 .15  .786 18    14 77   .857 .31 23 3.7  .714 900    31 14000   .714 .62 20 8.1 .714 880 150 11000
test24-1.yml .875 30   1400 350 .875 12   350 120 .0  .024 5.7 .13  .0  .049 5.7 .090 .75  10    15 41   .875 .14 21 1.3  .875 900    31 14000   .75  .34 19 3.8 .75  900 150 11000
test24-2.yml .9   27   1900 280 .9   9.8 450 110 .0  .027 5.7 .14  .0  .023 5.7 .16  .7   18    13 60   .9   .13 24 1.8  .5   900    31 12000   .8   .41 23 5.0 .8   890 150 12000
test25-1.yml 1.0   30   1900 310 1.0   20   390 220 .0  .053 5.5 .14  .0  .031 5.7 .068 .917 13    14 41   1.0   .22 23 2.7  .417 900    30 13000   .917 .41 22 5.3 .917 880 150 13000
test25-2.yml .917 900   1700 9900 .75  900   1200 11000 .0  .024 5.7 .074 .0  .023 5.7 .17  .833 12    13 36   .917 .20 22 2.3  .417 900    31 12000   .833 .37 21 4.4 .833 900 150 11000
test28-1.yml .875 23   730 190 .875 3.2 270 32 .0  .020 5.7 .15  .0  .053 5.8 .089 .5   28    16 66   .875 .13 21 1.1  .375 710    31 9800   .875 .46 19 5.8 .875 900 150 11000
test28-2.yml .875 23   730 210 .875 3.3 270 30 .0  .029 5.7 .11  .0  .022 5.7 .12  .5   28    17 66   .875 .13 21 .99 .875 900    31 14000   .875 .46 19 5.2 .875 900 150 12000
test29-1.yml 1.0   24   750 200 1.0   3.0 270 30 .0  .023 5.7 .13  .0  .027 5.7 .12  1.0   8.9  16 34   1.0   .12 21 1.0  .375 690    31 11000   1.0   .32 18 3.9 1.0   880 150 11000
test29-2.yml .875 23   780 200 .875 3.1 270 29 .0  .025 5.7 .10  .0  .029 5.7 .19  .5   19    16 83   .875 .14 21 1.0  .875 900    30 12000   .875 .34 18 4.0 .875 900 150 13000
../sv-benchmarks/c/ldv-regression/ 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 25 19.4 2300 24000 26000 25 18.7  1000 8200 12000 25 .0  .72 140 3.3 25 .0  .69 140 3.1 25 15.8  480 390 1700 25 19.4  900   770 10000 25 13.0 19000 770 270000 25 18.1 11 470 140 25 18.2 22000 3900 300000
Run set coveritest.test-comp19_prop-coverage-branches.ReachSafety-Heap cpa-tiger.test-comp19_prop-coverage-branches.ReachSafety-Heap esbmc-kind.test-comp19_prop-coverage-branches.ReachSafety-Heap esbmc-falsi.test-comp19_prop-coverage-branches.ReachSafety-Heap fairfuzz.test-comp19_prop-coverage-branches.ReachSafety-Heap klee.test-comp19_prop-coverage-branches.ReachSafety-Heap prtest.test-comp19_prop-coverage-branches.ReachSafety-Heap symbiotic.test-comp19_prop-coverage-branches.ReachSafety-Heap verifuzz.test-comp19_prop-coverage-branches.ReachSafety-Heap