ACL2 Version 2.3 (October, 1998) Notes
Versions of ACL2 preceding this one contain a subtle soundness bug! We found a flaw in our detection of subversive-recursions. The bug allowed some subversive recursions to slip through undetected.
We believe it would have been difficult to have exploited this flaw
inadvertently. In particular, the following five conditions are necessary.
(1) Introduce a constrained function, say
(2) In the same encapsulation, define a clique of mutually recursive functions. This clique must be non-
(3) In that mutually recursive clique, use the constrained function
(4) Fail to include the exploited properties of
(5) Later, outside the encapsulation, explicitly use a functional instantiation in which
See subversive-recursions for details.
Less important notes:
We have begun to write some introductory tutorial material for those who wish to learn to program in ACL2. Most of this material is HTML-based. See the Hyper-Card on the ACL2 home page.
The documentation of verify-guards was improved to explain why one
might wish to verify the ``guards'' of a
A bug was fixed in cross fertilization. The bug caused the system to report that it had substituted one term for another when in fact no substitution occurred. The bug was noticed by Bill McCune.