anchor.diff:      :short "Set :smt-cnf"
       :measure (len content)
       :hints (("Goal" :in-theory (enable smt-solver-cnf-fix)))
  -    :guard-hints (("Goal" :in-theory (enable smt-solver-cnf-fix smt-solver-cnf-p
  -                                             smt-solver-cnf-p-helper)
  +    :guard-hints (("Goal" :in-theory (e/d (smt-solver-cnf-fix smt-solver-cnf-p
  +                                                              smt-solver-cnf-p-helper)
  +                                          (stringp-of-cadr-of-smt-solver-cnf-p-helper))
                      :use ((:instance stringp-of-cadr-of-smt-solver-cnf-p-helper))
                      ))
       (b* ((hint (smtlink-hint-fix hint))
  
positive.code:                                  (smt-solver-params-p val))
                          (implies (equal option-type 'smt-solver-cnf-p)
                                   (smt-solver-cnf-p val)))))
          :hints(("Goal" :use((:instance lemma2 (term (list (car term) (cadr term))))))))
        )
  
      (encapsulate ()
  
negative.code:         (b* ((ok (smtlink-hint-syntax-p-helper term used)))
            (implies (acl2::set-equiv used-1 used)
                     (equal (smtlink-hint-syntax-p-helper term used-1) ok)))
          :rule-classes(:congruence))
  
        (encapsulate ()
          (local
           (defthm lemma-16
             (implies (and (smtlink-option-name-lst-p used)
  