z3永远挂？

Question

考虑一下在Klee帮助下生成的以下smt2文件。

我正在尝试使用z3来评估它。然而，z3永远挂起。具体来说，当公式是UNSAT时，z3将永远运行，不会产生任何结果。

1. 公式尺寸大吗？
2. 使用逻辑理论时有什么问题吗？

我可以得到一些改进z3性能的建议吗？

每个assert语句都有一些公共的子表达式。是否可以通过单独求解子表达式来提高z3性能？

Answer 1

这将是不可能回答的，因为您所链接的SMT-lib文件对于非KLEE用户来说是无法破解的。我建议让KLEE的人直接使用你最初的程序，这导致了这一点。如果做不到这一点，请尽量将SMT2Lib降到最低，并看看是否至少可以手工注释，看看它想要做什么。

关于常见子表达式的问题:你必须进行实验才能找到答案。但是，大多数此类求解器的构造方式，它们/将/发现公共子表达式本身，并在它们将您的输入转换为内部表示时自动重用关于它们的引理。所以，如果它能以任何重要的方式用手工完成这件事，我会感到惊讶的；除非输入真的很大。(你联系的例子并没有那么大，所以我怀疑这是个问题。)