2

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!

Ayrat
  • 1,221
  • 1
  • 18
  • 36

1 Answers1

2

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.

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53