Z3統計：什麼時間測量？

Question

當使用-st命令選項運行Z3 3.1時，我得到奇怪的統計結果。如果按Ctrl-C，則Z3會報告total_time <時間。否則，如果您等到Z3完成：total_time> time。

1. 「total-time」和「time」是什麼措施？
2. 這是一個錯誤（儘管小）（上述差異）？

謝謝！

Answer 1

這是Z3 for Linux（版本3.0和3.1）中的一個錯誤。該錯誤不會影響Windows版本。該修補程序將在下一個發行版中提供（Z3 3.2）。用於跟蹤time的計時器不正確。

順便說一句，total-time測量總執行時間，time只有最後一個check-sat命令消耗的時間。所以，我們必須有那total-time >= time。

備註：此答案已更新，使用Swen Jacobs提供的反饋意見。