1

我正在使用 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 二进制文件相同的性能?或者这是一个错误?

4

0 回答 0