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:         :define t
          :forward t
          :topic function-lst-syntax-p))
      )
  
    (defsection smt-solver-params
  
negative.code:                                  (hypothesis-syntax-p val))
                          (implies (equal option-type 'hypothesis-lst-syntax-p)
                                   (hypothesis-lst-syntax-p val)))))
          :hints(("Goal"
                  :in-theory (disable lemma2)
                  :use((:instance lemma2 (term (list (car term) (cadr term))))))))
        )
  
      (define function-syntax-p ((term t))
  