Z3时序可变性

Question

我在Z3中遇到了一些极端的时序可变性，相同的查询有时要花费几秒钟，有时要花费数小时-讨论的内容更为极端here（并且不对变量名进行任何更改）。这些查询仅涉及整数和布尔变量。这仅仅是使用随机化的试探法的正常结果吗？

Answer 1

应该在https://github.com/Z3Prover/z3/issues处提交一张票证，并且至少让开发人员看一下，然后以一种或另一种方式认为。您的示例越小越好。您当然也可以在此处发布它。