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-BitVectors cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors klee.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors prtest.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors
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)
bitvector/byte_add-1.yml done 1 33   1100 380 unknown 1 14   310 170 false(unreach-call) 1 .11 27 1.3 false(unreach-call) 1 .12  27 1.2 false(unreach-call) 1 44 18 140 false(unreach-call) 1 .17 21 1.5 unknown 1 .26 31 3.0 done 1 1.1  20 13   done 1 4.1 160 40
bitvector/s3_clnt_1.BV.c.cil-2.yml done 1 9.3 320 82 unknown 1 8.8 360 82 false(unreach-call) 4.1  89 47   false(unreach-call) 2.3   78 35   false(unreach-call) 1 300 17 900 false(unreach-call) 1 .20 23 2.5 timeout 900    31 15000   done 2.9  22 44   done 1 130   200 1600
bitvector/s3_clnt_2.BV.c.cil-2.yml done 1 35   1000 330 unknown 1 18   370 190 false(unreach-call) 4.4  96 54   false(unreach-call) 2.4   82 33   done 26 13 110 false(unreach-call) 1 .59 36 6.6 timeout 900    31 13000   done 3.3  22 46   done 1 670   200 7800
bitvector/s3_clnt_3.BV.c.cil-2.yml done 1 7.2 350 58 unknown 1 6.1 310 56 false(unreach-call) 1.6  57 22   false(unreach-call) .85  51 11   done 26 14 120 false(unreach-call) 1 .15 21 3.0 timeout 900    31 10000   done 1.8  20 25   done 1 40   200 430
bitvector/soft_float_1-3.c.cil.yml done 1 23   790 200 unknown 1 4.3 280 42 false(unreach-call) 1 .17 27 2.1 false(unreach-call) 1 .18  27 2.1 false(unreach-call) 1 100 21 550 false(unreach-call) 1 .23 22 2.2 unknown 1 .26 31 2.9 done 1 1.8  21 28   done 1 4.8 170 49
bitvector/soft_float_4-3.c.cil.yml done 1 16   600 130 unknown 1 3.9 280 34 false(unreach-call) 1 .32 27 3.8 false(unreach-call) 1 .32  27 4.0 false(unreach-call) 1 210 23 500 false(unreach-call) 1 .15 21 1.7 unknown 1 .26 31 3.4 done 1 1.7  21 24   done 1 4.3 170 42
bitvector/sum02-1.yml timeout 900   5500 9000 timeout 900   3200 8700 timeout 900    890 11000   timeout 900     640 11000   false(unreach-call) 1 740 10 11000 timeout 900    2400 11000   unknown 1 7.9  31 100   timeout (verification) 900    400 13000   done 1 9.6 150 100
bitvector-regression/recHanoi03-1.yml out of memory 140   15000 1400 error (recursion) 2.8 260 27 false(unreach-call) 1 .63 26 6.1 false(unreach-call) 1 .53  26 5.8 false(unreach-call) 1 690 11 8700 false(unreach-call) 1 .15 21 1.5 error (0) .25 31 3.5 timeout (verification) 900    730 13000   done 1 8.7 150 88
bitvector-loops/diamond_2-1.yml done 1 25   1100 230 unknown 1 3.1 280 31 false(unreach-call) 1 .11 26 1.2 false(unreach-call) 1 .092 27 1.7 false(unreach-call) 1 23 18 80 false(unreach-call) 1 .11 21 1.5 unknown 1 .29 31 2.9 done 1 .63 19 7.6 done 1 3.3 150 37
bitvector-loops/verisec_sendmail_tTflag_arr_one_loop.yml timeout 900   1600 12000 timeout 900   630 15000 false(unreach-call) 1 .26 27 3.1 false(unreach-call) 1 .21  27 2.4 false(unreach-call) 1 39 17 170 false(unreach-call) 1 .21 22 1.7 timeout 900    31 12000   done 1 .97 20 13   done 1 6.2 150 85
../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 10 7 2100 27000 24000 10 7 1900 6300 25000 10 6 910   1300 11000 10 6 910   1000 11000 10 8 2200 160 23000 10 9 900   2600 11000 10 5 3600 310 51000 10 5 1800 1300 27000 10 10 880 1700 10000
Run set coveritest.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors klee.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors prtest.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-BitVectors