Avoid invariant-risk checking for specified functions
See invariant-risk for an introduction to the notion of invariant-risk. Also see set-check-invariant-risk for a way to avoid invariant-risk checking at runtime. The present topic discusses a way to avoid marking specified functions as potentially having invariant-risk.
General Forms: (set-register-invariant-risk t) ; default (set-register-invariant-risk nil) ; requires active trust tag
See community book
Normally a function is marked by ACL2 as having ``invariant-risk'' if its
execution may have the potential to corrupt the ACL2 state. This causes
execution slowdown that is not necessary if there is actually no such
potential. In such cases it may be advisable to instruct ACL2 to avoid
marking that function as having invariant-risk. This can be done by including
To see the current setting (i.e., the default of
Note this utility does not affect whether a stobj primitive is
marked with invariant-risk (which seems too dangerous in general); it only
applies to functions introduced by defun. If you want a version of a
stobj updater that has no invariant-risk and you have invoked
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. Moreover, its effect is to set the ACL2-defaults-table, and hence its effect is local to the book or encapsulate form containing it; see ACL2-defaults-table.