Z3统计：什么时间测量？

Question

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

1. “total-time”和“time”是什么措施？
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提供的反馈意见。