布尔条件之外的语义
可满足性模理论（satisfiability modulo theories，SMT）询问：给定公式，是否存在符合某个背景理论的解释，使公式为真？“模理论”意指相对于该理论来判断，不是说所有问题都在做取模运算。背景理论可规定整数或实数算术、数组读写、定长位向量以及未解释函数等符号的含义。
普通布尔可满足性只关心命题的真假组合；SMT还须考虑这些命题内部的关系。例如把“x大于0”和“x小于0”分别抽象成命题p与q，布尔公式p且q允许二者同真，但在通常的实数或整数算术中，两个不等式不可能同时成立。布尔层面没有冲突，不代表理论层面也没有冲突。
布尔搜索与理论检查
一种重要求解架构是DPLL(T)：布尔求解部分组织真假赋值、传播与回溯，理论求解部分检查当前选中的算术条件或其他理论文字是否相容。发现理论冲突后，求解器可以产生理论上成立的子句，把导致矛盾的组合排除，再继续布尔搜索。
以上例而言，算术检查可解释p与q不能同时为真，于是加入“非p或非q”。这并不是随意删去不喜欢的候选解，而是把背景理论提供的必要约束反馈给搜索过程。实际系统还可在部分赋值阶段进行理论传播，并让多个理论求解器交换信息；它们之间的组合也有适用条件，不能任意拼接。
参考：[2]
选择理论就是选择含义
编码程序时，变量属于什么域直接影响答案。方程2x等于1在实数域有解，在整数域无解；固定宽度位向量又不同于无界整数，运算需要遵循其位宽和操作符语义。若把机器运算不加说明地替换成数学整数，求得的结论可能只适用于替代模型。
在验证中，常把程序路径条件与目标性质的否定合在一起，询问是否存在反例。可满足时得到的是模型中的候选反例；不可满足则排除了这组形式约束内的反例。程序的环境、输入限制与内存行为是否编码准确，仍需另外保证。SMT求解器是验证工具的组成部分，不会自行补全未写入公式的现实条件。
结果与能力边界
SMT-LIB为输入语言、背景理论和交互命令提供共同约定。标准区分sat、unsat与unknown：前两者分别报告可满足和不可满足，unknown表示求解器未能作出所需判断，不能当作任一方向的证明。资源耗尽或所采用过程不完备，都可能妨碍求解。
不同理论和公式片段的难度差异很大，是否含量词、是否包含非线性整数运算等，都会改变可判定性或求解策略。因而SMT不是一个保证快速解决全部一阶逻辑的单一算法，而是围绕特定语义组织自动推理的一类问题、方法和工具。