z3 - Z3 统计：时间衡量什么？

Question

使用 -st 命令选项运行 Z3 3.1 时，我得到了奇怪的统计结果。如果按 Ctrl-C，Z3 报告 total_time < time。否则，如果您等到 Z3 完成：total_time > time。

1. “总时间”和“时间”衡量什么？
2. 它是一个错误（虽然很小）（上面描述的差异）？

谢谢！

Answer 1

这是 Z3 for Linux（版本 3.0 和 3.1）中的一个错误。该错误不影响 Windows 版本。该修复程序将在下一个版本 (Z3 3.2) 中提供。用于跟踪的计时器time不正确。

顺便说一句，total-time测量总执行时间，并且time仅测量最后一个 check-sat 命令消耗的时间。所以，我们必须有那个total-time >= time。

备注：此答案已使用 Swen Jacobs 提供的反馈进行了更新。