Major Section: ACL2-BUILT-INS
(Read-run-time state) returns
(mv runtime state), where runtime is
the elapsed runtime since the start of the current ACL2 session and
is the resulting ACL2 state.
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 returned
runtime value from its acl2-oracle field.