Quoting :doc note-6-5:

  It is now the case that for a call (mbe :logic L :exec E) in a
  :[program] mode function definition, the :exec portion (E) will be
  evaluated (as has always been done in raw Lisp), regardless of the
  setting for guard-checking (see [set-guard-checking]). Formerly, if
  the guard-checking setting was :all or :none, then the :logic value
  (L) was evaluated. An exception holds as before: in safe-mode,
  which is used during evaluation of [defconst], [value-triple], and
  [defpkg] forms, and during macroexpansion. In safe-mode, as before,
  both the :logic and :exec forms are evaluated, and are checked for
  equality. But outside safe-mode, this change can avoid errors due
  to guard-checking of functions with ``invariant-risk'' potential to
  violate a stobj field's type. Thanks to Jared Davis for reporting
  this issue and for helpful chats about it.


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