I need to execute a command and get the execution time of it. I am using gtime but the output is a bit different from what I want.
gtime returns the result of the execution and then the execution time. I need to store the output of the command(which I need it to be the time only) in a variable and use it afterward. Is there a way to change the command to get the execution time only?
So if I write the command below:
executiontime=$(gtime -f "%U" /Users/Desktop/SemanticLocality/optimathsat-1.6.2-macos-64-bit/bin/optimathsat < file.smt2)
echo "$executiontime"
then this is an example of the output I get:
sat
(objectives
(misses_80 1)
)
9.94
To get executable time only from the output you can modify your command on such way:
executiontime=$(gtime -f "%U" /Users/ouafaelachhab/Desktop/SemanticLocality/optimathsat-1.6.2-macos-64-bit/bin/optimathsat < file.smt2|tail -1)