  Recursive algebraic data types (term algebras, ADTs) are one of the most
well-studied theories in logic, and find application in contexts including
functional programming, modelling languages, proof assistants, and
verification. At this point, several state-of-the-art theorem provers and SMT
solvers include tailor-made decision procedures for ADTs, and version 2.6 of
the SMT-LIB standard includes support for ADTs. We study an extremely simple
approach to decide satisfiability of ADT constraints, the reduction of ADT
constraints to equisatisfiable constraints over uninterpreted functions (EUF)
and linear integer arithmetic (LIA). We show that the reduction approach gives
rise to both decision and Craig interpolation procedures in (extensions of)
ADTs.
