Quoting :doc note-6-5:

  We fixed a soundness bug in the case of a [stobj] with a field that
  is a resizable array of stobjs. Thanks to Sol Swords for sending a
  proof of nil exploiting this bug, together with some helpful
  analysis attributing the bug to a mistake in the generated logical
  definition of the corresponding resize function. (His example is
  included in a comment in the form (defxdoc note-6-5 ...) in
  [community-books] file books/system/doc/acl2-doc.lisp.)


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1272 5d84a466-a78b-0930-a311-59b22171a541