开发者

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.

  1. What does "total-time" and "time" measure?
  2. 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.

0

上一篇:

下一篇:

精彩评论

暂无评论...
验证码 换一张
取 消

最新问答

问答排行榜