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-Arrays cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Arrays esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Arrays esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Arrays fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Arrays klee.test-comp19_prop-coverage-error-call.ReachSafety-Arrays prtest.test-comp19_prop-coverage-error-call.ReachSafety-Arrays symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Arrays verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Arrays
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)
array-examples/standard_copy1_ground-2.yml 900 2200 11000 900   7300 11000 900    11000 11000   940    8200 14000   1 900   59 13000 1 1.9  180 28   900    31 15000   1 6.9  420 100 1 3.4 150 36
array-examples/standard_copy2_ground-1.yml 900 2400 12000 900   7200 11000 900    11000 10000   900    10000 10000   1 900   71 11000 1 2.2  190 35   900    31 13000   1 9.3  530 120 1 3.4 150 39
array-examples/standard_copy3_ground-2.yml 900 2700 12000 900   7700 11000 900    11000 9900   940    3600 10000   1 900   72 11000 1 2.6  190 34   900    31 14000   1 10    580 150 1 3.7 150 36
array-examples/standard_copy4_ground-2.yml 900 2800 11000 900   8100 12000 900    11000 9600   900    11000 9900   1 900   79 13000 1 3.1  200 44   900    31 12000   1 11    640 160 1 3.6 150 44
array-examples/standard_copy5_ground-2.yml 900 2800 10000 900   7700 11000 900    11000 9900   900    11000 9400   1 900   63 13000 1 3.5  200 46   900    30 14000   1 13    700 170 1 3.6 150 39
array-examples/standard_copy6_ground-1.yml 900 2700 11000 900   8200 11000 900    11000 12000   900    10000 9700   1 900   74 11000 1 3.9  200 52   900    31 12000   1 13    770 220 1 3.6 150 39
array-examples/standard_copy7_ground-1.yml 900 2700 13000 900   8500 11000 900    11000 11000   900    11000 12000   1 900   62 11000 1 4.4  210 66   900    31 13000   1 15    850 190 1 3.7 150 39
array-examples/standard_copy8_ground-2.yml 900 3100 12000 900   9100 11000 900    11000 10000   900    11000 12000   1 900   65 9900 1 4.8  210 68   900    31 14000   1 16    930 200 1 3.4 150 35
array-examples/standard_copy9_ground-1.yml 900 3300 11000 900   9500 11000 900    11000 11000   900    11000 9600   1 900   79 11000 1 5.4  210 86   900    31 14000   1 17    1000 210 1 3.8 160 40
array-examples/standard_partition_ground-1.yml 900 2200 11000 900   6700 13000 900    4300 12000   900    3500 12000   1.4 14 17 8.3  15000 99   900    31 14000   45    15000 540 1 3.4 150 38
array-industry-pattern/array_ptr_single_elem_init-2.yml 900 1800 12000 930   4900 12000 900    5000 11000   900    4000 11000   1.4 15 15 900    11000 9400   900    35 13000   1 2.0  190 21 1 3.4 150 37
array-industry-pattern/array_single_elem_init.yml 900 2000 12000 900   6800 11000 900    5000 11000   900    3900 11000   900   69 12000 900    11000 8700   900    35 13000   15    15000 220 900   150 11000
reducercommutativity/rangesum.yml 48 940 460 29   540 340 1 1.1  62 15   1 .29 29 3.1 1 730   57 8800 1 .26 41 2.9 .26 31 3.4 1 1.3  23 21 1 4.0 150 37
reducercommutativity/rangesum05.yml 99 2400 980 79   670 830 1 .89 58 11   1 .11 26 1.4 1 11   15 32 1 .14 21 1.2 1 .28 31 2.9 1 .88 64 10 1 3.5 150 33
reducercommutativity/rangesum10.yml 900 3600 8200 900   2200 10000 1 .90 58 11   1 .13 26 1.3 1 8.4 13 27 1 .14 22 2.7 1 .28 31 3.1 1 .91 63 11 1 3.5 150 40
reducercommutativity/rangesum20.yml 900 4400 9800 900   1800 8100 1 1.4  58 15   1 .63 29 7.0 1 8.6 13 37 1 .18 36 3.1 1 .26 31 3.4 1 1.8  65 21 1 3.5 150 39
reducercommutativity/rangesum40.yml 900 4700 10000 900   2300 8900 1 9.3  59 120   1 8.5  45 98   1 14   12 42 1 .21 41 2.2 1 .26 31 3.2 1 7.3  70 100 1 3.5 150 36
reducercommutativity/rangesum60.yml 900 5200 12000 900   4600 8200 1 180    170 2400   1 180    170 2300   1 14   12 52 1 .23 48 2.7 1 .27 31 3.2 1 50    86 620 1 3.5 150 37
array-tiling/mlceu.yml 900 910 10000 900   610 12000 .13 27 1.8 900    160 12000   28   14 120 .16 21 1.2 .20 31 2.8 900    2200 12000 900   150 12000
array-tiling/skippedu.yml 1 23 780 190 1 3.3 280 30 .17 27 1.9 .14 27 1.6 1 900   34 13000 1 .17 21 1.5 .19 31 2.8 1.0  24 14 1 11   150 140
array-programs/copysome1-2.yml 900 2900 10000 900   8200 9800 900    10000 9100   900    9900 9900   3.1 17 45 1 5.1  350 74   900    31 14000   1 25    1200 220 1 3.6 150 33
array-programs/copysome2-2.yml 900 2900 10000 900   8900 11000 900    10000 9600   900    10000 9200   3.1 15 44 1 7.2  530 110   900    31 14000   1 44    1500 360 1 440   4200 6300
../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 22 1 17000 59000 210000 22 1 17000 120000 210000 22 6 13000 130000 150000 22 6 14000 120000 160000 22 16 11000 920 140000 22 18 1900 41000 19000 22 5 13000 680 190000 22 18 1200 42000 16000 22 20 2300 7400 30000
Run set coveritest.test-comp19_prop-coverage-error-call.ReachSafety-Arrays cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Arrays esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Arrays esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Arrays fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Arrays klee.test-comp19_prop-coverage-error-call.ReachSafety-Arrays prtest.test-comp19_prop-coverage-error-call.ReachSafety-Arrays symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Arrays verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Arrays