read elapsed runtime
Major Section:  ACL2-BUILT-INS

By default, (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. 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.