use of define-fun in z3's input language

Question

Going by this post, define-fun seems to be a macro that gets expanded by z3's preprocessor and not seen by the actual solver but makes the input file possibly compact and easier to read. I'm asking because I see some (apparently random) differences in the satisfying assignments and performance on the same problem: one which uses define-funand one which doesn't, which makes me wonder if it is more than just a macro. Does one have to be careful about the aggressive use of define-fun in certain cases? I observed this on some QF_NIRA, QF_LIRA problems that I have.

Answer 1

define-fun is treated as a macro in Z3. The behavior of Z3 will be different if you use equalities and uninterpreted functions. Furthermore, if you use "declare-fun" and then create quantified equalities, the problem is no longer in the QF_LIRA fragment.