Invalid bvurem simplification for divisor=0

[rainoftime]

Hi, for the following formula,

(set-logic QF_BV)
(set-option :model_validate true)
(set-option :rewriter.bv_urem_simpl true)
(declare-const bv_30-0 (_ BitVec 30))
(assert (xor true true true true (= (_ bv0 30) bv_30-0 (_ bv0 30) (bvsmod bv_30-0 bv_30-0)) true))
(check-sat-using (then simplify dom-simplify lira))

z3 commit dd064a5 gives an invalid model

sat
(error "line 6 column 50: an invalid model was generated")

[rainoftime]

@nunoplopes Can you have a check?

[nunoplopes]

Actually this has nothing to do with dom-simplify. Simplified test case:

(set-option :model_validate true)
(set-option :rewriter.bv_urem_simpl true)
(declare-const x (_ BitVec 30))

(assert (not (and
  (= x (_ bv0 30))
  (= x (bvsmod x x))))
)
(check-sat-using lira)