verification - 用于位向量算法的SMT求解器

我正在计划使用现成的SMT求解器进行C代码符号执行的一些实验，并想知道要使用哪个求解器。看SMT竞赛参赛者仅采用开源系统，将其范围缩小到Beaver，Boolector，CVC3，OpenSMT，Sateen，Sonolar，STP，Verit；这仍然是一长串。

在尝试进一步缩小范围时，我注意到某些系统宣告了处理位向量算术的能力，而其他系统仅宣告了处理一般整数算术的能力。原则上，前者对于C是正确的，其中变量是机器字，而不是无界整数。在实践中有什么不同？如果您尝试将通用整数系统用于此类工作，会发生什么情况？是否存在以下情况之一？

位矢量系统效率稍高，但是您可以使用其中任何一个，都没有问题。

您可以使用带有一些调整的通用整数系统。

对于有符号的int，一般的整数系统是合适的(因为溢出的结果是不确定的)，但对于无符号的，它将给出错误的答案。

通用整数系统对机器字算术不正确，我可以将我的简短 list 缩小为仅提供位向量算术的那些系统。

还有别的吗...？

我尝试过提出一个尽可能具体的问题，但是如果有人可以建议其他任何缩小范围的标准，那就太好了!

最佳答案

我在使用STP进行符号执行方面有丰富的经验。 STP正是为此任务而设计的。另外，有许多符号执行工具已成功地将STP用于此目的，因此有理由相信STP不会烂掉。我绝对会向其他人推荐STP作为此类实验的默认选择。

但是，我还没有尝试过其他系统，所以我不知道STP与它们相比。

我个人认为STP是这种应用程序的基准和默认选择。因此，如果您只有时间尝试一个求解器，那么尝试STP似乎是一个非常合理的选择。

如果我不得不猜测，我的猜测将是支持位向量算法很重要，因为任何大型系统代码都将具有大量执行位运算的代码。另外，我怀疑/担心某些系统代码可能依赖于无符号算术的行为来包装2n模，并且，如果您尝试使用整数对其进行建模，那么您将无法获得C的语义(因为正如您所说，整数对于机器单词算术而言是不正确的)，因此，如果您尝试使用仅整数解算器，则可能会遇到一些困难。但是，对于这些怀疑，我都没有确凿的证据。

P.S. Z3可能也是要添加到您的列表中考虑的竞争者。 (只要它是免费的，您是否真的需要您的求解器是开源的？我希望符号执行工具仅将其用作黑盒，而无需进行修改。)