问dafny输出作为SMT文件
EN

Stack Overflow用户

提问于 2019-07-14 08:38:05

回答 1查看 198关注 0票数 0

我成功地编写了一个经过验证的Dafny程序，该程序给出了一个整数数组，返回最长单调前缀的长度。permalink是这里。我希望能够检查SMT文件Dafny使用，即使没有错误。我尝试了各种旗标选项，例如：

$ dafny example_longest_monotone.dfy /useSmtOutputFormat /printModelToFile:smt_file.smt

但似乎都不起作用？我是否错误地认为，在达夫尼成功的情况下，一定有一些返回的底层SMT查询？

回答已采纳

发布于 2019-07-28 02:20:12

输出验证程序输入的命令行标志是/proverLog:<file>。

您还可以打印Dafny使用/print:<file>生成的Boogie文件。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/57025807

复制

相似问题

问dafny输出作为SMT文件EN