正如在Dafny GitHub的Wiki中所提到的，当Dafny无法证明程序中的断言时，可能是由于我的程序不正确或者Dafny的不完整性。但我认为Dafny的反例在我尝试理解之后是假的，所以我仍然不知道我的程序是否正确。
我的问题如下。如果我设法使用另一个Boogie后端（例如Corral）使用/print检查来自Dafny的翻译Boogie程序，并且Corral还返回一个模型以使Boogie程序无效，那么这将保证模型反驳我的Dafny程序并且我可以使用它进行调试？或者它仍然可能是假的，所以不要费心去试试吗？
从他们的论文来看，在我看来，Corral和Symbooglix应该保证所提供的模型应该是翻译的Boogie程序的具体反例。所以也许我的问题更多的是关于Dafny程序和翻译的Boogie程序是否在语义上等同。
PS：我尝试将已翻译的bpl文件传递给Corral并检查该bpl中的特定Boogie程序，而Corral只是说它无法找到该程序，所以我在争论是否要让它工作。
另一个后端不太可能在翻译的Boogie文件上有更好的运气，因为不完整的原因是根本的。
例如，Dafny发布了包括序列在内的几种数据结构的公理化，并且已知这些公理化是不完整的。
如果您在理解特定Dafny故障时遇到问题，我建议您询问有关您的特定计划的其他问题，并在可能的情况下包含最小的工作示例。