Consider the problem of determining whether a quantifier-free formula phi is
satisfiable in some first-order theory *T*. Shostak's algorithm decides this
problem for a certain class of theories with both interpreted and uninterpreted
functions. We present two new algorithms based on Shostak's method. The first
is a simple subset of Shostak's algorithm for the same class of theories but
without uninterpreted functions. This simplified algorithm is easy to
understand and prove correct, providing insight into how and why Shostak's
algorithm works. The simplified algorithm is then used as the foundation for a
generalization of Shostak's method based on the Nelson-Oppen method for
combining theories.