Refutation soundness issue on UFLIA formula (full-saturate-quant)

[rainoftime]

Hi, for the following formula,
cvc4 901cea3

(set-logic UFLIA)
(define-fun f ((x Int)) Int x)
(define-fun-rec g ((x Int)) Int (ite (<= x 0) 0 (+ (g x) x)))
(declare-fun h (Int) Int)
(push 1)
(assert (forall ((x Int)) (= (h x) 0)))
(check-sat)
(pop 1)

cvc4  --fmf-fun -i xx.smt2 
sat

cvc4  --full-saturate-quant -i xx.smt2 
unsat

z3 xx.smt2 
sat

[zhendongsu]

See #4403

[rainoftime]

(According to #4403,
define-fun-rec does not have the same effect as z3 unless some options such as --fmf-fun are enabled