get execution time only from the command gtime

Question

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

Answer 1

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)