z3 SMT 求解器 : unknown result after running QF_BVRE benchmark

Question

我刚刚下载了 seq 和 regexp 排序的基准(使用 z3-4.3.2)。运行“membership_1.smt2”后出现未知结果可能是什么问题？

我没有指定任何进一步的命令行选项。根据基准测试，结果应该是 sat，但在没有任何模型的情况下打印出 unknown。

谢谢

编辑:

我进一步注意到，无法识别“重新开始”。这与 z3 的版本有关还是您只是忘记了命令行选项？

Answer 1

首先，我不知道 OP 或评论者在哪里找到“membership_1.smt2”示例输入。我检查了 SMT-LIB benchmarks , 以及 Z3、S3 和 Z3-str 的来源，但找不到。

无论如何，问题在于 OP 正在测试为 S3 编写的基准测试或 Z3-str并针对未修改版本的 Z3 运行它。 S3 和 Z3-str 需要 Z3 的修改版本来处理这些扩展。这在 S3 网站 [S3: A Symbolic String Solver for Web Security Analysis, http://www.comp.nus.edu.sg/~trinhmt/S3/ ，2016 年 8 月 4 日访问]:

Modified Version of Z3 Solver

• The source code of the modified Z3 is available here.
• We modify Z3 to have the interaction between String theory and Arithmetic theory.

• These newly-added API methods allows us to query the length of a string variable, and relationship between the length of different string variables, as shown in our CCS'14 paper.

• Our modified version of Z3 is also used by Z3-str GROUP for integer/string theory integration.

搜索 (unmodified) Z3 source不显示“重新开始”或“重新连接”的匹配项。 Grepping 修改后的版本显示这些标记在 z3-source-060115.zip 的 lib/seq_decl_plugin.cpp 中定义。 .