位矢量算法的SMT求解器

Question

我计划用现成的SMT求解器进行C代码的符号执行实验，并想知道使用哪一个求解器；看看SMT竞赛参赛者，只使用开源系统，将其缩小到Beaver、Boolector、CVC3、OpenSMT、Sateen、some、STP、Verit；这仍然是一个很长的列表。

为了进一步缩小范围，我注意到一些系统宣传了处理位向量算法的能力，而另一些系统只宣传了处理一般整数算法的能力。原则上，前者对C是正确的，其中变量是机器单词，而不是无界整数。它在实践中有多大的区别？如果您尝试将通用整数系统用于这类工作，会发生什么情况？是否适用下列方案之一？

1. 一个位向量系统的效率略高，但你可以使用，没有问题。
2. 您可以使用一般整数系统进行一些调整。
3. 对于带符号的int (因为溢出的结果是未定义的)，一般的整数系统是可以的，但是对于无符号的结果会给出错误的答案。
4. 一般的整数系统对机器字算法是不正确的，我可以将我的短列表缩减为那些提供位向量算法的系统。
5. 别的什么.？

我试着提出一个尽可能具体的问题，但如果有人能提出缩小名单的其他标准，那就太好了！

Answer 1

根据2011-08年SMT-Wikipedia的数据，我们有：

基于这些措施，似乎最有活力、组织最完善的项目是OpenSMT、STP和CVC4。

我只是在检查这些东西--到目前为止，这三项似乎都是合理的，再加上较老的CVC -> CVC3。