dReal SMT求解器是否会返回反例？我已经看到了以下示例： 生产环境 模型是真的，但我不知道如何生成反例 . 此外，dReach工具有一个--visualize选项，因此看起来dReal需要生成一些模型信息 . 但是，当我在.smt2文件上运行它时，我似乎找不到查看反例的方法 .
哦，这是微不足道的:) . dReal不遵循通常的.smt2使用（get-model）惯例，但您可以使用命令行选项--model获取模型 .
例如：dReal --model microwave1.smt2
1 回答
哦，这是微不足道的:) . dReal不遵循通常的.smt2使用（get-model）惯例，但您可以使用命令行选项--model获取模型 .
例如：dReal --model microwave1.smt2