一句话：提出 ET，通过将 SMT 理论语法编译为代数数据类型并借助 FEAT 枚举，系统测试 SMT 求解器的正确性与性能。
SMT 求解器虽经广泛测试，仍可能残留正确性缺陷与性能回归。本文提出 ET，一种基于语法的枚举器：将布尔、整数、实数、实整数、位向量、数组、浮点与字符串等 SMT 理论语法编译为代数数据类型，并复用函数式枚举器 FEAT 生成测试公式。ET 在 Z3 与 cvc5 上发现 102 个缺陷，84 个被确认、40 个已修复。作者测试六年间 Z3 和 CVC4/cvc5 的全部 61 个连续版本，用 800 万公式与 4.88 亿次求解调用，发现近期版本正确性提升，但 Z3 自 4.8.11 起在小超时下性能下降，早期 cvc5 在大超时下出现回归。
We introduce ET, a grammar-based enumerator for validating SMT solver correctness and performance. By compiling grammars of the SMT theories to algebraic datatypes, ET leverages the functional enumerator FEAT. ET is highly effective at bug finding and has many complimentary benefits. Despite the extensive and continuous testing of the state-of-the-art SMT solvers Z3 and cvc5, ET found 102 bugs, out of which 84 were confirmed and 40 were fixed. Moreover, ET can be used to understand the evolution of solvers. We derive eight grammars realizing all major SMT theories including the booleans, integers, reals, realints, bit-vectors, arrays, floating points, and strings. Using ET, we test all consecutive releases of the SMT solvers Z3 and CVC4/cvc5 from the last six years (61 versions) on 8 million formulas, and 488 million solver calls. Our results suggest improved correctness in recent versions of both solvers but decreased performance in newer releases of Z3 on small timeouts (since z3-4.8.11) and regressions in early cvc5 releases on larger timeouts. Due to its systematic testing and efficiency, we further advocate ET’s use for continuous integration.
@article{Winterer024,
title = {Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration},
author = {Dominik Winterer and Zhendong Su},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689795}
}