(set-logic QF_AUFBV)

(declare-fun x () (_ BitVec 2))
(declare-fun y () (_ BitVec 2))
(declare-fun z () (_ BitVec 2))
(declare-fun m () (_ BitVec 2))

(assert (=> (and (bvult y z) (bvult x y)            ) (= m y)))
(assert (=> (and (bvult y z) (bvuge x y) (bvult x z)) (= m y))) ; fix 'y'->'x'
(assert (=> (and (bvult y z) (bvuge x y) (bvuge x z)) (= m z)))
(assert (=> (and (bvuge y z) (bvugt x y)            ) (= m y)))
(assert (=> (and (bvuge y z) (bvule x y) (bvugt x z)) (= m x)))
(assert (=> (and (bvuge y z) (bvule x y) (bvule x z)) (= m z)))

(declare-fun i () (_ BitVec 2))
(declare-fun j () (_ BitVec 2))
(declare-fun k () (_ BitVec 2))
(declare-fun a () (Array (_ BitVec 2) (_ BitVec 2)))

(assert (and (bvule #b00 i) (bvule i #b10)))
(assert (and (bvule #b00 j) (bvule j #b10)))
(assert (and (bvule #b00 k) (bvule k #b10)))

(assert (= (select a i) x)) 
(assert (= (select a j) y)) 
(assert (= (select a k) z)) 
(assert (bvule (select a #b00) (select a #b01)))
(assert (bvule (select a #b01) (select a #b10)))
(assert (distinct i j k))
(assert (distinct m (select a #b01))) 

(check-sat)
(get-model)
(exit)