Avoiding infinite loops in the ACL2 rewriter
Matt Kaufmann
ACL2 Seminar 1/15/03
Here is an example using ACL2 Version 2.8 (development version).
ACL2 !>(defthm app-assoc-1
(equal (append (append x y) z)
(append x y z)))
....
Time: 0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)
APP-ASSOC-1
ACL2 !>(defthm app-assoc-2
(equal (append x y z)
(append (append x y) z)))
....
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
APP-ASSOC-2
ACL2 !>(thm (equal (append a b c) xxx))
HARD ACL2 ERROR in PREPROCESS: The call depth limit of 1000 has been
exceeded in the ACL2 preprocessor (a sort of rewriter). There is probably
a loop caused by some set of enabled simple rules. To see why the
limit was exceeded, execute
:brr t
and next retry the proof with :hints
:do-not '(preprocess)
and then execute the form (cw-gstack). See :DOC rewrite-stack-limit.
ACL2 Error in TOP-LEVEL: Evaluation aborted. You *MAY* be able to
see a trace of calls leading up to this violation by executing (wet