当我使用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