read elapsed runtime
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.