  The first-order theory of finite and infinite trees has been studied since
the eighties, especially by the logic programming community. Following
Djelloul, Dao and Fr\"uhwirth, we consider an extension of this theory with an
additional predicate for finiteness of trees, which is useful for expressing
properties about (not just datatypes but also) codatatypes. Based on their
work, we present a simplification procedure that determines whether any given
(not necessarily closed) formula is satisfiable, returning a simplified formula
which enables one to read off all possible models. Our extension makes the
algorithm usable for algebraic (co)datatypes, which was impossible in their
original work due to restrictive assumptions. We also provide a prototype
implementation of our simplification procedure and evaluate it on instances
from the SMT-LIB.
