Some Issues with Guards and Evaluation in ACL2
Matt Kaufmann
ACL2 seminar, 8/4/04

ACL2 has some fairly elaborate mechanisms for dealing with guards during
evaluation.  In this talk I'll start by providing some relevant background on
how ACL2 uses guards and so-called "safe-mode" during evaluation.  Then I'll
focus on the following issues, which have come up very recently.

Part 1 of talk: A weakness in the current guard-checking mechanism recently
noticed by David Rager, and a proposal for a fix.

Part 2 of talk: A newly-found soundness bug (yes, a proof of nil) related to
safe-mode, and a proposed fix that may, in part, involve elimination of so-call
"small images".

Part 3 of talk: Some statistics on small vs. large images.