ACL2 Version 3.6.1 (September, 2009) Notes
NOTE! New users can ignore these release notes, because the documentation has been updated to reflect all changes that are recorded here.
The essential changes to ACL2 since Version 3.6 are the two bug fixes described below. There was also some functionality-neutral code refactoring, as requested by Daron Vroon in support of the ACL2 Sedan (see ACL2-sedan). Also see ReleaseVersionNumbers for a list of books in Version 3.6.1 of ACL2 but not Version 3.6. For changes to existing books rather than additions, see the log entries starting with revision r329 up through revision 350.
Fixed a soundness bug in the handling of ruler-extenders,
specifically in the handling of let-expressions. Thanks to Pete
Manolios, who sent us a proof of
(defun foo (x) (declare (xargs :ruler-extenders :all)) (let ((x (cons t x))) (if (endp (cdr x)) x (cons t (foo (cdr x)))))) (defthm foo-bad nil :hints (("Goal" :use ((:instance foo (x '(3)))) :in-theory (disable foo (foo)))) :rule-classes nil)
Fixed a typo in code supporting ruler-extenders (specifically,
swapped arguments in a recursive call of ACL2 source function