我正在使用 Z3 C-API 来解决一些包含非线性整数算术 (NIA) 约束的问题。我正在为 linux 使用 z3 4.0。当我运行调用 Z3 C-API 的程序时，它会卡在一些问题上，并且不会产生任何答案——sat、unsat 或 unknown。它卡在 Z3_check_and_get_model() 调用中。我尝试运行它超过 10 分钟，但没有得到任何答案。二进制文件继续做一些工作，CPU 使用率几乎是 100%。
我认为这是由于非线性约束而发生的，但是当我在 Z3-SMT 在线以及带有 -smt2 选项的 z3 linux 二进制文件上尝试相同的示例时，它快速为我提供了一个模型的解决方案。尽管在 NIA 领域中的问题相对简单。
我不确定为什么会这样。我是否在这里遗漏了一些东西 - 也许我需要提供一些配置设置才能获得与带有 -smt2 输入的 z3 二进制文件相同的性能？或者这是一个错误？