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

Question

我使用Z3 Java来使用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")

Answer 1

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