SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
ESModule

Uses equations (or Boolean assertions) to eliminate variables from the remaining formula. Let the formula have the form $ e \land \varphi' $, then we use knowledge gained from $ e $ to simplify $ \varphi' $. If $ e $ is an arithmetic equation such that we can rewrite it to the form $ x = t $ (with $ x $ a variable) then we substitute $ t $ for $ x $ into $ \varphi' $. Otherwise we simply replace $ e $ with $ true $ in $ \varphi' $. This is done recursively in the formula.