Invalid model for QF_BV formula

[muchang]

Hi, for this formula, z3 gives a genuinely invalid model

[569] % z3-4.8.8 model_validate=true small.smt2
sat
sat
sat
(model
 (define-fun c () (_ BitVec 32)
  #x80000003)
 (define-fun b () (_ BitVec 32)
  #x40000000)
 (define-fun d () (_ BitVec 32)
  #xfffffffe)
 (define-fun a () (_ BitVec 32)
  #x00000000)
)
[570] % z3release model_validate=true small.smt2
sat
sat
sat
(error "line 13 column 10: an invalid model was generated")
( 
 (define-fun c () (_ BitVec 32)
  #x00000001)
 (define-fun b () (_ BitVec 32)
  #x00000000)
 (define-fun d () (_ BitVec 32)
  #xfffffffe)
 (define-fun a () (_ BitVec 32)
  #x00000000)
)
[571] %
[571] % cat small.smt2
(declare-fun a () (_ BitVec 32))
(push)
(assert (distinct a (_ bv0 32)))
(check-sat)
(pop)
(check-sat)
(declare-fun b () (_ BitVec 32))
(declare-fun c () (_ BitVec 32))
(declare-fun d () (_ BitVec 32))
(assert (distinct (_ bv0 32) (_ bv1 32)))
(assert (distinct (bvadd d c) (_ bv1 32)))
(assert (= (bvadd (bvmul (_ bv2 32) b) c) (bvadd (bvneg d) (_ bv1 32))))
(check-sat)
(get-model)
[572] %

It might be related to #4824.

Commit: f58618a