我计划在 C 代码的符号执行方面进行一些实验，使用现成的 SMT 求解器，并想知道使用哪个求解器；例如，查看 SMT 竞赛的参赛者，仅采用开源系统，将其范围缩小到 Beaver、Boolector、CVC3、OpenSMT、Sateen、Sonolar、STP、Verit；这仍然是一个很长的清单。
试图进一步缩小范围，我注意到一些系统宣传处理位向量算术的能力，而其他系统只宣传处理一般整数算术的能力。原则上，前者对于 C 是正确的，其中变量是机器字，而不是无界整数。它在实践中有多大的不同？如果您尝试使用通用整数系统来完成此类工作，会发生什么情况？以下情况之一是否适用？
位向量系统的效率稍高一些，但您可以使用其中任何一个，没问题。
您可以使用稍作调整的通用整数系统。
一般整数系统适用于有符号整数（因为溢出的结果未定义），但会给出无符号的错误答案。
一般的整数系统对于机器字算术来说是不正确的，我可以将我的短名单减少到只有那些提供位向量算术的系统。
还有什么……？
我试图尽可能具体地提出一个问题，但如果有人可以提出任何其他标准来缩小列表范围，那就太好了！
我有使用 STP 进行符号执行的良好经验。STP 正是为此任务而设计的。此外，已经有许多符号执行工具成功地将 STP 用于此目的，因此有理由相信 STP 并不糟糕。我肯定会向其他人推荐 STP 作为此类实验的默认选择。
但是，我还没有尝试过其他系统，所以我不知道 STP 与它们相比如何。
就个人而言，我将 STP 视为此类应用程序的基线和默认选择。因此，如果您只有时间尝试一个求解器，那么尝试 STP 似乎是一个非常合理的选择。
如果我不得不猜测，我的猜测是位向量算术对支持很重要，因为任何大型系统代码都会有大量执行按位运算的代码。另外，我怀疑/担心某些系统代码可能依赖于无符号算术的行为来包装模 2 n，并且如果您尝试用整数对其进行建模，您将无法正确理解 C 的语义（因为，正如您所说, 整数对于机器字算术来说是不正确的），因此，如果您尝试使用仅整数求解器，您可能会遇到一些困难。但是，对于这些怀疑中的任何一个，我都没有确凿的证据。
PS Z3 也可能是添加到您要考虑的列表中的竞争者。（你真的需要你的求解器是开源的，只要它是免费的？我希望符号执行工具只会将它用作黑盒，无需修改。）
根据SMT-Wikipedia在 2011-08，我们有：
根据这些衡量标准，最活跃、组织最完善的项目似乎是 OpenSMT、STP 和 CVC4。
我只是在检查这些东西——到目前为止，这三个似乎都是合理的，加上旧的 CVC -> CVC3。