macro-finder breaks define-fun-rec

[Elarnon]

This is the follow-up to #5541 which has been closed and I'm not sure is still monitored, so I'm opening a new issue. macro-finder has the same problem with recursive function that was fixed for solve-eqs in #5541; the following input incorrectly returns sat.

(declare-fun W (Int) Int)
(declare-const x Int)
(define-fun-rec rW ((x Int)) Int (W x))
(assert (distinct (rW x) (W x)))
(assert (forall ((y Int)) (= (W y) 10)))

(check-sat-using (then macro-finder smt))