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-BitVectors cpa-tiger.test-comp19_prop-coverage-branches.ReachSafety-BitVectors esbmc-kind.test-comp19_prop-coverage-branches.ReachSafety-BitVectors esbmc-falsi.test-comp19_prop-coverage-branches.ReachSafety-BitVectors fairfuzz.test-comp19_prop-coverage-branches.ReachSafety-BitVectors klee.test-comp19_prop-coverage-branches.ReachSafety-BitVectors prtest.test-comp19_prop-coverage-branches.ReachSafety-BitVectors symbiotic.test-comp19_prop-coverage-branches.ReachSafety-BitVectors verifuzz.test-comp19_prop-coverage-branches.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 .983 34 810 330 timeout .967 900   10000 11000 unknown .0  .028 5.9 .22  unknown .0  .022 5.7 .12  false(unreach-call) .983  42   17 110 false(unreach-call) .983 .75 23 11   done .7    .26 31 3.3 done .85  1.7  20 21   error .983 880 160 13000
bitvector/byte_add_1-1.yml timeout .733 900 4200 12000 timeout .733 900   8300 9800 unknown .0  .024 5.7 .13  unknown .0  .042 5.7 .11  done .717  21   17 95 done .733 .26 21 2.1 timeout .733  900    30 11000   done .733 .71 20 8.8 error .733 890 160 13000
bitvector/byte_add_2-2.yml timeout .75  900 3700 11000 timeout .717 900   8700 11000 unknown .0  .024 5.7 .060 unknown .0  .025 5.7 .094 done .75   51   19 120 done .75  .23 21 2.4 timeout .75   900    31 14000   done .75  .72 20 10   error .75  890 160 13000
bitvector/gcd_1.yml done .833 29 1400 300 true .833 9.0 290 94 unknown .0  .041 5.6 .076 unknown .0  .028 5.6 .16  done .75   18   16 48 done .833 .14 21 1.7 timeout .833  900    31 11000   done .75  .72 24 10   timeout .75  900 150 12000
bitvector/gcd_2.yml done .9   26 1600 340 unknown .9   8.8 290 110 unknown .0  .046 5.7 .099 unknown .0  .025 5.7 .14  done .9    27   18 100 done .9   3.1  26 38   timeout .9    900    31 13000   done .7   29    45 380   timeout .9   900 150 13000
bitvector/gcd_3.yml done .9   130 1500 1600 unknown .9   93   300 1100 unknown .0  .024 5.7 .090 unknown .0  .025 5.7 .12  done .9    26   17 110 done .9   3.7  27 45   timeout .9    900    31 11000   done .7   35    44 420   timeout .9   900 150 11000
bitvector/interleave_bits.yml done .75  26 2300 290 true .75  10   460 92 unknown .0  .022 5.7 .11  unknown .0  .037 5.6 .061 done .75   20   15 98 done .75  .13 21 1.3 timeout .0    900    31 14000   done .75  .37 19 5.0 timeout .75  900 150 11000
bitvector/modulus-2.yml timeout .9   900 590 13000 timeout .9   900   420 13000 unknown .0  .025 5.7 .073 unknown .0  .024 5.7 .096 timeout .9    900   11 13000 done .9   320    84 4200   timeout .0    900    31 11000   done .8   870    210 11000   timeout .9   900 150 9800
bitvector/num_conversion_2.yml done .833 36 1100 310 true .833 14   440 140 unknown .0  .050 5.6 .085 unknown .0  .027 5.7 .21  done .667  20   16 91 done .833 .39 21 6.2 timeout .0    900    31 13000   done .667 .34 19 4.2 timeout .833 900 150 11000
bitvector/parity.yml done .875 180 2500 1900 unknown .875 120   660 1600 unknown .0  .018 5.7 .029 unknown .0  .022 5.7 .14  done .875  9.1 10 19 done .875 1.2  23 16   timeout .875  900    31 13000   done .75  26    27 350   timeout .875 900 150 12000
bitvector/s3_clnt_1.BV.c.cil-1.yml done .790 220 2300 2400 timeout .599 900   660 14000 unknown .0  .022 5.7 .13  unknown .0  .017 5.7 .17  done .753  270   17 890 done .790 1.7  31 24   timeout .426  900    31 14000   done .698 1.8  21 24   timeout .790 900 200 11000
bitvector/s3_clnt_1.BV.c.cil-2.yml done .926 58 1200 600 true .938 59   710 700 unknown .0  .023 5.7 .090 unknown .0  .026 5.7 .17  false(unreach-call) .790  550   19 2500 timeout (false(unreach-call)) .938 900    540 10000   timeout .426  900    31 13000   done .722 840    490 12000   error .907 890 200 11000
bitvector/s3_clnt_2.BV.c.cil-1.yml done .775 120 2000 1500 timeout .619 900   500 11000 unknown .0  .050 5.7 .084 unknown .0  .023 5.7 .11  done .025  37   13 100 done .775 1.7  31 26   timeout .0188 900    30 15000   done .688 1.7  20 28   timeout .775 900 200 12000
bitvector/s3_clnt_2.BV.c.cil-2.yml done .938 55 1200 610 true .938 33   690 340 unknown .0  .024 5.7 .12  unknown .0  .022 5.8 .11  done .025  26   14 120 timeout (false(unreach-call)) .938 900    450 10000   timeout .0188 900    31 11000   done .762 840    120 8800   error .938 890 200 11000
bitvector/s3_clnt_3.BV.c.cil-1.yml done .778 270 3600 3200 timeout .611 900   860 13000 unknown .0  .032 5.7 .17  unknown .0  .023 5.6 .12  done .0309 40   14 130 done .778 1.7  31 26   timeout .0247 900    31 14000   done .691 1.7  21 27   timeout .778 900 200 9700
bitvector/s3_clnt_3.BV.c.cil-2.yml done .636 140 2200 1900 timeout .549 930   510 12000 unknown .0  .031 5.7 .13  unknown .0  .026 5.6 .22  done .0309 37   14 98 false(unreach-call) .636 .33 23 4.7 timeout .0370 900    31 12000   done .568 1.1  20 13   error .636 890 200 12000
bitvector/s3_srvr_1.BV.c.cil.yml done .782 180 2400 2100 unknown .782 330   640 4200 unknown .0  .023 5.7 .17  unknown .0  .027 5.6 .19  timeout .771  900   21 3000 timeout .787 900    580 9900   timeout .383  900    31 12000   done .718 840    970 10000   timeout .787 900 210 11000
bitvector/s3_srvr_1_alt.BV.c.cil.yml timeout .0   900 2100 9700 timeout .0   900   600 9500 unknown .0  .030 5.6 .13  unknown .0  .048 5.8 .059 couldn't run: all seeds time out or crash .0    3.2 11 43 timeout .0   900    570 10000   timeout .0    900    31 15000   done .0   840    330 9200   timeout .0   900 210 11000
bitvector/s3_srvr_3.BV.c.cil.yml done .822 120 1600 1300 unknown .822 520   650 7200 unknown .0  .029 5.7 .094 unknown .0  .024 5.6 .12  done .805  590   19 1800 timeout .828 900    310 9500   timeout .391  900    31 13000   done .724 840    130 9800   timeout .822 900 210 9800
bitvector/s3_srvr_3_alt.BV.c.cil.yml done .822 110 1700 1300 timeout .644 900   840 9600 unknown .0  .025 5.6 .12  unknown .0  .035 5.7 .10  done .810  860   20 2800 timeout .828 900    320 9800   timeout .391  900    31 13000   done .736 840    130 10000   timeout .828 900 210 8800
bitvector/soft_float_1-2.c.cil.yml done .689 30 890 250 true .689 19   440 220 unknown .0  .030 5.7 .16  unknown .0  .053 5.6 .11  timeout .662  900   14 13000 done .689 370    260 5000   timeout .689  900    31 11000   done .608 840    120 14000   timeout .689 900 170 11000
bitvector/soft_float_1-3.c.cil.yml done .703 29 750 230 true .703 16   450 170 unknown .0  .025 5.7 .13  unknown .0  .026 5.7 .21  false(unreach-call) .689  170   22 500 false(unreach-call) .703 370    260 5700   done .0    .25 31 3.1 done .622 840    130 11000   error .703 890 160 13000
bitvector/soft_float_2.c.cil.yml done .688 160 2800 1800 true .688 160   890 1900 unknown .0  .025 5.7 .089 unknown .0  .033 5.7 .19  done .625  61   20 480 done .688 93    110 1100   timeout .688  900    31 14000   done .458 3.6  25 51   timeout .688 900 160 12000
bitvector/soft_float_3.c.cil.yml done .708 200 2800 2100 timeout .542 900   1100 6800 unknown .0  .026 5.7 .059 unknown .0  .023 5.6 .13  done .667  230   21 900 done .708 230    210 2600   timeout .604  900    31 13000   done .562 10    31 150   timeout .708 900 160 12000
bitvector/soft_float_4-2.c.cil.yml done .595 310 3000 3800 unknown .571 690   800 8000 unknown .0  .023 5.7 .091 unknown .0  .023 5.8 .15  timeout .571  900   15 13000 done .595 360    260 4000   timeout .595  900    31 12000   done .595 850    43 13000   timeout .595 900 170 11000
bitvector/soft_float_4-3.c.cil.yml done .619 340 4200 3900 unknown .595 580   490 7900 unknown .0  .019 5.7 .17  unknown .0  .025 5.8 .13  false(unreach-call) .595  120   23 520 false(unreach-call) .619 360    260 4600   done .0    .28 30 2.7 done .619 850    49 12000   error .619 890 160 12000
bitvector/soft_float_5.c.cil.yml done .688 160 3700 1800 true .688 160   880 1800 unknown .0  .025 5.7 .082 unknown .0  .025 5.7 .053 done .625  250   22 770 done .688 89    110 1200   timeout .688  900    31 14000   done .479 3.5  25 54   timeout .688 900 160 9700
bitvector/sum02-1.yml timeout .5   900 6500 9600 unknown .5   470   1500 5400 unknown .0  .022 5.7 .11  unknown .0  .030 5.7 .15  false(unreach-call) .875  700   10 9100 timeout .5   900    2400 11000   done .0    7.9  31 96   done .5   840    350 10000   timeout .875 900 150 11000
bitvector/sum02-2.yml timeout .5   900 7400 12000 timeout .5   900   3800 9900 unknown .0  .030 5.6 .084 unknown .0  .027 5.7 .089 done .5    880   10 10000 timeout .5   900    2400 12000   timeout .5    900    31 12000   done .5   840    360 12000   timeout .5   900 150 12000
bitvector-regression/recHanoi03-1.yml out of memory .75  140 15000 1400 error (recursion) .125 2.9 260 24 unknown .0  .031 5.5 .16  unknown .0  .029 5.7 .19  false(unreach-call) .875  680   10 8600 timeout (false(unreach-call)) .875 900    4100 13000   done .125  .25 30 2.9 done .875 840    730 12000   timeout .875 900 150 13000
bitvector-loops/diamond_2-1.yml done 1.0   26 970 210 unknown 1.0   4.9 300 42 unknown .0  .029 5.7 .22  unknown .0  .022 5.7 .097 false(unreach-call) 1.0    19   16 85 false(unreach-call) 1.0   .12 21 1.2 done .0    .24 31 3.4 done 1.0   .40 18 5.0 error 1.0   880 150 13000
bitvector-loops/verisec_sendmail_tTflag_arr_one_loop.yml timeout .875 900 1600 14000 timeout .75  930   540 14000 unknown .0  .020 5.7 .22  unknown .0  .028 5.7 .076 false(unreach-call) 1.0    58   16 210 false(unreach-call) .875 .19 22 1.7 timeout .875  900    31 12000   done .875 .77 20 11   error 1.0   880 150 11000
../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 32 24.0 9400 89000 120000 32 22.3  15000 48000 180000 32 .0  .89 180 3.8 32 .0  .89 180 4.2 32 20.9  9400 520 83000 32 24.2  10000 14000 120000 32 12.6 23000 980 330000 32 21.5 12000 4600 160000 32 24.6 29000 5500 370000
Run set coveritest.test-comp19_prop-coverage-branches.ReachSafety-BitVectors cpa-tiger.test-comp19_prop-coverage-branches.ReachSafety-BitVectors esbmc-kind.test-comp19_prop-coverage-branches.ReachSafety-BitVectors esbmc-falsi.test-comp19_prop-coverage-branches.ReachSafety-BitVectors fairfuzz.test-comp19_prop-coverage-branches.ReachSafety-BitVectors klee.test-comp19_prop-coverage-branches.ReachSafety-BitVectors prtest.test-comp19_prop-coverage-branches.ReachSafety-BitVectors symbiotic.test-comp19_prop-coverage-branches.ReachSafety-BitVectors verifuzz.test-comp19_prop-coverage-branches.ReachSafety-BitVectors