Quoting :doc note-6-4:

  Fixed a soundness bug in the handling of hypotheses of conditional
  :[definition] rules invoked during rewriting by applying :[expand]
  [hints]. See (defxdoc note-6-4 ...) in community book
  system/doc/acl2-doc.lisp for a proof of nil in ACL2 Version_6.3
  that exploits this bug.

Quoting the comment mentioned above:

; Here is an example proof of nil exploiting the soundness bug in the handling
; of hypotheses of conditional definition rules invoked during rewriting by
; applying expand hints.

;   (defun e (x y)
;     (iff (booleanp x) (booleanp y)))
;   (defun f (x)
;     (booleanp x))
;   (defun g (x)
;     (if (equal x nil) t x))
;   (defun h (x)
;     (equal x nil))
;   (defthm g-open
;     (implies (h x)
;              (equal (g x) t))
;     :rule-classes :definition)
;   (defequiv e)
;   (defcong e iff (f x) 1)
;   (in-theory (disable f g))
;   (defthm h-rewrite
;     (e (h x) t))
;   (defthm bad
;     (f (g x))
;     :hints (("Goal" :expand ((g x))))
;     :rule-classes nil)
;   (defthm contradiction
;     nil
;     :hints (("Goal" :use ((:instance bad (x 17)))))
;     :rule-classes nil)

Added #+ccl directive for recent addition,
(setq ccl:*trust-paths-from-environment* nil).


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