Soundness Example: BDD Package Bug

Below is the example sent by Rob Sumners, demonstrating the unsoundness of ACL2 (Versions 2.6 and some earlier versions) using a :bdd hint to exploit a bug in the determination of commutative functions.


(defthm append-commutes-special
  (equal (append (list x) nil) (append nil (list x))))

(defthm append-commutes
  (equal (append x y) (append y x))
  :hints (("Goal" :bdd (:vars nil))))

(defthm unsound
  nil 
  :hints (("Goal" :use (:instance append-commutes (x (list 1)) (y (list 2)))))
  :rule-classes nil)