Z3統計情報：時間は何を測定するのですか？

Question

-stコマンドオプションを指定してZ3 3.1を実行すると、奇妙な統計結果が表示されます。 Ctrl-Cを押すと、Z3はtotal_time <時間を報告します。そうでなければ、Z3が終了するまで待つなら、total_time> time。

1. 「合計時間」と「時間」は何を測定するのですか？
2. これはバグですか（マイナーですが）（上記の違い）？

ありがとう！

Answer 1

これは、Z3 for Linux（バージョン3.0および3.1）のバグです。このバグはWindowsのバージョンには影響しません。修正は、次のリリース（Z3 3.2）で利用可能になります。 timeのトラッキングに使用されたタイマーが正しくありません。

BTW、total-timeは合計実行時間を測定し、timeは最後のcheck-satコマンドで費やされた時間のみを測定します。だから、我々はそれを持っている必要がありますtotal-time >= time。

備考：この回答はSwen Jacobsのフィードバックを使用して更新されました。