## SET-REWRITE-STACK-LIMIT

Sets the rewrite stack depth used by the rewriter
Major Section: EVENTS

Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so
recorded.

Example Forms:
(set-rewrite-stack-limit 30) ; set to small limit
:set-rewrite-stack-limit 30 ; same as above
(set-rewrite-stack-limit *default-rewrite-stack-limit*) ; the default
:set-rewrite-stack-limit (1- (expt 2 28)) ; maximum legal limit
:set-rewrite-stack-limit nil ; same as above -- essentially, no limit

This event sets the maximum stack depth for calls of certain functions that
implement the ACL2 rewriter; see rewrite-stack-limit. It must be a
non-negative integer less than 2^28. A call
`(set-rewrite-stack-limit limit)`

is equivalent to:
(table acl2-defaults-table :rewrite-stack-limit limit).

The use of `acl2-defaults-table`

ensures that this event's effect is
implicitly `local`

to the book or `encapsulate`

form in which it
occurs.
For a different but somewhat related concept, see backchain-limit.