(eq2bv unit-subsume-simplify) Invalid model for integer formula

[rainoftime]

Hi, for the following formula, z3 Commit: 223bffd

(set-logic UFNIA)
(set-option :model_validate true)
(declare-fun i4 () Int)
(assert (= 1 i4))
(check-sat-using (then eq2bv unit-subsume-simplify smt))
(get-model)

sat
(error "line 5 column 55: an invalid model was generated")
(
  ;; universe for (_ bv 2):
  ;;   bv!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!0 () (_ bv 2))
  ;; cardinality constraint:
  (forall ((x (_ bv 2))) (= x bv!val!0))
  ;; -----------
  (define-fun i4 () Int
    0)
  (define-fun bv () (_ bv 2)
    #b01)
  (define-fun bv () (_ bv 1)
    #b0)
)

[NikolajBjorner]

UFNIA doesn't know bit-vectors. There were similar "abuse" bugs recently: setting the SMTLIB logic and using tactics that circumvent the logic.