Equinox is an automated reasoning tool for first-order logic. It is also a framework for building highly targeted automated reasoning tools for specific domains.
The aim behind Equinox is to obtain an automated reasoning tool with a modular and extensible architecture. SAT modulo theory (SMT) solvers have the same aim. However, the way in which this aim is realized in Equinox is quite different from the way this is done traditional SMT solvers.