How are definitions used?

[nancyday]

Are definitions of functions in Z3 immediately expanded prior to solving or are they expanded as necessary? Is there any value in using definitions from a solving time perspective?

[LeventErkok]

Related discussion at stack-overflow: https://stackoverflow.com/questions/71833499/define-fun-in-smt-solvers

[NikolajBjorner]

You can use define-fun-rec to ensure functions are expanded during solving.
define-fun behaves like a macro.