How z3 deal with define-fun?

[zxt5]

From the answer of this question , z3 treats the function definition as a macro, and replaces every occurrence of the function with its expression. But the answer is from 9 years ago, so I'm wondering it there any differences from the current z3? How z3 deal with define-fun now?

Thanks!

[NikolajBjorner]

Use define-fun-rec if you want to use use the function declaration inside of an array map. Example,

(define-fun-rec f ((x Int)) Int (+ x 1))

(declare-const A (Array Int Int))
(declare-const B (Array Int Int))

(assert (= ((_ map f) A) B))
(check-sat)
(get-model)

define-fun does is (still) treated as a macro with eager unfolding (= without lazy unfolding).

[zxt5]

Thank you!