Quantified formulas

[zxt5]

If there is a finite model can satisfy an smt theory with quantifiers, can z3 promise to get the SAT and generate a model?
For example, for the famous Monkey Village problem, I run z3 on this:

(set-option :smt.mbqi true)
(set-logic ALL)

(declare-sort M 0)
(declare-sort T 0)
(declare-sort B 0)

(declare-fun own (M B) Bool)
(declare-fun b1 (M) B)
(declare-fun b2 (M) B)
(declare-fun sit (M) T)
(declare-fun partner (M) M)

(assert (forall ((m M)) (and (own m (b1 m)) (own m (b2 m)) (not (= (b1 m) (b2 m))))))
(assert (forall ((m1 M) (m2 M) (b B)) (=> (and (own m1 b) (own m2 b)) (= m1 m2))))
(assert (forall ((t T)) (
    exists ((m1 M) (m2 M) (m3 M)) 
    (and 
        (= (sit m1) t) 
        (= (sit m2) t) 
        (= (sit m3) t) 
        (distinct m1 m2 m3))
)))
(assert (forall ((m1 M) (m2 M) (m3 M) (m4 M) (t T)) (
    => (and (= (sit m1) t) (= (sit m2) t) (= (sit m3) t) (= (sit m4) t)) 
    (not (distinct m1 m2 m3 m4))
)))
(assert (forall ((m M)) (and (not (= (partner m) m)) (= (partner (partner m)) m))))

(check-sat)

I got an unknown instead of SAT. Can z3 solve such problems, or do any other options need to be set?