(set-logic QF_UFBV)
(set-info :status sat)
(declare-sort m 0)
(declare-fun m (m) (_ BitVec 1))
(declare-fun a (m) (_ BitVec 1))
(declare-const s0 m)
(assert (not (= (_ bv0 1) ((_ extract 0 0) (a s0)))))
(assert (not (= (_ bv1 1) ((_ extract 0 0) (m s0)))))
(declare-const s1 m)
(assert (and (= (a s1) (_ bv0 1)) (= (m s1) (_ bv0 1))))
(declare-const s m)
(assert (= (_ bv1 1) ((_ extract 0 0) (m s))))
(check-sat)