z3 - UFBV 类别中的基准

Question

我正在寻找 UFBV 类别中的基准。此类别尚未在 SMT 比赛中直接代表。

当然，大多数 (A)UFLIA 基准可以轻松更改为 UFBV 基准，方法是将未解释的排序更改为位向量排序，将整数算术更改为位向量算术。一个自动化的脚本对我也有帮助。

问候， Aboubakr Achraf El Ghazi

Answer 1

您可以下载论文“有效求解量化位向量公式”中使用的 UFBV（和 BV）基准：

• http://research.microsoft.com/en-us/um/redmond/projects/z3/ufbv.zip
• http://research.microsoft.com/en-us/um/redmond/projects/z3/bv.zip

顺便说一句，这些基准已提交给 SMT-LIB。因此，它们最终将在 SMT-LIB 网站上提供。