【发布时间】：2017-02-24 13:15:35
【问题描述】：
dReal SMT 求解器是否返回反例？我见过 :produce-models 为真的例子，但我不知道如何生成反例。此外，dReach 工具有一个 --visualize 选项，因此 dReal 似乎需要生成一些模型信息。但是，当我在 .smt2 文件上运行它时，我似乎找不到查看反例的方法。
【问题讨论】：
【发布时间】：2017-02-24 13:15:35
【问题描述】：
好吧，这很简单:)。 dReal 不遵循使用 (get-model) 的通常 .smt2 约定，但您可以使用命令行选项 --model 获取模型。
例如：dReal --model微波1.smt2
【讨论】：