量词实例化是当前非基元 SMT 求解的主要手段：求解器先生成基元实例，然后使用 CDCL(T) 风格的推理求解得到的基元 SMT 问题。冲突出现时，冲突分析只会学习一条基元子句，尽管冲突本质上来源于非基元子句的实例。事实上，非基元推理能够提供指数级更短的证明。
我们提出了一套演算，包含基元实例化、CDCL(T) 规则以及非基元冲突分析。求解器仍在基元实例上进行推理，但冲突分析的消解步骤在这些实例对应的原始非基元子句上完成。这样得到的学习子句通常比纯基元冲突更一般化，配合合适的策略，甚至可以保证学习子句非冗余。
此外，我们展示了如何在 SMT 求解中加入时间顺序回溯（chronological backtracking），进一步提升求解效率。该演算统一了 CDCL(T) 风格的 SMT 求解、各种基于实例化的过程以及非基元子句学习，并且我们证明它能够模拟 CDCL、SCL(FOL)、SCL(T) 以及传统的分辨率推理。
点评：该工作通过在冲突分析阶段保留非基元信息，实现了更强的学习能力，为 SMT 求解器提供了理论上更紧凑的证明路径，并为实际实现提供了清晰的框架。