An important component of SMT solving is the theory of equality and uninterpreted functions, which is traditionally modelled in solvers via a congruence closure algorithm. Oftentimes, these algorithms are instrumented to provide machine checkable proofs when determining why two terms are equivalent. In a recent work published at FMCAD’22, Flatt et al. presented a modified congruence closure algorithm that could effectively produce demonstrably shorter proofs. This new algorithm relies on computing redundant equalities, which are not necessary to prove the equivalence between two terms but can provide shorter proofs. While promising, the modified algorithm was only considered in an equality saturation tool. In this work, we have adapted this algorithm to apply it within an SMT solver, and implemented our approach in the state-of-the-art solver cvc5. We discuss the challenges faced when integrating this algorithm into the backtracking nature of an SMT solver, and how we have addressed them. We evaluate our implementation on a large set of SMT-LIB benchmarks from multiple theories, and demonstrate how this new technique can result in smaller SMT proofs, while having only a moderate impact on runtime performance.