Z3 即使在将交互模式设置为 True 后仍然失败

Question

我正在使用 Z3 Java API 来解决使用该parseSMT2File()方法的 smt 文件。但是，即使我设置params.add("interactive-mode", true)了 then 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")

Answer 1

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