Unexpected unknown (incomplete quantifiers) for universal formula with uninterpreted functions/sorts

[wilcoxjay]

On the following SMT2-lib query, Z3 nearly immediately returns unknown on current master (294dcf7).

(set-option :smt.mbqi true)

(declare-sort A)
(declare-sort B)
(declare-fun f (A) B)

(assert
 (forall ((b B) (x A) (y A))
         (or (= x y)
             (not (= (f x) b)))))
(declare-fun a1 () A)
(declare-fun a2 () A)
(assert (not (= a1 a2)))
(check-sat)  ; unknown
(get-info :reason-unknown)

This formula falls in the decidable universal fragment with stratified uninterpreted functions, which I believe MBQI should be a decision procedure for. Is this a bug? Is there some other option I should set to get Z3 to try harder on formulas in this fragment?