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 session
and state 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.
