Here we describe the two soundness bugs in Version 2.6 and several earlier versions of ACL2. If you do not use the :bdd hint or :use hints with :functional-instance, then these bugs will not affect you.
One bug is in the ACL2 bdd package. We are grateful to Rob Sumners for finding
this bug, locating the faulty code, and sending a
concise proof of nil. The problem is with function
commutative-p1 in ACL2 source file file bdd.lisp.
This function attempted to verify the commutativity of a function fn by
searching through rewrite rules of the form (equal (fn u v) (fn v
u)). Unfortunately, we forgot to check that u and
v are variables (and in fact, distinct variables).
The second bug is a problem with our handling of functional instantiation. We are grateful to Francisco J. Martin-Mateos for sending email reporting this bug, including a concise proof of a contradiction and associated analysis. Here is a sketch of how the problem can occur. First, a lemma with a functional instantiation hint, generating unprovable constraints, must be proved by induction after the theorem prover abandoned pursuing goals after seeing the hint. (This means the functional instantiation hint is actually irrelevant: the lemma is proved without it.) Subsequently, a lemma with a functional instantiation hint that generates some of the same unprovable constraints must be proved -- only this time the constraints will be assumed true! In essence, we forgot to ``clear the cache'' of constraints when we reverted to the original goal. So the first lemma put an invalid constraint in the cache and did not clear it out, and the second lemma exploits the presence of the constraint in the cache.