limiting the stack depth of the ACL2 rewriter

ACL2 users can create rules of class :rewrite (see rule-classes) that have the potential of causing an infinite loop in the ACL2 rewriter. This could lead to Lisp stack overflows and even segmentation faults. For this reason, the depth of certain calls of functions in the ACL2 rewriter is limited by default using the value of the form (rewrite-stack-limit (w state)). To see the limit in action, execute the following forms.

(defthm app-assoc-1
  (equal (append (append x y) z)
         (append x y z)))
(defthm app-assoc-2
  (equal (append x y z)
         (append (append x y) z)))
(thm (equal (append a b c) xxx)
     ; try without these hints to see a slightly different error message
     :hints (("Goal" :do-not '(preprocess))))
The ensuing error message shows a stack of one greater than the value of (rewrite-stack-limit (w state)), which by default is the value of the constant *default-rewrite-stack-limit*. The error message also explains how to use :brr t and (cw-gstack) to find looping rewrite rules.

This limit can be changed; see set-rewrite-stack-limit.

For a related limit, see backchain-limit.