z3 - Z3 統計: 時間は何を測定するのですか?

Question

-st コマンド オプションを指定して Z3 3.1 を実行すると、奇妙な統計結果が得られます。Ctrl-C を押すと、Z3 は total_time < time を報告します。それ以外の場合、Z3 が終了するまで待つ場合: total_time > time。

1. 「合計時間」と「時間」は何を測定しますか?
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 から提供されたフィードバックを使用して更新されました。