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 done .25  23   1500 250 true .25  3.0 270 29 unknown .0  .023 5.7 .10  unknown .0  .028 5.7 .17  done .0   12    25 57   done .25  .13 21 1.3  timeout .25  900    31 13000   done .25  .29 16 3.8 timeout .25  900 150 13000
alias_of_return_2.yml done .75  23   1500 280 true .75  3.2 270 26 unknown .0  .032 5.6 .20  unknown .0  .022 5.7 .081 done .5   19    17 100   done .75  .11 21 1.6  timeout .75  900    31 12000   done .5   .30 16 3.9 timeout .5   900 150 13000
fo_test.yml done 1.0   5.7 280 52 unknown .5   3.8 270 39 unknown .0  .029 5.7 .15  unknown .0  .022 5.6 .15  false(unreach-call) 1.0   8.7  16 32   false(unreach-call) 1.0   .12 21 1.3  done .0   .24 31 3.4 done 1.0   .37 18 5.2 error 1.0   890 170 11000
rule60_list2.c_1.yml done .929 9.1 430 75 unknown .929 4.4 280 44 unknown .0  .023 5.7 .061 unknown .0  .025 5.7 .11  false(unreach-call) .929 14    14 64   false(unreach-call) .929 .12 21 1.7  timeout .714 900    31 13000   done .857 .49 19 5.4 error .929 890 170 11000
rule60_list2.yml done .857 8.6 330 70 true .857 4.3 280 43 unknown .0  .027 5.7 .12  unknown .0  .021 5.7 .043 done .857 18    15 54   done .857 .11 21 1.4  timeout .571 900    31 13000   done .786 .44 18 5.7 timeout .857 900 170 13000
sizeofparameters_test.yml done .5   4.0 270 37 true .5   3.6 270 37 unknown .0  .053 5.6 .14  unknown .0  .019 5.7 .084 couldn't run: all seeds time out or crash .0   .16 11 1.6 done .5   .11 21 1.8  timeout .5   900    31 12000   done .5   .32 16 4.1 timeout .5   900 170 13000
test10.yml done .5   23   1700 260 unknown .5   3.1 260 30 unknown .0  .031 5.7 .15  unknown .0  .029 5.7 .064 done .5   29    16 87   done .5   .12 21 1.2  timeout .5   900    31 13000   done .5   .31 16 2.7 timeout .5   900 150 13000
test11.yml exception .6   3.5 270 29 true .6   3.3 270 35 unknown .0  .025 5.7 .11  unknown .0  .021 5.7 .081 done .5   29    15 85   done .6   .13 22 1.3  timeout .5   900    31 13000   done .5   .34 17 3.7 timeout .6   900 150 12000
test14.yml exception .625 3.8 270 36 unknown .625 3.1 260 32 unknown .0  .023 5.7 .059 unknown .0  .023 5.7 .20  done .5   29    15 91   done .625 .13 21 1.1  timeout .5   900    31 14000   done .5   .33 17 3.7 timeout .5   900 150 12000
test15.yml done .5   23   1500 290 unknown .5   2.9 270 28 unknown .0  .029 5.7 .097 unknown .0  .023 5.6 .14  done .5   19    16 91   done .5   .12 21 1.1  timeout .5   900    31 15000   done .5   .30 16 3.3 timeout .5   900 150 13000
test19.yml done .5   23   1500 280 unknown .5   2.9 260 26 unknown .0  .050 5.6 .080 unknown .0  .025 5.7 .11  done .5   19    16 88   done .5   .13 21 1.1  timeout .5   900    31 13000   done .5   .33 17 3.3 timeout .5   900 150 11000
test21-1.yml done .75  24   700 200 unknown .75  3.3 270 31 unknown .0  .028 5.7 .17  unknown .0  .027 5.7 .18  done .5   31    17 110   done .75  .12 21 1.5  timeout .5   900    30 13000   done .75  .57 19 6.7 timeout .75  900 150 11000
test21-2.yml done .875 24   690 190 unknown .875 3.4 270 34 unknown .0  .022 5.7 .15  unknown .0  .027 5.7 .14  false(unreach-call) .875 16    16 76   false(unreach-call) .875 .11 21 1.6  done .0   .25 31 3.1 done .875 .59 19 8.9 error .875 890 150 13000
test22-1.yml done .833 32   680 320 unknown .833 12   290 150 unknown .0  .023 5.7 .090 unknown .0  .025 5.7 .14  done .333 32    16 110   done .833 .14 21 1.5  timeout .667 900    31 12000   done .833 .63 19 7.2 timeout .75  900 150 11000
test22-2.yml done .917 25   680 200 unknown .917 3.6 280 38 unknown .0  .024 5.7 .15  unknown .0  .030 5.7 .17  false(unreach-call) .917 19    15 52   timeout (false(unreach-call)) .917 900    250 9900    done .667 10    31 150   done .917 .88 19 12   timeout .833 900 150 12000
test23-1.yml timeout .857 900   830 11000 unknown .857 21   340 250 unknown .0  .029 5.7 .17  unknown .0  .047 5.6 .091 false(unreach-call) .857 31    16 71   false(unreach-call) .857 .33 23 4.1  done .429 580    31 8400   done .714 1.1  27 18   error .714 880 150 13000
test23-2.yml done .857 34   690 300 unknown .857 12   300 110 unknown .0  .024 5.7 .36  unknown .0  .019 5.7 .15  done .786 18    14 77   done .857 .31 23 3.7  timeout .714 900    31 14000   done .714 .62 20 8.1 error .714 880 150 11000
test24-1.yml done .875 30   1400 350 unknown .875 12   350 120 unknown .0  .024 5.7 .13  unknown .0  .049 5.7 .090 done .75  10    15 41   done .875 .14 21 1.3  timeout .875 900    31 14000   done .75  .34 19 3.8 timeout .75  900 150 11000
test24-2.yml done .9   27   1900 280 unknown .9   9.8 450 110 unknown .0  .027 5.7 .14  unknown .0  .023 5.7 .16  false(unreach-call) .7   18    13 60   false(unreach-call) .9   .13 24 1.8  timeout .5   900    31 12000   done .8   .41 23 5.0 error .8   890 150 12000
test25-1.yml done 1.0   30   1900 310 unknown 1.0   20   390 220 unknown .0  .053 5.5 .14  unknown .0  .031 5.7 .068 false(unreach-call) .917 13    14 41   false(unreach-call) 1.0   .22 23 2.7  timeout .417 900    30 13000   done .917 .41 22 5.3 error .917 880 150 13000
test25-2.yml timeout .917 900   1700 9900 timeout .75  900   1200 11000 unknown .0  .024 5.7 .074 unknown .0  .023 5.7 .17  done .833 12    13 36   done .917 .20 22 2.3  timeout .417 900    31 12000   done .833 .37 21 4.4 timeout .833 900 150 11000
test28-1.yml done .875 23   730 190 unknown .875 3.2 270 32 unknown .0  .020 5.7 .15  unknown .0  .053 5.8 .089 done .5   28    16 66   false(unreach-call) .875 .13 21 1.1  done .375 710    31 9800   done .875 .46 19 5.8 timeout .875 900 150 11000
test28-2.yml done .875 23   730 210 unknown .875 3.3 270 30 unknown .0  .029 5.7 .11  unknown .0  .022 5.7 .12  done .5   28    17 66   done .875 .13 21 .99 timeout .875 900    31 14000   done .875 .46 19 5.2 timeout .875 900 150 12000
test29-1.yml done 1.0   24   750 200 unknown 1.0   3.0 270 30 unknown .0  .023 5.7 .13  unknown .0  .027 5.7 .12  false(unreach-call) 1.0   8.9  16 34   false(unreach-call) 1.0   .12 21 1.0  done .375 690    31 11000   done 1.0   .32 18 3.9 error 1.0   880 150 11000
test29-2.yml done .875 23   780 200 unknown .875 3.1 270 29 unknown .0  .025 5.7 .10  unknown .0  .029 5.7 .19  done .5   19    16 83   done .875 .14 21 1.0  timeout .875 900    30 12000   done .875 .34 18 4.0 timeout .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