Invalid model in default mode about cvc5 HOT 2 CLOSED

(set-logic ALL)
(set-option :incremental true)
(declare-const i2 Int)
(declare-fun f (Int Int) Int)
(assert (! (forall ((q0 Int) (q1 Int))
            (=> (= (f i2 q0) 0) (= q1 (* i2 q0)))):named IP_3))
(push 1)
(assert (> i2 10))
(check-sat)
(get-model)
(pop 1)
(check-sat)
(get-model)

cvc5 --produce-models --check-model --finite-model-find   test.smt2
sat
(
(define-fun i2 () Int 11)
(define-fun f (($x1 Int) ($x2 Int)) Int 11)
)
unknown
(
(define-fun i2 () Int 11)
(define-fun f (($x1 Int) ($x2 Int)) Int (ite (and (= $x1 11) (= $x2 0)) (- 1) 0))
)

(set-logic ALL)
(declare-const i2 Int)
(declare-fun f (Int Int) Int)
(assert (! (forall ((q0 Int) (q1 Int))
            (=> (= (f i2 q0) 0) (= q1 (* i2 q0)))):named IP_3))
(check-sat)
(get-model)

cvc5 --produce-models --check-model --finite-model-find   test.smt2
sat
(
(define-fun i2 () Int 0)
(define-fun f (($x1 Int) ($x2 Int)) Int (- 1))
)