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
(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
)to find looping rewrite rules.
This limit can be changed; see set-rewrite-stack-limit.
For a related limit, see backchain-limit.