ACL2 Version 2.6 Patch Page

We have received reports of two soundness bugs in Version 2.6 of ACL2 as well as several earlier versions. Although both are unlikely to affect most users, we describe how they can do so in file bugs.html. We thank Francisco J. Martin-Mateos and Rob Sumners for their email reporting the two bugs, including concise examples and analysis.

You can choose any one of the following options in order to patch your copy of ACL2 Version 2.6.

Download an image built on the repaired sources.
Retrieve these repaired versions of ACL2 Version 2.6 source files:
- bdd.lisp
- prove.lisp
Then rebuild the system (e.g., using make; see the Installation Guide).
Download file patch.lisp and follow these steps:
1. Start up ACL2 Version 2.6.
2. Type :q if your copy of ACL2 puts you in the ACL2 command loop.
3. Evaluate: (acl2-compile-file "patch.lisp" "patch.lisp").
  Quit ACL2.
4. Then in subsequent ACL2 sessions start by evaluating:
```
:q ; only necessary if in ACL2 command loop
(load "patch")
(lp)
```

We apologize for the inconvenience.

Regards,

Matt Kaufmann
J Moore