z3 - Z3中相同代码的不同运行时间

Question

我用了z3的定点，发现定点的运行时间总是不一样的。你有遇到同样的问题吗？为什么会这样？

Answer 1

如果您从相同的状态开始对相同的代码有大量的变化，这听起来很意外。如果您从不同的状态开始（也就是说，如果您在两轮之间通过文本 API 或编程 API 对 Z3 进行了各种调用）。Z3 不应该表现出极大的不确定性行为。非确定性行为可能由错误引起，因此如果您能进一步更准确地描述正在执行它的场景，我们将不胜感激。