我偶尔(不经常，但足够经常(看到一个证明在Dafny中工作，然后一些看起来不相关的东西会改变(例如，变量名、与证明无关的函数定义等(，证明就会中断。
我很想知道发生这种情况的技术原因。我目前对电子匹配和量词实例化有一个大致的了解。对我来说，这些算法应该对这些看似无关的输入特征具有鲁棒性，这一点并不明显；也不清楚为什么它们不会是健壮的。我也不知道在实践中是否有任何考虑因素会导致E匹配实现的不健壮性。
通过"；稳健"；，我的意思是"；将永远成功或永远不会成功，这与变量名等因素无关；。
因此，我有兴趣了解这种非鲁棒性的技术原因(无论是实际的还是理论的(。
我想在这里获得更多直觉的部分原因是，当我遇到这样的情况时，我可以用这样的方式修补证据，使其更加稳健。(相反，现在通常发生的情况是，我会以某种任意的方式修补证据，它会被修复，然后它会在稍后再次损坏。(
我希望找到的答案是类似于"；Z3使用算法X，该算法使用复杂的启发式Y来确定何时放弃在搜索空间的一部分中搜索，并且很明显，Y取决于搜索顺序"；。这样的答案可能不会帮助我写出更好的愚蠢证明，但它会满足我的好奇心。
这些问题都没有简单的答案。下面，我将总结我使用z3的经验。虽然Dafny的人可能会提供其他建议，但我大胆猜测，它适用于现有的所有此类(半(自动化证明工具。
众所周知，即使更改变量名也会使z3响应sat或unknown，请参阅本线程进行讨论。
当你使用Dafny/Boogie等时，它们会对你的程序执行大量转换，即使是简单的更改也会导致后端求解器表现出截然不同的行为。(注意，sat永远不应该变成unsat，反之亦然：这将是一个合法的错误。但事情可能会变成unknown，或者需要非常不同的时间。(下面是另一个讨论类似现象的线程。
根本原因总是要追溯到z3用于该问题的随机种子、选择的启发式方法以及可能影响搜索过程的大量设置。在您的终端上运行z3 -pd。截至今天；参数"；你可以调整！几乎不可能尝试所有相关的选项，更不用说选择"；右"；设置。对"；修改"；为了回归的目的，可以选择性能最好的参数集，但这通常没有帮助，因为问题和求解器不断变化。
通过改变z3参数smt.random_seed=N，您甚至可以在完全相同的问题上获得不同的性能。对于不同的N值，性能可能会有所不同。
因此，作为一名从业者，你真的没什么可做的；不幸地尤其是如果你在z3上使用Dafny/Boogie这样的工具，它会增加自己的魔力。一个简单的想法是使用你的多个核心：用不同的种子、启发式方法、策略等在你的许多核心上启动求解器的许多实例，并选择最快的结果。当然，这说起来容易做起来难。
总之，这些解算器/系统中的大多数都是黑匣子。即使你对它们的内部了解很多，也很难总是"；稳健地"；使用它们。事实上，如果你能够想出一个不受这种差异影响的求解器/证明系统，那么能够做到这一点可能值得一篇博士级的论文。
作为最终用户，假设您使用的是SMTLib；普通的"；您应该注意的技巧和陷阱可以帮助创建性能更好的模型。请参阅此答案以了解概述。
但也没有必要绝望。情况正在好转，与去年相比，今天的解决方案的性能提高了很多倍。SMT竞赛结果是跟踪进度的好方法。
祝你好运！