\myheading{Modulo \textit{something}}

There is an idiom: \textit{modulo errors}.

For example:

\begin{framed}
\begin{quotation}
More recently, I learned another useful term: "modulo errors." This is used, for example, as "Q.E.D., modulo errors." One fellow often applied this to his blackboard proofs, meaning: "This is a representative of an equivalence class of proofs, one of which is correct and all of which look sort of like this one. At least one such proof is correct, but it might not be the one I wrote down."
\end{quotation}
\end{framed}
( \url{https://jcdverha.home.xs4all.nl/scijokes/1_7.html} )

Another example:

\begin{framed}
\begin{quotation}
Exact inference aims at solving the tasks in an exact way, modulo errors of computer floating point arithmetic.
\end{quotation}
\end{framed}
( Foundations of Probabilistic Logic Programming: Languages, Semantics ... --- Fabrizio Riguzzi \url{https://books.google.com/books?id=zk-MDwAAQBAJ} )

Donald Knuth uses this term:

\begin{framed}
\begin{quotation}
But if anybody has a significantly better idea, I'm happy to listen --- modulo the situation discussed in [don't send me email].
\end{quotation}
\end{framed}
( \url{https://www-cs-faculty.stanford.edu/~knuth/news98.html} )

Also, there is a tool:
``MCMT: Model Checker Modulo Theories'' ( \url{http://users.mat.unimi.it/users/ghilardi/mcmt/} ).

Now what about ``satisfiability modulo theories''?

Some thinks that means ``satisfiability modulo theories [that are supported by solver]'' or \textit{limited/adjusted/augmented} by them.

\begin{framed}
\begin{quotation}
According to one dictionary, "modulo" means "correcting or adjusting for something."  This is an appropriate definition for its use in satisfiability modulo theories:

First-order logic defines a notion of satisfiability for arbitrary formulas.  In SMT, we use the same definition of satisfiability, but *adjusted* by restricting the set of models we consider to those that also satisfy the theories involved.
\end{quotation}
\end{framed}
( Clark Barrett, \url{https://groups.google.com/u/1/g/smt-lib/c/Jio8V_vc3kU} )\\
\\
Some early mentions of ``SAT Modulo Theories'' term are in the following papers:

\begin{itemize}
\item ``Splitting on Demand in SAT Modulo Theories''
\footnote{\url{http://homepage.divms.uiowa.edu/~tinelli/papers/BarNOT-LPAR-06.pdf}}
(Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli)

\item ``Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)''
\footnote{\url{http://homepage.cs.uiowa.edu/~tinelli/papers/NieOT-JACM-06.pdf}}
(Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli)

\item ``On SAT Modulo Theories and Optimization Problems''
\footnote{\url{https://www.cs.upc.edu/~oliveras/sat06.pdf}}
(Robert Nieuwenhuis, Albert Oliveras)
\end{itemize}

All three are from the year 2006.