Z3 statistics: what does time measure?
I am getting strange statistics results when run Z3 3.1 with -st command option. If you press Ctrl-C, Z3 reports total_time < time. Otherwise, if you wait until Z3 finishes: total_time > time.
- What does "total-time" and "time" measure?
- Is it a bug(minor though)(the difference开发者_开发问答 described above)?
Thanks!
This is a bug in Z3 for Linux (versions 3.0 and 3.1). The bug does not affect the Windows version. The fix will be available in the next release (Z3 3.2). The timer used to track time
is incorrect.
BTW, total-time
measures the total execution time, and time
only the time consumed by the last check-sat command. So, we must have that total-time >= time
.
Remark: this answer has been updated using the feedback provided by Swen Jacobs.
精彩评论