anchor.diff:      (and (function-syntax-p first)
            (function-lst-syntax-p rest))))
   
  -(define function-lst-syntax-fix)
  +(define function-lst-syntax-fix ((term function-lst-syntax-p))
  +  :returns (fixed-term function-lst-syntax-p
  +                       :hints (("Goal" :in-theory (enable
  +                                                   function-lst-syntax-p))))
  +  :short "Fixing function for function-lst-syntax-fix"
  +  :verify-guards nil
  +  (mbe :logic (if (consp term)
  +                  (cons (function-syntax-fix (car term))
  +                        (function-lst-syntax-fix (cdr term)))
  +                nil)
  +       :exec term))
  +(verify-guards function-lst-syntax-fix
  +  :hints (("Goal" :in-theory (enable function-lst-syntax-fix
  +  function-syntax-fix function-lst-syntax-p function-syntax-p))))
   
   (define smt-solver-params-p ((term t))
     :returns (syntax-good? booleanp)
     :short "Recognizer for smt-solver-params."
     (true-listp term))
   
  -(define smt-solver-params-fix)
  +(define smt-solver-params-fix ((term smt-solver-params-p))
  +  :returns (fixed-term smt-solver-params-p
  +                       :hints (("Goal" :in-theory (enable smt-solver-params-p))))
  +  :short "Fixing function for smt-solver-params."
  +  (mbe :logic (if (smt-solver-params-p term) term (true-list-fix term))
  +       :exec term))
   
   (defconst *cnf-options*
     '(:interface-dir :SMT-files-dir :SMT-module
  
positive.code:          (function-option-name-lst-p rest))))
  
  (define function-option-name-lst-fix ((option-lst function-option-name-lst-p))
    :returns (fixed-option-name-lst function-option-name-lst-p
                                    :hints (("Goal" :in-theory (enable function-option-name-lst-p))))
    :short "Fixing function for option-name-lst."
    :verify-guards nil
    (mbe :logic (if (atom option-lst)
  
negative.code:     (merge-functions rest (hons-acons name merged-fn master-funcs))))
  
  
    (define combine-hints ((user-hint smtlink-hint-syntax-p) (hint smtlink-hint-p))
      :returns (combined-hint smtlink-hint-p)
      :ignore-ok t
      :irrelevant-formals-ok t
      (b* ((hint (smtlink-hint-fix hint))
           (user-hint (smtlink-hint-syntax-fix user-hint)))
        hint))
  
    (define process-hint ((cl pseudo-term-listp) (user-hint t))
  