The meaning of modulo in “formula modulo a background theory”
A theory, in this sense, is an equivalence relation on the formula, which states when these formula are equivalent (as in: $F$ is equivalent to $G$ iff $F$ implies $G$ and $G$ implies $F$). The theory is usually presented by a set of deduction rules, though this is not an obligation.

The word theory is often used in the context of rewriting systems: if you have rules to rewrite terms (which may be formulas, but the concept is more general) of the form $t \rightarrow t'$, then the induced equivalence relation $t_1 (\leftarrow \cup \rightarrow)^* t_2$ (any number of rewriting steps, alternating directions as often as desired) is the equational theory of this rewriting system.

Technically, “first-order formula modulo a theory $T$” means that you are manipulating equivalence classes which are sets of formulas. Intuitively and practically, this is saying that we are manipulating formulas, but we may replace a formula by some other equivalent formula at any time.