Major Section: MISCELLANEOUS
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.