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-Recursive cpa-tiger.test-comp19_prop-coverage-branches.ReachSafety-Recursive esbmc-kind.test-comp19_prop-coverage-branches.ReachSafety-Recursive esbmc-falsi.test-comp19_prop-coverage-branches.ReachSafety-Recursive fairfuzz.test-comp19_prop-coverage-branches.ReachSafety-Recursive klee.test-comp19_prop-coverage-branches.ReachSafety-Recursive prtest.test-comp19_prop-coverage-branches.ReachSafety-Recursive symbiotic.test-comp19_prop-coverage-branches.ReachSafety-Recursive verifuzz.test-comp19_prop-coverage-branches.ReachSafety-Recursive
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)
recursive/Ackermann01-2.yml out of memory .833 100 15000 880 error (recursion) .556 2.9 270 30 unknown .0  .024 5.7 .093 unknown .0  .048 5.7 .14  done .722 58    17 530   timeout .833 900    71 12000   timeout .389  900    31 13000   done .722 840    12000 13000   timeout .722 900 150 13000
recursive/Ackermann02.yml out of memory 1.0   100 15000 920 error (recursion) .438 3.0 270 28 unknown .0  .029 5.7 .16  unknown .0  .025 5.6 .11  false(unreach-call) .875 82    19 390   timeout (false(unreach-call)) 1.0   900    67 11000   timeout .438  900    31 14000   done .812 840    12000 13000   error .875 900 150 11000
recursive/Ackermann03.yml out of memory .944 110 15000 970 error (recursion) .444 2.9 270 27 unknown .0  .029 5.7 .30  unknown .0  .050 5.6 .094 done .833 62    19 350   timeout .944 900    72 13000   timeout .389  900    31 12000   done .611 840    12000 12000   timeout .833 900 150 14000
recursive/Ackermann04.yml out of memory .944 100 15000 990 error (recursion) .444 2.9 260 26 unknown .0  .018 5.6 .16  unknown .0  .042 5.6 .18  done .833 56    17 360   timeout .944 900    71 13000   timeout .389  900    31 12000   done .611 840    12000 12000   timeout .833 900 150 13000
recursive/Addition01-2.yml out of memory .75  190 15000 2200 error (recursion) .75  3.3 270 33 unknown .0  .030 5.7 .14  unknown .0  .034 5.7 .077 done .438 17    17 50   timeout .75  900    320 13000   done .188  .26 30 3.2 timeout (verification) .0   900    120 8100   timeout .625 900 150 10000
recursive/Addition02.yml out of memory .812 190 15000 2100 error (recursion) .812 3.1 270 30 unknown .0  .025 5.7 .10  unknown .0  .023 5.7 .13  false(unreach-call) .625 25    17 69   timeout (false(unreach-call)) .812 900    320 12000   done .188  .25 31 3.8 timeout (verification) .0   900    120 8100   timeout .688 900 150 12000
recursive/Addition03-1.yml out of memory .5   130 15000 1500 error (recursion) .167 3.0 270 26 unknown .0  .030 5.7 .13  unknown .0  .023 5.7 .085 timeout .667 900    11 9100   timeout .833 900    830 14000   done .0    .25 31 3.7 done .417 890    130 9700   timeout .5   900 150 11000
recursive/BallRajamani-SPIN2000-Fig1.yml out of memory 1.0   110 15000 1000 error (recursion) 1.0   2.8 260 28 unknown .0  .026 5.6 .11  unknown .0  .050 5.7 .083 false(unreach-call) 1.0   8.9  16 27   false(unreach-call) 1.0   .12 21 1.2 done .0    .25 31 2.9 done 1.0   .33 18 3.4 error 1.0   890 150 12000
recursive/EvenOdd01-1.yml timeout .786 900 6400 11000 error (recursion) .643 2.9 270 28 unknown .0  .021 5.7 .12  unknown .0  .023 5.7 .18  timeout .714 900    10 14000   timeout .786 900    3900 13000   done .0714 .24 31 4.2 done .786 840    1800 8700   timeout .786 900 150 12000
recursive/EvenOdd03.yml timeout .786 900 6900 10000 error (recursion) .714 3.0 270 24 unknown .0  .028 5.6 .15  unknown .0  .022 5.8 .14  timeout .786 900    11 12000   timeout (false(unreach-call)) .786 900    3900 12000   done .0714 .26 31 3.2 done .357 840    2200 8600   timeout .786 900 150 11000
recursive/Fibonacci01-1.yml out of memory .9   200 15000 2100 error (recursion) .2   2.9 260 29 unknown .0  .027 5.7 .070 unknown .0  .023 5.7 .12  done .9   320    16 4200   timeout .9   900    22 12000   timeout .8    900    31 11000   probably out of memory (killed (signal 9, verification)) .0   780    15000 13000   timeout .8   900 150 12000
recursive/Fibonacci03.yml out of memory .7   250 15000 2200 error (recursion) .6   2.9 270 28 unknown .0  .022 5.7 .062 unknown .0  .018 5.6 .049 done .9   460    18 6100   timeout .9   900    21 12000   timeout .9    900    31 13000   probably out of memory (killed (signal 9, verification)) .0   780    15000 13000   timeout .9   900 150 11000
recursive/Fibonacci04.yml out of memory .625 200 15000 2000 error (recursion) .0   2.7 260 27 unknown .0  .047 5.7 .10  unknown .0  .031 5.7 .12  timeout .875 900    17 14000   timeout (false(unreach-call)) .875 900    1100 11000   done .25   .24 30 4.0 done .875 840    2400 11000   timeout .875 900 150 14000
recursive/Fibonacci05.yml out of memory .625 200 15000 2100 error (recursion) .0   2.9 260 28 unknown .0  .030 5.7 .22  unknown .0  .022 5.7 .15  timeout 1.0   900    17 13000   timeout (false(unreach-call)) 1.0   900    1100 14000   done .25   .25 31 2.9 done .875 840    3100 11000   timeout 1.0   900 150 11000
recursive/McCarthy91-1.yml out of memory .875 120 15000 1200 error (recursion) .375 2.9 270 28 unknown .0  .022 5.7 .15  unknown .0  .036 5.7 .073 false(unreach-call) .875 750    19 11000   timeout (false(unreach-call)) .875 900    350 11000   done .0    .26 31 3.2 done .875 840    230 10000   timeout .875 900 150 12000
recursive/McCarthy91-2.yml out of memory .75  170 15000 1900 error (recursion) .375 2.8 260 24 unknown .0  .024 5.7 .11  unknown .0  .047 5.7 .076 false(unreach-call) .75  730    19 10000   timeout .75  900    47 11000   done .0    .25 31 3.1 done .75  840    230 12000   timeout .75  900 150 17000
recursive/MultCommutative-2.yml timeout .667 900 2000 12000 error (recursion) .389 2.9 260 22 unknown .0  .031 5.7 .083 unknown .0  .019 5.7 .043 done .444 15    16 51   timeout .667 900    830 11000   timeout .667  900    31 14000   done .556 840    46 13000   timeout .556 900 150 12000
recursive/gcd01-1.yml timeout .611 900 1900 12000 error (recursion) .389 3.0 270 26 unknown .0  .030 5.7 .083 unknown .0  .018 5.7 .023 done .611 720    18 9100   timeout .611 900    190 14000   done .611  .35 30 7.2 done .611 860    79 10000   timeout .611 900 150 11000
recursive/gcd02.yml timeout .727 900 1800 12000 error (recursion) .0   3.0 260 30 unknown .0  .029 5.5 .16  unknown .0  .026 5.7 .095 timeout .727 900    12 14000   timeout .727 900    74 14000   done .136  .26 31 3.4 timeout (verification) .0   900    77 11000   timeout .727 900 150 9100
recursive/recHanoi01.yml timeout .9   900 1500 12000 error (recursion) .0   2.9 270 27 unknown .0  .026 5.6 .15  unknown .0  .072 5.7 .14  done .8   710    16 10000   false(valid-deref) .9   860    21 12000   timeout .9    900    31 13000   done .8   840    13000 11000   timeout .8   900 150 11000
recursive/recHanoi02-2.yml out of memory .875 36 15000 370 error (recursion) .625 2.8 270 28 unknown .0  .027 5.6 .21  unknown .0  .021 5.7 .094 done .125 24    17 85   done .875 .13 21 1.6 timeout .875  900    31 12000   done .75  .63 19 7.2 timeout .75  900 160 12000
recursive/recHanoi03-2.yml out of memory .875 150 15000 1500 error (recursion) .625 2.9 270 28 unknown .0  .027 5.7 .096 unknown .0  .030 5.6 .079 done .75  16    16 81   done .875 .17 21 1.4 timeout .875  900    31 14000   done .75  .62 19 8.1 timeout .75  900 150 11000
recursive-simple/id2_b2_o3.yml out of memory .7   35 15000 350 error (recursion) .4   2.8 270 30 unknown .0  .029 5.7 .094 unknown .0  .025 5.7 .13  false(unreach-call) .9   67    17 440   timeout .9   900    500 13000   done .0    .28 31 3.6 done .7   840    860 10000   timeout .9   900 150 11000
recursive-simple/id2_b3_o2.yml out of memory .8   36 15000 350 error (recursion) .4   2.8 260 27 unknown .0  .043 5.5 .089 unknown .0  .023 5.7 .21  false(unreach-call) 1.0   65    17 620   timeout (false(unreach-call)) 1.0   900    650 12000   done .0    .28 31 2.9 done .8   840    980 9600   timeout 1.0   900 150 10000
recursive-simple/id2_b3_o5.yml out of memory .7   36 15000 350 error (recursion) .4   2.9 260 26 unknown .0  .023 5.7 .13  unknown .0  .025 5.7 .011 false(unreach-call) .9   70    17 540   timeout .9   900    650 12000   done .0    .25 31 3.3 done .7   840    840 9600   timeout .9   900 150 11000
recursive-simple/id2_b5_o10.yml out of memory .7   36 15000 370 error (recursion) .4   2.9 270 27 unknown .0  .023 5.7 .17  unknown .0  .028 5.7 .067 false(unreach-call) .9   63    17 510   timeout .9   900    650 12000   done .0    .28 30 3.4 done .7   840    840 9000   timeout .9   900 150 12000
recursive-simple/id_b2_o3.yml out of memory .667 37 15000 400 error (recursion) .0   2.8 260 24 unknown .0  .024 5.7 .062 unknown .0  .021 5.7 .095 false(unreach-call) .833 52    16 290   timeout .833 900    650 12000   done .0    .28 31 2.9 done .667 840    1900 8100   timeout .833 900 150 11000
recursive-simple/id_b3_o2-2.yml out of memory .833 36 15000 370 error (recursion) .333 2.9 270 28 unknown .0  .023 5.7 .11  unknown .0  .022 5.7 .089 false(unreach-call) 1.0   73    17 500   timeout (false(unreach-call)) 1.0   900    3900 11000   done .0    .26 30 3.8 done .833 840    2500 9300   timeout 1.0   900 150 11000
recursive-simple/id_b3_o5-2.yml out of memory .667 35 15000 420 error (recursion) .333 2.8 260 25 unknown .0  .030 5.6 .11  unknown .0  .026 5.6 .14  false(unreach-call) .833 55    17 380   timeout .833 900    3600 11000   done .0    .25 31 3.5 done .667 840    2000 9900   timeout .833 900 150 12000
recursive-simple/id_b5_o10-2.yml out of memory .667 35 15000 360 error (recursion) .333 3.0 260 24 unknown .0  .019 5.6 .16  unknown .0  .022 5.7 .13  false(unreach-call) .833 51    17 330   timeout .833 900    3700 12000   done .0    .26 31 3.1 done .667 840    2000 8900   timeout .833 900 150 11000
recursive-simple/id_o10.yml out of memory .75  35 15000 350 error (recursion) .0   2.7 260 25 unknown .0  .024 5.7 .099 unknown .0  .023 5.6 .12  false(unreach-call) 1.0   19    16 86   timeout (false(unreach-call)) 1.0   900    650 11000   done .0    .26 31 3.0 done 1.0   .31 18 3.9 timeout 1.0   900 150 12000
recursive-simple/id_o100.yml out of memory .75  36 15000 420 error (recursion) .0   2.9 260 26 unknown .0  .023 5.7 .10  unknown .0  .032 5.7 .17  false(unreach-call) 1.0   29    16 88   timeout (false(unreach-call)) 1.0   900    660 11000   done .0    .26 31 3.0 done 1.0   .32 18 3.2 timeout 1.0   900 150 10000
recursive-simple/id_o1000.yml out of memory .75  36 15000 330 error (recursion) .0   2.9 260 24 unknown .0  .040 5.8 .093 unknown .0  .037 5.6 .12  false(unreach-call) 1.0   20    18 87   timeout (false(unreach-call)) 1.0   900    660 13000   done .0    .24 31 3.3 done 1.0   .31 19 3.3 timeout 1.0   900 150 12000
recursive-simple/id_o20.yml out of memory .75  37 15000 360 error (recursion) .0   2.9 260 26 unknown .0  .026 5.7 .14  unknown .0  .048 5.7 .088 false(unreach-call) 1.0   25    18 94   timeout (false(unreach-call)) 1.0   900    650 13000   done .0    .25 31 3.7 done 1.0   .31 18 4.0 timeout 1.0   900 150 10000
recursive-simple/id_o200.yml out of memory .75  36 15000 410 error (recursion) .0   2.9 270 30 unknown .0  .025 5.7 .15  unknown .0  .025 5.6 .091 false(unreach-call) 1.0   24    17 82   timeout (false(unreach-call)) 1.0   900    660 12000   done .0    .25 31 2.9 done 1.0   .32 18 3.8 timeout .75  900 150 11000
recursive-simple/id_o3.yml out of memory .75  35 15000 440 error (recursion) .0   3.0 260 39 unknown .0  .037 5.6 .076 unknown .0  .023 5.7 .11  false(unreach-call) 1.0   28    18 80   timeout (false(unreach-call)) 1.0   900    650 12000   done .0    .27 31 3.1 done 1.0   .33 19 3.5 timeout 1.0   900 150 10000
recursive-simple/sum_non_eq-2.yml out of memory .75  140 15000 1400 error (recursion) .0   2.8 260 25 unknown .0  .018 5.7 .14  unknown .0  .023 5.7 .15  done .5   30    17 89   timeout .75  900    660 12000   done .0    .25 31 4.1 done .5   .31 16 3.5 timeout .75  900 150 10000
recursive-simple/sum_non_eq-3.yml out of memory .75  140 15000 1300 error (recursion) .0   2.8 260 25 unknown .0  .030 5.9 .12  unknown .0  .045 5.7 .11  couldn't run: all seeds time out or crash .0   .13 10 1.8 timeout (false(unreach-call)) .75  900    660 11000   done .0    .26 31 3.2 done .5   .32 16 3.5 timeout .75  900 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 38 29.2 8600 500000 100000 38 12.1 110 10000 1000 38 .0  1.0 220 4.8 38 .0  1.1 220 4.1 38 30.0 10000 620 130000 38 33.3  31000 33000 430000 38 8.39 9000 1200 130000 38 24.9 23000 110000 280000 38 31.5 34000 5800 440000
Run set coveritest.test-comp19_prop-coverage-branches.ReachSafety-Recursive cpa-tiger.test-comp19_prop-coverage-branches.ReachSafety-Recursive esbmc-kind.test-comp19_prop-coverage-branches.ReachSafety-Recursive esbmc-falsi.test-comp19_prop-coverage-branches.ReachSafety-Recursive fairfuzz.test-comp19_prop-coverage-branches.ReachSafety-Recursive klee.test-comp19_prop-coverage-branches.ReachSafety-Recursive prtest.test-comp19_prop-coverage-branches.ReachSafety-Recursive symbiotic.test-comp19_prop-coverage-branches.ReachSafety-Recursive verifuzz.test-comp19_prop-coverage-branches.ReachSafety-Recursive