Invalid model issue related to options

[r0ayane]

Hi! For the following instance, z3 with options smt.ematching=false and rewriter.enable_der=false generates an invalid model. I'm not sure whether this is expected.

(set-option :smt.ematching false)
(set-option :rewriter.enable_der false)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun a () (Array Bool Bool))
(assert (xor (select (store a v1 true) false) false))
(assert (distinct (forall ((q Int)) (not v1)) (select a (forall ((q Bool)) q))))
(check-sat)
(get-model)

$ ./z3 reduced.smt model-validate=true
sat
(error "line 8 column 10: an invalid model was generated")
(
  (define-fun v1 () Bool
    (forall ((q Bool)) q))
  (define-fun a () (Array Bool Bool)
    (lambda ((x!1 Bool)) x!1))
  (define-fun v2 () Bool
    false)
)

Version: 4.13.4
Commit: 6f24123