In this talk, we propose an approach to generating counterexamples (even more) efficiently in mCRL2. Currently, the mCRL2 glossary of tools has several PBES-level transformations which we cannot use if we also want to extract a counterexample. This means that we have to choose between (a) faster solving times and (b) a visual explanation of the solving outcome. We are working towards making it possible to do both (a) and (b) in one go. This talk will focus on one transformation (redundant parameter elimination), and how to combine it with counterexample generation.