コマンドを実行し、その実行時間を取得する必要があります。私は gtime を使用していますが、出力は私が望むものとは少し異なります。
gtime は実行結果と実行時間を返します。コマンドの出力（時間のみにする必要があります）を変数に保存し、後で使用する必要があります。コマンドを変更して実行時間のみを取得する方法はありますか?
したがって、以下のコマンドを書くと：
executiontime=$(gtime -f "%U" /Users/Desktop/SemanticLocality/optimathsat-1.6.2-macos-64-bit/bin/optimathsat < file.smt2)
echo "$executiontime"
次に、これは私が得る出力の例です:
sat
(objectives
(misses_80 1)
)
9.94