一句话：提出 SLOT，将 SMT 实例翻译为 LLVM IR 并复用编译器优化进行化简，从而实现求解器无关的 SMT 加速。
SMT 求解器是符号执行、程序合成等工具的核心推理引擎，其速度直接影响这些工具的性能与精度。已有加速手段多依赖在特定求解器内部设计新启发式，工程代价高。本文提出一种新视角：SMT-LLVM Optimizing Translation（SLOT），一种与求解器无关的预处理方法，先把 SMT 问题实例翻译到 LLVM IR，借助成熟的编译器优化通道化简，再转换回 SMT 供原求解器求解。作者针对两类最具应用价值的理论——位向量与浮点数——实现了 SLOT。基于标准 SMT-LIB 基准的广泛实验表明，在固定超时下 SLOT 能显著提高可解公式的数量，对大型基准的平均加速接近 3 倍。
SMT solvers are fundamental tools for reasoning about constraints in practical problems like symbolic execution and program synthesis. Faster SMT solving can improve the performance and precision of those analysis tools. Existing approaches typically speed up SMT solving by developing new heuristics inside particular solvers, which requires nontrivial engineering efforts. This paper presents a new perspective on speeding up SMT solving. We propose SMT-LLVM Optimizing Translation (SLOT), a solver-agnostic pre-processing approach that utilizes existing compiler optimizations to simplify SMT problem instances. We implement SLOT for the two most application-critical SMT theories, bitvectors, and floating-point numbers. Our extensive evaluation based on the standard SMT-LIB benchmarks shows that SLOT can substantially increase the number of solvable SMT formulas given fixed timeouts and achieve mean speedups of nearly 3× for large benchmarks.