Get-real-time
Read elapsed real time
(Get-real-time state) returns (mv rtime state) where
rtime is the elapsed real (wall clock) time in seconds since the start
of the current ACL2 session. See read-run-time for further
documentation.
Function: get-real-time
(defun get-real-time (state)
(declare (xargs :stobjs state))
(read-run-time state))
