Major Section: RELEASE-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 http://code.google.com/p/acl2-books/wiki/BooksSince36 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 at http://code.google.com/p/acl2-books/source/list 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 nil, essentially as follows. In the termination proof for
foo below, the binding of x to (cons t x) was not substituted
into the recursive call of foo for purposes of the termination proof.
(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
get-ruler-extenders2, which could cause problems for functions defined
using mutual-recursion). Thanks to Daron Vroon for bringing this bug
to our attention, pointing out the swapped arguments.
