dafny输出为SMT文件 [英] dafny output as SMT file

问题描述

我成功编写了一个经过验证的Dafny程序，该程序给出了一个整数数组，并返回了最长的单调前缀的长度。永久链接位于此处。我希望能够检查Dafny使用的SMT文件，即使没有错误。我尝试了各种标志选项，例如：

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

但似乎没有一个起作用？我误以为在Dafny成功的情况下，必须有一些底层SMT查询返回了 unsat ？

解决方案

用于输出证明者输入的命令行标志为 / proverLog：< file> 。

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

I successfully wrote a verified Dafny program that given an integer array, returns the length of the longest monotone prefix. The permalink is here. I want to be able to examine the SMT file Dafny used, even though there were no errors. I tried various flag options like:

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

But none seem to work? Am I wrong thinking that there must be some underlying SMT query that returned unsat in the case where Dafny succeeds?

解决方案

The command line flag to output the prover input is /proverLog:<file>.

You can also print the Boogie file that Dafny produces using /print:<file>.

这篇关于dafny输出为SMT文件的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！