Programs with recursive data structures, such as list and tree, are widely used in computer science. Program verification problems are often translated into satisfiability modulo theories (SMT) formulas for solving. Recursive data structures are usually converted into first-order logic formulas combining algebraic data types (ADTs) and other theories such as integers. To express properties of recursive data structures, programs often include recursive functions, which in SMT are represented using assertions with quantifiers and uninterpreted functions. This study focuses on solving methods for SMT formulas with both ADTs and recursive functions. Existing techniques are reviewed from three perspectives: SMT solvers, automated theorem provers, and constrained Horn clause (CHC) solvers. Furthermore, the study conducts unified experiments to compare state-of-the-art tools on different benchmarks. It investigates the advantages and limitations of existing solving tools and techniques on various types of problems and explores potential optimization directions, providing valuable analyses and references for researchers.