anchor.diff:  ;; To be compatible with Arithmetic books
   (include-book "ordinals/lexicographic-ordering-without-arithmetic" :dir :system)
   
  -;; (defsection SMT-goal-generator
  -;;   :parents (Smtlink)
  -;;   :short "SMT-goal-generator generates the three type of goals for the verified clause processor"
  +(defsection SMT-goal-generator
  +  :parents (Smtlink)
  +  :short "SMT-goal-generator generates the three type of goals for the verified clause processor"
   
     (defalist sym-nat-alist
       :key-type symbol
  
positive.code:            ;; We are going to expand all function like this for one level.
             ;; If the function is basic or has already been expanded once.
             ((unless fn)
              (b* (((unless (function-symbolp fn-call (w state)))
                    (prog2$
                     (er hard? 'SMT-goal-generator=>expand "Should be a function call: ~q0" fn-call)
                     a.term-lst))
                   (basic-function (member-equal fn-call *SMT-basic-functions*))
                   ((if (or basic-function (<= a.wrld-fn-len 0)))
                    (cons (cons fn-call (expand (change-ex-args a :term-lst fn-actuals) state))
                          (expand (change-ex-args a :term-lst rest) state)))
                   (formals (formals fn-call (w state)))
                   ((unless (symbol-listp formals))
                    (prog2$
                     (er hard? 'SMT-goal-generator=>expand "Formals should be symbol-listp: ~q0" formals)
                     a.term-lst))
                   (extract-res (meta-extract-formula fn-call state))
                   ((unless (true-listp extract-res))
                    (prog2$
                     (er hard? 'SMT-goal-generator=>expand "Function formula should be true-listp: ~q0" extract-res)
                     a.term-lst))
                   (body (nth 2 extract-res))
                   ((unless (pseudo-termp body))
                    (prog2$
                     (er hard? 'SMT-goal-generator=>expand "Should be a pseudo-termp: ~q0" body)
                     a.term-lst))
                   (expanded-lambda-body
                    (car (expand (change-ex-args a
                                                 :term-lst (list body)
  
negative.code:       )
      )
  
    (verify-guards expand
      :hints (("Goal" :use ((:instance pseudo-term-listp-of-pseudo-lambdap-of-cdar-ex-args->term-lst)))))
  
    (define initialize-fn-lvls ((fn-lst func-alistp))
  