【发布时间】：2011-09-07 21:45:58
【问题描述】：
使用 -st 命令选项运行 Z3 3.1 时，我得到了奇怪的统计结果。如果按 Ctrl-C，Z3 报告 total_time time。
- “总时间”和“时间”衡量什么？
- 这是一个错误（虽然很小）（上述差异）？
谢谢！
【问题讨论】：
标签： z3
【发布时间】：2011-09-07 21:45:58
【问题描述】：
这是 Z3 for Linux（版本 3.0 和 3.1）中的一个错误。该错误不影响 Windows 版本。该修复程序将在下一个版本 (Z3 3.2) 中提供。用于跟踪time 的计时器不正确。
顺便说一句，total-time 测量总执行时间，time 仅测量最后一个 check-sat 命令消耗的时间。所以，我们必须有那个total-time >= time。
备注：此答案已根据 Swen Jacobs 提供的反馈进行了更新。
【讨论】：