Incorrect model with `smt.bv.solver=2` and an unused `define-fun`

[wingsyuyi-satori]

Z3 Debug build reports sat but generates an invalid model.

The behavior appears to depend on the presence of the unused definition:
(define-fun g () Int 0)
Removing this definition causes Z3 to produce a valid model.

On my machine, changing smt.random_seed to a nonzero value makes the issue disappear: Z3 still reports sat, but model_validate=true no longer reports an invalid model.
Without smt.bv.solver=2, the instance does not finish within 60s timeout.

Input:

(set-option :produce-proofs true)
(define-fun g () Int 0)
(declare-fun f (Int) Int)
(declare-const a Int)
(declare-const d Int)
(declare-const p Int)
(declare-const q Int)
(declare-const n Int)
(declare-const m Int)
(declare-const c Int)
(declare-const r Int)
(assert (and (< 1 q) (= n (* p q)) (< -1 m n)))
(assert (= n (+ (mod a (ite (= n 0) 1 n)) (bv2nat (bvxor ((_ int_to_bv 32) (abs a)) ((_ int_to_bv 32) 1))))))
(assert (= r (+ (mod (f c) (ite (= n 0) 1 n)) (bv2nat (bvxor ((_ int_to_bv 32) (abs (f c))) ((_ int_to_bv 32) (+ c (str.len (str.from_int (abs d))))))))))
(assert (distinct 0 r))
(check-sat)

Output:

$ z3 test.smt2 smt.bv.solver=2 model_validate=true 
sat
(error "line 16 column 10: an invalid model was generated")
(
  (define-fun c () Int
    (- 4294967296))
  (define-fun q () Int
    3)
  (define-fun g () Int
    0)
  (define-fun m () Int
    0)
  (define-fun a () Int
    8589934592)
  (define-fun d () Int
    2)
  (define-fun n () Int
    3)
  (define-fun r () Int
    2147483654)
  (define-fun p () Int
    1)
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    0)
  (define-fun f ((x!0 Int)) Int
    2147483651)
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 2147483651) (= x!1 3)) 715827883
      2863311530))
)

The following excerpts from the -v:11 output may help localize the issue:

line 19:
  bxor 32

line 13806:
  band: (band[32] (if (>= #171 0) (f c) (* -1 #171)) (+ c (if #200 #230 #231))) 1 := 4294967295&1

lines 13832–13846:
  (= r a!3)))) expected: true
  #184: (= r #183) false
  #169: r 2147483654
  #183: (+ #172 #182) 2147483652
  #172: (mod #171 #84) 2
  #182: (ubv_to_int #181) 2147483650
  #181: (bvxor #174 #180) #x80000002
  #174: (int_to_bv[32] #173) #x80000003
  #180: (int_to_bv[32] #179) #x00000001

line 13883:
  (error "line 33 column 10: an invalid model was generated")

-v11.txt

Commit: c9a4a59