使用 Dafny 在 MVS 中违反断言，但在rise4fun 中进行了验证

Question

https://rise4fun.com/Dafny/ZkKN

此断言未经 Dafny 2.3.0 验证。在 MVS 上，但它在rise4fun 中得到验证，当然还有关于触发器的警告。导致“验证不确定”。

此外，https://rise4fun.com/Dafny/Um6t 不会在rise4fun 中打印“hello”（未运行）。这应该是一些错误，因为没有“断言违规”。 请帮忙？

Answer 1

当我添加 -arith:2 标志时，您的程序会进行验证，该标志会添加算术符号的符号同义词并允许在触发器中使用它们。

编辑： 更一般的答案是您的问题使用非线性算术，这通常是不可判定的。 https://github.com/dafny-lang/dafny/wiki/FAQ 的常见问题解答中有一些关于如何处理这些问题的提示，但是我自己对 Dafny 和非线性算术没有太多经验。

我不知道为什么您的文件以前可以正常工作，但为了调查，您可以将 SMT 编码 Dafny 提要打印到 Z3（请参阅dafny output as SMT file）并比较不同的版本，如果没有差异，可能 Z3 之间存在差异版本。

假设任何工具都没有错误，也许有一种方法可以对您的问题进行不同的编码，它可以在不同的求解器版本之间以更稳定的方式工作。