开发者

Z3 statistics: what does time measure?

开发者 https://www.devze.com 2023-04-03 21:26 出处:网络
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.

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

精彩评论

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

关注公众号