Major Section: ACL2-BUILT-INS
(read-run-time state) returns
(mv runtime state), where
runtime is the elapsed runtime in seconds since the start of the current ACL2
state is the resulting ACL2 state. But
read-run-time can be made to return elapsed realtime (wall clock time)
instead; see get-internal-time.
The logical definition probably won't concern many users, but for
completeness, we say a word about it here. That definition uses the function
read-acl2-oracle, which modifies state by popping the value to return
from its acl2-oracle field.