Z3 C++API产生&未知&q；，而序列化输出上的二进制产生&unsat&q；

当我使用Z3C++API构建特定的约束集时，得到的响应是"未知"。但是，如果我使用运算符<；<；()序列化z3::solver对象，并将输出传递给Z3二进制文件，它会像预期的那样产生"unsat"。非常有趣的是，如果我使用z3::solver::to_smt2()而不是运算符<；<；()，则Z3二进制输出"未知"。

为什么会发生这种情况？如何使用C++API获取Z3以"看到"独立二进制文件"看到"的内容？

我已将序列化的约束文件上传到pastebin，以防万一

使用运算符<；<；()：http://pastebin.com/uRfP90W5

Using to_smt2()：http://pastebin.com/6qQ6WsHN

---

解决方案

该示例使用的是非线性算法，因此最终使用的是不完整的求解器，尽管它是实数上的非线性算法。您可以使用命令

查询为什么Z3返回UNKNOWN

(GET-INFO：原因-未知)

在(check-sat)调用之后。然后它会说：

(：原因-未知"SMT策略未能显示目标已坐/未坐(不完整(理论算术))")

深入研究该公式，我们可以看到函数应用程序之间的几个乘法。在Z3中，没有使用自由函数对实数和公式进行非线性推理的完全整合。