即使将交互模式设置为 True，Z3 也会失败答案

【问题标题】：Z3 Failing Even After Setting interactive-mode to True即使将交互模式设置为 True，Z3 也会失败
【发布时间】：2019-11-16 16:21:14
【问题描述】：

我正在使用 Z3 Java API 通过 parseSMT2File() 方法解决 smt 文件。但是，即使我设置params.add("interactive-mode", true)，然后设置solver.setParameters(params)，Z3 也会抛出以下错误：

Exception in thread "main" com.microsoft.z3.Z3Exception: (error "line 276 column 23: model is not available")
(error "line 277 column 26: model is not available")
(error "line 279 column 15: command is only available in interactive mode, use command (set-option :interactive-mode true)")
(error "line 280 column 16: model is not available")

【问题讨论】：

标签： java z3 smt

【解决方案1】：

parseSMT2File() 只解析文件中的断言，并将它们作为一个表达式返回。它不会运行很多命令，包括 check-sat，即您必须在添加了断言的求解器上调用 check()。

【讨论】：

它是否解析声明？
是的，但是没有符号表可以在其中查找声明，必须从解析的表达式中获取。